Refactored AST valspecs into single constructor

12 files changed, 51 insertions, 90 deletions

diff --git a/src/ast.ml b/src/ast.ml
index ff3c998d..c4b225f1 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -490,11 +490,7 @@ type_def_aux =  (* Type definition body *)
 
 type
 val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
- | VS_extern_no_rename of typschm * id
- | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
- | VS_cast_spec of typschm * id
-
+   VS_val_spec of typschm * id * string option * bool
 
 type
 'a kind_def_aux =  (* Definition body for elements of kind; many are shorthands for type\_defs *)
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 3e4cae51..9f5fd4e6 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -589,20 +589,9 @@ let to_ast_spec (names,k_env,default_order) (val_:Parse_ast.val_spec) : (unit va
   match val_ with
   | Parse_ast.VS_aux(vs,l) ->
     (match vs with
-    | Parse_ast.VS_val_spec(ts,id) ->
-      (*let _ = Printf.eprintf "to_ast_spec called for internal spec: for %s\n" (id_to_string (to_ast_id id)) in*)
+    | Parse_ast.VS_val_spec(ts,id,ext,is_cast) ->
       let typsch,_,_ = to_ast_typschm k_env default_order ts in
-      VS_aux(VS_val_spec(typsch,to_ast_id id),(l,())),(names,k_env,default_order)
-    | Parse_ast.VS_extern_spec(ts,id,s) ->
-      let typsch,_,_ = to_ast_typschm k_env default_order ts in
-      VS_aux(VS_extern_spec(typsch,to_ast_id id,s),(l,())),(names,k_env,default_order)
-    | Parse_ast.VS_cast_spec(ts,id) ->
-      let typsch,_,_ = to_ast_typschm k_env default_order ts in
-      VS_aux(VS_cast_spec(typsch,to_ast_id id),(l,())),(names,k_env,default_order)
-    | Parse_ast.VS_extern_no_rename(ts,id) ->
-      let typsch,_,_ = to_ast_typschm k_env default_order ts in
-       VS_aux(VS_extern_no_rename(typsch,to_ast_id id),(l,())),(names,k_env,default_order))
-    
+      VS_aux(VS_val_spec(typsch,to_ast_id id,ext,is_cast),(l,())),(names,k_env,default_order))
 
 let to_ast_namescm (Parse_ast.Name_sect_aux(ns,l)) = 
   Name_sect_aux(
@@ -923,15 +912,12 @@ let typschm_of_string order str =
   let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
   typschm
 
-let val_spec_of_string order id str = mk_val_spec (VS_extern_no_rename (typschm_of_string order str, id))
+let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, Some str, false))
 
 let val_spec_ids (Defs defs) =
   let val_spec_id (VS_aux (vs_aux, _)) =
     match vs_aux with
-    | VS_val_spec (typschm, id) -> id
-    | VS_extern_no_rename (typschm, id) -> id
-    | VS_extern_spec (typschm, id, e) -> id
-    | VS_cast_spec (typschm, id) -> id
+    | VS_val_spec (_, id, _, _) -> id
   in
   let rec vs_ids = function
     | DEF_spec vs :: defs -> val_spec_id vs :: vs_ids defs
@@ -979,19 +965,19 @@ let generate_undefineds vs_ids (Defs defs) =
   let undefined_td = function
     | TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in
-       [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id));
+       [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, None, false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             (mk_pat (P_lit (mk_lit L_unit)))
                             (mk_exp (E_app (mk_id "internal_pick",
                                             [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]]
     | TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in
-       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id));
+       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None, false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             pat
                             (mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]]
     | TD_variant (id, _, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
-       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id));
+       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None, false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             (mk_pat (P_lit (mk_lit L_unit)))
                             (mk_exp (E_app (mk_id "internal_pick",
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 301d53fb..a4ced725 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -278,10 +278,8 @@ let ocaml_typedef ctx (TD_aux (td_aux, _)) =
 let get_externs (Defs defs) =
   let extern_id (VS_aux (vs_aux, _)) =
     match vs_aux with
-    | VS_val_spec (typschm, id) -> []
-    | VS_extern_no_rename (typschm, id) -> [(id, id)]
-    | VS_extern_spec (typschm, id, name) -> [(id, mk_id name)]
-    | VS_cast_spec (typschm, id) -> []
+    | VS_val_spec (typschm, id, None, _) -> []
+    | VS_val_spec (typschm, id, Some ext, _) -> [(id, mk_id ext)]
   in
   let rec extern_ids = function
     | DEF_spec vs :: defs -> extern_id vs :: extern_ids defs
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 1776d510..73f75919 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -422,10 +422,7 @@ type_def_aux =  (* Type definition body *)
 
 type 
 val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
- | VS_extern_no_rename of typschm * id
- | VS_extern_spec of typschm * id * string
- | VS_cast_spec of typschm * id
+   VS_val_spec of typschm * id * string option * bool
 
 
 type 
diff --git a/src/parser.mly b/src/parser.mly
index 8e7d81c6..dd0981fc 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -51,6 +51,10 @@ let locn m n = Range(Parsing.rhs_start_pos m,Parsing.rhs_end_pos n)
 
 let idl i = Id_aux(i, loc())
 
+let string_of_id = function
+  | Id_aux (Id str, _) -> str
+  | Id_aux (DeIid str, _) -> str
+
 let efl e = BE_aux(e, loc())
 
 let ploc p = P_aux(p,loc ())
@@ -1041,21 +1045,21 @@ fun_def:
 
 val_spec:
   | Val typquant typ id
-    { vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4)) }
+    { vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4, None, false)) }
   | Val typ id
-    { vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3)) }
+    { vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3, None, false)) }
   | Val Cast typquant typ id
-    { vloc (VS_cast_spec (mk_typschm $3 $4 3 4,$5)) }
+    { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, None, true)) }
   | Val Cast typ id
-    { vloc (VS_cast_spec (mk_typschm (mk_typqn ()) $3 3 3, $4)) }
+    { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, None, true)) }
   | Val Extern typquant typ id
-    { vloc (VS_extern_no_rename (mk_typschm $3 $4 3 4,$5)) }
+    { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some (string_of_id $5), false)) }
   | Val Extern typ id
-    { vloc (VS_extern_no_rename (mk_typschm (mk_typqn ()) $3 3 3, $4)) }
+    { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, Some (string_of_id $4), false)) }
   | Val Extern typquant typ id Eq String
-    { vloc (VS_extern_spec (mk_typschm $3 $4 3 4,$5,$7)) }
+    { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some $7, false)) }
   | Val Extern typ id Eq String
-    { vloc (VS_extern_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, $6)) }
+    { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, Some $6, false)) }
 
 kinded_id:
   | tyvar
diff --git a/src/parser2.mly b/src/parser2.mly
index 3de9b4f4..c00287e0 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -942,7 +942,7 @@ let_def:
 
 val_spec_def:
   | Val id Colon typschm
-    { mk_vs (VS_val_spec ($4, $2)) $startpos $endpos }
+    { mk_vs (VS_val_spec ($4, $2, None, false)) $startpos $endpos }
 
 register_def:
   | Register id Colon typ
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 7f04c495..d40381b9 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1429,13 +1429,7 @@ let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) =
   | DEC_alias(id,alspec) -> empty
   | DEC_typ_alias(typ,id,alspec) -> empty
 
-let doc_spec_lem mwords (VS_aux (valspec,annot)) =
-  match valspec with
-  | VS_extern_no_rename _
-  | VS_extern_spec _ -> empty (* ignore these at the moment *)
-  | VS_val_spec (typschm,id) | VS_cast_spec (typschm,id) -> empty
-(* separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem mwords typschm] ^/^ hardline *)
-
+let doc_spec_lem mwords (VS_aux (valspec,annot)) = empty
 
 let rec doc_def_lem sequential mwords def = match def with
   | DEF_spec v_spec -> (doc_spec_lem mwords v_spec,empty)
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 26249f75..a7631843 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -506,17 +506,17 @@ let pp_lem_default ppf (DT_aux(df,l)) =
   in
   fprintf ppf "@[<0>(DT_aux %a %a)@]" print_de df pp_lem_l l
 
+(* FIXME *)
 let pp_lem_spec ppf (VS_aux(v,(l,annot))) =
   let print_spec ppf v =
     match v with
-    | VS_val_spec(ts,id) ->
+    | VS_val_spec(ts,id,None,false) ->
       fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id
-    | VS_extern_spec(ts,id,s) ->
+    | VS_val_spec(ts,id,Some s,false) ->
       fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s
-    | VS_extern_no_rename(ts,id) ->
-      fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_extern_no_rename" pp_lem_typscm ts pp_lem_id id
-    | VS_cast_spec(ts,id) ->
-      fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_cast_spec" pp_lem_typscm ts pp_lem_id id
+    | VS_val_spec(ts,id,None,true) ->
+       fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_cast_spec" pp_lem_typscm ts pp_lem_id id
+    | _ -> failwith "Invalid valspec"
   in
   fprintf ppf "@[<0>(VS_aux %a (%a, %a))@]" print_spec v pp_lem_l l pp_annot annot
 
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 0f943efa..72218bc3 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -385,15 +385,14 @@ let doc_default (DT_aux(df,_)) = match df with
   | DT_order(ord) -> separate space [string "default"; string "Order"; doc_ord ord]
 
 let doc_spec (VS_aux(v,_)) = match v with
-  | VS_val_spec(ts,id) ->
+  | VS_val_spec(ts,id,None,false) ->
      separate space [string "val"; doc_typscm ts; doc_id id]
-  | VS_cast_spec (ts, id) ->
+  | VS_val_spec (ts, id,None,true) ->
      separate space [string "val"; string "cast"; doc_typscm ts; doc_id id]
-  | VS_extern_no_rename(ts,id) ->
-     separate space [string "val"; string "extern"; doc_typscm ts; doc_id id]
-  | VS_extern_spec(ts,id,s) ->
+  | VS_val_spec(ts,id,Some ext,false) ->
      separate space [string "val"; string "extern"; doc_typscm ts;
-                     doc_op equals (doc_id id) (dquotes (string s))]
+                     doc_op equals (doc_id id) (dquotes (string ext))]
+  | _ -> failwith "Invalid valspec"
 
 let doc_namescm (Name_sect_aux(ns,_)) = match ns with
   | Name_sect_none -> empty
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 0f46afa5..5c6aa0d8 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1290,15 +1290,10 @@ let rewrite_sizeof (Defs defs) =
         TypSchm_aux (TypSchm_ts (tq, typ'), l)
       else ts in
     match def with
-    | DEF_spec (VS_aux (VS_val_spec (typschm, id), a)) ->
-       DEF_spec (VS_aux (VS_val_spec (rewrite_typschm typschm id, id), a))
-    | DEF_spec (VS_aux (VS_extern_no_rename (typschm, id), a)) ->
-       DEF_spec (VS_aux (VS_extern_no_rename (rewrite_typschm typschm id, id), a))
-    | DEF_spec (VS_aux (VS_extern_spec (typschm, id, e), a)) ->
-       DEF_spec (VS_aux (VS_extern_spec (rewrite_typschm typschm id, id, e), a))
-    | DEF_spec (VS_aux (VS_cast_spec (typschm, id), a)) ->
-       DEF_spec (VS_aux (VS_cast_spec (rewrite_typschm typschm id, id), a))
-    | _ -> def in
+    | DEF_spec (VS_aux (VS_val_spec (typschm, id, ext, is_cast), a)) ->
+       DEF_spec (VS_aux (VS_val_spec (rewrite_typschm typschm id, id, ext, is_cast), a))
+    | def -> def
+  in
 
   let (params_map, defs) = List.fold_left rewrite_sizeof_def
                                           (Bindings.empty, []) defs in
@@ -2410,10 +2405,7 @@ let rewrite_dec_spec_typs rw_typ (DEC_aux (ds, annot)) =
 let rewrite_overload_cast (Defs defs) =
   let remove_cast_vs (VS_aux (vs_aux, annot)) =
     match vs_aux with
-    | VS_val_spec (typschm, id) -> VS_aux (VS_val_spec (typschm, id), annot)
-    | VS_extern_no_rename (typschm, id) -> VS_aux (VS_extern_no_rename (typschm, id), annot)
-    | VS_extern_spec (typschm, id, e) -> VS_aux (VS_extern_spec (typschm, id, e), annot)
-    | VS_cast_spec (typschm, id) -> VS_aux (VS_val_spec (typschm, id), annot)
+    | VS_val_spec (typschm, id, ext, _) -> VS_aux (VS_val_spec (typschm, id, ext, false), annot)
   in
   let simple_def = function
     | DEF_spec vs -> DEF_spec (remove_cast_vs vs)
@@ -2490,10 +2482,7 @@ let rewrite_simple_types (Defs defs) =
   in
   let simple_vs (VS_aux (vs_aux, annot)) =
     match vs_aux with
-    | VS_val_spec (typschm, id) -> VS_aux (VS_val_spec (simple_typschm typschm, id), annot)
-    | VS_extern_no_rename (typschm, id) -> VS_aux (VS_extern_no_rename (simple_typschm typschm, id), annot)
-    | VS_extern_spec (typschm, id, e) -> VS_aux (VS_extern_spec (simple_typschm typschm, id, e), annot)
-    | VS_cast_spec (typschm, id) -> VS_aux (VS_cast_spec (simple_typschm typschm, id), annot)
+    | VS_val_spec (typschm, id, ext, is_cast) -> VS_aux (VS_val_spec (simple_typschm typschm, id, ext, is_cast), annot)
   in
   let rec simple_lit (L_aux (lit_aux, l) as lit) =
     match lit_aux with
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index ddba4a6f..2e368c53 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -460,8 +460,7 @@ let fv_of_fun consider_var (FD_aux (FD_function(rec_opt,tannot_opt,_,funcls),_))
   init_env fun_name,Nameset.union ns ns_r
 
 let fv_of_vspec consider_var (VS_aux(vspec,_)) = match vspec with
-  | VS_val_spec(ts,id) | VS_extern_no_rename (ts,id) | VS_extern_spec(ts,id,_)
-  | VS_cast_spec(ts,id) ->
+  | VS_val_spec(ts,id,_,_) ->
      init_env ("val:" ^ (string_of_id id)), snd (fv_of_typschm consider_var mt mt ts)
 
 let rec find_scattered_of name = function
diff --git a/src/type_check.ml b/src/type_check.ml
index 3bbd2323..33c6ff6d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -3050,7 +3050,7 @@ let infer_funtyp l env tannotopt funcls =
      end
   | Typ_annot_opt_aux (Typ_annot_opt_none, _) -> typ_error l "Cannot infer function type for unannotated function"
 
-let mk_val_spec typq typ id = DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id), (Parse_ast.Unknown, None)))
+let mk_val_spec typq typ id = DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id, None, false), (Parse_ast.Unknown, None)))
 
 let check_tannotopt env typq ret_typ = function
   | Typ_annot_opt_aux (Typ_annot_opt_none, _) -> ()
@@ -3101,14 +3101,13 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
    the difference is irrelevant for the typechecker. *)
 let check_val_spec env (VS_aux (vs, (l, _))) =
   let (id, quants, typ, env) = match vs with
-    | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> (id, quants, typ, env)
-    | VS_cast_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> (id, quants, typ, Env.add_cast id env)
-    | VS_extern_no_rename (TypSchm_aux (TypSchm_ts (quants, typ), _), id) ->
-      let env = Env.add_extern id (string_of_id id) env in
-      (id, quants, typ, env)
-    | VS_extern_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, ext) ->
-      let env = Env.add_extern id ext env in
-      (id, quants, typ, env) in
+    | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, None, false) -> (id, quants, typ, env)
+    | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, None, true) -> (id, quants, typ, Env.add_cast id env)
+    | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, Some ext, false) ->
+       let env = Env.add_extern id ext env in
+       (id, quants, typ, env)
+    | _ -> typ_error l "Invalid valspec"
+  in
   [DEF_spec (VS_aux (vs, (l, None)))], Env.add_val_spec id (quants, Env.expand_synonyms env typ) env
 
 let check_default env (DT_aux (ds, l)) =