Add function's name for external tag, using register when a register

3 files changed, 17 insertions, 16 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index a75c690f..c9b12fe6 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -377,12 +377,12 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
         (match t.t,expect_t.t with 
         | Tfn _,_ -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is bound to a function and cannot be used as a value")
         | Tapp("register",[TA_typ(t')]),Tapp("register",[TA_typ(expect_t')]) -> 
-          let tannot = Some(([],t),External,cs,ef) in
+          let tannot = Some(([],t),External (Some "register"),cs,ef) in
           let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_t' in
           (e',t',t_env,cs@cs',ef)
         | Tapp("register",[TA_typ(t')]),_ ->
 	  let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
-          let tannot = Some(([],t),External,cs,ef') in
+          let tannot = Some(([],t),External (Some "register"),cs,ef') in
           let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_t in
           (e',t',t_env,cs@cs',ef)
         | Tapp("reg",[TA_typ(t)]),_ ->
@@ -866,7 +866,7 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema
 	  (match t.t with
 	    | Tapp("register",[TA_typ u]) ->
 	      let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in
-	      (LEXP_aux(lexp,(l,(Some(([],t),External,cs,ef)))),u,Envmap.empty,External,[],ef)
+	      (LEXP_aux(lexp,(l,(Some(([],t),External (Some "register"),cs,ef)))),u,Envmap.empty,External (Some "register"),[],ef)
 	    | Tapp("reg",[TA_typ u]) ->
 	      (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),u,Envmap.empty,Emp,[],pure_e)
 	    | _ -> 
@@ -881,7 +881,7 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema
       let i = id_to_string id in
       (match Envmap.apply t_env i with
 	| Some(Some((parms,t),tag,cs,ef)) ->
-	  let is_external = match tag with | External -> true | _ -> false in
+	  let is_external = match tag with | External any -> true | _ -> false in
 	  let t,cs,ef = subst parms t cs ef in
 	  let t,cs,ef = match get_abbrev d_env t with
 	    | None -> t,cs,ef
@@ -1109,11 +1109,11 @@ let check_val_spec envs (VS_aux(vs,(l,annot))) =
       (VS_aux(vs,(l,tannot)),
        Env(d_env,(Envmap.insert t_env (id_to_string id,tannot))))
     | VS_extern_no_rename(typs,id) ->
-      let tannot = typschm_to_tannot envs typs External in
+      let tannot = typschm_to_tannot envs typs (External None) in
       (VS_aux(vs,(l,tannot)),
        Env(d_env,(Envmap.insert t_env (id_to_string id,tannot))))
     | VS_extern_spec(typs,id,s) ->
-      let tannot = typschm_to_tannot envs typs External in
+      let tannot = typschm_to_tannot envs typs (External (Some s)) in
       (VS_aux(vs,(l,tannot)),
        Env(d_env,(Envmap.insert t_env (id_to_string id,tannot))))
 
@@ -1190,8 +1190,9 @@ let check_def envs (DEF_aux(def,(l,annot))) =
 			     (DEF_aux((DEF_default(ds)),(l,annot)),envs)
     | DEF_reg_dec(typ,id) -> 
       let t = (typ_to_t typ) in
-      let tannot = into_register (Some(([],t),External,[],pure_e)) in 
-      (DEF_aux(def,(l,tannot)),(Env(d_env,Envmap.insert t_env ((id_to_string id),tannot))))
+      let i = id_to_string id in
+      let tannot = into_register (Some(([],t),External (Some i),[],pure_e)) in 
+      (DEF_aux(def,(l,tannot)),(Env(d_env,Envmap.insert t_env (i,tannot))))
 
 
 (*val check : envs ->  tannot defs -> tannot defs*)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index f43b797c..d0d228ca 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -59,7 +59,7 @@ and t_arg =
 
 type tag =
   | Emp
-  | External
+  | External of string option
   | Default
   | Constructor
   | Enum
@@ -198,11 +198,11 @@ let nat_typ = {t=Tid "nat"}
 let pure_e = {effect=Eset []}
 let initial_typ_env =
   Envmap.from_list [
-    ("ignore",Some(([("a",{k=K_Typ});("b",{k=K_Efct})],{t=Tfn ({t=Tvar "a"},unit_t,{effect=Evar "b"})}),External,[],pure_e));
-    ("+",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e));
-    ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e));
-    ("-",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e));
-    ("|",Some(([],{t= Tfn ({t=Ttup([bit_t;bit_t])},bit_t,pure_e)}),External,[],pure_e));
+    ("ignore",Some(([("a",{k=K_Typ});("b",{k=K_Efct})],{t=Tfn ({t=Tvar "a"},unit_t,{effect=Evar "b"})}),External None,[],pure_e));
+    ("+",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "add"),[],pure_e));
+    ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "multiply"),[],pure_e));
+    ("-",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "minus"),[],pure_e));
+    ("|",Some(([],{t= Tfn ({t=Ttup([bit_t;bit_t])},bit_t,pure_e)}),External (Some "bitwise_or"),[],pure_e));
   ]
 
 let initial_abbrev_env =
@@ -542,7 +542,7 @@ let rec type_coerce l d_env t1 e t2 =
 		   (l,Some(([],t2),Emp,[],pure_e))))
 	  | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2))))
   | Tid("bit"),Tid("bool") ->
-    let e' = E_aux(E_app((Id_aux(Id "is_one",l)),[e]),(l,Some(([],bool_t),External,[],pure_e))) in
+    let e' = E_aux(E_app((Id_aux(Id "is_one",l)),[e]),(l,Some(([],bool_t),External None,[],pure_e))) in
     (t2,[],e')
   | Tid(i),Tapp("enum",[TA_nexp b1;TA_nexp r1;]) -> 
     (match get_abbrev d_env t1 with
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 13cb56ea..c00182ef 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -54,7 +54,7 @@ and t_arg =
 
 type tag =
   | Emp
-  | External
+  | External of string option
   | Default
   | Constructor
   | Enum