diff options
Diffstat (limited to 'src/Assembly/ConstrainedComputation.v')
| -rw-r--r-- | src/Assembly/ConstrainedComputation.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Assembly/ConstrainedComputation.v b/src/Assembly/ConstrainedComputation.v index f36b75187..aa5702506 100644 --- a/src/Assembly/ConstrainedComputation.v +++ b/src/Assembly/ConstrainedComputation.v @@ -1,12 +1,11 @@ Require Import Bedrock.Word. +(* Expression *) (* THEORY: if we permit operations on joined types, we can represent * vector operations without searching *) Inductive CType: Set := - | Int32: CType - | Int64: CType - | Join: CType -> CType -> CType . + | Words | list word Definition cTypeToWord(type: CType): Type := match type with @@ -44,6 +43,7 @@ Inductive CExpr (type: CType) := Inductive Sub (inType: CType) (outType: CType) := | CRet : Expr outType -> Sub inType outType + (* | Repeat *) | CCompose : forall medType, (Sub inType medType) -> (Sub medType outType) |