progress_xif

examples/BasicDemos/Demo_proof.v

 Set Implicit Arguments.
-(* LibInt LibWf *).
+(* LibInt LibWf *)
 Require Import CFLib.
 Require Import Demo_ml.
 
-(*Open Scope tag_scope.*)
+Require Import Pervasives_ml. (* optional, improves display of, e.g. [incr] *)
 
+(*Open Scope tag_scope.*)
 
 
 
 
+Lemma if_true_spec : 
+  app if_true [tt] \[] \[= 1].
+Proof using.
+  xcf. xif. xret. xsimpl. auto.
+Qed.
 
-(********************************************************************)
-(* ** Inlined total functions *)
+Lemma if_term_spec :
+  app if_term [tt] \[] \[= 1].
+Proof using.
+  xcf. xfun. xapp. xret. xextracts.
+  xif. xrets~.
+Qed.
 
-Lemma inlined_fun_arith_spec :
-  app inlined_fun_arith [tt] \[] \[= 3].
-Proof using.  
-  xcf.
-  xval.
-  xlet.
-  (* note: division by a possibly-null constant is not inlined *) 
-  xapp_skip.
-  xrets.
-  skip.
+Lemma if_else_if_spec : 
+  app if_else_if [tt] \[] \[= 0].
+Proof using.
+  xcf. xfun (fun f => forall (x:int), app f [x] \[] \[= false]).
+    { xrets~. }
+  xapps. xif. xapps. xif. xrets~.
 Qed.
 
 
+Definition Ref a (v:a) (l:loc) :=  (* TODO: change *)
+  heap_is_single l v.
 
+Notation "l '~~>' v" := (hdata (Ref v) l)
+  (at level 32, no associativity) : heap_scope.
 
-Lemma if_true () =
-   if true then 1 else 0
-Proof using.
-  xcf.
-Qed.
+Notation "'app_keep' f xs H Q" :=
+  (app f xs H%h (Q \*+ H))
+  (at level 80, f at level 0, xs at level 0, H at level 0) : charac.
 
-Lemma if_term () =
-   let f x = true in
-   if f 0 then 1 else 0
-Proof using.
-  xcf.
-Qed.
 
-Lemma if_else_if () =
-   let f x = false in
-   if f 0 then 1 
-   else if f 1 then 2
-   else 0
-Proof using.
-  xcf.
-Qed.
 
-Lemma if_then_no_else b =
-  let r = ref 0 in
-  if b
-     then incr r; 
-  !r
+Parameter ref_spec : forall a (v:a),
+  app ref [v] \[] (fun l => l ~~> v).
+
+Parameter get_spec : forall a (v:a) l,
+  app_keep get [l] (l ~~> v) \[= v].
+(* Print get_spec. *)
+(* keep (app get [l]) (l ~~> v) \[= v].*)
+
+Parameter set_spec : forall a (v w:a) l,
+  app set [l w] (l ~~> v) (# l ~~> w).
+
+Parameter incr_spec : forall (n:int) l,
+  app incr [l] (l ~~> n) (# l ~~> (n+1)).
+
+Parameter decr_spec : forall (n:int) l,
+  app decr [l] (l ~~> n) (# l ~~> (n+1)).
+
+
+Hint Extern 1 (RegisterSpec ref) => Provide ref_spec.
+Hint Extern 1 (RegisterSpec get) => Provide get_spec.
+Hint Extern 1 (RegisterSpec set) => Provide set_spec.
+Hint Extern 1 (RegisterSpec incr) => Provide incr_spec.
+Hint Extern 1 (RegisterSpec decr) => Provide decr_spec.
+
+
+
+
+
+Notation "`! l" := (App infix_emark_ l;)
+  (at level 69, no associativity, format "`! l") : machine_op_scope.
+
+
+Lemma if_then_no_else_spec : forall (b:bool),
+  app if_then_no_else [b] \[] \[= 1].
 Proof using.
-  xcf.
+  xcf. xapp. dup 3.
+  { xseq. xif. { xapp. } { xrets. skip. (* stuck *) } skip. } 
+  { xseq....
+
+  (* TODO: raise error message on xif *)
 Qed.
 
+
+
 (********************************************************************)
 (********************************************************************)
 (********************************************************************)
@@ -364,6 +393,29 @@ Proof using.
 Qed.
 
 
+(********************************************************************)
+(* ** Inlined total functions *)
+
+Lemma inlined_fun_arith_spec :
+  app inlined_fun_arith [tt] \[] \[= 3].
+Proof using.  
+  xcf.
+  xval.
+  xlet.
+  (* note: division by a possibly-null constant is not inlined *) 
+  xapp_skip.
+  xrets.
+  skip.
+Qed.
+
+Lemma inlined_fun_other_spec : forall (n:int),
+  app inlined_fun_others [n] \[] \[= n+1].
+Proof using.
+  xcf. xret. xsimpl. simpl. auto.
+Qed.
+
+
+
 
 (********************************************************************)
 (********************************************************************)

generator/renaming.ml

@@ -101,6 +101,10 @@ let find_builtin_constructor p =
 (** Fully-applied "inlined primitive" are translated directly as a 
     Coq application, and does not involve the "AppReturns" predicate. *)
 
+
+(* code for division and modulo, which have arity 2 but are treated
+   specially for the cases where the second argument is a non-zero constant *)
+
 let primitive_special = -1
 
 (* for the mli file:
@@ -120,11 +124,11 @@ let inlined_primitives_table =
    "Pervasives.not", (1, "LibBool.neg");
    "Pervasives.fst", (1, "(@Coq.Init.Datatypes.fst _ _)");
    "Pervasives.snd", (1, "(@Coq.Init.Datatypes.snd _ _)");
-   "Pervasives.pred", (primitive_special, "CFML.CFHeader.pred");
-   "Pervasives.succ", (primitive_special, "CFML.CFHeader.succ");
+   "Pervasives.pred", (1, "CFML.CFHeader.pred");
+   "Pervasives.succ", (1, "CFML.CFHeader.succ");
    "Pervasives./", (primitive_special, "CFML.CFHeader.int_div");
    "Pervasives.mod", (primitive_special, "CFML.CFHeader.int_mod");
-   "Pervasives.ignore", (primitive_special, "CFML.CFHeader.ignore");
+   "Pervasives.ignore", (1, "(@CFML.CFHeader.ignore _)");
    "Pervasives.&&", (2, "LibBool.and");
    "Pervasives.||", (2, "LibBool.or");
       (* TODO (but only for some types):

lib/coq/CFHeader.v

+Set Implicit Arguments.
 Require Export CFPrint.
 
 Require Coq.ZArith.BinInt.

lib/coq/CFTactics.v

@@ -2141,7 +2141,11 @@ Tactic Notation "xspec" :=
 (** [xapp] applies to goals of the form [app f xs H Q]. 
     It looks for a specification for [f] using [xspec],
     and applies it to the goal using [xapply].
-    [xapp_spec P] can be used to 
+    [xapp_spec P] can be used to provide a specification.
+    
+    The tactic also applies to goals starting with [LetApp] or [SeqApp].
+    In this case, it applies [xlet]/[xseq] first, and, in the
+    continuation branch, it calls [xextract].
 
     Variants:
 
@@ -2158,9 +2162,10 @@ Tactic Notation "xspec" :=
 
     - [xapp as x] is a shorthand for [xlet as x; xapp].
 
-    - [xapps] is a shorthand for either [xlet as x; xapp; try intro_subst]]
-      or [xseq; xapp; try intro_subst], or [xapp],
-      depending on the tag of the goal.
+    - [xapps] applies to goal starting with a [LetApp] or [SeqApp]
+      characteristic formula. It calls [xseq]/[xlet], then
+      calls [xapp], then in the continuation branch it calls [xextract] 
+      and attempts to substitute the first hypothesis using [intro_subst].
 
     Other variants:
     - [xapp_spec P] for providing specification.
@@ -2774,7 +2779,7 @@ Ltac xcf_core_app f :=
   xcf_core_app_exploit H. (* todo: might need sapply here *)
 
 Ltac xcf_fallback f :=
-  idtac "Warning: could not exploit the specification; if you intend to use the specification manually, call [xcf_show as S].";
+  idtac "Warning: could not exploit the specification; maybe the types don't match; if you intend to use the specification manually, call [xcf_show as S].";
   xcf_find f; 
   let Sf := fresh "Spec" in 
   intros Sf.