Add manual function definition to AL env

spectec/src/il2al/manual.ml

@@ -17,6 +17,11 @@ let eval_expr =
   let instrs = iterE (varE "instr" ~note:instrT, ["instr"], List) ~note:ty_instrs in
   let result = varE "val" ~note:valT in
 
+  (* Add function definition to AL environment *)
+  let param = Il.Ast.ExpP ("_" $ no_region, ty_instrs) $ no_region in
+  Al.Valid.env :=
+    Il.Env.bind_def !Al.Valid.env ("eval_expr" $ no_region) ([param], ty_vals, []);
+
   FuncA (
     "eval_expr",
     [expA instrs],

spectec/src/il2al/preprocess.ml

@@ -21,6 +21,13 @@ let rec preprocess_prem prem =
       let new_prem =
         IfPr (CmpE (EqOp, expanddt, ct) $$ prem.at % (BoolT $ no_region))
       in
+
+      (* Add function definition to AL environment *)
+      if not (Env.mem_def !Al.Valid.env id) then (
+        let param = ExpP ("_" $ no_region, dt.note) $ dt.at in
+        Al.Valid.env := Env.bind_def !Al.Valid.env id ([param], ct.note, [])
+      );
+
       [ new_prem $ prem.at ]
     (* Expand: ??? *)
     | _ -> [ prem ]
@@ -39,6 +46,13 @@ let rec preprocess_prem prem =
       let new_prem =
         IfPr (CmpE (EqOp, typing_function_call, rhs) $$ exp.at % (BoolT $ no_region))
       in
+
+      (* Add function definition to AL environment *)
+      if not (Env.mem_def !Al.Valid.env id) then (
+        let param = ExpP ("_" $ no_region, lhs.note) $ lhs.at in
+        Al.Valid.env := Env.bind_def !Al.Valid.env id ([param], rhs.note, [])
+      );
+
       [ new_prem $ prem.at ]
     | _ -> [ prem ]
     )