From 4d715aad663c7152fd49700c39b0d04a359a68e9 Mon Sep 17 00:00:00 2001
From: Wonho <new170527@kaist.ac.kr>
Date: Fri, 2 Aug 2024 15:33:59 +0900
Subject: [PATCH] Add manual function definition to AL env

---
 spectec/src/il2al/manual.ml     |  5 +++++
 spectec/src/il2al/preprocess.ml | 14 ++++++++++++++
 2 files changed, 19 insertions(+)

diff --git a/spectec/src/il2al/manual.ml b/spectec/src/il2al/manual.ml
index 31cfd2dbb5..912ffe5c24 100644
--- a/spectec/src/il2al/manual.ml
+++ b/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],
diff --git a/spectec/src/il2al/preprocess.ml b/spectec/src/il2al/preprocess.ml
index 26ea2d3d0d..3368346f2c 100644
--- a/spectec/src/il2al/preprocess.ml
+++ b/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 ]
     )