diff options
| -rw-r--r-- | lib/mono_rewrites.sail | 32 | ||||
| -rw-r--r-- | src/monomorphise.ml | 6 |
2 files changed, 21 insertions, 17 deletions
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index 144b7ae0..fd1d1b23 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -1,26 +1,30 @@ -(* Definitions for use with the -mono_rewrites option *) +/* Definitions for use with the -mono_rewrites option */ -(* External definitions not in the usual asl prelude *) +/* External definitions not in the usual asl prelude */ -val "shiftleft" : forall 'n 'o ('ord : Order). - (vector('o, 'n, 'ord, bit), int) -> vector('o, 'n, 'ord, bit) effect pure +infix 6 << + +val "shiftleft" : forall 'n ('ord : Order). + (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure overload operator << = {shiftleft} -val "shiftright" : forall 'n 'o ('ord : Order). - (vector('o, 'n, 'ord, bit), int) -> vector('o, 'n, 'ord, bit) effect pure +infix 6 >> + +val "shiftright" : forall 'n ('ord : Order). + (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure overload operator >> = {shiftright} -val "extz" : forall 'n 'm 'o 'p. (atom('p),atom('m),vector('o, 'n, dec, bit)) -> vector('p, 'm, dec, bit) effect pure -val extzv : forall 'n 'm 'o 'p. vector('o, 'n, dec, bit) -> vector('p, 'm, dec, bit) effect pure -function extzv(v) = extz(sizeof('p), sizeof('m),v) +val "extz" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure +function extzv(v) = extz(sizeof('m),v) -val "exts" : forall 'n 'm 'o 'p. (atom('p),atom('m),vector('o, 'n, dec, bit)) -> vector('p, 'm, dec, bit) effect pure -val extsv : forall 'n 'm 'o 'p. vector('o, 'n, dec, bit) -> vector('p, 'm, dec, bit) effect pure -function extsv(v) = exts(sizeof('p), sizeof('m),v) +val "exts" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +val extsv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure +function extsv(v) = exts(sizeof('m),v) -(* Definitions for the rewrites *) +/* Definitions for the rewrites */ val slice_mask : forall 'n, 'n >= 0. (int, int) -> bits('n) effect pure function slice_mask(i,l) = @@ -59,7 +63,7 @@ function slice_zeros_concat (xs, i, l, l') = { extzv(xs) << l' } -(* Assumes initial vectors are of equal size *) +/* Assumes initial vectors are of equal size */ val subrange_subrange_eq : forall 'n, 'n >= 0. (bits('n), int, int, bits('n), int, int) -> bool effect pure diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 3ea156d0..9098f03d 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -341,7 +341,7 @@ let split_src_type id ty (TypQ_aux (q,ql)) = List.concat insts, Typ_aux (Typ_tup tys,l)) (cross' tys) in (kidset_bigunion vars, insttys) | Typ_app (Id_aux (Id "vector",_), - [_;Typ_arg_aux (Typ_arg_nexp sz,_); + [Typ_arg_aux (Typ_arg_nexp sz,_); _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> (KidSet.of_list (size_nvars_nexp sz), [[],typ]) | Typ_app (_, tas) -> @@ -1312,7 +1312,7 @@ let split_defs continue_anyway splits defs = [L_zero; L_one] | _ -> cannot ("don't know about type " ^ string_of_id id)) - | Typ_app (Id_aux (Id "vector",_), [_;Typ_arg_aux (Typ_arg_nexp len,_);_;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> + | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp len,_);_;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> (match len with | Nexp_aux (Nexp_constant sz,_) -> let lits = make_vectors (Big_int.to_int sz) in @@ -1706,7 +1706,7 @@ let rec sizes_of_typ (Typ_aux (t,l)) = | Typ_exist (kids,_,typ) -> List.fold_left (fun s k -> KidSet.remove k s) (sizes_of_typ typ) kids | Typ_app (Id_aux (Id "vector",_), - [_;Typ_arg_aux (Typ_arg_nexp size,_); + [Typ_arg_aux (Typ_arg_nexp size,_); _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> KidSet.of_list (size_nvars_nexp size) | Typ_app (_,tas) -> |