Commit 82cab7c7 authored by Glen Mével's avatar Glen Mével
Browse files

upstream loop notations into notation.v

parent b81bb3dd
......@@ -3,20 +3,6 @@ From iris.base_logic Require Import invariants.
From cosmo.program_logic Require Export proofmode.
Set Default Proof Using "Type".
(* This must NOT be a value since it may be open.
Note: this notation captures the variable "_while". *)
Notation While cond body :=
((rec: "_while" <> :=
if: cond then
body ;; "_while" #()
else
#()
) #())%E.
Notation "'while:' e1 'do' e2 'enddo'" := (While e1%E e2%E)
(at level 200, e1, e2 at level 200,
format "'[' 'while:' e1 'do' '/ ' e2 '/' 'enddo' ']'") : expr_scope.
(*
......
......@@ -4,20 +4,6 @@ From cosmo.program_logic Require Export proofmode.
Set Default Proof Using "Type".
Open Scope Z.
(* This must NOT be a value since it may be open.
Note: this notation captures the variable "_while". *)
Notation While cond body :=
((rec: "_while" <> :=
if: cond then
body ;; "_while" #()
else
#()
) #())%E.
Notation "'while:' e1 'do' e2 'enddo'" := (While e1%E e2%E)
(at level 200, e1, e2 at level 200,
format "'[' 'while:' e1 'do' '/ ' e2 '/' 'enddo' ']'") : expr_scope.
(*
......
......@@ -9,22 +9,6 @@ Open Scope Z.
(** Implementation **)
(* This must NOT be a value since it may be open. *)
(* Beware that this notation captures the variables "_for", "_i", "_start" and "_stop". *)
Notation For iname start stop body :=
((let: "_stop" := stop in
rec: "_for" "_i" :=
if: "_i" "_stop" then
let: iname := "_i" in
body ;; "_for" ("_i" + #1)
else
#()
) start)%E.
Notation "'for:' i 'from' e1 'to' e2 'do' e3 'enddo'" := (For i e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200,
format "'[' 'for:' i 'from' e1 'to' e2 'do' '/ ' e3 '/' 'enddo' ']'") : expr_scope.
Section pipeline.
Context (capacity : nat) (capacity_min : capacity 1).
......
......@@ -190,3 +190,31 @@ Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
(Match e0 BAnon e1 x%binder e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
(** Shaky notations for imperative constructs *)
(* Beware! This notation captures the variable "_while". *)
Notation While cond body :=
((rec: "_while" <> :=
if: cond then
body ;; "_while" #()
else
#()
) #())%E.
Notation "'while:' e1 'do' e2 'enddo'" := (While e1%E e2%E)
(at level 200, e1, e2 at level 200,
format "'[' 'while:' e1 'do' '/ ' e2 '/' 'enddo' ']'") : expr_scope.
(* Beware! This notation captures the variables "_for", "_i", "_start" and "_stop". *)
Notation For iname start stop body :=
((let: "_stop" := stop in
rec: "_for" "_i" :=
if: "_i" "_stop" then
let: iname := "_i" in
body ;; "_for" ("_i" + #1)
else
#()
) start)%E.
Notation "'for:' i 'from' e1 'to' e2 'do' e3 'enddo'" := (For i e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200,
format "'[' 'for:' i 'from' e1 'to' e2 'do' '/ ' e3 '/' 'enddo' ']'") : expr_scope.
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