Merge some cleanup changes.

src/Verse.v

@@ -7,10 +7,6 @@ Require        Verse.Scope.
 Export Vector.VectorNotations.
 Delimit Scope vector_scope with vector.
 
-Module VerseNotations.
-  Open Scope verse_scope.
-End VerseNotations.
-
 (* This allows us to use the vector notations for lists as well
 
 <<
@@ -28,7 +24,6 @@ Coercion Vector.to_list : Vector.t >-> list.
 
 Definition VariableT := Variables.U verse_type_system.
 
-Notation "V 'of' 'type' T" := (V (existT _ _ T)) (at level 50).
 
 Definition constant ty := const ty.
 Definition Declaration := Verse.Scope.type verse_type_system.

src/Verse/Ast.v

@@ -47,22 +47,23 @@ Import EqNotations.
 
 Section VerseCode.
 
+  (* TODO : Do we need the Verse AST to be parametrized on the typeSystem any more? *)
   Variable ts : typeSystem.
 
   Variable v : Variables.U ts.
 
   (** Expressions that can occur on the left of an assignment. *)
-  Inductive lexpr : some (typeOf ts) -> Type :=
-  | var   :  forall {ty}, v (existT _ direct ty) -> lexpr (existT _ direct ty)
-  | deref :  forall {ty b e}, v (existT _ _ (arrayType ts b e ty)) -> {i | i < b} -> lexpr (existT _ direct ty).
+  Inductive lexpr : {k & ts k} -> Type :=
+  | var   :  forall {ty : ts direct}, v of type ty -> lexpr of type ty
+  | deref :  forall {ty b e}, v of type (arrayType ts b e ty) -> {i | i < b} -> lexpr of type ty.
 
   (** The expression type *)
 
-  Inductive expr : some (typeOf ts) -> Type :=
-  | cval     : forall {ty}, constOf ts ty -> expr (existT _ direct ty)
+  Inductive expr : {k & ts k} -> Type :=
+  | cval     : forall {ty : ts direct}, constOf ts ty -> expr of type ty
   | valueOf  : forall {ty}, lexpr ty -> expr ty
-  | uniOp    : forall {ty}, operator ts ty 1 -> expr (existT _ direct ty) -> expr (existT _ direct ty)
-  | binOp    : forall {ty}, operator ts ty 2 -> expr (existT _ direct ty) -> expr (existT _ direct ty) -> expr (existT _ direct ty)
+  | uniOp    : forall {ty : ts direct}, operator ts ty 1 -> expr of type ty -> expr of type ty
+  | binOp    : forall {ty : ts direct}, operator ts ty 2 -> expr of type ty -> expr of type ty -> expr of type ty
   .
 
   (** ** Instructions
@@ -93,10 +94,10 @@ Section VerseCode.
 
    *)
 
-  Inductive instruction : some (typeOf ts) -> Type :=
+  Inductive instruction : {k & ts k} -> Type :=
   | assign      kty : lexpr kty -> expr kty  -> instruction kty
-  | binopUpdate ty  : lexpr (existT _ direct ty) -> operator ts ty 2 -> expr (existT _ direct ty) -> instruction (existT _ direct ty)
-  | uniopUpdate ty  : lexpr (existT _ direct ty) -> operator ts ty 1 -> instruction (existT _ direct ty)
+  | binopUpdate (ty : ts direct)  : lexpr of type ty -> operator ts ty 2 -> expr of type ty -> instruction of type ty
+  | uniopUpdate (ty : ts direct)  : lexpr of type ty -> operator ts ty 1 -> instruction of type ty
   | moveTo      kty : lexpr kty -> v kty  -> instruction kty
   | clobber     kty : v kty -> instruction kty.
 
@@ -115,7 +116,7 @@ Arguments statement [ts].
    be able to use old code
 *)
 Coercion mapRep ts (v : Variables.U ts) (c : code v) : Repeat (statement v)
-  := List.map (fun x => repeat 1 [x]%list) c.
+  := [repeat 1 c]%list.
 
 (**
 
@@ -127,7 +128,7 @@ type [ty].
  *)
 Record iterator ts (v : Variables.U ts) (ty : typeOf ts memory)
   := { setup    : Repeat (statement v);
-       process  : v (existT _ _ ty) -> Repeat (statement v);
+       process  : v of type ty -> Repeat (statement v);
        finalise : Repeat (statement v)
      }.
 
@@ -156,7 +157,7 @@ Require Import Verse.Error.
 Module LExpr.
 
   (** Function for renaming variables *)
-  Definition rename {ts}{u v : Variables.U ts}(rn : Variables.renaming u v) {ty : some (typeOf ts) } (l : lexpr u ty)
+  Definition rename {ts}{u v : Variables.U ts}(rn : Variables.renaming u v) {ty : some ts } (l : lexpr u ty)
   : lexpr v ty
     := match l with
        | var x     => var (rn _ x)
@@ -175,14 +176,14 @@ Module LExpr.
        | @deref _ _ ty b e a i =>
          let compatPf := arrayCompatibility tr b e ty in
          let ap  := Variables.translate tr a in
-         deref (rew [fun t => v (existT tgt memory t)] compatPf in ap) i
+         deref (rew [fun t => v of type t] compatPf in ap) i
        end.
 
   Arguments translate [src tgt] tr [v ty].
 
   Definition result tgt (v : Variables.U tgt) (ty : some (Types.result tgt))
     := match ty with
-       | existT _ _ {- good -} => lexpr v (existT _ _ good)
+       | existT _ _ {- good -} => lexpr v of type good
        | existT _ _ (error _)  => Empty_set + {TranslationError}
        end.
 
@@ -264,7 +265,7 @@ Module Expr.
   Definition result tgt
              (v : Variables.U tgt) (ty : some (Types.result tgt))
     := match ty with
-       | existT _ _ {- good -} => expr v (existT _ _ good)
+       | existT _ _ {- good -} => expr v of type good
        | existT _ _ (error _)  => Empty_set + {TranslationError}
        end.
   Arguments result [tgt].
@@ -338,15 +339,15 @@ Module Instruction.
              (v  : Variables.U tgt)
              (ty : some (Types.result tgt))
     := match ty with
-       | existT _ _ {- tyc -} => instruction v (existT _ _ tyc)
+       | existT _ _ {- tyc -} => instruction v of type tyc
        | existT _ _ (error _) => Empty_set + {TranslationError}
        end.
 
   Arguments result [tgt].
 
   Definition extract tgt
              (v : Variables.U tgt)
-             (ty : some (Types.result tgt))
+             (ty : {k & Types.result tgt k})
     : instruction (Variables.Universe.inject v) ty -> result v ty
     := match ty with
        | existT _ _ (error err) =>  fun i => error (CouldNotTranslateBecause i err)
@@ -543,7 +544,7 @@ Module Iterator.
              (itr : iterator (Variables.Universe.coCompile cr v) memty)
              (good : typeOf tgt memory)
              (pf : Types.compile cr memty = {- good -})
-             (x  : v (existT _ _ good))
+             (x  : v of type good)
     : compiled tgt v + {TranslationError}
     := do stup <- RepCode.compile cr (setup itr) ;;
        do fnls <- RepCode.compile cr (finalise itr) ;;

src/Verse/CryptoLib/blake2/c/portable.v

@@ -1,5 +1,4 @@
 Require Import Verse.
-Import VerseNotations.
 Require Import Verse.CryptoLib.blake2.
 Require Import PeanoNat.
 Require Import Bvector.
@@ -139,17 +138,15 @@ Module Blake2 (C : CONFIG).
         applied to either the rows or the diagonals of this matrix.
 
      *)
+
+      (* Note : We are not using a vector of variables here beacuse the
+      vi's tend to get used a lot outside the code/verse custom syntax
+      and our indexing notation is only available inside those *)
       Variable v0 v4 v8  v12
                v1 v5 v9  v13
                v2 v6 v10 v14
                v3 v7 v11 v15 : progvar of type Word.
 
-      Definition state := [ v0 ; v4 ; v8  ; v12;
-                            v1 ; v5 ; v9  ; v13;
-                            v2 ; v6 ; v10 ; v14;
-                            v3 ; v7 ; v11 ; v15
-                          ].
-
       (** *** Variables to maintain byte count
 
           Recall that each of the blake2 blocks is compressed using a

src/Verse/CryptoLib/chacha20/c/portable.v

@@ -10,7 +10,6 @@ This module implements the following
  *)
 
 Require Import Verse.
-Import VerseNotations.
 Require Import Verse.CryptoLib.chacha20.common.
 
 Module Internal.

src/Verse/CryptoLib/curve25519/c/portable.v

@@ -1,5 +1,5 @@
 Require Import Verse.
-Import VerseNotations.
+
 (** * Curve 25519 and its parameters *)
 
 

src/Verse/CryptoLib/poly1305/c/portable.v

@@ -64,7 +64,6 @@
 
 
 Require Import Verse.
-Import VerseNotations.
 
 (** * Introduction
 

src/Verse/CryptoLib/sha2.v

@@ -8,7 +8,6 @@
 (** printing oplus  %$\oplus$%   #⊕#  *)
 
 Require Import Verse.
-Import VerseNotations.
 
 (** * SHA-2 hashes
 

src/Verse/CryptoLib/sha2/c/portable.v

@@ -14,7 +14,6 @@
 (** printing oplus %$\oplus$%    #⊕#  *)
 
 Require Import Verse.
-Import VerseNotations.
 Require Import Verse.CryptoLib.sha2.
 Require Import List.
 Import ListNotations.

src/Verse/Language/Macros/BitOps.v

@@ -92,7 +92,7 @@ The difference is illustrated in the picture below.
 (** There is also the update version of these functions that updates a
     given l-expr with the above mentioned operations.  *)
 Section ForAll.
-  Open Scope verse_scope.
+
   Variable v : VariableT.
   Variable ty : type direct.
   Variable E  : Type.

src/Verse/Language/Macros/Cache.v

@@ -2,7 +2,7 @@
 Require Import Verse.Ast.
 Require Import Verse.Language.Types.
 Require Import Verse.TypeSystem.
-Require        Verse.Language.Pretty.
+Require Import Verse.Language.Pretty.
 Require Import Verse.Language.Macros.Loops.
 Require Import List.
 Require Import Psatz.
@@ -47,12 +47,12 @@ Section ArrayUtils.
 
    *)
 
-  Definition indices (arr : v (existT _ _ (array b e ty))) := Loops.Internal.loop b.
+  Definition indices (arr : v of type (array b e ty)) := Loops.Internal.loop b.
 
 
   (** This function is similar to indices but gives the indices in the
       reverse order.  *)
-  Definition indices_reversed (arr : v (existT _ _ (array b e ty))) := List.rev (indices arr).
+  Definition indices_reversed (arr : v of type (array b e ty)) := List.rev (indices arr).
 
 
 
@@ -78,9 +78,9 @@ Section ArrayUtils.
 
    *)
 
-  Definition VarIndex := forall i, i < b  -> v (existT _ _ ty).
+  Definition VarIndex := forall i, i < b  -> v of type ty.
 
-  Definition varIndex (regs : Vector.t (v (existT _ _ ty)) b)
+  Definition varIndex (regs : Vector.t (v of type ty) b)
     : VarIndex := fun _ pf  => Vector.nth_order regs pf.
 
   (** One important use case for uniform indexing is the caching of
@@ -90,8 +90,8 @@ Section ArrayUtils.
 
   (** This macro loads the array to the corresponding chached
       variables *)
-  Definition loadCache (arr : v (existT _ _ (array b e ty)))
-    (ch : Vector.t (v (existT _ _ ty)) b) : Repeat (statement v) :=
+  Definition loadCache (arr : v of type (array b e ty))
+    (ch : Vector.t (v of type ty) b) : Repeat (statement v) :=
     (foreach (indices arr)
             (fun i pf => let ix := @exist _ _ i pf in
                       [ Pretty.assignStmt (Vector.nth_order ch pf) (deref arr ix) ]) : code v
@@ -113,8 +113,8 @@ Section ArrayUtils.
 
    *)
 
-  Definition moveBackCache (arr : v (existT _ _ (array b e ty)))
-    (ch : Vector.t (v (existT _ _ ty)) b)  : Repeat (statement v) :=
+  Definition moveBackCache (arr : v of type (array b e ty))
+    (ch : Vector.t (v of type ty) b)  : Repeat (statement v) :=
     (foreach (indices arr)
               (fun i pf => let ix := @exist _ _ i pf in
                            [ Pretty.moveStmt (deref arr ix) (Vector.nth_order ch pf) ])) : code v.
@@ -123,7 +123,7 @@ Section ArrayUtils.
        preserves the values in the cache variables. The cached
        variables can then be reused in the rest of the program.  *)
 
-    Definition backupCache  (arr : v (existT _ _ (array  b e ty))) (ch : VarIndex) : Repeat (statement v) :=
+    Definition backupCache  (arr : v of type (array  b e ty)) (ch : VarIndex) : Repeat (statement v) :=
       (foreach (indices arr)
               (fun i pf => let ix := @exist _ _ i pf in
                            let arrI := deref arr ix in