Commit e67bc044 authored by charguer's avatar charguer

compile_mlv

parent aaad917b
......@@ -43,6 +43,13 @@ let infix_aux x y = x + y
let (---) = infix_aux
(********************************************************************)
(* ** Inlined total functions *)
let f () =
1 - 1/(-1) + (2 / 2) mod 3
(********************************************************************)
(* ** Return *)
......
......@@ -10,6 +10,7 @@ open Formula
open Coq
open Primitives
open Path
open Renaming
open Printf
(*#########################################################################*)
......@@ -42,30 +43,15 @@ let external_modules_reset () =
external_modules := []
(*#########################################################################*)
(* ** Idenntifier name renaming conventions *)
(** Convention for naming record types *)
let record_type_name name =
name ^ "_record_"
(** Convention for naming record constructors *)
let record_constructor name =
name ^ "_record_of_"
(** Convention for naming module names*)
let module_name name =
name ^ "_ml"
(*#########################################################################*)
(* ** Lifting of paths *)
(* Take a module name and add "_ml" suffix to it;
Moreover, insert a "Require" directive in case the module
corresponds to a file (i.e. a compilation unit. *)
let lift_ident_name id =
let lift_module_name id =
let name = Ident.name id in
let coqname = module_name name in
if Ident.persistent id then external_modules_add coqname;
......@@ -78,11 +64,18 @@ let lift_ident_name id =
*)
(* -- old: if name = "OkaStream" then "CFPrim" else *)
(* Function for adding "_ml" to the modules in a path,
including the last constant which is assumed to a module name *)
(* TODO: rename this function *)
let rec lift_full_path = function
| Pident id -> Pident (Ident.create (lift_ident_name id))
| Pident id -> Pident (Ident.create (lift_module_name id))
| Pdot(p, s, pos) -> Pdot(lift_full_path p, (module_name s), pos)
| Papply(p1, p2) -> assert false
(* Function for adding "_ml" to the modules in a path,
but not changing the last constant in the path *)
let lift_path = function
| Pident id -> Pident id
| Pdot(p, s, pos) -> Pdot(lift_full_path p, s, pos)
......@@ -307,11 +300,13 @@ let pattern_aliases p : (typed_var*coq) list =
(* ** Helper functions for primitive functions *)
let register_cf x =
Coqtop_register ("database_cf", x, x ^ "_cf")
Coqtop_register ("database_cf", x, cf_axiom_name x)
let register_spec x v =
Coqtop_register ("database_spec", x, v)
(* TODO: rewrite this function by using a normalization functiont that returns p *)
let rec prefix_for_label typ =
match typ.desc with
| Tconstr (p, _, _) -> lift_path_name p
......@@ -331,20 +326,13 @@ let rec prefix_for_label typ =
| Tpoly _ -> failwith "x12"
*)
(* DEPRECATED
let string_of_label_with prefix lbl =
prefix ^ "_" ^ lbl.lbl_name
let name_for_record_new prefix =
"_new" ^ prefix
let name_for_record_get lbl =
"_get_" ^ lbl.lbl_name
let name_for_record_set lbl =
"_set_" ^ lbl.lbl_name
let string_of_label typ lbl =
string_of_label_with (prefix_for_label typ) lbl
*)
let simplify_apply_args oargs =
List.map (function (lab, Some e, Required) -> e | _ -> unsupported "optional arguments") oargs
......@@ -371,47 +359,6 @@ let exp_get_inlined_primitive e oargs =
| _ -> failwith "get_inlined_primitive: not an inlined primitive"
(*#########################################################################*)
(* ** Protection of infix function names *)
(** Auxiliary function for encoding infix function names *)
let infix_name_symbols =
['!', 'a';
'$', 'b';
'%', 'c';
'&', 'd';
'*', 'e';
'+', 'f';
'-', 'g';
'.', 'h';
'/', 'i';
':', 'j';
'<', 'k';
'=', 'l';
'>', 'm';
'?', 'n';
'@', 'o';
'^', 'p';
'|', 'q';
'~', 'r']
let infix_name_encode name =
let gen = String.map (fun c ->
try List.assoc c infix_name_symbols
with Not_found -> failwith ("infix_name_encode: cannot encode name: " ^ name))
name in
"infix_" ^ gen ^ "_"
let protect_infix name =
let n = String.length name in
let r = if n > 0 && List.mem_assoc name.[0] infix_name_symbols
then infix_name_encode name
else name in
r
(* debug: Printf.printf "protect %s as %s\n" name r;*)
(*#########################################################################*)
(* ** Lifting of values *)
......@@ -454,7 +401,7 @@ let rec lift_val env e =
let register_arg lbl v =
Array.iteri (fun i lbli -> if lbl.lbl_name = lbli.lbl_name then args.(i) <- v) labels in
List.iter (fun (p,lbl,v) -> register_arg lbl (aux v)) l;
let constr = record_constructor (prefix_for_label (e.exp_type)) in
let constr = record_constructor_name_from_type (prefix_for_label (e.exp_type)) in
let typ_args =
match btyp_of_typ_exp e.exp_type with
| Btyp_constr (id,ts) -> List.map lift_btyp ts
......@@ -511,6 +458,8 @@ let rec lift_val env e =
(*#########################################################################*)
(* ** Helper functions for producing label names *)
(* FOR FUTURE USE *)
let counter_local_label =
ref 0
let get_next_local_label () =
......@@ -597,7 +546,7 @@ let rec cfg_exp env e =
| Texp_record (lbl_expr_list, opt_init_expr) ->
if opt_init_expr <> None then unsupported "record-with"; (* TODO *)
let (pathfront,pathend) = get_record_decomposed_name_for_exp e in
let func = Coq_var (pathfront ^ (name_for_record_new ("_" ^ pathend))) in (* tood: move the underscore *)
let func = Coq_var (pathfront ^ (record_make_name pathend)) in (* tood: move the underscore *)
let named_args = List.map (fun (p,li,ei) -> (li.lbl_name,ei)) lbl_expr_list in
(* deprecated sorting: let args = List.map snd (list_ksort str_cmp named_args) in *)
let fields_names = extract_label_names_simple e.exp_env e.exp_type in
......@@ -740,13 +689,13 @@ let rec cfg_exp env e =
| Texp_field (arg, p, lbl) ->
let tr = coq_typ e in
let ts = coq_typ arg in (* todo: check it is always 'loc' *)
let func = Coq_var (name_for_record_get lbl) in
let func = Coq_var (record_field_get_name lbl.lbl_name) in
Cf_app ([ts], tr, func, [lift arg])
| Texp_setfield(arg, p, lbl, newval) ->
let ts1 = coq_typ arg in (* todo: check it is always 'loc' *)
let ts2 = coq_typ newval in
let func = Coq_var (name_for_record_set lbl) in
let func = Coq_var (record_field_set_name lbl.lbl_name) in
Cf_app ([ts1;ts2], coq_unit, func, [lift arg; lift newval])
| Texp_try(body, pat_expr_list) -> unsupported "try expression"
......@@ -926,7 +875,7 @@ let rec cfg_structure_item s : cftops =
a type abbreviation. *)
and cfg_type_abbrev (name,dec) =
let x = Ident.name name in
let x = type_constr_name (Ident.name name) in
let args = List.map name_of_type dec.typ_type.type_params in
let sort = coq_impl_types (List.length args) in
let coqs = match dec.typ_type.type_manifest with
......@@ -941,8 +890,7 @@ and cfg_type_abbrev (name,dec) =
and cfg_type_record (name,dec) =
let x = Ident.name name in
let name_of_field lbl =
"_" ^ lbl in (* "_" ^ x ^ *)
let record_name = record_type_name x in
record_field_name lbl in
let fields = match dec.typ_type.type_kind with Type_record (l,_) -> l | _ -> assert false in
(* let fields_base_names = List.map (fun (lbl,_,_) -> lbl) fields in *)
let declared_params = List.map name_of_type dec.typ_type.type_params in
......@@ -958,7 +906,8 @@ and cfg_type_record (name,dec) =
(* TODO: enlever le polymorphisme inutile : list_intersect remaining_params declared_params *)
let params = declared_params in
let top = {
coqind_name = record_name;
coqind_name = record_structure_name x;
coqind_constructor_name = record_constructor_name x;
coqind_targs = coq_types params;
coqind_ret = Coq_type;
coqind_branches = branches } in
......@@ -967,12 +916,12 @@ and cfg_type_record (name,dec) =
| [] -> []
| _ -> List.map (fun field -> Coqtop_implicit (field, List.map (fun p -> p, Coqi_maximal) params)) fields_names
in
let type_abbrev = Coqtop_def ((x,Coq_wild), coq_fun_types params loc_type) in
let type_abbrev = Coqtop_def ((type_constr_name x, Coq_wild), coq_fun_types params loc_type) in
[ type_abbrev ],
[ Coqtop_record top ]
@ (implicit_decl)
@ [ Coqtop_hint_constructors ([record_name], "typeclass_instances") ]
@ record_functions record_name (record_name ^ "_of") (str_capitalize_1 x) params fields_names fields_types
@ [ Coqtop_hint_constructors ([record_structure_name x], "typeclass_instances") ]
@ record_functions x (record_constructor_name x) (record_repr_name x) params fields_names fields_types
(* todo: move le "_of" *)
(** Auxiliary function to generate stuff for records *)
......@@ -983,9 +932,9 @@ and record_functions record_name record_constr repr_name params fields_names fie
let indices = list_nat n in
let for_indices f = List.map f indices in
let new_name = name_for_record_new record_name in
let get_names = for_indices (fun i -> "_get" ^ nth i fields_names) in
let set_names = for_indices (fun i -> "_set" ^ nth i fields_names) in
let new_name = record_make_name record_name in
let get_names = for_indices (fun i -> record_field_get_name (nth i fields_names)) in
let set_names = for_indices (fun i -> record_field_set_name (nth i fields_names)) in
let new_decl = Coqtop_param (new_name, val_type) in
let get_set_decl i =
[ Coqtop_param (nth i get_names, val_type);
......@@ -1156,8 +1105,8 @@ and record_functions record_name record_constr repr_name params fields_names fie
[ new_decl ]
@ (List.concat (List.map get_set_decl indices))
@ [ repr_def ]
(* TODO: revive
@ [ repr_def ]
@ repr_convert_focus_unfocus
@ fields_convert_focus_unfocus
@ new_spec
......@@ -1184,11 +1133,13 @@ and cfg_algebraic decls =
let coqind_decl =
if List.length decls = 1 then
{ coqind_name = x;
coqind_constructor_name = record_constructor_name x;
coqind_targs = coq_types params;
coqind_ret = Coq_type;
coqind_branches = List.map get_typed_constructor branches; }
else
{ coqind_name = x;
coqind_constructor_name = record_constructor_name x;
coqind_targs = [];
coqind_ret = coq_impl_types (List.length params);
coqind_branches = List.map
......@@ -1242,14 +1193,14 @@ and cfg_structure s =
a Caml signature definition. *)
and cfg_modtype id mt =
let id = lift_ident_name id in
let id = lift_module_name id in
let rec aux (bindings:mod_bindings) mt =
match mt.mty_desc with
| Tmty_ident p -> Coqtop_module_type (id, bindings, Mod_def_inline [lift_full_path_name p]), None
| Tmty_signature s -> Coqtop_module_type (id, bindings, Mod_def_declare), Some (cfg_signature s)
| Tmty_functor (x,mtx,mtr) ->
begin match mtx.mty_desc with
| Tmty_ident p -> aux (bindings @ [([lift_ident_name x], Mod_typ_var (lift_full_path_name p))]) mtr (* TODO: use List.rev *)
| Tmty_ident p -> aux (bindings @ [([lift_module_name x], Mod_typ_var (lift_full_path_name p))]) mtr (* TODO: use List.rev *)
| _ -> unsupported "functor with on-the-fly signature for its argument"
end
| Tmty_with _ -> unsupported "module sig with"
......@@ -1294,7 +1245,7 @@ and cfg_signature_item s =
*)
| Tsig_module (id,mt) ->
let x = lift_ident_name id in
let x = lift_module_name id in
let mt' =
match mt.mty_desc with
| Tmty_ident p -> Mod_typ_var (lift_full_path_name p)
......@@ -1349,7 +1300,7 @@ and cfg_signature s =
a Caml module. *)
and cfg_module id m =
let id = lift_ident_name id in
let id = lift_module_name id in
let rec aux bindings cast m =
let return def =
Coqtop_module (id, bindings, cast, def) in
......@@ -1357,12 +1308,12 @@ and cfg_module id m =
| Tmod_ident p -> return (Mod_def_inline [lift_full_path_name p]), None
| Tmod_structure str -> return Mod_def_declare, Some (cfg_structure str)
| Tmod_functor (x, mt, m1) ->
let x = lift_ident_name x in
let x = lift_module_name x in
if cast <> Mod_cast_free then unsupported "cast before arguments in module declaration";
begin match mt.mty_desc with
| Tmty_ident p -> aux (([x], Mod_typ_var (lift_full_path_name p))::bindings) cast m1
| _ ->
(* hack for Dijkstra Printf.printf "-->%s %s\n" (lift_ident_name x) id; Pident (Ident.create ("PqueueSig") *)
(* hack for Dijkstra Printf.printf "-->%s %s\n" (lift_module_name x) id; Pident (Ident.create ("PqueueSig") *)
if id = "MLDijkstra" && x = "MLPqueue"
then
aux (([x], Mod_typ_with_mod (Mod_typ_var "MLPqueueSig", "MLElement", "MLNextNode"))::bindings) cast m1
......@@ -1421,13 +1372,13 @@ let cfg_file str =
Coqtop_require ["LibLogic"; "LibRelation"; "LibInt"; "Shared"; "CFHeaps"; "CFApp" ];
Coqtop_require_import ["CFHeader"];
Coqtop_custom "Open Scope list_scope.";
Coqtop_custom "Local Notation \"'int'\" := (Coq.ZArith.BinInt.Z). Delimit Scope Z_scope with Z."
Coqtop_custom "Local Notation \"'int'\" := (Coq.ZArith.BinInt.Z).";
Coqtop_custom "Delimit Scope Z_scope with Z."
]
@ (external_modules_get_coqtop())) ]
@ cfg_structure str
(*deprecated: (if !pure_mode then "FuncPrim" else "CFHeader") *)
......
......@@ -66,7 +66,8 @@ type coqtop =
| Coqtop_module_type of var * mod_bindings * mod_def
| Coqtop_module_type_include of var
| Coqtop_end of var
| Coqtop_custom of string
and coqtops = coqtop list
(** Modules and signatures *)
......@@ -96,6 +97,7 @@ and mod_bindings = mod_binding list
and coqind = {
coqind_name : var;
coqind_constructor_name : var;
coqind_targs : typed_vars;
coqind_ret : coq;
coqind_branches : typed_vars; }
......
......@@ -39,12 +39,13 @@ and cftops = cftop list
(*#########################################################################*)
(* ** Shared functions *)
(** Abstract datatype for dynamic values *)
let coq_dyn_at = coq_var_at "CFHeaps.dyn"
let coq_dyn_at = coq_var_at "CFHeaps.dyn"
(** Abstract datatype for functions *)
......@@ -161,301 +162,3 @@ let heap_existss x_names_types h =
let heap_pred c =
Coq_app (Coq_var "CFHeaps.heap_is_empty_st", c)
(*#########################################################################*)
(* ** Conversion of IMPERATIVE characteristic formulae to Coq *)
let rec coqtops_of_imp_cf cf =
let coq_of_cf = coqtops_of_imp_cf in
let h = Coq_var "H" in
let q = Coq_var "Q" in
let funhq tag ?label ?rettype c =
let typ = match rettype with
| None -> Coq_wild
| Some t -> t
in
let f_core = coq_funs [("H", hprop);("Q", Coq_impl(typ,hprop))] c in
let f = Coq_app (Coq_var "CFHeaps.local", f_core) in
match label with
| None -> coq_tag tag f
| Some x -> (*todo:remove this hack*) if x = "_c" then coq_tag tag f else
coq_tag tag ~label:x f
in
match cf with
| Cf_ret v ->
funhq "tag_ret" (heap_impl h (Coq_app (q,v)))
(* (!R: fun H Q => H ==> Q v *)
| Cf_assert cf1 ->
let p = coq_eq (Coq_var "_b") coq_true in
let q' = Coq_fun (("_b",coq_bool), heap_star (heap_pred p) h) in
let c1 = coq_apps (coq_of_cf cf1) [h;q'] in
let c2 = heap_impl h (Coq_app (q,coq_tt)) in
funhq "tag_assert" (coq_conj c1 c2)
(* (!Assert (fun H Q => F1 H (fun (b:bool) => \[b = true] \* H) /\ H ==> Q tt)) *)
| Cf_fail ->
funhq "tag_fail" coq_false
| Cf_done ->
funhq "tag_done" coq_true
| Cf_app (ts, tret, f, vs) -> (* TODO: maybe make the return type explicit? *)
(* old: let arity = List.length vs in *)
assert (List.length ts = List.length vs);
let tvs = List.combine ts vs in
let args = List.map (fun (t,v) -> coq_apps coq_dyn_at [t;v]) tvs in
coq_tag "tag_apply" (coq_apps (coq_var_at "app_def") [f; coq_list args; tret])
(* (!Apply: (app_def f [(@dyn t1 v1) (@dyn t2 v2)])) *)
(* DEPRECATED
| Cf_body (f, fvs, targs, typ, cf) ->
let type_of_k = coq_impls ((List.map snd targs) @ [formula_type_of typ]) Coq_prop in
let args = List.map fst targs in
let args_of_k = (List.map coq_var args) @ [ coq_of_cf cf ] in
let var_k = Coq_var "K" in
let sarity = string_of_int (List.length targs) in
let spec_n = Coq_var ("spec_" ^ sarity) in
let is_spec_k = Coq_app (Coq_var ("is_spec_" ^ sarity), var_k) in
let hyp_k = coq_foralls targs (coq_apps var_k args_of_k) in
let concl_k = coq_apps spec_n [var_k; coq_var f] in
coq_tag "tag_body" (coq_forall_types fvs (coq_foralls ["K", type_of_k] (coq_impls [is_spec_k;hyp_k] concl_k)))
(* (!B: (forall Ai K, is_spec_2 K ->
(forall x1 x2, K x1 x2 F) -> spec_2 K f)) *)
*)
| Cf_body (f, fvs, targs, typ, cf1) ->
let narity = Coq_nat (List.length targs) in
let h_curried = coq_apps (Coq_var "curried") [narity; coq_var f] in
let h_body_hyp = coq_apps (coq_of_cf cf1) [h; q] in
let args = List.map (fun (x,t) -> coq_apps coq_dyn_at [t; coq_var x]) targs in
let h_body_conc = coq_apps (Coq_var "app_def") [coq_var f; coq_list args; h; q] in
let h_body_2 = Coq_impl (h_body_hyp, h_body_conc) in
let h_body_1 = coq_foralls [("H", hprop); ("Q", Coq_impl (typ, hprop))] h_body_2 in
let h_body = coq_forall_types fvs (coq_foralls targs h_body_1) in
coq_tag "tag_body" (coq_conj h_curried h_body)
(* (!B: curried 2 f /\
(forall Ai x1 x2 H Q, CF H Q -> app f [(dyn t1 x1) (dyn t2 x2)] H Q) *)
| Cf_let ((x,typ), cf1, cf2) ->
let q1 = Coq_var "Q1" in
let type_of_q1 = Coq_impl (typ, hprop) in
let c1 = coq_apps (coq_of_cf cf1) [h; q1] in
let c2 = coq_foralls [x,typ] (coq_apps (coq_of_cf cf2) [(Coq_app (q1, Coq_var x)); q]) in
funhq "tag_let_trm" ~label:x (coq_exist "Q1" type_of_q1 (coq_conj c1 c2))
(* !L: fun H Q => exists Q1, F1 H Q1 /\ forall (x:T), F2 (Q1 x) Q *)
| Cf_letval (x, fvs_strict, fvs_other, typ, v, cf) ->
let type_of_x = coq_forall_types fvs_strict typ in
let equ = coq_eq (Coq_var x) (coq_fun_types fvs_strict v) in
let conc = coq_apps (coq_of_cf cf) [h;q] in
funhq "tag_let_val" (*~label:x*) (Coq_forall ((x, type_of_x), Coq_impl (equ, conc)))
(*(!!L x: (fun H Q => forall (x:forall Ai,T), x = (fun Ai => v) -> F H Q)) *)
| Cf_letfunc (ncs, cf) ->
let ns, cs = List.split ncs in
let p_of n = "P" ^ n in
let fs = List.map (fun n -> (n, val_type)) ns in
let ps = List.map (fun n -> (p_of n, coq_pred val_type)) ns in
let c1hyps = List.map coq_of_cf cs in
let c1conc = coq_conjs (List.map (fun n -> Coq_app (Coq_var (p_of n), Coq_var n)) ns) in
let c1 = coq_impls c1hyps c1conc in
let c2hyps = List.map (fun n -> Coq_app (Coq_var (p_of n), Coq_var n)) ns in
let c2conc = coq_apps (coq_of_cf cf) [h;q] in
let c2 = coq_impls c2hyps c2conc in
let x = List.hd ns in
funhq "tag_let_fun" ~label:x (coq_foralls fs (coq_exists ps (coq_conj c1 c2)))
(* (!F a: fun H Q => forall f1 f2, exists P1 P2,
(B1 -> B2 -> P1 f1 /\ P2 f2) /\ (P1 f1 -> P2 f2 -> F H Q)) *)
(* old
| Cf_caseif (cf0,cf1,cf2) ->
let q' = Coq_var "Q'" in
let c0 = coq_apps (coq_of_cf cf0) [h;q'] in
let c1 = coq_apps (coq_of_cf cf1) [ Coq_app (q',coq_bool_true); q] in
let c2 = coq_apps (coq_of_cf cf2) [ Coq_app (q',coq_bool_false); q] in
funhq "tag_if" (coq_exist "Q'" (Coq_impl (coq_bool,hprop)) (coq_conjs [c0;c1;c2]))
(* (!I a: (fun H Q => exists Q', Q0 H Q' /\ Q1 (Q' true) Q /\ Q2 (Q' false) Q)) *)
*)
| Cf_caseif (v,cf1,cf2) ->
let c1 = Coq_impl (coq_eq v (Coq_var "true"), coq_apps (coq_of_cf cf1) [h;q]) in
let c2 = Coq_impl (coq_eq v (Coq_var "false"), coq_apps (coq_of_cf cf2) [h;q]) in
funhq "tag_if" (coq_conj c1 c2)
(* (!I a: (fun H Q => (x = true -> Q1 H Q) /\ (x = false -> Q2 H Q))) *)
| Cf_case (v,tps,pat,vwhenopt,aliases,cf1,cf2) ->
let add_alias ((name,typ),exp) cf : coq =
funhq "tag_alias" (coq_foralls [name,typ] (coq_impls [coq_eq (Coq_var name) exp] (coq_apps cf [h;q])))
(* !L a: (fun H Q => forall y, y = v -> F H Q) *)
in
let cf1_aliased = List.fold_right add_alias aliases (coq_of_cf cf1) in
let same = coq_eq v pat in
let same_when = match vwhenopt with None -> [same] | Some w -> [same; w] in
let c1 = coq_foralls tps (coq_impls same_when (coq_apps (cf1_aliased) [h;q])) in
let diff = coq_neq v pat in
let diff_when = match vwhenopt with None -> diff | Some w -> coq_disj diff (coq_neg w) in
let c2 = Coq_impl (coq_foralls tps diff_when, coq_apps (coq_of_cf cf2) [h;q]) in
let tag = match vwhenopt with None -> "tag_case" | Some w -> "tag_casewhen" in
funhq tag (coq_conj c1 c2)
(* (!C a: (fun H Q => (forall x1, x = p [-> trueb w] -> (!L a: y := v in F1) H Q)
/\ ((forall x1, x <> p [\/ trueb !w]) -> F2 H Q)))
where trueb are implicit by coercions *)
| Cf_match (label, n,cf1) ->
coq_tag (Printf.sprintf "(tag_match %d%snat)" n "%") (*~label:label*) (coq_of_cf cf1)
| Cf_seq (cf1,cf2) ->
let q' = Coq_var "Q'" in
let c1 = coq_apps (coq_of_cf cf1) [h;q'] in
let c2 = coq_apps (coq_of_cf cf2) [Coq_app (q', coq_tt); Coq_var "Q"] in
funhq "tag_seq" (coq_exist "Q'" wild_to_hprop (coq_conj c1 c2))
(* (!S: fun H Q => exists Q', F1 H Q /\ F2 (Q' tt) Q *)
| Cf_for (i_name,v1,v2,cf) ->
let s = Coq_var "S" in
let i = Coq_var i_name in
let typs = Coq_impl (coq_int,formula_type) in
let q' = Coq_var "Q'" in
let c1 = coq_apps (coq_of_cf cf) [h;q'] in
let c2 = coq_apps s [ coq_plus i (Coq_var "1"); Coq_app (q', coq_tt); q] in
let body_le = funhq "tag_seq" ~rettype:coq_unit (coq_exist "Q'" wild_to_hprop (coq_conj c1 c2)) in
let ple = Coq_impl (coq_le i v2, coq_apps body_le [h; q]) in
let body_gt = funhq "tag_ret" ~rettype:coq_unit (heap_impl_unit h q) in
let pgt = Coq_impl (coq_gt i v2, coq_apps body_gt [h; q]) in
let locals = Coq_app (Coq_var "CFHeaps.is_local_1", s) in
let bodys = coq_conj ple pgt in
let hypr = coq_foralls [(i_name, coq_int); ("H", hprop); ("Q", Coq_impl (coq_unit, hprop))] (Coq_impl (bodys,(coq_apps s [i;h;q]))) in
funhq "tag_for" (Coq_forall (("S",typs), coq_impls [locals; hypr] (coq_apps s [v1;h;q])))
(* (!For (fun H Q => forall S:int->~~unit, is_local_1 S ->
(forall i H Q,
((i <= v2 -> !Seq (fun H Q => exists Q', Q1 H Q' /\ S (i+1) (Q' tt) Q) H Q))
/\ (i > v2 -> !Ret: (fun H Q => H ==> Q tt) H Q) ))
-> S i H Q)
-> S v1 H Q) *)
(*--todo:optimize using rec calls *)
| Cf_while (cf1,cf2) ->
let r = Coq_var "R" in
let typr = formula_type in
let cfseq = Cf_seq (cf2, Cf_manual r) in
let cfret = Cf_ret coq_tt in
let cfif = Cf_caseif (Coq_var "_c", cfseq, cfret) in
let bodyr = coq_of_cf (Cf_let (("_c",coq_bool), cf1, cfif)) in
let hypr = coq_foralls [("H", hprop); ("Q", Coq_impl (coq_unit, hprop))] (Coq_impl (coq_apps bodyr [h;q],(coq_apps r [h;q]))) in
let localr = Coq_app (Coq_var "CFHeaps.is_local", r) in
funhq "tag_while" (Coq_forall (("R",typr), coq_impls [localr; hypr] (coq_apps r [h;q])))
(* (!While: (fun H Q => forall R:~~unit, is_local R ->
(forall H Q,
(Let _c = F1 in If _c Then (F2 ; R) Ret tt) H Q
-> R H Q)
-> R H Q). *)
| Cf_pay (cf1) ->
let h' = Coq_var "H'" in
let c1 = coq_apps (Coq_var "pay_one") [h;h'] in
let c2 = coq_apps (coq_of_cf cf1) [h'; Coq_var "Q"] in
funhq "tag_pay" (coq_exist "H'" hprop (coq_conj c1 c2))
(* (!Pay: fun H Q => exists H', pay_one H H' /\ F1 H' Q *)
(* old:
let r = Coq_var "R" in
let typr = formula_type in
let q' = Coq_var "Q'" in
let p1 = coq_apps (coq_of_cf cf1) [h;q'] in
let c1 = coq_apps (coq_of_cf cf2) [h;q'] in
let c2 = coq_apps r [ Coq_app (q', coq_tt); q] in
let body2 = funhq "tag_seq" ~rettype:coq_unit (coq_exist "Q'" wild_to_hprop (coq_conj c1 c2)) in
let p2 = coq_apps body2 [Coq_app(q',coq_bool_true); q] in
let body3 = funhq "tag_ret" ~rettype:coq_unit (heap_impl_unit h q) in
let p3 = coq_apps body3 [Coq_app(q',coq_bool_false); q] in
let bodyif = coq_exist "Q'" (Coq_impl (coq_bool, hprop)) (coq_conjs [p1;p2;p3]) in
let bodyr = coq_apps (funhq "tag_if" bodyif) [h;q] in
let hypr = coq_foralls [("H", hprop); ("Q", Coq_impl (coq_unit, hprop))] (Coq_impl (bodyr,(coq_apps r [h;q]))) in
funhq "tag_while" (Coq_forall (("R",typr), coq_impls [localr; hypr] (coq_apps r [h;q])))
(* (!While: (fun H Q => forall R:~~unit, is_local R ->
(forall H Q,
!If: (fun H Q => exists Q',
F1 H Q'
/\ (!Seq: (fun H Q => exists Q', F2 H Q' /\ R (Q' tt) Q) (Q' true) Q)
/\ (!Ret: (fun H Q => H ==> Q tt) (Q' false) Q)
H Q
-> R H Q)
-> R H Q). *)
*)
| Cf_manual c -> c
| Cf_letpure _ -> unsupported "letpure-expression in imperative mode"
(* --todo: scope of type variables should be different than that of program variables: prefix them! *)
(*#########################################################################*)
(* ** Characteristic formulae for top level declarations *)
let coqtops_of_cftop coq_of_cf cft =
match cft with
| Cftop_val (x,t) ->
(* the following is the same as for pure *)
(* TODO: later, when side effects are allowed, we need to check type is inhabited
[ Coqtop_instance ((x ^ "_type_inhab", Coq_app (Coq_var "Inhab", t)), true);
Coqtop_proof "inhab.";