Merge remote-tracking branch 'origin/sail2' into asl_flow2

2 files changed, 16 insertions, 19 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index c9953c57..a8251e97 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -107,7 +107,7 @@ type env =
     mappings : (typquant * typ * typ) Bindings.t;
     typ_vars : (Ast.l * kind_aux) KBindings.t;
     shadow_vars : int KBindings.t;
-    typ_synonyms : (env -> typ_arg list -> typ_arg) Bindings.t;
+    typ_synonyms : (Ast.l -> env -> typ_arg list -> typ_arg) Bindings.t;
     overloads : (id list) Bindings.t;
     flow : (typ -> typ) Bindings.t;
     enums : IdSet.t Bindings.t;
@@ -365,8 +365,8 @@ module Env : sig
   val add_typ_var : l -> kinded_id -> t -> t
   val get_ret_typ : t -> typ option
   val add_ret_typ : typ -> t -> t
-  val add_typ_synonym : id -> (t -> typ_arg list -> typ_arg) -> t -> t
-  val get_typ_synonym : id -> t -> t -> typ_arg list -> typ_arg
+  val add_typ_synonym : id -> (Ast.l -> t -> typ_arg list -> typ_arg) -> t -> t
+  val get_typ_synonym : id -> t -> Ast.l -> t -> typ_arg list -> typ_arg
   val add_overloads : id -> id list -> t -> t
   val get_overloads : id -> t -> id list
   val is_extern : id -> t -> string -> bool
@@ -550,7 +550,7 @@ end = struct
     | NC_and (nc1, nc2) -> NC_aux (NC_and (expand_constraint_synonyms env nc1, expand_constraint_synonyms env nc2), l)
     | NC_app (id, args) ->
        (try
-          begin match Bindings.find id env.typ_synonyms env args with
+          begin match Bindings.find id env.typ_synonyms l env args with
           | A_aux (A_bool nc, _) -> expand_constraint_synonyms env nc
           | arg -> typ_error env l ("Expected Bool when expanding synonym " ^ string_of_id id ^ " got " ^ string_of_typ_arg arg)
           end
@@ -562,7 +562,7 @@ end = struct
     match aux with
     | Nexp_app (id, args) ->
        (try
-          begin match Bindings.find id env.typ_synonyms env [] with
+          begin match Bindings.find id env.typ_synonyms l env [] with
           | A_aux (A_nexp nexp, _) -> expand_nexp_synonyms env nexp
           | _ -> typ_error env l ("Expected Int when expanding synonym " ^ string_of_id id)
           end
@@ -570,7 +570,7 @@ end = struct
         | Not_found -> Nexp_aux (Nexp_app (id, List.map (expand_nexp_synonyms env) args), l))
     | Nexp_id id ->
        (try
-          begin match Bindings.find id env.typ_synonyms env [] with
+          begin match Bindings.find id env.typ_synonyms l env [] with
           | A_aux (A_nexp nexp, _) -> expand_nexp_synonyms env nexp
           | _ -> typ_error env l ("Expected Int when expanding synonym " ^ string_of_id id)
           end
@@ -591,7 +591,7 @@ end = struct
     | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (expand_synonyms env typ1, expand_synonyms env typ2), l)
     | Typ_app (id, args) ->
        (try
-          begin match Bindings.find id env.typ_synonyms env args with
+          begin match Bindings.find id env.typ_synonyms l env args with
           | A_aux (A_typ typ, _) -> expand_synonyms env typ
           | _ -> typ_error env l ("Expected Type when expanding synonym " ^ string_of_id id)
           end
@@ -599,7 +599,7 @@ end = struct
         | Not_found -> Typ_aux (Typ_app (id, List.map (expand_synonyms_arg env) args), l))
     | Typ_id id ->
        (try
-          begin match Bindings.find id env.typ_synonyms env [] with
+          begin match Bindings.find id env.typ_synonyms l env [] with
           | A_aux (A_typ typ, _) -> expand_synonyms env typ
           | _ -> typ_error env l ("Expected Type when expanding synonym " ^ string_of_id id)
           end
@@ -4746,27 +4746,26 @@ let mk_synonym typq typ_arg =
   let ncs = List.map (fun nc -> List.fold_left (fun nc (kopt, fresh) -> constraint_subst (kopt_kid kopt) (arg_kopt fresh) nc) nc kopts) ncs in
   let typ_arg = List.fold_left (fun typ_arg (kopt, fresh) -> typ_arg_subst (kopt_kid kopt) (arg_kopt fresh) typ_arg) typ_arg kopts in
   let kopts = List.map snd kopts in
-  let rec subst_args kopts args =
+  let rec subst_args env l kopts args =
     match kopts, args with
     | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_nat_kopt kopt ->
-       let typ_arg, ncs = subst_args kopts args in
+       let typ_arg, ncs = subst_args env l kopts args in
        typ_arg_subst (kopt_kid kopt) (arg_nexp arg) typ_arg,
        List.map (constraint_subst (kopt_kid kopt) (arg_nexp arg)) ncs
     | kopt :: kopts, A_aux (A_typ arg, _) :: args when is_typ_kopt kopt ->
-       let typ_arg, ncs = subst_args kopts args in
+       let typ_arg, ncs = subst_args env l kopts args in
        typ_arg_subst (kopt_kid kopt) (arg_typ arg) typ_arg, ncs
     | kopt :: kopts, A_aux (A_order arg, _) :: args when is_order_kopt kopt ->
-       let typ_arg, ncs = subst_args kopts args in
+       let typ_arg, ncs = subst_args env l kopts args in
        typ_arg_subst (kopt_kid kopt) (arg_order arg) typ_arg, ncs
     | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_bool_kopt kopt ->
-       let typ_arg, ncs = subst_args kopts args in
+       let typ_arg, ncs = subst_args env l kopts args in
        typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs
     | [], [] -> typ_arg, ncs
-    | _, A_aux (_, l) :: _ -> typ_error Env.empty l "Synonym applied to bad arguments"
-    | _, _ -> typ_error Env.empty Parse_ast.Unknown "Synonym applied to bad arguments"
+    | _, _ -> typ_error env l "Synonym applied to bad arguments"
   in
-  fun env args ->
-    let typ_arg, ncs = subst_args kopts args in
+  fun l env args ->
+    let typ_arg, ncs = subst_args env l kopts args in
     if List.for_all (prove __POS__ env) ncs
     then typ_arg
     else typ_error env Parse_ast.Unknown ("Could not prove constraints " ^ string_of_list ", " string_of_n_constraint ncs
diff --git a/src/type_check.mli b/src/type_check.mli
index 81f769ba..eab96b07 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -154,8 +154,6 @@ module Env : sig
      won't throw any exceptions. *)
   val get_ret_typ : t -> typ option
 
-  val get_typ_synonym : id -> t -> (t -> typ_arg list -> typ_arg)
-
   val get_overloads : id -> t -> id list
 
   val is_extern : id -> t -> string -> bool