Note passing from il to al enabled

spectec/src/al/al_util.ml

@@ -6,6 +6,7 @@ open Source
 (* Constructor Shorthands *)
 
 let no = no_region
+let no_note = Il.Ast.VarT ("TODO" $ no_region, []) $ no_region
 
 let _nid_count = ref 0
 let gen_nid () =
@@ -35,47 +36,48 @@ let appendI ?(at = no) (e1, e2) = AppendI (e1, e2) |> mk_instr at
 let otherwiseI ?(at = no) il = OtherwiseI il |> mk_instr at
 let yetI ?(at = no) s = YetI s |> mk_instr at
 
-let mk_expr at it = Util.Source.($) it at
-
-let varE ?(at = no) id = VarE id |> mk_expr at
-let boolE ?(at = no) b = BoolE b |> mk_expr at
-let numE ?(at = no) i = NumE i |> mk_expr at
-let unE ?(at = no) (unop, e) = UnE (unop, e) |> mk_expr at
-let binE ?(at = no) (binop, e1, e2) = BinE (binop, e1, e2) |> mk_expr at
-let accE ?(at = no) (e, p) = AccE (e, p) |> mk_expr at
-let updE ?(at = no) (e1, pl, e2) = UpdE (e1, pl, e2) |> mk_expr at
-let extE ?(at = no) (e1, pl, e2, dir) = ExtE (e1, pl, e2, dir) |> mk_expr at
-let strE ?(at = no) r = StrE r |> mk_expr at
-let catE ?(at = no) (e1, e2) = CatE (e1, e2) |> mk_expr at
-let memE ?(at = no) (e1, e2) = MemE (e1, e2) |> mk_expr at
-let lenE ?(at = no) e = LenE e |> mk_expr at
-let tupE ?(at = no) el = TupE el |> mk_expr at
-let caseE ?(at = no) (a, el) = CaseE (a, el) |> mk_expr at
-let callE ?(at = no) (id, el) = CallE (id, el) |> mk_expr at
-let iterE ?(at = no) (e, idl, it) = IterE (e, idl, it) |> mk_expr at
-let optE ?(at = no) e_opt = OptE e_opt |> mk_expr at
-let listE ?(at = no) el = ListE el |> mk_expr at
-let infixE ?(at = no) (e1, infix, e2) = InfixE (e1, infix, e2) |> mk_expr at
-let arityE ?(at = no) e = ArityE e |> mk_expr at
-let frameE ?(at = no) (e_opt, e) = FrameE (e_opt, e) |> mk_expr at
-let labelE ?(at = no) (e1, e2) = LabelE (e1, e2) |> mk_expr at
-let getCurStateE ?(at = no) () = GetCurStateE |> mk_expr at
-let getCurFrameE ?(at = no) () = GetCurFrameE |> mk_expr at
-let getCurLabelE ?(at = no) () = GetCurLabelE |> mk_expr at
-let getCurContextE ?(at = no) () = GetCurContextE |> mk_expr at
-let contE ?(at = no) e = ContE e |> mk_expr at
-let isCaseOfE ?(at = no) (e, a) = IsCaseOfE (e, a) |> mk_expr at
-let isValidE ?(at = no) e = IsValidE e |> mk_expr at
-let contextKindE ?(at = no) (a, e) = ContextKindE (a, e) |> mk_expr at
-let isDefinedE ?(at = no) e = IsDefinedE e |> mk_expr at
-let matchE ?(at = no) (e1, e2) = MatchE (e1, e2) |> mk_expr at
-let hasTypeE ?(at = no) (e, ty) = HasTypeE (e, ty) |> mk_expr at
-let topLabelE ?(at = no) () = TopLabelE |> mk_expr at
-let topFrameE ?(at = no) () = TopFrameE |> mk_expr at
-let topValueE ?(at = no) e_opt = TopValueE e_opt |> mk_expr at
-let topValuesE ?(at = no) e = TopValuesE e |> mk_expr at
-let subE ?(at = no) (id, ty) = SubE (id, ty) |> mk_expr at
-let yetE ?(at = no) s = YetE s |> mk_expr at
+let mk_expr at note it = it $$ at % note
+
+let varE ?(at = no) ?(note = no_note) id = VarE id |> mk_expr at note
+let boolE ?(at = no) ?(note = no_note) b = BoolE b |> mk_expr at note
+let numE ?(at = no) ?(note = no_note) i = NumE i |> mk_expr at note
+let unE ?(at = no) ?(note = no_note) (unop, e) = UnE (unop, e) |> mk_expr at note
+let binE ?(at = no) ?(note = no_note) (binop, e1, e2) = BinE (binop, e1, e2) |> mk_expr at note
+let accE ?(at = no) ?(note = no_note) (e, p) = AccE (e, p) |> mk_expr at note
+let updE ?(at = no) ?(note = no_note) (e1, pl, e2) = UpdE (e1, pl, e2) |> mk_expr at note
+let extE ?(at = no) ?(note = no_note) (e1, pl, e2, dir) = ExtE (e1, pl, e2, dir) |> mk_expr at note
+let strE ?(at = no) ?(note = no_note) r = StrE r |> mk_expr at note
+let catE ?(at = no) ?(note = no_note) (e1, e2) = CatE (e1, e2) |> mk_expr at note
+let memE ?(at = no) ?(note = no_note) (e1, e2) = MemE (e1, e2) |> mk_expr at note
+let lenE ?(at = no) ?(note = no_note) e = LenE e |> mk_expr at note
+let tupE ?(at = no) ?(note = no_note) el = TupE el |> mk_expr at note
+let caseE ?(at = no) ?(note = no_note) (a, el) = CaseE (a, el) |> mk_expr at note
+let callE ?(at = no) ?(note = no_note) (id, el) = CallE (id, el) |> mk_expr at note
+let invCallE ?(at = no) ?(note = no_note) (id, il, el) = InvCallE (id, il, el) |> mk_expr at note
+let iterE ?(at = no) ?(note = no_note) (e, idl, it) = IterE (e, idl, it) |> mk_expr at note
+let optE ?(at = no) ?(note = no_note) e_opt = OptE e_opt |> mk_expr at note
+let listE ?(at = no) ?(note = no_note) el = ListE el |> mk_expr at note
+let infixE ?(at = no) ?(note = no_note) (e1, infix, e2) = InfixE (e1, infix, e2) |> mk_expr at note
+let arityE ?(at = no) ?(note = no_note) e = ArityE e |> mk_expr at note
+let frameE ?(at = no) ?(note = no_note) (e_opt, e) = FrameE (e_opt, e) |> mk_expr at note
+let labelE ?(at = no) ?(note = no_note) (e1, e2) = LabelE (e1, e2) |> mk_expr at note
+let getCurStateE ?(at = no) ?(note = no_note) () = GetCurStateE |> mk_expr at note
+let getCurFrameE ?(at = no) ?(note = no_note) () = GetCurFrameE |> mk_expr at note
+let getCurLabelE ?(at = no) ?(note = no_note) () = GetCurLabelE |> mk_expr at note
+let getCurContextE ?(at = no) ?(note = no_note) () = GetCurContextE |> mk_expr at note
+let contE ?(at = no) ?(note = no_note) e = ContE e |> mk_expr at note
+let isCaseOfE ?(at = no) ?(note = no_note) (e, a) = IsCaseOfE (e, a) |> mk_expr at note
+let isValidE ?(at = no) ?(note = no_note) e = IsValidE e |> mk_expr at note
+let contextKindE ?(at = no) ?(note = no_note) (a, e) = ContextKindE (a, e) |> mk_expr at note
+let isDefinedE ?(at = no) ?(note = no_note) e = IsDefinedE e |> mk_expr at note
+let matchE ?(at = no) ?(note = no_note) (e1, e2) = MatchE (e1, e2) |> mk_expr at note
+let hasTypeE ?(at = no) ?(note = no_note) (e, ty) = HasTypeE (e, ty) |> mk_expr at note
+let topLabelE ?(at = no) ?(note = no_note) () = TopLabelE |> mk_expr at note
+let topFrameE ?(at = no) ?(note = no_note) () = TopFrameE |> mk_expr at note
+let topValueE ?(at = no) ?(note = no_note) e_opt = TopValueE e_opt |> mk_expr at note
+let topValuesE ?(at = no) ?(note = no_note) e = TopValuesE e |> mk_expr at note
+let subE ?(at = no) ?(note = no_note) (id, ty) = SubE (id, ty) |> mk_expr at note
+let yetE ?(at = no) ?(note = no_note) s = YetE s |> mk_expr at note
 
 let mk_path at it = Util.Source.($) it at
 

spectec/src/al/ast.ml

@@ -73,7 +73,7 @@ type iter =
 
 (* Expressions *)
 
-and expr = expr' phrase
+and expr = (expr', Il.Ast.typ) note_phrase
 and expr' =
   | VarE of id                          (* varid *)
   | NumE of Z.t                         (* number *)

spectec/src/al/print.ml

@@ -331,7 +331,7 @@ let rec string_of_instr' depth instr =
   | ExecuteSeqI e ->
     sprintf "%s Execute the sequence (%s)." (make_index depth) (string_of_expr e)
   | PerformI (id, el) ->
-    sprintf "%s Perform %s." (make_index depth) (string_of_expr (CallE (id, el) $ instr.at))
+    sprintf "%s Perform %s." (make_index depth) (string_of_expr (CallE (id, el) $$ instr.at % (Il.Ast.VarT ("TODO" $ no_region, []) $ no_region)))
   | ExitI a ->
     sprintf "%s Exit from %s." (make_index depth) (string_of_atom a)
   | ReplaceI (e1, p, e2) ->

spectec/src/backend-prose/render.ml

@@ -571,12 +571,12 @@ let rec render_al_instr env algoname index depth instr =
   | Al.Ast.ExecuteSeqI e ->
     sprintf "%s Execute the sequence %s." (render_order index depth) (render_expr env e)
   | Al.Ast.PerformI (n, es) ->
-    sprintf "%s Perform %s." (render_order index depth) (render_expr env (Al.Ast.CallE (n, es) $ no_region))
+    sprintf "%s Perform %s." (render_order index depth) (render_expr env (Al.Al_util.callE (n, es) ~at:no_region))
   | Al.Ast.ExitI a ->
     sprintf "%s Exit from %s." (render_order index depth) (render_atom env a)
   | Al.Ast.ReplaceI (e1, p, e2) ->
     sprintf "%s Replace %s with %s." (render_order index depth)
-      (render_expr env (Al.Ast.AccE (e1, p) $ no_region)) (render_expr env e2)
+      (render_expr env (Al.Al_util.accE (e1, p) ~at:no_region)) (render_expr env e2)
   | Al.Ast.AppendI (e1, e2) ->
     sprintf "%s Append %s to the %s." (render_order index depth)
       (render_expr env e2) (render_expr env e1)
@@ -603,14 +603,14 @@ let render_atom_title env name params =
     | _ -> name'
   in
   let name = (name', typ) in
-  let expr = Al.Ast.CaseE (name, params) $ no_region in
+  let expr = Al.Al_util.caseE (name, params) ~at:no_region in
   match al_to_el_expr expr with
   | Some ({ it = El.Ast.ParenE (exp, _); _ }) -> render_el_exp env exp
   | Some exp -> render_el_exp env exp
   | None -> render_expr' env expr
 
 let render_funcname_title env fname params =
-  render_expr env (Al.Ast.CallE (fname, params) $ no_region)
+  render_expr env (Al.Al_util.callE (fname, params) ~at:no_region)
 
 let render_pred env name params instrs =
   let title = render_atom_title env name params in

spectec/src/il2al/translate.ml

@@ -119,27 +119,28 @@ let rec translate_iter = function
 (* `Il.exp` -> `expr` *)
 and translate_exp exp =
   let at = exp.at in
+  let note = exp.note in
   match exp.it with
-  | Il.NatE n -> numE n ~at:at
-  | Il.BoolE b -> boolE b ~at:at
+  | Il.NatE n -> numE n ~at:at ~note:note
+  | Il.BoolE b -> boolE b ~at:at ~note:note
   (* List *)
-  | Il.LenE inner_exp -> lenE (translate_exp inner_exp) ~at:at
-  | Il.ListE exps -> listE (List.map translate_exp exps) ~at:at
+  | Il.LenE inner_exp -> lenE (translate_exp inner_exp) ~at:at ~note:note
+  | Il.ListE exps -> listE (List.map translate_exp exps) ~at:at ~note:note
   | Il.IdxE (exp1, exp2) ->
-    accE (translate_exp exp1, idxP (translate_exp exp2)) ~at:at
+    accE (translate_exp exp1, idxP (translate_exp exp2)) ~at:at ~note:note
   | Il.SliceE (exp1, exp2, exp3) ->
-    accE (translate_exp exp1, sliceP (translate_exp exp2, translate_exp exp3)) ~at:at
-  | Il.CatE (exp1, exp2) -> catE (translate_exp exp1, translate_exp exp2) ~at:at
+    accE (translate_exp exp1, sliceP (translate_exp exp2, translate_exp exp3)) ~at:at ~note:note
+  | Il.CatE (exp1, exp2) -> catE (translate_exp exp1, translate_exp exp2) ~at:at ~note:note
   (* Variable *)
-  | Il.VarE id -> varE id.it ~at:at
-  | Il.SubE ({ it = Il.VarE id; _}, { it = VarT (t, _); _ }, _) -> subE (id.it, t.it) ~at:at
+  | 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 (inner_exp, _, _) -> translate_exp inner_exp
   | Il.IterE (inner_exp, (iter, ids)) ->
     let names = List.map (fun (id, _) -> id.it) ids in
-    iterE (translate_exp inner_exp, names, translate_iter iter) ~at:at
+    iterE (translate_exp inner_exp, names, translate_iter iter) ~at:at ~note:note
   (* property access *)
   | Il.DotE (inner_exp, ({it = Atom _; _} as atom)) ->
-    accE (translate_exp inner_exp, dotP (translate_atom atom)) ~at:at
+    accE (translate_exp inner_exp, dotP (translate_atom atom)) ~at:at ~note:note
   (* conacatenation of records *)
   | Il.CompE (inner_exp, { it = Il.StrE expfields; _ }) ->
     (* assumption: CompE is only used with at least one literal *)
@@ -149,7 +150,7 @@ and translate_exp exp =
       | {it = Il.Atom _; _} as atom, fieldexp ->
         let extend_expr = translate_exp fieldexp in
         if nonempty extend_expr then
-          extE (acc, [ dotP (translate_atom atom) ], extend_expr, Back) ~at:at
+          extE (acc, [ dotP (translate_atom atom) ], extend_expr, Back) ~at:at ~note:note
         else
           acc
       | _ -> error_exp exp "AL record expression")
@@ -162,15 +163,15 @@ and translate_exp exp =
       | {it = Il.Atom _; _} as atom, fieldexp ->
         let extend_expr = translate_exp fieldexp in
         if nonempty extend_expr then
-          extE (acc, [ dotP (translate_atom atom) ], extend_expr, Front) ~at:at
+          extE (acc, [ dotP (translate_atom atom) ], extend_expr, Front) ~at:at ~note:note
         else
           acc
       | _ -> error_exp exp "AL record expression")
       (translate_exp inner_exp) expfields
   (* extension of record field *)
-  | Il.ExtE (base, path, v) -> extE (translate_exp base, translate_path path, translate_exp v, Back) ~at:at
+  | Il.ExtE (base, path, v) -> extE (translate_exp base, translate_path path, translate_exp v, Back) ~at:at ~note:note
   (* update of record field *)
-  | Il.UpdE (base, path, v) -> updE (translate_exp base, translate_path path, translate_exp v) ~at:at
+  | Il.UpdE (base, path, v) -> updE (translate_exp base, translate_path path, translate_exp v) ~at:at ~note:note
   (* Binary / Unary operation *)
   | Il.UnE (op, exp) ->
     let exp' = translate_exp exp in
@@ -179,7 +180,7 @@ and translate_exp exp =
     | Il.MinusOp _ -> MinusOp
     | _ -> error_exp exp "AL unary expression"
     in
-    unE (op, exp') ~at:at
+    unE (op, exp') ~at:at ~note:note
   | Il.BinE (op, exp1, exp2) ->
     let lhs = translate_exp exp1 in
     let rhs = translate_exp exp2 in
@@ -196,7 +197,7 @@ and translate_exp exp =
       | Il.ImplOp -> ImplOp
       | Il.EquivOp -> EquivOp
     in
-    binE (op, lhs, rhs) ~at:at
+    binE (op, lhs, rhs) ~at:at ~note:note
   | Il.CmpE (op, exp1, exp2) ->
     let lhs = translate_exp exp1 in
     let rhs = translate_exp exp2 in
@@ -209,17 +210,17 @@ and translate_exp exp =
       | Il.LeOp _ -> LeOp
       | Il.GeOp _ -> GeOp
     in
-    binE (compare_op, lhs, rhs) ~at:at
+    binE (compare_op, lhs, rhs) ~at:at ~note:note
   (* Set operation *)
   | Il.MemE (exp1, exp2) ->
     let lhs = translate_exp exp1 in
     let rhs = translate_exp exp2 in
-    memE (lhs, rhs) ~at:at
+    memE (lhs, rhs) ~at:at ~note:note
   (* Tuple *)
   | Il.TupE [e] -> translate_exp e
-  | Il.TupE exps -> tupE (List.map translate_exp exps) ~at:at
+  | Il.TupE exps -> tupE (List.map translate_exp exps) ~at:at ~note:note
   (* Call *)
-  | Il.CallE (id, args) -> callE (id.it, translate_args args) ~at:at
+  | Il.CallE (id, args) -> callE (id.it, translate_args args) ~at:at ~note:note
   (* Record expression *)
   | Il.StrE expfields ->
     let f acc = function
@@ -230,7 +231,7 @@ and translate_exp exp =
       | _ -> error_exp exp "AL record expression"
     in
     let record = List.fold_left f Record.empty expfields in
-    strE record ~at:at
+    strE record ~at:at ~note:note
   (* CaseE *)
   | Il.CaseE (op, e) -> (
     let exps =
@@ -243,43 +244,43 @@ and translate_exp exp =
     (* TODO: Need a better way to convert these CaseE into ConstructE *)
     | [ [ {it = Il.Atom "MUT"; _} as atom ]; [ {it = Il.Quest; _} ]; [] ],
       [ { it = Il.OptE (Some { it = Il.TupE []; _ }); _}; t ] ->
-      tupE [ caseE (translate_atom atom, []); translate_exp t ] ~at:at
+      tupE [ caseE (translate_atom atom, []); translate_exp t ] ~at:at ~note:note
     | [ [ {it = Il.Atom "MUT"; _} ]; [ {it = Il.Quest; _} ]; [] ],
       [ { it = Il.IterE ({ it = Il.TupE []; _ }, (Il.Opt, [])); _}; t ] ->
-      tupE [ iterE (varE "mut", ["mut"], Opt); translate_exp t ] ~at:at
+      tupE [ iterE (varE "mut", ["mut"], Opt); translate_exp t ] ~at:at ~note:note
     | [ []; [ {it = Il.Atom "PAGE"; _} as atom ] ], el ->
-      caseE (translate_atom atom, List.map translate_exp el) ~at:at
+      caseE (translate_atom atom, List.map translate_exp el) ~at:at ~note:note
     | [ [ {it = Il.Atom "NULL"; _} as atom ]; [ {it = Il.Quest; _} ] ], el ->
-      caseE (translate_atom atom, List.map translate_exp el) ~at:at
+      caseE (translate_atom atom, List.map translate_exp el) ~at:at ~note:note
     | [ {it = Il.Atom _; _} as atom ] :: ll, el
       when List.for_all (function ([] | [ {it = (Il.Star | Il.Quest); _} ]) -> true | _ -> false) ll ->
-      caseE (translate_atom atom, List.map translate_exp el) ~at:at
+      caseE (translate_atom atom, List.map translate_exp el) ~at:at ~note:note
     | [ [{it = Il.LBrack; _}]; [{it = Il.Dot2; _}]; [{it = Il.RBrack; _}] ], [ e1; e2 ] ->
-      tupE [ translate_exp e1; translate_exp e2 ] ~at:at
+      tupE [ translate_exp e1; translate_exp e2 ] ~at:at ~note:note
     | (({it = Il.Atom _; _} as atom)::_)::_, _ ->
-        caseE (translate_atom atom, translate_argexp e) ~at:at
+        caseE (translate_atom atom, translate_argexp e) ~at:at ~note:note
     | [ []; [] ], [ e1 ] -> translate_exp e1
     | [ []; []; [] ], [ e1; e2 ] ->
-      tupE [ translate_exp e1; translate_exp e2 ] ~at:at
+      tupE [ translate_exp e1; translate_exp e2 ] ~at:at ~note:note
     | [ []; [{it = Il.Semicolon; _}]; [] ], [ e1; e2 ] ->
-      tupE [ translate_exp e1; translate_exp e2 ] ~at:at
+      tupE [ translate_exp e1; translate_exp e2 ] ~at:at ~note:note
     | [ []; [{it = Il.Arrow; _} as atom]; [] ], [ e1; e2 ] ->
-      infixE (translate_exp e1, translate_atom atom, translate_exp e2) ~at:at
+      infixE (translate_exp e1, translate_atom atom, translate_exp e2) ~at:at ~note:note
     | [ []; [{it = Il.Arrow; _} as atom]; []; [] ], [ e1; e2; e3 ] ->
-      infixE (translate_exp e1, translate_atom atom, catE (translate_exp e2, translate_exp e3)) ~at:at
+      infixE (translate_exp e1, translate_atom atom, catE (translate_exp e2, translate_exp e3)) ~at:at ~note:note
     | [ []; [{it = Il.ArrowSub; _} as atom]; []; [] ], [ e1; e2; e3 ] ->
-      infixE (translate_exp e1, translate_atom atom, catE (translate_exp e2, translate_exp e3)) ~at:at
+      infixE (translate_exp e1, translate_atom atom, catE (translate_exp e2, translate_exp e3)) ~at:at ~note:note
     | [ []; [{it = Il.Atom _; _} as atom]; [] ], [ e1; e2 ] ->
-      infixE (translate_exp e1, translate_atom atom, translate_exp e2) ~at:at
-    | _ -> yetE (Il.Print.string_of_exp exp) ~at:at)
+      infixE (translate_exp e1, translate_atom atom, translate_exp e2) ~at:at ~note:note
+    | _ -> yetE (Il.Print.string_of_exp exp) ~at:at ~note:note)
   | Il.UncaseE (e, op) -> (
     match op with
     | [ []; [] ] -> translate_exp e
-    | _ -> yetE (Il.Print.string_of_exp exp) ~at:at)
+    | _ -> yetE (Il.Print.string_of_exp exp) ~at:at ~note:note)
   | Il.ProjE (e, 0) -> translate_exp e
-  | Il.OptE inner_exp -> optE (Option.map translate_exp inner_exp) ~at:at
+  | Il.OptE inner_exp -> optE (Option.map translate_exp inner_exp) ~at:at ~note:note
   (* Yet *)
-  | _ -> yetE (Il.Print.string_of_exp exp) ~at:at
+  | _ -> yetE (Il.Print.string_of_exp exp) ~at:at ~note:note
 
 (* `Il.exp` -> `expr list` *)
 and translate_argexp exp =
@@ -536,12 +537,11 @@ and handle_inverse_function lhs rhs free_ids =
   (* All arguments are free *)
   if List.for_all contains_free args then
     let new_lhs = args2lhs args in
-    let new_rhs = InvCallE (f, [], rhs2args rhs) $ lhs.at in
+    let new_rhs = invCallE (f, [], rhs2args rhs) ~at:lhs.at in
     handle_special_lhs new_lhs new_rhs free_ids
 
   (* Some arguments are free *)
   else if List.exists contains_free args then
-
     (* Distinguish free arguments and bound arguments *)
     let free_args_with_index, bound_args =
       args
@@ -560,7 +560,7 @@ and handle_inverse_function lhs rhs free_ids =
 
     (* Free argument become new lhs & InvCallE become new rhs *)
     let new_lhs = args2lhs free_args in
-    let new_rhs = InvCallE (f, indices, bound_args @ rhs2args rhs) $ lhs.at in
+    let new_rhs = invCallE (f, indices, bound_args @ rhs2args rhs) ~at:lhs.at in
 
     (* Recursively translate new_lhs and new_rhs *)
     handle_special_lhs new_lhs new_rhs free_ids