Add typ to AL TypA

spectec/src/al/ast.ml

@@ -136,7 +136,7 @@ and path' =
 and arg = arg' phrase
 and arg' =
   | ExpA of expr
-  | TypA                (* TODO: Use Il.typ *)
+  | TypA of typ
 
 (* Instructions *)
 

spectec/src/al/eq.ml

@@ -87,7 +87,7 @@ and eq_paths pl1 pl2 = eq_list eq_path pl1 pl2
 and eq_arg a1 a2 =
   match a1.it, a2.it with
   | ExpA e1, ExpA e2 -> eq_expr e1 e2
-  | TypA, TypA -> true
+  | TypA typ1, TypA typ2 -> Il.Eq.eq_typ typ1 typ2
   | _ -> false
 
 and eq_args al1 al2 = eq_list eq_arg al1 al2

spectec/src/al/free.ml

@@ -80,7 +80,7 @@ and free_path path =
 and free_arg arg =
   match arg.it with
   | ExpA e -> free_expr e
-  | TypA -> IdSet.empty
+  | TypA _ -> IdSet.empty
 
 
 (* Instructions *)

spectec/src/al/print.ml

@@ -33,6 +33,8 @@ let rec repeat str num =
 let string_of_atom = El.Print.string_of_atom
 let string_of_mixop = Il.Print.string_of_mixop
 
+let string_of_typ = Il.Print.string_of_typ
+
 
 (* Directions *)
 
@@ -227,7 +229,7 @@ and string_of_paths paths = List.map string_of_path paths |> List.fold_left (^)
 and string_of_arg arg =
   match arg.it with
   | ExpA e -> string_of_expr e
-  | TypA -> "T"
+  | TypA typ -> string_of_typ typ
 
 and string_of_args sep = string_of_list string_of_arg sep
 
@@ -565,7 +567,7 @@ and structured_string_of_paths paths =
 and structured_string_of_arg arg =
   match arg.it with
   | ExpA e -> sprintf "ExpA (%s)" (structured_string_of_expr e)
-  | TypA -> "TypA"
+  | TypA typ -> sprintf "TypA (%s)" (string_of_typ typ)
 
 and structured_string_of_args al = string_of_list structured_string_of_arg ", " al
 

spectec/src/al/valid.ml

@@ -39,7 +39,7 @@ module Set = Free.IdSet
 let bound_set: Set.t ref = ref Set.empty
 let add_bound_var id = bound_set := Set.add id !bound_set
 let add_bound_vars expr = bound_set := Set.union (Free.free_expr expr) !bound_set
-let add_bound_vars_of_arg arg = match arg.it with ExpA e -> add_bound_vars e | TypA -> ()
+let add_bound_vars_of_arg arg = match arg.it with ExpA e -> add_bound_vars e | TypA _ -> ()
 let init_bound_set algo =
   bound_set := Set.empty;
   algo |> Al_util.params_of_algo |> List.iter add_bound_vars_of_arg

spectec/src/al/walk.ml

@@ -18,7 +18,7 @@ type unit_walker = {
 let walk_arg (walker: unit_walker) (arg: arg) : unit =
   match arg.it with
   | ExpA e -> walker.walk_expr walker e
-  | TypA   -> ()
+  | TypA _ -> ()
 
 let walk_iter (walker: unit_walker) (iter: iter) : unit =
   match iter with
@@ -104,7 +104,7 @@ let walk_arg (walker: walker) (arg: arg) : arg =
   let walk_expr = walker.walk_expr walker in
   match arg.it with
   | ExpA e -> { arg with it = ExpA (walk_expr e) }
-  | TypA   -> arg
+  | TypA _ -> arg
 
 let walk_iter (walker: walker) (iter: iter) : iter =
   let walk_expr = walker.walk_expr walker in
@@ -315,7 +315,7 @@ and walk_path f p =
 and walk_arg f a =
   match a.it with
   | ExpA e -> { a with it = ExpA (walk_expr f e) }
-  | TypA   -> a
+  | TypA _ -> a
 
 let rec walk_instr f (instr:instr) : instr list =
   let { pre_instr = pre; post_instr = post; stop_cond_instr = stop_cond; _ } = f in

spectec/src/backend-interpreter/interpreter.ml

@@ -53,7 +53,7 @@ let transpose matrix =
 let extract_exp a =
   match a.it with
   | ExpA e -> Some e
-  | TypA   -> None
+  | TypA _ -> None
 let extract_expargs = List.filter_map extract_exp
 
 

spectec/src/backend-prose/render.ml

@@ -68,7 +68,7 @@ let e2a e = Al.Ast.ExpA e $ e.at
 let a2e a =
   match a.it with
   | Al.Ast.ExpA e -> e
-  | Al.Ast.TypA -> error a.at "Caannot render inverse function with type argument"
+  | Al.Ast.TypA _ -> error a.at "Caannot render inverse function with type argument"
 
 let al_invcalle_to_al_bine e id nl al =
   let efree = (match e.it with Al.Ast.TupE el -> el | _ -> [ e ]) in
@@ -139,12 +139,14 @@ and al_to_el_path pl =
     (fun elp p -> Option.bind elp (fold_path p))
     (Some (El.Ast.RootP $ no_region)) pl
 
-and al_to_el_arg arg = match arg.it with
+and al_to_el_arg arg =
+  match arg.it with
   | Al.Ast.ExpA e ->
     let* ele = al_to_el_expr e in
     Some (El.Ast.ExpA ele)
-  | Al.Ast.TypA ->
-    Some (El.Ast.(TypA (VarT ("TODO" $ arg.at, []) $ arg.at))) (* TODO *)
+  | Al.Ast.TypA _typ ->
+    (* TODO: Require Il.Ast.typ to El.Ast.typ translation *)
+    Some (El.Ast.(TypA (VarT ("TODO" $ arg.at, []) $ arg.at)))
 
 and al_to_el_args args =
   List.fold_left

spectec/src/il2al/translate.ml

@@ -302,7 +302,7 @@ and translate_argexp exp =
 and translate_args args = List.concat_map ( fun arg ->
   match arg.it with
   | Il.ExpA e -> [ ExpA (translate_exp e) $ arg.at ]
-  | Il.TypA _ -> [ TypA $ arg.at ]
+  | Il.TypA typ -> [ TypA typ $ arg.at ]
   | Il.DefA _ -> [] (* TODO: handle functions *)
   | Il.GramA _ -> [] ) args
 
@@ -586,12 +586,12 @@ and call_lhs_to_inverse_call_rhs lhs rhs free_ids =
   let arg2expr a =
     match a.it with
     | ExpA e -> e
-    | TypA   -> error a.at "Cannot translate to inverse function for type argument"
+    | TypA _ -> error a.at "Cannot translate to inverse function for type argument"
   in
   let contains_free a =
     match a.it with
     | ExpA e -> contains_ids free_ids e
-    | TypA   -> false
+    | TypA _ -> false
   in
   let rhs2args e =
     (match e.it with

spectec/src/il2al/transpile.ml

@@ -464,13 +464,13 @@ let is_state expr = match expr.it with
 
 let is_store_arg arg = match arg.it with
   | ExpA e -> is_store e
-  | TypA   -> false
+  | TypA _ -> false
 let is_frame_arg arg = match arg.it with
   | ExpA e -> is_frame e
-  | TypA   -> false
+  | TypA _ -> false
 let is_state_arg arg = match arg.it with
   | ExpA e -> is_state e
-  | TypA   -> false
+  | TypA _ -> false
 
 let hide_state_args args =
   args