Library CFML.CFPrint

Set Implicit Arguments.
Require Import CFHeaps.
Require Export CFApp.

The idea is to tag nodes of the formulae with identity predicates carrying a tag information, that indicates the language construct from which the piece of characteristic formula has been generated.

Grammar of tags

Tag carrier, as an identity function

Definition tag (t:tag_type) (A:Type) (P:A) := P.

Arguments tag t [A].

xtag_add T adds the tag T to the head of the goal

Ltac xtag_add T :=
  match goal with |- ?G =>
  match get_fun_arg G with (?G1,?Q) =>
  match get_fun_arg G1 with (?F,?H) =>
    change G with ((@tag T _ F) H Q) end end end.

xtag_pre_post adds the tag tag_goal to the characteristic formula at the head of the goal.

If there are forall in the head, they are introduced, then regeneralized (this feature is useful for the implementation of xpull, for example).
It does nothing if there is no such formula (i.e. when there is no tag as head constant),
It does nothing if the tag tag_goal is already present.

Ltac xtag_pre_post_core tt :=
  match goal with
  | |- @tag tag_goal _ _ _ _ => idtac
  | |- @tag _ _ _ _ _ => xtag_add tag_goal
  | |- forall _, _ =>
     intro;
     xtag_pre_post_core tt;
     let x := get_last_hyp tt in
     revert x
  | _ => idtac
  end.

Tactic Notation "xtag_pre_post" :=
  xtag_pre_post_core tt.

xuntag_pre_post removes tag_goal from the head of the goal, or does nothing if there is no such tag.

Ltac xuntag_pre_post_core tt :=
  match goal with
  | |- @tag tag_goal _ _ _ _ => unfold tag at 1
  | _ => idtac
  end.

Tactic Notation "xuntag_pre_post" :=
  xuntag_pre_post_core tt.

cfml_get_goal tt returns the goal, ignoring the tag_goal at head

Ltac cfml_get_goal tt :=
  match goal with
  | |- @tag tag_goal _ ?F ?H ?Q => constr:(F H Q)
  | |- ?G => constr:(G)
  end.

cfml_get_tag tt returns the tag at the head of the goal

Ltac cfml_get_tag tt :=
  match cfml_get_goal tt with
    | @tag ?t _ _ ?H ?Q => constr:(t)
    | app ?f ?xs ?H ?Q => constr:(tag_none_app)
    | _ => constr:(tag_none)
  end.

cfml_check_not_tagged tt fails if the head of the goal contains a tag

xuntag T removes the tag T at the head of the goal, and fails if it is not there. The tag tag_goal is treated specially: it is automatically removed on the fly. To remove only tag_goal, use xuntag_pre_post.

Ltac xuntag_core T :=
  xuntag_pre_post;
  match goal with
  | |- @tag T _ _ => unfold tag at 1
  | |- @tag T _ _ _ _ => unfold tag at 1
  | _ => fail 1 "goal does not contain the expected tag: " T
  end.

Tactic Notation "xuntag" constr(T) :=
  xuntag_core T.

xuntag removes the tag at the head of the goal, and fails if there is not tag there. It automatically removes the tag_goal at the head, if any.

Tactic Notation "xuntag" :=
  xuntag_pre_post_core tt;
  match goal with
  | |- @tag _ _ _ => unfold tag at 1
  | |- @tag _ _ _ _ _ => unfold tag at 1
  end.

xuntags removes all tags from everywhere in the goal; useful for debugging.

Tactic Notation "xuntags" :=
  unfold tag in *.

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 "'!RecordNew' P" := (tag tag_record_new P)
  (at level 95) : tag_scope.
Notation "'!Val' P" := (tag tag_val (local P))
  (at level 95) : tag_scope.
Notation "'!Fun' P" := (tag tag_fun (local P))
  (at level 95) : tag_scope.
Notation "'!Let' P" := (tag tag_let (local P))
  (at level 95) : tag_scope.
Notation "'!LetPoly' P" := (tag tag_let_poly (local P))
  (at level 95) : tag_scope.
Notation "'!AppCurried' P" := (tag tag_app_curried P)
  (at level 95) : tag_scope.

Notation "'!Match' P" := (tag tag_match (local P))
  (at level 95).
Notation "'!Case' P" := (tag tag_case (local P))
  (at level 95) : tag_scope.
Notation "'!CaseWhen' P" := (tag tag_casewhen (local P))
  (at level 95) : tag_scope.
Notation "'!Alias' P" := (tag tag_alias (local P))
  (at level 95) : tag_scope.
Notation "'!Fail' P" := (tag tag_fail (local P))
  (at level 95) : tag_scope.
Notation "'!Done' P" := (tag tag_done (local P))
  (at level 95) : tag_scope.

Notation "'!If' P" := (tag tag_if (local P))
  (at level 95) : tag_scope.
Notation "'!Seq' P" := (tag tag_seq (local P))
  (at level 95) : tag_scope.
Notation "'!For' P" := (tag tag_for (local P))
  (at level 95) : tag_scope.
Notation "'!ForDown' P" := (tag tag_for_down (local P))
  (at level 95) : tag_scope.

Notation "'!While' P" := (tag tag_while (local P))
  (at level 95) : tag_scope.

Notation "'!Assert' P" := (tag tag_assert (local P))
  (at level 95) : tag_scope.
Notation "'!Pay' P" := (tag tag_pay (local P))
  (at level 95) : tag_scope.

Notation "'!TopVal' P" := (tag tag_top_val P)
  (at level 95) : tag_scope.
Notation "'!TopFun' P" := (tag tag_top_fun P)
  (at level 95) : tag_scope.

Notation "'!PrePost' P" := (tag tag_goal P)
  (at level 95) : tag_scope.
Notation "'!PrePost' P" := (tag tag_goal P)
  (at level 95) : charac.

Local Open Scope tag_scope.

Notation "P1 '==>' P2" :=
  (@pred_incl heap P1 P2) (at level 55, right associativity,
  format "'[v' '[' P1 ']' '/' '==>' '/' '[' P2 ']' ']'" )
  : charac.

Notation " Q1 '===>' Q2" :=
  (@rel_incl' _ heap Q1 Q2) (at level 55, right associativity,
  format "'[v' '[' Q1 ']' '/' '===>' '/' '[' Q2 ']' ']'")
  : charac.

Notation "'PRE' P1 '==>' 'POST' P2" :=
  (@pred_incl heap P1 P2) (at level 69,
  format "'[v' '[' 'PRE' P1 ']' '/' '==>' '/' '[' 'POST' P2 ']' ']'",
  only parsing)
  : charac.

Notation "'PRE' Q1 '===>' 'POST' Q2" :=
  (@rel_incl' _ heap Q1 Q2) (at level 69,
  format "'[v' '[' 'PRE' Q1 ']' '/' '===>' '/' '[' 'POST' Q2 ']' ']'",
  only parsing)
  : charac.

Notation "'PRE' H 'POST' Q 'CODE' F" :=
  (@tag tag_goal _ F H Q) (at level 69,
  format "'[v' '[' 'PRE' H ']' '/' '[' 'POST' Q ']' '/' '[' 'CODE' F ']' ']'")
  : charac.

Notation "F 'PRE' H 'POST' Q" :=
  (tag tag_goal F H Q)
  (at level 69, only parsing) : charac.

Notation "F 'INV' H 'POST' Q" :=
  (tag tag_goal F H%h (Q \*+ H%h))
  (at level 69, only parsing,
   format "'[v' F '/' '[' 'INV' H ']' '/' '[' 'POST' Q ']' ']'")
   : charac.

Notation "F 'PRE'' H1 'INV'' H2 'POST' Q" :=
  (tag tag_goal F (H1 \* H2)%h (Q \*+ H2%h))
  (at level 69, only parsing,
   format "'[v' F '/' '[' 'PRE'' H1 ']' '/' '[' 'INV'' H2 ']' '/' '[' 'POST' Q ']' ']'")
   : charac.

Ret

Notation "'Ret' v" :=
  (!Ret (fun H Q => H ==> Q v))
  (at level 69) : charac.

Notation "'Ret_' P" :=
  (Ret (isTrue P))
  (at level 69) : charac.

Open Scope charac.

App and LetApp

Notation "'App_' f xs" :=
  (!App (app f xs))
  (at level 68, f at level 0, xs at level 0) : charac.

Notation "'App' f x1 ;" :=
  (App_ f [x1])
  (at level 68, f at level 0, x1 at level 0) : charac.

Notation "'App' f x1 x2 ;" :=
  (App_ f [x1 x2])
  (at level 68, f at level 0, x1 at level 0,
   x2 at level 0) : charac.

Notation "'App' f x1 x2 x3 ;" :=
  (App_ f [x1 x2 x3])
  (at level 68, f at level 0, x1 at level 0, x2 at level 0,
   x3 at level 0) : charac.

Notation "'App' f x1 x2 x3 x4 ;" :=
  (App_ f [x1 x2 x3 x4])
  (at level 68, f at level 0, x1 at level 0, x2 at level 0,
   x3 at level 0, x4 at level 0) : charac.

Notation "'App' f x1 x2 x3 x4 x5 ;" :=
  (App_ f [x1 x2 x3 x4 x5])
  (at level 68, f at level 0, x1 at level 0, x2 at level 0,
   x3 at level 0, x4 at level 0, x5 at level 0) : charac.

Notation for record operations

Notation "'AppNew' L" := (!RecordNew (app_record_new L))
  (at level 69, no associativity, L at level 0,
   format "'AppNew' L") : charac.

Notation "'App'' r `. f" := (App record_get r f;)
  (at level 69, no associativity, f at level 0,
   format "'App'' r `. f") : charac.

Notation "'App'' r `. f `<- v" := (App record_set r f v;)
  (at level 69, no associativity, f at level 0,
   format "'App'' r `. f `<- v") : charac.

SetApp

Notation "'LetApp' x ':=' f xs 'in' F2" :=
  (!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.

Notation "'SeqApp' f xs ;; F2" :=
  (!Seq (fun H Q => exists Q', (App f xs;) H Q' /\ F2 (Q' tt) Q ))
  (at level 68, f at level 0, xs at level 0, right associativity,
   format "'[v' 'SeqApp' '[' f xs ']' ;; '/' '[' F2 ']' ']'") : charac.

Notation "'SeqApp'' r `. f `<- v ;; F2" :=
  (!Seq (fun H Q => exists Q', (App record_set r f v;) H Q' /\ F2 (Q' tt) Q ))
  (at level 68, r at level 0, f at level 0, v at level 0, right associativity,
   format "'[v' 'SeqApp'' '[' r `. f `<- v ']' ;; '/' '[' F2 ']' ']'") : charac.

Notation "'LetApp'' x ':=' r `. f 'in' F2" :=
  (!Let (fun H Q => exists Q1, (App record_get r f;) H Q1 /\ forall x, F2 (Q1 x) Q ))
  (at level 69, x ident, r at level 0, f at level 0,
   right associativity,
  format "'[v' '[' 'LetApp'' x ':=' r `. f 'in' ']' '/' '[' F2 ']' ']'") : charac.

Notation "'LetAppNew' L 'in' F2" :=
  (!Let (fun H Q => exists Q1, (!RecordNew (app_record_new L)) H Q1 /\ forall x, F2 (Q1 x) Q ))
  (at level 69, L at level 0,
   right associativity,
  format "'[v' '[' 'LetAppNew' L 'in' ']' '/' '[' F2 ']' ']'") : charac.

LetVal

Notation "'LetVal' x ':=' V 'in' F" :=
  (!Val (fun H Q => forall x, x = V -> F H Q ))
  (at level 69, x ident) : charac.

Notation "'LetVal' { A1 } x ':=' V 'in' F" :=
  (!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" :=
  (!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" :=
  (!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" :=
  (!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.

AppCurried

Notation "'AppCurried' f '[' x1 ']' ':=' K" :=
  (!AppCurried ( curried 1 f
          /\ (forall x1 H Q, K H Q -> app f [x1] H Q )))
  (at level 0, f at level 0, x1 ident) : charac.

Notation "'AppCurried' f [ x1 x2 ] ':=' K" :=
  (!AppCurried ( curried 2 f
          /\ (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 "'AppCurried' f [ x1 x2 x3 ] ':=' K" :=
  (!AppCurried ( curried 3 f
          /\ (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 "'AppCurried' f [ x1 x2 x3 x4 ] ':=' K" :=
  (!AppCurried ( curried 4 f
          /\ (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 "'AppCurried' f A1 '[' x1 ']' ':=' K" :=
  (!AppCurried ( curried 1 f
          /\ (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 "'AppCurried' f A1 '[' x1 x2 ']' ':=' K" :=
  (!AppCurried ( curried 2 f
          /\ (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 "'AppCurried' f A1 [ x1 x2 x3 ] ':=' K" :=
  (!AppCurried ( 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 "'AppCurried' f A1 [ x1 x2 x3 x4 ] ':=' K" :=
  (!AppCurried ( 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 "'AppCurried' f A1 A2 [ x1 ] ':=' K" :=
  (!AppCurried ( curried 1 f
          /\ (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 "'AppCurried' f A1 A2 [ x1 x2 ] ':=' K" :=
  (!AppCurried ( curried 2 f
          /\ (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 "'AppCurried' f A1 A2 [ x1 x2 x3 ] ':=' K" :=
  (!AppCurried ( 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 "'AppCurried' f A1 A2 [ x1 x2 x3 x4 ] ':=' K" :=
  (!AppCurried ( 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 "'AppCurried' f A1 A2 A3 [ x1 ] ':=' K" :=
  (!AppCurried ( 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 "'AppCurried' f A1 A2 A3 [ x1 x2 ] ':=' K" :=
  (!AppCurried ( 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 "'AppCurried' f A1 A2 A3 [ x1 x2 x3 ] ':=' K" :=
  (!AppCurried ( 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 "'AppCurried' f A1 A2 A3 [ x1 x2 x3 x4 ] ':=' K" :=
  (!AppCurried ( 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

Notation "'Func' f ':=' F1 'in' F2" :=
  (!Fun (fun H Q => forall f, F1 -> F2 H Q ))
  (at level 69, f ident) : charac.
Notation "'Fun' f [ x1 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f [ x1 ] := K) in F)
  (at level 69, f ident, x1 ident) : charac.

Notation "'Fun' f [ x1 x2 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f [ x1 x2 ] := K) in F)
  (at level 69, f ident, x1 ident, x2 ident) : charac.

Notation "'Fun' f [ x1 x2 x3 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f [ x1 x2 x3 ] := K) in F)
  (at level 69, f ident, x1 ident, x2 ident, x3 ident) : charac.

Notation "'Fun' f [ x1 x2 x3 x4 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f [ x1 x2 x3 x4 ] := K) in F)
  (at level 69, f ident, x1 ident, x2 ident, x3 ident, x4 ident) : charac.

Notation "'Fun' f A1 [ x1 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f A1 [ x1 ] := K) in F)
  (at level 69, f ident, x1 ident, A1 ident) : charac.

Notation "'Fun' f A1 [ x1 x2 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f A1 [ x1 x2 ] := K) in F)
  (at level 69, f ident, x1 ident, x2 ident, A1 ident) : charac.

Notation "'Fun' f A1 [ x1 x2 x3 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f A1 [ x1 x2 x3 ] := K) in F)
  (at level 69, f ident, x1 ident, x2 ident, x3 ident, A1 ident) : charac.

Notation "'Fun' f A1 [ x1 x2 x3 x4 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f A1 [ x1 x2 x3 x4 ] := K) in F)
  (at level 69, f ident, x1 ident, x2 ident, x3 ident, x4 ident, A1 ident) : charac.

Notation "'Fun' f A1 A2 [ x1 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f A1 A2 [ x1 ] := K) in F)
  (at level 69, f ident, x1 ident, A1 ident, A2 ident) : charac.

Notation "'Fun' f A1 A2 [ x1 x2 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f A1 A2 [ x1 x2 ] := K) in F)
  (at level 69, f ident, x1 ident, x2 ident, A1 ident, A2 ident) : charac.

Notation "'Fun' f A1 A2 [ x1 x2 x3 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f A1 A2 [ x1 x2 x3 ] := K) in F)
  (at level 69, f ident, x1 ident, x2 ident, x3 ident, A1 ident, A2 ident) : charac.

Notation "'Fun' f A1 A2 [ x1 x2 x3 x4 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f A1 A2 [ x1 x2 x3 x4 ] := K) in F)
  (at level 69, f ident, x1 ident, x2 ident, x3 ident, x4 ident, A1 ident, A2 ident) : charac.

Notation "'Fun' f A1 A2 A3 [ x1 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f A1 A2 A3 [ x1 ] := K) in F)
  (at level 69, f ident, x1 ident, A1 ident, A2 ident, A3 ident) : charac.

Notation "'Fun' f A1 A2 A3 [ x1 x2 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f A1 A2 A3 [ x1 x2 ] := K) in F)
  (at level 69, f ident, x1 ident, x2 ident, A1 ident, A2 ident, A3 ident) : charac.

Notation "'Fun' f A1 A2 A3 [ x1 x2 x3 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f A1 A2 A3 [ x1 x2 x3 ] := K) in F)
  (at level 69, f ident, x1 ident, x2 ident, x3 ident, A1 ident, A2 ident, A3 ident) : charac.

Notation "'Fun' f A1 A2 A3 [ x1 x2 x3 x4 ] ':=' K 'in' F" :=
  (Func f := (AppCurried f A1 A2 A3 [ x1 x2 x3 x4 ] := K) in F)
  (at level 69, f ident, x1 ident, x2 ident, x3 ident, x4 ident, A1 ident, A2 ident, A3 ident) : charac.

LetFuns

Notation "'Funs' f1 ':=' K1 'and' f2 ':=' K2 'in' F" := (!Fun fun H Q => forall f1 f2, exists P1 P2, (K1 -> K2 -> P1 f1 /\ P2 f2) /\ (P1 f1 -> P2 f2 -> F H Q)) (at level 69, f1 ident, f2 ident) : charac.

Notation "'Funs' f1 ':=' K1 'and' f2 ':=' K2 'and' f3 ':=' K3 'in' F" := (!Fun fun H Q => forall f1 f2 f3, exists P1 P2 P3, (K1 -> K2 -> K3 -> P1 f1 /\ P2 f2 /\ P3 f3) /\ (P1 f1 -> P2 f2 -> P3 f3 -> F H Q)) (at level 69, f1 ident, f2 ident, f3 ident) : charac.

Let

Definition cf_let (A B : Type) (F1:~~A) (F2:A ->~~B) : ~~ B :=
  (fun H Q => exists Q1, F1 H Q1 /\ forall x, F2 x (Q1 x) Q).

Arguments cf_let [A] [B].

Notation "'Let' x ':=' F1 'in' F2" :=
  (!Let (cf_let F1 (fun x => F2)))
  (at level 69, x ident, right associativity,
  format "'[v' '[' 'Let' x ':=' F1 'in' ']' '/' '[' F2 ']' ']'") : charac.

Notation "'Let' x ':' T ':=' F1 'in' F2" :=
  (!Let (fun H Q => exists Q1, F1 H Q1 /\ forall x:T, F2 (Q1 x) Q ))
  (at level 69, x ident, right associativity, only parsing) : charac.

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.

Seq

Notation "'Seq_' F1 ;; F2" :=
  (!Seq (fun H Q => exists Q', F1 H Q' /\ F2 (Q' tt) Q ))
  (at level 68, right associativity,
   format "'[v' 'Seq_' '[' F1 ']' ;; '/' '[' F2 ']' ']'") : charac.

Notation "F1 ;; F2" :=
  (!Seq (fun H Q => exists Q', F1 H Q' /\ F2 (Q' tt) Q ))
  (at level 68, right associativity, only parsing,
   format "'[v' '[' F1 ']' ;; '/' '[' F2 ']' ']'") : charac.

Assert

Notation "'Assert' F1" :=
  (!Assert (fun H Q => F1 H (fun (b:bool) => \[b = true ] \* H) /\ H ==> Q tt ))
  (at level 68, right associativity,
   format "'[v' 'Assert' F1 ']'") : charac.

Pay

Notation "'Pay_' ;; F1" :=
  (!Pay (fun H Q => exists H', pay_one H H' /\ F1 H' Q ))
  (at level 68, right associativity,
   format "'[v' 'Pay_' ;; '[' F1 ']' ']'") : charac.

If and IfTrm and IfProp LetIf

Notation "'If_' x 'Then' F1 'Else' F2" :=
  (!If (fun H Q => (x = true -> F1 H Q ) /\ (x = false -> F2 H Q )))
  (at level 69, x at level 0) : charac.

Notation "'LetIf' F0 'Then' F1 'Else' F2" :=
  (Let x := F0 in If_ x Then F1 Else F2)
  (at level 69, only parsing) : charac.

&& and ||

Notation "'And_' v1 `&&` F2" :=
  (!If (fun H Q => (v1 = true -> F2 H Q ) /\ (v1 = false -> (Ret false) H Q )))
  (at level 69, v1 at level 0) : charac.

Notation "'Or_' v1 `||` F2" :=
  (!If (fun H Q => (v1 = true -> (Ret true) H Q ) /\ (v1 = false -> F2 H Q )))
  (at level 69, v1 at level 0) : charac.

Case

Notation "'Case' x '=' p 'Then' F1 'Else' F2" :=
  (!Case (fun H Q => (x = p -> F1 H Q ) /\ (x <> p -> F2 H Q )))
  (at level 69, x at level 0) : charac.

Notation "'Case' x '=' p [ x1 ] 'Then' F1 'Else' F2" :=
  (!Case (fun H Q => (forall x1, x = p -> F1 H Q )
                /\ ((forall x1, x <> p) -> F2 H Q )))
  (at level 69, x at level 0, x1 ident) : charac.

Notation "'Case' x '=' p [ x1 x2 ] 'Then' F1 'Else' F2" :=
  (!Case (fun H Q => (forall x1 x2, x = p -> F1 H Q )
                /\ ((forall x1 x2, x <> p) -> F2 H Q )))
  (at level 69, x at level 0, x1 ident, x2 ident) : charac.

Notation "'Case' x '=' p [ x1 x2 x3 ] 'Then' F1 'Else' F2" :=
  (!Case (fun H Q => (forall x1 x2 x3, x = p -> F1 H Q )
                /\ ((forall x1 x2 x3, x <> p) -> F2 H Q )))
  (at level 69, x at level 0, x1 ident, x2 ident,
   x3 ident) : charac.

Notation "'Case' x '=' p [ x1 x2 x3 x4 ] 'Then' F1 'Else' F2" :=
  (!Case (fun H Q => (forall x1 x2 x3 x4, x = p -> F1 H Q )
                /\ ((forall x1 x2 x3 x4, x <> p) -> F2 H Q )))
  (at level 69, x at level 0, x1 ident, x2 ident,
   x3 ident, x4 ident) : charac.

Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 ] 'Then' F1 'Else' F2" :=
  (!Case (fun H Q => (forall x1 x2 x3 x4 x5, x = p -> F1 H Q )
                /\ ((forall x1 x2 x3 x4 x5, x <> p) -> F2 H Q )))
  (at level 69, x at level 0, x1 ident, x2 ident,
   x3 ident, x4 ident, x5 ident) : charac.

Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 x6 ] 'Then' F1 'Else' F2" :=
  (!Case (fun H Q => (forall x1 x2 x3 x4 x5 x6, x = p -> F1 H Q )
                /\ ((forall x1 x2 x3 x4 x5 x6, x <> p) -> F2 H Q )))
  (at level 69, x at level 0, x1 ident, x2 ident,
   x3 ident, x4 ident, x5 ident, x6 ident) : charac.

Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 x6 x7 ] 'Then' F1 'Else' F2" :=
  (!Case (fun H Q => (forall x1 x2 x3 x4 x5 x6 x7, x = p -> F1 H Q )
                /\ ((forall x1 x2 x3 x4 x5 x6 x7, x <> p) -> F2 H Q )))
  (at level 69, x at level 0, x1 ident, x2 ident,
   x3 ident, x4 ident, x5 ident, x6 ident, x7 ident) : charac.

CaseWhen

Notation "'Case' x '=' p 'When' w 'Then' F1 'Else' F2" :=
  (!CaseWhen (fun H Q => (x = p -> istrue (w)%bool -> F1 H Q )
                /\ (x <> p \/ istrue (!w%bool) -> F2 H Q )))
  (at level 69, x at level 0) : charac.

Notation "'Case' x '=' p [ x1 ] 'When' w 'Then' F1 'Else' F2" :=
  (!CaseWhen (fun H Q => (forall x1, x = p -> istrue w%bool -> F1 H Q )
                /\ ((forall x1, x <> p \/ istrue (!w%bool)) -> F2 H Q )))
  (at level 69, x at level 0, x1 ident) : charac.

Notation "'Case' x '=' p [ x1 x2 ] 'When' w 'Then' F1 'Else' F2" :=
  (!CaseWhen (fun H Q => (forall x1 x2, x = p -> istrue w%bool -> F1 H Q )
                /\ ((forall x1 x2, x <> p \/ istrue (!w%bool)) -> F2 H Q )))
  (at level 69, x at level 0, x1 ident, x2 ident) : charac.

Notation "'Case' x '=' p [ x1 x2 x3 ] 'When' w 'Then' F1 'Else' F2" :=
  (!CaseWhen (fun H Q => (forall x1 x2 x3, x = p -> istrue w%bool -> F1 H Q )
                /\ ((forall x1 x2 x3, x <> p \/ istrue (!w%bool)) -> F2 H Q )))
  (at level 69, x at level 0, x1 ident, x2 ident,
   x3 ident) : charac.

Notation "'Case' x '=' p [ x1 x2 x3 x4 ] 'When' w 'Then' F1 'Else' F2" :=
  (!CaseWhen (fun H Q => (forall x1 x2 x3 x4, x = p -> istrue w%bool -> F1 H Q )
                /\ ((forall x1 x2 x3 x4, x <> p \/ istrue (!w%bool)) -> F2 H Q )))
  (at level 69, x at level 0, x1 ident, x2 ident,
   x3 ident, x4 ident) : charac.

Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 ] 'When' w 'Then' F1 'Else' F2" :=
  (!CaseWhen (fun H Q => (forall x1 x2 x3 x4 x5, x = p -> istrue w%bool -> F1 H Q )
                /\ ((forall x1 x2 x3 x4 x5, x <> p \/ istrue (!w%bool)) -> F2 H Q )))
  (at level 69, x at level 0, x1 ident, x2 ident,
   x3 ident, x4 ident, x5 ident) : charac.

Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 x6 ] 'When' w 'Then' F1 'Else' F2" :=
  (!CaseWhen (fun H Q => (forall x1 x2 x3 x4 x5 x6, x = p -> istrue w%bool -> F1 H Q )
                /\ ((forall x1 x2 x3 x4 x5 x6, x <> p \/ istrue (!w%bool)) -> F2 H Q )))
  (at level 69, x at level 0, x1 ident, x2 ident,
   x3 ident, x4 ident, x5 ident, x6 ident) : charac.

Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 x6 x7 ] 'When' w 'Then' F1 'Else' F2" :=
  (!CaseWhen (fun H Q => (forall x1 x2 x3 x4 x5 x6 x7, x = p -> istrue w%bool -> F1 H Q )
                /\ ((forall x1 x2 x3 x4 x5 x6 x7, x <> p \/ istrue (!w%bool)) -> F2 H Q )))
  (at level 69, x at level 0, x1 ident, x2 ident,
   x3 ident, x4 ident, x5 ident, x6 ident, x7 ident) : charac.

Match

Notation "'Match' Q" :=
(!Match Q)
(at level 69) : charac.

Alias

Notation "'Alias' x ':=' v 'in' F" :=
(!Alias (fun H Q => forall x, x = v -> F H Q ))
(at level 69, x ident) : charac.

Fail

Notation "'Fail'" :=
(!Fail (fun _ _ => False ))
(at level 0) : charac.

Done

Notation "'Done'" :=
(!Done (fun _ _ => True ))
(at level 0) : charac.

While

Definition cf_while (F1:~~bool) (F2:~~unit) : ~~unit :=
  (fun H Q =>
    forall (R:~~unit), is_local R ->
      (forall H Q, (LetIf F1 Then (F2 ;; R ) Else (Ret tt )) H Q -> R H Q )
      -> R H Q).

Notation "'While' F1 'Do' F2 'Done_'" :=
  (!While (cf_while F1 F2))
  (at level 69, F2 at level 68,
   format "'[v' 'While' F1 'Do' '/' '[' F2 ']' '/' 'Done_' ']'")
   : charac.

For

Definition cf_for (a:int) (b:int) (F1:int ->~~unit) : ~~unit :=
  (fun H Q =>
      forall (S:int ->~~unit), CFHeaps.is_local_pred S ->
        (forall i H Q,
             (If_ isTrue (i <= (b)%Z) Then (F1 i ;; S (i +1)) Else (Ret tt )) H Q
          -> S i H Q )
       -> S a H Q).

Notation "'For' i '=' a 'To' b 'Do' F1 'Done_'" :=
  (!For (cf_for a b (fun i => F1)))
  (at level 69, i ident, a at level 0, b at level 0,
   format "'[v' 'For' i '=' a 'To' b 'Do' '/' '[' F1 ']' '/' 'Done_' ']'")
  : charac.

Definition cf_for_down (a:int) (b:int) (F1:int ->~~unit) : ~~unit :=
  (fun H Q =>
      forall (S:int ->~~unit), CFHeaps.is_local_pred S ->
        (forall i H Q,
             (If_ isTrue (i >= (b)%Z) Then (F1 i ;; S (i -1)) Else (Ret tt )) H Q
          -> S i H Q )
       -> S a H Q).

Notation "'For' i '=' a 'DownTo' b 'Do' F1 'Done_'" :=
  (!For (cf_for_down a b (fun i => F1)))
  (at level 69, i ident, a at level 0, b at level 0,
   format "'[v' 'For' i '=' a 'DownTo' b 'Do' '/' '[' F1 ']' '/' 'Done_' ']'")
  : charac.

TopVal

Notation "'TopVal' x ':=' Q" :=
  (!TopVal (forall P, Q P -> P x))
  (at level 69, x at level 0, Q at level 200)
   : charac.

Notation "'TopVal' '{' A1 '}' x ':=' Q" :=
  (!TopVal (forall A1 P, Q (P A1) -> (P A1) x))
  (at level 69, x at level 0, A1 ident, Q at level 200)
   : charac.

Notation "'TopVal' '{' A1 A2 '}' x ':=' Q" :=
  (!TopVal (forall A1 A2 P, Q (P A1 A2) -> (P A1 A2) x))
  (at level 69, x at level 0, A1 ident, A2 ident, Q at level 200)
   : charac.

Notation "'TopVal' '{' A1 A2 A3 '}' x ':=' Q" :=
  (!TopVal (forall A1 A2 A3 P, Q (P A1 A2 A3) -> (P A1 A2 A3) x))
  (at level 69, x at level 0, A1 ident, A2 ident, A3 ident, Q at level 200)
   : charac.

TopFun

Notation "'TopFun' ':=' H" :=
  (!TopFun H)
  (at level 69, H at level 200) : charac.

Notation "'TopFun' f ':=' K" :=
  (!TopFun (fun P => forall f, K -> P f))
  (at level 69, f ident) : charac.

Definition database_cf := True.

To register a specification, use: Hint Extern 1 (RegisterSpec f) => Provide f_spec.

or, if it involves time credits, use: Hint Extern 1 (RegisterSpecCredits f) => Provide f_spec.

Definition database_spec := True.
Notation "'RegisterSpec' T" := (Register database_spec T)
(at level 69) : charac.

Definition database_spec_credits := True.
Notation "'RegisterSpecCredits' T" := (Register database_spec_credits T)
(at level 69) : charac.

The focus and unfocus databases are used to register specifications for accessors to record fields, combined with focus/unfocus operations

Definition database_xopen := True.
Definition database_xclose := True.

Notation "'RegisterOpen' T" := (Register database_xopen T)
(at level 69) : charac.

Notation "'RegisterClose' T" := (Register database_xclose T)
(at level 69) : charac.