Commit bf06a855 authored by charguer's avatar charguer

updates_pour_uf

parent 8d8ef8c3
......@@ -422,15 +422,20 @@ let exp_find_inlined_primitive e oargs =
"Pervasives.>="; "Pervasives.<"; "Pervasives.>";
"Pervasives.min"; "Pervasives.max"; ] ->
let is_number =
begin match btyp_of_typ_exp e1.exp_type with
try Ctype.unify e1.exp_env e1.exp_type ((*instance*) Predef.type_int); true
with _ -> false
(*begin match btyp_of_typ_exp e1.exp_type with
| Btyp_constr (id,[]) when Path.name id = "int" -> true
| _ -> false
end in
end *)
in
(* Remark: by typing, [e2] has the same type as [e1] *)
if not is_number then begin
if List.mem name [ "Pervasives.="; "Pervasives.<>"; ]
then None
else unsupported loc (Printf.sprintf "comparison operators on non integer arguments (here, %s)" (string_of_type_exp e1.exp_type));
(* TODO: improve using type unification *)
else (* warning loc *)
unsupported loc (Printf.sprintf "comparison operators on non integer arguments (here, %s)" (string_of_type_exp e1.exp_type));
end else begin match find_inlined_primitive name with
| Some (Primitive_binary_only_numbers, coq_name) -> Some coq_name
| _ -> failwith ("in exp_find_inlined_primitive, could not find the coq translation of the function: " ^ name)
......@@ -847,7 +852,7 @@ let rec cfg_exp env e =
in
let ts = coq_apps (Coq_var "Coq.Init.Datatypes.list") [targ] in
let tr = coq_typ loc e in (* 'a array *)
let func = Coq_var "STDLIB.Array_ml.make_empty" in
let func = Coq_var "STDLIB.Array_ml.of_list" in
Cf_app ([ts], tr, func, [arg])
| Texp_field (arg, p, lbl) ->
......@@ -1398,19 +1403,18 @@ and cfg_algebraics decls =
and cfg_type_decls loc (decls : (Ident.t * Typedtree.type_declaration) list) =
let has_abbrev = List.exists is_type_abbrev decls in
let all_abbrev = List.for_all is_type_abbrev decls in
(*let all_abbrev = List.for_all is_type_abbrev decls in*)
let nb_decls = List.length decls in
if has_abbrev then begin
if not (all_abbrev && nb_decls = 1)
then unsupported loc "recursive type definitions that include type abbreviations (try inlining the type abbreviations)";
cfg_type_abbrev (List.hd decls)
end else begin
let decls_records = List.filter is_type_record decls in
let decls_algebraic = List.filter is_algebraic decls in
let records_def = list_concat_map cfg_type_record decls_records in
let algebraics_def = if decls_algebraic = [] then [] else cfg_algebraics decls_algebraic in
records_def @ algebraics_def
end
if has_abbrev && nb_decls <> 1 then begin
warning loc "relying on a best-effort support for mutually-recursive type definitions going through type abbreviations; if the Coq output does not compile, you will need to inline the type abbreviation at its places of occurences."
end;
let decls_abbrev = List.filter is_type_abbrev decls in
let decls_records = List.filter is_type_record decls in
let decls_algebraic = List.filter is_algebraic decls in
let records_def = list_concat_map cfg_type_record decls_records in
let abbrev_def = list_concat_map cfg_type_abbrev decls_abbrev in
let algebraics_def = if decls_algebraic = [] then [] else cfg_algebraics decls_algebraic in
abbrev_def @ records_def @ algebraics_def
(* DEPRECATED
experimental support: simply break circularity; might stack overflow!
......
......@@ -210,15 +210,14 @@ let show_str s =
let output s =
Printf.printf "%s\n" s
let warning s = (* DEPRECATED? *)
Printf.printf "### WARNING: %s\n" s
let unsupported_noloc s =
failwith ("Unsupported language construction : " ^ s)
let unsupported loc s =
Location.print_error Format.err_formatter loc;
unsupported_noloc s
(* TODO: report location *)
let warning loc s =
Location.print Format.err_formatter loc;
Format.fprintf Format.err_formatter "Warning: @[<v 2>%s@]\n" s
......@@ -118,10 +118,6 @@ val show_str : 'a -> 'a
val output : string -> unit
(** Display a string on stdout, preceeded by a "WARNING" string *)
val warning : string -> unit
(** Display a message explaining that a feature is not supported *)
val unsupported_noloc : string -> 'a
......@@ -130,3 +126,8 @@ val unsupported_noloc : string -> 'a
and report the location *)
val unsupported : Location.t -> string -> 'a
(** Display message associated with a warning,
and report the location *)
val warning : Location.t -> string -> unit
......@@ -55,3 +55,7 @@ val echo_eof: unit -> unit
val reset: unit -> unit
val highlight_locations: formatter -> t -> t -> bool
(* CFML added *)
val print: formatter -> t -> unit
......@@ -5,15 +5,17 @@ Require Export CFLib.
(* Note: if you wish to use credits in [nat] instead of [Z] which is the
default, please load CFLibCreditsNat. *)
(*---todo : same as in CFLib (why needed?)--*)
(*---todo : same as in CFLib (why needed?)--
Ltac xlocal_core tt ::=
first [ assumption
| apply local_is_local
| apply app_local_1
| match goal with H: is_local_1 ?S |- is_local (?S _) => apply H end
| apply app_local_1 ].
Notation "l '~~>' v" := (hdata (@Ref _ _ (@Id _) v) l)
(at level 32, no associativity).
*)
(*Notation "l '~~>' v" := (hdata (@Ref _ _ (@Id _) v) l)
(at level 32, no associativity). *)
......
......@@ -94,10 +94,26 @@ Ltac xuntag_pre_post_core tt :=
Tactic Notation "xuntag_pre_post" :=
xuntag_pre_post_core tt.
(** [cfml_get_goal tt] returns the goal, ignoring the [tag_goal] at head *)
Ltac cfml_get_goal tt :=
match goal with
| |- @tag tag_goal _ ?F ?H ?Q => constr:(F H Q)
| |- ?G => constr:(G)
end.
(** [cfml_get_tag tt] returns the tag at the head of the goal *)
Ltac cfml_get_tag tt :=
let G :=
match cfml_get_goal tt with
| @tag ?t _ _ ?H ?Q => constr:(t)
| app ?f ?xs ?H ?Q => constr:(tag_none_app)
| _ => constr:(tag_none)
end.
(* DEPRECATED
Ltac cfml_get_tag tt :=
let G :=
match goal with
| |- @tag tag_goal _ ?F _ _ => constr:(F)
| |- ?G => constr:(G)
......@@ -105,9 +121,11 @@ Ltac cfml_get_tag tt :=
match G with
| @tag ?t _ _ => constr:(t)
| @tag ?t _ _ _ _ => constr:(t)
| app ?f ?xs => constr:(tag_none_app)
| app ?f ?xs ?H ?Q => constr:(tag_none_app)
| _ => constr:(tag_none)
end.
*)
(** [cfml_check_not_tagged tt] fails if the head of the goal contains a tag *)
......@@ -227,27 +245,27 @@ Local Open Scope tag_scope.
(********************************************************************)
(* ** Notation for applied characteristic formulae [tag_goal] *)
Notation "'PRE' P1 '==>' 'POST' P2" :=
(@pred_le heap P1 P2) (at level 69,
format "'[v' '[' 'PRE' P1 ']' '/' '==>' '/' '[' 'POST' P2 ']' ']'" )
Notation "P1 '==>' P2" :=
(@pred_le heap P1 P2) (at level 55, right associativity,
format "'[v' '[' P1 ']' '/' '==>' '/' '[' P2 ']' ']'" )
: charac.
Notation "'PRE' Q1 '===>' 'POST' Q2" :=
(@rel_le _ heap Q1 Q2) (at level 69,
format "'[v' '[' 'PRE' Q1 ']' '/' '===>' '/' '[' 'POST' Q2 ']' ']'")
Notation " Q1 '===>' Q2" :=
(@rel_le _ heap Q1 Q2) (at level 55, right associativity,
format "'[v' '[' Q1 ']' '/' '===>' '/' '[' Q2 ']' ']'")
: charac.
(* TODO : maybe good enough?
Notation "P1 '==>' P2" :=
Notation "'PRE' P1 '==>' 'POST' P2" :=
(@pred_le heap P1 P2) (at level 69,
format "'[v' '[' P1 ']' '/' '==>' '/' '[' P2 ']' ']'" )
format "'[v' '[' 'PRE' P1 ']' '/' '==>' '/' '[' 'POST' P2 ']' ']'",
only parsing)
: charac.
Notation " Q1 '===>' Q2" :=
Notation "'PRE' Q1 '===>' 'POST' Q2" :=
(@rel_le _ heap Q1 Q2) (at level 69,
format "'[v' '[' Q1 ']' '/' '===>' '/' '[' Q2 ']' ']'")
format "'[v' '[' 'PRE' Q1 ']' '/' '===>' '/' '[' 'POST' Q2 ']' ']'",
only parsing)
: charac.
*)
Notation "'PRE' H 'POST' Q 'CODE' F" :=
(@tag tag_goal _ F H Q) (at level 69,
......@@ -258,19 +276,10 @@ Notation "F 'PRE' H 'POST' Q" :=
(tag tag_goal F H Q)
(at level 69, only parsing) : charac.
(* DEPRECATED
Notation "F 'PRE' H 'RET' x 'ST' Qx" :=
(tag tag_goal F H (fun x => Qx))
Notation "F 'PRE_KEEP' H 'POST' Q" :=
(tag tag_goal F H%h (Q \*+ H%h))
(at level 69, only parsing) : charac.
Notation "F 'PRE' H 'RET' x 'POST' Qx" :=
(tag tag_goal F H (fun x => Qx))
(at level 69, only parsing) : charac.
*)
(********************************************************************)
(** Ret *)
......
......@@ -64,10 +64,10 @@ Ltac cfml_postcondition_is_evar tt :=
[app] or [spec] at the head of the goal. *)
Ltac cfml_get_goal_fun tt :=
match goal with
| |- spec ?f ?n ?P => constr:(f)
| |- app ?f ?xs ?H ?Q => constr:(f)
| |- tag tag_apply (app ?f ?xs) ?H ?Q => constr:(f)
match cfml_get_goal tt with
| spec ?f ?n ?P => constr:(f)
| app ?f ?xs ?H ?Q => constr:(f)
| tag tag_apply (app ?f ?xs) ?H ?Q => constr:(f)
end.
(* [cfml_get_goal_arity] returns the arity associated with the
......@@ -76,11 +76,11 @@ Ltac cfml_get_goal_fun tt :=
Ltac cfml_get_goal_arity tt :=
let aux xs :=
let n := eval compute in (List.length xs) in constr:(n) in
match goal with
| |- spec ?f ?n ?P => constr:(n)
| |- app ?f ?xs ?H ?Q => aux xs
| |- tag tag_apply (app ?f ?xs) ?H ?Q => aux xs
end .
match cfml_get_goal tt with
| spec ?f ?n ?P => constr:(n)
| app ?f ?xs ?H ?Q => aux xs
| tag tag_apply (app ?f ?xs) ?H ?Q => aux xs
end.
(* [cfml_show_types_dyn_list L] displays the types of the
arguments in the list [L] *)
......@@ -106,7 +106,7 @@ Ltac cfml_get_app_args E :=
Ltac cfml_get_goal_app_args tt :=
match goal with |- ?G => cfml_get_app_args G end.
(* [cfml_get_goal_app_ret E] returns the arguments associated with the
(* [cfml_get_app_ret E] returns the arguments associated with the
[app] in the term [E] provided. *)
Ltac cfml_get_app_ret E :=
......@@ -137,6 +137,10 @@ Ltac cfml_show_app_type E :=
Ltac cfml_show_app_type_goal tt :=
match goal with |- ?G => cfml_show_app_type G end.
Ltac cfml_show_app_type_goal tt ::=
let G := cfml_get_goal tt in
cfml_show_app_type G.
(* [cfml_show_app_type_concl S] displays the type of
the function application in the conclusion of [S] *)
......@@ -232,6 +236,16 @@ Tactic Notation "xauto" "~" := xauto_tilde.
Tactic Notation "xauto" "*" := xauto_star.
Tactic Notation "xauto" := xauto~.
(** DEPRECATED Extensions for [hsimpl] to use [xauto]
Tactic Notation "hsimpl" "~" constr(L) :=
hsimpl L; xauto~.
Tactic Notation "hsimpl" "~" constr(X1) constr(X2) :=
hsimpl X1 X2; xauto~.
Tactic Notation "hsimpl" "~" constr(X1) constr(X2) constr(X3) :=
hsimpl X1 X2 X3; xauto~.
*)
(*--------------------------------------------------------*)
(* ** [xok] *)
......@@ -251,7 +265,6 @@ Tactic Notation "xok" "*" :=
xok_core ltac:(fun _ => xauto*).
(*--------------------------------------------------------*)
(* ** [xsimpl] *)
......@@ -271,14 +284,38 @@ Tactic Notation "xsimpl" constr(E) := xsimpl_core_with E.
Tactic Notation "xsimpl" "~" constr(E) := xsimpl E; xauto~.
Tactic Notation "xsimpl" "*" constr(E) := xsimpl E; xauto*.
Tactic Notation "hsimpl" "~" constr(L) :=
Tactic Notation "xsimpl" constr(L) :=
hsimpl L.
Tactic Notation "xsimpl" constr(X1) constr(X2) :=
xsimpl (>> X1 X2).
Tactic Notation "xsimpl" constr(X1) constr(X2) constr(X3) :=
xsimpl (>> X1 X2 X3).
Tactic Notation "xsimpl" constr(X1) constr(X2) constr(X3) constr(X4) :=
xsimpl (>> X1 X2 X3 X4).
Tactic Notation "xsimpl" constr(X1) constr(X2) constr(X3) constr(X4) constr(X5) :=
xsimpl (>> X1 X2 X3 X4 X5).
Tactic Notation "xsimpl" "~" constr(L) :=
hsimpl L; xauto~.
Tactic Notation "hsimpl" "~" constr(X1) constr(X2) :=
hsimpl X1 X2; xauto~.
Tactic Notation "hsimpl" "~" constr(X1) constr(X2) constr(X3) :=
hsimpl X1 X2 X3; xauto~.
Tactic Notation "xsimpl" "~" constr(X1) constr(X2) :=
xsimpl (>> X1 X2); xauto~.
Tactic Notation "xsimpl" "~" constr(X1) constr(X2) constr(X3) :=
xsimpl (>> X1 X2 X3); xauto~.
Tactic Notation "xsimpl" "~" constr(X1) constr(X2) constr(X3) constr(X4) :=
xsimpl (>> X1 X2 X3 X4); xauto~.
Tactic Notation "xsimpl" "~" constr(X1) constr(X2) constr(X3) constr(X4) constr(X5) :=
xsimpl (>> X1 X2 X3 X4 X5); xauto~.
Tactic Notation "xsimpl" "*" constr(L) :=
hsimpl L; xauto*.
Tactic Notation "xsimpl" "*" constr(X1) constr(X2) :=
xsimpl (>> X1 X2); xauto*.
Tactic Notation "xsimpl" "*" constr(X1) constr(X2) constr(X3) :=
xsimpl (>> X1 X2 X3); xauto*.
Tactic Notation "xsimpl" "*" constr(X1) constr(X2) constr(X3) constr(X4) :=
xsimpl (>> X1 X2 X3 X4); xauto*.
Tactic Notation "xsimpl" "*" constr(X1) constr(X2) constr(X3) constr(X4) constr(X5) :=
xsimpl (>> X1 X2 X3 X4 X5); xauto*.
(*--------------------------------------------------------*)
......
......@@ -20,11 +20,9 @@ SRC :=\
CFHeader \
CFBuiltin \
CFTactics \
CFLib
# CFLibCredits \
# CFLibCreditsNat
# CFRep \
CFLib \
CFLibCredits \
CFLibCreditsNat
V := $(SRC:=.v)
......
......@@ -239,23 +239,36 @@ Hint Extern 1 (RegisterSpec asr) => Provide asr_spec.
(************************************************************)
(** References *)
Definition Ref a (v:a) (r:loc) :=
Definition Ref {A} (v:A) (r:loc) :=
r ~> `{ contents' := v }.
Axiom Ref_Heapdata : forall A,
(Heapdata (@Ref A)).
(* TODO: need an axiom about allocated records *)
(*
Proof using.
intros. applys Heapdata_prove. intros x X1 X2.
xunfold @Ref.
lets: star_is_single_same_loc.
hchange (@star_is_single_same_loc x). hsimpl.
Qed.
*)
Notation "r '~~>' v" := (hdata (Ref v) r)
(at level 32, no associativity) : heap_scope.
Lemma ref_spec : forall a (v:a),
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,
Lemma infix_emark_spec : forall A (v:A) r,
app_keep infix_emark__ [r] (r ~~> v) \[= v].
Proof using. xunfold Ref. xcf_go~. Qed.
Proof using. xunfold @Ref. xcf_go~. Qed.
Lemma infix_colon_eq_spec : forall a (v w:a) r,
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.
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.
......@@ -281,6 +294,36 @@ Hint Extern 1 (RegisterSpec incr) => Provide incr_spec.
Hint Extern 1 (RegisterSpec decr) => Provide decr_spec.
(************************************************************)
(** Group of References *)
Axiom ref_spec_group : forall A (M:map loc A) (v:A),
app Pervasives_ml.ref [v]
PRE (Group Ref M)
POST (fun (r:loc) => Group Ref (M[r:=v]) \* \[r \notindom M]).
(* TODO: proof *)
Lemma infix_emark_spec_group : forall `{Inhab A} (M:map loc A) r,
r \indom M ->
app Pervasives_ml.infix_emark__ [r]
PRE_KEEP (Group Ref M)
POST (fun x => \[x = M[r]]).
Proof using.
intros. rewrite~ (Group_rem r M). xapp. xsimpl~.
Qed.
Lemma infix_colon_eq_spec_group : forall `{Inhab A} (M:map loc A) (v:A) r,
r \indom M ->
app Pervasives_ml.infix_colon_eq__ [r v]
PRE (Group Ref M)
POST (# Group Ref (M[r:=v])).
Proof using.
intros. rewrite~ (Group_rem r M). xapp. intros tt.
hchanges~ (Group_add' r M).
Qed.
(************************************************************)
(** Pairs *)
......@@ -376,33 +419,5 @@ Implicit Arguments unfocus_ref [a A].
(************************************************************)
(** Group of References *)
Parameter caml_ref_spec_group : forall a,
Spec caml_ref (v:a) |R>> forall (M:map loc a),
R (Group (Ref Id) M) (fun (r:loc) =>
Group (Ref Id) (M[r:=v]) \* \[r \notindom M]).
Lemma caml_get_spec_group : forall a,
Spec caml_get (r:loc) |R>> forall (M:map loc a),
forall `{Inhab a}, r \indom M ->
keep R (Group (Ref Id) M) (fun x => \[x = M[r]]).
Proof.
intros. xweaken. intros r R LR HR M IA IlM. simpls.
rewrite~ (Group_rem r M). xapply (HR (M[r])); hsimpl~.
Qed.
Lemma caml_set_spec_group : forall a,
Spec caml_set (r:loc) (v:a) |R>> forall (M:map loc a),
forall `{Inhab a}, r \indom M ->
R (Group (Ref Id) M) (# Group (Ref Id) (M[r:=v])).
Proof.
intros. xweaken. intros r v R LR HR M IA IlM. simpls.
rewrite~ (Group_rem r M).
xapply (HR (M[r])). hsimpl.
intros _. hchanges~ (Group_add' r M).
Qed.
*)
\ 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