Mlw: allow pure functions in programs

pure functions are always ghost, accept mutable values,
and are required to produce pure results

src/mlw/dexpr.ml

@@ -269,6 +269,14 @@ let specialize_rs {rs_cty = cty} =
   let spec ity = spec_ity hv hr cty.cty_freeze ity in
   List.map (fun v -> spec v.pv_ity) cty.cty_args, spec cty.cty_result
 
+let specialize_ls {ls_args = args; ls_value = res} =
+  let hv = Htv.create 3 and hr = Hreg.create 3 in
+  let rec ity ty = match ty.ty_node with
+    | Tyapp (s,tl) -> ity_app_fresh (restore_its s) (List.map ity tl)
+    | Tyvar v -> ity_var v in
+  let spec ty = spec_ity hv hr isb_empty (ity ty) in
+  List.map spec args, Opt.fold (Util.const spec) dity_bool res
+
 (** Patterns *)
 
 type dpattern = {
@@ -329,6 +337,7 @@ and dexpr_node =
   | DEvar of string * dvty
   | DEpv of pvsymbol
   | DErs of rsymbol
+  | DEls of lsymbol
   | DEconst of Number.constant
   | DEapp of dexpr * dexpr
   | DEfun of dbinder list * dspec later * dexpr
@@ -568,6 +577,8 @@ let dexpr ?loc node =
         [], specialize_pv pv
     | DErs rs ->
         specialize_rs rs
+    | DEls ls ->
+        specialize_ls ls
     | DEconst (Number.ConstInt _) ->
         dvty_int
     | DEconst (Number.ConstReal _) ->
@@ -955,15 +966,19 @@ and cexp uloc env ghost ({de_loc = loc} as de) =
   Loc.try4 ?loc try_cexp uloc env ghost de
 
 and try_cexp uloc env ghost de0 = match de0.de_node with
-  | DEvar _ | DErs _ | DEapp _ ->
+  | DEvar _ | DErs _ | DEls _ | DEapp _ ->
+      let argl, res = de0.de_dvty in
+      let argl = List.map ity_of_dity argl in
+      let res = ity_of_dity res in
       let app (ldl,c) el =
-        let argl, res = de0.de_dvty in
-        ext_c_app (ldl, c_ghostify ghost c) el
-          (List.map ity_of_dity argl) (ity_of_dity res) in
+        ext_c_app (ldl, c_ghostify ghost c) el argl res in
       let rec down de el = match de.de_node with
         | DEapp (de1,de2) -> down de1 (expr uloc env de2 :: el)
         | DEvar (n,_) -> app (ext_c_sym (get_rs env n)) el
         | DErs s -> app (ext_c_sym s) el
+        | DEls _ when not res.ity_pure ->
+            Loc.errorm "This expression must have pure type"
+        | DEls s -> ext_c_pur s el argl res
         | _ -> app (cexp uloc env ghost de) el in
       down de0 []
   | DEfun (bl,dsp,de) ->
@@ -1005,7 +1020,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
       let e1 = expr uloc env de1 in
       let e2 = expr uloc env de2 in
       e_app rs_func_app [e1; e2] [] (ity_of_dity res)
-  | DEvar _ | DErs _ | DEapp _ | DEfun _ | DEany _ ->
+  | DEvar _ | DErs _ | DEls _ | DEapp _ | DEfun _ | DEany _ ->
       let ldl,c = try_cexp uloc env false de0 in
       List.fold_right e_let_check ldl (e_exec c)
   | DElet ((id,_,_,{de_dvty = ([],_)}) as dldf,de) ->

src/mlw/dexpr.mli

@@ -91,6 +91,7 @@ and dexpr_node =
   | DEvar of string * dvty
   | DEpv of pvsymbol
   | DErs of rsymbol
+  | DEls of lsymbol
   | DEconst of Number.constant
   | DEapp of dexpr * dexpr
   | DEfun of dbinder list * dspec later * dexpr

src/mlw/expr.ml

@@ -310,6 +310,7 @@ and cexp = {
 
 and cexp_node =
   | Capp of rsymbol * pvsymbol list
+  | Cpur of lsymbol * pvsymbol list
   | Cfun of expr
   | Cany
 
@@ -665,6 +666,16 @@ let c_fun args p q xq old ({e_effect = eff} as e) =
 let c_app s vl ityl ity =
   mk_cexp (Capp (s,vl)) (cty_apply s.rs_cty vl ityl ity)
 
+let c_pur s vl ityl ity =
+  if not ity.ity_pure then invalid_arg "Expr.c_pur";
+  let v_args = List.map (create_pvsymbol (id_fresh "u")) ityl in
+  let t_args = List.map (fun v -> t_var v.pv_vs) (vl @ v_args) in
+  let res = Opt.map (fun _ -> ty_of_ity ity) s.ls_value in
+  let q = make_post (t_app s t_args res) in
+  let eff = eff_ghostify true eff_empty in
+  let cty = create_cty v_args [] [q] Mexn.empty Mpv.empty eff ity in
+  mk_cexp (Cpur (s,vl)) cty
+
 let proxy_label = create_label "whyml_proxy_symbol"
 let proxy_labels = Slab.singleton proxy_label
 
@@ -706,10 +717,23 @@ let ext_c_app (ldl,c) el ityl ity =
   match c.c_node with
     | Capp (s,ul) ->
         ldl, mk_cexp (Capp (s, ul @ vl)) (cty_apply c.c_cty vl ityl ity)
+    | Cpur (s,ul) ->
+        ldl, mk_cexp (Cpur (s, ul @ vl)) (cty_apply c.c_cty vl ityl ity)
     | Cfun _ | Cany ->
         let ld, s = let_sym (id_fresh ~label:proxy_labels "h") c in
         ldl @ [ld], c_app s vl ityl ity
 
+let ext_c_pur s el ityl ity =
+  let rec args hd al el = match al, el with
+    | _::al, e::el ->
+        let hd, v = mk_proxy ~ghost:true e hd in
+        let hd, vl = args hd al el in
+        hd, v::vl
+    | _, [] -> hd, []
+    | _ -> invalid_arg "Expr.ext_c_pur" in
+  let ldl, vl = args [] s.ls_args el in
+  ldl, c_pur s vl ityl ity
+
 (* assignment *)
 
 let e_assign_raw al =
@@ -903,6 +927,9 @@ and c_rs_subst sm ({c_node = n; c_cty = c} as d) =
   | Capp (s,vl) ->
       let al = List.map (fun v -> v.pv_ity) c.cty_args in
       c_app (Mrs.find_def s s sm) vl al c.cty_result
+  | Cpur (s,vl) ->
+      let al = List.map (fun v -> v.pv_ity) c.cty_args in
+      c_pur s vl al c.cty_result
   | Cfun e ->
       c_fun c.cty_args c.cty_pre c.cty_post
         c.cty_xpost c.cty_oldies (e_rs_subst sm e))
@@ -1005,7 +1032,7 @@ let forget_let_defn = function
   | LDrec rdl -> List.iter (fun fd -> forget_rs fd.rec_sym) rdl
 
 let extract_op s =
-  let s = s.rs_name.id_string in
+  let s = s.id_string in
   let len = String.length s in
   if len < 7 then None else
   let inf = String.sub s 0 6 in
@@ -1023,7 +1050,7 @@ let print_rs fmt ({rs_name = {id_string = nm}} as s) =
   if nm = "mixfix [_..]" then pp_print_string fmt "([_..])" else
   if nm = "mixfix [.._]" then pp_print_string fmt "([.._])" else
   if nm = "mixfix [_.._]" then pp_print_string fmt "([_.._])" else
-  match extract_op s, s.rs_logic with
+  match extract_op s.rs_name, s.rs_logic with
   | Some s, _ ->
       let s = Str.replace_first (Str.regexp "^\\*.") " \\0" s in
       let s = Str.replace_first (Str.regexp ".\\*$") "\\0 " s in
@@ -1072,52 +1099,61 @@ let ambig_cty c =
   let sres = ity_freeze isb_empty c.cty_result in
   not (Mtv.set_submap sres.isb_tv sarg.isb_tv)
 
-let ht_rs = Hrs.create 7 (* rec_rsym -> rec_sym *)
+let ambig_ls s =
+  let sarg = List.fold_left ty_freevars Stv.empty s.ls_args in
+  let sres = Opt.fold ty_freevars Stv.empty s.ls_value in
+  not (Stv.subset sres sarg)
 
-let rec print_expr fmt e = print_lexpr 0 fmt e
-
-and print_lexpr pri fmt e =
-  let print_elab pri fmt e =
-    if Debug.test_flag debug_print_labels && not (Slab.is_empty e.e_label)
-    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
-      (Pp.print_iter1 Slab.iter Pp.space print_label) e.e_label
-      (print_enode 0) e
-    else print_enode pri fmt e in
-  let print_eloc pri fmt e =
-    if Debug.test_flag debug_print_locs && e.e_loc <> None
-    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
-      (Pp.print_option print_loc) e.e_loc (print_elab 0) e
-    else print_elab pri fmt e in
-  print_eloc pri fmt e
+let ht_rs = Hrs.create 7 (* rec_rsym -> rec_sym *)
 
-and print_capp pri s fmt vl = match extract_op s, vl with
+let print_apply pri print s id fmt vl = match extract_op id, vl with
   | _, [] ->
-      print_rs fmt s
+      print fmt s
   | Some o, [t1] when tight_op o ->
       fprintf fmt (protect_on (pri > 7) "%s%a") o print_pv t1
-  | Some o, [t1] when String.get s.rs_name.id_string 0 = 'p' ->
+  | Some o, [t1] when String.get id.id_string 0 = 'p' ->
       fprintf fmt (protect_on (pri > 4) "%s %a") o print_pv t1
   | Some o, [t1;t2] ->
       fprintf fmt (protect_on (pri > 4) "@[<hov 1>%a %s@ %a@]")
         print_pv t1 o print_pv t2
-  | _, [t1;t2] when s.rs_name.id_string = "mixfix []" ->
+  | _, [t1;t2] when id.id_string = "mixfix []" ->
       fprintf fmt (protect_on (pri > 6) "%a[%a]") print_pv t1 print_pv t2
-  | _, [t1;t2;t3] when s.rs_name.id_string = "mixfix [<-]" ->
+  | _, [t1;t2;t3] when id.id_string = "mixfix [<-]" ->
       fprintf fmt (protect_on (pri > 6) "%a[%a <- %a]")
         print_pv t1 print_pv t2 print_pv t3
-  | _, [t1;t2;t3] when s.rs_name.id_string = "mixfix []<-" ->
+  | _, [t1;t2;t3] when id.id_string = "mixfix []<-" ->
       fprintf fmt (protect_on (pri > 0) "%a[%a] <- %a")
         print_pv t1 print_pv t2 print_pv t3
-  | _, [t1;t2] when s.rs_name.id_string = "mixfix [_..]" ->
+  | _, [t1;t2] when id.id_string = "mixfix [_..]" ->
       fprintf fmt (protect_on (pri > 6) "%a[%a..]") print_pv t1 print_pv t2
-  | _, [t1;t2] when s.rs_name.id_string = "mixfix [.._]" ->
+  | _, [t1;t2] when id.id_string = "mixfix [.._]" ->
       fprintf fmt (protect_on (pri > 6) "%a[..%a]") print_pv t1 print_pv t2
-  | _, [t1;t2;t3] when s.rs_name.id_string = "mixfix [_.._]" ->
+  | _, [t1;t2;t3] when id.id_string = "mixfix [_.._]" ->
       fprintf fmt (protect_on (pri > 6) "%a[%a..%a]")
         print_pv t1 print_pv t2 print_pv t3
   | _, tl ->
       fprintf fmt (protect_on (pri > 5) "@[<hov 1>%a@ %a@]")
-        print_rs s (Pp.print_list Pp.space print_pv) tl
+        print s (Pp.print_list Pp.space print_pv) tl
+
+let print_capp pri s fmt vl = print_apply pri print_rs s s.rs_name fmt vl
+
+let print_cpur pri s fmt vl = print_apply pri print_ls s s.ls_name fmt vl
+
+let rec print_expr fmt e = print_lexpr 0 fmt e
+
+and print_lexpr pri fmt e =
+  let print_elab pri fmt e =
+    if Debug.test_flag debug_print_labels && not (Slab.is_empty e.e_label)
+    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
+      (Pp.print_iter1 Slab.iter Pp.space print_label) e.e_label
+      (print_enode 0) e
+    else print_enode pri fmt e in
+  let print_eloc pri fmt e =
+    if Debug.test_flag debug_print_locs && e.e_loc <> None
+    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
+      (Pp.print_option print_loc) e.e_loc (print_elab 0) e
+    else print_elab pri fmt e in
+  print_eloc pri fmt e
 
 and print_cexp exec pri fmt {c_node = n; c_cty = c} = match n with
   | Cany when exec && c.cty_args = [] ->
@@ -1150,6 +1186,11 @@ and print_cexp exec pri fmt {c_node = n; c_cty = c} = match n with
         (print_capp 5 (Hrs.find_def ht_rs s s)) vl print_ity c.cty_result
   | Capp (s,vl) ->
       print_capp pri (Hrs.find_def ht_rs s s) fmt vl
+  | Cpur (s,vl) when exec && c.cty_args = [] && ambig_ls s ->
+      fprintf fmt (protect_on (pri > 0) "%a:%a")
+        (print_cpur 5 s) vl print_ity c.cty_result
+  | Cpur (s,vl) ->
+      print_cpur pri s fmt vl
 
 and print_enode pri fmt e = match e.e_node with
   | Evar v -> print_pv fmt v

src/mlw/expr.mli

@@ -130,6 +130,7 @@ and cexp = private {
 
 and cexp_node = private
   | Capp of rsymbol * pvsymbol list
+  | Cpur of lsymbol * pvsymbol list
   | Cfun of expr
   | Cany
 
@@ -176,6 +177,8 @@ val ls_decr_of_rec_defn : rec_defn -> lsymbol option
 
 val c_app : rsymbol -> pvsymbol list -> ity list -> ity -> cexp
 
+val c_pur : lsymbol -> pvsymbol list -> ity list -> ity -> cexp
+
 val c_fun : pvsymbol list ->
   pre list -> post list -> post list Mexn.t -> pvsymbol Mpv.t -> expr -> cexp
 
@@ -187,6 +190,8 @@ val ext_c_sym : rsymbol -> ext_cexp
 
 val ext_c_app : ext_cexp -> expr list -> ity list -> ity -> ext_cexp
 
+val ext_c_pur : lsymbol -> expr list -> ity list -> ity -> ext_cexp
+
 (** {2 Expression constructors} *)
 
 val e_var : pvsymbol -> expr

src/mlw/pdecl.ml

@@ -247,6 +247,8 @@ let get_syms node pure =
     | Capp (s,vl) ->
         let syms = List.fold_left syms_pv syms vl in
         syms_cty (Sid.add s.rs_name syms) s.rs_cty
+    | Cpur (s,vl) ->
+        List.fold_left syms_pv (Sid.add s.ls_name syms) vl
     | Cfun e -> syms_cty (syms_expr syms e) c.c_cty
     | Cany -> syms_cty syms c.c_cty
   and syms_let_defn syms = function
@@ -401,7 +403,9 @@ let create_let_decl ld =
         let axms = cty_axiom (id_clone ls.ls_name) cty f axms in
         let c = if Mrs.is_empty sm then c else c_rs_subst sm c in
         begin match c.c_node with
-        | Cany | Capp _ ->
+        | Cany | Capp _ | Cpur _ ->
+            (* TODO: should we produce definitions for Capp and Cpur
+               when possible? If yes, remove the redundant axioms. *)
             create_param_decl ls :: abst, defn, axms
         | Cfun e ->
             let res = if c.c_cty.cty_pre <> [] then None else

src/mlw/pmodule.ml

@@ -829,6 +829,11 @@ and clone_cexp cl sm c = c_ghostify (cty_ghost c.c_cty) (match c.c_node with
       let al = List.map (fun v -> clone_ity cl v.pv_ity) c.c_cty.cty_args in
       let res = clone_ity cl c.c_cty.cty_result in
       c_app (Mrs.find_def s s sm.sm_rs) vl al res
+  | Cpur (s,vl) ->
+      let vl = List.map (fun v -> sm_find_pv sm v) vl in
+      let al = List.map (fun v -> clone_ity cl v.pv_ity) c.c_cty.cty_args in
+      let res = clone_ity cl c.c_cty.cty_result in
+      c_pur (cl_find_ls cl s) vl al res
   | Cfun e ->
       let cty = clone_cty cl sm c.c_cty in
       let sm = sm_save_args sm c.c_cty cty in

src/parser/typing.ml

@@ -560,9 +560,11 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
     List.fold_left (fun e1 e2 ->
       DEapp (Dexpr.dexpr ~loc e1, e2)) e el
   in
-  let qualid_app loc q el = match find_prog_symbol muc q with
-    | PV pv -> expr_app loc (DEpv pv) el
-    | RS rs -> expr_app loc (DErs rs) el
+  let qualid_app loc q el =
+    let e = try match find_prog_symbol muc q with
+      | PV pv -> DEpv pv | RS rs -> DErs rs with
+      | _ -> DEls (find_lsymbol muc.muc_theory q) in
+    expr_app loc e el
   in
   let qualid_app loc q el = match q with
     | Qident {id_str = n} ->