Commit d8ecd3b8 authored by Mário Pereira's avatar Mário Pereira
Browse files

Code extraction : started treatment of record projections in function position

parent 614d8b16
......@@ -69,7 +69,6 @@ open Ident
open Ity
open Ty
open Term
open Printer
module ML = struct
......@@ -97,7 +96,6 @@ module ML = struct
type exn =
| Xident of ident
| Xsyntax of string
| Xexit (* Pervasives.Exit *)
type ity = I of Ity.ity | C of Ity.cty (* TODO: keep it like this? *)
......@@ -110,7 +108,6 @@ module ML = struct
and expr_node =
| Econst of Number.integer_constant
| Ebool of bool
| Eident of ident
| Eapp of ident * ident list
| Efun of var list * expr
......@@ -160,16 +157,6 @@ module ML = struct
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
......@@ -238,7 +225,7 @@ module Translate = struct
List.map pvty
(* expressions *)
let rec expr ({e_effect = eff } as e) =
let rec expr info ({e_effect = eff} as e) =
(* assert (not eff.eff_ghost); *)
match e.e_node with
| Econst c ->
......@@ -248,32 +235,31 @@ module Translate = struct
let pv_id = pv_name pvs in
ML.mk_expr (ML.Eident pv_id) (ML.I e.e_ity) eff
| Elet (LDvar (pvs, e1), e2) ->
let ml_let = ML.ml_let (pv_name pvs) (expr e1) (expr e2) in
let ml_let = ML.ml_let (pv_name pvs) (expr info e1) (expr info e2) in
ML.mk_expr ml_let (ML.I e.e_ity) eff
| Eexec ({c_node = Capp (rs, pvl)}, _) ->
let rs_id = rs.rs_name in
let pv_id = List.map pv_name pvl in
let rs_id = rs.rs_name in
let pv_id = List.map pv_name pvl in
ML.mk_expr (ML.Eapp (rs_id, pv_id)) (ML.I e.e_ity) eff
| Eabsurd ->
ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
| Ecase (e1, pl) ->
let e1 = expr e1 in
let pl = List.map ebranch pl in
let e1 = expr info e1 in
let pl = List.map (ebranch info) pl in
ML.mk_expr (ML.Ematch (e1, pl)) (ML.I e.e_ity) eff
| Eassert _ ->
ML.mk_unit
| Eif (e1, e2, e3) ->
let e1 = expr e1 in
let e2 = expr e2 in
let e3 = expr e3 in
let e1 = expr info e1 in
let e2 = expr info e2 in
let e3 = expr info e3 in
ML.mk_expr (ML.Eif (e1, e2, e3)) (ML.I e.e_ity) eff
(* | Eassign [(_, {rs_field = None; rs_name = id}, pv)] -> *)
(* let pv_id = pv_name pv in *)
(* ML.mk_expr ( *)
| Eghost eg ->
expr info eg (* it keeps its ghost status *)
| _ -> (* TODO *) assert false
and ebranch ({pp_pat = p}, e) =
pat p, expr e
and ebranch info ({pp_pat = p}, e) =
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
......@@ -289,7 +275,7 @@ module Translate = struct
rs.rs_name, List.map (fun {pv_vs = pv} -> type_ pv.vs_ty) rsc.cty_args)
(* type declarations/definitions *)
let tdef info itd =
let tdef itd =
let s = itd.itd_its in
let id = itd_name itd in
let args = its_args s in
......@@ -310,8 +296,7 @@ module Translate = struct
| PDlet (LDvar (_, _)) ->
[]
| PDlet (LDsym ({rs_name = rsn; rs_cty = cty}, {c_node = Cfun e})) ->
(* Format.printf "exec:%b@." (Exec.is_exec_pdecl () pd); *)
[ML.Dlet (false, [rsn, args cty.cty_args, expr e])]
[ML.Dlet (false, [rsn, args cty.cty_args, expr info e])]
| PDlet (LDsym ({rs_name = rsn}, {c_node = Capp _})) ->
Format.printf "LDsym Capp--> %s@." rsn.id_string;
[]
......@@ -325,12 +310,12 @@ module Translate = struct
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.rs_name, args rs.rs_cty.cty_args, expr e) rl in
rs.rs_name, args rs.rs_cty.cty_args, expr info e) rl in
[ML.Dlet (true, rec_def)]
| PDpure ->
[]
| PDtype itl ->
List.map (tdef info) itl
List.map tdef itl
| PDexn ({xs_name = xsn} as xs) ->
if ity_equal xs.xs_ity ity_unit then
[ML.Dexn (xsn, None)]
......
......@@ -17,6 +17,19 @@ open Pmodule
open Theory
open Ident
open Pp
open Ity
open Term
open Printer
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;
}
module Print = struct
......@@ -134,41 +147,59 @@ module Print = struct
try Some (Strings.remove_prefix "prefix " s) with Not_found ->
None
let print_apply fmt s vl =
let pv_name pv = pv.pv_vs.vs_name
let print_apply info fmt s vl =
let open Pdecl in
let open Expr in
let is_field {itd_fields = fl} =
List.exists (fun x ->
match x.rs_logic with
| RLls ls -> id_equal ls.ls_name s | _ -> false) fl
in
let isfield =
match Mid.find_opt s info.info_mo_known_map with
| Some {pd_node = PDtype itsd} -> (* can a record be encoded *)
(* in a recursive data-type ? *)
List.exists is_field itsd
| _ -> false
in
match extract_op s, vl with
| Some o, [t1; t2] ->
fprintf fmt "@[<hov 1>%a %s %a@]"
print_ident t1 o print_ident t2
| _, [] ->
print_ident fmt s
print_ident fmt s
| _, [t1] when isfield ->
fprintf fmt "%a.%a" print_ident t1 print_ident s
| _, tl ->
fprintf fmt "@[<hov 2>%a %a@]"
print_ident s (print_list space print_ident) tl
let rec print_enode fmt = function
let rec print_enode info fmt = function
| Econst c ->
fprintf fmt "%a" print_const c
| Eident id ->
print_ident fmt id
| Elet (id, e1, e2) ->
fprintf fmt "@[<hov 2>let @[%a@] =@ @[%a@]@] in@ %a"
print_ident id print_expr e1 print_expr e2
print_ident id (print_expr info) e1 (print_expr info) e2
| Eabsurd ->
fprintf fmt "assert false (* absurd *)"
| Eapp (s, vl) ->
print_apply fmt s vl
print_apply info fmt s vl
| Ematch (e, pl) ->
fprintf fmt "@[begin match @[%a@] with@\n@[<hov>%a@] end@]"
print_expr e (print_list newline print_branch) pl
(print_expr info) e (print_list newline (print_branch info)) pl
| Eblock [] ->
fprintf fmt "()"
| _ -> (* TODO *) assert false
and print_branch fmt (p, e) =
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_expr e
and print_branch info fmt (p, e) =
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p (print_expr info) e
and print_expr fmt e =
print_enode fmt e.e_node
and print_expr info fmt e =
print_enode info fmt e.e_node
let print_type_decl fmt (id, args, tydef) =
let print_constr fmt (id, cs_args) =
......@@ -203,13 +234,13 @@ module Print = struct
-> print_lident *)
print_def tydef
let print_decl fmt = function
let print_decl info fmt = function
| Dlet (isrec, [id, vl, e]) ->
fprintf fmt "@[<hov 2>%s %a@ %a =@ %a@]"
(if isrec then "let rec" else "let")
print_ident id
(print_list space print_vs_arg) vl
print_expr e;
(print_expr info) e;
fprintf fmt "@\n@\n"
| Dtype dl ->
print_list newline print_type_decl fmt dl;
......@@ -236,11 +267,12 @@ 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@\n" print_module m;
fprintf fmt
"(* This file has been generated from Why3 module %a *)@\n@\n"
Print.print_module_name m;
let mdecls = Translate.module_ info m in
print_list nothing Print.print_decl fmt mdecls;
print_list nothing (Print.print_decl info) fmt mdecls;
fprintf fmt "@."
let fg ?fname m =
......
......@@ -13,8 +13,6 @@ open Format
open Why3
open Stdlib
open Pmodule
(* open Compile (\* intermediate ML AST *\) *)
(* open Ocaml_printer *)
let usage_msg = sprintf
"Usage: %s [options] -D <driver> -o <dir> [[file|-] [-T <theory>]...]..."
......@@ -130,21 +128,6 @@ let extract_to =
let rec use_iter f l =
List.iter (function Uuse t -> f t | Uscope (_,_,l) -> use_iter f l | _ -> ()) l
(* let test_extract ?fname m = *)
(* Format.printf "antes@\n"; *)
(* let (fg, _, _) = Pdriver.lookup_printer opt_driver in *)
(* Format.printf "aqui@\n"; *)
(* let file = Filename.concat opt_output (fg ?fname m) in *)
(* let cout = open_out file in *)
(* let fmt = formatter_of_out_channel cout in *)
(* fprintf fmt "(\*@\n"; *)
(* print_module fmt m; *)
(* fprintf fmt "(\*@\n"; *)
(* fprintf fmt "@\n@\n"; *)
(* (\* Translate.module_ m *\) *)
(* extract_module opt_driver fmt m; *)
(* close_out cout *)
let rec do_extract_module ?fname m =
(* test_extract ?fname m; *)
let _extract_use m' =
......
......@@ -3,26 +3,26 @@ module M
use import int.Int
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 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;
......@@ -31,33 +31,38 @@ module M
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
end
(* 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 t (x:int) : int *)
(* requires { false } *)
(* = absurd *)
let a () : unit
= assert { true }
(* let a () : unit *)
(* = assert { true } *)
let singleton (x: int) (l: list int) : list int =
let x = Nil in x
(* let singleton (x: int) (l: list int) : list int = *)
(* let x = Nil in x *)
let test (x: int) : int =
let y = x in y + 1
(* use import int.Int *)
(* let test (x: int) : int = *)
(* let y = *)
(* let z = x in *)
(* (ghost z) + 1 *)
(* in 42 *)
end
......
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