diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/initial_check.ml | 1 | ||||
| -rw-r--r-- | src/parser.mly | 2 | ||||
| -rw-r--r-- | src/pretty_print.ml | 23 | ||||
| -rw-r--r-- | src/test/vectors.sail | 1 | ||||
| -rw-r--r-- | src/type_check.ml | 70 | ||||
| -rw-r--r-- | src/type_internal.ml | 14 | ||||
| -rw-r--r-- | src/type_internal.mli | 1 |
7 files changed, 77 insertions, 35 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index c6c08c67..b95bf279 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -341,6 +341,7 @@ and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) (match to_ast_fexps false k_env exps with | Some(fexps) -> E_record(fexps) | None -> E_block(List.map (to_ast_exp k_env) exps)) + | Parse_ast.E_nondet(exps) -> E_nondet(List.map (to_ast_exp k_env) exps) | Parse_ast.E_id(id) -> E_id(to_ast_id id) | Parse_ast.E_lit(lit) -> E_lit(to_ast_lit lit) | Parse_ast.E_cast(typ,exp) -> E_cast(to_ast_typ k_env typ, to_ast_exp k_env exp) diff --git a/src/parser.mly b/src/parser.mly index 0ee7093d..e1647642 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -528,6 +528,8 @@ npats: atomic_exp: | Lcurly semi_exps Rcurly { eloc (E_block $2) } + | Nondet Lcurly semi_exps Rcurly + { eloc (E_nondet $3) } | id { eloc (E_id($1)) } | lit diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 10cd2b68..0544c573 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -107,6 +107,7 @@ and pp_format_base_effect_lem (BE_aux(e,l)) = | BE_wreg -> "BE_wreg" | BE_rmem -> "BE_rmem" | BE_wmem -> "BE_wmem" + | BE_barr -> "BE_barr" | BE_undef -> "BE_undef" | BE_unspec -> "BE_unspec" | BE_nondet -> "BE_nondet") ^ " " ^ @@ -208,6 +209,7 @@ let rec pp_format_t t = | Tapp(i,args) -> "(T_app \"" ^ i ^ "\" (T_args [" ^ list_format "; " pp_format_targ args ^ "]))" | Tabbrev(ti,ta) -> "(T_abbrev " ^ (pp_format_t ti) ^ " " ^ (pp_format_t ta) ^ ")" | Tuvar(_) -> "(T_var (Kid_aux (Var \"fresh_v\") Unknown))" + | Toptions _ -> "(T_var \"fresh_v\" Unknown)" and pp_format_targ = function | TA_typ t -> "(T_arg_typ " ^ pp_format_t t ^ ")" | TA_nexp n -> "(T_arg_nexp " ^ pp_format_n n ^ ")" @@ -224,6 +226,8 @@ and pp_format_n n = | N2n(n,None) -> "(Ne_exp " ^ (pp_format_n n) ^ ")" | Nneg n -> "(Ne_unary " ^ (pp_format_n n) ^ ")" | Nuvar _ -> "(Ne_var \"fresh_v_" ^ string_of_int (get_index n) ^ "\")" + | Nneg_inf -> "(Ne_unary Ne_inf)" + | Npow _ -> "power_not_implemented" and pp_format_e e = "(Effect_aux " ^ (match e.effect with @@ -260,7 +264,7 @@ let rec pp_format_nes nes = | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) -> "(Nec_in \"" ^ i ^ "\" [" ^ (list_format "; " string_of_int ns)^ "])" - | InS(_,{nexp = Nuvar _},ns) -> + | InS(_,_,ns) -> "(Nec_in \"fresh\" [" ^ (list_format "; " string_of_int ns)^ "])" | CondCons(_,nes_c,nes_t) -> "(Nec_cond " ^ (pp_format_nes nes_c) ^ " " ^ (pp_format_nes nes_t) ^ ")" @@ -319,6 +323,10 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = kwd "(E_block" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")" pp_lem_l l pp_annot annot + | E_nondet(exps) -> fprintf ppf "@[<0>(E_aux %a [%a] %a (%a, %a))@]" + kwd "(E_nondet" + (list_pp pp_semi_lem_exp pp_lem_exp) exps + kwd ")" pp_lem_l l pp_annot 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 @@ -369,11 +377,12 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = | E_internal_exp (l, Base((_,t),_,_,_)) -> (match t.t with | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) -> - match r.nexp with - | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" - kwd (string_of_big_int bi) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e))) - (* Should be unreachable *) - | E_internal_cast ((_, Overload (_,_, _)), _) | E_internal_exp _ -> assert false + (match r.nexp with + | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" + kwd (string_of_big_int bi) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e)) + | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given vector without known length")) + | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given non-vector")) + | E_internal_cast ((_, Overload (_,_, _)), _) | E_internal_exp _ -> raise (Reporting_basic.err_unreachable l "Found internal cast or exp with overload") in print_e ppf e @@ -549,6 +558,7 @@ let doc_effect (BE_aux (e,_)) = | BE_wreg -> "wreg" | BE_rmem -> "rmem" | BE_wmem -> "wmem" + | BE_barr -> "barr" | BE_undef -> "undef" | BE_unspec -> "unspec" | BE_nondet -> "nondet") @@ -788,6 +798,7 @@ let doc_exp, doc_let = | E_block exps -> let exps_doc = separate_map (semi ^^ hardline) exp exps in surround 2 1 lbrace exps_doc rbrace +(* XXX Need to add E_nondet, not sure how to put the nondet in front of the block *) | E_id id -> doc_id id | E_lit lit -> doc_lit lit | E_cast(typ,e) -> prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp e)) diff --git a/src/test/vectors.sail b/src/test/vectors.sail index 79f3bf23..a861b65c 100644 --- a/src/test/vectors.sail +++ b/src/test/vectors.sail @@ -17,6 +17,7 @@ let (vector<0,3,inc,(register<(bit[10])>)>) gpr_small = [slice_check,slice_check let (bit[3]) indexed = [0=1,1=1,2=0] let (bit[50]) partial = [0 = 0, 5=1, 32=0; default = 0] +let (bit[50]) partial_unspec = [0=0, 4=0, 7=1, 49=1] function unit decode ([bitzero, bitzero, bitone, bitzero]) = match_success := 1 and decode x = match_success := x diff --git a/src/type_check.ml b/src/type_check.ml index 739cb6d6..73055541 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -42,7 +42,6 @@ let rec fields_to_rec fields rec_env = | None -> fields_to_rec fields rec_env else fields_to_rec fields rec_env -(*No checks necessary, unlike conversion in initial_check*) let kind_to_k (K_aux((K_kind baseks),l)) = let bk_to_k (BK_aux(bk,l')) = match bk with @@ -65,6 +64,7 @@ let rec typ_to_t (Typ_aux(typ,l)) = | Typ_fn (ty1,ty2,e) -> {t = Tfn (typ_to_t ty1,typ_to_t ty2,aeffect_to_effect e)} | Typ_tup(tys) -> {t = Ttup (List.map typ_to_t tys) } | Typ_app(i,args) -> {t = Tapp (id_to_string i,List.map typ_arg_to_targ args) } + | Typ_wild -> new_t () and typ_arg_to_targ (Typ_arg_aux(ta,l)) = match ta with | Typ_arg_nexp n -> TA_nexp (anexp_to_nexp n) @@ -246,14 +246,14 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) let (fst,lst) = (List.hd is),(List.hd (List.rev is)) in let inc_or_dec = if fst < lst then - (let is_increasing = List.fold_left + (let _ = List.fold_left (fun i1 i2 -> if i1 < i2 then i2 - else typ_error l "Indexed vector access was inconsistently increasing") fst (List.tl is) in + else typ_error l "Indexed vector pattern was inconsistently increasing") fst (List.tl is) in true) else if lst < fst then - (let is_decreasing = List.fold_left + (let _ = List.fold_left (fun i1 i2 -> if i1 > i2 then i2 - else typ_error l "Indexed vector access was inconsistently decreasing") fst (List.tl is) in + else typ_error l "Indexed vector pattern was inconsistently decreasing") fst (List.tl is) in false) else typ_error l "Indexed vector cannot be determined as either increasing or decreasing" in let base,rise = new_n (), new_n () in @@ -339,10 +339,14 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let Env(d_env,t_env) = envs in let rebuild annot = E_aux(e,(l,annot)) in match e with - | E_block(exps) -> + | E_block exps -> let (exps',annot',t_env',sc,t,ef) = check_block t_env envs expect_t exps in (E_aux(E_block(exps'),(l,annot')),t, t_env',sc,ef) - | E_id(id) -> + | E_nondet exps -> + let checked_exps = List.map (check_exp envs unit_t) exps in + let (exps',annot',t_env',sc,t,ef) = check_block t_env envs expect_t exps in (* WRONG WRONG, place holder. Needs to be a map, intersection of envs, and each should return unit *) + (E_aux(E_nondet(exps'),(l,annot')),t,t_env,sc,ef) + | E_id id -> let i = id_to_string id in (match Envmap.apply t_env i with | Some(Base((params,t),Constructor,cs,ef)) -> @@ -661,21 +665,28 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp | _ -> new_t (),new_n (), new_n () in let first,last = fst (List.hd eis), fst (List.hd (List.rev eis)) in let is_increasing = first <= last in - let es,cs,effect,_ = (List.fold_right - (fun ((i,e),c,ef) (es,cs,effect,prev) -> + let es,cs,effect,contains_skip,_ = (List.fold_right + (fun ((i,e),c,ef) (es,cs,effect,skips,prev) -> (*let _ = Printf.printf "Checking increasing %b %i %i\n" is_increasing prev i in*) - if is_increasing - then if prev >= i then (((i,e)::es),(c@cs),union_effects ef effect,i) - else (typ_error l "Indexed vector is not consistently increasing") - else if i >= prev then (((i,e)::es),(c@cs),union_effects ef effect,i) - else (typ_error l "Indexed vector is not consistently decreasing")) + let (esn, csn, efn) = (((i,e)::es), (c@cs), union_effects ef effect) in + if (is_increasing && prev > i) + then (esn,csn,efn,(((prev-i) > 1) || skips),i) + else if prev < i + then (esn,csn,efn,(((i-prev) > 1) || skips),i) + else if i = prev + then (typ_error l ("Indexed vector contains a duplicate definition of index " ^ (string_of_int i))) + else (typ_error l ("Indexed vector is not consistently " ^ (if is_increasing then "increasing" else "decreasing")))) (List.map (fun (i,e) -> let (e,_,_,cs,eft) = (check_exp envs item_t e) in ((i,e),cs,eft)) - eis) ([],[],pure_e,last)) in - let (default',fully_enumerate,cs_d,ef_d) = match default with - | Def_val_empty -> (Def_val_aux(Def_val_empty,(ld,Base(([],item_t),Emp_local,[],pure_e))),true,[],pure_e) - | Def_val_dec e -> let (de,t,_,cs_d,ef_d) = (check_exp envs item_t e) in - (*Check that ef_d doesn't write to memory or registers? *) - (Def_val_aux(Def_val_dec de,(ld,(Base(([],item_t),Emp_local,cs_d,ef_d)))),false,cs_d,ef_d) in + eis) ([],[],pure_e,false,(if is_increasing then (last+1) else (last-1)))) in + let (default',fully_enumerate,cs_d,ef_d) = match (default,contains_skip) with + | (Def_val_empty,false) -> (Def_val_aux(Def_val_empty,(ld,Base(([],item_t),Emp_local,[],pure_e))),true,[],pure_e) + | (Def_val_empty,true) -> + let ef = add_effect (BE_aux(BE_unspec,l)) pure_e in + (Def_val_aux(Def_val_dec ( (E_aux( E_lit( L_aux(L_undef, l)), (l, (Base(([],item_t),Emp_local,[],ef)))))), + (l,Base(([],item_t),Emp_local,[],pure_e))),false,[],ef) + | (Def_val_dec e,_) -> let (de,t,_,cs_d,ef_d) = (check_exp envs item_t e) in + (*Check that ef_d doesn't write to memory or registers? *) + (Def_val_aux(Def_val_dec de,(ld,(Base(([],item_t),Emp_local,cs_d,ef_d)))),false,cs_d,ef_d) in let (base_bound,length_bound,cs_bounds) = if fully_enumerate then ({nexp=Nconst (big_int_of_int first)},{nexp = Nconst (big_int_of_int (List.length eis))},[]) @@ -847,6 +858,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp match lookup_field_type i r with | NoTyp -> typ_error l ("Expected a struct of type " ^ n ^ ", which should not have a field " ^ i) + | Overload _ -> raise (Reporting_basic.err_unreachable l "Field given overload tannot") | 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 @@ -866,6 +878,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let i = id_to_string id in match lookup_field_type i r with | NoTyp -> raise (Reporting_basic.err_unreachable l "field_match didn't have a full match") + | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot") | 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 @@ -892,6 +905,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp match lookup_field_type fi r with | NoTyp -> typ_error l ("Expected a struct with type " ^ i ^ ", which does not have a field " ^ fi) + | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot") | 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 @@ -911,6 +925,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let i = id_to_string id in match lookup_field_type i r with | NoTyp -> raise (Reporting_basic.err_unreachable l "field_match didn't have a full match") + | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot") | 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 @@ -933,6 +948,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp (match lookup_field_type fi r with | NoTyp -> typ_error l ("Type " ^ i ^ " does not have a field " ^ fi) + | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot") | 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 false et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef)))) expect_t in @@ -945,6 +961,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp (match lookup_field_type fi r with | NoTyp -> typ_error l ("Type " ^ i ^ " does not have a field " ^ fi) + | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot") | 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 false et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef)))) expect_t in @@ -958,11 +975,13 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp (match lookup_field_type fi r with | NoTyp -> raise (Reporting_basic.err_unreachable l "lookup_possible_records returned a record that didn't include the field") + | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot") | 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 false 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; + equate_t t' {t=Tid i}; + (*TODO tHIS should be equate_t + t'.t <- Tid i;*) (acc,et',t_env,cs@c',ef)) | records -> typ_error l ("Multiple structs contain field " ^ fi ^ ", try adding a cast to disambiguate")) | _ -> typ_error l ("Expected a struct or register for access but found an expression of type " ^ t_to_string t')) @@ -986,6 +1005,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp 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,(Base(([],unit_t),tag,[],ef)))),unit_t,t_env',cs@cs'@c',union_effects ef ef') + | E_internal_cast _ | E_internal_exp _ -> raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker") 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 @@ -1185,11 +1205,12 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan | Tid i | Tabbrev({t=Tid i},_) -> (match lookup_record_typ i d_env.rec_env with | None -> typ_error l ("Expected a register or struct for this update, instead found an expression with type " ^ i) - | Some(((i,rec_kind,fields) as r)) -> + | Some(((i,rec_kind,fields) as r)) -> let fi = id_to_string id in (match lookup_field_type fi r with | NoTyp -> typ_error l ("Type " ^ i ^ " does not have a field " ^ fi) + | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot") | Base((params,et),_,cs,_) -> let et,cs,ef = subst params et cs ef in (LEXP_aux(LEXP_field(vec',id),(l,(Base(([],vec_t),tag,csi@cs,ef)))),et,env,tag,csi@cs,ef))) @@ -1377,7 +1398,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, | Some(Base( (params,u),Spec,constraints,eft)), Base( (p',t),_,c',eft') -> (*let _ = Printf.eprintf "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 + let _,cs = type_consistent (Specc l) d_env t u in let t_env = if is_rec then t_env else Envmap.remove t_env id in let funcls,cs_ef = check t_env in let cs,ef = ((fun (cses,efses) -> (List.concat cses),(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in @@ -1413,6 +1434,7 @@ let check_def envs def = let i = id_to_string id 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)))) + | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Unknown "Scattered given to type checker") (*val check : envs -> tannot defs -> tannot defs*) diff --git a/src/type_internal.ml b/src/type_internal.ml index 0d3f467b..134aa2c4 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -164,6 +164,7 @@ and ef_to_string (Ast.BE_aux(b,l)) = | Ast.BE_wreg -> "wreg" | Ast.BE_rmem -> "rmem" | Ast.BE_wmem -> "wmem" + | Ast.BE_barr -> "barr" | Ast.BE_undef -> "undef" | Ast.BE_unspec-> "unspec" | Ast.BE_nondet-> "nondet" @@ -1214,6 +1215,9 @@ let compare_effect (BE_aux(e1,_)) (BE_aux(e2,_)) = | (BE_wmem,BE_wmem) -> 0 | (BE_wmem,_) -> -1 | (_,BE_wmem) -> 1 + | (BE_barr,BE_barr) -> 0 + | (BE_barr,_) -> 1 + | (_,BE_barr) -> -1 | (BE_undef,BE_undef) -> 0 | (BE_undef,_) -> -1 | (_,BE_undef) -> 1 @@ -1309,7 +1313,7 @@ and conforms_to_e loosely spec actual = match (spec.effect,actual.effect,loosely) with | (Euvar _,_,true) -> true | (_,Euvar _,true) -> false - | (_,_,true) -> false (*Should check actual effect equality, using existing function*) + | _ -> false (*Should check actual effect equality, using existing function*) (*Is checking for structural equality amongst the types, building constraints for kind Nat. When considering two range type applications, will check for consistency instead of equality*) @@ -1342,7 +1346,7 @@ let rec type_consistent_internal co d_env t1 cs1 t2 cs2 = | Tfn(tin1,tout1,effect1),Tfn(tin2,tout2,effect2) -> let (tin,cin) = type_consistent co d_env tin1 tin2 in let (tout,cout) = type_consistent co d_env tout1 tout2 in - let effect = effects_eq co effect1 effect2 in + let _ = effects_eq co effect1 effect2 in (t2,csp@cin@cout) | Ttup t1s, Ttup t2s -> (t2,csp@(List.flatten (List.map snd (List.map2 (type_consistent co d_env) t1s t2s)))) @@ -1354,7 +1358,7 @@ let rec type_consistent_internal co d_env t1 cs1 t2 cs2 = let b2,r2 = new_n (), new_n () in let t2' = {t=Tapp("range",[TA_nexp b2;TA_nexp r2])} in equate_t t2 t2'; - (t2,csp@[GtEq(co,b,b2);LtEq(co,r,r2)]) (*This and above should maybe be In constraints when co is patt and tuvar is an in*) + (t2,csp@[GtEq(co,b,b2);LtEq(co,r,r2)]) | t,Tuvar _ -> equate_t t2 t1; (t1,csp) | _,_ -> eq_error l ("Type mismatch found " ^ (t_to_string t1) ^ " but expected a " ^ (t_to_string t2)) @@ -1698,7 +1702,7 @@ let check_tannot l annot constraints efs = (*let _ = Printf.printf "Checked tannot, t after removing uvars is %s\n" (t_to_string t) in *) Base((params,t),tag,cs,e) | NoTyp -> raise (Reporting_basic.err_unreachable l "check_tannot given the place holder annotation") - + | Overload _ -> raise (Reporting_basic.err_unreachable l "check_tannot given overload") let tannot_merge co denv t_older t_newer = match t_older,t_newer with @@ -1717,4 +1721,4 @@ let tannot_merge co denv t_older t_newer = let t,cs_b = type_consistent co denv t_n t_o in Base(([],t),Emp_local,cs_o@cs_n@cs_b,union_effects ef_o ef_n) | _,_ -> t_newer) - | Overload _, Overload _ -> t_newer + | _ -> t_newer diff --git a/src/type_internal.mli b/src/type_internal.mli index 5203f51e..bb530896 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -136,6 +136,7 @@ val new_t : unit -> t val new_n : unit -> nexp val new_o : unit -> order val new_e : unit -> effect +val equate_t : t -> t -> unit val subst : (string * kind) list -> t -> nexp_range list -> effect -> t * nexp_range list * effect val get_abbrev : def_envs -> t -> (t * nexp_range list) |