Make rewriter understand type abbreviations for removing internal_exp instances

3 files changed, 21 insertions, 2 deletions

diff --git a/src/initial_check_full_ast.ml b/src/initial_check_full_ast.ml
index 86c1dd2c..19f7cc94 100644
--- a/src/initial_check_full_ast.ml
+++ b/src/initial_check_full_ast.ml
@@ -61,6 +61,16 @@ let to_kind (k_env : kind Envmap.t) (K_aux(K_kind(klst),l)) : (Ast.kind * kind)
           | 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 typ_to_string (Typ_aux(t,_)) = match t with
+  | Typ_id i -> id_to_string i
+  | Typ_var (Kid_aux (Var i,_)) -> i
+  | _ -> "bigger than var"
+
+and nexp_to_string (Nexp_aux(n,_)) = match n with
+  | Nexp_id i -> id_to_string i
+  | Nexp_var (Kid_aux (Var i,_)) -> i
+  | _ -> "nexp bigger than var"
+
 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) ->
@@ -178,7 +188,14 @@ and to_typ_arg (k_env : kind Envmap.t) (def_ord : Ast.order) (kind : kind) (arg
     | 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)),
+    | _ ->
+      let tn_str = 
+        (match ta with
+         | Typ_arg_typ t -> typ_to_string t
+         | Typ_arg_nexp n -> nexp_to_string n
+         | _ -> "order or effect") in
+      typ_error l ("Kind declaration and kind of type argument, " ^ tn_str ^ " don't match here")
+        None None (Some kind)), 
     l)
 
 let to_nexp_constraint (k_env : kind Envmap.t) (c : n_constraint) : n_constraint =
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 2fbd81e2..4b1ac213 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -724,6 +724,7 @@ let doc_effect (BE_aux (e,_)) =
   | BE_eamem -> "eamem"
   | BE_barr -> "barr"
   | BE_depend -> "depend"
+  | BE_escape -> "escape"
   | BE_undef -> "undef"
   | BE_unspec -> "unspec"
   | BE_nondet -> "nondet")
diff --git a/src/rewriter.ml b/src/rewriter.ml
index b8e60ef9..4e147b36 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -377,7 +377,8 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) =
        (match t.t with
         (*Old case; should possibly be removed*)
         | Tapp("register",[TA_typ {t= Tapp("vector",[ _; TA_nexp r;_;_])}])
-        | Tapp("vector", [_;TA_nexp r;_;_]) ->
+        | Tapp("vector", [_;TA_nexp r;_;_])
+        | Tabbrev(_, {t=Tapp("vector",[_;TA_nexp r;_;_])}) ->
           (*let _ = Printf.eprintf "vector case with %s, bounds are %s\n" 
                 (n_to_string r) (bounds_to_string bounds) in*)
           let nexps = expand_nexp r in