diff options
| -rw-r--r-- | src/pretty_print.ml | 156 | ||||
| -rw-r--r-- | src/type_check.ml | 59 | ||||
| -rw-r--r-- | src/type_internal.ml | 19 | ||||
| -rw-r--r-- | src/type_internal.mli | 3 |
4 files changed, 174 insertions, 63 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index e01fbc3e..cd5b1b91 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -287,6 +287,8 @@ and pp_format_o o = let pp_format_tag = function | Emp_local -> "Tag_empty" + | Emp_intro -> "Tag_empty" (*TODO carry this out for use in future analysis that doesn't use the interpreter?*) + | Emp_set -> "Tag_empty" (* Same as above *) | Emp_global -> "Tag_global" | External (Some s) -> "(Tag_extern (Just \""^s^"\"))" | External None -> "(Tag_extern Nothing)" @@ -619,6 +621,7 @@ let doc_bkind (BK_aux(k,_)) = let doc_op symb a b = infix 2 1 symb a b let doc_unop symb a = prefix 2 1 symb a +let pipe = string "|" let arrow = string "->" let dotdot = string ".." let coloneq = string ":=" @@ -1248,18 +1251,24 @@ let doc_typ_ocaml, doc_atomic_typ_ocaml = let doc_lit_ocaml (L_aux(l,_)) = utf8string (match l with | L_unit -> "()" - | L_zero -> "V0" - | L_one -> "V1" - | L_true -> "V1" - | L_false -> "V0" + | L_zero -> "0" + | L_one -> "1" + | L_true -> "1" + | L_false -> "0" | L_num i -> string_of_int i | L_hex n -> "(num_to_vec" ^ ("0x" ^ n) ^ ")" | L_bin n -> "(num_to_vec" ^ ("0b" ^ n) ^ ")" - | L_undef -> "Vundef" + | L_undef -> "2" | L_string s -> "\"" ^ s ^ "\"") -(*Note: vector, vector concatenation, literal vectors, indexed vectors, record, and list patterns should - be removed prior to pp. The latter three have never yet been seen +(* typ_doc is the doc for the type being quantified *) +let doc_typquant_ocaml (TypQ_aux(tq,_)) typ_doc = typ_doc + +let doc_typscm_ocaml (TypSchm_aux(TypSchm_ts(tq,t),_)) = + (doc_typquant tq (doc_typ_ocaml t)) + +(*Note: vector concatenation, literal vectors, indexed vectors, and record should + be removed prior to pp. The latter two have never yet been seen *) let doc_pat_ocaml, doc_atomic_pat_ocaml = let rec pat pa = app_pat pa @@ -1271,10 +1280,22 @@ let doc_pat_ocaml, doc_atomic_pat_ocaml = | P_wild -> underscore | P_id id -> doc_id id | P_as(p,id) -> parens (separate space [pat p; string "as"; doc_id_ocaml id]) - | P_typ(typ,p) -> (*separate space [parens (doc_typ typ); atomic_pat p]*) pat p + | P_typ(typ,p) -> doc_op colon (pat p) (doc_typ_ocaml typ) | P_app(id,[]) -> doc_id_ocaml id + | P_vector pats -> + let non_bit_print () = parens (separate space [string "VvectorR"; squarebars (separate_map semi pat pats); underscore ; underscore]) in + (match annot with + | Base(([],t),_,_,_,_) -> + (match t.t with + | Tapp("vector",[_;_;_;TA_typ t]) | Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ t])}) -> + (match t.t with + | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> + parens (separate space [string "Vvector"; squarebars (separate_map semi pat pats); underscore ; underscore]) + | _ -> non_bit_print ()) + | _ -> non_bit_print ()) + | _ -> non_bit_print ()) | P_tup pats -> parens (separate_map comma_sp atomic_pat pats) - (* expose doc_pat and doc_atomic_pat *) + | P_list pats -> brackets (separate_map semi pat pats) (*Never seen but easy in ocaml*) in pat, atomic_pat let doc_exp_ocaml, doc_let_ocaml = @@ -1288,9 +1309,7 @@ let doc_exp_ocaml, doc_let_ocaml = doc_op coloneq (doc_lexp le) (exp e) | E_vector_append(l,r) -> group (parens (string "vector_append ") ^^ (exp l) ^^ space ^^ (exp r)) - | E_cons(l,r) -> - doc_op (group (colon^^colon)) (exp l) (exp r) - (* Special case: omit "else ()" when the else branch is empty. *) + | E_cons(l,r) -> doc_op (group (colon^^colon)) (exp l) (exp r) | E_if(c,t,E_aux(E_block [], _)) -> string "if" ^^ space ^^ string "toBool" ^^ (exp c) ^/^ string "then" ^^ space ^^ (exp t) @@ -1311,7 +1330,7 @@ let doc_exp_ocaml, doc_let_ocaml = | _ -> string "make a while loop") | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e) | E_app(f,args) -> - (*TODO, check for external call*) + (*TODO, check for external call, make call-by-copy semantics*) doc_unop (doc_id f) (parens (separate_map comma exp args)) | E_vector_access(v,e) -> parens ((string "vector_access") ^^ space ^^ exp v ^^ space ^^ exp e) @@ -1333,7 +1352,7 @@ let doc_exp_ocaml, doc_let_ocaml = braces (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps)) | E_vector exps -> (*TODO pull out direction and base value*) - group ((string "make_vector") ^^ space ^^ brackets (separate_map semi exp exps)) + group ((string "make_vector") ^^ space ^^ squarebars (separate_map semi exp exps)) | E_vector_indexed (iexps, (Def_val_aux (default,_))) -> (*TODO, indexed vectors shouldn't be in anymore by this point*) let default_string = @@ -1359,7 +1378,7 @@ let doc_exp_ocaml, doc_let_ocaml = | E_exit e -> separate space [string "exit"; exp e;] | E_app_infix (e1,id,e2) -> - group (parens (exp e1)) + separate space [string "get_external_function_name"; parens (separate_map semi exp [e1;e2])] and let_exp (LB_aux(lb,_)) = match lb with | LB_val_explicit(ts,pat,e) -> @@ -1374,28 +1393,103 @@ let doc_exp_ocaml, doc_let_ocaml = and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id id) (exp e) and doc_case (Pat_aux(Pat_exp(pat,e),_)) = - doc_op arrow (separate space [string "case"; doc_atomic_pat pat]) (group (exp e)) + doc_op arrow (separate space [pipe; doc_atomic_pat pat]) (group (exp e)) (* lexps are parsed as eq_exp - we need to duplicate the precedence * structure for them *) - and doc_lexp le = app_lexp le - and app_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with + and doc_lexp ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with + (*TODO: in the case of vector and memory and field, need to lift these up to rewrite them differently. *) | LEXP_memory(id,args) -> doc_id id ^^ parens (separate_map comma exp args) - | _ -> vaccess_lexp le - and vaccess_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with - | LEXP_vector(v,e) -> atomic_lexp v ^^ brackets (exp e) + | LEXP_vector(v,e) -> doc_lexp v ^^ brackets (exp e) | LEXP_vector_range(v,e1,e2) -> - atomic_lexp v ^^ brackets (exp e1 ^^ dotdot ^^ exp e2) - | _ -> field_lexp le - and field_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with - | LEXP_field(v,id) -> atomic_lexp v ^^ dot ^^ doc_id id - | _ -> atomic_lexp le - and atomic_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with - | LEXP_id id -> doc_id id - | LEXP_cast(typ,id) -> prefix 2 1 (parens (doc_typ typ)) (doc_id id) - | LEXP_memory _ | LEXP_vector _ | LEXP_vector_range _ - | LEXP_field _ -> group (parens (doc_lexp le)) + doc_lexp v ^^ brackets (exp e1 ^^ dotdot ^^ exp e2) + | LEXP_field(v,id) -> doc_lexp v ^^ dot ^^ doc_id id + | LEXP_id id -> doc_id_ocaml id + | LEXP_cast(typ,id) -> (*prefix 2 1 (parens (doc_typ typ)) *) (doc_id_ocaml id) (* expose doc_exp and doc_let *) in exp, let_exp +(*TODO Upcase and downcase type and constructors as needed*) +let doc_type_union_ocaml (Tu_aux(typ_u,_)) = match typ_u with + | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_ocaml id; string "of"; doc_typ_ocaml typ;] + | Tu_id id -> separate space [pipe; doc_id_ocaml id] + +let doc_typdef_ocaml (TD_aux(td,_)) = match td with + | TD_abbrev(id,nm,typschm) -> + doc_op equals (concat [string "type"; space; doc_id id;]) (doc_typscm_ocaml typschm) + | TD_record(id,nm,typq,fs,_) -> + let f_pp (typ,id) = concat [doc_id id; space; colon; doc_typ_ocaml typ; semi] in + let fs_doc = group (separate_map (break 1) f_pp fs) in + doc_op equals + (concat [string "type"; space; doc_id_ocaml id;]) (doc_typquant_ocaml typq (braces fs_doc)) + | TD_variant(id,nm,typq,ar,_) -> + let ar_doc = group (separate_map (break 1) doc_type_union_ocaml ar) in + doc_op equals + (concat [string "type"; space; doc_id_ocaml id;]) + (doc_typquant_ocaml typq ar_doc) + | TD_enum(id,nm,enums,_) -> + let enums_doc = group (separate_map (break 1 ^^ pipe) doc_id_ocaml enums) in + doc_op equals + (concat [string "type"; space; doc_id_ocaml id;]) + (enums_doc) + | TD_register(id,n1,n2,rs) -> + (*TODO: not sure*) + let doc_rid (r,id) = separate space [doc_range r; colon; doc_id id] ^^ semi in + let doc_rids = group (separate_map (break 1) doc_rid rs) in + string "(*" ^^ + doc_op equals + (string "typedef" ^^ space ^^ doc_id id) + (separate space [ + string "register bits"; + brackets (doc_nexp n1 ^^ colon ^^ doc_nexp n2); + braces doc_rids; + ]) ^^ string "*)" + +let doc_rec_ocaml (Rec_aux(r,_)) = match r with + | Rec_nonrec -> empty + (* include trailing space because caller doesn't know if we return + * empty *) + | Rec_rec -> string "rec" ^^ space + +let doc_tannot_opt_ocaml (Typ_annot_opt_aux(t,_)) = match t with + | Typ_annot_opt_some(tq,typ) -> doc_typquant_ocaml tq (doc_typ_ocaml typ) + +let doc_funcl_ocaml (FCL_aux(FCL_Funcl(id,pat,exp),_)) = + group (doc_op arrow (doc_pat_ocaml pat) (doc_exp_ocaml exp)) + +let get_id = function + | [] -> failwith "FD_function with empty list" + | (FCL_aux (FCL_Funcl (id,_,_),_))::_ -> id + +let doc_fundef_ocaml (FD_aux(FD_function(r, typa, efa, fcls),_)) = + match fcls with + | [] -> failwith "FD_function with empty function list" + | [FCL_aux (FCL_Funcl(id,pat,exp),_)] -> + separate space [(string "let"); (doc_rec_ocaml r); (doc_id_ocaml id); (doc_pat_ocaml pat); equals; (doc_exp_ocaml exp)] + | _ -> + let id = get_id fcls in + let sep = hardline ^^ pipe ^^ space in + let clauses = separate_map sep doc_funcl fcls in + separate space [string "let"; + doc_rec_ocaml r; + clauses] + +(*Aliases should be removed by here; registers not sure about*) +(*let doc_dec (DEC_aux (reg,_)) = + match reg with + | DEC_reg(typ,id) -> separate space [string "register"; doc_atomic_typ typ; doc_id id] + | DEC_alias(id,alspec) -> + doc_op equals (string "register alias" ^^ space ^^ doc_id id) (doc_alias alspec) + | DEC_typ_alias(typ,id,alspec) -> + doc_op equals (string "register alias" ^^ space ^^ doc_atomic_typ typ) (doc_alias alspec)*) + +let doc_def_ocaml def = group (match def with + | DEF_default df -> empty + | DEF_spec v_spec -> empty (*unless we want to have a separate pass to create mli files*) + | DEF_type t_def -> doc_typdef_ocaml t_def + | DEF_fundef f_def -> doc_fundef_ocaml f_def + | DEF_val lbind -> doc_let_ocaml lbind + | DEF_reg_dec dec -> empty (*unless we want to have something for the declaration of a register and guess a default init value*) + | DEF_scattered sdef -> empty (*shoulnd't still be here*) + ) ^^ hardline diff --git a/src/type_check.ml b/src/type_check.ml index e0e02856..694317f5 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1318,21 +1318,23 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) | LEXP_id id -> let i = id_to_string id in (match Envmap.apply t_env i with - (*TODO Should change this to use the default as the expected type*) - | Some(Base((parms,t),Default,_,_,_)) -> - typ_error l ("Identifier " ^ i ^ " cannot be assigned when only a default specification exists") - | Some(Base(([],t),Alias,_,_,_)) -> - let ef = {effect = Eset[BE_aux(BE_wreg,l)]} in - (match Envmap.apply d_env.alias_env i with - | Some(OneReg(reg, (Base(([],t'),_,_,_,_)))) -> - (LEXP_aux(lexp,(l,(Base(([],t'),Alias,[],ef,nob)))), t, false, Envmap.empty, External (Some reg),[],nob,ef) - | Some(TwoReg(reg1,reg2, (Base(([],t'),_,_,_,_)))) -> - let u = match t.t with - | Tapp("register", [TA_typ u]) -> u - | _ -> raise (Reporting_basic.err_unreachable l "TwoReg didn't contain a register type") in - (LEXP_aux(lexp,(l,Base(([],t'),Alias,[],ef,nob))), u, false, Envmap.empty, External None,[],nob,ef) - | _ -> assert false) - | Some(Base((parms,t),tag,cs,_,b)) -> + | Some(Base((parms,t),Default,_,_,_)) -> + let t = {t=Tapp("reg",[TA_typ t])} in + let bounds = extract_bounds d_env i t in + let tannot = (Base(([],t),Emp_intro,[],pure_e,bounds)) in + (LEXP_aux(lexp,(l,tannot)),t,false,Envmap.from_list [i,tannot],Emp_intro,[],bounds,pure_e) + | Some(Base(([],t),Alias,_,_,_)) -> + let ef = {effect = Eset[BE_aux(BE_wreg,l)]} in + (match Envmap.apply d_env.alias_env i with + | Some(OneReg(reg, (Base(([],t'),_,_,_,_)))) -> + (LEXP_aux(lexp,(l,(Base(([],t'),Alias,[],ef,nob)))), t, false, Envmap.empty, External (Some reg),[],nob,ef) + | Some(TwoReg(reg1,reg2, (Base(([],t'),_,_,_,_)))) -> + let u = match t.t with + | Tapp("register", [TA_typ u]) -> u + | _ -> raise (Reporting_basic.err_unreachable l "TwoReg didn't contain a register type") in + (LEXP_aux(lexp,(l,Base(([],t'),Alias,[],ef,nob))), u, false, Envmap.empty, External None,[],nob,ef) + | _ -> assert false) + | Some(Base((parms,t),tag,cs,_,b)) -> let t,cs,_,_ = match tag with | External _ | Emp_global -> subst parms false t cs pure_e | _ -> t,cs,pure_e,Envmap.empty in @@ -1347,17 +1349,17 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) Envmap.empty,External (Some i),[],nob,ef) | Tapp("reg",[TA_typ u]),_ -> (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs_o,pure_e,b)))),u,false, - Envmap.empty,Emp_local,[],nob,pure_e) + Envmap.empty,Emp_set,[],nob,pure_e) | Tapp("vector",_),false -> - (LEXP_aux(lexp,(l,(Base(([],t),tag,cs_o,pure_e,b)))),t,true,Envmap.empty,Emp_local,[],nob,pure_e) + (LEXP_aux(lexp,(l,(Base(([],t),tag,cs_o,pure_e,b)))),t,true,Envmap.empty,Emp_set,[],nob,pure_e) | (Tfn _ ,_) -> (match tag with | External _ | Spec | Emp_global -> let u = new_t() in let t = {t = Tapp("reg",[TA_typ u])} in let bounds = extract_bounds d_env i t in - let tannot = (Base(([],t),Emp_local,[],pure_e,bounds)) in - (LEXP_aux(lexp,(l,tannot)),u,false,Envmap.from_list [i,tannot],Emp_local,[],bounds,pure_e) + let tannot = (Base(([],t),Emp_intro,[],pure_e,bounds)) in + (LEXP_aux(lexp,(l,tannot)),u,false,Envmap.from_list [i,tannot],Emp_intro,[],bounds,pure_e) | _ -> typ_error l ("Cannot assign to " ^ i ^" with type " ^ t_to_string t ^ ". Assignment must be to registers or non-parameter, non-let-bound local variables.")) @@ -1372,13 +1374,12 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) let u = new_t() in let t = {t=Tapp("reg",[TA_typ u])} in let bounds = extract_bounds d_env i u in - let tannot = (Base(([],t),Emp_local,[],pure_e,bounds)) in - (LEXP_aux(lexp,(l,tannot)),u,false,Envmap.from_list [i,tannot],Emp_local,[],bounds,pure_e)) + let tannot = (Base(([],t),Emp_intro,[],pure_e,bounds)) in + (LEXP_aux(lexp,(l,tannot)),u,false,Envmap.from_list [i,tannot],Emp_intro,[],bounds,pure_e)) | LEXP_memory(id,exps) -> let i = id_to_string id in (match Envmap.apply t_env i with | Some(Base((parms,t),tag,cs,ef,_)) -> - (*let is_external = match tag with | External any -> true | _ -> false in*) let t,cs,ef,_ = subst parms false t cs ef in (match t.t with | Tfn(apps,out,_,ef') -> @@ -1452,18 +1453,18 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) | Tapp("reg",[TA_typ u]),_ -> let t',cs = type_consistent (Expr l) d_env Require false ty u in (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,bs)))),ty,false, - Envmap.empty,Emp_local,[],bs,pure_e) + Envmap.empty,Emp_set,[],bs,pure_e) | Tapp("vector",_),false -> - (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,bs)))),ty,true,Envmap.empty,Emp_local,[],bs,pure_e) + (LEXP_aux(lexp,(l,(Base(([],t),tag,cs,pure_e,bs)))),ty,true,Envmap.empty,Emp_set,[],bs,pure_e) | Tuvar _,_ -> let u' = {t=Tapp("reg",[TA_typ ty])} in equate_t t u'; - (LEXP_aux(lexp,(l,(Base((([],u'),Emp_local,cs,pure_e,bs))))),ty,false,Envmap.empty,Emp_local,[],bs,pure_e) + (LEXP_aux(lexp,(l,(Base((([],u'),Emp_local,cs,pure_e,bs))))),ty,false,Envmap.empty,Emp_set,[],bs,pure_e) | (Tfn _ ,_) -> (match tag with | External _ | Spec | Emp_global -> - let tannot = (Base(([],ty),Emp_local,[],pure_e,new_bounds)) in - (LEXP_aux(lexp,(l,tannot)),ty,false,Envmap.from_list [i,tannot],Emp_local,[],new_bounds,pure_e) + let tannot = (Base(([],ty),Emp_intro,[],pure_e,new_bounds)) in + (LEXP_aux(lexp,(l,tannot)),ty,false,Envmap.from_list [i,tannot],Emp_intro,[],new_bounds,pure_e) | _ -> typ_error l ("Cannot assign to " ^ i ^ " with type " ^ t_to_string t)) | _,_ -> @@ -1476,8 +1477,8 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,nob)))),ty,false,Envmap.empty,Emp_local,[],nob,pure_e)) | _ -> let t = {t=Tapp("reg",[TA_typ ty])} in - let tannot = (Base(([],t),Emp_local,[],pure_e,new_bounds)) in - (LEXP_aux(lexp,(l,tannot)),ty,false,Envmap.from_list [i,tannot],Emp_local,[],new_bounds,pure_e)) + let tannot = (Base(([],t),Emp_intro,[],pure_e,new_bounds)) in + (LEXP_aux(lexp,(l,tannot)),ty,false,Envmap.from_list [i,tannot],Emp_intro,[],new_bounds,pure_e)) | LEXP_vector(vec,acc) -> let (vec',vec_t,reg_required,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in let vec_t,cs' = get_abbrev d_env vec_t in diff --git a/src/type_internal.ml b/src/type_internal.ml index aa9c1202..f91e7178 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -76,6 +76,8 @@ and t_arg = type tag = | Emp_local | Emp_global + | Emp_intro + | Emp_set | External of string option | Default | Constructor @@ -314,6 +316,8 @@ and o_to_string o = let tag_to_string = function | Emp_local -> "Emp_local" | Emp_global -> "Emp_global" + | Emp_intro -> "Emp_intro" + | Emp_set -> "Emp_set" | External None -> "External" | External (Some s) -> "External " ^ s | Default -> "Default" @@ -321,7 +325,7 @@ let tag_to_string = function | Enum _ -> "Enum" | Alias -> "Alias" | Spec -> "Spec" - + let enforce_to_string = function | Require -> "require" | Guarantee -> "guarantee" @@ -448,6 +452,13 @@ let rec pow_i i n = | n -> mult_int_big_int i (pow_i i (n-1)) let two_pow = pow_i 2 +let is_bit_vector t = match t.t with + | Tapp("vector", [_;_;_; TA_typ t]) | Tabbrev(_,{t=Tapp("vector",[_;_;_; TA_typ t])}) -> + (match t.t with + | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> true + | _ -> false) + | _ -> false + (* predicate to determine if pushing a constant in for addition or multiplication could change the form *) let rec contains_const n = match n.nexp with @@ -3487,10 +3498,12 @@ let tannot_merge co denv widen t_older t_newer = Base(([],t),tag_n,cs_o,ef_o,bounds_o) | _ -> t_newer) | Emp_local, Emp_local -> - (*let _ = Printf.eprintf "local-local case\n" in*) - (*TODO Check conforms to first; if true check consistent, if false replace with t_newer *) + (*let _ = Printf.eprintf "local-local case\n" in*) + if conforms_to_t denv true false t_n t_o + then let t,cs_b = type_consistent co denv Guarantee widen t_n t_o in (*let _ = Printf.eprintf "types consistent\n" in*) Base(([],t),Emp_local,cs_o@cs_n@cs_b,union_effects ef_o ef_n, merge_bounds bounds_o bounds_n) + else Base(([],t_n),Emp_local,cs_n,ef_n,bounds_n) | _,_ -> t_newer) | _ -> t_newer diff --git a/src/type_internal.mli b/src/type_internal.mli index 78ca63e7..93bb1f7c 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -78,6 +78,8 @@ type nexp_map = nexp Nexpmap.t type tag = | Emp_local (* Standard value, variable, expression *) | Emp_global (* Variable from global instead of local scope *) + | Emp_intro (* Local mutable variable, and this is its introduction *) + | Emp_set (* Local mutable expression being set *) | External of string option (* External function or register name *) | Default (* Variable has default type, has not been bound *) | Constructor (* Variable is a data constructor *) @@ -220,6 +222,7 @@ val type_param_consistent : Parse_ast.l -> t_arg emap -> t_arg emap -> nexp_rang val get_abbrev : def_envs -> t -> (t * nexp_range list) val is_enum_typ : def_envs -> t -> int option +val is_bit_vector : t -> bool val extract_bounds : def_envs -> string -> t -> bounds_env val merge_bounds : bounds_env -> bounds_env -> bounds_env |