diff options
Diffstat (limited to 'src/Assembly/Pseudo.v')
| -rw-r--r-- | src/Assembly/Pseudo.v | 48 |
1 files changed, 27 insertions, 21 deletions
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index b8aae4521..ca4700a7f 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -1,6 +1,7 @@ Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.State. Require Import Crypto.Assembly.Language Crypto.Assembly.QhasmEvalCommon. Require Import Coq.Lists.List Coq.Arith.Compare_dec Coq.omega.Omega. +Require Import Crypto.Util.Notations. Require Export Crypto.Util.FixCoqMistakes. Module Pseudo <: Language. @@ -31,8 +32,8 @@ Module Pseudo <: Language. }. Definition Params := Params'. - Definition State (p: Params): Type := ListState (width p). - Definition Program (p: Params): Type := + Definition State (p: Params) : Type := ListState (width p). + Definition Program (p: Params) : Type := @Pseudo (width p) (spec p) (inputs p) (outputs p). Definition Unary32: Params := mkParams 32 W32 1 1. @@ -40,7 +41,7 @@ Module Pseudo <: Language. (* Evaluation *) - Fixpoint pseudoEval {n m w s} (prog: @Pseudo w s n m) (st: ListState w): option (ListState w) := + Fixpoint pseudoEval {n m w s} (prog: @Pseudo w s n m) (st: ListState w) : option (ListState w) := match prog with | PVar n _ i => omap (getVar i st) (fun x => Some (setList [x] st)) | PMem n m v i => omap (getMem v i st) (fun x => Some (setList [x] st)) @@ -114,7 +115,7 @@ Module Pseudo <: Language. Delimit Scope pseudo_notations with p. Local Open Scope pseudo_notations. - Definition indexize {n: nat} (x: nat): Index n. + Definition indexize {n: nat} (x: nat) : Index n. intros; destruct (le_dec n 0). - exists 0; abstract intuition auto with zarith. @@ -123,60 +124,65 @@ Module Pseudo <: Language. Defined. Notation "% A" := (PVar _ (Some false) (indexize A)) - (at level 20, right associativity) : pseudo_notations. + : pseudo_notations. Notation "$ A" := (PVar _ (Some true) (indexize A)) - (at level 20, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :[ B ]:" := (PMem _ _ (indexize A) (indexize B)) - (at level 20, right associativity) : pseudo_notations. + : pseudo_notations. Notation "# A" := (PConst _ (natToWord _ A)) - (at level 20, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :+: B" := (PBin _ IAdd (PComb _ _ _ A B)) - (at level 60, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :+c: B" := (PCarry _ AddWithCarry (PComb _ _ _ A B)) - (at level 60, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :-: B" := (PBin _ ISub (PComb _ _ _ A B)) - (at level 60, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :&: B" := (PBin _ IAnd (PComb _ _ _ A B)) - (at level 45, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :^: B" := (PBin _ IXor (PComb _ _ _ A B)) - (at level 45, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :>>: B" := (PShift _ Shr (indexize B) A) - (at level 60, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :<<: B" := (PShift _ Shl (indexize B) A) - (at level 60, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :*: B" := (PDual _ Mult (PComb _ _ _ A B)) - (at level 55, right associativity) : pseudo_notations. + : pseudo_notations. + (* TODO(rsloan, from jgross): This notation is not okay. It breaks + [constr:(nat)] and [((1):nat)]. Please remove all frowny faces + from notations, and then move [Reserved Notation] line to + Fiat.Crypto.Util.Notations. *) + Reserved Notation "O :( A , B ): :?: L ::: R" (at level 70, right associativity). Notation "O :( A , B ): :?: L ::: R" := (PIf _ _ O (indexize A) (indexize B) L R) - (at level 70, right associativity) : pseudo_notations. + : pseudo_notations. Notation "F :**: e" := (PFunExp _ F e) - (at level 70, right associativity) : pseudo_notations. + : pseudo_notations. Notation "E :->: F" := (PLet _ _ _ E F) - (at level 70, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :|: B" := (PComb _ _ _ A B) - (at level 65, left associativity) : pseudo_notations. + : pseudo_notations. Notation "n ::: A :():" := (PCall _ _ n A) - (at level 65, left associativity) : pseudo_notations. + : pseudo_notations. Close Scope pseudo_notations. End Pseudo. |