summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorKathy Gray2014-04-28 13:38:20 +0100
committerKathy Gray2014-04-28 13:38:20 +0100
commit58941d81218adf425255a6369358b8b21f4344d3 (patch)
treed9aadf1894b9bf4dc5a2c55c6fc6b3a12e63f3f2 /src
parent11a52d9ec6f4c2eae49bb07d08603df5f86c1162 (diff)
Add support for overloading for better constraints, and for reducing the number of coercions
Diffstat (limited to 'src')
-rw-r--r--src/initial_check.ml40
-rw-r--r--src/pretty_print.ml16
-rw-r--r--src/type_check.ml330
-rw-r--r--src/type_internal.ml250
-rw-r--r--src/type_internal.mli9
5 files changed, 382 insertions, 263 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 9f1d46d2..2548bf19 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -313,14 +313,14 @@ let rec to_ast_pat (k_env : kind Envmap.t) (Parse_ast.P_aux(pat,l) : Parse_ast.p
then P_id (to_ast_id id)
else P_app(to_ast_id id, List.map (to_ast_pat k_env) pats)
| Parse_ast.P_record(fpats,_) -> P_record(List.map
- (fun (Parse_ast.FP_aux(Parse_ast.FP_Fpat(id,fp),l)) -> FP_aux(FP_Fpat(to_ast_id id, to_ast_pat k_env fp),(l,None)))
+ (fun (Parse_ast.FP_aux(Parse_ast.FP_Fpat(id,fp),l)) -> FP_aux(FP_Fpat(to_ast_id id, to_ast_pat k_env fp),(l,NoTyp)))
fpats, false)
| Parse_ast.P_vector(pats) -> P_vector(List.map (to_ast_pat k_env) pats)
| Parse_ast.P_vector_indexed(ipats) -> P_vector_indexed(List.map (fun (i,pat) -> i,to_ast_pat k_env pat) ipats)
| Parse_ast.P_vector_concat(pats) -> P_vector_concat(List.map (to_ast_pat k_env) pats)
| Parse_ast.P_tup(pats) -> P_tup(List.map (to_ast_pat k_env) pats)
| Parse_ast.P_list(pats) -> P_list(List.map (to_ast_pat k_env) pats)
- ), (l,None))
+ ), (l,NoTyp))
let rec to_ast_letbind (k_env : kind Envmap.t) (Parse_ast.LB_aux(lb,l) : Parse_ast.letbind) : tannot letbind =
@@ -331,7 +331,7 @@ let rec to_ast_letbind (k_env : kind Envmap.t) (Parse_ast.LB_aux(lb,l) : Parse_a
LB_val_explicit(typsch,to_ast_pat k_env pat, to_ast_exp k_env exp)
| Parse_ast.LB_val_implicit(pat,exp) ->
LB_val_implicit(to_ast_pat k_env pat, to_ast_exp k_env exp)
- ), (l,None))
+ ), (l,NoTyp))
and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot exp =
E_aux(
@@ -370,7 +370,7 @@ and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
| Parse_ast.E_case(exp,pexps) -> E_case(to_ast_exp k_env exp, List.map (to_ast_case k_env) pexps)
| Parse_ast.E_let(leb,exp) -> E_let(to_ast_letbind k_env leb, to_ast_exp k_env exp)
| Parse_ast.E_assign(lexp,exp) -> E_assign(to_ast_lexp k_env lexp, to_ast_exp k_env exp)
- ), (l,None))
+ ), (l,NoTyp))
and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot lexp =
LEXP_aux(
@@ -390,15 +390,15 @@ and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
| Parse_ast.E_vector_subrange(vexp,exp1,exp2) -> LEXP_vector_range(to_ast_lexp k_env vexp, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
| Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env fexp, to_ast_id id)
| _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None)
- , (l,None))
+ , (l,NoTyp))
and to_ast_case (k_env : kind Envmap.t) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : tannot pexp =
match pex with
- | Parse_ast.Pat_exp(pat,exp) -> Pat_aux(Pat_exp(to_ast_pat k_env pat, to_ast_exp k_env exp),(l,None))
+ | Parse_ast.Pat_exp(pat,exp) -> Pat_aux(Pat_exp(to_ast_pat k_env pat, to_ast_exp k_env exp),(l,NoTyp))
and to_ast_fexps (fail_on_error : bool) (k_env : kind Envmap.t) (exps : Parse_ast.exp list) : tannot fexps option =
match exps with
- | [] -> Some(FES_aux(FES_Fexps([],false), (Parse_ast.Unknown,None)))
+ | [] -> Some(FES_aux(FES_Fexps([],false), (Parse_ast.Unknown,NoTyp)))
| fexp::exps -> let maybe_fexp,maybe_error = to_ast_record_try k_env fexp in
(match maybe_fexp,maybe_error with
| Some(fexp),None ->
@@ -416,7 +416,7 @@ and to_ast_record_try (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_as
| Parse_ast.E_app_infix(left,op,r) ->
(match left, op with
| Parse_ast.E_aux(Parse_ast.E_id(id),li), Parse_ast.Id_aux(Parse_ast.Id("="),leq) ->
- Some(FE_aux(FE_Fexp(to_ast_id id, to_ast_exp k_env r), (l,None))),None
+ Some(FE_aux(FE_Fexp(to_ast_id id, to_ast_exp k_env r), (l,NoTyp))),None
| Parse_ast.E_aux(_,li) , Parse_ast.Id_aux(Parse_ast.Id("="),leq) ->
None,Some(li,"Expected an identifier to begin this field assignment")
| Parse_ast.E_aux(Parse_ast.E_id(id),li), Parse_ast.Id_aux(_,leq) ->
@@ -446,13 +446,13 @@ let to_ast_spec (names,k_env,t_env) (val_:Parse_ast.val_spec) : (tannot val_spec
(match vs with
| Parse_ast.VS_val_spec(ts,id) ->
let typsch,_,_ = to_ast_typschm k_env ts in
- VS_aux(VS_val_spec(typsch,to_ast_id id),(l,None)),(names,k_env,t_env)
+ VS_aux(VS_val_spec(typsch,to_ast_id id),(l,NoTyp)),(names,k_env,t_env)
| Parse_ast.VS_extern_spec(ts,id,s) ->
let typsch,_,_ = to_ast_typschm k_env ts in
- VS_aux(VS_extern_spec(typsch,to_ast_id id,s),(l,None)),(names,k_env,t_env)
+ VS_aux(VS_extern_spec(typsch,to_ast_id id,s),(l,NoTyp)),(names,k_env,t_env)
| Parse_ast.VS_extern_no_rename(ts,id) ->
let typsch,_,_ = to_ast_typschm k_env ts in
- VS_aux(VS_extern_no_rename(typsch,to_ast_id id),(l,None)),(names,k_env,t_env))(*Do names and t_env need updating this pass? *)
+ VS_aux(VS_extern_no_rename(typsch,to_ast_id id),(l,NoTyp)),(names,k_env,t_env))(*Do names and t_env need updating this pass? *)
let to_ast_namescm (Parse_ast.Name_sect_aux(ns,l)) =
@@ -483,7 +483,7 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de
let id = to_ast_id id in
let key = id_to_string id in
let typschm,k_env,_ = to_ast_typschm k_env typschm in
- let td_abrv = TD_aux(TD_abbrev(id,to_ast_namescm name_scm_opt,typschm),(l,None)) in
+ let td_abrv = TD_aux(TD_abbrev(id,to_ast_namescm name_scm_opt,typschm),(l,NoTyp)) in
let typ = (match typschm with
| TypSchm_aux(TypSchm_ts(tq,typ), _) ->
begin match (typquant_to_quantkinds k_env tq) with
@@ -496,7 +496,7 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de
let key = id_to_string id in
let typq,k_env,_ = to_ast_typquant k_env typq in
let fields = List.map (fun (atyp,id) -> (to_ast_typ k_env atyp),(to_ast_id id)) fields in (* Add check that all arms have unique names locally *)
- let td_rec = TD_aux(TD_record(id,to_ast_namescm name_scm_opt,typq,fields,false),(l,None)) in
+ let td_rec = TD_aux(TD_record(id,to_ast_namescm name_scm_opt,typq,fields,false),(l,NoTyp)) in
let typ = (match (typquant_to_quantkinds k_env typq) with
| [ ] -> {k = K_Typ}
| typs -> {k = K_Lam(typs,{k=K_Typ})}) in
@@ -506,7 +506,7 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de
let key = id_to_string id in
let typq,k_env,_ = to_ast_typquant k_env typq in
let arms = List.map (to_ast_type_union k_env) arms in (* Add check that all arms have unique names *)
- let td_var = TD_aux(TD_variant(id,to_ast_namescm name_scm_opt,typq,arms,false),(l,None)) in
+ let td_var = TD_aux(TD_variant(id,to_ast_namescm name_scm_opt,typq,arms,false),(l,NoTyp)) in
let typ = (match (typquant_to_quantkinds k_env typq) with
| [ ] -> {k = K_Typ}
| typs -> {k = K_Lam(typs,{k=K_Typ})}) in
@@ -516,7 +516,7 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de
let key = id_to_string id in
let enums = List.map to_ast_id enums in
let keys = List.map id_to_string enums in
- let td_enum = TD_aux(TD_enum(id,to_ast_namescm name_scm_opt,enums,false),(l,None)) in (* Add check that all enums have unique names *)
+ let td_enum = TD_aux(TD_enum(id,to_ast_namescm name_scm_opt,enums,false),(l,NoTyp)) in (* Add check that all enums have unique names *)
let k_env = List.fold_right (fun k k_env -> Envmap.insert k_env (k,{k=K_Nat})) keys (Envmap.insert k_env (key,{k=K_Typ})) in
td_enum, (names,k_env,t_env)
| Parse_ast.TD_register(id,t1,t2,ranges) ->
@@ -525,7 +525,7 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de
let n1 = to_ast_nexp k_env t1 in
let n2 = to_ast_nexp k_env t2 in
let ranges = List.map (fun (range,id) -> (to_ast_range range),to_ast_id id) ranges in
- TD_aux(TD_register(id,n1,n2,ranges),(l,None)), (names,Envmap.insert k_env (key, {k=K_Typ}),t_env))
+ TD_aux(TD_register(id,n1,n2,ranges),(l,NoTyp)), (names,Envmap.insert k_env (key, {k=K_Typ}),t_env))
let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt =
Rec_aux((match r with
@@ -553,7 +553,7 @@ let to_ast_fundef (names,k_env,t_env) (Parse_ast.FD_aux(fd,l):Parse_ast.fundef)
match fd with
| Parse_ast.FD_function(rec_opt,tannot_opt,effects_opt,funcls) ->
let tannot_opt, k_env,_ = to_ast_tannot_opt k_env tannot_opt in
- FD_aux(FD_function(to_ast_rec rec_opt, tannot_opt, to_ast_effects_opt k_env effects_opt, List.map (to_ast_funcl (names, k_env, t_env)) funcls), (l,None)), (names,k_env,t_env)
+ FD_aux(FD_function(to_ast_rec rec_opt, tannot_opt, to_ast_effects_opt k_env effects_opt, List.map (to_ast_funcl (names, k_env, t_env)) funcls), (l,NoTyp)), (names,k_env,t_env)
type def_progress =
No_def
@@ -573,7 +573,7 @@ let rec def_in_progress (id : id) (partial_defs : (id * partial_def) list) : par
let to_ast_dec (names,k_env,t_env) (Parse_ast.DEC_aux(Parse_ast.DEC_reg(typ,id),l)) =
let t = to_ast_typ k_env typ in
let id = to_ast_id id in
- (DEC_aux(DEC_reg(t,id),(l,None)))
+ (DEC_aux(DEC_reg(t,id),(l,NoTyp)))
let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out * (id * partial_def) list =
let envs = (names,k_env,t_env) in
@@ -604,7 +604,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
let effects_opt = to_ast_effects_opt k_env' effects_opt in
let id = to_ast_id id in
(match (def_in_progress id partial_defs) with
- | None -> let partial_def = ref ((DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,None)))),false) in
+ | None -> let partial_def = ref ((DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,NoTyp)))),false) in
(No_def,envs),((id,(partial_def,k_local))::partial_defs)
| Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None)
| Parse_ast.SD_scattered_funcl(funcl) ->
@@ -626,7 +626,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
let name = to_ast_namescm naming_scheme_opt in
let typq, k_env',_ = to_ast_typquant k_env typquant in
(match (def_in_progress id partial_defs) with
- | None -> let partial_def = ref ((DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,None)))),false) in
+ | None -> let partial_def = ref ((DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,NoTyp)))),false) in
(Def_place_holder(id,l),(names,Envmap.insert k_env ((id_to_string id),{k=K_Typ}),t_env)),(id,(partial_def,k_env'))::partial_defs
| Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None)
| Parse_ast.SD_scattered_unioncl(id,tu) ->
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index f0dea03f..ecafc5f2 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -219,10 +219,10 @@ and pp_exp ppf (E_aux(e,(_,annot))) =
| E_id(id) -> pp_id ppf id
| E_lit(lit) -> pp_lit ppf lit
| E_cast(typ,exp) -> fprintf ppf "@[<0>%a%a%a %a@]" kwd "(" pp_typ typ kwd ")" pp_exp exp
- | E_internal_cast((_,None),e) -> pp_exp ppf e
- | E_internal_cast((_,Some((_,t),_,_,_)), (E_aux(_,(_,eannot)) as exp)) ->
+ | E_internal_cast((_,NoTyp),e) -> pp_exp ppf e
+ | E_internal_cast((_,Base((_,t),_,_,_)), (E_aux(_,(_,eannot)) as exp)) ->
(match t.t,eannot with
- | Tapp("vector",[TA_nexp n1;_;_;_]),Some((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_) ->
+ | Tapp("vector",[TA_nexp n1;_;_;_]),Base((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_) ->
if nexp_eq n1 n2
then pp_exp ppf exp
else
@@ -600,8 +600,8 @@ let pp_format_nes nes =
nes) ^*) "]"
let pp_format_annot = function
- | None -> "Nothing"
- | Some((_,t),tag,nes,efct) ->
+ | NoTyp -> "Nothing"
+ | Base((_,t),tag,nes,efct) ->
"(Just (" ^ pp_format_t t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ pp_format_e efct ^ "))"
let pp_annot ppf ant = base ppf (pp_format_annot ant)
@@ -650,10 +650,10 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
| E_id(id) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_id" pp_lem_id id pp_lem_l l pp_annot annot
| E_lit(lit) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_lit" pp_lem_lit lit pp_lem_l l pp_annot annot
| E_cast(typ,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp pp_lem_l l pp_annot annot
- | E_internal_cast((_,None),e) -> pp_lem_exp ppf e
- | E_internal_cast((_,Some((_,t),_,_,_)), (E_aux(ec,(_,eannot)) as exp)) ->
+ | E_internal_cast((_,NoTyp),e) -> pp_lem_exp ppf e
+ | E_internal_cast((_,Base((_,t),_,_,_)), (E_aux(ec,(_,eannot)) as exp)) ->
(match t.t,eannot with
- | Tapp("vector",[TA_nexp n1;_;_;_]),Some((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_) ->
+ | Tapp("vector",[TA_nexp n1;_;_;_]),Base((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_) ->
if nexp_eq n1 n2
then pp_lem_exp ppf exp
else fprintf ppf "@[<0>(E_aux (E_cast %a %a) (%a, %a))@]" pp_lem_typ (t_to_typ t) pp_lem_exp exp pp_lem_l l pp_annot annot
diff --git a/src/type_check.ml b/src/type_check.ml
index f8a5cb52..7f0efc35 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -143,17 +143,17 @@ let typschm_to_tannot envs ((TypSchm_aux(typschm,l)):typschm) (tag : tag) : tann
| TypSchm_ts(tq,typ) ->
let t = typ_to_t typ in
let (ids,constraints) = typq_to_params envs tq in
- Some((ids,t),tag,constraints,pure_e)
+ Base((ids,t),tag,constraints,pure_e)
let into_register d_env (t : tannot) : tannot =
match t with
- | Some((ids,ty),tag,constraints,eft) ->
+ | Base((ids,ty),tag,constraints,eft) ->
let ty',_ = get_abbrev d_env ty in
(match ty'.t with
| Tapp("register",_)-> t
- | Tabbrev(ti,{t=Tapp("register",_)}) -> Some((ids,ty'),tag,constraints,eft)
- | _ -> Some((ids, {t= Tapp("register",[TA_typ ty'])}),tag,constraints,eft))
- | None -> None
+ | Tabbrev(ti,{t=Tapp("register",_)}) -> Base((ids,ty'),tag,constraints,eft)
+ | _ -> Base((ids, {t= Tapp("register",[TA_typ ty'])}),tag,constraints,eft))
+ | t -> t
let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap) * nexp_range list * t) =
let (Env(d_env,t_env)) = envs in
@@ -186,57 +186,57 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
| L_string s -> {t = Tid "string"},lit
| L_undef -> typ_error l' "Cannot pattern match on undefined") in
let t',cs' = type_consistent (Patt l) d_env t expect_t in
- (P_aux(P_lit(L_aux(lit,l')),(l,Some(([],t),Emp_local,cs@cs',pure_e))),Envmap.empty,cs@cs',t)
+ (P_aux(P_lit(L_aux(lit,l')),(l,Base(([],t),Emp_local,cs@cs',pure_e))),Envmap.empty,cs@cs',t)
| P_wild ->
- (P_aux(p,(l,Some(([],expect_t),Emp_local,cs,pure_e))),Envmap.empty,cs,expect_t)
+ (P_aux(p,(l,Base(([],expect_t),Emp_local,cs,pure_e))),Envmap.empty,cs,expect_t)
| P_as(pat,id) ->
let (pat',env,constraints,t) = check_pattern envs emp_tag expect_t pat in
- let tannot = Some(([],t),emp_tag,cs,pure_e) in
+ let tannot = Base(([],t),emp_tag,cs,pure_e) in
(P_aux(P_as(pat',id),(l,tannot)),Envmap.insert env (id_to_string id,tannot),cs@constraints,t)
| P_typ(typ,pat) ->
let t = typ_to_t typ in
let (pat',env,constraints,u) = check_pattern envs emp_tag t pat in
- (P_aux(P_typ(typ,pat'),(l,Some(([],t),Emp_local,[],pure_e))),env,cs@constraints,t)
+ (P_aux(P_typ(typ,pat'),(l,Base(([],t),Emp_local,[],pure_e))),env,cs@constraints,t)
| P_id id ->
- let tannot = Some(([],expect_t),emp_tag,cs,pure_e) in
+ let tannot = Base(([],expect_t),emp_tag,cs,pure_e) in
(P_aux(p,(l,tannot)),Envmap.from_list [(id_to_string id,tannot)],cs,expect_t)
| P_app(id,pats) ->
let i = id_to_string id in
(match Envmap.apply t_env i with
- | None | Some None -> typ_error l ("Constructor " ^ i ^ " in pattern is undefined")
- | Some(Some((params,t),Constructor,constraints,eft)) ->
+ | None | Some NoTyp | Some Overload _ -> typ_error l ("Constructor " ^ i ^ " in pattern is undefined")
+ | Some(Base((params,t),Constructor,constraints,eft)) ->
let t,constraints,_ = subst params t constraints eft in
(match t.t with
| Tid id -> if pats = [] then
let t',constraints' = type_consistent (Patt l) d_env t expect_t in
- (P_aux(p,(l,Some(([],t'),Constructor,constraints,pure_e))),Envmap.empty,constraints@constraints',t')
+ (P_aux(p,(l,Base(([],t'),Constructor,constraints,pure_e))),Envmap.empty,constraints@constraints',t')
else typ_error l ("Constructor " ^ i ^ " does not expect arguments")
| Tfn(t1,t2,ef) ->
(match pats with
| [] -> let _ = type_consistent (Patt l) d_env unit_t t1 in
let t',constraints' = type_consistent (Patt l) d_env t2 expect_t in
- (P_aux(P_app(id,[]),(l,Some(([],t'),Constructor,constraints,pure_e))),Envmap.empty,constraints@constraints',t')
+ (P_aux(P_app(id,[]),(l,Base(([],t'),Constructor,constraints,pure_e))),Envmap.empty,constraints@constraints',t')
| [p] -> let (p',env,constraints,u) = check_pattern envs emp_tag t1 p in
let t',constraints' = type_consistent (Patt l) d_env t2 expect_t in
- (P_aux(P_app(id,[p']),(l,Some(([],t'),Constructor,constraints,pure_e))),env,constraints@constraints',t')
+ (P_aux(P_app(id,[p']),(l,Base(([],t'),Constructor,constraints,pure_e))),env,constraints@constraints',t')
| pats -> let (pats',env,constraints,u) =
match check_pattern envs emp_tag t1 (P_aux(P_tup(pats),(l,annot))) with
| ((P_aux(P_tup(pats'),_)),env,constraints,u) -> pats',env,constraints,u
| _ -> assert false in
let t',constraints' = type_consistent (Patt l) d_env t2 expect_t in
- (P_aux(P_app(id,pats'),(l,Some(([],t'),Constructor,constraints,pure_e))),env,constraints@constraints',t'))
+ (P_aux(P_app(id,pats'),(l,Base(([],t'),Constructor,constraints,pure_e))),env,constraints@constraints',t'))
| _ -> typ_error l ("Identifier " ^ i ^ " is not bound to a constructor"))
- | Some(Some((params,t),tag,constraints,eft)) -> typ_error l ("Identifier " ^ i ^ " used in pattern is not a constructor"))
+ | Some(Base((params,t),tag,constraints,eft)) -> typ_error l ("Identifier " ^ i ^ " used in pattern is not a constructor"))
| P_record(fpats,_) ->
(match (fields_to_rec fpats d_env.rec_env) with
| None -> typ_error l ("No struct exists with the listed fields")
| Some(id,typ_pats) ->
let pat_checks =
List.map (fun (tan,id,l,pat) ->
- let (Some((vs,t),tag,cs,eft)) = tan in
+ let (Base((vs,t),tag,cs,eft)) = tan in
let t,cs,_ = subst vs t cs eft in
let (pat,env,constraints,u) = check_pattern envs emp_tag t pat in
- let pat = FP_aux(FP_Fpat(id,pat),(l,Some(([],t),tag,cs,pure_e))) in
+ let pat = FP_aux(FP_Fpat(id,pat),(l,Base(([],t),tag,cs,pure_e))) in
(pat,env,cs@constraints)) typ_pats in
let pats' = List.map (fun (a,b,c) -> a) pat_checks in
(*Need to check for variable duplication here*)
@@ -244,7 +244,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
let constraints = List.fold_right (fun (_,_,cs) cons -> cs@cons) pat_checks [] in
let t = {t=Tid id} in
let t',cs' = type_consistent (Patt l) d_env t expect_t in
- (P_aux((P_record(pats',false)),(l,Some(([],t'),Emp_local,constraints@cs',pure_e))),env,constraints@cs',t'))
+ (P_aux((P_record(pats',false)),(l,Base(([],t'),Emp_local,constraints@cs',pure_e))),env,constraints@cs',t'))
| P_vector pats ->
let item_t = match expect_actual.t with
| Tapp("vector",[b;r;o;TA_typ i]) -> i
@@ -259,7 +259,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
let env = List.fold_right (fun e env -> Envmap.union e env) t_envs Envmap.empty in (*Need to check for non-duplication of variables*)
let (u,cs) = List.fold_right (fun u (t,cs) -> let t',cs = type_consistent (Patt l) d_env u t in t',cs) ts (item_t,[]) in
let t = {t = Tapp("vector",[(TA_nexp {nexp= Nconst 0});(TA_nexp {nexp= Nconst (List.length ts)});(TA_ord{order=Oinc});(TA_typ u)])} in
- (P_aux(P_vector(pats'),(l,Some(([],t),Emp_local,cs,pure_e))), env,cs@constraints,t)
+ (P_aux(P_vector(pats'),(l,Base(([],t),Emp_local,cs,pure_e))), env,cs@constraints,t)
| P_vector_indexed(ipats) ->
let item_t = match expect_actual.t with
| Tapp("vector",[b;r;o;TA_typ i]) -> i
@@ -296,7 +296,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
GtEq(co,rise, {nexp = Nconst (lst-fst)});]@cs
else [GtEq(co,base, {nexp = Nconst fst});
LtEq(co,rise, { nexp = Nconst (fst -lst)});]@cs in
- (P_aux(P_vector_indexed(pats'),(l,Some(([],t),Emp_local,cs,pure_e))), env,constraints@cs,t)
+ (P_aux(P_vector_indexed(pats'),(l,Base(([],t),Emp_local,cs,pure_e))), env,constraints@cs,t)
| P_tup(pats) ->
let item_ts = match expect_actual.t with
| Ttup ts ->
@@ -313,23 +313,23 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
(List.combine pats item_ts) ([],[],[],[]) in
let env = List.fold_right (fun e env -> Envmap.union e env) t_envs Envmap.empty in (*Need to check for non-duplication of variables*)
let t = {t = Ttup ts} in
- (P_aux(P_tup(pats'),(l,Some(([],t),Emp_local,[],pure_e))), env,constraints,t)
+ (P_aux(P_tup(pats'),(l,Base(([],t),Emp_local,[],pure_e))), env,constraints,t)
| P_vector_concat pats ->
+ let item_t,base,rise,order =
+ match expect_t.t with
+ | Tapp("vector",[TA_nexp(b);TA_nexp(r);TA_ord(o);TA_typ item])
+ | Tabbrev(_,{t=Tapp("vector",[TA_nexp(b);TA_nexp(r);TA_ord(o);TA_typ item])}) -> item,b,r,o
+ | _ -> new_t (),new_n (), new_n (), new_o () in
+ let vec_ti _ = {t= Tapp("vector",[TA_nexp (new_n ());TA_nexp (new_n ());TA_ord order;TA_typ item_t])} in
let (pats',ts,envs,constraints) =
List.fold_right
(fun pat (pats,ts,t_envs,constraints) ->
- let (pat',env,cons,t) = check_pattern envs emp_tag expect_t pat in
+ let (pat',env,cons,t) = check_pattern envs emp_tag (vec_ti ()) pat in
(pat'::pats,t::ts,env::t_envs,cons@constraints))
pats ([],[],[],[]) in
- let env = List.fold_right (fun e env -> Envmap.union e env) envs Envmap.empty in (*Need to check for non-duplication of variables*)
- let t_init = new_t () in
- let or_init = new_o () in
- let ts = List.map
- (fun t->let ti= { t = Tapp("vector",[TA_nexp(new_n ());TA_nexp(new_n ());TA_ord(or_init);TA_typ t_init])} in
- type_consistent (Patt l) d_env t ti) ts in
- let ts,cs = List.split ts in
- let base,rise = new_n (),new_n () in
- let t = {t = Tapp("vector",[(TA_nexp base);(TA_nexp rise);(TA_ord or_init);(TA_typ t_init)])} in
+ let env =
+ List.fold_right (fun e env -> Envmap.union e env) envs Envmap.empty in (*Need to check for non-duplication of variables*)
+ let t = {t = Tapp("vector",[(TA_nexp base);(TA_nexp rise);(TA_ord order);(TA_typ item_t)])} in
let base_c,r1 = match (List.hd ts).t with
| Tapp("vector",[(TA_nexp b);(TA_nexp r);(TA_ord o);(TA_typ u)]) -> b,r
| _ -> raise (Reporting_basic.err_unreachable l "vector concat pattern impossibility") in
@@ -338,8 +338,8 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
match t.t with
| Tapp("vector",[(TA_nexp b);(TA_nexp r);(TA_ord o);(TA_typ u)]) -> {nexp = Nadd(r,rn)}
| _ -> raise (Reporting_basic.err_unreachable l "vector concat pattern impossibility") ) (List.tl ts) r1 in
- let cs = [Eq((Patt l),base,base_c);Eq((Patt l),rise,range_c)]@(List.flatten cs) in
- (P_aux(P_vector_concat(pats'),(l,Some(([],t),Emp_local,cs,pure_e))), env,constraints@cs,t)
+ let cs = [Eq((Patt l),base,base_c);Eq((Patt l),rise,range_c)]@cs in
+ (P_aux(P_vector_concat(pats'),(l,Base(([],t),Emp_local,cs,pure_e))), env,constraints@cs,t)
| P_list(pats) ->
let item_t = match expect_actual.t with
| Tapp("list",[TA_typ i]) -> i
@@ -354,7 +354,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
let env = List.fold_right (fun e env -> Envmap.union e env) envs Envmap.empty in (*Need to check for non-duplication of variables*)
let u,cs = List.fold_right (fun u (t,cs) -> let t',cs' = type_consistent (Patt l) d_env u t in t',cs@cs') ts (item_t,[]) in
let t = {t = Tapp("list",[TA_typ u])} in
- (P_aux(P_list(pats'),(l,Some(([],t),Emp_local,cs,pure_e))), env,constraints@cs,t)
+ (P_aux(P_list(pats'),(l,Base(([],t),Emp_local,cs,pure_e))), env,constraints@cs,t)
let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp * t * tannot emap * nexp_range list * effect) =
let Env(d_env,t_env) = envs in
@@ -366,22 +366,22 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| E_id(id) ->
let i = id_to_string id in
(match Envmap.apply t_env i with
- | Some(Some((params,t),Constructor,cs,ef)) ->
+ | Some(Base((params,t),Constructor,cs,ef)) ->
let t,cs,ef = subst params t cs ef in
(match t.t with
| Tfn({t = Tid "unit"},t',ef) ->
- let t',cs',e' = type_coerce (Expr l) d_env t' (rebuild (Some(([],{t=Tfn(unit_t,t',ef)}),Constructor,cs,ef))) expect_t in
+ let t',cs',e' = type_coerce (Expr l) d_env t' (rebuild (Base(([],{t=Tfn(unit_t,t',ef)}),Constructor,cs,ef))) expect_t in
(e',t',t_env,cs@cs',ef)
| Tfn(t1,t',e) ->
typ_error l ("Constructor " ^ i ^ " expects arguments of type " ^ (t_to_string t) ^ ", found none")
| _ -> raise (Reporting_basic.err_unreachable l "Constructor tannot does not have function type"))
- | Some(Some((params,t),Enum,cs,ef)) ->
+ | Some(Base((params,t),Enum,cs,ef)) ->
let t',cs,_ = subst params t cs ef in
- let t',cs',e' = type_coerce (Expr l) d_env t' (rebuild (Some(([],t'),Enum,cs,pure_e))) expect_t in
+ let t',cs',e' = type_coerce (Expr l) d_env t' (rebuild (Base(([],t'),Enum,cs,pure_e))) expect_t in
(e',t',t_env,cs@cs',pure_e)
- | Some(Some(tp,Default,cs,ef)) | Some(Some(tp,Spec,cs,ef)) ->
+ | Some(Base(tp,Default,cs,ef)) | Some(Base(tp,Spec,cs,ef)) ->
typ_error l ("Identifier " ^ i ^ " must be defined, not just specified, before use")
- | Some(Some((params,t),tag,cs,ef)) ->
+ | Some(Base((params,t),tag,cs,ef)) ->
let t,cs,ef = match tag with | Emp_global | External _ -> subst params t cs ef | _ -> t,cs,ef in
let t,cs' = get_abbrev d_env t in
let cs = cs@cs' in
@@ -393,28 +393,28 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
(match t_actual.t,expect_actual.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),Emp_local,cs,ef) in
+ let tannot = Base(([],t),Emp_local,cs,ef) in
let t',cs',e' = type_coerce (Expr l) d_env t' (rebuild tannot) expect_t' in
(e',t,t_env,cs@cs',ef)
| Tapp("register",[TA_typ(t')]),Tuvar _ ->
let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
- let tannot = Some(([],t),External (Some i),cs,ef') in
+ let tannot = Base(([],t),External (Some i),cs,ef') in
let t',cs',e' = type_coerce (Expr l) d_env t' (rebuild tannot) expect_actual 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 (Some i),cs,ef') in
+ let tannot = Base(([],t),External (Some i),cs,ef') in
let t',cs',e' = type_coerce (Expr l) d_env t' (rebuild tannot) expect_actual in
(e',t',t_env,cs@cs',ef)
| Tapp("reg",[TA_typ(t')]),_ ->
- let tannot = Some(([],t),Emp_local,cs,pure_e) in
+ let tannot = Base(([],t),Emp_local,cs,pure_e) in
let t',cs',e' = type_coerce (Expr l) d_env t' (rebuild tannot) expect_actual in
(e',t',t_env,cs@cs',pure_e)
| _ ->
- let t',cs',e' = type_coerce (Expr l) d_env t (rebuild (Some(([],t),tag,cs,pure_e))) expect_t in
+ let t',cs',e' = type_coerce (Expr l) d_env t (rebuild (Base(([],t),tag,cs,pure_e))) expect_t in
(e',t,t_env,cs@cs',pure_e)
)
- | Some None | None -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is unbound"))
+ | Some NoTyp | Some Overload _ | None -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is unbound"))
| E_lit (L_aux(lit,l')) ->
let t,lit',effect = (match lit with
| L_unit -> unit_t,lit,pure_e
@@ -453,7 +453,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| L_string s -> {t = Tid "string"},lit,pure_e
| L_undef -> new_t (),lit,{effect=Eset[BE_aux(BE_undef,l)]}) in
let t',cs',e' =
- type_coerce (Expr l) d_env t (E_aux(E_lit(L_aux(lit',l')),(l,(Some(([],t),Emp_local,[],effect))))) expect_t in
+ type_coerce (Expr l) d_env t (E_aux(E_lit(L_aux(lit',l')),(l,(Base(([],t),Emp_local,[],effect))))) expect_t in
(e',t',t_env,cs',effect)
| E_cast(typ,e) ->
let t = typ_to_t typ in
@@ -464,42 +464,76 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| E_app(id,parms) ->
let i = id_to_string id in
(match Envmap.apply t_env i with
- | Some(Some(tp,Enum,cs,ef)) ->
+ | Some(Base(tp,Enum,cs,ef)) ->
typ_error l ("Expected function with name " ^ i ^ " but found an enumeration identifier")
- | Some(Some(tp,Default,cs,ef)) ->
+ | Some(Base(tp,Default,cs,ef)) ->
typ_error l ("Function " ^ i ^ " must be defined, not just declared as a default, before use")
- | Some(Some((params,t),tag,cs,ef)) ->
+ | Some(Base((params,t),tag,cs,ef)) ->
let t,cs,ef = subst params t cs ef in
(match t.t with
| Tfn(arg,ret,ef') ->
(match parms with
| [] ->
let (p',cs') = type_consistent (Expr l) d_env unit_t arg in
- let (ret_t,cs_r,e') = type_coerce (Expr l) d_env ret (rebuild (Some(([],ret),tag,cs@cs',ef))) expect_t in
+ let (ret_t,cs_r,e') = type_coerce (Expr l) d_env ret (rebuild (Base(([],ret),tag,cs@cs',ef))) expect_t in
(e',ret_t,t_env,cs@cs'@cs_r,ef)
| [parm] ->
let (parm',arg_t,t_env,cs',ef_p) = check_exp envs arg parm in
- let (ret_t,cs_r',e') = type_coerce (Expr l) d_env ret (E_aux(E_app(id,[parm']),(l,(Some(([],ret),tag,cs,ef'))))) expect_t in
+ let (ret_t,cs_r',e') = type_coerce (Expr l) d_env ret (E_aux(E_app(id,[parm']),(l,(Base(([],ret),tag,cs,ef'))))) expect_t in
(e',ret_t,t_env,cs@cs'@cs_r',union_effects ef_p ef')
| parms ->
- let ((E_aux(E_tuple parms',tannot')),arg_t,t_env,cs',ef_p) = check_exp envs arg (E_aux(E_tuple parms,(l,None))) in
- let (ret_t,cs_r',e') = type_coerce (Expr l) d_env ret (E_aux(E_app(id, parms'),(l,(Some(([],ret),tag,cs,ef'))))) expect_t in
+ let ((E_aux(E_tuple parms',tannot')),arg_t,t_env,cs',ef_p) = check_exp envs arg (E_aux(E_tuple parms,(l,NoTyp))) in
+ let (ret_t,cs_r',e') = type_coerce (Expr l) d_env ret (E_aux(E_app(id, parms'),(l,(Base(([],ret),tag,cs,ef'))))) expect_t in
(e',ret_t,t_env,cs@cs'@cs_r',union_effects ef_p ef'))
| _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
+ | Some(Overload(Base((params,t),tag,cs,ef),variants)) ->
+ let t_p,cs_p,ef_p = subst params t cs ef in
+ let args,arg_t,arg_cs,arg_ef =
+ (match t.t with
+ | Tfn(arg,ret,ef') ->
+ (match parms with
+ | [] ->
+ let (p',cs') = type_consistent (Expr l) d_env unit_t arg in
+ ([E_aux(E_lit(L_aux(L_unit, l)), (l,Base(([],unit_t),Emp_local,cs',pure_e)))],p',cs',pure_e)
+ | [parm] ->
+ let (parm', arg_t,_,cs',ef_p) = check_exp envs arg parm in
+ [parm'],arg_t,cs',ef_p
+ | parms ->
+ let ((E_aux(E_tuple parms',tannot')),arg_t,_,cs',ef_p) = check_exp envs arg (E_aux(E_tuple parms,(l,NoTyp))) in
+ (parms',arg_t,cs',ef_p))
+ | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in
+ (match (select_overload_variant d_env variants arg_t) with
+ | NoTyp -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t))
+ | Base((params,t),tag,cs,ef) ->
+ (match t.t with
+ | Tfn(arg,ret,ef') ->
+ let args',arg_cs' =
+ (match args with
+ | [parm] ->
+ let _,cs,parm' = type_coerce (Expr l) d_env arg_t parm arg in
+ [parm'],cs
+ | parms ->
+ let (_,cs,(E_aux(E_tuple parms',tannot'))) =
+ type_coerce (Expr l) d_env arg_t (E_aux(E_tuple parms,(l,NoTyp))) arg in
+ parms',cs) in
+ let (ret_t,cs_r,e') =
+ type_coerce (Expr l) d_env ret (E_aux(E_app(id,args'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in
+ (e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,union_effects ef_p (union_effects arg_ef ef'))
+ | _ -> assert false))
| _ -> typ_error l ("Unbound function " ^ i))
| E_app_infix(lft,op,rht) ->
let i = id_to_string op in
(match Envmap.apply t_env i with
- | Some(Some(tp,Enum,cs,ef)) ->
+ | Some(Base(tp,Enum,cs,ef)) ->
typ_error l ("Expected function with name " ^ i ^ " but found an enumeration identifier")
- | Some(Some(tp,Default,cs,ef)) ->
+ | Some(Base(tp,Default,cs,ef)) ->
typ_error l ("Function " ^ i ^ " must be defined, not just declared as a default, before use")
- | Some(Some((params,t),tag,cs,ef)) ->
+ | Some(Base((params,t),tag,cs,ef)) ->
let t,cs,ef = subst params t cs ef in
(match t.t with
| Tfn(arg,ret,ef) ->
- let (E_aux(E_tuple [lft';rht'],tannot'),arg_t,t_env,cs',ef') = check_exp envs arg (E_aux(E_tuple [lft;rht],(l,None))) in
- let ret_t,cs_r',e' = type_coerce (Expr l) d_env ret (E_aux(E_app_infix(lft',op,rht'),(l,(Some(([],ret),tag,cs,ef))))) expect_t in
+ let (E_aux(E_tuple [lft';rht'],tannot'),arg_t,t_env,cs',ef') = check_exp envs arg (E_aux(E_tuple [lft;rht],(l,NoTyp))) in
+ let ret_t,cs_r',e' = type_coerce (Expr l) d_env ret (E_aux(E_app_infix(lft',op,rht'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in
(e',ret_t,t_env,cs@cs'@cs_r',union_effects ef ef')
| _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
| _ -> typ_error l ("Unbound infix function " ^ i))
@@ -515,7 +549,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
let (e',t',_,c,ef) = check_exp envs t e in ((e'::exps),(t'::typs),c@consts,union_effects ef effect))
exps ts ([],[],[],pure_e) in
let t = {t = Ttup typs} in
- (E_aux(E_tuple(exps),(l,Some(([],t),Emp_local,[],pure_e))),t,t_env,consts,effect)
+ (E_aux(E_tuple(exps),(l,Base(([],t),Emp_local,[],pure_e))),t,t_env,consts,effect)
else typ_error l ("Expected a tuple with length " ^ (string_of_int tl) ^ " found one of length " ^ (string_of_int el))
| _ ->
let exps,typs,consts,effect =
@@ -524,7 +558,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
let (e',t,_,c,ef) = check_exp envs (new_t ()) e in ((e'::exps),(t::typs),c@consts,union_effects ef effect))
exps ([],[],[],pure_e) in
let t = { t=Ttup typs } in
- let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_tuple(exps),(l,Some(([],t),Emp_local,[],pure_e)))) expect_t in
+ let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_tuple(exps),(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
(e',t',t_env,consts@cs',effect))
| E_if(cond,then_,else_) ->
let (cond',_,_,c1,ef1) = check_exp envs bool_t cond in
@@ -532,7 +566,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
let else',else_t,else_env,else_c,else_ef = check_exp envs expect_t else_ in
let t_cs = CondCons((Expr l),c1,then_c) in
let e_cs = CondCons((Expr l),[],else_c) in
- (E_aux(E_if(cond',then',else'),(l,Some(([],expect_t),Emp_local,[],pure_e))),
+ (E_aux(E_if(cond',then',else'),(l,Base(([],expect_t),Emp_local,[],pure_e))),
expect_t,Envmap.intersect_merge (tannot_merge (Expr l) d_env) then_env else_env,[t_cs;e_cs],
union_effects ef1 (union_effects then_ef else_ef))
| E_for(id,from,to_,step,order,block) ->
@@ -545,15 +579,15 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
let new_annot,local_cs =
match (aorder_to_ord order).order with
| Oinc ->
- (Some(([],{t=Tapp("range",[TA_nexp fb;TA_nexp {nexp=Nadd(tb,tr)}])}),Emp_local,[],pure_e),
+ (Base(([],{t=Tapp("range",[TA_nexp fb;TA_nexp {nexp=Nadd(tb,tr)}])}),Emp_local,[],pure_e),
[LtEq((Expr l),{nexp=Nadd(fb,fr)},{nexp=Nadd(tb,tr)});LtEq((Expr l),fb,tb)])
| Odec ->
- (Some(([],{t=Tapp("range",[TA_nexp tb; TA_nexp {nexp=Nadd(fb,fr)}])}),Emp_local,[],pure_e),
+ (Base(([],{t=Tapp("range",[TA_nexp tb; TA_nexp {nexp=Nadd(fb,fr)}])}),Emp_local,[],pure_e),
[GtEq((Expr l),{nexp=Nadd(fb,fr)},{nexp=Nadd(tb,tr)});GtEq((Expr l),fb,tb)])
| _ -> (typ_error l "Order specification in a foreach loop must be either inc or dec, not polymorphic")
in
let (block',b_t,_,b_c,b_ef) = check_exp (Env(d_env,Envmap.insert t_env (id_to_string id,new_annot))) expect_t block in
- (E_aux(E_for(id,from',to_',step',order,block'),(l,Some(([],b_t),Emp_local,local_cs,pure_e))),expect_t,Envmap.empty,
+ (E_aux(E_for(id,from',to_',step',order,block'),(l,Base(([],b_t),Emp_local,local_cs,pure_e))),expect_t,Envmap.empty,
b_c@from_c@to_c@step_c@local_cs,(union_effects b_ef (union_effects step_ef (union_effects to_ef from_ef))))
| E_vector(es) ->
let item_t = match expect_t.t with
@@ -563,7 +597,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
(fun (e,_,_,c,ef) (es,cs,effect) -> (e::es),(c@cs),union_effects ef effect)
(List.map (check_exp envs item_t) es) ([],[],pure_e)) in
let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst 0});TA_nexp({nexp=Nconst (List.length es)});TA_ord({order=Oinc});TA_typ item_t])} in
- let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector es,(l,Some(([],t),Emp_local,[],pure_e)))) expect_t in
+ let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
(e',t',t_env,cs@cs',effect)
| E_vector_indexed eis ->
let item_t = match expect_t.t with
@@ -582,7 +616,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
eis) ([],[],pure_e,first)) in
let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst first});TA_nexp({nexp=Nconst (List.length eis)});
TA_ord({order= if is_increasing then Oinc else Odec});TA_typ item_t])} in
- let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector_indexed es,(l,Some(([],t),Emp_local,[],pure_e)))) expect_t in
+ let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector_indexed es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
(e',t',t_env,cs@cs',effect)
| E_vector_access(vec,i) ->
let base,rise,ord = new_n(),new_n(),new_o() in
@@ -604,7 +638,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| _ -> typ_error l "A vector must be either increasing or decreasing to access a single element"
in
(*let _ = Printf.printf "Type checking vector access. item_t is %s and expect_t is %s\n" (t_to_string item_t) (t_to_string expect_t) in*)
- let t',cs',e'=type_coerce (Expr l) d_env item_t (E_aux(E_vector_access(vec',i'),(l,Some(([],item_t),Emp_local,[],pure_e)))) expect_t in
+ let t',cs',e'=type_coerce (Expr l) d_env item_t (E_aux(E_vector_access(vec',i'),(l,Base(([],item_t),Emp_local,[],pure_e)))) expect_t in
(e',t',t_env,cs_loc@cs_i@cs@cs',union_effects ef ef_i)
| E_vector_subrange(vec,i1,i2) ->
let base,rise,ord = new_n(),new_n(),new_o() in
@@ -634,7 +668,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| _ -> typ_error l "A vector must be either increasing or decreasing to access a slice" in
let nt = {t=Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord;TA_typ item_t])} in
let (t,cs3,e') =
- type_coerce (Expr l) d_env nt (E_aux(E_vector_subrange(vec',i1',i2'),(l,Some(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in
+ type_coerce (Expr l) d_env nt (E_aux(E_vector_subrange(vec',i1',i2'),(l,Base(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in
(e',t,t_env,cs3@cs@cs_i1@cs_i2@cs_loc,(union_effects ef (union_effects ef_i1 ef_i2)))
| E_vector_update(vec,i,e) ->
let base,rise,ord = new_n(),new_n(),new_o() in
@@ -657,7 +691,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
in
let nt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise; TA_ord ord;TA_typ item_t])} in
let (t,cs3,e') =
- type_coerce (Expr l) d_env nt (E_aux(E_vector_update(vec',i',e'),(l,Some(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in
+ type_coerce (Expr l) d_env nt (E_aux(E_vector_update(vec',i',e'),(l,Base(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in
(e',t,t_env,cs3@cs@cs_i@cs_e@cs_loc,(union_effects ef (union_effects ef_i ef_e)))
| E_vector_update_subrange(vec,i1,i2,e) ->
let base,rise,ord = new_n(),new_n(),new_o() in
@@ -691,7 +725,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| _ -> typ_error l "A vector must be either increasing or decreasing to modify a slice" in
let nt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise; TA_ord ord;TA_typ item_t])} in
let (t,cs3,e') =
- type_coerce (Expr l) d_env nt (E_aux(E_vector_update_subrange(vec',i1',i2',e'),(l,Some(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in
+ type_coerce (Expr l) d_env nt (E_aux(E_vector_update_subrange(vec',i1',i2',e'),(l,Base(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in
(e',t,t_env,cs3@cs@cs_i1@cs_i2@cs_loc@cs_e,(union_effects ef (union_effects ef_i1 (union_effects ef_i2 ef_e))))
| E_list(es) ->
let item_t = match expect_t.t with
@@ -701,7 +735,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
(List.fold_right (fun (e,_,_,c,ef) (es,cs,effect) -> (e::es),(c@cs),union_effects ef effect)
(List.map (check_exp envs item_t) es) ([],[],pure_e)) in
let t = {t = Tapp("list",[TA_typ item_t])} in
- let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_list es,(l,Some(([],t),Emp_local,[],pure_e)))) expect_t in
+ let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_list es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
(e',t',t_env,cs@cs',effect)
| E_cons(ls,i) ->
let item_t = match expect_t.t with
@@ -710,7 +744,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
let lt = {t=Tapp("list",[TA_typ item_t])} in
let (ls',t',_,cs,ef) = check_exp envs lt ls in
let (i', ti, _,cs_i,ef_i) = check_exp envs item_t i in
- let (t',cs',e') = type_coerce (Expr l) d_env lt (E_aux(E_cons(ls',i'),(l,Some(([],lt),Emp_local,[],pure_e)))) expect_t in
+ let (t',cs',e') = type_coerce (Expr l) d_env lt (E_aux(E_cons(ls',i'),(l,Base(([],lt),Emp_local,[],pure_e)))) expect_t in
(e',t',t_env,cs@cs'@cs_i,(union_effects ef ef_i))
| E_record(FES_aux(FES_Fexps(fexps,_),l')) ->
let u,_ = get_abbrev d_env expect_t in
@@ -726,14 +760,14 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
(fun (FE_aux(FE_Fexp(id,exp),(l,annot))) (fexps,cons,ef') ->
let i = id_to_string id in
match lookup_field_type i r with
- | None ->
+ | NoTyp ->
typ_error l ("Expected a struct of type " ^ n ^ ", which should not have a field " ^ i)
- | Some((params,et),tag,cs,ef) ->
+ | Base((params,et),tag,cs,ef) ->
let et,cs,_ = subst params et cs ef in
let (e,t',_,c,ef) = check_exp envs et exp in
- (FE_aux(FE_Fexp(id,e),(l,Some(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef'))
+ (FE_aux(FE_Fexp(id,e),(l,Base(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef'))
fexps ([],[],pure_e) in
- E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,Some(([],u),Emp_local,[],pure_e))),expect_t,t_env,cons,ef
+ E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,Base(([],u),Emp_local,[],pure_e))),expect_t,t_env,cons,ef
else typ_error l ("Expected a struct of type " ^ n ^ ", which should have " ^ string_of_int (List.length fields) ^ " fields")
| Some(i,Register,fields) -> typ_error l ("Expected a value with register type, found a struct"))
| Tuvar _ ->
@@ -746,14 +780,14 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
(fun (FE_aux(FE_Fexp(id,exp),(l,annot))) (fexps,cons,ef') ->
let i = id_to_string id in
match lookup_field_type i r with
- | None -> raise (Reporting_basic.err_unreachable l "field_match didn't have a full match")
- | Some((params,et),tag,cs,ef) ->
+ | NoTyp -> raise (Reporting_basic.err_unreachable l "field_match didn't have a full match")
+ | Base((params,et),tag,cs,ef) ->
let et,cs,_ = subst params et cs ef in
let (e,t',_,c,ef) = check_exp envs et exp in
- (FE_aux(FE_Fexp(id,e),(l,Some(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef'))
+ (FE_aux(FE_Fexp(id,e),(l,Base(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef'))
fexps ([],[],pure_e) in
expect_t.t <- Tid i; (*TODO THis should use equate_t !!*)
- E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,Some(([],expect_t),Emp_local,[],pure_e))),expect_t,t_env,cons,ef
+ E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,Base(([],expect_t),Emp_local,[],pure_e))),expect_t,t_env,cons,ef
| Some(i,Register,fields) -> typ_error l "Expected a value with register type, found a struct")
| _ -> typ_error l ("Expected an expression of type " ^ t_to_string expect_t ^ " but found a struct"))
| E_record_update(exp,FES_aux(FES_Fexps(fexps,_),l')) ->
@@ -771,15 +805,15 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
(fun (FE_aux(FE_Fexp(id,exp),(l,annot))) (fexps,cons,ef') ->
let fi = id_to_string id in
match lookup_field_type fi r with
- | None ->
+ | NoTyp ->
typ_error l ("Expected a struct with type " ^ i ^ ", which does not have a field " ^ fi)
- | Some((params,et),tag,cs,ef) ->
+ | Base((params,et),tag,cs,ef) ->
let et,cs,_ = subst params et cs ef in
let (e,t',_,c,ef) = check_exp envs et exp in
- (FE_aux(FE_Fexp(id,e),(l,Some(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef'))
+ (FE_aux(FE_Fexp(id,e),(l,Base(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef'))
fexps ([],[],pure_e) in
E_aux(E_record_update(e',FES_aux(FES_Fexps(fexps,false),l')),
- (l,Some(([],expect_t),Emp_local,[],pure_e))),expect_t,t_env,cons,ef
+ (l,Base(([],expect_t),Emp_local,[],pure_e))),expect_t,t_env,cons,ef
else typ_error l ("Expected fields from struct " ^ i ^ ", given more fields than struct includes"))
| Tuvar _ ->
let field_names = List.map (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) -> id_to_string id) fexps in
@@ -791,15 +825,15 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
(fun (FE_aux(FE_Fexp(id,exp),(l,annot))) (fexps,cons,ef') ->
let i = id_to_string id in
match lookup_field_type i r with
- | None -> raise (Reporting_basic.err_unreachable l "field_match didn't have a full match")
- | Some((params,et),tag,cs,ef) ->
+ | NoTyp -> raise (Reporting_basic.err_unreachable l "field_match didn't have a full match")
+ | Base((params,et),tag,cs,ef) ->
let et,cs,_ = subst params et cs ef in
let (e,t',_,c,ef) = check_exp envs et exp in
- (FE_aux(FE_Fexp(id,e),(l,Some(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef'))
+ (FE_aux(FE_Fexp(id,e),(l,Base(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef'))
fexps ([],[],pure_e) in
expect_t.t <- Tid i;
E_aux(E_record_update(e',FES_aux(FES_Fexps(fexps,false),l')),
- (l,Some(([],expect_t),Emp_local,[],pure_e))),expect_t,t_env,cons,ef
+ (l,Base(([],expect_t),Emp_local,[],pure_e))),expect_t,t_env,cons,ef
| [(i,Register,fields)] -> typ_error l "Expected a value with register type, found a struct"
| records -> typ_error l "Multiple structs contain this set of fields, try adding a cast to disambiguate")
| _ -> typ_error l ("Expected a struct to update but found an expression of type " ^ t_to_string expect_t))
@@ -812,11 +846,11 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| Some(((i,rec_kind,fields) as r)) ->
let fi = id_to_string id in
(match lookup_field_type fi r with
- | None ->
+ | NoTyp ->
typ_error l ("Type " ^ i ^ " does not have a field " ^ fi)
- | Some((params,et),tag,cs,ef) ->
+ | Base((params,et),tag,cs,ef) ->
let et,cs,ef = subst params et cs ef in
- let (et',c',acc) = type_coerce (Expr l) d_env et (E_aux(E_field(e',id),(l,Some(([],et),tag,cs,ef)))) expect_t in
+ let (et',c',acc) = type_coerce (Expr l) d_env et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef)))) expect_t in
(acc,et',t_env,cs@c',ef)))
| Tid i ->
(match lookup_record_typ i d_env.rec_env with
@@ -824,11 +858,11 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| Some(((i,rec_kind,fields) as r)) ->
let fi = id_to_string id in
(match lookup_field_type fi r with
- | None ->
+ | NoTyp ->
typ_error l ("Type " ^ i ^ " does not have a field " ^ fi)
- | Some((params,et),tag,cs,ef) ->
+ | Base((params,et),tag,cs,ef) ->
let et,cs,ef = subst params et cs ef in
- let (et',c',acc) = type_coerce (Expr l) d_env et (E_aux(E_field(e',id),(l,Some(([],et),tag,cs,ef)))) expect_t in
+ let (et',c',acc) = type_coerce (Expr l) d_env et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef)))) expect_t in
(acc,et',t_env,cs@c',ef)))
| Tuvar _ ->
let fi = id_to_string id in
@@ -837,11 +871,11 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| [(((i,rkind,fields) as r))] ->
let fi = id_to_string id in
(match lookup_field_type fi r with
- | None ->
+ | NoTyp ->
raise (Reporting_basic.err_unreachable l "lookup_possible_records returned a record that didn't include the field")
- | Some((params,et),tag,cs,ef) ->
+ | Base((params,et),tag,cs,ef) ->
let et,cs,ef = subst params et cs ef in
- let (et',c',acc) = type_coerce (Expr l) d_env et (E_aux(E_field(e',id),(l,Some(([],et),tag,cs,ef)))) expect_t in
+ let (et',c',acc) = type_coerce (Expr l) d_env et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef)))) expect_t in
(*TODO tHIS should be equate_t*)
t'.t <- Tid i;
(acc,et',t_env,cs@c',ef))
@@ -857,21 +891,21 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| _ -> t' in
(*let _ = Printf.printf "Type of pattern after register check %s\n" (t_to_string t') in*)
let (pexps',t,cs',ef') = check_cases envs t' expect_t pexps in
- (E_aux(E_case(e',pexps'),(l,Some(([],t),Emp_local,[],pure_e))),t,t_env,cs@cs',union_effects ef ef')
+ (E_aux(E_case(e',pexps'),(l,Base(([],t),Emp_local,[],pure_e))),t,t_env,cs@cs',union_effects ef ef')
| E_let(lbind,body) ->
let (lb',t_env',cs,ef) = (check_lbind envs false Emp_local lbind) in
let (e,t,_,cs',ef') = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env t_env')) expect_t body in
- (E_aux(E_let(lb',e),(l,Some(([],t),Emp_local,[],pure_e))),t,t_env,cs@cs',union_effects ef ef')
+ (E_aux(E_let(lb',e),(l,Base(([],t),Emp_local,[],pure_e))),t,t_env,cs@cs',union_effects ef ef')
| E_assign(lexp,exp) ->
let (lexp',t',t_env',tag,cs,ef) = check_lexp envs true lexp in
let (exp',t'',_,cs',ef') = check_exp envs t' exp in
let (t',c') = type_consistent (Expr l) d_env unit_t expect_t in
- (E_aux(E_assign(lexp',exp'),(l,(Some(([],unit_t),tag,[],ef)))),unit_t,t_env',cs@cs'@c',union_effects ef ef')
+ (E_aux(E_assign(lexp',exp'),(l,(Base(([],unit_t),tag,[],ef)))),unit_t,t_env',cs@cs'@c',union_effects ef ef')
and check_block orig_envs envs expect_t exps : ((tannot exp) list * tannot * tannot emap * nexp_range list * t * effect) =
let Env(d_env,t_env) = envs in
match exps with
- | [] -> ([],None,orig_envs,[],unit_t,pure_e)
+ | [] -> ([],NoTyp,orig_envs,[],unit_t,pure_e)
| [e] -> let (E_aux(e',(l,annot)),t,envs,sc,ef) = check_exp envs expect_t e in
([E_aux(e',(l,annot))],annot,orig_envs,sc,t,ef)
| e::exps -> let (e',t',t_env',sc,ef') = check_exp envs unit_t e in
@@ -887,13 +921,13 @@ and check_cases envs check_t expect_t pexps : ((tannot pexp) list * typ * nexp_r
let pat',env,cs_p,u = check_pattern envs Emp_local check_t pat in
let e,t,_,cs_e,ef = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env env)) expect_t exp in
let cs = [CondCons(Expr l, cs_p, cs_e)] in
- [Pat_aux(Pat_exp(pat',e),(l,Some(([],t),Emp_local,cs,ef)))],t,cs,ef
+ [Pat_aux(Pat_exp(pat',e),(l,Base(([],t),Emp_local,cs,ef)))],t,cs,ef
| ((Pat_aux(Pat_exp(pat,exp),(l,annot)))::pexps) ->
let pat',env,cs_p,u = check_pattern envs Emp_local check_t pat in
let (e,t,_,cs_e,ef) = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env env)) expect_t exp in
let cs = CondCons(Expr l,cs_p,cs_e) in
let (pes,tl,csl,efl) = check_cases envs check_t expect_t pexps in
- ((Pat_aux(Pat_exp(pat',e),(l,(Some(([],t),Emp_local,[cs],ef)))))::pes,
+ ((Pat_aux(Pat_exp(pat',e),(l,(Base(([],t),Emp_local,[cs],ef)))))::pes,
tl,
cs::csl,union_effects efl ef)
@@ -903,9 +937,9 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
| LEXP_id id ->
let i = id_to_string id in
(match Envmap.apply t_env i with
- | Some(Some((parms,t),Default,_,_)) ->
+ | Some(Base((parms,t),Default,_,_)) ->
typ_error l ("Identifier " ^ i ^ " cannot be assigned when only a default specification exists")
- | Some(Some((parms,t),tag,cs,_)) ->
+ | Some(Base((parms,t),tag,cs,_)) ->
let t,cs,_ = match tag with | External _ | Emp_global -> subst parms t cs pure_e | _ -> t,cs,pure_e in
let t,cs' = get_abbrev d_env t in
let t_actual = match t.t with
@@ -915,26 +949,26 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
(match t_actual.t,is_top with
| Tapp("register",[TA_typ u]),_ ->
let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in
- (LEXP_aux(lexp,(l,(Some(([],t),External (Some i),cs@cs',ef)))),u,Envmap.empty,External (Some i),[],ef)
+ (LEXP_aux(lexp,(l,(Base(([],t),External (Some i),cs@cs',ef)))),u,Envmap.empty,External (Some i),[],ef)
| Tapp("reg",[TA_typ u]),_ ->
- (LEXP_aux(lexp,(l,(Some(([],t),Emp_local,cs@cs',pure_e)))),u,Envmap.empty,Emp_local,[],pure_e)
+ (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs@cs',pure_e)))),u,Envmap.empty,Emp_local,[],pure_e)
| Tapp("vector",_),false ->
- (LEXP_aux(lexp,(l,(Some(([],t),Emp_local,cs@cs',pure_e)))),t,Envmap.empty,Emp_local,[],pure_e)
+ (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs@cs',pure_e)))),t,Envmap.empty,Emp_local,[],pure_e)
| _,_ ->
if is_top
then typ_error l
("Can only assign to identifiers with type register or reg, found identifier " ^ i ^ " with type " ^ t_to_string t)
else
- (LEXP_aux(lexp,(l,(Some(([],t),Emp_local,cs@cs',pure_e)))),t,Envmap.empty,Emp_local,[],pure_e) (* TODO, make sure this is a record *))
+ (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs@cs',pure_e)))),t,Envmap.empty,Emp_local,[],pure_e) (* TODO, make sure this is a record *))
| _ ->
let u = new_t() in
let t = {t=Tapp("reg",[TA_typ u])} in
- let tannot = (Some(([],t),Emp_local,[],pure_e)) in
+ let tannot = (Base(([],t),Emp_local,[],pure_e)) in
(LEXP_aux(lexp,(l,tannot)),u,Envmap.from_list [i,tannot],Emp_local,[],pure_e))
| LEXP_memory(id,exps) ->
let i = id_to_string id in
(match Envmap.apply t_env i with
- | Some(Some((parms,t),tag,cs,ef)) ->
+ | Some(Base((parms,t),tag,cs,ef)) ->
let is_external = match tag with | External any -> true | _ -> false in
let t,cs,ef = subst parms t cs ef in
(match t.t with
@@ -947,15 +981,15 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
let out,cs_o = get_abbrev d_env out in
(match app.t with
| Ttup ts | Tabbrev(_,{t=Ttup ts}) ->
- let (E_aux(E_tuple es,(l',tannot)),t',_,cs',ef_e) = check_exp envs apps (E_aux(E_tuple exps,(l,None))) in
+ let (E_aux(E_tuple es,(l',tannot)),t',_,cs',ef_e) = check_exp envs apps (E_aux(E_tuple exps,(l,NoTyp))) in
let item_t = match out.t with
| Tid "unit" -> {t = Tapp("vector",[TA_nexp (new_n());TA_nexp (new_n()); TA_ord (new_o());TA_typ bit_t])}
| _ -> out in
let ef = if is_external then add_effect (BE_aux(BE_wmem,l)) ef_e else union_effects ef ef_e in
- (LEXP_aux(LEXP_memory(id,es),(l,Some(([],unit_t),tag,cs@cs',ef))),item_t,Envmap.empty,tag,cs@cs',ef)
+ (LEXP_aux(LEXP_memory(id,es),(l,Base(([],unit_t),tag,cs@cs',ef))),item_t,Envmap.empty,tag,cs@cs',ef)
| app_t ->
let e = match exps with
- | [] -> E_aux(E_lit(L_aux(L_unit,l)),(l,None))
+ | [] -> E_aux(E_lit(L_aux(L_unit,l)),(l,NoTyp))
| [e] -> e
| es -> typ_error l ("Expected only one argument for memory access of " ^ i) in
let (e,t',_,cs',ef_e) = check_exp envs apps e in
@@ -963,7 +997,7 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
| Tid "unit" -> {t = Tapp("vector",[TA_nexp (new_n());TA_nexp (new_n()); TA_ord (new_o());TA_typ bit_t])}
| _ -> out in
let ef = if is_external then add_effect (BE_aux(BE_wmem,l)) ef_e else union_effects ef ef_e in
- (LEXP_aux(LEXP_memory(id,[e]),(l,Some(([],unit_t),tag,cs@cs',ef))), item_t,Envmap.empty,tag,cs@cs',ef))
+ (LEXP_aux(LEXP_memory(id,[e]),(l,Base(([],unit_t),tag,cs@cs',ef))), item_t,Envmap.empty,tag,cs@cs',ef))
else typ_error l ("Memory assignments require functions with wmem effect")
| _ -> typ_error l ("Memory assignments require functions with declared wmem effect"))
| _ -> typ_error l ("Memory assignments require functions, found " ^ i ^ " which has type " ^ (t_to_string t)))
@@ -972,9 +1006,9 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
let i = id_to_string id in
let ty = typ_to_t typ in
(match Envmap.apply t_env i with
- | Some(Some((parms,t),Default,_,_)) ->
+ | Some(Base((parms,t),Default,_,_)) ->
typ_error l ("Identifier " ^ i ^ " cannot be assigned when only a default specification exists")
- | Some(Some((parms,t),tag,cs,_)) ->
+ | Some(Base((parms,t),tag,cs,_)) ->
let t,cs,_ = match tag with | External _ | Emp_global -> subst parms t cs pure_e | _ -> t,cs,pure_e in
let t,cs' = get_abbrev d_env t in
let t_actual = match t.t with | Tabbrev(_,t) -> t | _ -> t in
@@ -982,25 +1016,25 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
| Tapp("register",[TA_typ u]),_ ->
let t',cs = type_consistent (Expr l) d_env ty u in
let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in
- (LEXP_aux(lexp,(l,(Some(([],t),External (Some i),cs,ef)))),ty,Envmap.empty,External (Some i),[],ef)
+ (LEXP_aux(lexp,(l,(Base(([],t),External (Some i),cs,ef)))),ty,Envmap.empty,External (Some i),[],ef)
| Tapp("reg",[TA_typ u]),_ ->
let t',cs = type_consistent (Expr l) d_env ty u in
- (LEXP_aux(lexp,(l,(Some(([],t),Emp_local,cs,pure_e)))),ty,Envmap.empty,Emp_local,[],pure_e)
+ (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e)))),ty,Envmap.empty,Emp_local,[],pure_e)
| Tapp("vector",_),false ->
- (LEXP_aux(lexp,(l,(Some(([],t),Emp_local,cs,pure_e)))),ty,Envmap.empty,Emp_local,[],pure_e)
+ (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e)))),ty,Envmap.empty,Emp_local,[],pure_e)
| Tuvar _,_ ->
let u' = {t=Tapp("reg",[TA_typ ty])} in
t.t <- u'.t;
- (LEXP_aux(lexp,(l,(Some((([],u'),Emp_local,cs,pure_e))))),ty,Envmap.empty,Emp_local,[],pure_e)
+ (LEXP_aux(lexp,(l,(Base((([],u'),Emp_local,cs,pure_e))))),ty,Envmap.empty,Emp_local,[],pure_e)
| _,_ ->
if is_top
then typ_error l
("Can only assign to identifiers with type register or reg, found identifier " ^ i ^ " with type " ^ t_to_string t)
else
- (LEXP_aux(lexp,(l,(Some(([],t),Emp_local,cs,pure_e)))),ty,Envmap.empty,Emp_local,[],pure_e)) (* TODO, make sure this is a record *)
+ (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e)))),ty,Envmap.empty,Emp_local,[],pure_e)) (* TODO, make sure this is a record *)
| _ ->
let t = {t=Tapp("reg",[TA_typ ty])} in
- let tannot = (Some(([],t),Emp_local,[],pure_e)) in
+ let tannot = (Base(([],t),Emp_local,[],pure_e)) in
(LEXP_aux(lexp,(l,tannot)),ty,Envmap.from_list [i,tannot],Emp_local,[],pure_e))
| LEXP_vector(vec,acc) ->
let (vec',item_t,env,tag,csi,ef) = check_lexp envs false vec in
@@ -1019,7 +1053,7 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
| Tapp("register",[TA_typ t]) | Tabbrev(_,{t=Tapp("register",[TA_typ t])}) -> t,true
| _ -> t,false in
let ef = if add_reg_write then add_effect (BE_aux(BE_wreg,l)) ef else ef in
- (LEXP_aux(LEXP_vector(vec',e),(l,Some(([],t),tag,csi,ef))),t,env,tag,csi@cs',union_effects ef ef_e)
+ (LEXP_aux(LEXP_vector(vec',e),(l,Base(([],t),tag,csi,ef))),t,env,tag,csi@cs',union_effects ef ef_e)
| Tuvar _ -> typ_error l "Assignment to one position expected a vector with a known order, found a polymorphic value, try adding a cast"
| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string item_t)))
| LEXP_vector_range(vec,e1,e2)->
@@ -1054,13 +1088,13 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
let (e2',t',_,cs2,ef_e') = check_exp envs range_t e2 in
let cs = cs_t@cs@cs1@cs2 in
let ef = union_effects ef (union_effects ef_e ef_e') in
- (LEXP_aux(LEXP_vector_range(vec',e1',e2'),(l,Some(([],item_t),tag,cs,ef))),res_t,env,tag,cs,ef)
+ (LEXP_aux(LEXP_vector_range(vec',e1',e2'),(l,Base(([],item_t),tag,cs,ef))),res_t,env,tag,cs,ef)
| Tuvar _ -> typ_error l "Assignement to a range of elements requires a vector with a known order, found a polymorphic value, try addinga cast"
| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string item_t)))
| LEXP_field(vec,id)->
let (vec',item_t,env,tag,csi,ef) = check_lexp envs false vec in
let vec_t = match vec' with
- | LEXP_aux(_,(l',Some((parms,t),_,_,_))) -> t
+ | LEXP_aux(_,(l',Base((parms,t),_,_,_))) -> t
| _ -> item_t in
(match vec_t.t with
| Tid i | Tabbrev({t=Tid i},_) ->
@@ -1069,11 +1103,11 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
| Some(((i,rec_kind,fields) as r)) ->
let fi = id_to_string id in
(match lookup_field_type fi r with
- | None ->
+ | NoTyp ->
typ_error l ("Type " ^ i ^ " does not have a field " ^ fi)
- | Some((params,et),_,cs,_) ->
+ | Base((params,et),_,cs,_) ->
let et,cs,ef = subst params et cs ef in
- (LEXP_aux(LEXP_field(vec',id),(l,(Some(([],vec_t),tag,csi@cs,ef)))),et,env,tag,csi@cs,ef)))
+ (LEXP_aux(LEXP_field(vec',id),(l,(Base(([],vec_t),tag,csi@cs,ef)))),et,env,tag,csi@cs,ef)))
| _ -> typ_error l ("Expected a register binding here, found " ^ (t_to_string item_t)))
and check_lbind envs is_top_level emp_tag (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * nexp_range list * effect =
@@ -1082,21 +1116,21 @@ and check_lbind envs is_top_level emp_tag (LB_aux(lbind,(l,annot))) : tannot let
| LB_val_explicit(typ,pat,e) ->
let tan = typschm_to_tannot envs typ emp_tag in
(match tan with
- | Some((params,t),tag,cs,ef) ->
+ | Base((params,t),tag,cs,ef) ->
let t,cs,ef = subst params t cs ef in
let (pat',env,cs1,u) = check_pattern envs emp_tag t pat in
let (e,t,_,cs2,ef2) = check_exp envs u e in
let cs = resolve_constraints cs@cs1@cs2 in
let ef = union_effects ef ef2 in
- let tannot = check_tannot l (Some((params,t),tag,cs,ef)) cs ef (*in top level, must be pure_e*) in
+ let tannot = check_tannot l (Base((params,t),tag,cs,ef)) cs ef (*in top level, must be pure_e*) in
(LB_aux (LB_val_explicit(typ,pat',e),(l,tannot)),env,cs,ef)
- | None -> raise (Reporting_basic.err_unreachable l "typschm_to_tannot failed to produce a Some"))
+ | NoTyp -> raise (Reporting_basic.err_unreachable l "typschm_to_tannot failed to produce a Some"))
| LB_val_implicit(pat,e) ->
let t = new_t () in
let (pat',env,cs1,u) = check_pattern envs emp_tag (new_t ()) pat in
let (e,t',_,cs2,ef) = check_exp envs u e in
let cs = resolve_constraints cs1@cs2 in
- let tannot = check_tannot l (Some(([],t'),emp_tag,cs,ef)) cs ef (* see above *) in
+ let tannot = check_tannot l (Base(([],t'),emp_tag,cs,ef)) cs ef (* see above *) in
(LB_aux (LB_val_implicit(pat',e),(l,tannot)), env,cs,ef)
(*val check_type_def : envs -> (tannot type_def) -> (tannot type_def) envs_out*)
@@ -1110,16 +1144,16 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
| TD_record(id,nmscm,typq,fields,_) ->
let id' = id_to_string id in
let (params,constraints) = typq_to_params envs typq in
- let tyannot = Some((params,{t=Tid id'}),Emp_global,constraints,pure_e) in
+ let tyannot = Base((params,{t=Tid id'}),Emp_global,constraints,pure_e) in
let fields' = List.map
- (fun (ty,i)->(id_to_string i),Some((params,(typ_to_t ty)),Emp_global,constraints,pure_e)) fields in
+ (fun (ty,i)->(id_to_string i),Base((params,(typ_to_t ty)),Emp_global,constraints,pure_e)) fields in
(TD_aux(td,(l,tyannot)),Env({d_env with rec_env = (id',Record,fields')::d_env.rec_env},t_env))
| TD_variant(id,nmscm,typq,arms,_) ->
let id' = id_to_string id in
let (params,constraints) = typq_to_params envs typq in
let ty = {t=Tid id'} in
- let tyannot = Some((params,ty),Constructor,constraints,pure_e) in
- let arm_t input = Some((params,{t=Tfn(input,ty,pure_e)}),Constructor,constraints,pure_e) in
+ let tyannot = Base((params,ty),Constructor,constraints,pure_e) in
+ let arm_t input = Base((params,{t=Tfn(input,ty,pure_e)}),Constructor,constraints,pure_e) in
let arms' = List.map
(fun (Tu_aux(tu,l')) ->
match tu with
@@ -1131,7 +1165,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
| TD_enum(id,nmscm,ids,_) ->
let id' = id_to_string id in
let ids' = List.map id_to_string ids in
- let ty = Some (([],{t = Tid id' }),Enum,[],pure_e) in
+ let ty = Base (([],{t = Tid id' }),Enum,[],pure_e) in
let t_env = List.fold_right (fun id t_env -> Envmap.insert t_env (id,ty)) ids' t_env in
let enum_env = Envmap.insert d_env.enum_env (id',ids') in
(TD_aux(td,(l,ty)),Env({d_env with enum_env = enum_env;},t_env))
@@ -1148,7 +1182,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
List.map
(fun ((BF_aux(idx,l)),id) ->
((id_to_string id),
- Some(([],
+ Base(([],
match idx with
| BF_single i ->
if b <= i && i <= t
@@ -1163,7 +1197,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
| BF_concat _ -> assert false (* What is this supposed to imply again?*)),Emp_global,[],pure_e)))
ranges
in
- let tannot = into_register d_env (Some(([],ty),Emp_global,[],pure_e)) in
+ let tannot = into_register d_env (Base(([],ty),Emp_global,[],pure_e)) in
(TD_aux(td,(l,tannot)),
Env({d_env with rec_env = ((id',Register,franges)::d_env.rec_env);
abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env)))
@@ -1187,10 +1221,10 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
else typ_error l ("register type declaration " ^ id' ^ " is not consistently decreasing")
| BF_concat _ -> assert false (* What is this supposed to imply again?*) in
((id_to_string id),
- Some(([],{t=Tapp("vector",[TA_nexp base;TA_nexp climb;TA_ord({order=Odec});TA_typ({t= Tid "bit"})])}),Emp_global,[],pure_e)))
+ Base(([],{t=Tapp("vector",[TA_nexp base;TA_nexp climb;TA_ord({order=Odec});TA_typ({t= Tid "bit"})])}),Emp_global,[],pure_e)))
ranges
in
- let tannot = into_register d_env (Some(([],ty),Emp_global,[],pure_e)) in
+ let tannot = into_register d_env (Base(([],ty),Emp_global,[],pure_e)) in
(TD_aux(td,(l,tannot)),
Env({d_env with rec_env = (id',Register,franges)::d_env.rec_env;
abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env)))
@@ -1242,7 +1276,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
let t,constraints,_ = subst ids t constraints pure_e in
let p_t = new_t () in
let ef = new_e () in
- t,p_t,Some((ids,{t=Tfn(p_t,t,ef)}),Emp_global,constraints,ef) in
+ t,p_t,Base((ids,{t=Tfn(p_t,t,ef)}),Emp_global,constraints,ef) in
let check t_env =
List.split
(List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),l)) ->
@@ -1254,7 +1288,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
let cs = [CondCons(Fun l,cs_p,cs_e)] in
(FCL_aux((FCL_Funcl(id,pat',exp')),l),(cs,ef))) funcls) in
match (in_env,tannot) with
- | Some(Some( (params,u),Spec,constraints,eft)), Some( (p',t),_,c',eft') ->
+ | Some(Base( (params,u),Spec,constraints,eft)), Base( (p',t),_,c',eft') ->
(*let _ = Printf.printf "Function %s is in env\n" id in*)
let u,constraints,eft = subst params u constraints eft in
let t',cs = type_consistent (Specc l) d_env t u in
@@ -1291,7 +1325,7 @@ let check_def envs def =
| DEF_reg_dec(DEC_aux(DEC_reg(typ,id), (l,annot))) ->
let t = (typ_to_t typ) in
let i = id_to_string id in
- let tannot = into_register d_env (Some(([],t),External (Some i),[],pure_e)) in
+ let tannot = into_register d_env (Base(([],t),External (Some i),[],pure_e)) in
(DEF_reg_dec(DEC_aux(DEC_reg(typ,id),(l,tannot))),(Env(d_env,Envmap.insert t_env (i,tannot))))
diff --git a/src/type_internal.ml b/src/type_internal.ml
index d305335d..0d8e195c 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -81,9 +81,15 @@ type nexp_range =
| In of constraint_origin * string * int list
| InS of constraint_origin * nexp * int list (* This holds the given value for string after a substitution *)
| CondCons of constraint_origin * nexp_range list * nexp_range list
+ | BranchCons of constraint_origin * nexp_range list
type t_params = (string * kind) list
-type tannot = ((t_params * t) * tag * nexp_range list * effect) option
+type tannot =
+ | NoTyp
+ | Base of (t_params * t) * tag * nexp_range list * effect
+ | Overload of tannot * tannot list (* First tannot is the most polymorphic version; the list includes all variants. All t to be Tfn *)
+
+(*type tannot = ((t_params * t) * tag * nexp_range list * effect) option*)
type 'a emap = 'a Envmap.t
type rec_kind = Record | Register
@@ -104,7 +110,7 @@ let get_index n =
| _ -> assert false
let get_c_loc = function
- | Patt l | Expr l | Specc l -> l
+ | Patt l | Expr l | Specc l | Fun l -> l
let rec string_of_list sep string_of = function
| [] -> ""
@@ -156,10 +162,12 @@ let tag_to_string = function
| Enum -> "Enum"
| Spec -> "Spec"
-let tannot_to_string = function
- | None -> "No tannot"
- | Some((vars,t),tag,ncs,ef) ->
+let rec tannot_to_string = function
+ | NoTyp -> "No tannot"
+ | Base((vars,t),tag,ncs,ef) ->
"Tannot: type = " ^ (t_to_string t) ^ " tag = " ^ tag_to_string tag ^ " constraints = not printing effect = " ^ e_to_string ef
+ | Overload(poly,variants) ->
+ "Overloaded: poly = " ^ tannot_to_string poly
let rec effect_remove_dups = function
| [] -> []
@@ -213,7 +221,7 @@ let rec lookup_possible_records (fields : string list) (env : rec_env list) : re
let lookup_field_type (field: string) ((id,r_kind,fields) : rec_env) : tannot =
if List.mem_assoc field fields
then List.assoc field fields
- else None
+ else NoTyp
(* eval an nexp as much as possible *)
let rec eval_nexp n =
@@ -511,54 +519,78 @@ let mk_bitwise_op name symb arity =
let vec_typ = mk_vector bit_t ovar (Nconst 0) (Nvar "n") in
let args = Array.to_list (Array.make arity vec_typ) in
let arg = if ((List.length args) = 1) then List.hd args else {t= Ttup args} in
- (symb,Some((["n",{k=K_Nat}; "o",{k=K_Ord}], {t= Tfn (arg, vec_typ, pure_e)}),External (Some name),[],pure_e))
+ (symb,Base((["n",{k=K_Nat}; "o",{k=K_Ord}], {t= Tfn (arg, vec_typ, pure_e)}),External (Some name),[],pure_e))
let initial_typ_env =
Envmap.from_list [
- ("ignore",Some(([("a",{k=K_Typ});("b",{k=K_Efct})],{t=Tfn ({t=Tvar "a"},unit_t,pure_e)}),External None,[],pure_e));
- ("+",Some(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})],
+ ("ignore",Base(([("a",{k=K_Typ});("b",{k=K_Efct})],{t=Tfn ({t=Tvar "a"},unit_t,pure_e)}),External None,[],pure_e));
+ ("+",Base(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})],
{t= Tfn({t=Ttup([mk_range (Nvar "n") (Nvar "m");
mk_range (Nvar "o") (Nvar "p")])},
(mk_range (Nadd({nexp=Nvar "n"},{nexp=Nvar "o"})) (Nadd({nexp=Nvar "m"},{nexp=Nvar "p"}))),
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(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})],
+ ("*",Base(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "multiply"),[],pure_e));
+ ("-",Base(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})],
{t= Tfn({t=Ttup([mk_range (Nvar "n") (Nvar "m");
mk_range (Nvar "o") (Nvar "p")])},
(mk_range (Nadd ({nexp=(Nvar "n")},{ nexp = Nneg({nexp=Nvar "o"})})) (Nadd({nexp=Nvar "m"},{nexp =Nneg {nexp=Nvar "p"}}))),
pure_e)}),External (Some "minus"),
[GtEq(Specc(Parse_ast.Int("-",None)),{nexp=Nvar "n"},{nexp=Nvar "o"});
GtEq(Specc(Parse_ast.Int("-",None)),{nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},{nexp=Nvar "o"})],pure_e));
- ("mod",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "mod"),[],pure_e));
- ("quot",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "quot"),[],pure_e));
+ ("mod",Base(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "mod"),[],pure_e));
+ ("quot",Base(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "quot"),[],pure_e));
(*Type incomplete*)
- (":",Some(([("a",{k=K_Typ});("b",{k=K_Typ});("c",{k=K_Typ})],
+ (":",Base(([("a",{k=K_Typ});("b",{k=K_Typ});("c",{k=K_Typ})],
{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "b"}])},{t=Tvar "c"},pure_e)}),External (Some "vec_concat"),[],pure_e));
- ("to_num_inc",Some(([("a",{k=K_Typ})],{t= Tfn ({t=Tvar "a"},nat_typ,pure_e)}),External None,[],pure_e));
- ("to_num_dec",Some(([("a",{k=K_Typ})],{t= Tfn ({t=Tvar "a"},nat_typ,pure_e)}),External None,[],pure_e));
- ("to_vec_inc",Some(([("a",{k=K_Typ})],{t= Tfn (nat_typ,{t=Tvar "a"},pure_e)}),External None,[],pure_e));
- ("to_vec_dec",Some(([("a",{k=K_Typ})],{t= Tfn (nat_typ,{t=Tvar "a"},pure_e)}),External None,[],pure_e));
- ("==",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "eq"),[],pure_e));
- ("!=",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "neq"),[],pure_e));
- ("<",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "lt"),[],pure_e));
- (">",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "gt"),[],pure_e));
- ("<_u",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "ltu"),[],pure_e));
- (">_u",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "gtu"),[],pure_e));
- ("is_one",Some(([],{t= Tfn (bit_t,bool_t,pure_e)}),External (Some "is_one"),[],pure_e));
+ ("to_num_inc",Base(([("a",{k=K_Typ})],{t= Tfn ({t=Tvar "a"},nat_typ,pure_e)}),External None,[],pure_e));
+ ("to_num_dec",Base(([("a",{k=K_Typ})],{t= Tfn ({t=Tvar "a"},nat_typ,pure_e)}),External None,[],pure_e));
+ ("to_vec_inc",Base(([("a",{k=K_Typ})],{t= Tfn (nat_typ,{t=Tvar "a"},pure_e)}),External None,[],pure_e));
+ ("to_vec_dec",Base(([("a",{k=K_Typ})],{t= Tfn (nat_typ,{t=Tvar "a"},pure_e)}),External None,[],pure_e));
+ ("==",
+ Overload( Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "eq"),[],pure_e),
+ [Base(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})],
+ {t = Tfn({t=Ttup([mk_range (Nvar "n") (Nvar "m");mk_range (Nvar "o") (Nvar "p")])},bit_t,pure_e)}), External (Some "eq"),
+ [Eq(Specc(Parse_ast.Int("==",None)),
+ {nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},
+ {nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})})],pure_e);
+ Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "eq"),[],pure_e)]));
+ ("!=",Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "neq"),[],pure_e));
+ ("<",
+ Overload(Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "lt"),[],pure_e),
+ [Base(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})],
+ {t = Tfn({t=Ttup([mk_range (Nvar "n") (Nvar "m");mk_range (Nvar "o") (Nvar "p")])},bit_t,pure_e)}), External (Some "lt"),
+ [LtEq(Specc(Parse_ast.Int("<",None)),
+ {nexp=Nadd({nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},{nexp=Nconst 1})},
+ {nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})})],pure_e);
+ (*Probably should talk about vectors, but of what size restrictions? *)
+ Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "lt"),[],pure_e)])
+ );
+ (">",
+ Overload(Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "gt"),[],pure_e),
+ [Base(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})],
+ {t = Tfn({t=Ttup([mk_range (Nvar "n") (Nvar "m");mk_range (Nvar "o") (Nvar "p")])},bit_t,pure_e)}), External (Some "gt"),
+ [GtEq(Specc(Parse_ast.Int(">",None)),
+ {nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},
+ {nexp=Nadd({nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})},{nexp=Nconst 1})})],pure_e);
+ Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "gt"),[],pure_e)])
+ );
+ ("<_u",Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "ltu"),[],pure_e));
+ (">_u",Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "gtu"),[],pure_e));
+ ("is_one",Base(([],{t= Tfn (bit_t,bool_t,pure_e)}),External (Some "is_one"),[],pure_e));
mk_bitwise_op "bitwise_not" "~" 1;
mk_bitwise_op "bitwise_or" "|" 2;
mk_bitwise_op "bitwise_xor" "^" 2;
mk_bitwise_op "bitwise_and" "&" 2;
- ("^^",Some(([("n",{k=K_Nat});("m",{k=K_Nat})],
+ ("^^",Base(([("n",{k=K_Nat});("m",{k=K_Nat})],
{t= Tfn ({t=Ttup([bit_t;mk_range (Nvar "n") (Nvar "m")])},
mk_vector bit_t Oinc (Nconst 0) (Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})),
pure_e)}),External (Some "duplicate"),[],pure_e));
- ("<<<",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};nat_typ])},{t=Tvar "a"},pure_e)}),External (Some "bitwise_leftshift"),[],pure_e));
+ ("<<<",Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};nat_typ])},{t=Tvar "a"},pure_e)}),External (Some "bitwise_leftshift"),[],pure_e));
]
let initial_abbrev_env =
Envmap.from_list [
- ("nat",Some(([],nat_t),Emp_global,[],pure_e));
+ ("nat",Base(([],nat_t),Emp_global,[],pure_e));
]
let rec t_subst s_env t =
@@ -617,6 +649,8 @@ let rec cs_subst t_env cs =
| _ -> ());
InS(l,nexp,ns)::(cs_subst t_env cs)
| InS(l,n,ns)::cs -> InS(l,n_subst t_env n,ns)::(cs_subst t_env cs)
+ | CondCons(l,cs_p,cs_e)::cs -> CondCons(l,cs_subst t_env cs_p,cs_subst t_env cs_e)::(cs_subst t_env cs)
+ | BranchCons(l,bs)::cs -> BranchCons(l,cs_subst t_env bs)::(cs_subst t_env cs)
let subst k_env t cs e =
let subst_env = Envmap.from_list
@@ -667,15 +701,6 @@ and e_remove_unifications s_env e =
| None -> s_env)
| _ -> s_env
-let rec cs_subst t_env cs =
- match cs with
- | [] -> []
- | Eq(l,n1,n2)::cs -> Eq(l,n_subst t_env n1,n_subst t_env n2)::(cs_subst t_env cs)
- | GtEq(l,n1,n2)::cs -> GtEq(l,n_subst t_env n1, n_subst t_env n2)::(cs_subst t_env cs)
- | LtEq(l,n1,n2)::cs -> LtEq(l,n_subst t_env n1, n_subst t_env n2)::(cs_subst t_env cs)
- | In(l,s,ns)::cs -> InS(l,n_subst t_env {nexp=Nvar s},ns)::(cs_subst t_env cs)
- | InS(l,n,ns)::cs -> InS(l,n_subst t_env n,ns)::(cs_subst t_env cs)
- | CondCons(l, pats, exps)::cs -> CondCons(l, cs_subst t_env pats, cs_subst t_env exps)::(cs_subst t_env cs)
let subst k_env t cs e =
let subst_env = Envmap.from_list
@@ -735,7 +760,7 @@ let rec get_abbrev d_env t =
match t.t with
| Tid i ->
(match Envmap.apply d_env.abbrevs i with
- | Some(Some((params,ta),tag,cs,efct)) ->
+ | Some(Base((params,ta),tag,cs,efct)) ->
let ta,cs,_ = subst params ta cs efct in
let ta,cs' = get_abbrev d_env ta in
(match ta.t with
@@ -744,7 +769,7 @@ let rec get_abbrev d_env t =
| _ -> t,[])
| Tapp(i,args) ->
(match Envmap.apply d_env.abbrevs i with
- | Some(Some((params,ta),tag,cs,efct)) ->
+ | Some(Base((params,ta),tag,cs,efct)) ->
let env = Envmap.from_list2 (List.map fst params) args in
let ta,cs' = get_abbrev d_env (t_subst env ta) in
(match ta.t with
@@ -888,18 +913,18 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
let tl1,tl2 = List.length t1s,List.length t2s in
if tl1=tl2 then
let ids = List.map (fun _ -> Id_aux(Id (new_id ()),l)) t1s in
- let vars = List.map2 (fun i t -> E_aux(E_id(i),(l,Some(([],t),Emp_local,[],pure_e)))) ids t1s in
+ let vars = List.map2 (fun i t -> E_aux(E_id(i),(l,Base(([],t),Emp_local,[],pure_e)))) ids t1s in
let (coerced_ts,cs,coerced_vars) =
List.fold_right2 (fun v (t1,t2) (ts,cs,es) -> let (t',c',e') = type_coerce co d_env t1 v t2 in
((t'::ts),c'@cs,(e'::es)))
vars (List.combine t1s t2s) ([],[],[]) in
if vars = coerced_vars then (t2,cs,e)
else let e' = E_aux(E_case(e,[(Pat_aux(Pat_exp(P_aux(P_tup (List.map2
- (fun i t -> P_aux(P_id i,(l,(Some(([],t),Emp_local,[],pure_e)))))
- ids t1s),(l,Some(([],t1),Emp_local,[],pure_e))),
- E_aux(E_tuple coerced_vars,(l,Some(([],t2),Emp_local,cs,pure_e)))),
- (l,Some(([],t2),Emp_local,[],pure_e))))]),
- (l,(Some(([],t2),Emp_local,[],pure_e)))) in
+ (fun i t -> P_aux(P_id i,(l,(Base(([],t),Emp_local,[],pure_e)))))
+ ids t1s),(l,Base(([],t1),Emp_local,[],pure_e))),
+ E_aux(E_tuple coerced_vars,(l,Base(([],t2),Emp_local,cs,pure_e)))),
+ (l,Base(([],t2),Emp_local,[],pure_e))))]),
+ (l,(Base(([],t2),Emp_local,[],pure_e)))) in
(t2,csp@cs,e')
else eq_error l ("Found a tuple of length " ^ (string_of_int tl1) ^ " but expected a tuple of length " ^ (string_of_int tl2))
| Tapp(id1,args1),Tapp(id2,args2) ->
@@ -917,19 +942,19 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
| _,_ -> equate_o o1 o2);
let cs = csp@[Eq(co,r1,r2)] in
let t',cs' = type_consistent co d_env t1i t2i in
- let tannot = Some(([],t2),Emp_local,cs@cs',pure_e) in
- let e' = E_aux(E_internal_cast ((l,(Some(([],t2),Emp_local,[],pure_e))),e),(l,tannot)) in
+ let tannot = Base(([],t2),Emp_local,cs@cs',pure_e) in
+ let e' = E_aux(E_internal_cast ((l,(Base(([],t2),Emp_local,[],pure_e))),e),(l,tannot)) in
(t2,cs@cs',e'))
| "vector","range" ->
(match args1,args2 with
| [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
[TA_nexp b2;TA_nexp r2;] ->
let cs = [Eq(co,b2,{nexp=Nconst 0});GtEq(co,{nexp=Nadd(b2,r2)},{nexp=N2n r1})] in
- (t2,cs,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Some(([],t2),External None,cs,pure_e))))
+ (t2,cs,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Base(([],t2),External None,cs,pure_e))))
| [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
[TA_nexp b2;TA_nexp r2;] ->
let cs = [Eq(co,b2,{nexp=Nconst 0});GtEq(co,{nexp=Nadd(b2,r2)},{nexp=N2n r1})] in
- (t2,cs,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Some(([],t2),External None,cs,pure_e))))
+ (t2,cs,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Base(([],t2),External None,cs,pure_e))))
| [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ ->
eq_error l "Cannot convert a vector to an range without an order"
| [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ ->
@@ -940,11 +965,11 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
| [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
[TA_nexp b2;TA_nexp r2;] ->
let cs = [LtEq(co,{nexp=Nadd(b2,r2)},{nexp=N2n r1})] in
- (t2,cs,E_aux(E_app((Id_aux(Id "to_vec_inc",l)),[e]),(l,Some(([],t2),External None,cs,pure_e))))
+ (t2,cs,E_aux(E_app((Id_aux(Id "to_vec_inc",l)),[e]),(l,Base(([],t2),External None,cs,pure_e))))
| [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
[TA_nexp b2;TA_nexp r2;] ->
let cs = [LtEq(co,{nexp=Nadd(b2,r2)},{nexp=N2n r1})] in
- (t2,cs,E_aux(E_app((Id_aux(Id "to_vec_dec",l)),[e]),(l,Some(([],t2),External None,cs,pure_e))))
+ (t2,cs,E_aux(E_app((Id_aux(Id "to_vec_dec",l)),[e]),(l,Base(([],t2),External None,cs,pure_e))))
| [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ ->
eq_error l "Cannot convert an range to a vector without an order"
| [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ ->
@@ -955,7 +980,7 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
| [TA_typ t] ->
(*TODO Should this be an internal cast? Probably, make sure it doesn't interfere with the other internal cast and get removed *)
(*let _ = Printf.printf "Adding cast to remove register read\n" in*)
- let new_e = E_aux(E_cast(t_to_typ unit_t,e),(l,Some(([],t),External None,[],(add_effect (BE_aux(BE_rreg, l)) pure_e)))) in
+ let new_e = E_aux(E_cast(t_to_typ unit_t,e),(l,Base(([],t),External None,[],(add_effect (BE_aux(BE_rreg, l)) pure_e)))) in
type_coerce co d_env t new_e t2
| _ -> raise (Reporting_basic.err_unreachable l "register is not properly kinded"))
| _,_ ->
@@ -963,41 +988,41 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
| Tid("bit"),Tapp("vector",[TA_nexp {nexp=Nconst i};TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]) ->
let cs = [Eq(co,r1,{nexp = Nconst 1})] in
let t2' = {t = Tapp("vector",[TA_nexp {nexp=Nconst i};TA_nexp {nexp=Nconst 1};TA_ord o;TA_typ {t=Tid "bit"}])} in
- (t2',cs,E_aux(E_vector_indexed [(i,e)],(l,Some(([],t2),Emp_local,cs,pure_e))))
+ (t2',cs,E_aux(E_vector_indexed [(i,e)],(l,Base(([],t2),Emp_local,cs,pure_e))))
| Tapp("vector",[TA_nexp ({nexp=Nconst i} as b1);TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]),Tid("bit") ->
let cs = [Eq(co,r1,{nexp = Nconst 1})] in
(t2,cs,E_aux((E_vector_access (e,(E_aux(E_lit(L_aux(L_num i,l)),
- (l,Some(([],{t=Tapp("range",[TA_nexp b1;TA_nexp {nexp=Nconst 0}])}),Emp_local,cs,pure_e)))))),
- (l,Some(([],t2),Emp_local,cs,pure_e))))
+ (l,Base(([],{t=Tapp("range",[TA_nexp b1;TA_nexp {nexp=Nconst 0}])}),Emp_local,cs,pure_e)))))),
+ (l,Base(([],t2),Emp_local,cs,pure_e))))
| Tid("bit"),Tapp("range",[TA_nexp b1;TA_nexp r1]) ->
let t',cs'= type_consistent co d_env {t=Tapp("range",[TA_nexp{nexp=Nconst 0};TA_nexp{nexp=Nconst 1}])} t2 in
- (t2,cs',E_aux(E_case (e,[Pat_aux(Pat_exp(P_aux(P_lit(L_aux(L_zero,l)),(l,Some(([],t1),Emp_local,[],pure_e))),
- E_aux(E_lit(L_aux(L_num 0,l)),(l,Some(([],t2),Emp_local,[],pure_e)))),
- (l,Some(([],t2),Emp_local,[],pure_e)));
- Pat_aux(Pat_exp(P_aux(P_lit(L_aux(L_one,l)),(l,Some(([],t1),Emp_local,[],pure_e))),
- E_aux(E_lit(L_aux(L_num 1,l)),(l,Some(([],t2),Emp_local,[],pure_e)))),
- (l,Some(([],t2),Emp_local,[],pure_e)));]),
- (l,Some(([],t2),Emp_local,[],pure_e))))
+ (t2,cs',E_aux(E_case (e,[Pat_aux(Pat_exp(P_aux(P_lit(L_aux(L_zero,l)),(l,Base(([],t1),Emp_local,[],pure_e))),
+ E_aux(E_lit(L_aux(L_num 0,l)),(l,Base(([],t2),Emp_local,[],pure_e)))),
+ (l,Base(([],t2),Emp_local,[],pure_e)));
+ Pat_aux(Pat_exp(P_aux(P_lit(L_aux(L_one,l)),(l,Base(([],t1),Emp_local,[],pure_e))),
+ E_aux(E_lit(L_aux(L_num 1,l)),(l,Base(([],t2),Emp_local,[],pure_e)))),
+ (l,Base(([],t2),Emp_local,[],pure_e)));]),
+ (l,Base(([],t2),Emp_local,[],pure_e))))
| Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tid("bit") ->
let t',cs'= type_consistent co d_env t1 {t=Tapp("range",[TA_nexp{nexp=Nconst 0};TA_nexp{nexp=Nconst 1}])}
- in (t2,cs',E_aux(E_if(E_aux(E_app(Id_aux(Id "is_one",l),[e]),(l,Some(([],bool_t),External None,[],pure_e))),
- E_aux(E_lit(L_aux(L_one,l)),(l,Some(([],bit_t),Emp_local,[],pure_e))),
- E_aux(E_lit(L_aux(L_zero,l)),(l,Some(([],bit_t),Emp_local,[],pure_e)))),
- (l,Some(([],bit_t),Emp_local,cs',pure_e))))
+ in (t2,cs',E_aux(E_if(E_aux(E_app(Id_aux(Id "is_one",l),[e]),(l,Base(([],bool_t),External None,[],pure_e))),
+ E_aux(E_lit(L_aux(L_one,l)),(l,Base(([],bit_t),Emp_local,[],pure_e))),
+ E_aux(E_lit(L_aux(L_zero,l)),(l,Base(([],bit_t),Emp_local,[],pure_e)))),
+ (l,Base(([],bit_t),Emp_local,cs',pure_e))))
| Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tid(i) ->
(match Envmap.apply d_env.enum_env i with
| Some(enums) ->
(t2,[GtEq(co,b1,{nexp=Nconst 0});LtEq(co,r1,{nexp=Nconst (List.length enums)})],
E_aux(E_case(e,
List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_lit(L_aux((L_num i),l)),
- (l,Some(([],t1),Emp_local,[],pure_e))),
+ (l,Base(([],t1),Emp_local,[],pure_e))),
E_aux(E_id(Id_aux(Id a,l)),
- (l,Some(([],t2),Emp_local,[],pure_e)))),
- (l,Some(([],t2),Emp_local,[],pure_e)))) enums),
- (l,Some(([],t2),Emp_local,[],pure_e))))
+ (l,Base(([],t2),Emp_local,[],pure_e)))),
+ (l,Base(([],t2),Emp_local,[],pure_e)))) enums),
+ (l,Base(([],t2),Emp_local,[],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 None,[],pure_e))) in
+ let e' = E_aux(E_app((Id_aux(Id "is_one",l)),[e]),(l,Base(([],bool_t),External None,[],pure_e))) in
(t2,[],e')
| Tid(i),Tapp("range",[TA_nexp b1;TA_nexp r1;]) ->
(match Envmap.apply d_env.enum_env i with
@@ -1005,16 +1030,61 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
(t2,[Eq(co,b1,{nexp=Nconst 0});GtEq(co,r1,{nexp=Nconst (List.length enums)})],
E_aux(E_case(e,
List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_id(Id_aux(Id a,l)),
- (l,Some(([],t1),Emp_local,[],pure_e))),
+ (l,Base(([],t1),Emp_local,[],pure_e))),
E_aux(E_lit(L_aux((L_num i),l)),
- (l,Some(([],t2),Emp_local,[],pure_e)))),
- (l,Some(([],t2),Emp_local,[],pure_e)))) enums),
- (l,Some(([],t2),Emp_local,[],pure_e))))
+ (l,Base(([],t2),Emp_local,[],pure_e)))),
+ (l,Base(([],t2),Emp_local,[],pure_e)))) enums),
+ (l,Base(([],t2),Emp_local,[],pure_e))))
| None -> eq_error l ("Type mismatch: " ^ (t_to_string t1) ^ " , " ^ (t_to_string t2)))
| _,_ -> let t',cs = type_consistent co d_env t1 t2 in (t',cs,e)
and type_coerce co d_env t1 e t2 = type_coerce_internal co d_env t1 [] e t2 [];;
+let rec conforms_to_t spec actual =
+ match spec.t,actual.t with
+ | Tuvar _,_ -> true
+ | Ttup ss, Ttup acs -> (List.length ss == List.length acs) && List.for_all2 conforms_to_t ss acs
+ | Tid is, Tid ia -> is == ia
+ | Tapp(is,tas), Tapp(ia, taa) -> (is == ia) && (List.length tas == List.length taa) &&
+ List.for_all2 conforms_to_ta tas taa
+ | Tabbrev(_,s),a -> conforms_to_t s actual
+ | s,Tabbrev(_,a) -> conforms_to_t spec a
+ | _,_ -> false
+and conforms_to_ta spec actual =
+ match spec,actual with
+ | TA_typ s, TA_typ a -> conforms_to_t s a
+ | TA_nexp s, TA_nexp a -> conforms_to_n s a
+ | TA_ord s, TA_ord a -> conforms_to_o s a
+ | TA_eft s, TA_eft a -> conforms_to_e s a
+and conforms_to_n spec actual =
+ match spec.nexp,actual.nexp with
+ | Nuvar _,_ -> true
+ | Nconst si,Nconst ai -> si==ai
+ | _,_ -> false
+and conforms_to_o spec actual =
+ match spec.order,actual.order with
+ | Ouvar _,_ | Oinc,Oinc | Odec,Odec -> true
+ | _,_ -> false
+and conforms_to_e spec actual =
+ match spec.effect,actual.effect with
+ | Euvar _,_ -> true
+ | _,Euvar _ -> false
+ | _,_ -> false
+
+let rec select_overload_variant d_env variants actual_type =
+ match variants with
+ | [] -> NoTyp
+ | NoTyp::variants | Overload _::variants -> select_overload_variant d_env variants actual_type
+ | Base((parms,t),tag,cs,ef)::variants ->
+ let t,cs,ef = subst parms t cs ef in
+ let t,cs' = get_abbrev d_env t in
+ (match t.t with
+ | Tfn(a,r,e) ->
+ if conforms_to_t a actual_type
+ then Base(([],t),tag,cs@cs',ef)
+ else select_overload_variant d_env variants actual_type
+ | _ -> assert false (*Turn into unreachable error*))
+
let rec in_constraint_env = function
| [] -> []
| InS(co,nexp,vals)::cs ->
@@ -1117,6 +1187,13 @@ let rec simple_constraint_check in_env cs =
else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires "
^ string_of_int i1 ^ " to be less than or equal to " ^ string_of_int i2)
| _,_ -> LtEq(co,n1',n2')::(check cs))
+ | CondCons(co,pats,exps):: cs ->
+ let pats' = check pats in
+ let exps' = check exps in
+ (match pats',exps' with
+ | [],[] -> check cs
+ | _,[] -> check cs
+ | _ -> CondCons(co,pats',exps')::(check cs))
| x::cs -> x::(check cs)
let rec resolve_in_constraints cs = cs
@@ -1138,28 +1215,29 @@ let resolve_constraints cs =
let check_tannot l annot constraints efs =
match annot with
- | Some((params,t),tag,cs,e) ->
+ | Base((params,t),tag,cs,e) ->
ignore(effects_eq (Specc l) efs e);
let params = Envmap.to_list (t_remove_unifications (Envmap.from_list params) t) in
(*let _ = Printf.printf "Checked tannot, t after removing uvars is %s\n" (t_to_string t) in *)
- Some((params,t),tag,cs,e)
- | None -> raise (Reporting_basic.err_unreachable l "check_tannot given the place holder annotation")
+ Base((params,t),tag,cs,e)
+ | NoTyp -> raise (Reporting_basic.err_unreachable l "check_tannot given the place holder annotation")
let tannot_merge co denv t_older t_newer =
match t_older,t_newer with
- | None,None -> None
- | None,_ -> t_newer
- | _,None -> t_older
- | Some((ps_o,t_o),tag_o,cs_o,ef_o),Some((ps_n,t_n),tag_n,cs_n,ef_n) ->
- match tag_o,tag_n with
+ | NoTyp,NoTyp -> NoTyp
+ | NoTyp,_ -> t_newer
+ | _,NoTyp -> t_older
+ | Base((ps_o,t_o),tag_o,cs_o,ef_o),Base((ps_n,t_n),tag_n,cs_n,ef_n) ->
+ (match tag_o,tag_n with
| Default,tag ->
(match t_n.t with
| Tuvar _ -> let t_o,cs_o,ef_o = subst ps_o t_o cs_o ef_o in
let t,_ = type_consistent co denv t_n t_o in
- Some(([],t),tag_n,cs_o,ef_o)
+ Base(([],t),tag_n,cs_o,ef_o)
| _ -> t_newer)
| Emp_local, Emp_local ->
let t,cs_b = type_consistent co denv t_n t_o in
- Some(([],t),Emp_local,cs_o@cs_n@cs_b,union_effects ef_o ef_n)
- | _,_ -> t_newer
+ Base(([],t),Emp_local,cs_o@cs_n@cs_b,union_effects ef_o ef_n)
+ | _,_ -> t_newer)
+ | Overload _, Overload _ -> t_newer
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 04c5bf9c..13c27386 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -76,11 +76,16 @@ type nexp_range =
| In of constraint_origin * string * int list
| InS of constraint_origin * nexp * int list (* This holds the given value for string after a substitution *)
| CondCons of constraint_origin * nexp_range list * nexp_range list (* Constraints from one path from a conditional (pattern or if) and the constraints from that conditional *)
+ | BranchCons of constraint_origin * nexp_range list (* CondCons constraints from all branches of a conditional; list should be all CondCons *)
val get_c_loc : constraint_origin -> Parse_ast.l
type t_params = (string * kind) list
-type tannot = ((t_params * t) * tag * nexp_range list * effect) option
+type tannot =
+ | NoTyp
+ | Base of (t_params * t) * tag * nexp_range list * effect
+ | Overload of tannot * tannot list (* First tannot is the most polymorphic version; the list includes all variants. All t to be Tfn *)
+(*type tannot = ((t_params * t) * tag * nexp_range list * effect) option*)
type 'a emap = 'a Envmap.t
type rec_kind = Record | Register
@@ -128,6 +133,8 @@ val get_abbrev : def_envs -> t -> (t * nexp_range list)
val eval_nexp : nexp -> nexp
val get_index : nexp -> int (*TEMPORARILY expose nindex through this for debugging purposes*)
+val select_overload_variant : def_envs -> tannot list -> t -> tannot
+
(*May raise an exception if a contradiction is found*)
val resolve_constraints : nexp_range list -> nexp_range list
(* whether to actually perform constraint resolution or not *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 20:10:15 +0000