Commit a99f7b84 authored by Mário Pereira's avatar Mário Pereira

Code extraction: wip (added exec.ml)

parent d4bcbf86
......@@ -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 compile ocaml_printer
pinterp pdriver cprinter exec compile ocaml_printer
LIB_PARSER = ptree glob typing parser lexer
......
......@@ -224,7 +224,7 @@ module Translate = struct
(* expressions *)
let rec expr ({e_effect = eff } as e) =
assert (not eff.eff_ghost);
(* assert (not eff.eff_ghost); *)
match e.e_node with
| Econst c ->
let c = match c with Number.ConstInt c -> c | _ -> assert false in
......@@ -247,6 +247,11 @@ module Translate = struct
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
ML.mk_expr (ML.Eif (e1, e2, e3)) (ML.I e.e_ity) eff
| _ -> (* TODO *) assert false
and ebranch ({pp_pat = p}, e) =
......@@ -287,6 +292,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])]
| PDlet (LDsym ({rs_name = rsn}, {c_node = Capp _})) ->
Format.printf "LDsym Capp--> %s@." rsn.id_string;
......
(********************************************************************)
(* *)
(* 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 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
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