Commit 6fd5902a authored by charguer's avatar charguer

xgc

parent c8ee1439
......@@ -9,36 +9,36 @@ MAJOR TODAY
MAJOR NEXT
- record single field and array single cell notation
Notation "x `. f '~>' S" :=
Notation "x `[ i ] '~>' S" :=
- record with
- realize array specification using single-cell array specifications
- when clauses
- partial application
- partial/over application
- xabstract => reimplement and rename as xgen
- record with
- when clauses
MAJOR NEXT NEXT
- implement the work around for type abbreviations:
type typerecb1 = | Typerecb_1 of typerecb2
and typerecb2 = typerecb1 list
- record single field and array single cell notation
Notation "x `. f '~>' S" :=
Notation "x `[ i ] '~>' S" :=
- support float
- realize array specification using single-cell array specifications
- xfocus
MAJOR POSTPONED
- support float
- add support for pure records
=> need type information for normalization
=> how to shared typed/untyped AST
- implement the work around for type abbreviations:
type typerecb1 = | Typerecb_1 of typerecb2
and typerecb2 = typerecb1 list
SANITY
......
......@@ -437,6 +437,21 @@ let order_array () =
[| g() ; f() |]
(********************************************************************)
(* ** References *)
let ref_gc () =
let r1 = ref 1 in
let r2 = ref 1 in
let r3 = ref 1 in
let r4 = ref 1 in
let x =
let r5 = ref 2 in
!r5
in
x + !r1
(********************************************************************)
(* ** Arrays *)
......
......@@ -10,6 +10,44 @@ Require Import Stdlib.
(********************************************************************)
(* ** While loops *)
Lemma while_decr () =
let n = ref 3 in
let c = ref 0 in
while !n > 0 do
incr c;
decr n;
done;
!c
Proof using.
xcf.
Qed.
Lemma while_false () =
while false do () done
Proof using.
xcf.
Qed.
(********************************************************************)
(* ** For loops *)
Lemma for_incr () =
let n = ref 0 in
for i = 1 to 10 do
incr n;
done;
!n
(* "for .. down to" not yet supported *)
Proof using.
xcf.
Qed.
(********************************************************************)
(********************************************************************)
......@@ -360,22 +398,6 @@ Qed.
(********************************************************************)
(* ** Type annotations *)
Ltac xval_anonymous_impl tt ::=
xval_pre tt;
intro;
let x := get_last_hyp tt in
revert x;
let Hx := fresh "P" x in
intros x Hx;
xtag_goal.
Lemma annot_let_spec :
app annot_let [tt] \[] \[= 3].
Proof using.
......@@ -717,6 +739,28 @@ Qed.
(********************************************************************)
(* ** Reference and garbage collection *)
Lemma ref_gc_spec :
app ref_gc [tt] \[] \[= 3].
Proof using.
xcf.
xapp.
xapp.
xapp.
xapp.
dup 4.
{ xgc (r3 ~~> 1). skip. }
{ xgc r3. skip. }
{ xgc_but r1. skip. }
{ xlet (fun x => \[x = 2] \* r1 ~~> 1).
{ xapp. xapp. xsimpl~. } (* auto GC on r5 *)
{ intro_subst. xapps. xrets~. } (* auto GC on r1 *)
}
Qed.
(********************************************************************)
(* ** Records *)
......@@ -904,72 +948,3 @@ Qed.
*)
(********************************************************************)
(********************************************************************)
(********************************************************************)
(* TODO: xgc demo *)
(********************************************************************)
(********************************************************************)
(********************************************************************)
(*
(********************************************************************)
(* ** While loops *)
Lemma while_decr () =
let n = ref 3 in
let c = ref 0 in
while !n > 0 do
incr c;
decr n;
done;
!c
Proof using.
xcf.
Qed.
Lemma while_false () =
while false do () done
Proof using.
xcf.
Qed.
(********************************************************************)
(* ** For loops *)
Lemma for_incr () =
let n = ref 0 in
for i = 1 to 10 do
incr n;
done;
!n
(* "for .. down to" not yet supported *)
Proof using.
xcf.
Qed.
(* TODO: include demo of xpost (fun r =>\[r = 3]). *)
(*************************************************************************)
(*************************************************************************)
*)
\ No newline at end of file
......@@ -336,6 +336,19 @@ End IntrovTest.
(* ** Shared auxiliary functions *)
(*--------------------------------------------------------*)
(* ** Tools for manipulating pre-conditions *)
(** [cfml_find_hprop_at X] returns the hprop [X ~> T] that
appears in the pre-condition. *)
Ltac cfml_find_hprop_at X :=
match goal with |- ?R ?H ?Q =>
match H with context [ X ~> ?T ] =>
constr:(X ~> T) end end.
(*--------------------------------------------------------*)
(* ** Tools for manipulating post-conditions *)
......@@ -747,22 +760,40 @@ Tactic Notation "xextract" "as" simple_intropattern(I1) simple_intropattern(I2)
[xgc_post] applied to the goal [F H Q] replaces the goal
with [F H ?Q'] and [Q' ===> Q \*+ \GC], which allows to
perform garbage collection.
[xgc x] is same as [xgc (x ~> T)] where [T] is read in the pre-condition.
TODO: [xgc] with several arguments, or a list of arguments.
*)
Ltac xgc_remove_core H :=
xextract_check_not_needed tt;
Ltac xgc_remove_hprop H :=
eapply (@local_gc_pre_on H);
[ try xlocal
| hsimpl
| xtag_goal ].
Ltac xgc_keep_core H :=
Ltac xgc_remove_core X :=
xextract_check_not_needed tt;
match type of X with
| hprop => xgc_remove_hprop X
| _ => let E := cfml_find_hprop_at X in
xgc_remove_hprop E
end.
Ltac xgc_keep_hprop H :=
eapply (@local_gc_pre H);
[ try xlocal
| hsimpl
| xtag_goal ].
Ltac xgc_keep_core X :=
xextract_check_not_needed tt;
match type of X with
| hprop => xgc_keep_hprop X
| _ => let E := cfml_find_hprop_at X in
xgc_keep_hprop E
end.
Ltac xgc_post_core :=
xextract_check_not_needed tt;
eapply local_gc_post;
......
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