Commit 3172196f authored by Mário Pereira's avatar Mário Pereira

Code extraction (wip)

parent d02c17b3
......@@ -91,9 +91,8 @@ module ML = struct
type pat =
| Pwild
| Pident of ident
| Papp of ident * pat list
| Papp of lsymbol * pat list
| Ptuple of pat list
| Precord of (ident * pat) list
| Por of pat * pat
| Pas of pat * ident
......@@ -282,7 +281,7 @@ module Translate = struct
(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)
ML.Papp (ls, List.rev pat_pl)
(** programs *)
......@@ -343,15 +342,9 @@ module Translate = struct
ML.mk_expr (ML.Eapp (rsc, args)) (ML.C cty_app) cty_app.cty_effect in
ML.mk_expr (ML.Efun (args_f, eapp)) (ML.C cty_app) cty_app.cty_effect
let app info rs pvl =
let app pvl =
let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in
if isconstructor info rs then
filter_ghost_params pv_not_ghost def pvl
else
let al _ = ML.mk_unit in
filter2_ghost_params pv_not_ghost def al pvl
(* let rec let_defn *)
filter_ghost_params pv_not_ghost def pvl
(* expressions *)
let rec expr info ({e_effect = eff} as e) =
......@@ -388,7 +381,7 @@ module Translate = struct
let ml_letrec = ML.Elet (ML.Lsym (rsf, [], eta_app), ein) in
ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
| Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) ->
let pvl = app info rs_app pvl in
let pvl = app pvl in
let eapp =
ML.mk_expr (ML.Eapp (rs_app, pvl)) (ML.C cty) cty.cty_effect in
let ein = expr info ein in
......@@ -417,7 +410,7 @@ module Translate = struct
| Eexec ({c_node = Capp (rs, _)}, _) when rs_ghost rs ->
ML.mk_unit
| Eexec ({c_node = Capp (rs, pvl); _}, _) ->
let pvl = app info rs pvl in
let pvl = app pvl in
ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff
| Eexec ({c_node = Cfun e; c_cty = cty}, _) ->
let def pv = pv_name pv, ity pv.pv_ity, pv.pv_ghost in
......@@ -559,13 +552,31 @@ module Translate = struct
end
(** Erasure operations related to ghost code *)
(** Optimistion operations *)
(* module Erasure = struct *)
(* open ML *)
(* let rec remove_superf_let subs e = *)
(* match e.e_node with *)
(* | Evar pv -> try let Hpv.find pv *)
(* | Eapp of rsymbol * expr list *)
(* | Efun of var list * expr *)
(* | Elet of let_def * expr *)
(* | Eif of expr * expr * expr *)
(* | Ecast of expr * ty *)
(* | Eassign of (pvsymbol * rsymbol * pvsymbol) list *)
(* | Etuple of expr list (\* at least 2 expressions *\) *)
(* | Ematch of expr * (pat * expr) list *)
(* | Ebinop of expr * binop * expr *)
(* | Enot of expr *)
(* | Eblock of expr list *)
(* | Ewhile of expr * expr *)
(* | Efor of pvsymbol * pvsymbol * for_direction * pvsymbol * expr *)
(* | Eraise of exn * expr option *)
(* | Etry of expr * (exn * pvsymbol option * expr) list *)
(* | _ -> e.e_node *)
(* end *)
......
......@@ -68,7 +68,6 @@ module Print = struct
| Pwild -> ()
| Pident id -> forget_id id
| Papp (_, pl) | Ptuple pl -> List.iter forget_pat pl
| Precord pl -> List.iter (fun (_,p) -> forget_pat p) pl
| Por (p1, p2) -> forget_pat p1; forget_pat p2
| Pas (p, _) -> forget_pat p
......@@ -163,73 +162,87 @@ module Print = struct
let print_module_name fmt m =
print_theory_name fmt m.mod_theory
let rec print_pat fmt = function
let get_record info rs =
match Mid.find_opt rs.rs_name info.info_mo_known_map with
| Some {pd_node = PDtype itdl} ->
let itd = List.find (fun {itd_constructors=constr} ->
List.exists (rs_equal rs) constr) itdl in
List.filter (fun e -> not (rs_ghost e)) itd.itd_fields
| _ -> []
let rec print_pat info fmt = function
| Pwild ->
fprintf fmt "_"
| Pident id ->
print_ident fmt id
| Pas (p, id) ->
fprintf fmt "%a as %a" print_pat p print_ident id
fprintf fmt "%a as %a" (print_pat info) p print_ident id
| Por (p1, p2) ->
fprintf fmt "%a | %a" print_pat p1 print_pat p2
fprintf fmt "%a | %a" (print_pat info) p1 (print_pat info) p2
| Ptuple pl ->
fprintf fmt "(%a)" (print_list comma print_pat) pl
| Papp (id, []) ->
print_ident fmt id
| Papp (id, [p]) ->
fprintf fmt "%a %a" print_ident id print_pat p
| Papp (id, pl) ->
fprintf fmt "%a (%a)" print_ident id (print_list comma print_pat) pl
| Precord fl ->
let print_field fmt (id, p) =
fprintf fmt "%a = %a" print_ident id print_pat p
in
fprintf fmt "{ %a }" (print_list semi print_field) fl
fprintf fmt "(%a)" (print_list comma (print_pat info)) pl
| Papp (ls, pl) ->
match query_syntax info.info_syn ls.ls_name, pl with
| Some s, _ ->
syntax_arguments s (print_pat info) fmt pl
| None, pl ->
let rs = restore_rs ls in
let pjl = get_record info rs in
match pjl, pl with
| [], [] ->
fprintf fmt "%a" (print_uident info) ls.ls_name
| [], [p] ->
fprintf fmt "%a %a"
(print_uident info) ls.ls_name (print_pat info) p
| [], _ ->
fprintf fmt "%a (%a)"
(print_uident info) ls.ls_name
(print_list comma (print_pat info)) pl
| _, _ ->
let rec print_list2 sep sep_m print1 print2 fmt (l1, l2) =
match l1, l2 with
| x1 :: r1, x2 :: r2 ->
print1 fmt x1; sep_m fmt (); print2 fmt x2; sep fmt ();
print_list2 sep sep_m print1 print2 fmt (r1, r2)
| _ -> ()
in
let print_rs info fmt rs =
fprintf fmt "%a" (print_lident info) rs.rs_name in
fprintf fmt "@[<hov 2>{ %a}@]"
(print_list2 semi equal (print_rs info) (print_pat info)) (pjl, pl)
(** Expressions *)
let extract_op {id_string = s} =
try Some (Strings.remove_prefix "infix " s) with Not_found ->
try Some (Strings.remove_prefix "prefix " s) with Not_found ->
None
let pv_name pv = pv.pv_vs.vs_name
let get_record info rs =
match Mid.find_opt rs.rs_name info.info_mo_known_map with
| Some {pd_node = PDtype itdl} ->
let itd = List.find (fun {itd_constructors=constr} ->
List.exists (rs_equal rs) constr) itdl in
List.filter (fun e -> not (rs_ghost e)) itd.itd_fields
| _ -> []
let ht_rs = Hrs.create 7 (* rec_rsym -> rec_sym *)
let rec args_syntax info fmt s tl =
try
ignore (Str.search_forward (Str.regexp "[%]\\([tv]?\\)[0-9]+") s 0);
syntax_arguments s (print_expr info) fmt tl
with Not_found -> ()
and 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 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
| _ -> false in
match query_syntax info.info_convert rs.rs_name,
query_syntax info.info_syn rs.rs_name, pvl with
| Some s, _, _
| Some s, _, _ ->
let print_constant fmt e = match e.e_node with
| Econst c ->
let c = BigInt.to_int (Number.compute_int c) in
fprintf fmt "%d" c
| _ -> print_expr info fmt e in
syntax_arguments s print_constant fmt pvl
| _, Some s, _ ->
syntax_arguments s (print_expr info) fmt pvl
| _, _, tl when is_rs_tuple rs ->
fprintf fmt "@[(%a)@]"
(print_list comma (print_expr info)) tl
| _, _, [] ->
print_ident fmt rs.rs_name
| _, _, [t1] when isfield ->
......@@ -245,22 +258,19 @@ module Print = struct
| x1 :: r1, x2 :: r2 ->
print1 fmt x1; sep_m fmt (); print2 fmt x2; sep fmt ();
print_list2 sep sep_m print1 print2 fmt (r1, r2)
| _ -> ()
in
| _ -> () in
let print_rs info fmt rs =
fprintf fmt "%a" (print_lident info) rs.rs_name
in
fprintf fmt "%a" (print_lident info) rs.rs_name in
fprintf fmt "@[<hov 2>{ %a}@]"
(print_list2 semi equal (print_rs info) (print_expr info)) (pjl, tl)
| _, _, tl ->
fprintf fmt "@[<hov 2>%a %a@]"
print_ident rs.rs_name (print_list space (print_expr info)) tl
fprintf fmt "@[<hov 2>%a %a@]"
print_ident rs.rs_name (print_list space (print_expr info)) tl
and print_let_def info fmt = function
| Lvar (pv, e) ->
fprintf fmt "@[<hov 2>let %a =@ %a@]"
(print_lident info) (pv_name pv) (print_expr info) e;
(* forget_id (pv_name pv) *)
| Lsym (rs, args, ef) ->
fprintf fmt "@[<hov 2>let %a %a@ =@ @[%a@]@]"
(print_lident info) rs.rs_name
......@@ -356,7 +366,8 @@ module Print = struct
| Eassign _ -> (* TODO *) assert false
and print_branch info fmt (p, e) =
fprintf fmt "@[<hov 4>| %a ->@ @[%a@]@]" print_pat p (print_expr info) e
fprintf fmt "@[<hov 4>| %a ->@ @[%a@]@]"
(print_pat info) p (print_expr info) e
and print_expr info fmt e =
print_enode info fmt e.e_node
......@@ -424,6 +435,7 @@ let extract_module pargs ?old fmt ({mod_theory = th} as m) =
info_mo_known_map = m.mod_known;
info_fname = None; (* TODO *)
} in
(* fprintf fmt "(\*@\n%a@\n*\)@\n" print_module m; *)
fprintf fmt
"(* This file has been generated from Why3 module %a *)@\n@\n"
Print.print_module_name m;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment