Code extraction : erasure of ghost code in function definition, application, and pattern-matching

src/mlw/compile.ml

@@ -56,6 +56,8 @@
     - faire un module Erasure, pour y concentrer tout ce qui
       appartient à l'éffacement du code fantôme ?
 
+    - comment est-ce qu'il marche la [mask] d'un [prog_pattern] ?
+
  *)
 
 (*
@@ -69,11 +71,11 @@ open Ident
 open Ity
 open Ty
 open Term
+open Printer
 
 module ML = struct
 
   open Expr
-  open Pdecl
 
   type ty =
     | Tvar    of tvsymbol
@@ -114,12 +116,13 @@ module ML = struct
   and expr_node =
     | Econst  of Number.integer_constant
     | Evar    of pvsymbol
-    | Eapp    of rsymbol * pvsymbol list
+    | Eapp    of rsymbol * expr list
     | Efun    of var list * expr
     | Elet    of pvsymbol * expr * expr
     | Eletrec of is_rec * (rsymbol * var list * expr) list * expr
     | Eif     of expr * expr * expr
     | Ecast   of expr * ty
+    | Eassign of (rsymbol * pvsymbol) list
     | Etuple  of expr list (* at least 2 expressions *)
     | Ematch  of expr * (pat * expr) list
     | Ebinop  of expr * binop * expr
@@ -170,8 +173,26 @@ module ML = struct
   let mk_its_defn id args private_ def =
     { its_name = id; its_args = args; its_private = private_; its_def = def; }
 
+  let eseq e1 e2 =
+    match e1.e_node, e2.e_node with
+    | Eblock [], e | e, Eblock [] -> e
+    | Eblock e1, Eblock e2 -> Eblock (e1 @ e2)
+    | _, Eblock e2 -> Eblock (e1 :: e2)
+    | Eblock e1, _ -> Eblock (e1 @ [e2])
+    | _ -> Eblock [e1; e2]
+
 end
 
+type info = {
+  info_syn          : syntax_map;
+  info_convert      : syntax_map;
+  info_current_th   : Theory.theory;
+  info_current_mo   : Pmodule.pmodule option;
+  info_th_known_map : Decl.known_map;
+  info_mo_known_map : Pdecl.known_map;
+  info_fname        : string option;
+}
+
 (** Translation from Mlw to ML *)
 
 module Translate = struct
@@ -197,35 +218,76 @@ module Translate = struct
   let type_args = (* point-free *)
     List.map (fun x -> x.tv_name)
 
+  let filter_ghost_params l =
+    let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in
+    let p e = not e.pv_ghost in
+    let rec filter_ghost_params_cps l k =
+      match l with
+      | [] -> k []
+      | e :: r ->
+        filter_ghost_params_cps r
+          (fun fr -> k (if p e then (def e) :: fr else fr))
+    in
+    filter_ghost_params_cps l (fun x -> x)
+
+  let filter2_ghost_params p def al l =
+    let rec filter2_ghost_params_cps l k =
+      match l with
+      | []  -> k []
+      | [e] -> k (if p e then [def e] else [al e])
+      | e :: r ->
+        filter2_ghost_params_cps r
+          (fun fr -> k (if p e then (def e) :: fr else fr))
+    in
+    filter2_ghost_params_cps l (fun x -> x)
+
+  let rec filter_ghost_params_pat = function
+    | MaskVisible -> Format.printf "visible@\n"
+    | MaskGhost   -> Format.printf "ghost@\n"
+    | MaskTuple l ->
+      Format.printf "list@\n";
+      List.iter (filter_ghost_params_pat) l
+
   let rec pat p =
     match p.pat_node with
     | Pwild ->
-       ML.Pwild
+      ML.Pwild
     | Pvar vs ->
-       ML.Pident vs.vs_name
+      ML.Pident vs.vs_name
     | Por (p1, p2) ->
-       ML.Por (pat p1, pat p2)
+      ML.Por (pat p1, pat p2)
     | Pas (p, vs) ->
-       ML.Pas (pat p, vs.vs_name)
+      ML.Pas (pat p, vs.vs_name)
     | Papp (ls, pl) when is_fs_tuple ls ->
-       ML.Ptuple (List.map pat pl)
+      ML.Ptuple (List.map pat pl)
     | Papp (ls, pl) ->
-       ML.Papp (ls.ls_name, List.map pat pl)
+      let rs = restore_rs ls in
+      let args = rs.rs_cty.cty_args in
+      let pat_pl = List.fold_left2
+          (fun acc pv pp -> if not pv.pv_ghost then (pat pp) :: acc else acc)
+          [] args pl
+      in
+      ML.Papp (ls.ls_name, List.rev pat_pl)
 
   (** programs *)
 
+  let pv_name pv = pv.pv_vs.vs_name
+
+  let is_underscore pv =
+    (pv_name pv).id_string = "_" && ity_equal pv.pv_ity ity_unit
+
   (* individual types *)
   let rec ity t =
     match t.ity_node with
     | Ityvar (tvs, _) ->
-       ML.Tvar tvs
+      ML.Tvar tvs
     | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
-       ML.Ttuple (List.map ity itl)
+      ML.Ttuple (List.map ity itl)
     | Ityapp ({its_ts = ts}, itl, _) ->
-       ML.Tapp (ts.ts_name, List.map ity itl)
-    | _ -> (* TODO *) assert false
-
-  let pv_name pv = pv.pv_vs.vs_name
+      ML.Tapp (ts.ts_name, List.map ity itl)
+    | Ityreg {reg_its = its; reg_args = args} ->
+      let args = List.map ity args in
+      ML.Tapp (its.its_ts.ts_name, args)
 
   let pvty pv =
     if pv.pv_ghost then
@@ -242,6 +304,23 @@ module Translate = struct
   let args = (* point-free *)
     List.map pvty
 
+  let app info rs pvl =
+    let isconstructor () =
+      match Mid.find_opt rs.rs_name info.info_mo_known_map with
+      | Some {pd_node = PDtype its} ->
+        let is_constructor its =
+          List.exists (rs_equal rs) its.itd_constructors in
+        List.exists is_constructor its
+      | _ -> false
+    in
+    match pvl with
+    | pvl when isconstructor () -> filter_ghost_params pvl
+    | pvl ->
+      let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in
+      let al _ = ML.mk_unit in
+      let p e = not e.pv_ghost in
+      filter2_ghost_params p def al pvl
+
   (* expressions *)
   let rec expr info ({e_effect = eff} as e) =
     (* assert (not eff.eff_ghost); *)
@@ -250,14 +329,26 @@ module Translate = struct
        let c = match c with Number.ConstInt c -> c | _ -> assert false in
        ML.mk_expr (ML.Econst c) (ML.I e.e_ity) eff
     | Evar pvs ->
-       ML.mk_expr (ML.Evar pvs) (ML.I e.e_ity) eff
+      ML.mk_expr (ML.Evar pvs) (ML.I e.e_ity) eff
+    | Elet (LDvar (pvs, e1), e2) when is_underscore pvs ->
+      ML.mk_expr (ML.eseq (expr info e1) (expr info e2)) (ML.I e.e_ity) eff
+    | Elet (LDvar (pvs, e1), e2) when e_ghost e1 ->
+      let ml_let = ML.ml_let pvs ML.mk_unit (expr info e2) in
+       ML.mk_expr ml_let (ML.I e.e_ity) eff
     | Elet (LDvar (pvs, e1), e2) ->
        let ml_let = ML.ml_let pvs (expr info e1) (expr info e2) in
        ML.mk_expr ml_let (ML.I e.e_ity) eff
+    | Eexec ({c_node = Capp (rs, [])}, _) when is_rs_tuple rs ->
+      ML.mk_unit
+    | Eexec ({c_node = Capp (rs, _)}, _) when rs_ghost rs ->
+      ML.mk_unit
     | Eexec ({c_node = Capp (rs, pvl)}, _) ->
-       ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff
+      let pvl = app info rs pvl in
+      ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff
     | Eabsurd ->
-       ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
+      ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
+    | Ecase (e1, _) when e_ghost e1 ->
+      ML.mk_unit
     | Ecase (e1, pl) ->
        let e1 = expr info e1 in
        let pl = List.map (ebranch info) pl in
@@ -270,11 +361,13 @@ module Translate = struct
        let e3 = expr info e3 in
        ML.mk_expr (ML.Eif (e1, e2, e3)) (ML.I e.e_ity) eff
     | Eghost eg ->
-       expr info eg (* it keeps its ghost status *)
+      expr info eg (* it keeps its ghost status *)
+    | Eassign [(_, rs, pv)] ->
+      ML.mk_expr (ML.Eassign [(rs, pv)]) (ML.I e.e_ity) eff
     | _ -> (* TODO *) assert false
 
-  and ebranch info ({pp_pat = p}, e) =
-    pat p, expr info e
+  and ebranch info ({pp_pat = p} as pp, e) =
+    (filter_ghost_params_pat pp.pp_mask; pat p, expr info e)
 
   let its_args ts = ts.its_ts.ts_args
   let itd_name td = td.itd_its.its_ts.ts_name
@@ -313,24 +406,31 @@ module Translate = struct
   (* program declarations *)
   let pdecl info pd =
     match pd.pd_node with
-    | PDlet (LDvar (_, _)) ->
-       []
+    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
+      []
     | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
-       [ML.Dlet (false, [rs, args cty.cty_args, expr info e])]
-    | PDlet (LDsym ({rs_name = rsn}, {c_node = Capp _})) ->
-       []
-    | PDlet (LDsym ({rs_name = rsn}, {c_node = Cpur _})) ->
-       []
-    | PDlet (LDsym ({rs_name = rsn}, {c_node = Cany})) ->
-       []
+      let args_filter =
+        let p (_, _, is_ghost) = not is_ghost in
+        let def = fun x -> x in
+        let al = fun x -> x in
+        filter2_ghost_params p def al (args cty.cty_args) in
+      [ML.Dlet (false, [rs, args_filter, expr info e])]
     | PDlet (LDrec rl) ->
-       let rec_def =
-         List.map (fun {rec_fun = e; rec_rsym = rs} ->
-           let e = match e.c_node with Cfun e -> e | _ -> assert false in
-           rs, args rs.rs_cty.cty_args, expr info e) rl in
-       [ML.Dlet (true, rec_def)]
+      let rec_def =
+        List.map (fun {rec_fun = e; rec_rsym = rs} ->
+          let e = match e.c_node with Cfun e -> e | _ -> assert false in
+          let args_filter =
+            let p (_, _, is_ghost) = not is_ghost in
+            let def = fun x -> x in
+            let al = fun x -> x in
+            filter2_ghost_params p def al (args rs.rs_cty.cty_args) in
+          rs, args_filter, expr info e) rl
+      in
+      [ML.Dlet (true, rec_def)]
+    | PDlet (LDsym _)
+    | PDlet (LDvar (_, _))
     | PDpure ->
-       []
+      []
     | PDtype itl ->
        [ML.Dtype (List.map tdef itl)]
     | PDexn xs ->

src/mlw/ocaml_printer.ml

@@ -13,25 +13,15 @@
 
 open Compile
 open Format
-open Pmodule
-open Theory
 open Ident
 open Pp
 open Ity
 open Term
-open Printer
 open Expr
 open Ty
-
-type info = {
-  info_syn          : syntax_map;
-  info_convert      : syntax_map;
-  info_current_th   : Theory.theory;
-  info_current_mo   : Pmodule.pmodule option;
-  info_th_known_map : Decl.known_map;
-  info_mo_known_map : Pdecl.known_map;
-  info_fname        : string option;
-}
+open Theory
+open Pmodule
+open Stdlib
 
 module Print = struct
 
@@ -48,6 +38,11 @@ module Print = struct
      "true"; "try"; "type"; "val"; "virtual"; "when"; "while"; "with";
      "raise";]
 
+  let is_ocaml_keyword =
+    let h = Hstr.create 16 in
+    List.iter (fun s -> Hstr.add h s ()) ocaml_keywords;
+    Hstr.mem h
+
   let iprinter, aprinter =
     let isanitize = sanitizer char_to_alpha char_to_alnumus in
     let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
@@ -58,8 +53,29 @@ module Print = struct
     let s = id_unique iprinter id in
     fprintf fmt "%s" s
 
-  (* let print_lident = print_qident ~sanitizer:Strings.uncapitalize *)
-  (* let print_uident = print_qident ~sanitizer:Strings.capitalize *)
+  let print_qident ~sanitizer info fmt id =
+    try
+      let lp, m, q =
+        try Pmodule.restore_path id
+        with Not_found -> Theory.restore_path id in
+      let s = String.concat "__" q in
+      let s = Ident.sanitizer char_to_alpha char_to_alnumus s in
+      let s = sanitizer s in
+      let s = if is_ocaml_keyword s then s ^ "_renamed" else s in
+      if Sid.mem id info.info_current_th.th_local ||
+         Opt.fold (fun _ m -> Sid.mem id m.Pmodule.mod_local)
+           false info.info_current_mo
+      then fprintf fmt "%s" s
+      else
+        let fname = if lp = [] then info.info_fname else None in
+        let m = Strings.capitalize "m" in
+        fprintf fmt "%s.%s" m s
+    with Not_found ->
+      let s = id_unique ~sanitizer iprinter id in
+      fprintf fmt "%s" s
+
+  let print_lident = print_qident ~sanitizer:Strings.uncapitalize
+  let print_uident = print_qident ~sanitizer:Strings.capitalize
 
   let print_tv fmt tv =
     fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
@@ -73,21 +89,21 @@ module Print = struct
 
   let rec print_ty ?(paren=false) fmt = function
     | Tvar tv ->
-       print_tv fmt tv
+      print_tv fmt tv
     | Ttuple [] ->
-       fprintf fmt "unit"
+      fprintf fmt "unit"
     | Ttuple tl ->
-       fprintf fmt (protect_on paren "@[%a@]")
-               (print_list star (print_ty ~paren:false)) tl
+      fprintf fmt (protect_on paren "@[%a@]")
+        (print_list star (print_ty ~paren:false)) tl
     | Tapp (ts, []) ->
-       print_ident fmt ts
+      print_ident fmt ts
     | Tapp (ts, [ty]) ->
-       fprintf fmt (protect_on paren "%a@ %a")
-               (print_ty ~paren:true) ty print_ident ts
+      fprintf fmt (protect_on paren "%a@ %a")
+        (print_ty ~paren:true) ty print_ident ts
     | Tapp (ts, tl) ->
-       fprintf fmt (protect_on paren "(%a)@ %a")
-               (print_list comma (print_ty ~paren:false)) tl
-               print_ident ts
+      fprintf fmt (protect_on paren "(%a)@ %a")
+        (print_list comma (print_ty ~paren:false)) tl
+        print_ident ts
 
   let print_vsty fmt (v, ty, _) =
     fprintf fmt "%a:@ %a" print_ident v (print_ty ~paren:false) ty
@@ -151,32 +167,43 @@ module Print = struct
 
   let pv_name pv = pv.pv_vs.vs_name
 
-  let print_apply info fmt rs pvl =
+  let rec print_apply info fmt rs pvl =
     let isfield =
       match rs.rs_field with
       | None -> false
-      | Some _ -> true
+      | Some _ -> true in
+    let isconstructor () =
+      let open Pdecl in
+      match Mid.find_opt rs.rs_name info.info_mo_known_map with
+      | Some {pd_node = PDtype its} ->
+        let is_constructor its =
+          List.exists (rs_equal rs) its.itd_constructors in
+        List.exists is_constructor its
+      | _ -> false
     in
     match extract_op rs.rs_name, pvl with
     | Some o, [t1; t2] ->
        fprintf fmt "@[<hov 1>%a %s %a@]"
-         print_pv t1 o print_pv t2
+         (print_expr info) t1 o (print_expr info) t2
     | _, [] ->
        print_ident fmt rs.rs_name
     | _, [t1] when isfield ->
-       fprintf fmt "%a.%a" print_pv t1 print_ident rs.rs_name
+      fprintf fmt "%a.%a" (print_expr info) t1 print_ident rs.rs_name
+    | _, tl when isconstructor () ->
+      fprintf fmt "@[<hov 2>%a (%a)@]"
+        print_ident rs.rs_name (print_list comma (print_expr info)) tl
     | _, tl ->
        fprintf fmt "@[<hov 2>%a %a@]"
-         print_ident rs.rs_name (print_list space print_pv) tl
+         print_ident rs.rs_name (print_list space (print_expr info)) tl
 
-  let rec print_enode info fmt = function
+  and print_enode info fmt = function
     | Econst c ->
        fprintf fmt "%a" print_const c
     | Evar pvs ->
-       print_ident fmt (pv_name pvs)
+       (print_lident info) fmt (pv_name pvs)
     | Elet (pv, e1, e2) ->
        fprintf fmt "@[<hov 2>let @[%a@] =@ @[%a@]@] in@ %a"
-         print_ident (pv_name pv) (print_expr info) e1 (print_expr info) e2
+         (print_lident info) (pv_name pv) (print_expr info) e1 (print_expr info) e2
     | Eabsurd ->
        fprintf fmt "assert false (* absurd *)"
     | Eapp (s, []) when rs_equal s rs_true ->
@@ -186,10 +213,20 @@ module Print = struct
     | Eapp (s, pvl) ->
        print_apply info fmt s pvl
     | Ematch (e, pl) ->
-       fprintf fmt "@[begin match @[%a@] with@\n@[<hov>%a@] end@]"
-         (print_expr info) e (print_list newline (print_branch info)) pl
+      fprintf fmt "@[begin match @[%a@] with@\n@[<hov>%a@] end@]"
+        (print_expr info) e (print_list newline (print_branch info)) pl
+    | Eassign [(rs, pv)] ->
+      fprintf fmt "%a <-@ %a" print_ident rs.rs_name print_ident (pv_name pv)
+    | Eif (e1, e2, e3) ->
+      fprintf fmt
+        "@[<hv>@[<hov 2>if@ %a@]@ then@;<1 2>@[%a@]@;<1 0>else@;<1 2>@[%a@]@]"
+        (print_expr info) e1 (print_expr info) e2 (print_expr info) e3
     | Eblock [] ->
-       fprintf fmt "()"
+      fprintf fmt "()"
+    | Eblock [e] ->
+      print_expr info fmt e
+    | Eblock el ->
+      fprintf fmt "@[<hv>begin@;<1 2>@[%a@]@ end@]" (print_list semi (print_expr info)) el
     | _ -> (* TODO *) assert false
 
   and print_branch info fmt (p, e) =
@@ -235,7 +272,7 @@ module Print = struct
 
   let print_decl info fmt = function
     | Dlet (isrec, [rs, pvl, e]) ->
-       fprintf fmt "@[<hov 2>%s %a@ %a =@ %a@]"
+       fprintf fmt "@[<hov 2>%s %a@ %a@ =@ %a@]"
                (if isrec then "let rec" else "let")
                print_ident rs.rs_name
                (print_list space print_vs_arg) pvl

tests/test_extraction_mario.mlw

 module M
 
   use import int.Int
-  use import seq.Seq
+  (* use import seq.Seq *)
 
-  let function f (y: int) (x: int) : int
-    requires { x >= 0 }
-    ensures  { result >= 0 }
-  = x
+  (* let function f (y: int) (x: int) : int *)
+  (*   requires { x >= 0 } *)
+  (*   ensures  { result >= 0 } *)
+  (* = x *)
 
-  let g (ghost z: int) (x: int) : int
-    requires { x > 0 }
-    ensures  { result > 0 }
-  = let y = x in
-    y
+  (* let g (ghost z: int) (x: int) : int *)
+  (*   requires { x > 0 } *)
+  (*   ensures  { result > 0 } *)
+  (* = let y = x in *)
+  (*   y *)
 
-  type t 'a 'b 'c 'd
+  (* type t 'a 'b 'c 'd *)
 
-  type list 'a = Nil | Cons 'a (list 'a)
+  (* type list 'a = Nil | Cons 'a (list 'a) *)
 
-  type btree 'a = E | N (btree 'a) 'a (btree 'a)
+  (* type btree 'a = E | N (btree 'a) 'a (btree 'a) *)
 
-  type ntree 'a = Empty | Node 'a (list 'a)
+  (* type ntree 'a = Empty | Node 'a (list 'a) *)
 
-  type list_int = list int
+  (* type list_int = list int *)
 
-  type cursor 'a = {
-    collection : list 'a;
-    index      : int;
-    mutable index2     : int;
-    ghost mutable v : seq 'a;
-  }
+  (* type cursor 'a = { *)
+  (*   collection : list 'a; *)
+  (*   index      : int; *)
+  (*   mutable index2     : int; *)
+  (*   ghost mutable v : seq 'a; *)
+  (* } *)
 
-  use import ref.Ref
+  (* use import ref.Ref *)
 
-  let update (c: cursor int) : int
-  = c.index
+  (* let update (c: cursor int) : int *)
+  (* = c.index *)
 
-  exception Empty (list int, int)
-  exception Out_of_bounds int
+  (* exception Empty (list int, int) *)
+  (* exception Out_of_bounds int *)
 
-  let rec length (l: list 'a) : int
-    variant  { l }
-  = match l with
-    | Nil -> 0
-    | Cons _ r -> 1 + length r
+  (* let rec length (l: list 'a) : int *)
+  (*   variant  { l } *)
+  (* = match l with *)
+  (*   | Nil -> 0 *)
+  (*   | Cons _ r -> 1 + length r *)
+  (*   end *)
+
+  (* let t (x:int) : int *)
+  (*   requires { false } *)
+  (* = absurd *)
+
+  (* let a () : unit *)
+  (* = assert { true } *)
+
+  (* let singleton (x: int) (l: list int) : list int = *)
+  (*   let x = Nil in x *)
+
+  (* use import int.Int *)
+
+  (* let test (x: int) : int = *)
+  (*   let y = *)
+  (*     let z = x in *)
+  (*     (ghost z) + 1 *)
+  (*   in 42 *)
+
+  type list_ghost = Nil2 | Cons2 int list_ghost (ghost int)
+
+  let add_list_ghost (x: int) (l: list_ghost) : list_ghost =
+    match l with
+    | Cons2 _ Nil2 _ | Nil2 -> Cons2 x Nil2 1
+    | Cons2 _ _ n -> Cons2 x l (n+1)
     end
 
-  let t (x:int) : int
-    requires { false }
-  = absurd
+  type t = { c: int; ghost c2: (int, bool, int) }
 
-  let a () : unit
-  = assert { true }
+  let ghost f (x: t) : int =
+    match x.c2 with
+    | (n, b, m) -> m
+    end
 
-  let singleton (x: int) (l: list int) : list int =
-    let x = Nil in x
+  let ggg () : int = 42
 
-  use import int.Int
+  let call (x:int) : int =
+    ggg () + 42
+
+  let test_filter_ghost_args (x: int) (ghost y: int) : int =
+    x + 42
+
+  let test_filter_ghost_args2 (x: int) (ghost y: int) (z: int) : int =
+    x + z
+
+  let test_filter_ghost_args3 (ghost y: int) : int =
+    42
+
+  let test_call (x: int) : int =
+    test_filter_ghost_args x 0
+
+  let many_args (a b c d e f g h i j k l m: int) : int = 42
 
-  let test (x: int) : int =
-    let y =
-      let z = x in
-      (ghost z) + 1
-    in 42
+  let foo (x: int) : int =
+    let _ = 42 in
+    x
 
 end