From 0c814c97dd8e5167f24b0dbb14186d674e4d097b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 13 Dec 2023 11:44:58 +0100
Subject: Update Pure.fun_sig_info

---
 compiler/PureUtils.ml | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'compiler/PureUtils.ml')

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 39dcd52d..23a41f0e 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -57,6 +57,25 @@ end
 module FunLoopIdMap = Collections.MakeMap (FunLoopIdOrderedType)
 module FunLoopIdSet = Collections.MakeSet (FunLoopIdOrderedType)
 
+let inputs_info_is_wf (info : inputs_info) : bool =
+  let {
+    has_fuel;
+    num_inputs_no_fuel_no_state;
+    num_inputs_with_fuel_no_state;
+    num_inputs_with_fuel_with_state;
+  } =
+    info
+  in
+  let fuel = if has_fuel then 1 else 0 in
+  num_inputs_no_fuel_no_state >= 0
+  && num_inputs_with_fuel_no_state = num_inputs_no_fuel_no_state + fuel
+  && num_inputs_with_fuel_with_state >= num_inputs_with_fuel_no_state
+
+let fun_sig_info_is_wf (info : fun_sig_info) : bool =
+  inputs_info_is_wf info.fwd_info
+  &&
+  match info.back_info with None -> true | Some info -> inputs_info_is_wf info
+
 let dest_arrow_ty (ty : ty) : ty * ty =
   match ty with
   | TArrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
-- 
cgit v1.2.3


From f69ac6a4a244c99a41a90ed57f74ea83b3835882 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 14 Dec 2023 17:11:01 +0100
Subject: Start updating Pure.fun_sig_info to handle merged forward and
 backward functions

---
 compiler/PureUtils.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'compiler/PureUtils.ml')

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 23a41f0e..3c038149 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -74,7 +74,11 @@ let inputs_info_is_wf (info : inputs_info) : bool =
 let fun_sig_info_is_wf (info : fun_sig_info) : bool =
   inputs_info_is_wf info.fwd_info
   &&
-  match info.back_info with None -> true | Some info -> inputs_info_is_wf info
+  match info.back_info with
+  | SingleBack None -> true
+  | SingleBack (Some info) -> inputs_info_is_wf info
+  | AllBacks infos ->
+      List.for_all inputs_info_is_wf (RegionGroupId.Map.values infos)
 
 let dest_arrow_ty (ty : ty) : ty * ty =
   match ty with
-- 
cgit v1.2.3


From 83c5be42e1750d329ad31bc9151d7b0446af5a0f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 15 Dec 2023 12:14:01 +0100
Subject: Make progress on generalizing the signature information

---
 compiler/PureUtils.ml | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

(limited to 'compiler/PureUtils.ml')

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 3c038149..dfea255a 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -73,12 +73,6 @@ let inputs_info_is_wf (info : inputs_info) : bool =
 
 let fun_sig_info_is_wf (info : fun_sig_info) : bool =
   inputs_info_is_wf info.fwd_info
-  &&
-  match info.back_info with
-  | SingleBack None -> true
-  | SingleBack (Some info) -> inputs_info_is_wf info
-  | AllBacks infos ->
-      List.for_all inputs_info_is_wf (RegionGroupId.Map.values infos)
 
 let dest_arrow_ty (ty : ty) : ty * ty =
   match ty with
@@ -210,9 +204,7 @@ let fun_sig_substitute (subst : subst) (sg : fun_sig) : inst_fun_sig =
   let subst = ty_substitute subst in
   let inputs = List.map subst sg.inputs in
   let output = subst sg.output in
-  let doutputs = List.map subst sg.doutputs in
-  let info = sg.info in
-  { inputs; output; doutputs; info }
+  { inputs; output }
 
 (** We use this to check whether we need to add parentheses around expressions.
     We only look for outer monadic let-bindings.
-- 
cgit v1.2.3


From ea583d9f0f5e4a1a687b70f0e04e875969462157 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 15 Dec 2023 17:20:30 +0100
Subject: Make good progress on updating SymbolicToPure

---
 compiler/PureUtils.ml | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'compiler/PureUtils.ml')

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index dfea255a..80b25641 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -221,6 +221,9 @@ let rec let_group_requires_parentheses (e : texpression) : bool =
       if monadic then true else let_group_requires_parentheses next_e
   | Switch (_, _) -> false
   | Meta (_, next_e) -> let_group_requires_parentheses next_e
+  | Lambda (_, _) ->
+      (* Being conservative here *)
+      true
   | Loop _ ->
       (* Should have been eliminated *)
       raise (Failure "Unreachable")
@@ -713,3 +716,23 @@ let type_decl_from_type_id_is_tuple_struct (ctx : TypesAnalysis.type_infos)
       let info = TypeDeclId.Map.find id ctx in
       info.is_tuple_struct
   | TAssumed _ -> false
+
+let mk_lambda_from_var (var : var) (mp : mplace option) (e : texpression) :
+    texpression =
+  let ty = TArrow (var.ty, e.ty) in
+  let pat = PatVar (var, mp) in
+  let pat = { value = pat; ty = var.ty } in
+  let e = Lambda (pat, e) in
+  { e; ty }
+
+let mk_lambdas_from_vars (vars : var list) (mps : mplace option list)
+    (e : texpression) : texpression =
+  let vars = List.combine vars mps in
+  List.fold_left (fun e (v, mp) -> mk_lambda_from_var v mp e) e vars
+
+let rec destruct_lambdas (e : texpression) : typed_pattern list * texpression =
+  match e.e with
+  | Lambda (pat, e) ->
+      let pats, e = destruct_lambdas e in
+      (pat :: pats, e)
+  | _ -> ([], e)
-- 
cgit v1.2.3


From 955fdab55304979ba2d61432ea654241f20abaa4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 15 Dec 2023 18:14:12 +0100
Subject: Make progress on propagating the changes

---
 compiler/PureUtils.ml | 24 +++++++-----------------
 1 file changed, 7 insertions(+), 17 deletions(-)

(limited to 'compiler/PureUtils.ml')

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 80b25641..6e86578c 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -215,8 +215,7 @@ let fun_sig_substitute (subst : subst) (sg : fun_sig) : inst_fun_sig =
  *)
 let rec let_group_requires_parentheses (e : texpression) : bool =
   match e.e with
-  | Var _ | CVar _ | Const _ | App _ | Abs _ | Qualif _ | StructUpdate _ ->
-      false
+  | Var _ | CVar _ | Const _ | App _ | Qualif _ | StructUpdate _ -> false
   | Let (monadic, _, _, next_e) ->
       if monadic then true else let_group_requires_parentheses next_e
   | Switch (_, _) -> false
@@ -374,18 +373,6 @@ let opt_destruct_tuple (ty : ty) : ty list option =
       Some generics.types
   | _ -> None
 
-let mk_abs (x : typed_pattern) (e : texpression) : texpression =
-  let ty = TArrow (x.ty, e.ty) in
-  let e = Abs (x, e) in
-  { e; ty }
-
-let rec destruct_abs_list (e : texpression) : typed_pattern list * texpression =
-  match e.e with
-  | Abs (x, e') ->
-      let xl, e'' = destruct_abs_list e' in
-      (x :: xl, e'')
-  | _ -> ([], e)
-
 let destruct_arrow (ty : ty) : ty * ty =
   match ty with
   | TArrow (ty0, ty1) -> (ty0, ty1)
@@ -717,13 +704,16 @@ let type_decl_from_type_id_is_tuple_struct (ctx : TypesAnalysis.type_infos)
       info.is_tuple_struct
   | TAssumed _ -> false
 
+let mk_lambda (x : typed_pattern) (e : texpression) : texpression =
+  let ty = TArrow (x.ty, e.ty) in
+  let e = Lambda (x, e) in
+  { e; ty }
+
 let mk_lambda_from_var (var : var) (mp : mplace option) (e : texpression) :
     texpression =
-  let ty = TArrow (var.ty, e.ty) in
   let pat = PatVar (var, mp) in
   let pat = { value = pat; ty = var.ty } in
-  let e = Lambda (pat, e) in
-  { e; ty }
+  mk_lambda pat e
 
 let mk_lambdas_from_vars (vars : var list) (mps : mplace option list)
     (e : texpression) : texpression =
-- 
cgit v1.2.3


From 8835d87df111d09122267fadc9a32f16b52d234a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 21 Dec 2023 14:37:43 +0100
Subject: Make good progress on merging the fwd/back functions

---
 compiler/PureUtils.ml | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

(limited to 'compiler/PureUtils.ml')

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 6e86578c..6579e84c 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -321,14 +321,23 @@ let destruct_apps (e : texpression) : texpression * texpression list =
 
 (** Make an [App (app, arg)] expression *)
 let mk_app (app : texpression) (arg : texpression) : texpression =
+  let raise_or_return msg =
+    if !Config.fail_hard then raise (Failure msg)
+    else
+      let e = App (app, arg) in
+      (* Dummy type - TODO: introduce an error type *)
+      let ty = app.ty in
+      { e; ty }
+  in
   match app.ty with
   | TArrow (ty0, ty1) ->
       (* Sanity check *)
-      assert (ty0 = arg.ty);
-      let e = App (app, arg) in
-      let ty = ty1 in
-      { e; ty }
-  | _ -> raise (Failure "Expected an arrow type")
+      if ty0 <> arg.ty then raise_or_return "App: wrong input type"
+      else
+        let e = App (app, arg) in
+        let ty = ty1 in
+        { e; ty }
+  | _ -> raise_or_return "Expected an arrow type"
 
 (** The reverse of {!destruct_apps} *)
 let mk_apps (app : texpression) (args : texpression list) : texpression =
-- 
cgit v1.2.3


From d9f91cfcd538525f024c6019d7c8250dda8d76fd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 21 Dec 2023 15:25:06 +0100
Subject: Remove some asserts which are now useless

---
 compiler/PureUtils.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'compiler/PureUtils.ml')

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 6579e84c..d4aaba16 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -332,7 +332,10 @@ let mk_app (app : texpression) (arg : texpression) : texpression =
   match app.ty with
   | TArrow (ty0, ty1) ->
       (* Sanity check *)
-      if ty0 <> arg.ty then raise_or_return "App: wrong input type"
+      if
+        (* TODO: we need to normalize the types *)
+        !Config.type_check_pure_code && ty0 <> arg.ty
+      then raise_or_return "App: wrong input type"
       else
         let e = App (app, arg) in
         let ty = ty1 in
-- 
cgit v1.2.3


From 2f681446b11739e650b1d6050b717da872be9022 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 21 Dec 2023 19:23:29 +0100
Subject: Simplify the type of the merged fwd/back functions

---
 compiler/PureUtils.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'compiler/PureUtils.ml')

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index d4aaba16..78d0b120 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -448,6 +448,7 @@ let mk_simpl_tuple_ty (tys : ty list) : ty =
 
 let mk_bool_ty : ty = TLiteral TBool
 let mk_unit_ty : ty = TAdt (TTuple, empty_generic_args)
+let ty_is_unit ty : bool = ty = mk_unit_ty
 
 let mk_unit_rvalue : texpression =
   let id = AdtCons { adt_id = TTuple; variant_id = None } in
-- 
cgit v1.2.3


From 6dc2b0f0906adc5d6f8f2f48404cf21d3595c957 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 21 Dec 2023 23:02:51 +0100
Subject: Improve the pure micro passes

---
 compiler/PureUtils.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'compiler/PureUtils.ml')

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 78d0b120..cc439e64 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -739,3 +739,16 @@ let rec destruct_lambdas (e : texpression) : typed_pattern list * texpression =
       let pats, e = destruct_lambdas e in
       (pat :: pats, e)
   | _ -> ([], e)
+
+let opt_dest_tuple_texpression (e : texpression) : texpression list option =
+  let app, args = destruct_apps e in
+  match app.e with
+  | Qualif { id = AdtCons { adt_id = TTuple; variant_id = None }; generics = _ }
+    ->
+      Some args
+  | _ -> None
+
+let opt_dest_struct_pattern (pat : typed_pattern) : typed_pattern list option =
+  match pat.value with
+  | PatAdt { variant_id = None; field_values } -> Some field_values
+  | _ -> None
-- 
cgit v1.2.3


From 9a8e43df626400aacdfcb9d2cf2eec38d71d2d73 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 22 Dec 2023 23:04:31 +0100
Subject: Fix minor issues

---
 compiler/PureUtils.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/PureUtils.ml')

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index cc439e64..80bf3c42 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -731,7 +731,7 @@ let mk_lambda_from_var (var : var) (mp : mplace option) (e : texpression) :
 let mk_lambdas_from_vars (vars : var list) (mps : mplace option list)
     (e : texpression) : texpression =
   let vars = List.combine vars mps in
-  List.fold_left (fun e (v, mp) -> mk_lambda_from_var v mp e) e vars
+  List.fold_right (fun (v, mp) e -> mk_lambda_from_var v mp e) vars e
 
 let rec destruct_lambdas (e : texpression) : typed_pattern list * texpression =
   match e.e with
-- 
cgit v1.2.3