Commit 193f7455 authored by charguer's avatar charguer

renaming

parent bb1a10d2
see if we can get rid of make_cmj
xwhile: error reporting when arguments don't have the right types.
notation "# H" uniquement lorsque H est au type hprop.
rename xextract to xpull; and xgen to xpush.
todo: model K/E -> list V
infix_eq_
comparable_type A || comparable_value x || comparable_value y
x = y : A
comparable_value x || comparable_value y
comparable_value x || comparable_value y
x = y : A
forall x : int, comparable_value x
mettre trop de let pour les fonctions builtin;
xuntag_goal. => dans xcf.
CFPrint.tag
app_def
infix_eq_
assume
MAJOR TODAY
......@@ -52,15 +33,19 @@ MAJOR NEXT
- xabstract => reimplement and rename as xgen
- open no scope in CF.
MAJOR NEXT NEXT
- record single field and array single cell notation
Notation "x `. f '~>' S" :=
Notation "x `[ i ] '~>' S" :=
Notation "x `. f '~>' S" :=
Notation "x `[ i ] '~>' S" :=
- realize array specification using single-cell array specifications
- see if we can get rid of make_cmj
MAJOR POSTPONED
......@@ -71,36 +56,17 @@ MAJOR POSTPONED
=> how to shared typed/untyped AST
- implement the work around for type abbreviations:
type typerecb1 = | Typerecb_1 of typerecb2
and typerecb2 = typerecb1 list
SANITY
- discuss the naming scheme
=> type t --> t_ || x'
=> var fresh x --> x12__
=> var x' --> x_prime_
=> var (++) --> plus_plus_infix_ || infix_plus_plus_
=> PB: plus_plus_infix' !
=> var x_ --> forbidden
type typerecb1 = | Typerecb_1 of typerecb2
and typerecb2 = typerecb1 list
- reject programs with constructor names ending with "_"
(e.g. "A_" is already used for type variables *)
- would it be better to perform all renaming during normalization phase?
- reject variable names and type definition that belongs to the list
builtin_type_constructors
- have a flag to control whether functions such as "min", "max", "abs", etc..
should be systematically let-bound; this would allow binding these names.
- rename on the fly coq keyword such as exists, forall, etc..
=> requires a list of all coq keywords: see
else if name = "exists" then "exists__"
else if name = "forall" then "forall__"
- prevent rebinding of List
- restriction on not binding "min" and "max" might be a bit restrictive..
- need to prevent double-underscore in the names?
##################################################################
# FUTURE WORK
OTHER LANGUAGES
......@@ -132,7 +98,31 @@ MAKEFILE BEAUTIFY
- make systematic use of || (rm -f $@; exit 1) in cfml calls
- In the makefile.Coq, when building the .vq and obtaining
"Error: /home/charguer/tlc/src/LibPer.vio: premature end of file. Try to rebuild it."
"Error: /home/charguer/tlc/src/LibPer.vio: premature end of file. Try to rebuild it."
=> then delete the .vio file
(useful for compilations interrupted using CTRL+C)
=> even better, wrap "coqc -quick" with an atomic commit of its result.
##################################################################
# PROPOSAL FOR DEFENSIVE CODE
- VStack.ml contains a verified stack implemementation using CFML.
(not polluted by any runtime checks).
- SStack.ml is a wrapper for VStack which adds asserts;
e.g. let pop s = assert (!s <> nil); VStack.pop s
- The file SStack.ml is processed using a special mode of CFML,
in which "assert t" is interpreted as "t needs to run safely
and produce some boolean; and the rest of the code may
assume this boolean to be true". Formally:
(Assert F) H Q :=
exists (P:Prop),
(F H (fun (b:bool) => [b = true <-> P] \* H))
/\ (H \* [P] ==> Q tt)
During the proof, the user needs to provide the proposition
[P] that is tested by the assertion. This proposition can
be assumed to be true after the assert is executed.
......@@ -24,6 +24,28 @@ let f () : 'a list =
*)
(********************************************************************)
(* ** Encoding of names *)
(* type renaming_t_ = int --rejected *)
(* type renaming_t__ = int --rejected *)
(* type renaming_t1 = C_ --rejected *)
type renaming_t' = int
type renaming_t2 = C'
type 'a renaming_t3 = int
type 'a_ renaming_t4 = int
let renaming_demo () =
(* let x_ = 3 in --rejected *)
(* let x__ = 3 in --rejected *)
let x = 3 in
let x' = 3 in
let x_' = 3 in
let exists = 3 in
let array = 3 in
()
(********************************************************************)
(* ** Return *)
......
This diff is collapsed.
......@@ -233,7 +233,7 @@ let rec pattern_variables p : typed_vars = (* ignores aliases *)
let aux = pattern_variables in
match p.pat_desc with
| Tpat_any -> not_in_normal_form loc "wildcard patterns remain after normalization"
| Tpat_var s -> [Ident.name s, coq_typ_pat p]
| Tpat_var s -> [var_name (Ident.name s), coq_typ_pat p]
| Tpat_alias (p, s) -> aux p
| Tpat_constant c -> []
| Tpat_tuple l -> list_concat_map aux l
......@@ -252,7 +252,7 @@ let rec lift_pat ?(through_aliases=true) p : coq =
let aux = lift_pat ~through_aliases:through_aliases in
match p.pat_desc with
| Tpat_var s ->
Coq_var (Ident.name s)
Coq_var (var_name (Ident.name s))
| Tpat_constant (Const_int n) ->
Coq_int n
| Tpat_tuple l ->
......@@ -262,7 +262,7 @@ let rec lift_pat ?(through_aliases=true) p : coq =
| Tpat_alias (p, ak) ->
begin match ak with
| TPat_alias id ->
if through_aliases then aux p else Coq_var (Ident.name id)
if through_aliases then aux p else Coq_var (var_name (Ident.name id))
| TPat_constraint ty ->
let typ = lift_typ_exp ty.ctyp_type in
Coq_annot (aux p, typ)
......@@ -430,7 +430,7 @@ let exp_is_inlined_primitive e oargs =
let lift_exp_path env p =
match find_primitive (Path.name p) with
| None ->
let x = lift_path_name (protect_infix_path p) in
let x = lift_path_name (var_path p) in
coq_app_var_wilds x (typ_arity_var env p)
| Some y ->
Coq_var y
......@@ -570,8 +570,7 @@ let pattern_name p =
(** Takes a function name and encodes its name in case of an infix operator *)
let pattern_name_protect_infix p =
protect_infix (pattern_name p)
var_name (pattern_name p)
(** An alternative version of function extract_label_names, for obtaining record labels *)
......@@ -960,7 +959,7 @@ let rec cfg_structure_item s : cftops =
[ Cftop_coqs [ Coqtop_require_import [ lift_full_path_name path ] ] ]
| Tstr_primitive(id, descr) ->
let id = protect_infix (Ident.name id) in
let id = var_name (Ident.name id) in
let fvs, typ = lift_typ_sch descr.val_desc.ctyp_type in
let typ = coq_fun_types fvs typ in
[ Cftop_val (id, typ) ]
......@@ -980,20 +979,25 @@ let rec cfg_structure_item s : cftops =
a type abbreviation. *)
and cfg_type_abbrev (name,dec) =
let x = type_constr_name (Ident.name name) in
let loc = dec.typ_loc in
let x = Ident.name name in
check_type_constr_name loc x;
let name = type_constr_name x 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
| None -> [Coqtop_param (x, sort)]
| Some t -> [Coqtop_def ((x, sort), coq_fun_types args (lift_typ_exp t));
Coqtop_hint_unfold ([x],"typeclass_instances") ] in
| None -> [Coqtop_param (name, sort)]
| Some t -> [Coqtop_def ((name, sort), coq_fun_types args (lift_typ_exp t));
Coqtop_hint_unfold ([name],"typeclass_instances") ] in
coqs
(** Generate the top-level Coq declarations associated with
a record definition. *)
and cfg_type_record (name,dec) =
let loc = dec.typ_loc in
let x = Ident.name name in
check_type_constr_name loc x;
let name_of_field lbl =
record_field_name lbl in
let fields = match dec.typ_type.type_kind with Type_record (l,_) -> l | _ -> assert false in
......@@ -1241,22 +1245,25 @@ and cfg_algebraics decls =
(* -- todo: Caml types often clash with Caml program variables, since in Coq
they get put in the same namespace *)
let trans_ind (name,dec) =
let loc = dec.typ_loc in
let x = Ident.name name in
check_type_constr_name loc x;
let branches = match dec.typ_type.type_kind with Type_variant l -> l | _ -> assert false in
let params = List.map name_of_type dec.typ_type.type_params in
let ret_typ = coq_apps (Coq_var (type_constr_name x)) (coq_vars params) in
let get_typed_constructor (c,ts) =
check_constr_name loc c;
(c, coq_impls (List.map lift_typ_exp ts) ret_typ) in
let coqind_decl =
if List.length decls = 1 then
{ coqind_name = type_constr_name x;
coqind_constructor_name = record_constructor_name x;
coqind_constructor_name = algebraic_constructor_name x;
coqind_targs = coq_types params;
coqind_ret = Coq_type;
coqind_branches = List.map get_typed_constructor branches; }
else
{ coqind_name = type_constr_name x;
coqind_constructor_name = record_constructor_name x;
coqind_constructor_name = algebraic_constructor_name x;
coqind_targs = [];
coqind_ret = coq_impl_types (List.length params);
coqind_branches = List.map
......
......@@ -79,7 +79,7 @@ let rec coqtops_of_imp_cf cf =
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_conc = coq_apps (Coq_var "CFML.CFApp.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
......
......@@ -24,7 +24,7 @@ let fullname_of_lident idt =
String.concat "." words
let check_lident loc idt = (* DEPRECATED *)
check_var loc (name_of_lident idt)
check_var_name loc (name_of_lident idt)
(*#########################################################################*)
......@@ -120,9 +120,9 @@ let normalize_pattern p =
| Ppat_any -> Ppat_var (next_name())
| Ppat_var s ->
(* hack to handle generated vars *)
if loc <> Location.none then check_var loc s;
if loc <> Location.none then check_var_name loc s;
Ppat_var s
| Ppat_alias (p, s) -> check_var loc s; Ppat_alias (aux p, s)
| Ppat_alias (p, s) -> check_var_name loc s; Ppat_alias (aux p, s)
| Ppat_constant c -> Ppat_constant c
| Ppat_tuple l -> Ppat_tuple (List.map aux l)
| Ppat_construct (li, po, b) -> Ppat_construct (li, option_map aux po, b)
......
......@@ -172,7 +172,7 @@ and expr1 = function
else parens (apps ((string tag)::(List.map expr0 args)))
in
apps [
string "CFPrint.tag"; (* @ *)
string "CFML.CFPrint.tag"; (* @ *)
stag;
(* FUTURE USE: label l;*)
(* string "_"; *)
......
This diff is collapsed.
......@@ -577,7 +577,7 @@ Notation "Q \*+ H" :=
(fun x => heap_is_star (Q x) H)
(at level 40) : heap_scope.
Notation "# H" := (fun _:unit => H)
Notation "# H" := (fun (_:unit) => (H:hprop))
(at level 39, H at level 99) : heap_scope.
Notation "\[= v ]" := (fun x => \[x = v])
......@@ -585,12 +585,14 @@ Notation "\[= v ]" := (fun x => \[x = v])
Notation "P ==+> Q" := (pred_le P%h (heap_is_star P Q))
(at level 55, only parsing) : heap_scope.
(* TODO: notation PRE P '/' ==> KEEP '/' POST Q *)
(* DEPRECATED
Notation "'hkeep' P '==>' Q" := (pred_le P%h (Q \* P))
(at level 55, P at level 0, right associativity) : heap_scope.
*)
(*------------------------------------------------------------------*)
(* ** Properties of heap empty *)
......
......@@ -875,13 +875,14 @@ Notation "'RegisterSpecCredits' T" := (Register database_spec_credits T)
(** The focus and unfocus databases are used to register specifications
for accessors to record fields, combined with focus/unfocus operations *)
Definition database_spec_focus := True.
Notation "'focus'" := database_spec_focus.
Definition database_spec_unfocus := True.
Notation "'unfocus'" := database_spec_unfocus.
Definition database_xopen := True.
Definition database_xclose := True.
Notation "'RegisterOpen' T" := (Register database_xopen T)
(at level 69) : charac.
Notation "'RegisterClose' T" := (Register database_xclose T)
(at level 69) : charac.
......
This diff is collapsed.
......@@ -129,7 +129,8 @@ endif
# Only the %.cmj target is known to "make".
%.cmj: %.ml $(CFML_MLV)
$(CFML_MLV) $(OCAML_FLAGS) -nostdlib -I $(CFML)/lib/stdlib -I . $< || (rm -f $@; exit 1)
echo $(CFML_MLV) $(OCAML_FLAGS) -nostdlib -I $(CFML)/lib/stdlib -I . $<
@$(CFML_MLV) $(OCAML_FLAGS) -nostdlib -I $(CFML)/lib/stdlib -I . $< || (rm -f $@; exit 1)
# We use Coq to produce a .vio file out of a .v file.
......
......@@ -58,11 +58,11 @@ Qed.
Hint Extern 1 (RegisterSpec append) => Provide append_spec.
Lemma infix_at__spec : forall A (l1 l2:list A),
app infix_at_ [l1 l2] \[] \[= (@TLC.LibList.append _) l1 l2].
Lemma infix_at_spec : forall A (l1 l2:list A),
app infix_at__ [l1 l2] \[] \[= (@TLC.LibList.append _) l1 l2].
Proof using. xcf_go~. Qed.
Hint Extern 1 (RegisterSpec infix_at_) => Provide infix_at__spec.
Hint Extern 1 (RegisterSpec infix_at__) => Provide infix_at_spec.
Lemma concat_spec : forall A (l:list (list A)),
app concat [l] \[] \[= (@TLC.LibList.concat _) l].
......
......@@ -19,43 +19,43 @@ Hint Extern 1 (RegisterSpec not) => Provide not_spec.
(************************************************************)
(** Physical equality *)
Parameter infix_eq_eq__spec : curried 2%nat infix_eq_eq_ /\
Parameter infix_eq_eq_spec : curried 2%nat infix_eq_eq__ /\
forall (a b:loc),
app infix_eq_eq_ [a b] \[] \[= isTrue (a = b) ].
app infix_eq_eq__ [a b] \[] \[= isTrue (a = b) ].
Hint Extern 1 (RegisterSpec infix_eq_eq_) => Provide infix_eq_eq__spec.
Hint Extern 1 (RegisterSpec infix_eq_eq__) => Provide infix_eq_eq_spec.
Lemma infix_emark_eq__spec : curried 2%nat infix_emark_eq_ /\
Lemma infix_emark_eq_spec : curried 2%nat infix_emark_eq__ /\
forall (a b:loc),
app infix_emark_eq_ [a b] \[] \[= isTrue (a <> b) ].
app infix_emark_eq__ [a b] \[] \[= isTrue (a <> b) ].
Proof using.
xcf. xgo*. rew_refl; xauto*.
Qed.
Hint Extern 1 (RegisterSpec infix_emark_eq_) => Provide infix_emark_eq__spec.
Hint Extern 1 (RegisterSpec infix_emark_eq__) => Provide infix_emark_eq_spec.
(************************************************************)
(** Comparison *)
Definition eq_spec_for (A:Type) := curried 2%nat infix_eq_ /\
Definition eq_spec_for (A:Type) := curried 2%nat infix_eq__ /\
forall (a b:bool),
app infix_eq_ [a b] \[] \[= isTrue (a = b) ].
app infix_eq__ [a b] \[] \[= isTrue (a = b) ].
Parameter eq_bool_spec : eq_spec_for bool.
Parameter eq_int_spec : eq_spec_for int.
Hint Extern 1 (RegisterSpec infix_eq_) => Provide eq_int_spec.
Hint Extern 1 (RegisterSpec infix_eq__) => Provide eq_int_spec.
(* TODO: register several specs *)
Definition neq_spec_for (A:Type) := curried 2%nat infix_lt_gt_ /\
Definition neq_spec_for (A:Type) := curried 2%nat infix_lt_gt__ /\
forall (a b:bool),
app infix_lt_gt_ [a b] \[] \[= isTrue (a <> b) ].
app infix_lt_gt__ [a b] \[] \[= isTrue (a <> b) ].
Parameter neq_bool_spec : neq_spec_for bool.
Parameter neq_int_spec : neq_spec_for int.
Hint Extern 1 (RegisterSpec infix_lt_gt_) => Provide neq_int_spec.
Hint Extern 1 (RegisterSpec infix_lt_gt__) => Provide neq_int_spec.
(* LATER: give specification for partially applied comparison operators *)
......@@ -82,51 +82,51 @@ Hint Extern 1 (RegisterSpec max) => Provide max_spec.
(************************************************************)
(** Boolean *)
Parameter infix_bar_bar__spec : forall (a b:bool),
app infix_bar_bar_ [a b] \[] \[= a && b ].
Parameter infix_bar_bar_spec : forall (a b:bool),
app infix_bar_bar__ [a b] \[] \[= a && b ].
Parameter infix_amp_amp__spec : forall (a b:bool),
app infix_amp_amp_ [a b] \[] \[= a || b ].
Parameter infix_amp_amp_spec : forall (a b:bool),
app infix_amp_amp__ [a b] \[] \[= a || b ].
Hint Extern 1 (RegisterSpec infix_bar_bar_) => Provide infix_bar_bar__spec.
Hint Extern 1 (RegisterSpec infix_amp_amp_) => Provide infix_amp_amp__spec.
Hint Extern 1 (RegisterSpec infix_bar_bar__) => Provide infix_bar_bar_spec.
Hint Extern 1 (RegisterSpec infix_amp_amp__) => Provide infix_amp_amp_spec.
(************************************************************)
(** Integer *)
Parameter infix_tilde_minus__spec : curried 1%nat infix_tilde_minus_ /\
Parameter infix_tilde_minus_spec : curried 1%nat infix_tilde_minus__ /\
forall (n:int),
app infix_tilde_minus_ [n] \[] \[= Coq.ZArith.BinInt.Zopp n ].
app infix_tilde_minus__ [n] \[] \[= Coq.ZArith.BinInt.Zopp n ].
Parameter infix_plus__spec : curried 2%nat infix_plus_ /\
Parameter infix_plus_spec : curried 2%nat infix_plus__ /\
forall (n m:int),
app infix_plus_ [n m] \[] \[= Coq.ZArith.BinInt.Zplus n m ].
app infix_plus__ [n m] \[] \[= Coq.ZArith.BinInt.Zplus n m ].
Parameter infix_minus__spec : curried 2%nat infix_minus_ /\
Parameter infix_minus_spec : curried 2%nat infix_minus__ /\
forall (n m:int),
app infix_minus_ [n m] \[] \[= Coq.ZArith.BinInt.Zminus n m ].
app infix_minus__ [n m] \[] \[= Coq.ZArith.BinInt.Zminus n m ].
Parameter infix_star__spec : curried 2%nat infix_star_ /\
Parameter infix_star_spec : curried 2%nat infix_star__ /\
forall (n m:int),
app infix_star_ [n m] \[] \[= Coq.ZArith.BinInt.Zmult n m ].
app infix_star__ [n m] \[] \[= Coq.ZArith.BinInt.Zmult n m ].
Parameter infix_slash__spec : curried 2%nat infix_slash_ /\
Parameter infix_slash_spec : curried 2%nat infix_slash__ /\
forall (n m:int),
m <> 0 ->
app infix_slash_ [n m] \[] \[= CFML.CFHeader.int_div n m ].
app infix_slash__ [n m] \[] \[= CFML.CFHeader.int_div n m ].
Parameter infix_mod__spec : curried 2%nat infix_mod_ /\
Parameter infix_mod_spec : curried 2%nat infix_mod__ /\
forall (n m:int),
m <> 0 ->
app infix_mod_ [n m] \[] \[= CFML.CFHeader.int_mod n m ].
app infix_mod__ [n m] \[] \[= CFML.CFHeader.int_mod n m ].
Hint Extern 1 (RegisterSpec infix_tilde_minus_) => Provide infix_tilde_minus__spec.
Hint Extern 1 (RegisterSpec infix_plus_) => Provide infix_plus__spec.
Hint Extern 1 (RegisterSpec infix_minus_) => Provide infix_minus__spec.
Hint Extern 1 (RegisterSpec infix_star_) => Provide infix_star__spec.
Hint Extern 1 (RegisterSpec infix_slash_) => Provide infix_slash__spec.
Hint Extern 1 (RegisterSpec infix_mod_) => Provide infix_mod__spec.
Hint Extern 1 (RegisterSpec infix_tilde_minus__) => Provide infix_tilde_minus_spec.
Hint Extern 1 (RegisterSpec infix_plus__) => Provide infix_plus_spec.
Hint Extern 1 (RegisterSpec infix_minus__) => Provide infix_minus_spec.
Hint Extern 1 (RegisterSpec infix_star__) => Provide infix_star_spec.
Hint Extern 1 (RegisterSpec infix_slash__) => Provide infix_slash_spec.
Hint Extern 1 (RegisterSpec infix_mod__) => Provide infix_mod_spec.
(* NOT NEEDED
Notation "`~- n" := (App infix_tilde_minus_ n;)
......@@ -182,23 +182,23 @@ Lemma ref_spec : forall a (v:a),
app ref [v] \[] (fun r => r ~~> v).
Proof using. xcf_go~. Qed.
Lemma infix_emark__spec : forall a (v:a) r,
app_keep infix_emark_ [r] (r ~~> v) \[= v].
Lemma infix_emark_spec : forall a (v:a) r,
app_keep infix_emark__ [r] (r ~~> v) \[= v].
Proof using. xunfold Ref. xcf_go~. Qed.
Lemma infix_colon_eq__spec : forall a (v w:a) r,
app infix_colon_eq_ [r w] (r ~~> v) (# r ~~> w).
Lemma infix_colon_eq_spec : forall a (v w:a) r,
app infix_colon_eq__ [r w] (r ~~> v) (# r ~~> w).
Proof using. xunfold Ref. xcf_go~. Qed.
Hint Extern 1 (RegisterSpec ref) => Provide ref_spec.
Hint Extern 1 (RegisterSpec infix_emark_) => Provide infix_emark__spec.
Hint Extern 1 (RegisterSpec infix_colon_eq_) => Provide infix_colon_eq__spec.
Hint Extern 1 (RegisterSpec infix_emark__) => Provide infix_emark_spec.
Hint Extern 1 (RegisterSpec infix_colon_eq__) => Provide infix_colon_eq_spec.
Notation "'App'' `! r" := (App infix_emark_ r;)
Notation "'App'' `! r" := (App infix_emark__ r;)
(at level 69, no associativity, r at level 0,
format "'App'' `! r") : charac.
Notation "'App'' r `:= x" := (App infix_colon_eq_ r x;)
Notation "'App'' r `:= x" := (App infix_colon_eq__ r x;)
(at level 69, no associativity, r at level 0,
format "'App'' r `:= x") : charac.
......
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