Commit aaad917b authored by charguer's avatar charguer

inprogress

parent 0dfb5e23
......@@ -36,7 +36,7 @@ let external_modules_add name =
external_modules := name::!external_modules
let external_modules_get_coqtop () =
List.map (fun name -> Coqtop_require name) !external_modules
List.map (fun name -> Coqtop_require [name]) !external_modules
let external_modules_reset () =
external_modules := []
......@@ -371,6 +371,48 @@ 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 *)
......@@ -381,8 +423,10 @@ let lift_exp_path env p =
match find_primitive (Path.name p) with
| None ->
let x = lift_path_name p in
let x = protect_infix x in
coq_app_var_wilds x (typ_arity_var env p)
| Some y -> Coq_var y
| Some y ->
Coq_var y
(** Translate a Caml value into a Coq value. Fails if the Coq
expression provided is not a value. *)
......@@ -508,45 +552,10 @@ let rec pattern_ident p =
let pattern_name p =
Ident.name (pattern_ident p)
(** 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 ^ "_"
(** Takes a function name and encodes its name in case of an infix operator *)
let pattern_name_protect_infix p =
let name = pattern_name p in
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
(* debug: Printf.printf "protect %s as %s\n" name r;*)
r
protect_infix (pattern_name p)
(** An alternative version of function extract_label_names, for obtaining record labels *)
......@@ -894,7 +903,7 @@ let rec cfg_structure_item s : cftops =
| Tstr_open path ->
if is_primitive_module (Path.name path) then [] else
[ Cftop_coqs [ Coqtop_require_import (lift_full_path_name path) ] ]
[ Cftop_coqs [ Coqtop_require_import [ lift_full_path_name path ] ] ]
| Tstr_primitive(id, descr) ->
let id = Ident.name id in
......@@ -1148,12 +1157,14 @@ 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_convert_focus_unfocus
@ fields_convert_focus_unfocus
@ new_spec
@ (List.concat (List.map get_set_spec indices))
@ (List.concat (List.map get_spec_focus indices))
@ (List.concat (List.map set_spec_unfocus indices))
*)
(** Generate the top-level Coq declarations associated with
......@@ -1407,8 +1418,17 @@ and cfg_module id m =
let cfg_file str =
[ Cftop_coqs ([
Coqtop_set_implicit_args;
Coqtop_require_import "CFHeader" ]
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."
]
@ (external_modules_get_coqtop())) ]
@ cfg_structure str
(*deprecated: (if !pure_mode then "FuncPrim" else "CFHeader") *)
\ No newline at end of file
(*deprecated: (if !pure_mode then "FuncPrim" else "CFHeader") *)
(* TODO: prevent "let int = 3" to work *)
\ No newline at end of file
......@@ -56,9 +56,9 @@ type coqtop =
| Coqtop_register of string * var * var
| Coqtop_hint_constructors of vars * var
| Coqtop_hint_unfold of vars * var
| Coqtop_require of string
| Coqtop_import of string
| Coqtop_require_import of var
| Coqtop_require of vars
| Coqtop_import of vars
| Coqtop_require_import of vars
| Coqtop_set_implicit_args
| Coqtop_text of string
| Coqtop_declare_module of var * mod_typ
......
......@@ -42,6 +42,10 @@ and cftops = cftop list
(*#########################################################################*)
(* ** Shared functions *)
(** Abstract datatype for dynamic values *)
let coq_dyn_at = coq_var_at "CFHeaps.dyn"
(** Abstract datatype for functions *)
let val_type = Coq_var "CFApp.func"
......@@ -99,7 +103,7 @@ let formula_type =
(** Hprop entailment [H1 ==> H2] *)
let heap_impl h1 h2 =
coq_apps (Coq_var "pred_le") [h1;h2]
coq_apps (Coq_var "LibLogic.pred_le") [h1;h2]
(** Specialized Hprop entailment [H1 ==> Q2 tt] *)
......@@ -109,7 +113,7 @@ let heap_impl_unit h1 q2 =
(** Postcondition entailment [Q1 ===> Q2] *)
let post_impl q1 q2 =
coq_apps (Coq_var "rel_le") [q1;q2]
coq_apps (Coq_var "LibRelation.rel_le") [q1;q2]
(** Specialized post-conditions [fun (_:unit) => H], i.e. [# H] *)
......@@ -119,17 +123,17 @@ let post_unit h =
(** Separating conjunction [H1 * H2] *)
let heap_star h1 h2 =
coq_apps (Coq_var "heap_is_star") [h1;h2]
coq_apps (Coq_var "CFHeaps.heap_is_star") [h1;h2]
(** Base data [heap_is_single c1 c2] *)
let heap_is_single c1 c2 =
coq_apps (coq_var_at "heap_is_single") [c1;Coq_wild;c2]
coq_apps (coq_var_at "CFHeaps.heap_is_single") [c1;Coq_wild;c2]
(** Empty heap predicate [[]] *)
let heap_empty =
Coq_var "heap_is_empty"
Coq_var "CFHeaps.heap_is_empty"
(** Iterated separating conjunction [H1 * .. * HN] *)
......@@ -141,7 +145,7 @@ let heap_stars hs =
(** Lifted existentials [Hexists x, H] *)
let heap_exists xname xtype h =
Coq_app (Coq_var "heap_is_pack", Coq_fun ((xname, xtype), h))
Coq_app (Coq_var "CFHeaps.heap_is_pack", Coq_fun ((xname, xtype), h))
(** Lifted existentials [Hexists x, H], alternative *)
......@@ -156,7 +160,7 @@ let heap_existss x_names_types h =
(** Lifted propositions [ [P] ] *)
let heap_pred c =
Coq_app (Coq_var "heap_is_empty_st", c)
Coq_app (Coq_var "CFHeaps.heap_is_empty_st", c)
(*#########################################################################*)
......@@ -173,7 +177,7 @@ let rec coqtops_of_imp_cf cf =
| Some t -> t
in
let f_core = coq_funs [("H", hprop);("Q", Coq_impl(typ,hprop))] c in
let f = Coq_app (Coq_var "local", f_core) 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
......@@ -204,7 +208,7 @@ let rec coqtops_of_imp_cf cf =
(* 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_var_at "dyn") [t;v]) tvs 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)])) *)
......@@ -228,7 +232,7 @@ let rec coqtops_of_imp_cf cf =
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_var_at "dyn") [t; coq_var x]) targs 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
......@@ -323,7 +327,7 @@ let rec coqtops_of_imp_cf cf =
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 "is_local_1", s) 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])))
......@@ -343,7 +347,7 @@ let rec coqtops_of_imp_cf cf =
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 "is_local", r) 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,
......
......@@ -135,6 +135,7 @@ let rec expr0 = function
| Coq_int n ->
parens (string (string_of_int n)) ^^ string "%Z"
| Coq_list cs ->
(* TODO: *)
if (cs = []) then string "nil" else
parens ((separate_map (string "::" ^^ break 1) expr0 cs) ^^ string "::nil")
| Coq_wild ->
......@@ -408,12 +409,18 @@ let top = function
spacecolon ^/^
string base
^^ dot
| Coqtop_require x ->
sprintf "Require %s." x
| Coqtop_import x ->
sprintf "Import %s." x
| Coqtop_require_import x ->
sprintf "Require Import %s." x
| Coqtop_require xs ->
string "Require " ^^
flow_map space string xs
^^ dot
| Coqtop_import xs ->
string "Import " ^^
flow_map space string xs
^^ dot
| Coqtop_require_import xs ->
string "Require Import " ^^
flow_map space string xs
^^ dot
| Coqtop_set_implicit_args ->
sprintf "Set Implicit Arguments."
| Coqtop_text s ->
......@@ -436,6 +443,9 @@ let top = function
sprintf "Include Type %s." x
| Coqtop_end x ->
sprintf "End %s." x
| Coqtop_custom x ->
sprintf "%s" x
let top t =
group (top t)
......
Set Implicit Arguments.
Require Export LibCore LibEpsilon Shared.
Require Export CFHeaps.
Require Import LibCore LibEpsilon Shared.
Require Import CFHeaps.
Open Local Scope heap_scope_advanced.
Hint Extern 1 (_ ===> _) => apply rel_le_refl.
......
Require Export CFPrint.
Require LibCore.
Require Export LibInt.
(* Require LibInt. *)
(* LibCore LibSet LibMap LibListZ *)
......@@ -17,8 +17,8 @@ SRC :=\
CFHeaps \
CFApp \
CFPrint \
CFTactics \
CFHeader \
CFTactics \
CFRep \
CFLib
......
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