Merge branch 'master' of bitbucket.org:Peter_Sewell/l2

Conflicts:
	src/Makefile

17 files changed, 836 insertions, 78 deletions

diff --git a/src/Makefile b/src/Makefile
index b67d9f5e..1e9ca694 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -17,9 +17,12 @@ test: sail interpreter
 	ocamlbuild test/run_tests.native
 	./run_tests.native
 
-LEM = ~/bitbucket/lem/lem
-LEMLIBOCAML = ~/bitbucket/lem/ocaml-lib/
-ELFDIR= ~/bitbucket/linksem
+THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST)))
+BITBUCKET_ROOT=$(realpath $(dir $(THIS_MAKEFILE))../..)
+
+LEM = $(BITBUCKET_ROOT)/lem/lem
+LEMLIBOCAML = $(BITBUCKET_ROOT)/lem/ocaml-lib
+ELFDIR= $(BITBUCKET_ROOT)/linksem
 
 elf:
 	make -C $(ELFDIR)
@@ -45,9 +48,7 @@ _build/mips.lem: _build/mips.sail ./sail.native
 	$(LEM) -only_changed_output -ocaml -lib lem_interp/ $<
 
 run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml interpreter
-	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package zarith -package num  -package uint -I $(LEMLIBOCAML) -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)extract.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml  -o run_mips.native
-
-#-package batteries
+	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml  -o run_mips.native
 
 mips: elf run_mips.native
 
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 80008453..df46b0cc 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -13,17 +13,6 @@ let id_to_string (Id_aux(id,l)) =
 
 let var_to_string (Kid_aux(Var v,l)) = v
 
-(*placeholder, write in type_internal*)
-let rec kind_to_string kind = match kind.k with
-  | K_Nat -> "Nat"
-  | K_Typ -> "Type"
-  | K_Ord -> "Order"
-  | K_Efct -> "Effect"
-  | K_infer -> "Infer"
-  | K_Val -> "Val"
-  | K_Lam (kinds,kind) -> "Lam ... -> " ^ (kind_to_string kind)
-
-
 let typquant_to_quantkinds k_env typquant = 
   match typquant with
   | TypQ_aux(tq,_) ->
@@ -804,11 +793,13 @@ let rec to_ast_defs_helper envs partial_defs = function
               | No_def -> defs,envs,partial_defs
               | Def_place_holder(id,l) -> 
                 (match (def_in_progress id partial_defs) with
-                | None -> raise (Reporting_basic.err_unreachable l "Id stored in place holder not retrievable from partial defs")
-                | Some(d,k) -> 
-                  if (snd !d) 
-                  then (fst !d) :: defs, envs, partial_defs
-                  else typ_error l "Scattered type definition never ended" (Some id) None None))                
+                 | None ->
+                   raise
+                     (Reporting_basic.err_unreachable l "Id stored in place holder not retrievable from partial defs")
+                 | Some(d,k) -> 
+                   if (snd !d) 
+                   then (fst !d) :: defs, envs, partial_defs
+                   else typ_error l "Scattered type definition never ended" (Some id) None None))                
 
 let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (def_ord : order) (Parse_ast.Defs(defs)) =
   let defs,(_,k_env,def_ord),partial_defs = to_ast_defs_helper (default_names,kind_env,def_ord) [] defs in
diff --git a/src/initial_check_full_ast.ml b/src/initial_check_full_ast.ml
new file mode 100644
index 00000000..23a2f264
--- /dev/null
+++ b/src/initial_check_full_ast.ml
@@ -0,0 +1,663 @@
+open Type_internal
+open Ast
+open Type_internal
+
+(*Envs is a tuple of used names (currently unused), map from id to kind, default order for vector types and literal vectors *)
+type envs = Nameset.t * kind Envmap.t * Ast.order 
+type 'a envs_out = 'a * envs
+
+let id_to_string (Id_aux(id,l)) =
+  match id with | Id(x) | DeIid(x) -> x
+
+let var_to_string (Kid_aux(Var v,l)) = v
+
+let typquant_to_quantkinds k_env typquant = 
+  match typquant with
+  | TypQ_aux(tq,_) ->
+    (match tq with
+    | TypQ_no_forall -> []
+    | TypQ_tq(qlist) ->
+      List.fold_right
+        (fun (QI_aux(qi,_)) rst ->
+          match qi with
+          | QI_const _ -> rst
+          | QI_id(ki) -> begin
+            match ki with 
+            | KOpt_aux(KOpt_none(v),l) | KOpt_aux(KOpt_kind(_,v),l) -> 
+              (match Envmap.apply k_env (var_to_string v) with
+              | Some(typ) -> typ::rst
+              | None -> raise (Reporting_basic.err_unreachable l "Envmap didn't get an entry during typschm processing"))
+          end)
+        qlist
+        [])
+
+let typ_error l msg opt_id opt_var opt_kind =
+  let full_msg = (msg ^
+                  (match opt_id, opt_var, opt_kind with
+                   | Some(id),None,Some(kind) -> (id_to_string id) ^ " of " ^ (kind_to_string kind)
+                   | Some(id),None,None -> ": " ^ (id_to_string id)
+                   | None,Some(v),Some(kind) -> (var_to_string v) ^ " of " ^ (kind_to_string kind)
+                   | None,Some(v),None -> ": " ^ (var_to_string v)
+                   | None,None,Some(kind) -> " " ^ (kind_to_string kind)
+                   | _ -> "")) in
+  Reporting_basic.report_error (Reporting_basic.Err_type(l, full_msg))
+                
+let to_base_kind (BK_aux(k,l')) =
+  match k with
+  | BK_type -> BK_aux(BK_type,l'), { k = K_Typ}
+  | BK_nat -> BK_aux(BK_nat,l'), { k = K_Nat }
+  | BK_order -> BK_aux(BK_order,l'), { k = K_Ord }
+  | BK_effect -> BK_aux(BK_effect,l'), { k = K_Efct }
+
+let to_kind (k_env : kind Envmap.t) (K_aux(K_kind(klst),l)) : (Ast.kind * kind) =
+  match klst with
+  | [] -> raise (Reporting_basic.err_unreachable l "Kind with empty kindlist encountered")
+  | [k] -> let k_ast,k_typ = to_base_kind k in
+           K_aux(K_kind([k_ast]),l), k_typ
+  | ks -> let k_pairs = List.map to_base_kind ks in
+          let reverse_typs = List.rev (List.map snd k_pairs) in
+          let ret,args = List.hd reverse_typs, List.rev (List.tl reverse_typs) in
+          match ret.k with
+          | K_Typ -> K_aux(K_kind(List.map fst k_pairs), l), { k = K_Lam(args,ret) }
+          | _ -> typ_error l "Type constructor must have an -> kind ending in Type" None None None
+
+let rec to_typ (k_env : kind Envmap.t) (def_ord : Ast.order) (t: Ast.typ) : Ast.typ =
+  match t with
+  | Typ_aux(t,l) ->
+    Typ_aux( (match t with 
+              | Typ_id(id) -> 
+                let mk = Envmap.apply k_env (id_to_string id) in
+                (match mk with
+                 | Some(k) ->
+                   (match k.k with
+                    | K_Typ -> Typ_id id
+                    | K_infer -> k.k <- K_Typ; Typ_id id
+                    | _ -> typ_error l "Required an identifier with kind Type, encountered " (Some id) None (Some k))
+                 | None -> typ_error l "Encountered an unbound type identifier" (Some id) None None)
+              | Typ_var(v) -> 
+                let mk = Envmap.apply k_env (var_to_string v) in
+                (match mk with
+                 | Some(k) -> (match k.k with
+                     | K_Typ -> Typ_var v
+                     | K_infer -> k.k <- K_Typ; Typ_var v
+                     | _ -> typ_error l "Required a variable with kind Type, encountered " None (Some v) (Some k))
+                | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
+              | Typ_fn(arg,ret,efct) -> Typ_fn( (to_typ k_env def_ord arg),
+                                                (to_typ k_env def_ord ret),
+                                                (to_effects k_env efct))
+              | Typ_tup(typs) -> Typ_tup( List.map (to_typ k_env def_ord) typs)
+              | Typ_app(id,typs) ->
+                let k = Envmap.apply k_env (id_to_string id) in
+                (match k with 
+                 | Some({k = K_Lam(args,t)}) -> 
+                   if ((List.length args) = (List.length typs))
+                   then
+                     Typ_app(id,(List.map2 (fun k a -> (to_typ_arg k_env def_ord k a)) args typs))
+                   else typ_error l "Type constructor given incorrect number of arguments" (Some id) None None
+                 | None ->
+                   typ_error l "Required a type constructor, encountered an unbound identifier" (Some id) None None
+                 | _ -> typ_error l "Required a type constructor, encountered a base kind variable" (Some id) None None)
+              | _ ->
+                typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None None
+      ), l)
+
+and to_nexp (k_env : kind Envmap.t) (n: Ast.nexp) : Ast.nexp =
+  match n with
+  | Nexp_aux(t,l) ->
+    (match t with
+    | Nexp_var(v) ->                 
+      let mk = Envmap.apply k_env (var_to_string v) in
+      (match mk with
+       | Some(k) -> Nexp_aux((match k.k with
+           | K_Nat -> Nexp_var v
+           | K_infer -> k.k <- K_Nat; Nexp_var v
+           | _ -> typ_error l "Required a variable with kind Nat, encountered " None (Some v) (Some k)),l)
+       | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
+    | Nexp_constant(i) -> Nexp_aux(Nexp_constant(i),l)
+    | Nexp_sum(t1,t2) ->
+      let n1 = to_nexp k_env t1 in
+      let n2 = to_nexp k_env t2 in
+      Nexp_aux(Nexp_sum(n1,n2),l)
+    | Nexp_exp(t1) -> Nexp_aux(Nexp_exp(to_nexp k_env t1),l)
+    | Nexp_neg(t1) -> Nexp_aux(Nexp_neg(to_nexp k_env t1),l)
+    | Nexp_times(t1,t2) ->
+      let n1 = to_nexp k_env t1 in
+      let n2 = to_nexp k_env t2 in
+      Nexp_aux(Nexp_times(n1,n2),l)
+    | Nexp_minus(t1,t2) ->
+      let n1 = to_nexp k_env t1 in
+      let n2 = to_nexp k_env t2 in
+      Nexp_aux(Nexp_minus(n1,n2),l))
+    
+and to_order (k_env : kind Envmap.t) (def_ord : Ast.order) (o: Ast.order) : Ast.order =
+  match o with
+  | Ord_aux(t,l) ->
+    (match t with
+      | Ord_var(v) -> 
+        let mk = Envmap.apply k_env (var_to_string v) in
+        (match mk with
+         | Some(k) -> (match k.k with
+             | K_Ord -> Ord_aux(Ord_var v, l)
+             | K_infer -> k.k <- K_Ord; Ord_aux(Ord_var v,l)
+             | _ -> typ_error l "Required a variable with kind Order, encountered " None (Some v) (Some k))
+         | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
+      | Ord_inc -> Ord_aux(Ord_inc,l)
+      | Ord_dec -> Ord_aux(Ord_dec,l)
+    )
+
+and to_effects (k_env : kind Envmap.t) (e : Ast.effect) : Ast.effect =
+  match e with
+  | Effect_aux(t,l) ->
+    Effect_aux( (match t with
+        | Effect_var(v) ->  
+          let mk = Envmap.apply k_env (var_to_string v) in
+          (match mk with
+           | Some(k) -> (match k.k with
+               | K_Efct -> Effect_var v
+               | K_infer -> k.k <- K_Efct; Effect_var v
+               | _ -> typ_error l "Required a variable with kind Effect, encountered " None (Some v) (Some k))
+           | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
+        | Effect_set(effects) -> Effect_set(effects)
+    ), l)
+
+and to_typ_arg (k_env : kind Envmap.t) (def_ord : Ast.order) (kind : kind) (arg : Ast.typ_arg) : Ast.typ_arg =
+  let l,ta = (match arg with Typ_arg_aux(ta,l) -> l,ta) in
+  Typ_arg_aux (  
+    (match kind.k,ta with 
+    | K_Typ,Typ_arg_typ t     -> Typ_arg_typ (to_typ k_env def_ord t)
+    | K_Nat,Typ_arg_nexp n    -> Typ_arg_nexp (to_nexp k_env n)
+    | K_Ord,Typ_arg_order o   -> Typ_arg_order (to_order k_env def_ord o)
+    | K_Efct,Typ_arg_effect e -> Typ_arg_effect (to_effects k_env e)
+    | (K_Lam _ | K_infer | K_Val),_ -> 
+      raise (Reporting_basic.err_unreachable l "To_ast_typ_arg received Lam kind or infer kind")
+    | _ -> typ_error l "Kind declaration and kind of type argument don't match here" None None (Some kind)),
+    l)
+
+let to_nexp_constraint (k_env : kind Envmap.t) (c : n_constraint) : n_constraint =
+  match c with 
+  | NC_aux(nc,l) ->
+    NC_aux( (match nc with
+             | NC_fixed(t1,t2) -> 
+               let n1 = to_nexp k_env t1 in
+               let n2 = to_nexp k_env t2 in
+               NC_fixed(n1,n2)
+             | NC_bounded_ge(t1,t2) ->
+               let n1 = to_nexp k_env t1 in
+               let n2 = to_nexp k_env t2 in
+               NC_bounded_ge(n1,n2)
+             | NC_bounded_le(t1,t2) ->
+               let n1 = to_nexp k_env t1 in
+               let n2 = to_nexp k_env t2 in
+               NC_bounded_le(n1,n2)
+             | NC_nat_set_bounded(id,bounds) ->
+               NC_nat_set_bounded(id, bounds)
+    ), l)               
+
+(* Transforms a typquant while building first the kind environment of declared variables, and also the kind environment in context *)
+let to_typquant (k_env: kind Envmap.t) (tq : typquant) : typquant * kind Envmap.t * kind Envmap.t =
+  let opt_kind_to_ast k_env local_names local_env (KOpt_aux(ki,l)) =
+    let v, key, kind, ktyp =
+      match ki with
+      | KOpt_none(v) ->
+        let key = var_to_string v in
+        let kind,ktyp =
+          if (Envmap.in_dom key k_env) then None,(Envmap.apply k_env key)
+          else None,(Some{ k = K_infer }) in
+        v,key,kind, ktyp
+      | KOpt_kind(k,v) ->
+        let key = var_to_string v in
+        let kind,ktyp = to_kind k_env k in
+        v,key,Some(kind),Some(ktyp)
+    in
+    if (Nameset.mem key local_names)
+    then typ_error l "Encountered duplicate name in type scheme" None (Some v) None
+    else 
+      let local_names = Nameset.add key local_names in
+      let kopt,k_env,k_env_local = (match kind,ktyp with
+        | Some(k),Some(kt) -> KOpt_kind(k,v), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt))
+        | None, Some(kt) -> KOpt_none(v), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt))
+        | _ -> raise (Reporting_basic.err_unreachable l "Envmap in dom is true but apply gives None")) in
+      KOpt_aux(kopt,l),k_env,local_names,k_env_local
+  in
+  match tq with
+  | TypQ_aux(tqa,l) ->
+    (match tqa with
+    | TypQ_no_forall -> TypQ_aux(TypQ_no_forall,l), k_env, Envmap.empty
+    | TypQ_tq(qlist) ->
+      let rec to_q_items k_env local_names local_env = function
+        | [] -> [],k_env,local_env
+        | q::qs ->
+          (match q with
+           | QI_aux(qi,l) ->
+             (match qi with
+              | QI_const(n_const) -> 
+                let c = QI_aux(QI_const(to_nexp_constraint k_env n_const),l) in
+                        let qis,k_env,local_env = to_q_items k_env local_names local_env qs in
+                        (c::qis),k_env,local_env
+                      | QI_id(kid) ->
+                        let kid,k_env,local_names,local_env = opt_kind_to_ast k_env local_names local_env kid in
+                        let c = QI_aux(QI_id(kid),l) in
+                        let qis,k_env,local_env = to_q_items k_env local_names local_env qs in
+                        (c::qis),k_env,local_env))      
+      in
+      let lst,k_env,local_env = to_q_items k_env Nameset.empty Envmap.empty qlist in
+      TypQ_aux(TypQ_tq(lst),l), k_env, local_env)
+
+let to_typschm (k_env:kind Envmap.t) (def_ord:Ast.order) (tschm:Ast.typschm)
+  :Ast.typschm * kind Envmap.t * kind Envmap.t =
+  match tschm with
+  | TypSchm_aux(ts,l) -> 
+    (match ts with | TypSchm_ts(tquant,t) ->
+      let tq,k_env,local_env = to_typquant k_env tquant in
+      let typ = to_typ k_env def_ord t in
+      TypSchm_aux(TypSchm_ts(tq,typ),l),k_env,local_env)
+
+let rec to_pat (k_env : kind Envmap.t) (def_ord : Ast.order) (P_aux(pat,(l,_)) : tannot pat) : tannot pat = 
+  P_aux(
+    (match pat with 
+    | P_lit(lit) -> P_lit(lit)
+    | P_wild -> P_wild
+    | P_as(pat,id) -> P_as(to_pat k_env def_ord pat, id)
+    | P_typ(typ,pat) -> P_typ(to_typ k_env def_ord typ,to_pat k_env def_ord pat)
+    | P_id(id) -> P_id(id)
+    | P_app(id,pats) ->
+      if pats = [] 
+      then P_id (id)
+      else P_app(id, List.map (to_pat k_env def_ord) pats)
+    | P_record(fpats,_) -> 
+      P_record(List.map 
+                 (fun (FP_aux(FP_Fpat(id,fp),(l,_))) -> 
+                      FP_aux(FP_Fpat(id, to_pat k_env def_ord fp),(l,NoTyp)))
+                 fpats, false)
+    | P_vector(pats) -> P_vector(List.map (to_pat k_env def_ord) pats)
+    | P_vector_indexed(ipats) -> P_vector_indexed(List.map (fun (i,pat) -> i,to_pat k_env def_ord pat) ipats)
+    | P_vector_concat(pats) -> P_vector_concat(List.map (to_pat k_env def_ord) pats)
+    | P_tup(pats) -> P_tup(List.map (to_pat k_env def_ord) pats)
+    | P_list(pats) -> P_list(List.map (to_pat k_env def_ord) pats)
+    ), (l,NoTyp))
+
+
+let rec to_letbind (k_env : kind Envmap.t) (def_ord : Ast.order) (LB_aux(lb,(l,_)) : tannot letbind) : tannot letbind =
+  LB_aux(
+    (match lb with
+    | LB_val_explicit(typschm,pat,exp) ->
+      let typsch, k_env, _  = to_typschm k_env def_ord typschm in
+      LB_val_explicit(typsch,to_pat k_env def_ord pat, to_exp k_env def_ord exp)
+    | LB_val_implicit(pat,exp) ->
+      LB_val_implicit(to_pat k_env def_ord pat, to_exp k_env def_ord exp)
+    ), (l,NoTyp))
+
+and to_exp (k_env : kind Envmap.t) (def_ord : Ast.order) (E_aux(exp,(l,_)) :  exp) : exp = 
+  E_aux(
+    (match exp with
+    | E_block(exps) -> E_block(List.map (to_exp k_env def_ord) exps)
+    | E_nondet(exps) -> E_nondet(List.map (to_exp k_env def_ord) exps)
+    | E_id(id) -> E_id(id)
+    | E_lit(lit) -> E_lit(lit)
+    | E_cast(typ,exp) -> E_cast(to_typ k_env def_ord typ, to_exp k_env def_ord exp)
+    | E_app(f,args) -> 
+      (match List.map (to_exp k_env def_ord) args with
+        | [] -> E_app(f, [])
+        | [E_aux(E_tuple(exps),_)] -> E_app(f, exps)
+        | exps -> E_app(f, exps))
+    | E_app_infix(left,op,right) -> 
+      E_app_infix(to_exp k_env def_ord left, op, to_exp k_env def_ord right)
+    | E_tuple(exps) -> E_tuple(List.map (to_exp k_env def_ord) exps)
+    | E_if(e1,e2,e3) -> E_if(to_exp k_env def_ord e1, to_exp k_env def_ord e2, to_exp k_env def_ord e3)
+    | E_for(id,e1,e2,e3,atyp,e4) -> 
+      E_for(id,to_exp k_env def_ord e1, to_exp k_env def_ord e2,
+            to_exp k_env def_ord e3,to_order k_env def_ord atyp, to_exp k_env def_ord e4)
+    | E_vector(exps) -> E_vector(List.map (to_exp k_env def_ord) exps)
+    | E_vector_indexed(iexps,Def_val_aux(default,(dl,_))) -> 
+      E_vector_indexed (to_iexps true k_env def_ord iexps, 
+                        Def_val_aux((match default with
+                            | Def_val_empty -> Def_val_empty
+                            | Def_val_dec e -> Def_val_dec (to_exp k_env def_ord e)),(dl,NoTyp)))
+    | E_vector_access(vexp,exp) -> E_vector_access(to_exp k_env def_ord vexp, to_exp k_env def_ord exp)
+    | E_vector_subrange(vex,exp1,exp2) -> 
+      E_vector_subrange(to_exp k_env def_ord vex, to_exp k_env def_ord exp1, to_exp k_env def_ord exp2)
+    | E_vector_update(vex,exp1,exp2) -> 
+      E_vector_update(to_exp k_env def_ord vex, to_exp k_env def_ord exp1, to_exp k_env def_ord exp2)
+    | E_vector_update_subrange(vex,e1,e2,e3) -> 
+      E_vector_update_subrange(to_exp k_env def_ord vex, to_exp k_env def_ord e1, 
+                               to_exp k_env def_ord e2, to_exp k_env def_ord e3)
+    | E_vector_append(e1,e2) -> E_vector_append(to_exp k_env def_ord e1,to_exp k_env def_ord e2)
+    | E_list(exps) -> E_list(List.map (to_exp k_env def_ord) exps)
+    | E_cons(e1,e2) -> E_cons(to_exp k_env def_ord e1, to_exp k_env def_ord e2)
+    | E_record(fexps) ->
+      (match to_fexps true k_env def_ord fexps with
+       | Some(fexps) -> E_record(fexps)
+       | None -> raise (Reporting_basic.err_unreachable l "to_fexps with true returned none"))
+    | E_record_update(exp,fexps) -> 
+      (match to_fexps true k_env def_ord fexps with
+      | Some(fexps) -> E_record_update(to_exp k_env def_ord exp, fexps)
+      | _ -> raise (Reporting_basic.err_unreachable l "to_fexps with true returned none"))
+    | E_field(exp,id) -> E_field(to_exp k_env def_ord exp, id)
+    | E_case(exp,pexps) -> E_case(to_exp k_env def_ord exp, List.map (to_case k_env def_ord) pexps)
+    | E_let(leb,exp) -> E_let(to_letbind k_env def_ord leb, to_exp k_env def_ord exp)
+    | E_assign(lexp,exp) -> E_assign(to_lexp k_env def_ord lexp, to_exp k_env def_ord exp)
+    | E_exit exp -> E_exit(to_exp k_env def_ord exp)
+    | E_assert(cond,msg) -> E_assert(to_exp k_env def_ord cond, to_exp k_env def_ord msg)
+    | E_comment s -> E_comment s
+    | E_comment_struc e -> E_comment_struc e
+    | _ -> raise (Reporting_basic.err_unreachable l "to_exp given internal node")
+    ), (l,NoTyp))
+
+and to_lexp (k_env : kind Envmap.t) (def_ord : Ast.order) (LEXP_aux(exp,(l,_)) : tannot lexp) : tannot lexp = 
+  LEXP_aux(
+    (match exp with
+    | LEXP_id(id) -> LEXP_id(id)
+    | LEXP_memory(f,args) -> 
+      (match List.map (to_exp k_env def_ord) args with
+       | [] -> LEXP_memory(f,[])
+       | [E_aux(E_tuple exps,_)] -> LEXP_memory(f,exps)
+       | args -> LEXP_memory(f, args))
+    | LEXP_cast(typ,id) ->
+      LEXP_cast(to_typ k_env def_ord typ, id)
+    | LEXP_vector(vexp,exp) -> LEXP_vector(to_lexp k_env def_ord vexp, to_exp k_env def_ord exp)
+    | LEXP_vector_range(vexp,exp1,exp2) -> 
+      LEXP_vector_range(to_lexp k_env def_ord vexp, to_exp k_env def_ord exp1, to_exp k_env def_ord exp2)
+    | LEXP_field(fexp,id) -> LEXP_field(to_lexp k_env def_ord fexp, id))
+  , (l,NoTyp))
+
+and to_case (k_env : kind Envmap.t) (def_ord : Ast.order) (Pat_aux(pex,(l,_)) : tannot pexp) : tannot pexp =
+  match pex with 
+  | Pat_exp(pat,exp) -> Pat_aux(Pat_exp(to_pat k_env def_ord pat, to_exp k_env def_ord exp),(l,NoTyp))
+
+and to_fexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:Ast.order) (FES_aux (FES_Fexps(fexps,_),(l,_)))
+  : tannot fexps option =
+  let wrap fs = FES_aux (FES_Fexps(fs,false),(l,NoTyp)) in
+  match fexps with
+  | [] -> if fail_on_error then typ_error l "Record or record update must include fields" None None None
+    else None
+  | fexp::exps ->
+    match fexp with
+    | FE_aux(FE_Fexp(id,exp),(fl,_)) ->
+      (match (to_fexps false k_env def_ord (wrap exps)) with
+       | Some(FES_aux(FES_Fexps(fexps,_),(l,_))) ->
+         Some(wrap(fexp::fexps))
+       | None ->
+         Some(wrap([fexp])))
+
+and to_iexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:Ast.order) (iexps: (int * exp) list)
+  :(int * exp) list =
+  match iexps with
+  | [] -> []
+  | (i,exp)::exps ->
+    (i, to_exp k_env def_ord exp)::to_iexps fail_on_error k_env def_ord exps
+      
+let to_default (names, k_env, default_order) (default : tannot default_spec) : (tannot default_spec) envs_out =
+  match default with
+  | DT_aux(df,l) ->
+    (match df with 
+    | DT_kind(bk,v) ->
+      let k,k_typ = to_base_kind bk in
+      let key = var_to_string v in
+      DT_aux(DT_kind(k,v),l),(names,(Envmap.insert k_env (key,k_typ)),default_order)
+    | DT_typ(typschm,id) ->
+      let tps,_,_ = to_typschm k_env default_order typschm in
+      DT_aux(DT_typ(tps,id),l),(names,k_env,default_order)
+    | DT_order(o) ->
+      (match o with
+       | Ord_aux(Ord_inc,lo) ->
+         let default_order = Ord_aux(Ord_inc,lo) in
+         DT_aux(DT_order default_order,l),(names,k_env,default_order)
+       | Ord_aux(Ord_dec,lo) ->
+         let default_order = Ord_aux(Ord_dec,lo) in
+         DT_aux(DT_order default_order,l),(names,k_env,default_order)
+       | _ -> typ_error l "Default order must be Inc or Dec" None None None))
+
+let to_spec (names,k_env,default_order) (val_: tannot val_spec) : (tannot val_spec) envs_out =
+  match val_ with
+  | VS_aux(vs,(l,_)) ->
+    (match vs with
+    | VS_val_spec(ts,id) ->
+      let typsch,_,_ = to_typschm k_env default_order ts in
+      VS_aux(VS_val_spec(typsch, id),(l,NoTyp)),(names,k_env,default_order)
+    | VS_extern_spec(ts,id,s) ->
+      let typsch,_,_ = to_typschm k_env default_order ts in
+      VS_aux(VS_extern_spec(typsch,id,s),(l,NoTyp)),(names,k_env,default_order)
+    | VS_extern_no_rename(ts,id) ->
+      let typsch,_,_ = to_typschm k_env default_order ts in
+       VS_aux(VS_extern_no_rename(typsch,id),(l,NoTyp)),(names,k_env,default_order))
+    
+let to_namescm ns = ns
+
+let rec to_range (BF_aux(r,l)) = (* TODO add check that ranges are sensible for some definition of sensible *)
+  BF_aux(
+    (match r with
+    | BF_single(i) -> BF_single(i)
+    | BF_range(i1,i2) -> BF_range(i1,i2)
+    | BF_concat(ir1,ir2) -> BF_concat( to_range ir1, to_range ir2)),
+    l)
+
+let to_type_union k_env default_order (Tu_aux(tu,l)) =
+  match tu with
+    | Tu_ty_id(atyp,id) -> (Tu_aux(Tu_ty_id ((to_typ k_env default_order atyp),id),l))
+    | Tu_id id -> (Tu_aux(Tu_id(id),l)) 
+
+let to_typedef (names,k_env,def_ord) (td: tannot type_def) : (tannot type_def) envs_out =
+  match td with
+  |TD_aux(td,(l,_)) ->
+  (match td with 
+  | TD_abbrev(id,name_scm_opt,typschm) ->
+    let key = id_to_string id in
+    let typschm,k_env,_ = to_typschm k_env def_ord typschm in
+    let td_abrv = TD_aux(TD_abbrev(id,to_namescm name_scm_opt,typschm),(l,NoTyp)) in
+    let typ = (match typschm with 
+      | TypSchm_aux(TypSchm_ts(tq,typ), _) ->
+        begin match (typquant_to_quantkinds k_env tq) with
+        | [] -> {k = K_Typ}
+        | typs -> {k= K_Lam(typs,{k=K_Typ})}
+        end) in
+    td_abrv,(names,Envmap.insert k_env (key,typ),def_ord)
+  | TD_record(id,name_scm_opt,typq,fields,_) -> 
+    let key = id_to_string id in
+    let typq,k_env,_ = to_typquant k_env typq in
+    let fields = List.map (fun (atyp,id) -> (to_typ k_env def_ord atyp),id) fields in (* Add check that all arms have unique names locally *)
+    let td_rec = TD_aux(TD_record(id,to_namescm name_scm_opt,typq,fields,false),(l,NoTyp)) in
+    let typ = (match (typquant_to_quantkinds k_env typq) with
+      | [ ] -> {k = K_Typ}
+      | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
+    td_rec, (names,Envmap.insert k_env (key,typ), def_ord)
+  | TD_variant(id,name_scm_opt,typq,arms,_) ->
+    let key = id_to_string id in
+    let typq,k_env,_ = to_typquant k_env typq in
+    let arms = List.map (to_type_union k_env def_ord) arms in (* Add check that all arms have unique names *)
+    let td_var = TD_aux(TD_variant(id,to_namescm name_scm_opt,typq,arms,false),(l,NoTyp)) in
+    let typ = (match (typquant_to_quantkinds k_env typq) with
+      | [ ] -> {k = K_Typ}
+      | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
+    td_var, (names,Envmap.insert k_env (key,typ), def_ord)
+  | TD_enum(id,name_scm_opt,enums,_) -> 
+    let key = id_to_string id in
+    let keys = List.map id_to_string enums in
+    let td_enum = TD_aux(TD_enum(id,to_namescm name_scm_opt,enums,false),(l,NoTyp)) in (* Add check that all enums have unique names *)
+    let k_env = List.fold_right (fun k k_env -> Envmap.insert k_env (k,{k=K_Nat})) keys (Envmap.insert k_env (key,{k=K_Typ})) in
+    td_enum, (names,k_env,def_ord)
+  | TD_register(id,t1,t2,ranges) -> 
+    let key = id_to_string id in
+    let n1 = to_nexp k_env t1 in
+    let n2 = to_nexp k_env t2 in
+    let ranges = List.map (fun (range,id) -> (to_range range),id) ranges in
+    TD_aux(TD_register(id,n1,n2,ranges),(l,NoTyp)), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord))
+
+let to_tannot_opt (k_env:kind Envmap.t) (def_ord:Ast.order) (Typ_annot_opt_aux(tp,l))
+  :tannot_opt * kind Envmap.t * kind Envmap.t=
+  match tp with
+  | Typ_annot_opt_some(tq,typ) ->
+    let typq,k_env,k_local = to_typquant k_env tq in
+    Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_typ k_env def_ord typ),l),k_env,k_local
+
+let to_effects_opt (k_env : kind Envmap.t) (Effect_opt_aux(e,l)) : effect_opt =
+  match e with
+  | Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,l)
+  | Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_effects k_env typ),l)
+
+let to_funcl (names,k_env,def_ord) (FCL_aux(fcl,(l,_)) : tannot funcl) : (tannot funcl) =
+  match fcl with
+  | FCL_Funcl(id,pat,exp) -> 
+    FCL_aux(FCL_Funcl(id, to_pat k_env def_ord pat, to_exp k_env def_ord exp),(l,NoTyp))
+
+let to_fundef  (names,k_env,def_ord) (FD_aux(fd,(l,_)): tannot fundef) : (tannot fundef) envs_out = 
+  match fd with
+  | FD_function(rec_opt,tannot_opt,effects_opt,funcls) -> 
+    let tannot_opt, k_env,_ = to_tannot_opt k_env def_ord tannot_opt in
+    FD_aux(FD_function(rec_opt, tannot_opt, to_effects_opt k_env effects_opt,
+                       List.map (to_funcl (names, k_env, def_ord)) funcls), (l,NoTyp)), (names,k_env,def_ord)
+    
+type def_progress =
+    No_def
+  | Def_place_holder of id * Parse_ast.l
+  | Finished of tannot def
+
+type partial_def = ((tannot def) * bool) ref * kind Envmap.t
+
+let rec def_in_progress (id : id) (partial_defs : (id * partial_def) list) : partial_def option =
+  match partial_defs with
+  | [] -> None
+  | (n,pd)::defs -> 
+    (match n,id with
+    | Id_aux(Id(n),_), Id_aux(Id(i),_) -> if (n = i) then Some(pd) else def_in_progress id defs
+    | _,_ -> def_in_progress id defs)
+
+let to_alias_spec k_env def_ord (AL_aux(ae,(le,_))) = 
+  AL_aux(
+    (match ae with
+      | AL_subreg(reg, field) -> AL_subreg(reg, field)
+      | AL_bit(reg,range) -> AL_bit(reg,to_exp k_env def_ord range)
+      | AL_slice(reg,base,stop) ->
+        AL_slice(reg,to_exp k_env def_ord base,to_exp k_env def_ord stop)
+      | AL_concat(first,second) -> AL_concat(first,second)
+    ), (le,NoTyp))
+
+let to_dec (names,k_env,def_ord) (DEC_aux(regdec,(l,_))) =
+  DEC_aux(
+    (match regdec with
+      | DEC_reg(typ,id) ->
+        DEC_reg(to_typ k_env def_ord typ,id)
+      | DEC_alias(id,ae) ->
+        DEC_alias(id,to_alias_spec k_env def_ord ae)
+      | DEC_typ_alias(typ,id,ae) ->
+        DEC_typ_alias(to_typ k_env def_ord typ,id,to_alias_spec k_env def_ord ae)
+    ),(l,NoTyp))
+      
+let to_def (names, k_env, def_ord) partial_defs def : def_progress envs_out * (id * partial_def) list = 
+  let envs = (names,k_env,def_ord) in
+  match def with
+  | DEF_type(t_def) -> 
+    let td,envs = to_typedef envs t_def in
+    ((Finished(DEF_type(td))),envs),partial_defs
+  | DEF_fundef(f_def) -> 
+    let fd,envs = to_fundef envs f_def in
+    ((Finished(DEF_fundef(fd))),envs),partial_defs
+  | DEF_val(lbind) -> 
+    let lb = to_letbind k_env def_ord lbind in
+    ((Finished(DEF_val(lb))),envs),partial_defs
+  | DEF_spec(val_spec) -> 
+    let vs,envs = to_spec envs val_spec in
+    ((Finished(DEF_spec(vs))),envs),partial_defs
+  | DEF_default(typ_spec) -> 
+    let default,envs = to_default envs typ_spec in
+    ((Finished(DEF_default(default))),envs),partial_defs
+  | DEF_comm c-> ((Finished(DEF_comm c)),envs),partial_defs
+  | DEF_reg_dec(dec) ->
+    let d = to_dec envs dec in
+    ((Finished(DEF_reg_dec(d))),envs),partial_defs
+  | DEF_scattered(SD_aux(sd,(l,_))) ->
+    (match sd with
+    | SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) ->
+      let tannot,k_env',k_local = to_tannot_opt k_env def_ord tannot_opt in
+      let effects_opt = to_effects_opt k_env' effects_opt in
+      (match (def_in_progress id partial_defs) with
+       | None ->
+         let partial_def = ref ((DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,NoTyp)))),false) in
+         (No_def,envs),((id,(partial_def,k_local))::partial_defs)
+       | Some(d,k) ->
+         typ_error l
+           "Scattered function definition header name already in use by scattered definition" (Some id) None None)
+    | SD_scattered_funcl(funcl) -> 
+      (match funcl with
+       | FCL_aux(FCL_Funcl(id,_,_),_) -> 
+         (match (def_in_progress id partial_defs) with
+          | None ->
+            typ_error l
+              "Scattered function definition clause does not match any exisiting function definition headers"
+              (Some id) None None
+          | Some(d,k) ->
+            (match !d with
+             | DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),false -> 
+               let funcl = to_funcl (names,Envmap.union k k_env,def_ord) funcl in 
+               d:= DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[funcl]),fl)),false;
+               (No_def,envs),partial_defs
+             | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None None
+             | _ -> typ_error l
+                      "Scattered function definition clause matches an existing scattered type definition header"
+                      (Some id) None None)))
+    | SD_scattered_variant(id,naming_scheme_opt,typquant) -> 
+      let name = to_namescm naming_scheme_opt in
+      let typq, k_env',_ = to_typquant k_env typquant in
+      let kind = (match (typquant_to_quantkinds k_env' typq) with
+        | [ ] -> {k = K_Typ}
+        | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
+      (match (def_in_progress id partial_defs) with
+       | None -> let partial_def = ref ((DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,NoTyp)))),false) in
+         (Def_place_holder(id,l),
+          (names,Envmap.insert k_env ((id_to_string id),kind),def_ord)),(id,(partial_def,k_env'))::partial_defs
+       | Some(d,k) ->
+         typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None)
+    | SD_scattered_unioncl(id,tu) -> 
+      (match (def_in_progress id partial_defs) with
+       | None -> typ_error l
+                   "Scattered type definition clause does not match any existing type definition headers"
+                   (Some id) None None
+       | Some(d,k) ->
+         (match !d with
+          | DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)), false -> 
+            d:= DEF_type(TD_aux(TD_variant(id,name,typq,arms@[to_type_union k def_ord tu],false),tl)),false;
+            (No_def,envs),partial_defs
+          | _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None
+          | _ -> typ_error l
+                   "Scattered type definition clause matches an existing scattered function definition header"
+                   (Some id) None None))
+    | SD_scattered_end(id) ->
+      (match (def_in_progress id partial_defs) with
+      | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None
+      | Some(d,k) ->
+        (match !d with
+        | (DEF_type(_) as def),false ->
+          d:= (def,true);
+          (No_def,envs),partial_defs
+        | (DEF_fundef(_) as def),false ->
+          d:= (def,true);
+          ((Finished def), envs),partial_defs
+        | _, true -> 
+          typ_error l "Scattered definition ended multiple times" (Some id) None None
+        | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type"))))
+    
+let rec to_defs_helper envs partial_defs = function
+  | [] -> ([],envs,partial_defs)
+  | d::ds  -> let ((d', envs), partial_defs) = to_def envs partial_defs d in
+              let (defs,envs,partial_defs) = to_defs_helper envs partial_defs ds in
+              (match d' with
+              | Finished def -> (def::defs,envs, partial_defs)
+              | No_def -> defs,envs,partial_defs
+              | Def_place_holder(id,l) -> 
+                (match (def_in_progress id partial_defs) with
+                 | None ->
+                   raise
+                     (Reporting_basic.err_unreachable l "Id stored in place holder not retrievable from partial defs")
+                 | Some(d,k) -> 
+                   if (snd !d) 
+                   then (fst !d) :: defs, envs, partial_defs
+                   else typ_error l "Scattered type definition never ended" (Some id) None None))                
+
+let to_checked_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (def_ord : Ast.order) (Defs(defs)) =
+  let defs,(_,k_env,def_ord),partial_defs = to_defs_helper (default_names,kind_env,def_ord) [] defs in
+  List.iter 
+    (fun (id,(d,k)) -> 
+      (match !d with
+      | (d,false) -> typ_error Parse_ast.Unknown "Scattered definition never ended" (Some id) None None
+      | (_, true) -> ()))
+    partial_defs;
+  (Defs defs),k_env,def_ord
diff --git a/src/initial_check_full_ast.mli b/src/initial_check_full_ast.mli
new file mode 100644
index 00000000..57346dcf
--- /dev/null
+++ b/src/initial_check_full_ast.mli
@@ -0,0 +1,10 @@
+
+open Ast
+open Type_internal
+
+(*Envs is a tuple of used names (currently unused), map from id to kind, default order for vector types and literal vectors *)
+type envs = Nameset.t * kind Envmap.t * Ast.order 
+type 'a envs_out = 'a * envs
+
+val to_checked_ast : Nameset.t -> kind Envmap.t -> Ast.order -> tannot defs -> tannot defs * kind Envmap.t * Ast.order
+val to_exp : kind Envmap.t -> Ast.order -> exp -> exp
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 400bbd8e..df5413ae 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -686,9 +686,13 @@ let library_functions direction = [
   ("bitwise_rightshift", shift_op_vec ">>");
   ("bitwise_rotate", shift_op_vec "<<<");
   ("modulo", arith_op_no0 (mod));
+  ("mod_signed", arith_op_no0 hardware_mod);
   ("mod_vec", arith_op_vec_no0 hardware_mod "mod" Unsigned 1);
   ("mod_vec_range", arith_op_vec_range_no0 hardware_mod "mod" Unsigned 1);
+  ("mod_signed_vec", arith_op_vec_no0 hardware_mod "mod" Signed 1);
+  ("mod_signed_vec_range", arith_op_vec_range_no0 hardware_mod "mod" Signed 1);
   ("quot", arith_op_no0 hardware_quot);
+  ("quot_signed", arith_op_no0 hardware_quot);
   ("quot_vec", arith_op_vec_no0 hardware_quot "quot" Unsigned 1);
   ("quot_overflow_vec", arith_op_overflow_vec_no0 hardware_quot "quot" Unsigned 1);
   ("quot_vec_signed", arith_op_vec_no0 hardware_quot "quot" Signed 1);
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 3703940a..a9a44dfe 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -285,7 +285,7 @@ let doc_exp, doc_let =
   and star_exp env add_red ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id (
       "*" | "/"
-    | "div" | "quot" | "rem" | "mod" | "quot_s"
+    | "div" | "quot" | "rem" | "mod" | "quot_s" | "mod_s" 
     | "*_s" | "*_si" | "*_u" | "*_ui"),_) as op),r) ->
       doc_op (doc_id op) (star_exp env add_red l) (starstar_exp env add_red r)
   | _ -> starstar_exp env add_red expr
@@ -410,7 +410,7 @@ let doc_exp, doc_let =
     | ">>" | ">>>" | "<<" | "<<<"
     | "+" | "+_s" | "-" | "-_s" 
     | "*" | "/"
-    | "div" | "quot" | "quot_s" | "rem" | "mod"
+    | "div" | "quot" | "quot_s" | "rem" | "mod" | "mod_s" 
     | "*_s" | "*_si" | "*_u" | "*_ui"
     | "**"), _))
     , _) ->
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 9d0af83d..c971550d 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -46,7 +46,7 @@ let rec load_memory_segment' (bytes,addr) mem =
 
 let rec load_memory_segment (segment: Elf_interpreted_segment.elf64_interpreted_segment) mem =
   let (Byte_sequence.Sequence bytes) = segment.Elf_interpreted_segment.elf64_segment_body in
-  let addr = segment.Elf_interpreted_segment.elf64_segment_base in
+  let addr = segment.Elf_interpreted_segment.elf64_segment_paddr in
   load_memory_segment' (bytes,addr) mem
 
 
@@ -447,7 +447,7 @@ let initial_stack_and_reg_data_of_AAarch64_elf_file e_entry all_data_memory =
 let mips_register_data_all =  [
   (*Pseudo registers*)
   ("branchPending", (D_decreasing, 1, 0));
-  ("exceptionSignalled", (D_decreasing, 1, 0));
+  ("inBranchDelay", (D_decreasing, 1, 0));
   ("delayedPC", (D_decreasing, 64, 63));
   ("nextPC", (D_decreasing, 64, 63));
   (* General purpose registers *)
@@ -490,6 +490,8 @@ let mips_register_data_all =  [
   ("CP0Status", (D_decreasing, 32, 31));
   ("CP0Cause", (D_decreasing, 32, 31));
   ("CP0EPC", (D_decreasing, 64, 63));
+  ("CP0LLAddr", (D_decreasing, 64, 63));
+  ("CP0LLBit", (D_decreasing, 1, 0));
 ]
 
 let initial_stack_and_reg_data_of_MIPS_elf_file e_entry all_data_memory =
@@ -860,7 +862,7 @@ let set_next_instruction_address model =
 
 let add1 = Nat_big_num.add (Nat_big_num.of_int 1)
 
-let fetch_instruction_opcode_and_update_ia model =
+let fetch_instruction_opcode_and_update_ia model addr_trans =
   match model with
   | PPC ->
     let cia = Reg.find "CIA" !reg in
@@ -902,7 +904,10 @@ let fetch_instruction_opcode_and_update_ia model =
     let pc_addr = address_of_register_value nextPC in
     (match pc_addr with
     | Some pc_addr ->
-      let pc_a = integer_of_address pc_addr in
+      let pc_a = match addr_trans pc_addr with
+        | Some a, _ -> integer_of_address a
+        | None, Some i -> failwith ("Address translation failed with error code " ^ (Nat_big_num.to_string i))
+        | _ -> failwith "Neither an address or a code on translate address" in
       let opcode = List.map (fun b -> match b with
         | Some b -> b
         | None -> failwith "A byte in opcode contained unknown or undef")
@@ -924,7 +929,7 @@ let get_pc_address = function
   | AArch64 -> Reg.find "_PC" !reg
         
 
-let rec fde_loop count context model mode track_dependencies opcode =
+let rec fde_loop count context model mode track_dependencies opcode addr_trans =
   if !max_cut_off && count = !max_instr
   then resultf "\nEnding evaluation due to reaching cut off point of %d instructions\n" count
   else begin
@@ -956,8 +961,8 @@ let rec fde_loop count context model mode track_dependencies opcode =
         | true, mode, track_dependencies, (my_reg, my_mem) ->
           reg := my_reg;
           prog_mem := my_mem;
-          let opcode = fetch_instruction_opcode_and_update_ia model in
-          fde_loop (count + 1) context model (Some mode) (ref track_dependencies) opcode
+          let opcode = fetch_instruction_opcode_and_update_ia model addr_trans in
+          fde_loop (count + 1) context model (Some mode) (ref track_dependencies) opcode addr_trans
       end
   end
   
@@ -982,8 +987,8 @@ let run () =
           endian mode, and translate function name 
   *)
   let addr_trans = translate_address context E_big_endian "TranslateAddress" in
-  let startaddr,startaddr_internal = match addr_trans startaddr_internal with
-    | Some a, _ -> integer_of_address a, a
+  let startaddr = match addr_trans startaddr_internal with
+    | Some a, _ -> integer_of_address a
     | None, Some i -> failwith ("Address translation failed with error code " ^ (Nat_big_num.to_string i))
     | _ -> failwith "Neither an address or a code on translate address"
   in
@@ -999,7 +1004,7 @@ let run () =
   
   (* entry point: unit -> unit fde *)
   let name = Filename.basename !file in
-  let t = time_it (fun () -> fde_loop 0 context isa_model (Some Run) (ref false) initial_opcode) () in
+  let t = time_it (fun () -> fde_loop 0 context isa_model (Some Run) (ref false) initial_opcode addr_trans) () in
   resultf "Execution time for file %s: %f seconds\n" name t;;
 
 run () ;;
diff --git a/src/lexer.mll b/src/lexer.mll
index a6b1bcfa..b6328ab7 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -108,6 +108,7 @@ let kw_table =
 
      ("div",			 (fun x -> Div_));
      ("mod",			 (fun x -> Mod));
+     ("mod_s",                   (fun x -> ModUnderS));
      ("quot",			 (fun x -> Quot));
      ("quot_s",                  (fun x -> QuotUnderS));
      ("rem",			 (fun x -> Rem));
@@ -159,7 +160,6 @@ rule token = parse
   | ":"                                 { Colon(r ":") }
   | ","                                 { Comma }
   | "."                                 { Dot }
-  | "/"			                { (Div(r "/")) }
   | "="                                 { (Eq(r"=")) }
   | "!"					{ (Excl(r"!")) }
   | ">"					{ (Gt(r">")) }
@@ -186,7 +186,6 @@ rule token = parse
   | ":>"                                { ColonGt }
   | ":]"                                { ColonSquare }
   | ".."				{ DotDot }
-  | "=/="				{ (EqDivEq(r"=/=")) }
   | "=="				{ (EqEq(r"==")) }
   | "!="				{ (ExclEq(r"!=")) }
   | "!!"				{ (ExclExcl(r"!!")) }
@@ -264,7 +263,6 @@ rule token = parse
   | "&&" oper_char+ as i                { (AmpAmpI(r i)) }
   | "^^" oper_char+ as i		{ (CarrotCarrotI(r i)) }
   | "::" oper_char+ as i                { (ColonColonI(r i)) }
-  | "=/=" oper_char+ as i		{ (EqDivEqI(r i)) }
   | "==" oper_char+ as i		{ (EqEqI(r i)) }
   | "!=" oper_char+ as i		{ (ExclEqI(r i)) }
   | "!!" oper_char+ as i		{ (ExclExclI(r i)) }
diff --git a/src/parser.mly b/src/parser.mly
index 7bd0a72f..3261551b 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -142,7 +142,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %nonassoc Then
 %nonassoc Else
 
-%token Div_ Mod Quot Rem QuotUnderS
+%token Div_ Mod ModUnderS Quot Rem QuotUnderS
 
 %token Bar Comma Dot Eof Minus Semi Under
 %token Lcurly Rcurly Lparen Rparen Lsquare Rsquare
@@ -156,7 +156,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %token <string> String Bin Hex
 
 %token <string> Amp At Carrot  Div Eq Excl Gt Lt Plus Star Tilde
-%token <string> AmpAmp CarrotCarrot Colon ColonColon EqDivEq EqEq ExclEq ExclExcl
+%token <string> AmpAmp CarrotCarrot Colon ColonColon EqEq ExclEq ExclExcl
 %token <string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt
 %token <string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar TildeCarrot
 
@@ -166,7 +166,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %token <string> StarUnderSi StarUnderU StarUnderUi TwoCarrot PlusUnderS MinusUnderS 
 
 %token <string> AmpI AtI CarrotI  DivI EqI ExclI GtI LtI PlusI StarI TildeI
-%token <string> AmpAmpI CarrotCarrotI ColonColonI EqDivEqI EqEqI ExclEqI ExclExclI
+%token <string> AmpAmpI CarrotCarrotI ColonColonI EqEqI ExclEqI ExclExclI
 %token <string> GtEqI GtEqPlusI GtGtI GtGtGtI GtPlusI HashGtGtI HashLtLtI
 %token <string> LtEqI LtEqPlusI LtGtI LtLtI LtLtLtI LtPlusI StarStarI TildeCarrotI
 
@@ -238,8 +238,6 @@ id:
     { idl (DeIid($3)) }
   | Lparen Deinfix ColonColon Rparen
     { idl (DeIid($3)) }
-  | Lparen Deinfix EqDivEq Rparen
-    { idl (DeIid($3)) }
   | Lparen Deinfix EqEq Rparen
     { idl (DeIid($3)) }
   | Lparen Deinfix ExclEq Rparen
@@ -433,7 +431,7 @@ nexp_typ:
    | Num Minus nexp_typ
      { tloc (ATyp_minus((tlocl (ATyp_constant $1) 1 1),$3)) }
    | Lparen Num Minus nexp_typ Rparen
-     { tloc (ATyp_minus((tlocl (ATyp_constant $2) 2 2),$4)) } 
+       { tloc (ATyp_minus((tlocl (ATyp_constant $2) 2 2),$4)) }
 
 
 tup_typ_list:
@@ -686,7 +684,9 @@ star_exp:
   | star_exp Rem starstar_exp
     { eloc (E_app_infix($1,Id_aux(Id("rem"), locn 2 2), $3)) }
   | star_exp Mod starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id("mod"), locn 2 2), $3)) }
+      { eloc (E_app_infix($1,Id_aux(Id("mod"), locn 2 2), $3)) }
+  | star_exp ModUnderS starstar_exp
+      { eloc (E_app_infix($1,Id_aux(Id("mod_s"), locn 2 2), $3)) }
   | star_exp StarUnderS starstar_exp
     { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
   | star_exp StarUnderSi starstar_exp
@@ -713,6 +713,8 @@ star_right_atomic_exp:
     { eloc (E_app_infix($1,Id_aux(Id("rem"), locn 2 2), $3)) }
   | star_exp Mod starstar_right_atomic_exp
     { eloc (E_app_infix($1,Id_aux(Id("mod"), locn 2 2), $3)) }
+  | star_exp ModUnderS starstar_right_atomic_exp
+    { eloc (E_app_infix($1,Id_aux(Id("mod_s"), locn 2 2), $3)) }
   | star_exp StarUnderS starstar_right_atomic_exp
     { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
   | star_exp StarUnderSi starstar_right_atomic_exp
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index b85b31da..5f0990d1 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -639,6 +639,9 @@ let squarebarbars = enclose lsquarebarbar rsquarebarbar
 let lsquarecolon = string "[:"
 let rsquarecolon = string ":]"
 let squarecolons = enclose lsquarecolon rsquarecolon
+let lcomment = string "(*"
+let rcomment = string "*)"
+let comment = enclose lcomment rcomment
 let string_lit = enclose dquote dquote
 let spaces op = enclose space space op
 let semi_sp = semi ^^ space
@@ -691,11 +694,26 @@ let doc_typ, doc_atomic_typ, doc_nexp =
       Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _);
       Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_inc, _)), _);
       Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) ->
-        (doc_id id) ^^ (brackets (if n = 0 then doc_int m else doc_op colon (doc_int n) (doc_int (n+m-1))))
+    (doc_id id) ^^ (brackets (if n = 0 then doc_int m else doc_op colon (doc_int n) (doc_int (n+m-1))))
+  | Typ_app(Id_aux (Id "vector", _), [
+      Typ_arg_aux(Typ_arg_nexp
+                    (Nexp_aux(Nexp_minus (Nexp_aux(Nexp_constant n, _),
+                                          Nexp_aux(Nexp_constant 1, _)),_)),_);
+      Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _);
+      Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _);
+      Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) ->
+    (doc_id id) ^^ (brackets (if n = m then doc_int m else doc_op colon (doc_int m) (doc_int (n-1))))
+  | Typ_app(Id_aux (Id "vector", _), [
+      Typ_arg_aux(Typ_arg_nexp
+                  (Nexp_aux(Nexp_minus (n', Nexp_aux((Nexp_constant 1), _)),_) as n_n),_);
+      Typ_arg_aux(Typ_arg_nexp m_nexp, _);
+      Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _);
+      Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) ->
+    (doc_id id) ^^ (brackets (if n' = m_nexp then nexp m_nexp else doc_op colon (nexp m_nexp) (nexp n_n)))
   | Typ_app(Id_aux (Id "range", _), [
     Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _);
     Typ_arg_aux(Typ_arg_nexp m, _);]) ->
-    (squarebars (if n = 0 then nexp m else doc_op colon (doc_int n) (nexp m))) 
+    (squarebars (if n = 0 then nexp m else doc_op colon (doc_int n) (nexp m)))
   | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
     (squarecolons (nexp n))
   | Typ_app(id,args) ->
@@ -897,7 +915,7 @@ let doc_exp, doc_let =
   | _ -> group (parens (exp expr))
   and app_exp ((E_aux(e,_)) as expr) = match e with
   | E_app(f,args) ->
-      doc_unop (doc_id f) (parens (separate_map comma exp args))
+      (doc_id f) ^^ (parens (separate_map comma exp args))
   | _ -> vaccess_exp expr
   and vaccess_exp ((E_aux(e,_)) as expr) = match e with
   | E_vector_access(v,e) ->
@@ -973,7 +991,7 @@ let doc_exp, doc_let =
       let cases = separate_map (break 1) doc_case pexps in
       surround 2 1 opening cases rbrace
   | E_exit e ->
-    separate space [string "exit"; exp e;]
+    separate space [string "exit"; atomic_exp e;]
   | E_assert(c,m) ->
     separate space [string "assert"; parens (separate comma [exp c; exp m])]
   (* adding parens and loop for lower precedence *)
@@ -1001,7 +1019,9 @@ let doc_exp, doc_let =
   (* XXX default precedence for app_infix? *)
   | E_app_infix(l,op,r) ->
       failwith ("unexpected app_infix operator " ^ (pp_format_id op))
-      (* doc_op (doc_id op) (exp l) (exp r) *)
+  (* doc_op (doc_id op) (exp l) (exp r) *)
+  | E_comment s -> comment (string s)
+  | E_comment_struc e -> comment (exp e)
   | E_internal_exp((l, Base((_,t),_,_,_,_,bindings))) -> (*TODO use bindings, and other params*)
     (match t.t with
       | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}])
@@ -1139,10 +1159,13 @@ let doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),_)) =
   | _ ->
       let sep = hardline ^^ string "and" ^^ space in
       let clauses = separate_map sep doc_funcl fcls in
-      separate space [string "function";
-        doc_rec r ^^ doc_tannot_opt typa;
-        string "effect"; doc_effects_opt efa;
-        clauses]
+      separate space ([string "function";
+                      doc_rec r ^^ doc_tannot_opt typa;]@
+                      (match efa with
+                       | Effect_opt_aux (Effect_opt_pure,_) -> []
+                       | _ -> [string "effect";
+                               doc_effects_opt efa;])
+                      @[clauses])
 
 let doc_alias (AL_aux (alspec,_)) =
   match alspec with
@@ -1161,15 +1184,17 @@ let doc_dec (DEC_aux (reg,_)) =
 
 let doc_scattered (SD_aux (sdef, _)) = match sdef with
  | SD_scattered_function (r, typa, efa, id) ->
-     separate space [
+     separate space ([
        string "scattered function";
-       doc_rec r ^^ doc_tannot_opt typa;
-       string "effect"; doc_effects_opt efa;
-       doc_id id]
+       doc_rec r ^^ doc_tannot_opt typa;]@
+       (match efa with
+        | Effect_opt_aux (Effect_opt_pure,_) -> []
+        | _ -> [string "effect"; doc_effects_opt efa;])
+         @[doc_id id])
  | SD_scattered_variant (id, ns, tq) ->
      doc_op equals
        (string "scattered typedef" ^^ space ^^ doc_id id ^^ doc_namescm ns)
-       (doc_typquant tq empty)
+       (string "const union" ^^ space ^^ (doc_typquant tq empty))
  | SD_scattered_funcl funcl ->
      string "function clause" ^^ space ^^ doc_funcl funcl
  | SD_scattered_unioncl (id, tu) ->
@@ -1177,7 +1202,7 @@ let doc_scattered (SD_aux (sdef, _)) = match sdef with
      string "member"; doc_type_union tu]
  | SD_scattered_end id -> string "end" ^^ space ^^ doc_id id
 
-let doc_def def = group (match def with
+let rec doc_def def = group (match def with
   | DEF_default df -> doc_default df
   | DEF_spec v_spec -> doc_spec v_spec
   | DEF_type t_def -> doc_typdef t_def
@@ -1185,6 +1210,8 @@ let doc_def def = group (match def with
   | DEF_val lbind -> doc_let lbind
   | DEF_reg_dec dec -> doc_dec dec
   | DEF_scattered sdef -> doc_scattered sdef
+  | DEF_comm (DC_comm s) -> comment (string s)
+  | DEF_comm (DC_comm_struct d) -> comment (doc_def d)
   ) ^^ hardline
 
 let doc_defs (Defs(defs)) =
diff --git a/src/process_file.ml b/src/process_file.ml
index b3990ba4..db064b83 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -91,6 +91,8 @@ let parse_file (f : string) : Parse_ast.defs =
 let convert_ast (defs : Parse_ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t * Ast.order)=
   Initial_check.to_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs
 
+let initi_check_ast (defs : Type_internal.tannot Ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t * Ast.order)=
+  Initial_check_full_ast.to_checked_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs
 
 let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.order) : Type_internal.tannot Ast.defs =
   let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env; 
diff --git a/src/process_file.mli b/src/process_file.mli
index 38ac057f..e9a1d43c 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -46,6 +46,7 @@
 
 val parse_file : string -> Parse_ast.defs
 val convert_ast : Parse_ast.defs -> Type_internal.tannot Ast.defs * Type_internal.kind Type_internal.Envmap.t * Ast.order
+val initi_check_ast : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs * Type_internal.kind Type_internal.Envmap.t * Ast.order
 val check_ast: Type_internal.tannot Ast.defs -> Type_internal.kind Type_internal.Envmap.t -> Ast.order -> Type_internal.tannot Ast.defs
 val rewrite_ast: Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
 val rewrite_ast_lem : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
diff --git a/src/sail.ml b/src/sail.ml
index d91d229b..0d66215a 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -47,6 +47,7 @@
 open Process_file
 
 let lib = ref []
+let opt_file_out : string option ref = ref None
 let opt_print_version = ref false
 let opt_print_verbose = ref false
 let opt_print_lem_ast = ref false
@@ -60,16 +61,16 @@ let options = Arg.align ([
     Arg.String (fun l -> lib := l::!lib),
     " treat the file as input only and generate no output for it");
   ( "-verbose",
-    Arg.Unit (fun b -> opt_print_verbose := true),
+    Arg.Set opt_print_verbose,
     " pretty-print out the file");
   ( "-lem_ast",
-    Arg.Unit (fun b -> opt_print_lem_ast := true),
+    Arg.Set opt_print_lem_ast,
     " pretty-print a Lem AST representation of the file");
   ( "-lem",
-    Arg.Unit (fun b -> opt_print_lem := true),
+    Arg.Set opt_print_lem,
     " print a Lem translated version of the specification");
   ( "-ocaml",
-    Arg.Unit (fun b -> opt_print_ocaml := true),
+    Arg.Set opt_print_ocaml,
     " print an Ocaml translated version of the specification");
   ( "-skip_constraints",
     Arg.Clear Type_internal.do_resolve_constraints,
@@ -81,8 +82,11 @@ let options = Arg.align ([
     Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml),
     " provide additional library to open in Ocaml output");
   ( "-v",
-    Arg.Unit (fun b -> opt_print_version := true),
+    Arg.Set opt_print_version,
     " print version");
+  ( "-o",
+    Arg.String (fun f -> opt_file_out := Some f),
+    " select output filename prefix";)
 ] )
 
 let usage_msg =
@@ -107,25 +111,28 @@ let main() =
     let (ast,kenv,ord) = convert_ast ast in
     let ast = check_ast ast kenv ord in 
     let ast = rewrite_ast ast in
+    let out_name = match !opt_file_out with
+      | None -> fst (List.hd parsed)
+      | Some f -> f ^ ".sail" in
     (*let _ = Printf.eprintf "Type checked, next to pretty print" in*)
     begin 
       (if !(opt_print_verbose)
        then ((Pretty_print.pp_defs stdout) ast)
        else ());
       (if !(opt_print_lem_ast)
-       then output "" Lem_ast_out [(fst (List.hd parsed)),ast]
+       then output "" Lem_ast_out [out_name,ast]
        else ());
       (if !(opt_print_ocaml)
        then let ast_ocaml = rewrite_ast_ocaml ast in
          if !(opt_libs_ocaml) = []
-         then output "" (Ocaml_out None) [(fst (List.hd parsed)),ast_ocaml]
-         else output "" (Ocaml_out (Some (List.hd !opt_libs_ocaml))) [(fst (List.hd parsed)),ast_ocaml]
+         then output "" (Ocaml_out None) [out_name,ast_ocaml]
+         else output "" (Ocaml_out (Some (List.hd !opt_libs_ocaml))) [out_name,ast_ocaml]
        else ());
       (if !(opt_print_lem)
        then let ast_lem = rewrite_ast_lem ast in
          if !(opt_libs_lem) = []
-         then output "" (Lem_out None) [(fst (List.hd parsed)),ast_lem]
-         else output "" (Lem_out (Some (List.hd !opt_libs_lem))) [(fst (List.hd parsed)),ast_lem]
+         then output "" (Lem_out None) [out_name,ast_lem]
+         else output "" (Lem_out (Some (List.hd !opt_libs_lem))) [out_name,ast_lem]
        else ())
     end
 
diff --git a/src/test/mips/test_casmgp_cached.elf b/src/test/mips/test_casmgp_cached.elf
new file mode 100755
index 00000000..9ca566cc
--- /dev/null
+++ b/src/test/mips/test_casmgp_cached.elf
diff --git a/src/type_check.ml b/src/type_check.ml
index 1458940b..d8c4a400 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -786,7 +786,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
           | Tfn(arg,ret,_,ef') -> check_parms arg lft rht
           | _ -> typ_error l ("Expected a function, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in
         (*let _ = Printf.eprintf "Looking for overloaded function %s, generic type is %s, arg_t is %s\n"
-          i (t_to_string t_p) (t_to_string arg_t) in*)
+            i (t_to_string t_p) (t_to_string arg_t) in*)
         (match (select_overload_variant d_env true overload_return variants arg_t) with
         | [] -> 
           typ_error l ("No function found with name " ^ i ^
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 26b68fa6..a48e7b85 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -247,6 +247,15 @@ let get_c_loc = function
 (*To string functions *)
 let debug_mode = ref true;;
 
+let rec kind_to_string kind = match kind.k with
+  | K_Nat -> "Nat"
+  | K_Typ -> "Type"
+  | K_Ord -> "Order"
+  | K_Efct -> "Effect"
+  | K_infer -> "Infer"
+  | K_Val -> "Val"
+  | K_Lam (kinds,kind) -> "Lam [" ^ string_of_list ", " kind_to_string kinds ^ "] -> " ^ (kind_to_string kind)
+
 let co_to_string = function
   | Patt l -> "Pattern " (*^ Reporting_basic.loc_to_string l *)
   | Expr l -> "Expression " (*^ Reporting_basic.loc_to_string l *)
@@ -1963,6 +1972,28 @@ let initial_typ_env =
                                     mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")])
                  (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))),
              (External (Some "mod_vec")),[],pure_e,pure_e,nob)]));
+    ("mod_s",
+     Overload(
+       Base(((mk_typ_params ["a";"b";"c"]),
+             (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})),
+            (External (Some "mod_signed")),[],pure_e,pure_e,nob),
+       true,
+       [Base(((mk_nat_params["n";"o";]),
+              (mk_pure_fun (mk_tup [mk_atom (mk_nv "n") ; mk_atom (mk_nv "o")])
+                           (mk_range n_zero (mk_sub (mk_nv "o") n_one)))),
+             (External (Some "mod_signed")),
+             [GtEq(Specc(Parse_ast.Int("modulo",None)),Require,(mk_nv "o"),n_one)],pure_e,pure_e,nob);
+        Base(((mk_nat_params["n";"m";"o"])@(mk_ord_params["ord"]),
+              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+                                    mk_range n_one (mk_nv "o")])
+                           (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))),
+             (External (Some "mod_signed_vec_range")),
+             [GtEq(Specc(Parse_ast.Int("mod",None)),Require,(mk_nv "o"),n_one);],pure_e,pure_e,nob);
+        Base(((mk_nat_params["n";"m"])@(mk_ord_params["ord"]),
+              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+                                    mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")])
+                 (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))),
+             (External (Some "mod_signed_vec")),[],pure_e,pure_e,nob)]));
     ("quot",
      Overload(
        Base(((mk_typ_params ["a";"b";"c"]),
@@ -1971,8 +2002,9 @@ let initial_typ_env =
        true,
        [Base(((mk_nat_params["n";"m";"o";]),
               (mk_pure_fun (mk_tup [mk_atom (mk_nv "n");mk_atom (mk_nv "m")])
-                           (mk_atom (mk_nv "o")))),
-             (External (Some "quot")),[GtEq(Specc(Parse_ast.Int("quot",None)),Require,(mk_nv "m"),n_one);
+                 (mk_atom (mk_nv "o")))),
+             (*This should really be != to 0, as negative is just fine*)
+             (External (Some "quot")),[(*GtEq(Specc(Parse_ast.Int("quot",None)),Require,(mk_nv "m"),n_one);*)
                                      LtEq(Specc(Parse_ast.Int("quot",None)),Guarantee,
                                           (mk_mult (mk_nv "n") (mk_nv "o")),(mk_nv "m"))],
              pure_e,pure_e,nob);
@@ -1998,7 +2030,7 @@ let initial_typ_env =
               (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") (mk_nv "p")])
                            (mk_range (mk_nv "q") (mk_nv "r")))),
              (External (Some "quot_signed")),
-             [GtEq(Specc(Parse_ast.Int("quot",None)),Require,(mk_nv "o"),n_one);
+             [(*GtEq(Specc(Parse_ast.Int("quot",None)),Require,(mk_nv "o"),n_one);*)
               LtEq(Specc(Parse_ast.Int("quot",None)),Guarantee,(mk_mult (mk_nv "p") (mk_nv "r")),mk_nv "m")],
              pure_e,pure_e,nob);
         Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]),
@@ -2270,10 +2302,22 @@ let initial_typ_env =
     mk_bitwise_op  "bitwise_or" "|" 2;
     mk_bitwise_op  "bitwise_xor" "^" 2;
     mk_bitwise_op  "bitwise_and" "&" 2;
-    ("^^",Base((mk_nat_params ["n"],
-                (mk_pure_fun (mk_tup [bit_t;mk_atom (mk_nv "n")])
-                             (mk_vector bit_t Oinc (mk_c zero) (mk_nv "n")))),
-               External (Some "duplicate"),[],pure_e,pure_e,nob));
+    ("^^",
+     Overload(
+       Base((mk_nat_params["n";"o";"p"]@[("a",{k=K_Typ})],
+             (mk_pure_fun (mk_tup [{t=Tvar "a"}; mk_atom (mk_nv "n")])
+                (mk_vector bit_t Oinc (mk_nv "o") (mk_nv "p")))),
+            External (Some "duplicate"), [], pure_e, pure_e, nob),
+       false,
+       [Base((mk_nat_params ["n"],
+              (mk_pure_fun (mk_tup [bit_t;mk_atom (mk_nv "n")])
+                           (mk_vector bit_t Oinc (mk_c zero) (mk_nv "n")))),
+             External (Some "duplicate"),[],pure_e,pure_e,nob);
+        Base((mk_nat_params ["n";"m";"o"]@mk_ord_params["or"],
+              mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "or") (mk_nv "o") (mk_nv "m");
+                                   mk_atom (mk_nv "n")])
+                (mk_vector bit_t (Ovar "or") (mk_nv "o") (mk_mult (mk_nv "m") (mk_nv "n")))),
+             External (Some "duplicate_bits"),[],pure_e,pure_e,nob);]));
     ("<<",Base((((mk_nat_params ["n";"m"])@[("ord",{k=K_Ord})]),
                 (mk_pure_fun (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"));
                                       (mk_range n_zero (mk_nv "m"))])
@@ -2297,6 +2341,9 @@ let initial_typ_env =
                   (mk_pure_imp (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"))
                      (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "m")) "m")),
                  External (Some "extz"),[],pure_e,pure_e,nob));
+    ("abs",Base(((mk_nat_params ["n";"m";]),
+                 (mk_pure_fun (mk_atom (mk_nv "n")) (mk_range n_zero (mk_nv "m")))),
+                External (Some "abs"),[],pure_e,pure_e,nob));
   ]
 
 
diff --git a/src/type_internal.mli b/src/type_internal.mli
index dd7993fd..17f4f2ff 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -228,7 +228,7 @@ val tag_efs_annot: t -> tag -> effect -> effect -> tannot
 val cons_bs_annot : t -> nexp_range list -> bounds_env -> tannot
 val cons_bs_annot_efr : t -> nexp_range list -> bounds_env -> effect -> tannot
 
-
+val kind_to_string : kind -> string
 val t_to_string : t -> string
 val n_to_string : nexp -> string
 val constraints_to_string : nexp_range list -> string