Commit 70dacda8 authored by charguer's avatar charguer

ca compile rm Array.cmj && make tools && make

parent e67bc044
......@@ -34,7 +34,9 @@ let not_in_normal_form s =
let external_modules = ref []
let external_modules_add name =
external_modules := name::!external_modules
if not (List.mem name !external_modules)
then external_modules := name::!external_modules
(* TODO: use a structure more efficient than lists *)
let external_modules_get_coqtop () =
List.map (fun name -> Coqtop_require [name]) !external_modules
......@@ -369,8 +371,7 @@ let exp_get_inlined_primitive e oargs =
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
let x = lift_path_name (protect_infix_path p) in
coq_app_var_wilds x (typ_arity_var env p)
| Some y ->
Coq_var y
......@@ -1369,7 +1370,7 @@ and cfg_module id m =
let cfg_file str =
[ Cftop_coqs ([
Coqtop_set_implicit_args;
Coqtop_require ["LibLogic"; "LibRelation"; "LibInt"; "Shared"; "CFHeaps"; "CFApp" ];
Coqtop_require [ "Coq.ZArith.BinInt"; "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).";
......
......@@ -269,7 +269,7 @@ let coq_gt c1 c2 =
coq_apps (Coq_var "LibOrder.gt") [ c1; c2 ]
let coq_plus c1 c2 =
coq_apps (Coq_var "Zplus") [ c1; c2 ]
coq_apps (Coq_var "Coq.ZArith.BinInt.Zplus") [ c1; c2 ]
(** Toplevel *)
......
......@@ -32,7 +32,7 @@ let rec coqtops_of_imp_cf cf =
(* (!R: fun H Q => H ==> Q v *)
| Cf_assert cf1 ->
let p = coq_eq (Coq_var "_b") coq_true in
let p = coq_eq (Coq_var "_b") coq_bool_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
......@@ -164,15 +164,15 @@ let rec coqtops_of_imp_cf cf =
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 body_le = funhq "tag_seq" ~rettype:coq_unit (coq_exist "Q'" (Coq_impl (coq_unit, 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 locals = Coq_app (Coq_var "CFHeaps.is_local_pred", 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 ->
(* (!For (fun H Q => forall S:int->~~unit, is_local_pred 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) ))
......
......@@ -54,6 +54,7 @@ let _ =
failwith "Expects one argument: the filename of the ML source file";
let sourcefile = args.(1) in
*)
Clflags.strict_sequence := true;
(* todo: improve the path to mystdlib *)
let gen_dir = Filename.dirname Sys.argv.(0) in
......
......@@ -29,6 +29,8 @@ let _ =
(fun f -> files := f::!files)
("usage: [-I dir] [..other options..] file.mli");
Clflags.strict_sequence := true;
(* todo: improve the path to mystdlib *)
let gen_dir = Filename.dirname Sys.argv.(0) in
if not !no_mystd_include
......
......@@ -19,10 +19,12 @@ let check_var loc x =
(* TODO: should check that constructor names don't end with "_"
because these are used by type variables, e.g. "A_" *)
(* TODO: rename on the fly coq keyword such as exists, forall, etc...*)
(*#########################################################################*)
(* ** Fresh name generation *)
(** Fresh pattern variable name *)
let pattern_generated_name i =
......@@ -121,7 +123,8 @@ let cf_axiom_name name =
(*#########################################################################*)
(* ** Renaming of infix function names *)
(* ** Renaming of infix function names, and special names *)
(* TODO: rename "infix" into something more general *)
(** Auxiliary function for encoding infix function names *)
......@@ -143,7 +146,8 @@ let infix_name_symbols =
'@', 'o';
'^', 'p';
'|', 'q';
'~', 'r']
'~', 'r';
'>', 's'] (* why was ">" not in the list? TODO *)
let infix_name_encode name =
let gen = String.map (fun c ->
......@@ -156,8 +160,23 @@ let infix_name_encode name =
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
let r =
if n > 0 && List.mem_assoc name.[0] infix_name_symbols
then infix_name_encode name
else if name = "exists" then "exists__"
else if name = "forall" then "forall__"
else name in
r
(* debug: Printf.printf "protect %s as %s\n" name r;*)
(** Same extended to paths;
TODO: this breaks identities of variables, maybe not an issue? *)
let rec protect_infix_path p =
Path.(
match p with
| Pident id -> Pident (Ident.create (protect_infix (Ident.name id)))
| Pdot(p, s, pos) -> Pdot(p, protect_infix s, pos)
| Papply(p1, p2) -> Papply(p1, protect_infix_path p2) (* TODO: is this correct? *)
)
\ No newline at end of file
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