From 8bab67e7dbe9e854a1ee6800c7025110b3e3b07b Mon Sep 17 00:00:00 2001
From: DavidFangWJ <2500097466@qq.com>
Date: Fri, 22 Nov 2024 12:41:58 -0500
Subject: [PATCH] Minimal change.

---
 src/haz3lcore/dynamics/Elaborator.re | 6 +++++-
 src/haz3lcore/statics/Statics.re     | 7 ++++---
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index 487b998a8..c1b76d96b 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -146,6 +146,8 @@ let rec elaborate_pattern =
       DHPat.Tuple(ps') |> rewrap |> cast_from(Typ.Prod(tys) |> Typ.temp);
     | Ap(p1, p2) =>
       let (p1', ty1) = elaborate_pattern(m, p1);
+      // print_endline("p1' = " ++ DHPat.show(p1'));
+      // print_endline("ty1 = " ++ Typ.show(ty1));
       let (p2', ty2) = elaborate_pattern(m, p2);
       let (ty1l, ty1r) = Typ.matched_arrow(ctx, ty1);
       let p1'' = fresh_pat_cast(p1', ty1, Arrow(ty1l, ty1r) |> Typ.temp);
@@ -295,6 +297,8 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
           };
         }
       );
+      print_endline("ELA p(1) = " ++ UPat.show(p));
+      print_endline("ELA m = " ++ Statics.Map.show(m));
       let (p, ty1) = elaborate_pattern(m, p);
       let is_recursive =
         Statics.is_recursive(ctx, p, def, ty1)
@@ -302,7 +306,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
         |> Option.get
         |> List.exists(f => VarMap.lookup(co_ctx, f) != None);
       if (!is_recursive) {
-        print_endline("ELA p = " ++ DHPat.show(p));
+        print_endline("ELA p(2) = " ++ DHPat.show(p));
         let def = add_name(Pat.get_var(p), def);
         print_endline("ELA def = " ++ DHExp.show(def));
         let (def, ty2) = elaborate(m, def);
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 5d9f06beb..56c94e001 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -453,8 +453,8 @@ and uexp_to_info_map =
               term:
                 UPat.Cast(
                   {ids, term: UPat.Var(f_name), copied: false},
-                  Typ.temp(Unknown(Internal)),
                   f_type,
+                  Typ.temp(Unknown(Internal)),
                 ),
               copied: false,
             };
@@ -469,8 +469,8 @@ and uexp_to_info_map =
             (def, p, p_syn);
           | None => (def, p, p_syn) // Use the original code
           };
-        print_endline("STA def = " ++ UExp.show(def));
-        print_endline("STA p = " ++ UPat.show(p));
+        // print_endline("STA def = " ++ UExp.show(def));
+        // print_endline("STA p = " ++ UPat.show(p));
         // print_endline("STA p_syn = " ++ Info.show_pat(p_syn));
         let (def, m) = go(~mode=Ana(p_syn.ty), def, m);
         let ty_p_ana = def.ty;
@@ -483,6 +483,7 @@ and uexp_to_info_map =
             p,
             m,
           );
+        // print_endline("STA p_ana'.ctx = " ++ Ctx.show(p_ana'.ctx));
         (def, p_ana'.ctx, m, ty_p_ana);
       } else {
         let (def_base, _) =