Commit 43d33b87 authored by charguer's avatar charguer
Browse files

polymorphism_ok

parent 1e3305ab
MAJOR TODAY
- patterns
- rename xextract to xpull; and xgen to xpush.
- record with
- when clauses
- add support for pure records
MAJOR NEXT
- xchanges
- patterns and when clauses
- add support for pure records
TopVal check brackets
MAJOR NEXT
- record with
- partial/over application
- xabstract => reimplement and rename as xgen
MAJOR NEXT NEXT
- xwhile: error reporting when arguments don't have the right types.
......
......@@ -8,6 +8,30 @@ open Pervasives
*)
(********************************************************************)
(* ** 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
()
(********************************************************************)
(* ** Polymorphic let bindings and value restriction *)
......@@ -115,29 +139,6 @@ let h1 =
(********************************************************************)
(* ** 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 *)
......
......@@ -3,127 +3,46 @@ Set Implicit Arguments.
Require Import CFLib.
Require Import Demo_ml.
Require Import Stdlib.
(* Open Scope tag_scope.*)
Open Scope tag_scope.
Notation "'LetPoly' '{' A1 '}' x ':=' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1, F1 H (fun r => \[@P1 A1 r] \* H1))
/\ forall x, (forall A1, @P1 A1 (@x A1)) -> F2 H1 Q))
(at level 69, A1 ident, x ident, right associativity) : charac.
(*--------------------------------------------------------*)
(* ** [xlet_poly] *)
(** [xlet_poly] is used to reason on a let node, i.e. on a goal
of the form [(LetPoly {A1} x := F1 in F2) H Q].
Variants:
- [xlet_poly P H] to describe the pure postcondition and
the final state.
- [xlet_poly_keep P] to provide a pure postcondition and
use the current pre-condition as final state.
- [xlet_poly P] to provide a pure postcondition and introduce
a unification variable for the imperative state.
- [xlet_poly as y] to rename [x] into [y].
- [xlet_poly P H as y].
*)
Ltac xlet_poly_core cont0 cont1 cont2 :=
apply local_erase;
cont0 tt;
split; [ intros | cont1 tt; cont2 tt ];
xtag_goal.
Ltac xlet_poly_def cont0 cont1 cont2 :=
xextract_check_not_needed tt;
xuntag tag_let_poly;
xlet_poly_core cont0 cont1 cont2.
Tactic Notation "xlet_poly" constr(P) constr(H) "as" simple_intropattern(x) simple_intropattern(Hx) :=
xlet_poly_def
ltac:(fun _ => exists P; exists H)
ltac:(fun _ => intros x Hx)
ltac:(fun _ => try xextract).
Tactic Notation "xlet_poly" constr(P) constr(H) "as" simple_intropattern(x) :=
let Hx := fresh "H" x in
xlet_poly P H as x Hx.
Tactic Notation "xlet_poly" constr(P) constr(H) :=
xlet_poly_def
ltac:(fun _ => exists P; exists H)
ltac:(fun _ => intro)
ltac:(fun _ => try xextract).
Tactic Notation "xlet_poly" constr(P) "as" simple_intropattern(x) simple_intropattern(Hx) :=
xlet_poly_def
ltac:(fun _ => exists P; esplit)
ltac:(fun _ => intros x Hx)
ltac:(fun _ => idtac).
Tactic Notation "xlet_poly" constr(P) "as" simple_intropattern(x) :=
let Hx := fresh "H" x in
xlet_poly P as x Hx.
Tactic Notation "xlet_poly" constr(P) :=
xlet_poly_def
ltac:(fun _ => exists P; esplit)
ltac:(fun _ => intro)
ltac:(fun _ => idtac).
Tactic Notation "xlet_poly_keep" constr(P) "as" simple_intropattern(x) simple_intropattern(Hx) :=
let H := cfml_get_precondition tt in
xlet_poly P H as x.
Tactic Notation "xlet_poly_keep" constr(P) "as" simple_intropattern(x) :=
let Hx := fresh "H" x in
xlet_poly_keep P as x Hx.
Tactic Notation "xlet_poly_keep" constr(P) :=
let H := cfml_get_precondition tt in
xlet_poly P H.
(* LATER
Tactic Notation "xlet_poly" "~" := xlet; xauto~.
Tactic Notation "xlet" "~" "as" simple_intropattern(x) := xlet as x; xauto~.
Tactic Notation "xlet" "~" constr(Q) := xlet Q; xauto~.
Tactic Notation "xlet" "~" constr(Q) "as" simple_intropattern(x) := xlet Q as x; xauto~.
Tactic Notation "xlet" "*" := xlet; xauto*.
Tactic Notation "xlet" "*" "as" simple_intropattern(x) := xlet as x; xauto*.
Tactic Notation "xlet" "*" constr(Q) := xlet Q; xauto*.
Tactic Notation "xlet" "*" constr(Q) "as" simple_intropattern(x) := xlet Q as x; xauto*.
*)
(********************************************************************)
(********************************************************************)
(*-------*)
Ltac xapps_skip_core tt :=
let cont2 tt := instantiate; try xextract; try intro_subst in
let cont1 tt :=
match cfml_get_tag tt with
| tag_apply => xuntag tag_apply; xapp_skip_core
| tag_none_app => xapp_skip_core
| tag_record_new => xapp_skip_core
end
in
match cfml_get_tag tt with
| tag_let => xlet; [ cont1 tt | cont2 tt ]
| tag_seq => xseq; [ cont1 tt | cont2 tt ]
| _ => cont1 tt
end.
Tactic Notation "xapps_skip" :=
xapps_skip_core tt.
(********************************************************************)
(********************************************************************)
(********************************************************************)
(*
let compare_options =
let _r1 = (None = None) in
let _r2 = (Some 3 = None) in
let _r3 = ((Some 3, None) = (None, Some 3)) in
let _r4 = ((Some 3, None) = (Some 3, None)) in
let _r5 = (true = false) in
()
let match_term_when () =
let f x = x + 1 in
match f 3 with
| 0 -> 1
| n when n > 0 -> 2
| _ -> 3
(* captures (Some x, _) or (_, Some x) with x > 0 *)
let match_or_clauses p =
match p with
| (None, None) -> false
| ((Some x, _) | (_, Some x)) when x > 0 -> true
| (Some x, _) | (_, Some x) -> false
*)
(********************************************************************)
......@@ -131,19 +50,36 @@ Tactic Notation "xapps_skip" :=
(********************************************************************)
Notation "'LetPoly' '{' A1 '}' x ':' T ':=' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1, F1 H (fun r => \[P1 r] \* H1))
/\ forall (x:T), (P1 x) -> F2 H1 Q))
(at level 69, A1 ident, x ident, T at level 0, right associativity) : charac.
Notation "'LetPoly' '{' A1 '}' x ':' T ':=' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1, F1 H (fun r => \[@P1 A1 r] \* H1))
/\ forall (x:T), (forall A1, @P1 A1 (@x A1)) -> F2 H1 Q))
(at level 69, A1 ident, x ident, T at level 0, right associativity) : charac.
(********************************************************************)
(* ** Encoding of names *)
Lemma renaming_types : True.
Proof using.
pose renaming_t'_.
pose renaming_t2_. pose C'.
pose renaming_t3_.
pose renaming_t4_.
auto.
Qed.
Lemma renaming_demo_spec :
app renaming_demo [tt] \[] \[= tt].
Proof using.
xcf.
xval.
xval.
xval.
xval.
xval.
xrets.
auto.
Qed.
(********************************************************************)
(* ** Polymorphic let bindings and value restriction *)
Lemma let_poly_p0_spec :
app let_poly_p0 [tt] \[] \[= tt].
......@@ -222,123 +158,73 @@ Proof using.
xcf. xapps. xapps. xapps. xsimpl~.
Qed.
Lemma let_poly_h0_spec :
app let_poly_h0 [tt] \[] \[= 4::nil].
Lemma let_poly_h0_spec : forall A,
app let_poly_h0 [tt] \[] (fun (r:loc) => r ~~> (@nil A)).
Proof using.
xcf. xapps. xapps. xapps. xsimpl~.
xcf. xapps. xret~.
Qed.
(*
let let_poly_h0 () =
let r = ref [] in
r
let let_poly_h1 () =
let g =
let f () = ref [] in
f in
g
let let_poly_h2 () =
let f () : 'a list ref = ref [] in
f
let let_poly_h3 () =
let f () = ref [] in
f()
let let_poly_k1 () =
[]
let let_poly_k2 () =
ref []
let let_poly_r1 () =
let _x = ref [] in
()
let let_poly_r2 () =
let _x = ref [] in
let y = [] in
y
let let_poly_r3 () =
let r =
let x = ref [] in
[] in
r
*)
(********************************************************************)
(********************************************************************)
(********************************************************************)
(*
let compare_options =
let _r1 = (None = None) in
let _r2 = (Some 3 = None) in
let _r3 = ((Some 3, None) = (None, Some 3)) in
let _r4 = ((Some 3, None) = (Some 3, None)) in
let _r5 = (true = false) in
()
let match_term_when () =
let f x = x + 1 in
match f 3 with
| 0 -> 1
| n when n > 0 -> 2
| _ -> 3
(* captures (Some x, _) or (_, Some x) with x > 0 *)
let match_or_clauses p =
match p with
| (None, None) -> false
| ((Some x, _) | (_, Some x)) when x > 0 -> true
| (Some x, _) | (_, Some x) -> false
*)
Lemma let_poly_h1_spec : forall A,
app let_poly_h1 [tt] \[] (fun (f:func) =>
\[ app f [tt] \[] (fun (r:loc) => r ~~> (@nil A)) ]).
Proof using.
xcf. xlet (fun g => \[ app g [tt] \[] (fun (r:loc) => r ~~> (@nil A)) ]).
{ xfun. xrets. xapps. xapps. }
intros Hg. xrets. xapps.
Qed.
Lemma let_poly_h2_spec : forall A,
app let_poly_h2 [tt] \[] (fun (f:func) =>
\[ app f [tt] \[] (fun (r:loc) => r ~~> (@nil A)) ]).
Proof using.
xcf. xfun. xrets. xapps. xapps.
Qed.
(********************************************************************)
(********************************************************************)
(********************************************************************)
Lemma let_poly_h3_spec : forall A,
app let_poly_h3 [tt] \[] (fun (r:loc) => r ~~> (@nil A)).
Proof using.
xcf. xfun. xapps. xapps.
Qed.
Lemma let_poly_k1_spec : forall A,
app let_poly_k1 [tt] \[] \[= @nil A].
Proof using.
xcf. xrets~.
Qed.
Lemma let_poly_k2_spec : forall A,
app let_poly_k2 [tt] \[] (fun (r:loc) => r ~~> (@nil A)).
Proof using.
xcf. xapps.
Qed.
(********************************************************************)
(* ** Encoding of names *)
Lemma let_poly_r1_spec :
app let_poly_r1 [tt] \[] \[= tt].
Proof using.
xcf. xapps. xrets~.
Unshelve. solve_type.
Qed.
Lemma renaming_types : True.
Lemma let_poly_r2_spec : forall A,
app let_poly_r2 [tt] \[] \[= @nil A].
Proof using.
pose renaming_t'_.
pose renaming_t2_. pose C'.
pose renaming_t3_.
pose renaming_t4_.
auto.
Qed.
xcf. xapps. dup 2.
{ xval. xrets~. }
{ xvals. xrets~. }
Unshelve. solve_type.
Qed.
Lemma renaming_demo_spec :
app renaming_demo [tt] \[] \[= tt].
Lemma let_poly_r3_spec : forall A,
app let_poly_r3 [tt] \[] \[= @nil A].
Proof using.
xcf.
xval.
xval.
xval.
xval.
xval.
xrets.
auto.
xcf. xlet_poly_keep (fun A (r:list A) => r = nil).
{ xapps. xrets~. }
intros Hr. xrets. auto.
Qed.
(********************************************************************)
(* ** Top-level values *)
......
......@@ -598,6 +598,88 @@ Notation "'Let' x ':' T ':=' F1 'in' F2" :=
(********************************************************************)
(** LetPoly *)
Notation "'LetPoly' x ':' T ':=' '{' B1 '}' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall B1, F1 H (fun (r:T) => \[P1 r] \* H1))
/\ forall x, (P1 x) -> F2 H1 Q))
(at level 69, x ident, T at level 0, B1 ident, right associativity) : charac.
Notation "'LetPoly' x ':' T ':=' '{' B1 B2 '}' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall B1 B2, F1 H (fun (r:T) => \[P1 r] \* H1))
/\ forall x, (P1 x) -> F2 H1 Q))
(at level 69, x ident, T at level 0, B1 ident, B2 ident, right associativity) : charac.
Notation "'LetPoly' x ':' T ':=' '{' B1 B2 B3 '}' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall B1 B2 B3, F1 H (fun (r:T) => \[P1 r] \* H1))
/\ forall x, (P1 x) -> F2 H1 Q))
(at level 69, x ident, T at level 0, B1 ident, B2 ident, B3 ident, right associativity) : charac.
Notation "'LetPoly' x ':' '{' A1 '}' T ':=' '{' '}' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1, F1 H (fun (r:T) => \[@P1 A1 r] \* H1))
/\ forall x, (forall A1, @P1 A1 (@x A1)) -> F2 H1 Q))
(at level 69, x ident, A1 ident, T at level 0, right associativity) : charac.
Notation "'LetPoly' x ':' '{' A1 '}' T ':=' '{' B1 '}' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1 B1, F1 H (fun (r:T) => \[@P1 A1 r] \* H1))
/\ forall x, (forall A1, @P1 A1 (@x A1)) -> F2 H1 Q))
(at level 69, x ident, A1 ident, T at level 0, B1 ident, F1 at level 0) : charac.
Notation "'LetPoly' x ':' '{' A1 '}' T ':=' '{' B1 B2 '}' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1 B1 B2, F1 H (fun (r:T) => \[@P1 A1 r] \* H1))
/\ forall x, (forall A1, @P1 A1 (@x A1)) -> F2 H1 Q))
(at level 69, x ident, A1 ident, T at level 0, B1 ident, B2 ident, F1 at level 0) : charac.
Notation "'LetPoly' x ':' '{' A1 '}' T ':=' '{' B1 B2 B3 '}' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1 B1 B2 b3, F1 H (fun (r:T) => \[@P1 A1 r] \* H1))
/\ forall x, (forall A1, @P1 A1 (@x A1)) -> F2 H1 Q))
(at level 69, x ident, A1 ident, T at level 0, B1 ident, B2 ident, B3 ident, F1 at level 0)
: charac.
Notation "'LetPoly' x ':' '{' A1 A2 '}' T ':=' '{' '}' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1 A2, F1 H (fun (r:T) => \[@P1 A1 A2 r] \* H1))
/\ forall x, (forall A1 A2, @P1 A1 A2 (@x A1)) -> F2 H1 Q))
(at level 69, x ident, A1 ident, A2 ident, T at level 0, right associativity) : charac.
Notation "'LetPoly' x ':' '{' A1 A2 '}' T ':=' '{' B1 '}' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1 A2 B1, F1 H (fun (r:T) => \[@P1 A1 A2 r] \* H1))
/\ forall x, (forall A1 A2, @P1 A2 A1 (@x A1)) -> F2 H1 Q))
(at level 69, x ident, A1 ident, A2 ident, T at level 0, B1 ident, F1 at level 0) : charac.
Notation "'LetPoly' x ':' '{' A1 A2 '}' T ':=' '{' B1 B2 '}' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1 A2 B1 B2, F1 H (fun (r:T) => \[@P1 A1 A2 r] \* H1))
/\ forall x, (forall A1 A2, @P1 A1 A2 (@x A1)) -> F2 H1 Q))
(at level 69, x ident, A1 ident, A2 ident, T at level 0, B1 ident, B2 ident, F1 at level 0)
: charac.
Notation "'LetPoly' x ':' '{' A1 A2 '}' T ':=' '{' B1 B2 B3 '}' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1 A2 B1 B2 b3, F1 H (fun (r:T) => \[@P1 A1 A2 r] \* H1))
/\ forall x, (forall A1, @P1 A1 A2 (@x A1)) -> F2 H1 Q))
(at level 69, x ident, A1 ident, A2 ident, T at level 0, B1 ident, B2 ident, B3 ident,
F1 at level 0)
: charac.
(* Anomaly on let_poly_r3_spec
Notation "'LetPoly' x ':' '{' A1 '}' T ':=' '{' XB1 '}' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1 XB1, F1 H (fun (r:T) => \[@P1 A1 r] \* H1))
/\ forall x, (forall A1, @P1 A1 (@x A1)) -> F2 H1 Q))
(at level 69, x ident, A1 ident, T at level 0, XB1 ident) : charac.
*)
(********************************************************************)
(** Seq *)
......
......@@ -1391,6 +1391,97 @@ Tactic Notation "xlets" constr(Q) :=
xlet Q; [ | intro_subst ].
*)
(*--------------------------------------------------------*)
(* ** [xlet_poly] *)
(** [xlet_poly] is used to reason on a let node, i.e. on a goal
of the form [(LetPoly {A1} x := F1 in F2) H Q].
Variants:
- [xlet_poly P H] to describe the pure postcondition and
the final state.
- [xlet_poly_keep P] to provide a pure postcondition and
use the current pre-condition as final state.
- [xlet_poly P] to provide a pure postcondition and introduce
a unification variable for the imperative state.