optional memories for empty map

Author: oskgo

src/ecAst.ml

@@ -292,9 +292,10 @@ type ss_inv = {
   inv : form;
 }
 
-let map_ss_inv (fn: form list -> form) (invs: ss_inv list): ss_inv = 
-  assert (List.length invs > 0);
-  let m' = (List.hd invs).m in
+let map_ss_inv ?m (fn: form list -> form) (invs: ss_inv list): ss_inv = 
+  let m' = match m with
+  | Some m -> m
+  | None -> (List.hd invs).m in
   let inv = fn (List.map (fun {inv;m} -> assert (m = m'); inv) invs) in
   { m = m'; inv = inv }
 
@@ -333,10 +334,13 @@ type ts_inv = {
   inv : form;
 }
 
-let map_ts_inv (fn: form list -> form) (invs: ts_inv list): ts_inv =
-  assert (List.length invs > 0);
-  let ml' = (List.hd invs).ml in
-  let mr' = (List.hd invs).mr in
+let map_ts_inv ?ml ?mr (fn: form list -> form) (invs: ts_inv list): ts_inv =
+  let ml' = match ml with 
+   | Some m -> m 
+   | None -> (List.hd invs).ml in
+  let mr' = match mr with 
+   | Some m -> m 
+   | None -> (List.hd invs).mr in
   let inv = fn (List.map (fun {inv;ml;mr} -> assert (ml = ml' && mr = mr'); inv) invs) in
   { ml = ml'; mr = mr'; inv = inv }
 

src/ecAst.mli

@@ -309,7 +309,7 @@ type ss_inv = {
   inv : form;
 }
 
-val map_ss_inv : (form list -> form) -> ss_inv list -> ss_inv
+val map_ss_inv : ?m:memory -> (form list -> form) -> ss_inv list -> ss_inv
 val map_ss_inv1 : (form -> form) -> ss_inv -> ss_inv
 val map_ss_inv2 : (form -> form -> form) -> ss_inv -> ss_inv -> ss_inv
 val map_ss_inv3 : (form -> form -> form -> form) -> ss_inv -> ss_inv -> ss_inv -> ss_inv
@@ -323,7 +323,7 @@ type ts_inv = {
   inv : form;
 }
 
-val map_ts_inv : (form list -> form) -> ts_inv list -> ts_inv
+val map_ts_inv : ?ml:memory -> ?mr:memory -> (form list -> form) -> ts_inv list -> ts_inv
 val map_ts_inv1 : (form -> form) -> ts_inv -> ts_inv
 val map_ts_inv2 : (form -> form -> form) -> ts_inv -> ts_inv -> ts_inv
 val map_ts_inv3 : (form -> form -> form -> form) -> ts_inv -> ts_inv -> ts_inv -> ts_inv

src/ecCoreFol.ml

@@ -950,92 +950,57 @@ let equantif_of_quantif (qt : quantif) : equantif =
   | Lexists -> `EExists
 
 (* -------------------------------------------------------------------- *)
-let rec ss_inv_of_expr m (e : expr) =
+
+let rec form_of_expr_r ?m (e : expr) =
   match e.e_node with
   | Eint n ->
-     {m;inv=f_int n}
+     f_int n
 
   | Elocal id ->
-     {m;inv=f_local id e.e_ty}
+     f_local id e.e_ty
 
   | Evar pv ->
-     f_pvar pv e.e_ty m
+    begin
+     match m with
+     | None -> failwith "expecting memory"
+     | Some m -> (f_pvar pv e.e_ty m).inv
+    end
 
   | Eop (op, tys) ->
-     {m;inv=f_op op tys e.e_ty}
+     f_op op tys e.e_ty
 
   | Eapp (ef, es) ->
-     let f_app' f = f_app (List.hd f) (List.tl f) e.e_ty in
-     map_ss_inv f_app' ((ss_inv_of_expr m ef)::(List.map (ss_inv_of_expr m) es))
+     f_app (form_of_expr_r ?m ef) (List.map (form_of_expr_r ?m) es) e.e_ty
 
   | Elet (lpt, e1, e2) ->
-     map_ss_inv2 (f_let lpt) (ss_inv_of_expr m e1) (ss_inv_of_expr m e2)
+     f_let lpt (form_of_expr_r ?m e1) (form_of_expr_r ?m e2)
 
   | Etuple es ->
-     map_ss_inv f_tuple (List.map (ss_inv_of_expr m) es)
+     f_tuple (List.map (form_of_expr_r ?m) es)
 
   | Eproj (e1, i) ->
-     let f_proj' f = f_proj f i e.e_ty in
-     map_ss_inv1 f_proj' (ss_inv_of_expr m e1)
+     f_proj (form_of_expr_r ?m e1) i e.e_ty
 
   | Eif (e1, e2, e3) ->
-     let e1 = ss_inv_of_expr m e1 in
-     let e2 = ss_inv_of_expr m e2 in
-     let e3 = ss_inv_of_expr m e3 in
-     map_ss_inv3 f_if e1 e2 e3
+     let e1 = form_of_expr_r ?m e1 in
+     let e2 = form_of_expr_r ?m e2 in
+     let e3 = form_of_expr_r ?m e3 in
+     f_if e1 e2 e3
 
   | Ematch (b, fs, ty) ->
-     let b'  = ss_inv_of_expr m b in
-     let fs' = List.map (ss_inv_of_expr m) fs in
-     let f_match' fl = f_match (List.hd fl) (List.tl fl) ty in
-     map_ss_inv f_match' (b'::fs')
+     let b'  = form_of_expr_r ?m b in
+     let fs' = List.map (form_of_expr_r ?m) fs in
+     f_match b' fs' ty
 
   | Equant (qt, b, e) ->
      let b = List.map (fun (x, ty) -> (x, GTty ty)) b in
-     let e = ss_inv_of_expr m e in
-     map_ss_inv1 (f_quant (quantif_of_equantif qt) b) e
+     let e = form_of_expr_r ?m e in
+     f_quant (quantif_of_equantif qt) b e
 
-let rec form_of_expr e = 
-  match e.e_node with
-     | Eint n ->
-        f_int n
-   
-     | Elocal id ->
-        f_local id e.e_ty
-   
-     | Evar _ ->
-        failwith "needs memory for program variable"
-
-     | Eop (op, tys) ->
-        f_op op tys e.e_ty
-
-     | Eapp (ef, es) ->
-        f_app (form_of_expr ef) (List.map form_of_expr es) e.e_ty
-   
-     | Elet (lpt, e1, e2) ->
-        f_let lpt (form_of_expr e1) (form_of_expr e2)
-   
-     | Etuple es ->
-        f_tuple (List.map form_of_expr es)
-   
-     | Eproj (e1, i) ->
-        f_proj (form_of_expr e1) i e.e_ty
-   
-     | Eif (e1, e2, e3) ->
-        let e1 = form_of_expr e1 in
-        let e2 = form_of_expr e2 in
-        let e3 = form_of_expr e3 in
-        f_if e1 e2 e3
-   
-     | Ematch (b, fs, ty) ->
-        let b'  = form_of_expr b in
-        let fs' = List.map form_of_expr fs in
-        f_match b' fs' ty
-   
-     | Equant (qt, b, e) ->
-        let b = List.map (fun (x, ty) -> (x, GTty ty)) b in
-        let e = form_of_expr e in
-        f_quant (quantif_of_equantif qt) b e
+let form_of_expr e = form_of_expr_r e
+
+let ss_inv_of_expr m (e : expr) =
+  {m;inv=form_of_expr_r ~m e}
 
 (* -------------------------------------------------------------------- *)
 exception CannotTranslate

src/ecEnv.ml

@@ -2448,7 +2448,7 @@ module NormMp = struct
     let globs = List.map (fun id -> f_glob id m) globs in
     let pv = List.map (fun (xp, ty) -> f_pvar (pv_glob xp) ty m) pv in
 
-    map_ss_inv f_tuple (globs @ pv)
+    map_ss_inv ~m f_tuple (globs @ pv)
 
   let norm_glob env m mp = globals env m mp
 

src/phl/ecPhlFun.ml

@@ -68,7 +68,7 @@ let subst_pre env fs (m : memory) s =
     | Some v -> { v_name = v; v_type = ov.ov_type }
   in
   let v = List.map (fun v -> f_pvloc (fresh v) m) fs.fs_anames in
-  PVM.add env pv_arg m (map_ss_inv f_tuple v).inv s
+  PVM.add env pv_arg m (map_ss_inv ~m f_tuple v).inv s
 
 (* ------------------------------------------------------------------ *)
 let t_hoareF_fun_def_r tc =

src/phl/ecPhlTrans.ml

@@ -98,7 +98,7 @@ let t_equivS_trans_eq side s tc =
     let xr x ty = ss_inv_generalize_left (f_pvar x ty mr) ml in
     let veq = List.map (fun (x,ty) -> map_ts_inv2 f_eq (xl x ty) (xr x ty)) vfv in
     let geq = List.map (fun mp -> ts_inv_eqglob mp ml mp mr) gfv in
-    map_ts_inv f_ands (veq @ geq) in
+    map_ts_inv ~ml ~mr f_ands (veq @ geq) in
   let pre = mk_eqs (EcPV.PV.union (EcPV.PV.union fv_pr fv_po) fv_r) in
   let pre = map_ts_inv2 f_and pre (odfl {ml=pre.ml;mr=pre.mr;inv=f_true} mem_pre) in
   let post = mk_eqs fv_po in