Allow arbitrary identifiers in nexp expressions

Fixed some bugs in the initial check that caused valid code to fail to
parse

Add a nid utility function that creates an id n-expression, similar to
nvar, nconstant etc

5 files changed, 24 insertions, 41 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index cfdf9807..7be3a940 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -219,49 +219,28 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp)
     ), l)
 
 and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp =
-  (*let _ = Printf.eprintf "to_ast_nexp\n" in*)
   match n with
   | Parse_ast.ATyp_aux(t,l) ->
     (match t with
-     | Parse_ast.ATyp_id(i) ->
-       let i = to_ast_id i in
-       let v = id_to_string i in
-       let mk = Envmap.apply k_env v in
-       (match mk with
-        | Some(k) -> Nexp_aux((match k.k with
-            | K_Nat -> Nexp_id i
-            | K_infer -> k.k <- K_Nat; Nexp_id i
-            | _ -> typ_error l "Required an identifier with kind Nat, encountered " (Some i) None (Some k)),l)
-        | None -> typ_error l "Encountered an unbound variable" (Some i) None None)
-     | Parse_ast.ATyp_var(v) ->                 
-       let v = to_ast_var v in
-       let mk = Envmap.apply k_env (var_to_string v) in
-       (*let _ = 
-         Envmap.iter (fun v' k -> Printf.eprintf "%s -> %s, %s =? %b\n"
-         v' (kind_to_string k) (var_to_string v) ((var_to_string v) = v') ) k_env 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)
-    | Parse_ast.ATyp_constant(i) -> Nexp_aux(Nexp_constant(i),l)
-    | Parse_ast.ATyp_sum(t1,t2) ->
-      let n1 = to_ast_nexp k_env t1 in
-      let n2 = to_ast_nexp k_env t2 in
-      Nexp_aux(Nexp_sum(n1,n2),l)
-    | Parse_ast.ATyp_exp(t1) -> Nexp_aux(Nexp_exp(to_ast_nexp k_env t1),l)
-    | Parse_ast.ATyp_neg(t1) -> Nexp_aux(Nexp_neg(to_ast_nexp k_env t1),l)
-    | Parse_ast.ATyp_times(t1,t2) ->
-      let n1 = to_ast_nexp k_env t1 in
-      let n2 = to_ast_nexp k_env t2 in
-      Nexp_aux(Nexp_times(n1,n2),l)
-    | Parse_ast.ATyp_minus(t1,t2) ->
-      let n1 = to_ast_nexp k_env t1 in
-      let n2 = to_ast_nexp k_env t2 in
-      Nexp_aux(Nexp_minus(n1,n2),l)
-    | _ -> typ_error l "Requred an item of kind Nat, encountered an illegal form for this kind" None None None)
-    
+     | Parse_ast.ATyp_id i -> Nexp_aux (Nexp_id (to_ast_id i), l)
+     | Parse_ast.ATyp_var v -> Nexp_aux (Nexp_var (to_ast_var v), l)
+     | Parse_ast.ATyp_constant i -> Nexp_aux (Nexp_constant i, l)
+     | Parse_ast.ATyp_sum (t1, t2) ->
+        let n1 = to_ast_nexp k_env t1 in
+        let n2 = to_ast_nexp k_env t2 in
+        Nexp_aux (Nexp_sum (n1, n2), l)
+     | Parse_ast.ATyp_exp t1 -> Nexp_aux(Nexp_exp(to_ast_nexp k_env t1),l)
+     | Parse_ast.ATyp_neg t1 -> Nexp_aux(Nexp_neg(to_ast_nexp k_env t1),l)
+     | Parse_ast.ATyp_times (t1, t2) ->
+        let n1 = to_ast_nexp k_env t1 in
+        let n2 = to_ast_nexp k_env t2 in
+        Nexp_aux (Nexp_times (n1, n2), l)
+     | Parse_ast.ATyp_minus (t1, t2) ->
+        let n1 = to_ast_nexp k_env t1 in
+        let n2 = to_ast_nexp k_env t2 in
+        Nexp_aux (Nexp_minus (n1, n2), l)
+     | _ -> typ_error l "Requred an item of kind Nat, encountered an illegal form for this kind" None None None)
+
 and to_ast_order (k_env : kind Envmap.t) (def_ord : order) (o: Parse_ast.atyp) : Ast.order =
   match o with
   | Parse_ast.ATyp_aux(t,l) ->
diff --git a/src/parser.mly b/src/parser.mly
index 8e5023c8..62a2c9f4 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -427,6 +427,8 @@ nexp_typ4:
     { tlocl (ATyp_constant $1) 1 1 }
   | tid
     { tloc (ATyp_id $1) }
+  | Lcurly id Rcurly
+    { tloc (ATyp_id $2) }
   | tyvar
     { tloc (ATyp_var $1) }
   | Lparen tup_typ Rparen
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 5c3339c6..a627328d 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -209,7 +209,7 @@ let doc_typ, doc_atomic_typ, doc_nexp =
   | _ -> atomic_nexp_typ ne
   and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with
     | Nexp_var v -> doc_var v
-    | Nexp_id i  -> doc_id i
+    | Nexp_id i  -> braces (doc_id i)
     | Nexp_constant i -> doc_int i
     | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _->
       group (parens (nexp ne))
diff --git a/src/type_check.ml b/src/type_check.ml
index c2351a8a..320a4a34 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -119,6 +119,7 @@ let nsum n1 n2 = Nexp_aux (Nexp_sum (n1, n2), Parse_ast.Unknown)
 let ntimes n1 n2 = Nexp_aux (Nexp_times (n1, n2), Parse_ast.Unknown)
 let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown)
 let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown)
+let nid id = Nexp_aux (Nexp_id id, Parse_ast.Unknown)
 
 let nc_eq n1 n2 = mk_nc (NC_fixed (n1, n2))
 let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2))
diff --git a/src/type_check.mli b/src/type_check.mli
index 92465cd5..647feaaa 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -147,6 +147,7 @@ val nsum : nexp -> nexp -> nexp
 val ntimes : nexp -> nexp -> nexp
 val npow2 : nexp -> nexp
 val nvar : kid -> nexp
+val nid : id -> nexp
 
 (* Sail builtin types. *)
 val int_typ : typ