Commit 5773f39d authored by charguer's avatar charguer

fixes

parent 544ae44a
Set Implicit Arguments.
Record dynamic := dyn {
dyn_type : Type;
dyn_value : dyn_type }.
Definition loc := nat.
Definition heap := loc -> dynamic -> Prop.
(* isomorphic to:
Definition heap := loc -> option dynamic.
*)
Definition hprop := heap -> Prop.
Definition single id val : hprop :=
fun (h:heap) =>
(h = (fun id' val' => id = id' /\ val = val')).
Definition pure (P:Prop) : hprop :=
fun (h:heap) =>
(h = (fun id' val' => False)) /\ P.
Definition star (H1 H2:hprop) : hprop :=
fun (h:heap) => H1 h /\ H2 h. (* should be star def *)
Definition heap_is_pack A (Hof : A -> hprop) : hprop :=
fun h => exists x, Hof x h.
Notation "'Hexists' ( x1 : T ) , H" := (heap_is_pack (fun x1 : T => H))
(at level 39, x1 ident, H at level 200).
Definition hpropsyntax := nat.
Parameter hpropsyntax_interp : hpropsyntax -> hprop.
Inductive lock_type : Type :=
| lock : hpropsyntax -> lock_type.
Definition islock id (H:hprop) : hprop :=
Hexists (HS:hpropsyntax),
star (pure (H = hpropsyntax_interp HS))
(single id (dyn (lock HS))).
Definition id0 := 0.
Definition H0 : hprop :=
Hexists (H:hprop), islock id0 H.
Set Implicit Arguments.
Record dynamic := dyn {
dyn_type : Type;
dyn_value : dyn_type }.
Definition loc := nat.
Definition heap := loc -> dynamic -> Prop.
(* isomorphic to:
Definition heap := loc -> option dynamic.
*)
Definition hprop := heap -> Prop.
Definition single id val : hprop :=
fun (h:heap) =>
(h = (fun id' val' => id = id' /\ val = val')).
(* if using Type, then H1 raises universe inconsistency *)
Inductive Lock : Prop :=
| Lock_intro : hprop -> Lock.
Definition id0 := 0.
Definition H0 : hprop := single id0 (dyn 3).
Definition id1 := 1.
Definition H1 : hprop := single id1 (dyn (Lock_intro H0)).
\ No newline at end of file
let f x = x
\ No newline at end of file
let f x = x
open Aux (* required for cfml to do the require in Coq, in the current implementation *)
(* open Aux (* required for cfml to do the require in Coq, in the current implementation *) *)
open NullPointers
let g x = Aux.f x
......
......@@ -36,7 +36,7 @@ let lift_ident_name id =
let name = Ident.name id in
if name = "OkaStream" then "CFPrim" else (* TODO : improve *)
if Ident.persistent id
then name ^ "_ml"
then (Printf.printf "require %s\n" name; name ^ "_ml")
else "ML" ^ name
let rec lift_full_path = function
......
Set Implicit Arguments.
Require Import LibTactics.
Require Import Omega.
(*****************************************************************************)
(*****************************************************************************)
......@@ -348,7 +350,7 @@ Definition sound (c:com) (R:Formula) :=
Lemma sound_local : forall c R,
sound c R -> sound c (local R).
Proof.
introv M Wea Pre.
introv M. introv Wea Pre.
destruct (Wea _ Pre) as (P'&Q'&Pre'&Main&Post').
forwards* (st'&?&?): M.
Qed.
......@@ -615,7 +617,7 @@ Proof.
clears st. destruct n as [|n']. false.
xseq (fun st => st Z = n' /\ st Y = k * (S n')).
xseq (fun st => st Z = S n' /\ st Y = k * (S n')).
xass; auto*.
xass; autos*.
xass; auto. destruct Pst. omega.
unfold real_fact. fold (real_fact n').
rewrite Mult.mult_assoc. apply~ H.
......
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