Use typ in AL expression

spectec/src/al/ast.ml

@@ -114,15 +114,15 @@ and expr' =
   | IsDefinedE of expr                            (* expr is defined *)
   | MatchE of expr * expr                         (* expr matches expr *)
   (* TODO: use typ *)
-  | HasTypeE of expr * string                     (* the type of expr is ty *)
+  | HasTypeE of expr * typ                     (* the type of expr is ty *)
   | TopFrameE                                     (* "a frame is now on the top of the stack" *)
   | TopLabelE                                     (* "a label is now on the top of the stack" *)
   (* Conditions used in assertions *)
   | TopValueE of expr option                      (* "a value (of type expr)? is now on the top of the stack" *)
   | TopValuesE of expr                            (* "at least expr number of values on the top of the stack" *)
   (* Administrative Instructions *)
   (* TODO: use typ *)
-  | SubE of id * string                           (* varid, with specific type *)
+  | SubE of id * typ                           (* varid, with specific type *)
   | YetE of string                                (* for future not yet implemented feature *)
 
 and path = path' phrase

spectec/src/al/eq.ml

@@ -47,12 +47,12 @@ let rec eq_expr e1 e2 =
   | ContextKindE (a1, e1), ContextKindE (a2, e2) -> El.Atom.eq a1 a2 && eq_expr e1 e2
   | IsDefinedE e1, IsDefinedE e2 -> eq_expr e1 e2
   | MatchE (e11, e12), MatchE (e21, e22) -> eq_expr e11 e21 && eq_expr e12 e22
-  | HasTypeE (e1, t1), HasTypeE (e2, t2) -> eq_expr e1 e2 && t1 = t2
+  | HasTypeE (e1, t1), HasTypeE (e2, t2) -> eq_expr e1 e2 && Il.Eq.eq_typ t1 t2
   | TopLabelE, TopLabelE
   | TopFrameE, TopFrameE -> true
   | TopValueE eo1, TopValueE eo2 -> eq_expr_opt eo1 eo2
   | TopValuesE e1, TopValuesE e2 -> eq_expr e1 e2
-  | SubE (i1, t1), SubE (i2, t2) -> i1 = i2 && t1 = t2
+  | SubE (i1, t1), SubE (i2, t2) -> i1 = i2 && Il.Eq.eq_typ t1 t2
   | YetE s1, YetE s2 -> s1 = s2
   | _ -> false
 

spectec/src/al/print.ml

@@ -197,7 +197,7 @@ and string_of_expr expr =
   | ContextKindE (a, e) -> sprintf "%s == %s" (string_of_expr e) (string_of_atom a)
   | IsDefinedE e -> sprintf "%s != None" (string_of_expr e)
   | IsCaseOfE (e, a) -> sprintf "case(%s) == %s" (string_of_expr e) (string_of_atom a)
-  | HasTypeE (e, t) -> sprintf "type(%s) == %s" (string_of_expr e) t
+  | HasTypeE (e, t) -> sprintf "type(%s) == %s" (string_of_expr e) (string_of_typ t)
   | IsValidE e -> sprintf "valid(%s)" (string_of_expr e)
   | TopLabelE -> "top_label()"
     (* TODO: "type(top()) == label"*)
@@ -494,7 +494,7 @@ and structured_string_of_expr expr =
     ^ structured_string_of_expr e2
     ^ ")"
   | VarE id -> "VarE (" ^ id ^ ")"
-  | SubE (id, t) -> "SubE (" ^ id ^ "," ^ t ^ ")"
+  | SubE (id, t) -> sprintf "SubE (%s, %s)" id (string_of_typ t)
   | IterE (e, ids, iter) ->
     "IterE ("
     ^ structured_string_of_expr e
@@ -511,7 +511,8 @@ and structured_string_of_expr expr =
   | ContextKindE (a, e) -> sprintf "ContextKindE (%s, %s)" (string_of_atom a) (structured_string_of_expr e)
   | IsDefinedE e -> "DefinedE (" ^ structured_string_of_expr e ^ ")"
   | IsCaseOfE (e, a) -> "CaseOfE (" ^ structured_string_of_expr e ^ ", " ^ string_of_atom a ^ ")"
-  | HasTypeE (e, t) -> "HasTypeE (" ^ structured_string_of_expr e ^ ", " ^ t ^ ")"
+  | HasTypeE (e, t) ->
+    sprintf "HasTypeE (%s, %s)" (structured_string_of_expr e) (string_of_typ t)
   | IsValidE e -> "IsValidE (" ^ structured_string_of_expr e ^ ")"
   | TopLabelE -> "TopLabelE"
   | TopFrameE -> "TopFrameE"

spectec/src/al/print.mli

@@ -7,6 +7,7 @@ val string_of_value : value -> string
 val string_of_values : string -> value list -> string
 val string_of_iter : iter -> string
 val string_of_iters : iter list -> string
+val string_of_typ : typ -> string
 val string_of_expr : expr -> string
 val string_of_path : path -> string
 val string_of_arg : arg -> string

spectec/src/backend-interpreter/interpreter.ml

@@ -379,11 +379,11 @@ and eval_expr env expr =
     | _ ->
       fail_expr expr "TODO: deferring validation to reference interpreter"
     )
-  | HasTypeE (e, s) ->
+  | HasTypeE (e, t) ->
     (* TODO: This shouldn't be hardcoded *)
     (* check type *)
     let v = eval_expr env e in
-    check_type s v expr
+    check_type (string_of_typ t) v expr
   | MatchE (e1, e2) ->
     (* Deferred to reference interpreter *)
     let rt1 = e1 |> eval_expr env |> Construct.al_to_ref_type in

spectec/src/backend-prose/print.ml

@@ -172,7 +172,7 @@ and string_of_expr expr =
   | ContextKindE (a, e) -> sprintf "%s is %s" (string_of_expr e) (string_of_atom a)
   | IsDefinedE e -> sprintf "%s is defined" (string_of_expr e)
   | IsCaseOfE (e, a) -> sprintf "%s is of the case %s" (string_of_expr e) (string_of_atom a)
-  | HasTypeE (e, t) -> sprintf "the type of %s is %s" (string_of_expr e) t
+  | HasTypeE (e, t) -> sprintf "the type of %s is %s" (string_of_expr e) (string_of_typ t)
   | IsValidE e -> sprintf "%s is valid" (string_of_expr e)
   | TopLabelE -> "a label is now on the top of the stack"
   | TopFrameE -> "a frame is now on the top of the stack"

spectec/src/backend-prose/render.ml

@@ -444,7 +444,7 @@ and render_expr' env expr =
     sprintf "%s is of the case %s" se sa
   | Al.Ast.HasTypeE (e, t) ->
     let se = render_expr env e in
-    sprintf "the type of %s is %s" se t
+    sprintf "the type of %s is %s" se (Il.Print.string_of_typ t)
   | Al.Ast.IsValidE e ->
     let se = render_expr env e in
     sprintf "%s is valid" se

spectec/src/il2al/translate.ml

@@ -133,7 +133,7 @@ and translate_exp exp =
   | Il.CatE (exp1, exp2) -> catE (translate_exp exp1, translate_exp exp2) ~at:at ~note:note
   (* Variable *)
   | Il.VarE id -> varE id.it ~at:at ~note:note
-  | Il.SubE ({ it = Il.VarE id; _}, { it = VarT (t, _); _ }, _) -> subE (id.it, t.it) ~at:at ~note:note
+  | Il.SubE ({ it = Il.VarE id; _}, t, _) -> subE (id.it, t) ~at:at ~note:note
   | Il.SubE (inner_exp, _, _) -> translate_exp inner_exp
   | Il.IterE (inner_exp, (iter, ids)) ->
     let names = List.map (fun (id, _) -> id.it) ids in
@@ -1109,7 +1109,7 @@ let translate_context_winstr winstr =
 let translate_context ctx vs =
   let at = ctx.at in
   let ty = listT valT in
-  let e_vals = iterE (subE ("val", "val") ~note:valT, [ "val" ], List) ~note:ty in
+  let e_vals = iterE (subE ("val", valT) ~note:valT, [ "val" ], List) ~note:ty in
   let vs = List.rev vs in
   let instr_popall = popallI e_vals in
   let instr_pop_context =