Created prelude.sail for initial typing environment

Other things:

* Cleaned up several files a bit

* Fixed a bug in the parser where (deinfix |) got parsed as (definfix ||)

* Turned of the irritating auto-indent in sail-mode.el

9 files changed, 347 insertions, 145 deletions

diff --git a/editors/sail-mode.el b/editors/sail-mode.el
index 1fe51137..e1da042b 100644
--- a/editors/sail-mode.el
+++ b/editors/sail-mode.el
@@ -688,8 +688,8 @@ Based on Tuareg mode. See Tuareg mode for usage"
   (setq comment-multi-line t)
   (make-local-variable 'parse-sexp-ignore-comments)
   (setq parse-sexp-ignore-comments nil)
-  (make-local-variable 'indent-line-function)
-  (setq indent-line-function 'sail-indent-command)
+  ;; (make-local-variable 'indent-line-function)
+  ;; setq indent-line-function 'sail-indent-command)
   (unless sail-use-syntax-ppss
     (add-hook 'before-change-functions 'sail-before-change-function nil t))
   (make-local-variable 'normal-auto-fill-function)
diff --git a/lib/prelude.sail b/lib/prelude.sail
new file mode 100644
index 00000000..6eb21f05
--- /dev/null
+++ b/lib/prelude.sail
@@ -0,0 +1,202 @@
+
+val cast forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned
+
+(* Vector access can't actually be properly polymorphic on vector
+   direction because of the ranges being different for each type, so
+   we overload it instead *)
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
+
+(* Type safe vector subrange *)
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+
+overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+
+(* Type safe vector append *)
+val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+
+(* Implicit register dereferencing *)
+val cast forall Type 'a. register<'a> -> 'a effect pure reg_deref
+
+overload vector_access [vector_access_inc; vector_access_dec]
+
+(* Bitvector duplication *)
+val forall Nat 'n. (bit, [:'n:]) -> vector<'n - 1,'n,dec,bit> effect pure duplicate
+
+val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord.
+  (vector<'o,'n,'ord,bit>, [:'m:]) -> vector<'o,'m*'n,'ord,bit> effect pure duplicate_bits
+
+overload (deinfix ^^) [duplicate; duplicate_bits]
+
+(* Bitvector extension *)
+val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord.
+    vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz
+
+val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord.
+    vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts
+
+overload EXTZ [extz]
+overload EXTS [exts]
+
+val forall Type 'a, Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord, 'm >= 'o.
+    vector<'n, 'm, 'ord, 'a> -> vector<'p, 'o, 'ord, 'a> effect pure mask
+
+(* Adjust the start index of a decreasing bitvector *)
+val cast forall Nat 'n, Nat 'm, Nat 'o, 'n >= 'm - 1, 'o >= 'm - 1.
+  vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit>
+  effect pure adjust_dec
+
+(* Various casts from 0 and 1 to bitvectors *)
+val cast forall Nat 'n, Nat 'l, Order 'ord. [:0:] -> vector<'n,'l,'ord,bit> effect pure cast_0_vec
+val cast forall Nat 'n, Nat 'l, Order 'ord. [:1:] -> vector<'n,'l,'ord,bit> effect pure cast_1_vec
+val cast forall Nat 'n, Nat 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec
+
+val cast forall Nat 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool
+val cast bit -> bool effect pure cast_bit_bool
+
+(* MSB *)
+val forall Nat 'n, Nat 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect pure most_significant
+
+(* Arithmetic *)
+
+val forall Nat 'n, Nat 'm.
+    (atom<'n>, atom<'m>) -> atom<'n+'m> effect pure add
+
+val forall Nat 'n, Nat 'o, Nat 'p, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'p, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec
+
+val forall Nat 'n, Nat 'o, Nat 'p, Nat 'q, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'p, 'n, 'ord, bit>) -> range<'q, 2**'n> effect pure add_vec_vec_range
+
+(* FIXME: the parser is broken for 2**... it's just been hacked to work for this common case *)
+val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o <= 2** 'm - 1.
+    (vector<'n, 'm, 'ord, bit>, atom<'o>) -> vector<'n, 'm, 'ord, bit> effect pure add_vec_range
+
+val forall Nat 'n, Nat 'o, Nat 'p, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'p, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure add_overflow_vec
+
+(* but it doesn't parse this
+val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o <= 2** 'm - 1.
+    (vector<'n, 'm, 'ord, bit>, atom<'o>) -> range<'o, 'o+2** 'm> effect pure add_vec_range_range
+    *)
+
+val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o <= 2** 'm - 1.
+    (atom<'o>, vector<'n, 'm, 'ord, bit>) -> vector<'n, 'm, 'ord, bit> effect pure add_range_vec
+
+(* or this
+val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o <= 2** 'm - 1.
+    (atom<'o>, vector<'n, 'm, 'ord, bit>) -> range<'o, 'o+2**'m-1> effect pure add_range_vec_range
+*)
+
+val forall Nat 'o, Nat 'p, Order 'ord.
+    (vector<'o, 'p, 'ord, bit>, bit) -> vector<'o, 'p, 'ord, bit> effect pure add_vec_bit
+
+val forall Nat 'o, Nat 'p, Order 'ord.
+    (bit, vector<'o, 'p, 'ord, bit>) -> vector<'o, 'p, 'ord, bit> effect pure add_bit_vec
+
+val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure sub_exact
+val forall Nat 'n, Nat 'm, Nat 'o, 'o <= 'm - 'n. ([|'n:'m|], [:'o:]) -> [|'n:'m - 'o|] effect pure sub_range
+val forall Nat 'n, Nat 'm, Order 'ord. (vector<'n,'m,'ord,bit>, int) -> vector<'n,'m,'ord,bit> effect pure sub_bv
+
+overload (deinfix +) [
+  add;
+  add_vec;
+  add_vec_vec_range;
+  add_vec_range;
+  add_overflow_vec;
+  add_vec_range_range;
+  add_range_vec;
+  add_range_vec_range;
+  add_vec_bit;
+  add_bit_vec;
+]
+
+overload (deinfix -) [
+  sub_exact;
+  sub_bv;
+  sub_range;
+]
+
+(* Equality *)
+
+(* Sail gives a bunch of overloads for equality, but apparantly also
+gives an equality and inequality for any type 'a, so why bother
+overloading? *)
+
+val forall Type 'a. ('a, 'a) -> bool effect pure eq
+val forall Type 'a. ('a, 'a) -> bool effect pure neq
+
+overload (deinfix ==) [eq]
+overload (deinfix !=) [neq]
+
+(* Boolean operators *)
+val bool -> bool effect pure bool_not
+val (bool, bool) -> bool effect pure bool_or
+val (bool, bool) -> bool effect pure bool_and
+
+overload ~ [bool_not]
+overload (deinfix &) [bool_and]
+overload (deinfix | ) [bool_or]
+
+(*
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange
+
+val forall Nat 'n, Nat 'l, Order 'ord. ([|0:1|], vector<'n,'l,'ord,bit>) -> bool effect pure vec_eq_01_left
+val forall Nat 'n, Nat 'l, Order 'ord. (vector<'n,'l,'ord,bit>, [|0:1|]) -> bool effect pure vec_eq_01_right
+
+val forall Nat 'n, Nat 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_to_vec
+
+val forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure cast_vec_to_range
+
+val forall Type 'a. register<'a> -> 'a effect pure reg_deref
+
+val forall Nat 'n, Nat 'l, Type 'a.
+    (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|], 'a) -> vector<'n,'l,dec,'a>
+    effect pure vector_update_dec
+
+val forall Nat 'n, Nat 'm, Nat 'o, Type 'a, 'o <= 'm.
+    vector<'n,'m,dec,'a> -> vector<'o - 1,'o,dec,'a>
+    effect pure mask_dec
+
+val forall Nat 'n, Nat 'm, Nat 'o, Type 'a, 'o <= 'm.
+    vector<'n,'m,inc,'a> -> vector<0,'o,inc,'a>
+    effect pure mask_inc
+
+val bool -> bool effect pure not
+val (bool, bool) -> bool effect pure bool_or
+val (bool, bool) -> bool effect pure bool_and
+
+val forall Nat 'n. vector<'n,'n,dec,bit> -> bool effect pure cast_dec_bv_to_bool
+
+val bit -> bool effect pure cast_bit_to_bool
+
+val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure sub_exact
+val forall Nat 'n, Nat 'm, Nat 'o, 'o <= 'm - 'n. ([|'n:'m|], [:'o:]) -> [|'n:'m - 'o|] effect pure sub_range
+val forall Nat 'n, Nat 'm, Order 'ord. (vector<'n,'m,'ord,bit>, int) -> vector<'n,'m,'ord,bit> effect pure sub_bv
+
+val [:1:] -> bit effect pure cast_one_bit
+val forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv
+val [:0:] -> bit effect pure cast_zero_bit
+val forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv
+
+val forall Type 'a. ('a, 'a) -> bool effect pure eq_anything
+val forall Type 'a. ('a, 'a) -> bool effect pure neq_anything
+
+val forall Nat 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool
+
+val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord, 'm >= 'n.
+  vector<'o,'n,'ord,bit> -> vector<'p,'m,'ord,bit> effect pure EXTS
+
+val forall Nat 'n, Nat 'm, Order 'ord.
+  (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> vector<'n,'m,'ord,bit>
+  effect pure bv_add
+
+val forall Nat 'n, Nat 'm, Nat 'o, 'n >= 'm - 1, 'o >= 'm - 1.
+  vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit>
+  effect pure ADJUST
+*)
diff --git a/src/ast.ml b/src/ast.ml
index df3098b5..1106c808 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -52,7 +52,7 @@ type 'a annot = l * 'a
 type x = text (* identifier *)
 type ix = text (* infix identifier *)
 
-type 
+type
 base_kind_aux =  (* base kind *)
    BK_type (* kind of types *)
  | BK_nat (* kind of natural number size expressions *)
@@ -60,43 +60,43 @@ base_kind_aux =  (* base kind *)
  | BK_effect (* kind of effect sets *)
 
 
-type 
-base_kind = 
+type
+base_kind =
    BK_aux of base_kind_aux * l
 
 
-type 
+type
 id_aux =  (* Identifier *)
    Id of x
  | DeIid of x (* remove infix status *)
 
 
-type 
+type
 kid_aux =  (* variables with kind, ticked to differntiate from program variables *)
    Var of x
 
 
-type 
+type
 kind_aux =  (* kinds *)
    K_kind of (base_kind) list
 
 
-type 
-id = 
+type
+id =
    Id_aux of id_aux * l
 
 
-type 
-kid = 
+type
+kid =
    Kid_aux of kid_aux * l
 
 
-type 
-kind = 
+type
+kind =
    K_aux of kind_aux * l
 
 
-type 
+type
 nexp_aux =  (* expression of kind Nat, for vector sizes and origins *)
    Nexp_id of id (* identifier, bound by def Nat x = nexp *)
  | Nexp_var of kid (* variable *)
@@ -107,11 +107,11 @@ nexp_aux =  (* expression of kind Nat, for vector sizes and origins *)
  | Nexp_exp of nexp (* exponential *)
  | Nexp_neg of nexp (* For internal use *)
 
-and nexp = 
+and nexp =
    Nexp_aux of nexp_aux * l
 
 
-type 
+type
 base_effect_aux =  (* effect *)
    BE_rreg (* read register *)
  | BE_wreg (* write register *)
@@ -132,41 +132,41 @@ base_effect_aux =  (* effect *)
  | BE_lret (* Local return happened; not user-writable *)
 
 
-type 
-base_effect = 
+type
+base_effect =
    BE_aux of base_effect_aux * l
 
 
-type 
+type
 order_aux =  (* vector order specifications, of kind Order *)
    Ord_var of kid (* variable *)
  | Ord_inc (* increasing (little-endian) *)
  | Ord_dec (* decreasing (big-endian) *)
 
 
-type 
+type
 effect_aux =  (* effect set, of kind Effects *)
    Effect_var of kid
  | Effect_set of (base_effect) list (* effect set *)
 
 
-type 
-order = 
+type
+order =
    Ord_aux of order_aux * l
 
 
-type 
-effect = 
+type
+effect =
    Effect_aux of effect_aux * l
 
 
-type 
+type
 kinded_id_aux =  (* optionally kind-annotated identifier *)
    KOpt_none of kid (* identifier *)
  | KOpt_kind of kind * kid (* kind-annotated variable *)
 
 
-type 
+type
 n_constraint_aux =  (* constraint over kind $_$ *)
    NC_fixed of nexp * nexp
  | NC_bounded_ge of nexp * nexp
@@ -176,34 +176,34 @@ n_constraint_aux =  (* constraint over kind $_$ *)
  | NC_set_subst of nexp * int list
 
 
-type 
-kinded_id = 
+type
+kinded_id =
    KOpt_aux of kinded_id_aux * l
 
 
-type 
-n_constraint = 
+type
+n_constraint =
    NC_aux of n_constraint_aux * l
 
 
-type 
+type
 quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
    QI_id of kinded_id (* An optionally kinded identifier *)
  | QI_const of n_constraint (* A constraint for this type *)
 
 
-type 
-quant_item = 
+type
+quant_item =
    QI_aux of quant_item_aux * l
 
 
-type 
+type
 typquant_aux =  (* type quantifiers and constraints *)
    TypQ_tq of (quant_item) list
  | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
-type 
+type
 lit_aux =  (* Literal constant *)
    L_unit (* $() : _$ *)
  | L_zero (* $_ : _$ *)
@@ -217,12 +217,12 @@ lit_aux =  (* Literal constant *)
  | L_string of string (* string constant *)
 
 
-type 
-typquant = 
+type
+typquant =
    TypQ_aux of typquant_aux * l
 
 
-type 
+type
 typ_aux =  (* Type expressions, of kind $_$ *)
    Typ_wild (* Unspecified type *)
  | Typ_id of id (* Defined type *)
@@ -231,7 +231,7 @@ typ_aux =  (* Type expressions, of kind $_$ *)
  | Typ_tup of (typ) list (* Tuple type *)
  | Typ_app of id * (typ_arg) list (* type constructor application *)
 
-and typ = 
+and typ =
    Typ_aux of typ_aux * l
 
 and typ_arg_aux =  (* Type constructor arguments of all kinds *)
@@ -240,21 +240,21 @@ and typ_arg_aux =  (* Type constructor arguments of all kinds *)
  | Typ_arg_order of order
  | Typ_arg_effect of effect
 
-and typ_arg = 
+and typ_arg =
    Typ_arg_aux of typ_arg_aux * l
 
 
-type 
-lit = 
+type
+lit =
    L_aux of lit_aux * l
 
 
-type 
+type
 typschm_aux =  (* type scheme *)
    TypSchm_ts of typquant * typ
 
 
-type 
+type
 'a pat_aux =  (* Pattern *)
    P_lit of lit (* literal constant pattern *)
  | P_wild (* wildcard *)
@@ -269,27 +269,27 @@ type
  | P_tup of ('a pat) list (* tuple pattern *)
  | P_list of ('a pat) list (* list pattern *)
 
-and 'a pat = 
+and 'a pat =
    P_aux of 'a pat_aux * 'a annot
 
 and 'a fpat_aux =  (* Field pattern *)
    FP_Fpat of id * 'a pat
 
-and 'a fpat = 
+and 'a fpat =
    FP_aux of 'a fpat_aux * 'a annot
 
 
-type 
-typschm = 
+type
+typschm =
    TypSchm_aux of typschm_aux * l
 
 
-type 
-'a reg_id_aux = 
+type
+'a reg_id_aux =
    RI_id of id
 
 
-type 
+type
 'a exp_aux =  (* Expression *)
    E_block of ('a exp) list (* block *)
  | E_nondet of ('a exp) list (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *)
@@ -330,7 +330,7 @@ type
  | E_internal_plet of 'a pat * 'a exp * 'a exp (* This is an internal node, used to distinguised some introduced lets during processing from original ones *)
  | E_internal_return of 'a exp (* For internal use to embed into monad definition *)
 
-and 'a exp = 
+and 'a exp =
    E_aux of 'a exp_aux * 'a annot
 
 and 'a lexp_aux =  (* lvalue expression *)
@@ -342,82 +342,82 @@ and 'a lexp_aux =  (* lvalue expression *)
  | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *)
  | LEXP_field of 'a lexp * id (* struct field *)
 
-and 'a lexp = 
+and 'a lexp =
    LEXP_aux of 'a lexp_aux * 'a annot
 
 and 'a fexp_aux =  (* Field-expression *)
    FE_Fexp of id * 'a exp
 
-and 'a fexp = 
+and 'a fexp =
    FE_aux of 'a fexp_aux * 'a annot
 
 and 'a fexps_aux =  (* Field-expression list *)
    FES_Fexps of ('a fexp) list * bool
 
-and 'a fexps = 
+and 'a fexps =
    FES_aux of 'a fexps_aux * 'a annot
 
 and 'a opt_default_aux =  (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *)
    Def_val_empty
  | Def_val_dec of 'a exp
 
-and 'a opt_default = 
+and 'a opt_default =
    Def_val_aux of 'a opt_default_aux * 'a annot
 
 and 'a pexp_aux =  (* Pattern match *)
    Pat_exp of 'a pat * 'a exp
 
-and 'a pexp = 
+and 'a pexp =
    Pat_aux of 'a pexp_aux * 'a annot
 
 and 'a letbind_aux =  (* Let binding *)
    LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
  | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
 
-and 'a letbind = 
+and 'a letbind =
    LB_aux of 'a letbind_aux * 'a annot
 
 
-type 
-'a reg_id = 
+type
+'a reg_id =
    RI_aux of 'a reg_id_aux * 'a annot
 
 
-type 
+type
 type_union_aux =  (* Type union constructors *)
    Tu_id of id
  | Tu_ty_id of typ * id
 
 
-type 
+type
 name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
    Name_sect_none
  | Name_sect_some of string
 
 
-type 
+type
 effect_opt_aux =  (* Optional effect annotation for functions *)
    Effect_opt_pure (* sugar for empty effect set *)
  | Effect_opt_effect of effect
 
 
-type 
+type
 'a funcl_aux =  (* Function clause *)
    FCL_Funcl of id * 'a pat * 'a exp
 
 
-type 
+type
 rec_opt_aux =  (* Optional recursive annotation for functions *)
    Rec_nonrec (* non-recursive *)
  | Rec_rec (* recursive *)
 
 
-type 
+type
 tannot_opt_aux =  (* Optional type annotation for functions *)
    Typ_annot_opt_some of typquant * typ
 
 
-type 
+type
 'a alias_spec_aux =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
    AL_subreg of 'a reg_id * id
  | AL_bit of 'a reg_id * 'a exp
@@ -425,59 +425,59 @@ type
  | AL_concat of 'a reg_id * 'a reg_id
 
 
-type 
-type_union = 
+type
+type_union =
    Tu_aux of type_union_aux * l
 
 
-type 
+type
 index_range_aux =  (* index specification, for bitfields in register types *)
    BF_single of int (* single index *)
  | BF_range of int * int (* index range *)
  | BF_concat of index_range * index_range (* concatenation of index ranges *)
 
-and index_range = 
+and index_range =
    BF_aux of index_range_aux * l
 
 
-type 
-name_scm_opt = 
+type
+name_scm_opt =
    Name_sect_aux of name_scm_opt_aux * l
 
 
-type 
-effect_opt = 
+type
+effect_opt =
    Effect_opt_aux of effect_opt_aux * l
 
 
-type 
-'a funcl = 
+type
+'a funcl =
    FCL_aux of 'a funcl_aux * 'a annot
 
 
-type 
-rec_opt = 
+type
+rec_opt =
    Rec_aux of rec_opt_aux * l
 
 
-type 
-tannot_opt = 
+type
+tannot_opt =
    Typ_annot_opt_aux of tannot_opt_aux * l
 
 
-type 
-'a alias_spec = 
+type
+'a alias_spec =
    AL_aux of 'a alias_spec_aux * 'a annot
 
 
-type 
+type
 default_spec_aux =  (* Default kinding or typing assumption *)
    DT_kind of base_kind * kid
  | DT_order of order
  | DT_typ of typschm * id
 
 
-type 
+type
 type_def_aux =  (* Type definition body *)
    TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
  | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
@@ -486,7 +486,7 @@ type_def_aux =  (* Type definition body *)
  | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
 
 
-type 
+type
 val_spec_aux =  (* Value type specification *)
    VS_val_spec of typschm * id
  | VS_extern_no_rename of typschm * id
@@ -494,7 +494,7 @@ val_spec_aux =  (* Value type specification *)
  | VS_cast_spec of typschm * id
 
 
-type 
+type
 'a kind_def_aux =  (* Definition body for elements of kind; many are shorthands for type\_defs *)
    KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *)
  | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *)
@@ -504,7 +504,7 @@ type
  | KD_register of kind * id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
 
 
-type 
+type
 'a scattered_def_aux =  (* Function and type union definitions that can be spread across
          a file. Each one must end in $_$ *)
    SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
@@ -514,54 +514,54 @@ type
  | SD_scattered_end of id (* scattered definition end *)
 
 
-type 
+type
 'a fundef_aux =  (* Function definition *)
    FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
 
 
-type 
+type
 'a dec_spec_aux =  (* Register declarations *)
    DEC_reg of typ * id
  | DEC_alias of id * 'a alias_spec
  | DEC_typ_alias of typ * id * 'a alias_spec
 
 
-type 
-'a default_spec = 
+type
+'a default_spec =
    DT_aux of default_spec_aux * l
 
 
-type 
-'a type_def = 
+type
+'a type_def =
    TD_aux of type_def_aux * 'a annot
 
 
-type 
-'a val_spec = 
+type
+'a val_spec =
    VS_aux of val_spec_aux * 'a annot
 
 
-type 
-'a kind_def = 
+type
+'a kind_def =
    KD_aux of 'a kind_def_aux * 'a annot
 
 
-type 
-'a scattered_def = 
+type
+'a scattered_def =
    SD_aux of 'a scattered_def_aux * 'a annot
 
 
-type 
-'a fundef = 
+type
+'a fundef =
    FD_aux of 'a fundef_aux * 'a annot
 
 
-type 
-'a dec_spec = 
+type
+'a dec_spec =
    DEC_aux of 'a dec_spec_aux * 'a annot
 
 
-type 
+type
 'a dec_comm =  (* Top-level generated comments *)
    DC_comm of string (* generated unstructured comment *)
  | DC_comm_struct of 'a def (* generated structured comment *)
@@ -578,7 +578,7 @@ and 'a def =  (* Top-level definition *)
  | DEF_reg_dec of 'a dec_spec (* register declaration *)
  | DEF_comm of 'a dec_comm (* generated comments *)
 
-type 
+type
 'a defs =  (* Definition sequence *)
    Defs of ('a def) list
 
diff --git a/src/constraint.ml b/src/constraint.ml
index 8b28fa4a..f71193b2 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -2,7 +2,7 @@ open Big_int
 open Util
 
 (* ===== Integer Constraints ===== *)
-       
+
 type nexp_op = Plus | Minus | Mult
 
 type nexp =
@@ -14,24 +14,24 @@ type nexp =
 let big_int_op : nexp_op -> big_int -> big_int -> big_int = function
   | Plus -> add_big_int
   | Minus -> sub_big_int
-  | Mult -> mult_big_int 
-              
+  | Mult -> mult_big_int
+
 let rec arith constr =
   let constr' = match constr with
     | NFun (op, x, y) -> NFun (op, arith x, arith y)
     | N2n c -> arith c
     | c -> c
-  in                  
+  in
   match constr' with
   | NFun (op, NConstant x, NConstant y) -> NConstant (big_int_op op x y)
   | N2n (NConstant x) -> NConstant (power_int_positive_big_int 2 x)
   | c -> c
 
 (* ===== Boolean Constraints ===== *)
- 
+
 type constraint_bool_op = And | Or
 
-type constraint_compare_op = Gt | Lt | GtEq | LtEq | Eq | NEq 
+type constraint_compare_op = Gt | Lt | GtEq | LtEq | Eq | NEq
 
 let negate_comparison = function
   | Gt -> LtEq
@@ -40,14 +40,14 @@ let negate_comparison = function
   | LtEq -> Gt
   | Eq -> NEq
   | NEq -> Eq
-                                                            
+
 type 'a constraint_bool =
   | BFun of (constraint_bool_op * 'a constraint_bool * 'a constraint_bool)
   | Not of 'a constraint_bool
   | CFun of (constraint_compare_op * 'a * 'a)
   | Branch of ('a constraint_bool list)
   | Boolean of bool
-       
+
 let rec pairs (xs : 'a list) (ys : 'a list) : ('a * 'b) list =
   match xs with
   | [] -> []
@@ -60,7 +60,7 @@ let rec unbranch : 'a constraint_bool -> 'a constraint_bool list = function
      let xs, ys = unbranch x, unbranch y in
      List.map (fun (z, w) -> BFun (op, z, w)) (pairs xs ys)
   | c -> [c]
-       
+
 (* Apply De Morgan's laws to push all negations to just before integer
    constraints *)
 let rec de_morgan : 'a constraint_bool -> 'a constraint_bool = function
@@ -77,7 +77,7 @@ let rec remove_nots : 'a constraint_bool -> 'a constraint_bool = function
   | BFun (op, x, y) -> BFun (op, remove_nots x, remove_nots y)
   | Not (CFun (c, x, y)) -> CFun (negate_comparison c, x, y)
   | c -> c
-           
+
 (* Apply distributivity so all Or clauses are within And clauses *)
 let rec distrib_step : 'a constraint_bool -> ('a constraint_bool * int) = function
   | BFun (Or, x, BFun (And, y, z)) ->
@@ -91,7 +91,7 @@ let rec distrib_step : 'a constraint_bool -> ('a constraint_bool * int) = functi
   | BFun (op, x, y) ->
      let (x', n) = distrib_step x in
      let (y', m) = distrib_step y in
-     BFun (op, x', y'), n + m 
+     BFun (op, x', y'), n + m
   | c -> (c, 0)
 
 let rec distrib (c : 'a constraint_bool) : 'a constraint_bool =
@@ -111,7 +111,7 @@ let rec flatten_or : 'a constraint_bool -> 'a constraint_leaf list = function
   | CFun comparison -> [LFun comparison]
   | Boolean b -> [LBoolean b]
   | _ -> assert false
-  
+
 let rec flatten : 'a constraint_bool -> 'a constraint_leaf list list = function
   | BFun (And, x, y) -> flatten x @ flatten y
   | Boolean b -> [[LBoolean b]]
@@ -130,7 +130,7 @@ module IntSet = Set.Make(
     let compare = Pervasives.compare
     type t = int
   end)
-                    
+
 let rec int_expr_vars : nexp -> IntSet.t = function
   | NConstant _ -> IntSet.empty
   | NVar v -> IntSet.singleton v
@@ -151,12 +151,12 @@ let constraint_vars constr : IntSet.t =
    lightweight representation of those here. *)
 type sexpr = List of (sexpr list) | Atom of string
 
-let sfun (fn : string) (xs : sexpr list) : sexpr = List (Atom fn :: xs) 
-                                              
+let sfun (fn : string) (xs : sexpr list) : sexpr = List (Atom fn :: xs)
+
 let rec pp_sexpr : sexpr -> string = function
   | List xs -> "(" ^ string_of_list " " pp_sexpr xs ^ ")"
   | Atom x -> x
-                   
+
 let var_decs constr =
   constraint_vars constr
   |> IntSet.elements
@@ -183,7 +183,7 @@ let rec sexpr_of_nexp = function
   | N2n x -> sfun "^" [Atom "2"; sexpr_of_nexp x]
   | NConstant c -> Atom (string_of_big_int c) (* CHECK: do we do negative constants right? *)
   | NVar var -> Atom ("v" ^ string_of_int var)
-              
+
 let rec sexpr_of_cbool = function
   | BFun (And, x, y) -> sfun "and" [sexpr_of_cbool x; sexpr_of_cbool y]
   | BFun (Or, x, y) -> sfun "or" [sexpr_of_cbool x; sexpr_of_cbool y]
@@ -192,7 +192,7 @@ let rec sexpr_of_cbool = function
   | Branch xs -> sfun "BRANCH" (List.map sexpr_of_cbool xs)
   | Boolean true -> Atom "true"
   | Boolean false -> Atom "false"
-                     
+
 let sexpr_of_constraint_leaf = function
   | LFun (op, x, y) -> cop_sexpr op (sexpr_of_nexp x) (sexpr_of_nexp y)
   | LBoolean true -> Atom "true"
@@ -213,7 +213,7 @@ let smtlib_of_constraint constr : string =
 type t = nexp constraint_bool
 
 type smt_result = Unknown of t list | Unsat of t
-                    
+
 let rec call_z3 constraints : smt_result =
   let problems = unbranch constraints in
   let z3_file =
@@ -222,9 +222,9 @@ let rec call_z3 constraints : smt_result =
     |> List.map smtlib_of_constraint
     |> string_of_list "\n" (fun x -> x)
   in
-  
+
   (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *)
-  
+
   let rec input_lines chan = function
     | 0 -> []
     | n ->
@@ -234,7 +234,7 @@ let rec call_z3 constraints : smt_result =
          l :: ls
        end
   in
-  
+
   begin
     let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in
     output_string tmp_chan z3_file;
@@ -260,12 +260,12 @@ let string_of constr =
   |> List.map normalize
   |> List.map (fun c -> smtlib_of_constraint c)
   |> string_of_list "\n" (fun x -> x)
-    
+
 (* ===== Abstract API for building constraints ===== *)
 
 (* These functions are exported from constraint.mli, and ensure that
    the internal representation of constraints remains opaque. *)
-                    
+
 let implies (x : t) (y : t) : t =
   BFun (Or, Not x, y)
 
@@ -296,9 +296,9 @@ let neq x y : t = CFun (NEq, x, y)
 let pow2 x : nexp = N2n x
 
 let add x y : nexp = NFun (Plus, x, y)
-                                     
+
 let sub x y : nexp = NFun (Minus, x, y)
-                                     
+
 let mult x y : nexp = NFun (Mult, x, y)
 
 let constant (x : big_int) : nexp = NConstant x
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index cfb09bf5..8b52b2ab 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -419,7 +419,7 @@ val_spec_aux =  (* Value type specification *)
  | VS_extern_no_rename of typschm * id
  | VS_extern_spec of typschm * id * string
  | VS_cast_spec of typschm * id
-                                      
+
 
 type 
 kind_def_aux =  (* Definition body for elements of kind; many are shorthands for type\_defs *)
diff --git a/src/parser.mly b/src/parser.mly
index 6cf954ef..0240e368 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -226,7 +226,7 @@ id:
   | Lparen Deinfix AmpAmp Rparen
     { idl (DeIid($3)) }
   | Lparen Deinfix Bar Rparen
-    { idl (DeIid("||")) }
+    { idl (DeIid("|")) }
   | Lparen Deinfix BarBar Rparen
     { idl (DeIid("||")) }
   | Lparen Deinfix CarrotCarrot Rparen
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index f33a7db1..4093e84c 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -122,7 +122,7 @@ let string_of_id = function
 let deinfix = function
   | Id_aux (Id v, l) -> Id_aux (DeIid v, l)
   | Id_aux (DeIid v, l) -> Id_aux (DeIid v, l)
-                                               
+
 let string_of_kid = function
   | Kid_aux (Var v, _) -> v
 
@@ -313,7 +313,7 @@ let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown)
 let mk_typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown)
 let mk_id str = Id_aux (Id str, Parse_ast.Unknown)
 let mk_infix_id str = Id_aux (DeIid str, Parse_ast.Unknown)
-                       
+
 let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown)
 
 let unit_typ = mk_id_typ (mk_id "unit")
@@ -345,7 +345,7 @@ and nc_subst_nexp_aux l sv subst = function
      if Kid.compare kid sv = 0
      then NC_set_subst (Nexp_aux (subst, Parse_ast.Unknown), ints)
      else set_nc
-  | NC_set_subst (nexp, ints) -> NC_set_subst (nexp_subst sv subst nexp, ints) 
+  | NC_set_subst (nexp, ints) -> NC_set_subst (nexp_subst sv subst nexp, ints)
 
 let rec typ_subst_nexp sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_nexp_aux sv subst typ, l)
 and typ_subst_nexp_aux sv subst = function
@@ -788,7 +788,7 @@ end = struct
     | NC_bounded_le (n1, n2) -> wf_nexp env n1; wf_nexp env n2
     | NC_nat_set_bounded (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *)
     | NC_set_subst (nexp, ints) -> wf_nexp env nexp
-                                          
+
   let get_constraints env = env.constraints
 
   let add_constraint (NC_aux (_, l) as constr) env =
@@ -1094,7 +1094,7 @@ let subtyp l env typ1 typ2 =
 
 let typ_equality l env typ1 typ2 =
   subtyp l env typ1 typ2; subtyp l env typ2 typ1
-                 
+
 let rec nexp_frees (Nexp_aux (nexp, l)) =
   match nexp with
   | Nexp_id _ -> typ_error l "Unimplemented Nexp_id in nexp_frees"
@@ -1271,7 +1271,7 @@ let lvector_typ env l typ =
      vector_typ (nconstant 0) l ord typ
   | Ord_aux (Ord_dec, _) as ord ->
      vector_typ (nminus l (nconstant 1)) l ord typ
-                                         
+
 let infer_lit env (L_aux (lit_aux, l) as lit) =
   match lit_aux with
   | L_unit -> mk_typ (Typ_id (mk_id "unit"))
@@ -1364,7 +1364,7 @@ let typ_of (E_aux (_, (_, tannot))) = match tannot with
 let pat_typ_of (P_aux (_, (_, tannot))) = match tannot with
   | Some (_, typ) -> typ
   | None -> assert false
-                   
+
 let crule r env exp typ =
   incr depth;
   typ_print ("Check " ^ string_of_exp exp ^ " <= " ^ string_of_typ typ);
diff --git a/src/type_check_new.mli b/src/type_check_new.mli
index e8685bb2..a77b2cd0 100644
--- a/src/type_check_new.mli
+++ b/src/type_check_new.mli
@@ -68,13 +68,13 @@ module Env : sig
   val fresh_kid : t -> kid
   val expand_synonyms : t -> typ -> typ
   val no_casts : t -> t
-  val empty : t                                   
+  val empty : t
 end
 
 type tannot = (Env.t * typ) option
 
 val check_exp : Env.t -> unit exp -> typ -> tannot exp
-               
+
 val check : Env.t -> 'a defs -> tannot defs * Env.t
 
 val initial_env : Env.t
diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail
index 5c48db77..8857bd18 100644
--- a/test/typecheck/pass/vector_subrange_gen.sail
+++ b/test/typecheck/pass/vector_subrange_gen.sail
@@ -11,7 +11,7 @@ val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure minus
 default Order inc
 
 val forall 'n, 'm, 'n >= 5. bit['n] -> bit['n - 2] effect pure test
-    
+
 function forall 'n, 'n >= 5. bit['n - 2] test v =
 {
   z := vector_subrange(v, 0, minus(sizeof 'n, 2));