Skip to content

GitLab

Commit 011ac52a authored by charguer's avatar charguer
Browse files

xpat

parent 01ae4e48
Hide whitespace changes
Inline Side-by-side
Showing with 346 additions and 186 deletions
examples/BasicDemos/Demo.ml
View file @ 011ac52a
......@@ -12,7 +12,7 @@ open Pervasives
(********************************************************************)
(* ** Return *)
let ret_unit () =
let ret_unit x =
()
let ret_int () =
......@@ -28,11 +28,10 @@ let ret_poly () =
(********************************************************************)
(* ** Sequence *)
let seq_noop () =
let f x = () in
f 1;
f 2;
f 3
let seq_ret_unit () =
ret_unit 1;
ret_unit 2;
ret_unit 3
(********************************************************************)
......@@ -204,7 +203,7 @@ let match_nested () =
let l = [ (1,1); (0,0); (2,2) ] in
match l with
| _::(0,0)::q -> q
| _ -> []
| _ -> [(2,2)]
(* not yet supported when clauses
let match_term_when () =
......
examples/BasicDemos/Demo_proof.v
View file @ 011ac52a
......@@ -3,51 +3,124 @@ Require Import LibTactics CFHeaps CFLib LibInt LibWf Demo_ml.
Open Scope tag_scope.
(********************************************************************)
(* ** Return *)
(* ** Let-pattern *)
(* includes deoms of [xret] variants *)
Lemma ret_unit_spec :
app ret_unit [tt] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)
Lemma let_pattern_pair_int () =
let (x,y) = (3,4) in
x
Proof using.
xcf. dup 5.
xret. xsimpl. auto.
(* demos *)
xrets. auto.
xrets*.
xret_no_gc. xsimpl. auto.
xret_no_clean. xsimpl*.
xcf.
Qed.
Lemma ret_int_spec :
app ret_int [tt] \[] \[= 3].
Proof using. xcf. xrets*. Qed.
Lemma let_pattern_pair_int_wildcard () =
let (x,_) = (3,4) in
x
Proof using.
xcf.
Qed.
Lemma ret_int_pair_spec :
app ret_int_pair [tt] \[] \[= (3,4)].
Proof using. xcf. xrets*. Qed.
Lemma ret_poly_spec : forall A,
app ret_poly [tt] \[] \[= @nil A].
Proof using. xcf. xrets*. Qed.
(********************************************************************)
(* ** Let-term *)
Lemma let_term_nested_id_calls () =
let f x = x in
let a = f (f (f 2)) in
a
Proof using.
xcf.
Qed.
Lemma let_term_nested_pairs_calls () =
let f x y = (x,y) in
let a = f (f 1 2) (f 3 (f 4 5)) in
a
Proof using.
xcf.
Qed.
(********************************************************************)
(* ** Let-function *)
Lemma let_fun_const () =
let f () = 3 in
f()
Proof using.
xcf.
Qed.
Lemma let_fun_poly_id () =
let f x = x in
f 3
Proof using.
xcf.
Qed.
Lemma let_fun_poly_pair_homogeneous () =
let f (x:'a) (y:'a) = (x,y) in
f 3 3
Proof using.
xcf.
Qed.
Lemma let_fun_on_the_fly () =
(fun x f -> f x) 3 (fun x -> x+1)
Proof using.
xcf.
Qed.
(********************************************************************)
(********************************************************************)
(*
(* ** Sequence *)
Axiom ret_unit_spec :
app ret_unit [tt] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)
Proof using.
Lemma seq_noop_spec :
app seq_noop [tt] \[] \[= tt].
Proof using.
xcf.
xfun.
xret.
Qed.
(********************************************************************)
(********************************************************************)
(********************************************************************)
(********************************************************************)
(* ** Top-level values *)
(* includes demos of [xcf] variants *)
Lemma top_val_int_spec :
top_val_int = 5.
Proof using.
......@@ -75,112 +148,122 @@ Lemma top_val_poly_list_pair_spec : forall A B,
Proof using. xcf*. Qed.
(********************************************************************)
(* ** Sequence *)
(* ** Return *)
Lemma seq_noop () =
let f x = () in
f 1;
f 2;
f 3
Lemma ret_unit_spec :
app ret_unit [tt] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)
Proof using.
xcf.
xcf. dup 5.
xret. xsimpl. auto.
(* demos *)
xrets. auto.
xrets*.
xret_no_gc. xsimpl. auto.
xret_no_clean. xsimpl*.
Qed.
Lemma ret_int_spec :
app ret_int [tt] \[] \[= 3].
Proof using. xcf. xrets*. Qed.
Lemma ret_int_pair_spec :
app ret_int_pair [tt] \[] \[= (3,4)].
Proof using. xcf. xrets*. Qed.
(********************************************************************)
(* ** Let-value *)
Lemma let_val_int () =
let x = 3 in
x
Proof using.
xcf.
Qed.
Lemma let_val_pair_int () =
let x = (3,4) in
x
Proof using.
xcf.
Qed.
Lemma ret_poly_spec : forall A,
app ret_poly [tt] \[] \[= @nil A].
Proof using. xcf. xrets*. Qed.
Lemma let_val_poly () =
let _x = [] in
3
Proof using.
xcf.
Qed.
(********************************************************************)
(* ** Let-pattern *)
(* ** Let-value *)
Lemma let_pattern_pair_int () =
let (x,y) = (3,4) in
x
Lemma let_val_int_spec :
app let_val_int [tt] \[] \[= 3].
Proof using.
xcf.
xcf. dup 7.
xval. xrets~.
(* demos *)
xval as r. xrets~.
xval as r Er. xrets~.
xvals. xrets~.
xval_st (= 3). auto. xrets~.
xval_st (= 3) as r. auto. xrets~.
xval_st (= 3) as r Er. auto. xrets~.
Qed.
Lemma let_pattern_pair_int_wildcard () =
let (x,_) = (3,4) in
x
Lemma let_val_pair_int_spec :
app let_val_pair_int [tt] \[] \[= (3,4)].
Proof using. xcf. xvals. xrets*. Qed.
Lemma let_val_poly_spec :
app let_val_poly [tt] \[] \[= 3].
Proof using.
xcf.
xcf. dup 3.
xval. xret. xsimpl. auto.
xval as r. xrets~.
xvals. xrets~.
Qed.
(********************************************************************)
(* ** Let-term *)
(* ** Pattern-matching *)
Lemma let_term_nested_id_calls () =
let f x = x in
let a = f (f (f 2)) in
a
Proof using.
xcf.
Lemma match_pair_as_spec :
app match_pair_as [tt] \[] \[= (4,(3,4))].
Proof using.
xcf. dup 8.
{ xmatch. xrets*. }
{ xmatch_subst_alias. xrets*. }
{ xmatch_no_alias. xalias. xalias as L. skip. }
{ xmatch_no_cases. dup 5.
{ xcase_no_simpl.
{ dup 3.
{ xalias. xalias. xret. xsimpl. xauto*. }
{ xalias as u U.
xalias as v. skip. }
{ xalias_subst. xalias_subst. skip. } }
{ xdone. } }
{ xcase_no_simpl as E. skip. skip. }
{ xcase_no_intros. intros x y E. skip. intros F. skip. }
{ xcase. skip. skip. }
{ xcase as C. skip. skip.
(* note: inversion got rid of C *)
} }
{ xmatch_no_simpl_no_alias. skip. }
{ xmatch_no_simpl_subst_alias. skip. }
{ xmatch_no_intros. skip. skip. }
{ xmatch_no_simpl. inverts C. skip. }
Qed.
Lemma match_nested_spec :
app match_nested [tt] \[] \[= (2,2)::nil].
Proof using.
xcf. xval. dup 3.
{ xmatch_no_simpl.
{ xrets~. }
{ false. (* note: [xrets] would produce a ununified [hprop].
caused by [tryfalse] in [hextract_cleanup]. TODO: avoid this. *) } }
{ xmatch.
xrets~.
(* second case is killed by [xcase_post] *) }
{ xmatch_no_intros. skip. skip. }
Qed.
Lemma let_term_nested_pairs_calls () =
let f x y = (x,y) in
let a = f (f 1 2) (f 3 (f 4 5)) in
a
Proof using.
xcf.
Qed.
(********************************************************************)
(* ** Let-function *)
(********************************************************************)
(********************************************************************)
Lemma let_fun_const () =
let f () = 3 in
f()
Proof using.
xcf.
Qed.
(*
Lemma let_fun_poly_id () =
let f x = x in
f 3
Proof using.
xcf.
Qed.
Lemma let_fun_poly_pair_homogeneous () =
let f (x:'a) (y:'a) = (x,y) in
f 3 3
Proof using.
xcf.
Qed.
Lemma let_fun_on_the_fly () =
(fun x f -> f x) 3 (fun x -> x+1)
Proof using.
xcf.
Qed.
(********************************************************************)
......@@ -341,33 +424,6 @@ Qed.
(*
(* ** Pattern-matching *)
Lemma match_pair_as () =
match (3,4) with (a, (b as c)) as p -> (c,p)
Proof using.
xcf.
Qed.
Lemma match_nested () =
let l = [ (1,1); (0,0); (2,2) ] in
match l with
| _::(0,0)::q -> q
| _ -> []
Proof using.
xcf.
Qed.
(* not yet supported when clauses
Lemma match_term_when () =
let f x = x + 1 in
match f 3 with
| 0 -> 1
| n when n > 0 -> 2
| _ -> 3
*)
(********************************************************************)
(* ** Fatal Exceptions *)
......
lib/coq/CFPrint.v
View file @ 011ac52a
......@@ -107,11 +107,11 @@ Notation "'!Ret' P" := (tag tag_ret (local P))
(at level 69) : tag_scope.
Notation "'!App' P" := (tag tag_apply P)
(at level 95) : tag_scope.
Notation "'!LetVal' P" := (tag tag_let_val (local P))
Notation "'!Val' P" := (tag tag_let_val (local P))
(at level 95) : tag_scope.
Notation "'!LetFun' P" := (tag tag_let_fun (local P))
Notation "'!Fun' P" := (tag tag_let_fun (local P))
(at level 95) : tag_scope.
Notation "'!LetTrm' P" := (tag tag_let_trm (local P))
Notation "'!Let' P" := (tag tag_let_trm (local P))
(at level 95) : tag_scope.
Notation "'!Body' P" := (tag tag_body P)
(at level 95) : tag_scope.
......@@ -203,7 +203,7 @@ Notation "'App' f x1 x2 x3 x4 x5 ;" :=
Notation "'LetApp' x ':=' f xs 'in' F2" :=
(!LetTrm (fun H Q => exists Q1, App_ f xs H Q1 /\ forall x, F2 (Q1 x) Q))
(!Let (fun H Q => exists Q1, App_ f xs H Q1 /\ forall x, F2 (Q1 x) Q))
(at level 69, x ident, f at level 0, xs at level 0,
right associativity,
format "'[v' '[' 'LetApp' x ':=' f xs 'in' ']' '/' '[' F2 ']' ']'") : charac.
......@@ -245,23 +245,23 @@ Notation "'SeqApp' f xs ;; F2" :=
(** LetVal *)
Notation "'LetVal' x ':=' V 'in' F" :=
(!LetVal (fun H Q => forall x, x = V -> F H Q))
(!Val (fun H Q => forall x, x = V -> F H Q))
(at level 69, x ident) : charac.
Notation "'LetVal' [ A1 ] x ':=' V 'in' F" :=
(!LetVal (fun H Q => forall x, x = (fun (A1:Type) => V) -> F H Q))
(!Val (fun H Q => forall x, x = (fun (A1:Type) => V) -> F H Q))
(at level 69, x ident, A1 ident) : charac.
Notation "'LetVal' [ A1 A2 ] x ':=' V 'in' F" :=
(!LetVal (fun H Q => forall x, x = (fun (A1 A2:Type) => V) -> F H Q))
(!Val (fun H Q => forall x, x = (fun (A1 A2:Type) => V) -> F H Q))
(at level 69, x ident, A1 ident, A2 ident) : charac.
Notation "'LetVal' [ A1 A2 A3 ] x ':=' V 'in' F" :=
(!LetVal (fun H Q => forall x, x = (fun (A1 A2 A3:Type) => V) -> F H Q))
(!Val (fun H Q => forall x, x = (fun (A1 A2 A3:Type) => V) -> F H Q))
(at level 69, x ident, A1 ident, A2 ident, A3 ident) : charac.
Notation "'LetVal' [ A1 A2 A3 A4 ] x ':=' V 'in' F" :=
(!LetVal (fun H Q => forall x, x = (fun (A1 A2 A3 A4:Type) => V) -> F H Q))
(!Val (fun H Q => forall x, x = (fun (A1 A2 A3 A4:Type) => V) -> F H Q))
(at level 69, x ident, A1 ident, A2 ident, A3 ident, A4 ident) : charac.
......@@ -270,91 +270,181 @@ Notation "'LetVal' [ A1 A2 A3 A4 ] x ':=' V 'in' F" :=
Notation "'Body' f x1 '=>' K" :=
(!Body ( curried 1 f
/\ (forall x1 B H Q, K H Q -> app f [x1] H Q)))
/\ (forall x1 H Q, K H Q -> app f [x1] H Q)))
(at level 0, f at level 0, x1 ident) : charac.
Notation "'Body' f x1 x2 '=>' K" :=
(!Body ( curried 2 f
/\ (forall x1 x2 B H Q, K H Q -> app f [x1 x2] H Q)))
/\ (forall x1 x2 H Q, K H Q -> app f [x1 x2] H Q)))
(at level 0, f at level 0, x1 ident, x2 ident) : charac.
Notation "'Body' f x1 x2 x3 '=>' K" :=
(!Body ( curried 3 f
/\ (forall x1 x2 x3 B H Q, K H Q -> app f [x1 x2 x3] H Q)))
/\ (forall x1 x2 x3 H Q, K H Q -> app f [x1 x2 x3] H Q)))
(at level 0, f at level 0, x1 ident, x2 ident, x3 ident) : charac.
Notation "'Body' f x1 x2 x3 x4 '=>' K" :=
(!Body ( curried 4 f
/\ (forall x1 x2 x3 x4 B H Q, K H Q -> app f [x1 x2 x3 x4] H Q)))
/\ (forall x1 x2 x3 x4 H Q, K H Q -> app f [x1 x2 x3 x4] H Q)))
(at level 0, f at level 0, x1 ident, x2 ident, x3 ident, x4 ident) : charac.
Notation "'Body' f [ A1 ] x1 '=>' K" :=
(!Body ( curried 1 f
/\ (forall A1 x1 B H Q, K H Q -> app f [x1] H Q)))
/\ (forall A1 x1 H Q, K H Q -> app f [x1] H Q)))
(at level 0, f at level 0, x1 ident, A1 ident) : charac.
Notation "'Body' f [ A1 ] x1 x2 '=>' K" :=
(!Body ( curried 2 f
/\ (forall A1 x1 x2 B H Q, K H Q -> app f [x1 x2] H Q)))
/\ (forall A1 x1 x2 H Q, K H Q -> app f [x1 x2] H Q)))
(at level 0, f at level 0, x1 ident, x2 ident, A1 ident) : charac.
Notation "'Body' f [ A1 ] x1 x2 x3 '=>' K" :=
(!Body ( curried 3 f
/\ (forall A1 x1 x2 x3 H Q, K H Q -> app f [x1 x2 x3] H Q)))
(at level 0, f at level 0, x1 ident, x2 ident, x3 ident, A1 ident) : charac.
Notation "'Body' f [ A1 ] x1 x2 x3 x4 '=>' K" :=
(!Body ( curried 4 f
/\ (forall A1 x1 x2 x3 x4 H Q, K H Q -> app f [x1 x2 x3 x4] H Q)))
(at level 0, f at level 0, x1 ident, x2 ident, x3 ident, x4 ident, A1 ident) : charac.
Notation "'Body' f [ A1 A2 ] x1 '=>' K" :=
(!Body ( curried 1 f
/\ (forall A1 A2 x1 B H Q, K H Q -> app f [x1] H Q)))
/\ (forall A1 A2 x1 H Q, K H Q -> app f [x1] H Q)))
(at level 0, f at level 0, x1 ident, A1 ident, A2 ident) : charac.
Notation "'Body' f [ A1 A2 ] x1 x2 '=>' K" :=
(!Body ( curried 2 f
/\ (forall A1 A2 x1 x2 B H Q, K H Q -> app f [x1 x2] H Q)))
/\ (forall A1 A2 x1 x2 H Q, K H Q -> app f [x1 x2] H Q)))
(at level 0, f at level 0, x1 ident, x2 ident, A1 ident, A2 ident) : charac.
Notation "'Body' f [ A1 A2 ] x1 x2 x3 '=>' K" :=
(!Body ( curried 3 f
/\ (forall A1 A2 x1 x2 x3 H Q, K H Q -> app f [x1 x2 x3] H Q)))
(at level 0, f at level 0, x1 ident, x2 ident, x3 ident, A1 ident, A2 ident) : charac.
Notation "'Body' f [ A1 A2 ] x1 x2 x3 x4 '=>' K" :=
(!Body ( curried 4 f
/\ (forall A1 A2 x1 x2 x3 x4 H Q, K H Q -> app f [x1 x2 x3 x4] H Q)))
(at level 0, f at level 0, x1 ident, x2 ident, x3 ident, x4 ident, A1 ident, A2 ident) : charac.
Notation "'Body' f [ A1 A2 A3 ] x1 '=>' K" :=
(!Body ( curried 1 f
/\ (forall A1 A2 A3 x1 H Q, K H Q -> app f [x1] H Q)))
(at level 0, f at level 0, x1 ident, A1 ident, A2 ident, A3 ident) : charac.
Notation "'Body' f [ A1 A2 A3 ] x1 x2 '=>' K" :=
(!Body ( curried 2 f
/\ (forall A1 A2 A3 x1 x2 H Q, K H Q -> app f [x1 x2] H Q)))
(at level 0, f at level 0, x1 ident, x2 ident, A1 ident, A2 ident, A3 ident) : charac.
Notation "'Body' f [ A1 A2 A3 ] x1 x2 x3 '=>' K" :=
(!Body ( curried 3 f
/\ (forall A1 A2 A3 x1 x2 x3 H Q, K H Q -> app f [x1 x2 x3] H Q)))
(at level 0, f at level 0, x1 ident, x2 ident, x3 ident, A1 ident, A2 ident, A3 ident) : charac.
Notation "'Body' f [ A1 A2 A3 ] x1 x2 x3 x4 '=>' K" :=
(!Body ( curried 4 f
/\ (forall A1 A2 A3 x1 x2 x3 x4 H Q, K H Q -> app f [x1 x2 x3 x4] H Q)))
(at level 0, f at level 0, x1 ident, x2 ident, x3 ident, x4 ident, A1 ident, A2 ident, A3 ident) : charac.
(********************************************************************)
(** LetFun *)
(* [LetFunc] is an auxiliary notation used by [LetFun] *)
Notation "'LetFunc' f ':=' F1 'in' F2" :=
(!LetFun (fun H Q => forall f, exists P1,
(* [Func] is an auxiliary notation used by [LetFun] *)
Notation "'Func' f ':=' F1 'in' F2" :=
(!Fun (fun H Q => forall f, exists P1,
(F1 -> P1 f) /\ (P1 f -> F2 H Q)))
(at level 69, f ident, only parsing) : charac.
(at level 69, f ident) : charac. (* , only parsing *)
Notation "'LetFun' f x1 ':=' K 'in' F" :=
(LetFunc f := (Body f x1 => K) in F)
Notation "'Fun' f x1 ':=' K 'in' F" :=
(Func f := (Body f x1 => K) in F)
(at level 69, f ident, x1 ident) : charac.
Notation "'LetFun' f x1 x2 ':=' K 'in' F" :=
(LetFunc f := (Body f x1 x2 => K) in F)
Notation "'Fun' f x1 x2 ':=' K 'in' F" :=
(Func f := (Body f x1 x2 => K) in F)
(at level 69, f ident, x1 ident, x2 ident) : charac.
Notation "'LetFun' f x1 x2 x3 ':=' K 'in' F" :=
(LetFunc f := (Body f x1 x2 x3 => K) in F)
Notation "'Fun' f x1 x2 x3 ':=' K 'in' F" :=
(Func f := (Body f x1 x2 x3 => K) in F)
(at level 69, f ident, x1 ident, x2 ident, x3 ident) : charac.
Notation "'LetFun' f x1 x2 x3 x4 ':=' K 'in' F" :=
(LetFunc f := (Body f x1 x2 x3 x4 => K) in F)
Notation "'Fun' f x1 x2 x3 x4 ':=' K 'in' F" :=
(Func f := (Body f x1 x2 x3 x4 => K) in F)
(at level 69, f ident, x1 ident