Skip to content

GitLab

why3
why3
Commit a469b306 authored by Mário Pereira's avatar Mário Pereira
Browse files
Options

Code extraction : some changes in the AST; deleted exec.ml file

parent d8ecd3b8
Hide whitespace changes
Inline Side-by-side
Showing with 153 additions and 211 deletions
Makefile.in
View file @ a469b306
......@@ -177,7 +177,7 @@ LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer dri
parse_smtv2_model_parser parse_smtv2_model_lexer parse_smtv2_model
LIB_MLW = ity expr dexpr pdecl eval_match vc pmodule \
pinterp pdriver cprinter exec compile ocaml_printer
pinterp pdriver cprinter compile ocaml_printer
LIB_PARSER = ptree glob typing parser lexer
......
src/mlw/compile.ml
View file @ a469b306
......@@ -72,12 +72,17 @@ open Term
module ML = struct
open Expr
open Pdecl
type ty =
| Tvar of ident
| Tvar of tvsymbol
| Tapp of ident * ty list
| Ttuple of ty list
type var = ident * ty
type is_ghost = bool
type var = ident * ty * is_ghost
type pat =
| Pwild
......@@ -108,38 +113,43 @@ module ML = struct
and expr_node =
| Econst of Number.integer_constant
| Eident of ident
| Eapp of ident * ident list
| Evar of pvsymbol
| Eapp of rsymbol * pvsymbol list
| Efun of var list * expr
| Elet of ident * expr * expr
| Eletrec of is_rec * (ident * var list * expr) 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
| Etuple of expr list (* at least 2 expressions *)
| Econstr of ident * expr list
| Ematch of expr * (pat * expr) list
| Ebinop of expr * binop * expr
| Enot of expr
| Eblock of expr list
| Ewhile of expr * expr
| Efor of ident * ident * for_direction * ident * expr
| Efor of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
| Eraise of exn * expr option
| Etry of expr * (exn * ident option * expr) list
| Etry of expr * (exn * pvsymbol option * expr) list
| Eabsurd
type is_mutable = bool
type typedef =
| Dabstract
| Ddata of (ident * ty list) list
| Drecord of (is_mutable * ident * ty) list
| Dalias of ty
type its_defn = {
its_name : ident;
its_args : tvsymbol list;
its_private : bool;
its_def : typedef option;
}
type decl = (* TODO add support for the extraction of ocaml modules *)
| Dtype of (ident * ident list * typedef) list
| Dlet of is_rec * (ident * var list * expr) list
| Dtype of its_defn list
| Dlet of is_rec * (rsymbol * var list * expr) list
(* TODO add return type? *)
| Dexn of ident * ty option
| Dexn of xsymbol * ty option
let mk_expr e_node e_ity e_effect =
{ e_node = e_node; e_ity = e_ity; e_effect = e_effect }
......@@ -155,6 +165,11 @@ module ML = struct
let mk_unit =
mk_expr enope (I Ity.ity_unit) Ity.eff_empty
let mk_var id ty ghost = (id, ty, ghost)
let mk_its_defn id args private_ def =
{ its_name = id; its_args = args; its_private = private_; its_def = def; }
end
(** Translation from Mlw to ML *)
......@@ -170,7 +185,7 @@ module Translate = struct
let rec type_ ty =
match ty.ty_node with
| Tyvar tvs ->
ML.Tvar tvs.tv_name
ML.Tvar tvs
| Tyapp (ts, tyl) when is_ts_tuple ts ->
ML.Ttuple (List.map type_ tyl)
| Tyapp (ts, tyl) ->
......@@ -202,8 +217,8 @@ module Translate = struct
(* individual types *)
let rec ity t =
match t.ity_node with
| Ityvar ({tv_name = tv}, _) ->
ML.Tvar tv
| Ityvar (tvs, _) ->
ML.Tvar tvs
| Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
ML.Ttuple (List.map ity itl)
| Ityapp ({its_ts = ts}, itl, _) ->
......@@ -213,8 +228,11 @@ module Translate = struct
let pv_name pv = pv.pv_vs.vs_name
let pvty pv =
if pv.pv_ghost then (pv_name pv, ML.tunit)
else vsty pv.pv_vs
if pv.pv_ghost then
ML.mk_var (pv_name pv) ML.tunit true
else
let (vs, vs_ty) = vsty pv.pv_vs in
ML.mk_var vs vs_ty false
let for_direction = function
| To -> ML.To
......@@ -232,15 +250,12 @@ 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 ->
let pv_id = pv_name pvs in
ML.mk_expr (ML.Eident pv_id) (ML.I e.e_ity) eff
ML.mk_expr (ML.Evar pvs) (ML.I e.e_ity) eff
| Elet (LDvar (pvs, e1), e2) ->
let ml_let = ML.ml_let (pv_name pvs) (expr info e1) (expr info e2) in
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, pvl)}, _) ->
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
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
| Ecase (e1, pl) ->
......@@ -264,30 +279,35 @@ module Translate = struct
let its_args ts = ts.its_ts.ts_args
let itd_name td = td.itd_its.its_ts.ts_name
let drecord_fields {itd_its = its; itd_fields = fl} =
List.map (fun ({rs_cty = rsc} as rs) ->
(List.exists (pv_equal (Opt.get rs.rs_field)) its.its_mfields),
rs.rs_name,
if rs_ghost rs then ML.tunit else ity rsc.cty_result) fl
let ddata_constructs = (* point-free *)
List.map (fun ({rs_cty = rsc} as rs) ->
rs.rs_name, List.map (fun {pv_vs = pv} -> type_ pv.vs_ty) rsc.cty_args)
(* type declarations/definitions *)
let tdef itd =
let s = itd.itd_its in
let id = itd_name itd in
let args = its_args s in
let ddata_constructs = (* point-free *)
List.map (fun ({rs_cty = rsc} as rs) ->
rs.rs_name,
let args = List.filter (fun x -> not x.pv_ghost) rsc.cty_args in
List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
in
let drecord_fields = (* point-free *)
List.map (fun ({rs_cty = rsc} as rs) ->
(List.exists (pv_equal (Opt.get rs.rs_field)) s.its_mfields),
rs.rs_name,
if rs_ghost rs then ML.tunit else ity rsc.cty_result)
in
let id = s.its_ts.ts_name in
let is_private = s.its_private in
let args = s.its_ts.ts_args in
begin match s.its_def, itd.itd_constructors, itd.itd_fields with
| None, [], [] ->
ML.Dtype [id, type_args args, ML.Dabstract]
ML.mk_its_defn id args is_private None
| None, cl, [] ->
ML.Dtype [id, type_args args, ML.Ddata (ddata_constructs cl)]
| None, _, _ ->
ML.Dtype [id, type_args args, ML.Drecord (drecord_fields itd)]
let cl = ddata_constructs cl in
ML.mk_its_defn id args is_private (Some (ML.Ddata cl))
| None, _, pjl ->
let pjl = drecord_fields pjl in
ML.mk_its_defn id args is_private (Some (ML.Drecord pjl))
| Some t, _, _ ->
ML.Dtype [id, type_args args, ML.Dalias (ity t)]
ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t)))
end
(* program declarations *)
......@@ -295,32 +315,29 @@ module Translate = struct
match pd.pd_node with
| PDlet (LDvar (_, _)) ->
[]
| PDlet (LDsym ({rs_name = rsn; rs_cty = cty}, {c_node = Cfun e})) ->
[ML.Dlet (false, [rsn, args cty.cty_args, expr info e])]
| 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 _})) ->
Format.printf "LDsym Capp--> %s@." rsn.id_string;
[]
| PDlet (LDsym ({rs_name = rsn}, {c_node = Cpur _})) ->
Format.printf "LDsym Cpur--> %s@." rsn.id_string;
[]
| PDlet (LDsym ({rs_name = rsn}, {c_node = Cany})) ->
Format.printf "LDsym Cany--> %s@." rsn.id_string;
[]
| 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.rs_name, args rs.rs_cty.cty_args, expr info e) rl in
rs, args rs.rs_cty.cty_args, expr info e) rl in
[ML.Dlet (true, rec_def)]
| PDpure ->
[]
| PDtype itl ->
List.map tdef itl
| PDexn ({xs_name = xsn} as xs) ->
[ML.Dtype (List.map tdef itl)]
| PDexn xs ->
if ity_equal xs.xs_ity ity_unit then
[ML.Dexn (xsn, None)]
[ML.Dexn (xs, None)]
else
[ML.Dexn (xsn, Some (ity xs.xs_ity))]
[ML.Dexn (xs, Some (ity xs.xs_ity))]
(* unit module declarations *)
let mdecl info = function
......
src/mlw/exec.ml deleted 100644 → 0
View file @ d8ecd3b8
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(* Decide wheter an expression/symbol/declaration is executable *)
(* Based on the implementation by Jacques-Pascal Deplaix (2014), *)
(* for the old system *)
open Ident
open Pdecl
open Ity
open Expr
open Term
open Pdriver
type t = {
driver : Pdriver.driver;
th_known_map : Decl.known_map;
mo_known_map : Pdecl.known_map;
is_exec_id : bool Hid.t;
}
let create dr thkm mokm =
{ driver = dr;
th_known_map = thkm;
mo_known_map = mokm;
is_exec_id = Hid.create 16; }
let has_syntax {driver = drv} id =
Mid.mem id (drv.drv_syntax) || Mid.mem id (drv.drv_converter)
let is_exec_pdecl _ _ = assert false (* TODO *)
(*
let rec is_exec_expr cxt e =
match e.e_node with
| Evar _
| Econst _
| Eassert _
| Eabsurd -> true
| Econst of Number.constant
| Eexec of cexp * cty
| Eassign of assign list
| Elet of let_defn * expr
| Eif of expr * expr * expr
| Ecase of expr * (prog_pattern * expr) list
| Ewhile of expr * invariant list * variant list * expr
| Efor of pvsymbol * for_bounds * invariant list * expr
| Etry of expr * (pvsymbol list * expr) Mexn.t
| Eraise of xsymbol * expr
| Eassert of assertion_kind * term
| Eghost of expr
| Epure of term
| Eabsurd
let is_exec_pdecl cxt pd =
match pd.pd_node with
| PDtype _ | PDexn _ -> true
| PDpure -> false
| PDlet (LDvar (pv, _)) when pv.pv_ghost -> false
| PDlet (LDsym (_, c)) when cty_ghost c.c_cty -> false
| PDlet (LDvar ({pv_vs = vs}, _)) ->
has_syntax cxt vs.vs_name
| PDlet (LDsym ({rs_name = rs}, {c_node = Cfun e})) ->
is_exec_expr cxt e
| _ -> assert false
*)
src/mlw/ocaml_printer.ml
View file @ a469b306
......@@ -20,6 +20,8 @@ open Pp
open Ity
open Term
open Printer
open Expr
open Ty
type info = {
info_syn : syntax_map;
......@@ -60,7 +62,7 @@ module Print = struct
(* let print_uident = print_qident ~sanitizer:Strings.capitalize *)
let print_tv fmt tv =
fprintf fmt "'%s" (id_unique aprinter tv)
fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
let protect_on b s =
if b then "(" ^^ s ^^ ")" else s
......@@ -70,8 +72,8 @@ module Print = struct
(** Types *)
let rec print_ty ?(paren=false) fmt = function
| Tvar id ->
print_tv fmt id
| Tvar tv ->
print_tv fmt tv
| Ttuple [] ->
fprintf fmt "unit"
| Ttuple tl ->
......@@ -87,7 +89,7 @@ module Print = struct
(print_list comma (print_ty ~paren:false)) tl
print_ident ts
let print_vsty fmt (v, ty) =
let print_vsty fmt (v, ty, _) =
fprintf fmt "%a:@ %a" print_ident v (print_ty ~paren:false) ty
let print_tv_arg = print_tv
......@@ -149,45 +151,40 @@ module Print = struct
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 print_apply info fmt rs pvl =
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
match rs.rs_field with
| None -> false
| Some _ -> true
in
match extract_op s, vl with
match extract_op rs.rs_name, pvl with
| Some o, [t1; t2] ->
fprintf fmt "@[<hov 1>%a %s %a@]"
print_ident t1 o print_ident t2
print_pv t1 o print_pv t2
| _, [] ->
print_ident fmt s
print_ident fmt rs.rs_name
| _, [t1] when isfield ->
fprintf fmt "%a.%a" print_ident t1 print_ident s
fprintf fmt "%a.%a" print_pv t1 print_ident rs.rs_name
| _, tl ->
fprintf fmt "@[<hov 2>%a %a@]"
print_ident s (print_list space print_ident) tl
print_ident rs.rs_name (print_list space print_pv) tl
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) ->
| Evar pvs ->
print_ident fmt (pv_name pvs)
| Elet (pv, e1, e2) ->
fprintf fmt "@[<hov 2>let @[%a@] =@ @[%a@]@] in@ %a"
print_ident id (print_expr info) e1 (print_expr info) e2
print_ident (pv_name pv) (print_expr info) e1 (print_expr info) e2
| Eabsurd ->
fprintf fmt "assert false (* absurd *)"
| Eapp (s, vl) ->
print_apply info fmt s vl
| Eapp (s, []) when rs_equal s rs_true ->
fprintf fmt "true"
| Eapp (s, []) when rs_equal s rs_false ->
fprintf fmt "false"
| 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
......@@ -201,7 +198,7 @@ module Print = struct
and print_expr info fmt e =
print_enode info fmt e.e_node
let print_type_decl fmt (id, args, tydef) =
let print_type_decl fmt its =
let print_constr fmt (id, cs_args) =
match cs_args with
| [] ->
......@@ -216,40 +213,42 @@ module Print = struct
fprintf fmt "%s%a: %a;"
(if is_mutable then "mutable " else "")
print_ident id
(print_ty ~paren:false) ty
in
(print_ty ~paren:false) ty in
let print_def fmt = function
| Dabstract ->
()
| Ddata csl ->
fprintf fmt " =@\n%a" (print_list newline print_constr) csl
| Drecord fl ->
fprintf fmt " = {@\n%a@\n}" (print_list newline print_field) fl
| Dalias ty ->
fprintf fmt " =@ %a" (print_ty ~paren:false) ty in
| None ->
()
| Some (Ddata csl) ->
fprintf fmt " =@\n%a" (print_list newline print_constr) csl
| Some (Drecord fl) ->
fprintf fmt " = %s{@\n%a@\n}"
(if its.its_private then "private " else "")
(print_list newline print_field) fl
| Some (Dalias ty) ->
fprintf fmt " =@ %a" (print_ty ~paren:false) ty
in
fprintf fmt "@[<hov 2>%s %a%a%a@]"
(if true then "type" else "and") (* FIXME: mutual recursive types *)
print_tv_args args
print_ident id (* FIXME: first letter must be lowercase
(if true then "type" else "and") (* FIXME: mutual recursive types *)
print_tv_args its.its_args
print_ident its.its_name (* FIXME: first letter must be lowercase
-> print_lident *)
print_def tydef
print_def its.its_def
let print_decl info fmt = function
| Dlet (isrec, [id, vl, e]) ->
| Dlet (isrec, [rs, pvl, 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_ident rs.rs_name
(print_list space print_vs_arg) pvl
(print_expr info) e;
fprintf fmt "@\n@\n"
| Dtype dl ->
print_list newline print_type_decl fmt dl;
fprintf fmt "@\n@\n"
| Dexn (id, None) ->
fprintf fmt "exception %a@\n@\n" print_ident id
| Dexn (id, Some t) ->
| Dexn (xs, None) ->
fprintf fmt "exception %a@\n@\n" print_ident xs.xs_name
| Dexn (xs, Some t) ->
fprintf fmt "@[<hov 2>exception %a of %a@]@\n@\n"
print_ident id (print_ty ~paren:true) t
print_ident xs.xs_name (print_ty ~paren:true) t
| _ -> (* TODO *) assert false
end
......
tests/test_extraction_mario.mlw
View file @ a469b306
......@@ -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,38 +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
(* 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
(* use import int.Int *)
use import int.Int
(* let test (x: int) : int = *)
(* let y = *)
(* let z = x in *)
(* (ghost z) + 1 *)
(* in 42 *)
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