[spectec] IL AST elaboration

spectec/src/backend-ast/print.ml

@@ -126,6 +126,7 @@ and exp e =
   | CatE (e1, e2) -> Node ("cat", [exp e1; exp e2])
   | CvtE (e1, nt1, nt2) -> Node ("cvt", [numtyp nt1; numtyp nt2; exp e1])
   | SubE (e1, t1, t2) -> Node ("sub", [typ t1; typ t2; exp e1])
+  | AnnE (e1, t1) -> Node ("ann", [typ t1; exp e1])
 
 and expfield (at, e) =
   Node ("field", [mixop (Mixop.Atom at); exp e])

spectec/src/frontend/det.ml

@@ -46,7 +46,7 @@ and det_exp e =
   (* We consider arithmetic expressions determinate,
    * since we sometimes need to use invertible formulas. *)
   | CvtE (e1, _, _) | UnE (#Xl.Num.unop, _, e1) | TheE e1 | LiftE e1
-  | SubE (e1, _, _) -> det_exp e1
+  | SubE (e1, _, _) | AnnE (e1, _) -> det_exp e1
   | BinE (#Xl.Num.binop, _, e1, e2) | CatE (e1, e2) -> det_exp e1 ++ det_exp e2
   | OptE eo -> free_opt det_exp eo
   | ListE es | TupE es -> det_list det_exp es
@@ -123,7 +123,7 @@ and det_quant_exp e =
   | VarE x -> bound_varid x
   | BoolE _ | NumE _ | TextE _ -> empty
   | UnE (_, _, e1) | ProjE (e1, _) | TheE e1 | LiftE e1 | LenE e1
-  | CvtE (e1, _, _) | SubE (e1, _, _) ->
+  | CvtE (e1, _, _) | SubE (e1, _, _) | AnnE (e1, _) ->
     det_quant_exp e1
   | BinE (_, _, e1, e2) | CmpE (_, _, e1, e2)
   | IdxE (e1, e2) | MemE (e1, e2) | CatE (e1, e2) | CompE (e1, e2) ->

spectec/src/frontend/dim.ml

@@ -215,6 +215,9 @@ and check_exp dims ctx e =
     check_exp dims ctx e1;
     check_typ dims ctx t1;
     check_typ dims ctx t2
+  | AnnE (e1, t1) ->
+    check_exp dims ctx e1;
+    check_typ dims ctx t1
 
 and check_expfield dims ctx (_, e) =
   check_exp dims ctx e
@@ -575,6 +578,10 @@ and annot_exp side dims e : exp * occur =
       let t1', occur2 = annot_typ dims t1 in
       let t2', occur3 = annot_typ dims t2 in
       SubE (e1', t1', t2'), union occur1 (union occur2 occur3)
+    | AnnE (e1, t1) ->
+      let e1', occur1 = annot_exp side dims e1 in
+      let t1', occur2 = annot_typ dims t1 in
+      AnnE (e1', t1'), union occur1 occur2
   in {e with it}, occur
 
 and annot_expfield side dims (atom, e) : expfield * occur =

spectec/src/il/ast.ml

@@ -81,6 +81,7 @@ and exp' =
   | IterE of exp * iterexp                  (* exp iter *)
   | CvtE of exp * numtyp * numtyp           (* exp : typ1 <:> typ2 *)
   | SubE of exp * typ * typ                 (* exp : typ1 <: typ2 *)
+  | AnnE of exp * typ                       (* exp : typ *)
 
 and expfield = atom * exp                   (* atom exp *)
 

spectec/src/il/dune

@@ -3,3 +3,5 @@
   (libraries util zarith xl el)
   (modules ast eq free fresh subst iter env eval print debug valid)
 )
+
+(env (dev (flags :standard -w -8-26-27-32-33-34)))

spectec/src/il/eval.ml

@@ -398,6 +398,14 @@ and reduce_exp env e : exp =
       {e1' with note = e.note}
     | _ -> SubE (e1', t1', t2') $> e
     )
+  | AnnE (e1, t1) ->
+    let e1' = reduce_exp env e1 in
+    let t1' = reduce_typ env t1 in
+    (match e1'.it with
+    | BoolE _ | NumE _ | TextE _ | UnE _ | BinE _ | CmpE _
+    | MemE _ | LenE _ | SubE _ | CvtE _ | AnnE _ -> e1'
+    | _ -> AnnE (e1', t1') $> e
+    )
 
 and reduce_iter env = function
   | ListN (e, ido) -> ListN (reduce_exp env e, ido)

spectec/src/il/free.ml

@@ -75,6 +75,7 @@ and free_exp e =
   | IterE (e1, ite) -> (free_exp e1 -- bound_iterexp ite) ++ free_iterexp ite
   | CvtE (e1, _nt1, _nt2) -> free_exp e1
   | SubE (e1, t1, t2) -> free_exp e1 ++ free_typ t1 ++ free_typ t2
+  | AnnE (e1, t1) -> free_exp e1 ++ free_typ t1
 
 and free_expfield (_, e) = free_exp e
 

spectec/src/il/iter.ml

@@ -174,6 +174,7 @@ and exp e =
   | IterE (e1, it) -> iterexp exp e1 it
   | CvtE (e1, nt1, nt2) -> exp e1; numtyp nt1; numtyp nt2
   | SubE (e1, t1, t2) -> exp e1; typ t1; typ t2
+  | AnnE (e1, t1) -> exp e1; typ t1
 
 and expfield (at, e) = atom at; exp e
 

spectec/src/il/print.ml

@@ -159,6 +159,7 @@ and string_of_exp e =
     "(" ^ string_of_exp e1 ^ " : " ^ string_of_numtyp nt1 ^ " <:> " ^ string_of_numtyp nt2 ^ ")"
   | SubE (e1, t1, t2) ->
     "(" ^ string_of_exp e1 ^ " : " ^ string_of_typ t1 ^ " <: " ^ string_of_typ t2 ^ ")"
+  | AnnE (e1, t1) -> "(" ^ string_of_exp e1 ^ " : " ^ string_of_typ t1 ^ ")"
   ) ^
   (if !print_notes then ")@[" ^ string_of_typ e.note ^ "]" else "")
 

spectec/src/il/subst.ml

@@ -191,6 +191,7 @@ and subst_exp s e =
     CaseE (op, subst_exp s e1)
   | CvtE (e1, nt1, nt2) -> CvtE (subst_exp s e1, nt1, nt2)
   | SubE (e1, t1, t2) -> SubE (subst_exp s e1, subst_typ s t1, subst_typ s t2)
+  | AnnE (e1, t1) -> AnnE (subst_exp s e1, subst_typ s t1)
   ) $$ e.at % subst_typ s e.note
 
 and subst_expfield s (atom, e) = (atom, subst_exp s e)