diff options
| -rw-r--r-- | src/rewriter.ml | 294 | ||||
| -rw-r--r-- | src/rewriter.mli | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 2032 | ||||
| -rw-r--r-- | src/type_internal.ml | 373 | ||||
| -rw-r--r-- | src/type_internal.mli | 10 |
5 files changed, 1451 insertions, 1260 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml index 6d2d9417..1682710a 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -19,200 +19,208 @@ let rec rewrite_nexp_to_exp program_vars l nexp = match nexp.nexp with | Nconst i -> E_aux (E_lit (L_aux (L_num (int_of_big_int i),l)), (l,simple_annot typ)) | Nadd (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "+",l)),rewrite n2), - (l, (tag_annot typ (External (Some "add"))))) + (l, (tag_annot typ (External (Some "add"))))) | Nmult (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "*",l)),rewrite n2), - (l, tag_annot typ (External (Some "multiply")))) + (l, tag_annot typ (External (Some "multiply")))) | Nsub (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "-",l)),rewrite n2), - (l, tag_annot typ (External (Some "minus")))) + (l, tag_annot typ (External (Some "minus")))) | N2n (n, _) -> E_aux (E_app_infix (E_aux (E_lit (L_aux (L_num 2,l)), (l, simple_annot (mk_atom_typ n_two))), - (Id_aux (Id "**",l)), - rewrite n), (l, tag_annot typ (External (Some "power")))) + (Id_aux (Id "**",l)), + rewrite n), (l, tag_annot typ (External (Some "power")))) | Npow(n,i) -> E_aux (E_app_infix - (rewrite n, (Id_aux (Id "**",l)), - E_aux (E_lit (L_aux (L_num i,l)), - (l, simple_annot (mk_atom_typ (mk_c_int i))))), - (l, tag_annot typ (External (Some "power")))) + (rewrite n, (Id_aux (Id "**",l)), + E_aux (E_lit (L_aux (L_num i,l)), + (l, simple_annot (mk_atom_typ (mk_c_int i))))), + (l, tag_annot typ (External (Some "power")))) | Nneg(n) -> E_aux (E_app_infix (E_aux (E_lit (L_aux (L_num 0,l)), (l, simple_annot (mk_atom_typ n_zero))), - (Id_aux (Id "-",l)), - rewrite n), - (l, tag_annot typ (External (Some "minus")))) + (Id_aux (Id "-",l)), + rewrite n), + (l, tag_annot typ (External (Some "minus")))) | Nvar v -> (*TODO these need to generate an error as it's a place where there's insufficient specification. - But, for now I need to permit this to make power.sail compile, and most errors are in trap - or vectors *) - (*let _ = Printf.eprintf "unbound variable here %s\n" v in*) - E_aux (E_id (Id_aux (Id v,l)),(l,simple_annot typ)) + But, for now I need to permit this to make power.sail compile, and most errors are in trap + or vectors *) + (*let _ = Printf.eprintf "unbound variable here %s\n" v in*) + E_aux (E_id (Id_aux (Id v,l)),(l,simple_annot typ)) | _ -> raise (Reporting_basic.err_unreachable l ("rewrite_nexp given n that can't be rewritten: " ^ (n_to_string nexp))) in match program_vars with | None -> actual_rewrite_n nexp | Some program_vars -> (match partial_assoc nexp_eq_check nexp program_vars with - | None -> actual_rewrite_n nexp - | Some(None,ev) -> - (*let _ = Printf.eprintf "var case of rewrite, %s\n" ev in*) - E_aux (E_id (Id_aux (Id ev,l)), (l, simple_annot typ)) - | Some(Some f,ev) -> - E_aux (E_app ((Id_aux (Id f,l)), [ (E_aux (E_id (Id_aux (Id ev,l)), (l,simple_annot typ)))]), - (l, tag_annot typ (External (Some f))))) + | None -> actual_rewrite_n nexp + | Some(None,ev) -> + (*let _ = Printf.eprintf "var case of rewrite, %s\n" ev in*) + E_aux (E_id (Id_aux (Id ev,l)), (l, simple_annot typ)) + | Some(Some f,ev) -> + E_aux (E_app ((Id_aux (Id f,l)), [ (E_aux (E_id (Id_aux (Id ev,l)), (l,simple_annot typ)))]), + (l, tag_annot typ (External (Some f))))) let rec match_to_program_vars ns bounds = match ns with | [] -> [] | n::ns -> match find_var_from_nexp n bounds with - | None -> match_to_program_vars ns bounds - | Some(augment,ev) -> - (*let _ = Printf.eprintf "adding n %s to program var %s\n" (n_to_string n) ev in*) - (n,(augment,ev))::(match_to_program_vars ns bounds) + | None -> match_to_program_vars ns bounds + | Some(augment,ev) -> + (*let _ = Printf.eprintf "adding n %s to program var %s\n" (n_to_string n) ev in*) + (n,(augment,ev))::(match_to_program_vars ns bounds) -let rec rewrite_exp (E_aux (exp,(l,annot))) = +let rec rewrite_exp nmap (E_aux (exp,(l,annot))) = let rewrap e = E_aux (e,(l,annot)) in + let rewrite = rewrite_exp nmap in match exp with - | E_block exps -> rewrap (E_block (List.map rewrite_exp exps)) - | E_nondet exps -> rewrap (E_nondet (List.map rewrite_exp exps)) + | E_block exps -> rewrap (E_block (List.map rewrite exps)) + | E_nondet exps -> rewrap (E_nondet (List.map rewrite exps)) | E_id _ | E_lit _ -> rewrap exp - | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite_exp exp)) - | E_app (((Id_aux ((Id name),_)) as id),exps) -> rewrap (E_app (id,List.map rewrite_exp exps)) - | E_app_infix(el,id,er) -> rewrap (E_app_infix(rewrite_exp el,id,rewrite_exp er)) - | E_tuple exps -> rewrap (E_tuple (List.map rewrite_exp exps)) - | E_if (c,t,e) -> rewrap (E_if (rewrite_exp c,rewrite_exp t, rewrite_exp e)) + | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite exp)) + | E_app (id,exps) -> rewrap (E_app (id,List.map rewrite exps)) + | E_app_infix(el,id,er) -> rewrap (E_app_infix(rewrite el,id,rewrite er)) + | E_tuple exps -> rewrap (E_tuple (List.map rewrite exps)) + | E_if (c,t,e) -> rewrap (E_if (rewrite c,rewrite t, rewrite e)) | E_for (id, e1, e2, e3, o, body) -> - rewrap (E_for (id, rewrite_exp e1, rewrite_exp e2, rewrite_exp e3, o, rewrite_exp body)) - | E_vector exps -> rewrap (E_vector (List.map rewrite_exp exps)) + rewrap (E_for (id, rewrite e1, rewrite e2, rewrite e3, o, rewrite body)) + | E_vector exps -> rewrap (E_vector (List.map rewrite exps)) | E_vector_indexed (exps,(Def_val_aux(default,dannot))) -> let def = match default with - | Def_val_empty -> default - | Def_val_dec e -> Def_val_dec (rewrite_exp e) in - rewrap (E_vector_indexed (List.map (fun (i,e) -> (i, rewrite_exp e)) exps, Def_val_aux(def,dannot))) - | E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite_exp vec,rewrite_exp index)) + | Def_val_empty -> default + | Def_val_dec e -> Def_val_dec (rewrite e) in + rewrap (E_vector_indexed (List.map (fun (i,e) -> (i, rewrite e)) exps, Def_val_aux(def,dannot))) + | E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite vec,rewrite index)) | E_vector_subrange (vec,i1,i2) -> - rewrap (E_vector_subrange (rewrite_exp vec,rewrite_exp i1,rewrite_exp i2)) + rewrap (E_vector_subrange (rewrite vec,rewrite i1,rewrite i2)) | E_vector_update (vec,index,new_v) -> - rewrap (E_vector_update (rewrite_exp vec,rewrite_exp index,rewrite_exp new_v)) + rewrap (E_vector_update (rewrite vec,rewrite index,rewrite new_v)) | E_vector_update_subrange (vec,i1,i2,new_v) -> - rewrap (E_vector_update_subrange (rewrite_exp vec,rewrite_exp i1,rewrite_exp i2,rewrite_exp new_v)) - | E_vector_append (v1,v2) -> rewrap (E_vector_append (rewrite_exp v1,rewrite_exp v2)) - | E_list exps -> rewrap (E_list (List.map rewrite_exp exps)) - | E_cons(h,t) -> rewrap (E_cons (rewrite_exp h,rewrite_exp t)) + rewrap (E_vector_update_subrange (rewrite vec,rewrite i1,rewrite i2,rewrite new_v)) + | E_vector_append (v1,v2) -> rewrap (E_vector_append (rewrite v1,rewrite v2)) + | E_list exps -> rewrap (E_list (List.map rewrite exps)) + | E_cons(h,t) -> rewrap (E_cons (rewrite h,rewrite t)) | E_record (FES_aux (FES_Fexps(fexps, bool),fannot)) -> rewrap (E_record - (FES_aux (FES_Fexps - (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) -> - FE_aux(FE_Fexp(id,rewrite_exp e),fannot)) fexps, bool), fannot))) + (FES_aux (FES_Fexps + (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) -> + FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps, bool), fannot))) | E_record_update (re,(FES_aux (FES_Fexps(fexps, bool),fannot))) -> - rewrap (E_record_update ((rewrite_exp re), - (FES_aux (FES_Fexps - (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) -> - FE_aux(FE_Fexp(id,rewrite_exp e),fannot)) fexps, bool), fannot)))) - | E_field(exp,id) -> rewrap (E_field(rewrite_exp exp,id)) + rewrap (E_record_update ((rewrite re), + (FES_aux (FES_Fexps + (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) -> + FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps, bool), fannot)))) + | E_field(exp,id) -> rewrap (E_field(rewrite exp,id)) | E_case (exp ,pexps) -> - rewrap (E_case (rewrite_exp exp, - (List.map - (fun (Pat_aux (Pat_exp(p,e),pannot)) -> - Pat_aux (Pat_exp(p,rewrite_exp e),pannot)) pexps))) - | E_let (letbind,body) -> rewrap (E_let(rewrite_let letbind,rewrite_exp body)) - | E_assign (lexp,exp) -> rewrap (E_assign(rewrite_lexp lexp,rewrite_exp exp)) - | E_exit e -> rewrap (E_exit (rewrite_exp e)) + rewrap (E_case (rewrite exp, + (List.map + (fun (Pat_aux (Pat_exp(p,e),pannot)) -> + Pat_aux (Pat_exp(p,rewrite e),pannot)) pexps))) + | E_let (letbind,body) -> rewrap (E_let(rewrite_let nmap letbind,rewrite body)) + | E_assign (lexp,exp) -> rewrap (E_assign(rewrite_lexp nmap lexp,rewrite exp)) + | E_exit e -> rewrap (E_exit (rewrite e)) | E_internal_cast ((_,casted_annot),exp) -> - let new_exp = rewrite_exp exp in + let new_exp = rewrite exp in (*let _ = Printf.eprintf "Removing an internal_cast with %s\n" (tannot_to_string casted_annot) in*) (match casted_annot,exp with - | Base((_,t),_,_,_,_),E_aux(ec,(ecl,Base((_,exp_t),_,_,_,_))) -> - (*let _ = Printf.eprintf "Considering removing an internal cast where the two types are %s and %s\n" (t_to_string t) (t_to_string exp_t) in*) - (match t.t,exp_t.t with - (*TODO should pass d_env into here so that I can look at the abbreviations if there are any here*) - | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]), - Tapp("vector",[TA_nexp n2;TA_nexp nw2;TA_ord o2;_]) - | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]), - Tapp("reg",[TA_typ {t=(Tapp("vector",[TA_nexp n2; TA_nexp nw2; TA_ord o2;_]))}]) -> - (match n1.nexp with - | Nconst i1 -> if nexp_eq n1 n2 then new_exp else rewrap (E_cast (t_to_typ t,new_exp)) - | _ -> (match o1.order with - | Odec -> - (*let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n" (n_to_string nw1) (n_to_string n1) (nexp_one_more_than nw1 n1) in*) - (*if nexp_one_more_than nw1 n1 - then *) rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Unknown)), Unknown), new_exp)) - (*else new_exp*) - | _ -> new_exp) - | _ -> new_exp) - | _ -> new_exp) - | Base((_,t),_,_,_,_),_ -> - (*let _ = Printf.eprintf "Considering removing an internal cast where the remaining type is %s\n%!" (t_to_string t) in*) - (match t.t with - | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]) -> - (match o1.order with - | Odec -> - (*let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n" (n_to_string nw1) (n_to_string n1) (nexp_one_more_than nw1 n1) in - if nexp_one_more_than nw1 n1 - then*) rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Unknown)), Unknown), new_exp)) - (*else new_exp*) - | _ -> new_exp) - | _ -> new_exp) - | _ -> (*let _ = Printf.eprintf "Not a base match?\n" in*) new_exp) + | Base((_,t),_,_,_,_),E_aux(ec,(ecl,Base((_,exp_t),_,_,_,_))) -> + (*let _ = Printf.eprintf "Considering removing an internal cast where the two types are %s and %s\n" (t_to_string t) (t_to_string exp_t) in*) + (match t.t,exp_t.t with + (*TODO should pass d_env into here so that I can look at the abbreviations if there are any here*) + | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]), + Tapp("vector",[TA_nexp n2;TA_nexp nw2;TA_ord o2;_]) + | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]), + Tapp("reg",[TA_typ {t=(Tapp("vector",[TA_nexp n2; TA_nexp nw2; TA_ord o2;_]))}]) -> + (match n1.nexp with + | Nconst i1 -> if nexp_eq n1 n2 then new_exp else rewrap (E_cast (t_to_typ t,new_exp)) + | _ -> (match o1.order with + | Odec -> + (*let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n" + (n_to_string nw1) (n_to_string n1) (nexp_one_more_than nw1 n1) in*) + rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"),Parse_ast.Unknown)), + Parse_ast.Unknown),new_exp)) + | _ -> new_exp)) + | _ -> new_exp) + | Base((_,t),_,_,_,_),_ -> + (*let _ = Printf.eprintf "Considering removing an internal cast where the remaining type is %s\n%!" + (t_to_string t) in*) + (match t.t with + | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]) -> + (match o1.order with + | Odec -> + (*let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n" + (n_to_string nw1) (n_to_string n1) (nexp_one_more_than nw1 n1) in*) + rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Parse_ast.Unknown)), + Parse_ast.Unknown), new_exp)) + | _ -> new_exp) + | _ -> new_exp) + | _ -> (*let _ = Printf.eprintf "Not a base match?\n" in*) new_exp) | E_internal_exp (l,impl) -> (match impl with - | Base((_,t),_,_,_,bounds) -> - (*let _ = Printf.eprintf "Rewriting internal expression, with type %s\n" (t_to_string t) in*) - (match t.t with - (*Old case; should possibly be removed*) - | Tapp("register",[TA_typ {t= Tapp("vector",[ _; TA_nexp r;_;_])}]) - | Tapp("vector", [_;TA_nexp r;_;_]) -> - (*let _ = Printf.eprintf "vector case with %s, bounds are %s\n" (n_to_string r) (bounds_to_string bounds) in*) - let nexps = expand_nexp r in - (match (match_to_program_vars nexps bounds) with - | [] -> rewrite_nexp_to_exp None l r - | map -> rewrite_nexp_to_exp (Some map) l r) - | Tapp("implicit", [TA_nexp i]) -> - (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*) - let nexps = expand_nexp i in - (match (match_to_program_vars nexps bounds) with - | [] -> rewrite_nexp_to_exp None l i - | map -> rewrite_nexp_to_exp (Some map) l i) - | _ -> - raise (Reporting_basic.err_unreachable l - ("Internal_exp given unexpected types " ^ (t_to_string t)))) - | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp given none Base annot"))) + | Base((_,t),_,_,_,bounds) -> + let bounds = match nmap with | None -> bounds | Some nm -> add_map_to_bounds nm bounds in + (*let _ = Printf.eprintf "Rewriting internal expression, with type %s\n" (t_to_string t) in*) + (match t.t with + (*Old case; should possibly be removed*) + | Tapp("register",[TA_typ {t= Tapp("vector",[ _; TA_nexp r;_;_])}]) + | Tapp("vector", [_;TA_nexp r;_;_]) -> + (*let _ = Printf.eprintf "vector case with %s, bounds are %s\n" + (n_to_string r) (bounds_to_string bounds) in*) + let nexps = expand_nexp r in + (match (match_to_program_vars nexps bounds) with + | [] -> rewrite_nexp_to_exp None l r + | map -> rewrite_nexp_to_exp (Some map) l r) + | Tapp("implicit", [TA_nexp i]) -> + (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*) + let nexps = expand_nexp i in + (match (match_to_program_vars nexps bounds) with + | [] -> rewrite_nexp_to_exp None l i + | map -> rewrite_nexp_to_exp (Some map) l i) + | _ -> + raise (Reporting_basic.err_unreachable l + ("Internal_exp given unexpected types " ^ (t_to_string t)))) + | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp given none Base annot"))) | E_internal_exp_user ((l,user_spec),(_,impl)) -> (match (user_spec,impl) with - | (Base((_,tu),_,_,_,_), Base((_,ti),_,_,_,bounds)) -> - (*let _ = Printf.eprintf "E_interal_user getting rewritten two types are %s and %s\n" (t_to_string tu) (t_to_string ti) in*) - (match (tu.t,ti.t) with - | (Tapp("implicit", [TA_nexp u]),Tapp("implicit",[TA_nexp i])) -> - (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*) - let nexps = expand_nexp i in - (match (match_to_program_vars nexps bounds) with - | [] -> rewrite_nexp_to_exp None l i - (*add u to program_vars env; for now it will work out properly by accident*) - | map -> rewrite_nexp_to_exp (Some map) l i) - | _ -> - raise (Reporting_basic.err_unreachable l - ("Internal_exp_user given unexpected types " ^ (t_to_string tu) ^ ", " ^ (t_to_string ti)))) - | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp_user given none Base annot"))) + | (Base((_,tu),_,_,_,_), Base((_,ti),_,_,_,bounds)) -> + (*let _ = Printf.eprintf "E_interal_user getting rewritten two types are %s and %s\n" + (t_to_string tu) (t_to_string ti) in*) + let bounds = match nmap with | None -> bounds | Some nm -> add_map_to_bounds nm bounds in + (match (tu.t,ti.t) with + | (Tapp("implicit", [TA_nexp u]),Tapp("implicit",[TA_nexp i])) -> + (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*) + let nexps = expand_nexp i in + (match (match_to_program_vars nexps bounds) with + | [] -> rewrite_nexp_to_exp None l i + (*add u to program_vars env; for now it will work out properly by accident*) + | map -> rewrite_nexp_to_exp (Some map) l i) + | _ -> + raise (Reporting_basic.err_unreachable l + ("Internal_exp_user given unexpected types " ^ (t_to_string tu) ^ ", " ^ (t_to_string ti)))) + | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp_user given none Base annot"))) -and rewrite_let (LB_aux(letbind,(l,annot))) = match letbind with +and rewrite_let map (LB_aux(letbind,(l,annot))) = + let map = merge_option_maps map (get_map_tannot annot) in + match letbind with | LB_val_explicit (typschm, pat,exp) -> - LB_aux(LB_val_explicit (typschm,pat, rewrite_exp exp),(l,annot)) + LB_aux(LB_val_explicit (typschm,pat, rewrite_exp map exp),(l,annot)) | LB_val_implicit ( pat, exp) -> - LB_aux(LB_val_implicit (pat,rewrite_exp exp),(l,annot)) + LB_aux(LB_val_implicit (pat,rewrite_exp map exp),(l,annot)) -and rewrite_lexp (LEXP_aux(lexp,(l,annot))) = +and rewrite_lexp map (LEXP_aux(lexp,(l,annot))) = let rewrap le = LEXP_aux(le,(l,annot)) in match lexp with | LEXP_id _ | LEXP_cast _ -> rewrap lexp - | LEXP_memory (id,exps) -> rewrap (LEXP_memory(id,List.map rewrite_exp exps)) - | LEXP_vector (lexp,exp) -> rewrap (LEXP_vector (rewrite_lexp lexp,rewrite_exp exp)) + | LEXP_memory (id,exps) -> rewrap (LEXP_memory(id,List.map (rewrite_exp map) exps)) + | LEXP_vector (lexp,exp) -> rewrap (LEXP_vector (rewrite_lexp map lexp,rewrite_exp map exp)) | LEXP_vector_range (lexp,exp1,exp2) -> - rewrap (LEXP_vector_range (rewrite_lexp lexp,rewrite_exp exp1,rewrite_exp exp2)) - | LEXP_field (lexp,id) -> rewrap (LEXP_field (rewrite_lexp lexp,id)) + rewrap (LEXP_vector_range (rewrite_lexp map lexp,rewrite_exp map exp1,rewrite_exp map exp2)) + | LEXP_field (lexp,id) -> rewrap (LEXP_field (rewrite_lexp map lexp,id)) -let rewrite_fun (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,annot))) = +let rewrite_fun (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) = let rewrite_funcl (FCL_aux (FCL_Funcl(id,pat,exp),(l,annot))) = - (*let _ = Printf.eprintf "Rewriting function %s, pattern %s\n" (match id with (Id_aux (Id i,_)) -> i) (Pretty_print.pat_to_string pat) in*) - (FCL_aux (FCL_Funcl (id,pat,rewrite_exp exp),(l,annot))) - in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,annot)) + (*let _ = Printf.eprintf "Rewriting function %s, pattern %s\n" + (match id with (Id_aux (Id i,_)) -> i) (Pretty_print.pat_to_string pat) in*) + (FCL_aux (FCL_Funcl (id,pat,rewrite_exp (get_map_tannot fdannot) exp),(l,annot))) + in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot)) let rewrite_def d = match d with | DEF_type _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ -> d | DEF_fundef fdef -> DEF_fundef (rewrite_fun fdef) - | DEF_val letbind -> DEF_val (rewrite_let letbind) + | DEF_val letbind -> DEF_val (rewrite_let None letbind) | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "DEF_scattered survived to rewritter") let rewrite_defs (Defs defs) = diff --git a/src/rewriter.mli b/src/rewriter.mli index 3e81952d..1f1a2591 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -6,5 +6,5 @@ type 'a exp = 'a Ast.exp type 'a emap = 'a Envmap.t type envs = Type_check.envs -val rewrite_exp : tannot exp -> tannot exp +val rewrite_exp : nexp_map option -> tannot exp -> tannot exp val rewrite_defs : tannot defs -> tannot defs diff --git a/src/type_check.ml b/src/type_check.ml index 4c996e50..e0e02856 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -27,9 +27,9 @@ let rec field_equivs fields fmaps = | (FP_aux(FP_Fpat(id,pat),(l,annot)))::fields -> if (List.mem_assoc (id_to_string id) fmaps) then match (field_equivs fields fmaps) with - | None -> None - | Some [] -> None - | Some fs -> Some(((List.assoc (id_to_string id) fmaps),id,l,pat)::fs) + | None -> None + | Some [] -> None + | Some fs -> Some(((List.assoc (id_to_string id) fmaps),id,l,pat)::fs) else None let rec fields_to_rec fields rec_env = @@ -38,9 +38,9 @@ let rec fields_to_rec fields rec_env = | (id,Register,tannot,fmaps)::rec_env -> fields_to_rec fields rec_env | (id,Record,tannot,fmaps)::rec_env -> if (List.length fields) = (List.length fmaps) then - match field_equivs fields fmaps with - | Some(ftyps) -> Some(id,tannot,ftyps) - | None -> fields_to_rec fields rec_env + match field_equivs fields fmaps with + | Some(ftyps) -> Some(id,tannot,ftyps) + | None -> fields_to_rec fields rec_env else fields_to_rec fields rec_env let kind_to_k (K_aux((K_kind baseks),l)) = @@ -55,8 +55,8 @@ let kind_to_k (K_aux((K_kind baseks),l)) = | [] -> raise (Reporting_basic.err_unreachable l "Empty kind") | [bk] -> bk_to_k bk | bks -> (match List.rev bks with - | [] -> raise (Reporting_basic.err_unreachable l "Empty after reverse") - | out::args -> {k = K_Lam( List.map bk_to_k (List.rev args), bk_to_k out) }) + | [] -> raise (Reporting_basic.err_unreachable l "Empty after reverse") + | out::args -> {k = K_Lam( List.map bk_to_k (List.rev args), bk_to_k out) }) let rec has_typ_app check_nested name (Typ_aux(typ,_)) = match typ with @@ -79,8 +79,8 @@ let rec extract_if_first recur name (Typ_aux(typ,l)) = | Some(t,_) -> Some(t,t2) | None -> None) | (Typ_tup(t'::ts),true) -> (match (extract_if_first false name t') with - | Some(t,_) -> Some(t, Typ_aux(Typ_tup ts,l)) - | None -> None) + | Some(t,_) -> Some(t, Typ_aux(Typ_tup ts,l)) + | None -> None) | _ -> None let rec typ_to_t imp_ok fun_ok (Typ_aux(typ,l)) = @@ -91,17 +91,17 @@ let rec typ_to_t imp_ok fun_ok (Typ_aux(typ,l)) = | Typ_fn (ty1,ty2,e) -> if fun_ok then - if has_typ_app false "implicit" ty1 - then - if imp_ok - then (match extract_if_first true "implicit" ty1 with - | Some(imp,new_ty1) -> (match imp with - | Typ_app(_,[Typ_arg_aux(Typ_arg_nexp ((Nexp_aux(n,l')) as ne),_)]) -> - {t = Tfn (trans new_ty1, trans ty2, IP_user (anexp_to_nexp ne), aeffect_to_effect e)} - | _ -> typ_error l "Declaring an implicit parameter requires a Nat specification") - | None -> typ_error l "A function type with an implicit parameter must declare the implicit first") - else typ_error l "This function has one (or more) implicit parameter(s) not permitted here" - else {t = Tfn (trans ty1,trans ty2,IP_none,aeffect_to_effect e)} + if has_typ_app false "implicit" ty1 + then + if imp_ok + then (match extract_if_first true "implicit" ty1 with + | Some(imp,new_ty1) -> (match imp with + | Typ_app(_,[Typ_arg_aux(Typ_arg_nexp ((Nexp_aux(n,l')) as ne),_)]) -> + {t = Tfn (trans new_ty1, trans ty2, IP_user (anexp_to_nexp ne), aeffect_to_effect e)} + | _ -> typ_error l "Declaring an implicit parameter requires a Nat specification") + | None -> typ_error l "A function type with an implicit parameter must declare the implicit first") + else typ_error l "This function has one (or more) implicit parameter(s) not permitted here" + else {t = Tfn (trans ty1,trans ty2,IP_none,aeffect_to_effect e)} else typ_error l "Function types are only permitted at the top level." | Typ_tup(tys) -> {t = Ttup (List.map trans tys) } | Typ_app(i,args) -> {t = Tapp (id_to_string i,List.map typ_arg_to_targ args) } @@ -137,36 +137,36 @@ let rec quants_to_consts ((Env (d_env,t_env,b_env,tp_env)) as env) qis : (t_para | (QI_aux(qi,l))::qis -> let (ids,typarms,cs) = quants_to_consts env qis in (match qi with - | QI_id(KOpt_aux(ki,l')) -> - (match ki with - | KOpt_none (Kid_aux((Var i),l'')) -> - (match Envmap.apply d_env.k_env i with - | Some k -> + | QI_id(KOpt_aux(ki,l')) -> + (match ki with + | KOpt_none (Kid_aux((Var i),l'')) -> + (match Envmap.apply d_env.k_env i with + | Some k -> let targ = match k.k with | K_Typ -> TA_typ {t = Tvar i} | K_Nat -> TA_nexp (mk_nv i) | K_Ord -> TA_ord { order = Ovar i} | K_Efct -> TA_eft { effect = Evar i} - | _ -> raise (Reporting_basic.err_unreachable l'' "illegal kind allowed") in + | _ -> raise (Reporting_basic.err_unreachable l'' "illegal kind allowed") in ((i,k)::ids,targ::typarms,cs) - | None -> raise (Reporting_basic.err_unreachable l'' "Unkinded id without default after initial check")) - | KOpt_kind(kind,Kid_aux((Var i),l'')) -> + | None -> raise (Reporting_basic.err_unreachable l'' "Unkinded id without default after initial check")) + | KOpt_kind(kind,Kid_aux((Var i),l'')) -> let k = kind_to_k kind in let targ = match k.k with | K_Typ -> TA_typ {t = Tvar i} | K_Nat -> TA_nexp (mk_nv i) | K_Ord -> TA_ord { order = Ovar i} | K_Efct -> TA_eft { effect = Evar i} - | K_Lam _ -> typ_error l'' "kind -> kind not permitted here" - | _ -> raise (Reporting_basic.err_unreachable l'' "Kind either infer or internal here") in + | K_Lam _ -> typ_error l'' "kind -> kind not permitted here" + | _ -> raise (Reporting_basic.err_unreachable l'' "Kind either infer or internal here") in ((i,k)::ids,targ::typarms,cs)) - | QI_const(NC_aux(nconst,l')) -> - (*TODO: somehow the requirement vs best guarantee needs to be derived from user or context*) - (match nconst with - | NC_fixed(n1,n2) -> (ids,typarms,Eq(Specc l',anexp_to_nexp n1,anexp_to_nexp n2)::cs) - | NC_bounded_ge(n1,n2) -> (ids,typarms,GtEq(Specc l',Guarantee,anexp_to_nexp n1,anexp_to_nexp n2)::cs) - | NC_bounded_le(n1,n2) -> (ids,typarms,LtEq(Specc l',Guarantee,anexp_to_nexp n1,anexp_to_nexp n2)::cs) - | NC_nat_set_bounded(Kid_aux((Var i),l''), bounds) -> (ids,typarms,In(Specc l',i,bounds)::cs))) + | QI_const(NC_aux(nconst,l')) -> + (*TODO: somehow the requirement vs best guarantee needs to be derived from user or context*) + (match nconst with + | NC_fixed(n1,n2) -> (ids,typarms,Eq(Specc l',anexp_to_nexp n1,anexp_to_nexp n2)::cs) + | NC_bounded_ge(n1,n2) -> (ids,typarms,GtEq(Specc l',Guarantee,anexp_to_nexp n1,anexp_to_nexp n2)::cs) + | NC_bounded_le(n1,n2) -> (ids,typarms,LtEq(Specc l',Guarantee,anexp_to_nexp n1,anexp_to_nexp n2)::cs) + | NC_nat_set_bounded(Kid_aux((Var i),l''), bounds) -> (ids,typarms,In(Specc l',i,bounds)::cs))) let typq_to_params envs (TypQ_aux(tq,l)) = match tq with @@ -185,9 +185,9 @@ let into_register d_env (t : tannot) : tannot = | Base((ids,ty),tag,constraints,eft,bindings) -> let ty',_ = get_abbrev d_env ty in (match ty'.t with - | Tapp("register",_)-> t + | Tapp("register",_)-> t | Tabbrev(ti,{t=Tapp("register",_)}) -> Base((ids,ty'),tag,constraints,eft,bindings) - | _ -> Base((ids, {t= Tapp("register",[TA_typ ty'])}),tag,constraints,eft,bindings)) + | _ -> Base((ids, {t= Tapp("register",[TA_typ ty'])}),tag,constraints,eft,bindings)) | t -> t let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap) * nexp_range list * bounds_env * t) = @@ -199,38 +199,39 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) match p with | P_lit (L_aux(lit,l')) -> let t,lit = - (match lit with - | L_unit -> unit_t,lit - | L_zero -> bit_t,lit - | L_one -> bit_t,lit - | L_true -> bit_t,L_one - | L_false -> bit_t,L_zero - | L_num i -> - (match expect_actual.t with - | Tid "bit" -> - if i = 0 then bit_t,L_zero - else if i = 1 then bit_t,L_one - else {t = Tapp("atom", - [TA_nexp (mk_c_int i)])},lit - | _ -> {t = Tapp("atom", - [TA_nexp (mk_c_int i)])},lit) - | L_hex s -> - let size = big_int_of_int ((String.length s) * 4) in - let is_inc = match d_env.default_o.order with | Oinc -> true | _ -> false in - {t = Tapp("vector", - [TA_nexp (if is_inc then n_zero else mk_c(sub_big_int size one)); - TA_nexp (mk_c size); - TA_ord d_env.default_o; TA_typ{t=Tid "bit"}])},lit - | L_bin s -> - let size = big_int_of_int (String.length s) in - let is_inc = match d_env.default_o.order with | Oinc -> true | _ -> false in - {t = Tapp("vector", - [TA_nexp(if is_inc then n_zero else mk_c(sub_big_int size one)); - TA_nexp (mk_c size); - TA_ord d_env.default_o;TA_typ{t = Tid"bit"}])},lit - | L_string s -> {t = Tid "string"},lit - | L_undef -> typ_error l' "Cannot pattern match on undefined") in - (*let _ = Printf.eprintf "checking pattern literal. expected type is %s. t is %s\n" (t_to_string expect_t) (t_to_string t) in*) + (match lit with + | L_unit -> unit_t,lit + | L_zero -> bit_t,lit + | L_one -> bit_t,lit + | L_true -> bit_t,L_one + | L_false -> bit_t,L_zero + | L_num i -> + (match expect_actual.t with + | Tid "bit" -> + if i = 0 then bit_t,L_zero + else if i = 1 then bit_t,L_one + else {t = Tapp("atom", + [TA_nexp (mk_c_int i)])},lit + | _ -> {t = Tapp("atom", + [TA_nexp (mk_c_int i)])},lit) + | L_hex s -> + let size = big_int_of_int ((String.length s) * 4) in + let is_inc = match d_env.default_o.order with | Oinc -> true | _ -> false in + {t = Tapp("vector", + [TA_nexp (if is_inc then n_zero else mk_c(sub_big_int size one)); + TA_nexp (mk_c size); + TA_ord d_env.default_o; TA_typ{t=Tid "bit"}])},lit + | L_bin s -> + let size = big_int_of_int (String.length s) in + let is_inc = match d_env.default_o.order with | Oinc -> true | _ -> false in + {t = Tapp("vector", + [TA_nexp(if is_inc then n_zero else mk_c(sub_big_int size one)); + TA_nexp (mk_c size); + TA_ord d_env.default_o;TA_typ{t = Tid"bit"}])},lit + | L_string s -> {t = Tid "string"},lit + | L_undef -> typ_error l' "Cannot pattern match on undefined") in + (*let _ = Printf.eprintf "checking pattern literal. expected type is %s. t is %s\n" + (t_to_string expect_t) (t_to_string t) in*) let t',cs' = type_consistent (Patt l) d_env Require true t expect_t in let cs_l = cs@cs' in (P_aux(P_lit(L_aux(lit,l')),(l,cons_tag_annot t emp_tag cs_l)),Envmap.empty,cs_l,nob,t) @@ -252,99 +253,99 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) let i = id_to_string id in let default_bounds = extract_bounds d_env i expect_t in let default = let id_annot = Base(([],expect_t),emp_tag,cs,pure_e,default_bounds) in - let pat_annot = match is_enum_typ d_env expect_t with - | None -> id_annot - | Some n -> Base(([],expect_t), Enum n, cs,pure_e,default_bounds) in - (P_aux(p,(l,pat_annot)),Envmap.from_list [(i,id_annot)],cs,default_bounds,expect_t) in + let pat_annot = match is_enum_typ d_env expect_t with + | None -> id_annot + | Some n -> Base(([],expect_t), Enum n, cs,pure_e,default_bounds) in + (P_aux(p,(l,pat_annot)),Envmap.from_list [(i,id_annot)],cs,default_bounds,expect_t) in (match Envmap.apply t_env i with - | Some(Base((params,t),Constructor,cs,ef,bounds)) -> - let t,cs,ef,_ = subst params false t cs ef in + | Some(Base((params,t),Constructor,cs,ef,bounds)) -> + let t,cs,ef,_ = subst params false t cs ef in (match t.t with | Tfn({t = Tid "unit"},t',IP_none,ef) -> - if conforms_to_t d_env false false t' expect_t - then - let tp,cp = type_consistent (Expr l) d_env Guarantee false t' expect_t in - (P_aux(P_app(id,[]),(l,tag_annot t Constructor)),Envmap.empty,cs@cp,bounds,tp) - else default + if conforms_to_t d_env false false t' expect_t + then + let tp,cp = type_consistent (Expr l) d_env Guarantee false t' expect_t in + (P_aux(P_app(id,[]),(l,tag_annot t Constructor)),Envmap.empty,cs@cp,bounds,tp) + else default | Tfn(t1,t',IP_none,e) -> - if conforms_to_t d_env false false t' expect_t - then typ_error l ("Constructor " ^ i ^ " expects arguments of type " ^ (t_to_string t) ^ ", found none") - else default + if conforms_to_t d_env false false t' expect_t + then typ_error l ("Constructor " ^ i ^ " expects arguments of type " ^ (t_to_string t) ^ ", found none") + else default | _ -> raise (Reporting_basic.err_unreachable l "Constructor tannot does not have function type")) - | Some(Base((params,t),Enum max,cs,ef,bounds)) -> - let t,cs,ef,_ = subst params false t cs ef in - if conforms_to_t d_env false false t expect_t - then - let tp,cp = type_consistent (Expr l) d_env Guarantee false t expect_t in - (P_aux(P_app(id,[]),(l,tag_annot t (Enum max))),Envmap.empty,cs@cp,bounds,tp) - else default - | _ -> default) + | Some(Base((params,t),Enum max,cs,ef,bounds)) -> + let t,cs,ef,_ = subst params false t cs ef in + if conforms_to_t d_env false false t expect_t + then + let tp,cp = type_consistent (Expr l) d_env Guarantee false t expect_t in + (P_aux(P_app(id,[]),(l,tag_annot t (Enum max))),Envmap.empty,cs@cp,bounds,tp) + else default + | _ -> default) | P_app(id,pats) -> let i = id_to_string id in (*let _ = Printf.eprintf "checking constructor pattern %s\n" i in*) (match Envmap.apply t_env i with - | None | Some NoTyp | Some Overload _ -> typ_error l ("Constructor " ^ i ^ " in pattern is undefined") - | Some(Base((params,t),Constructor,constraints,eft,bounds)) -> + | None | Some NoTyp | Some Overload _ -> typ_error l ("Constructor " ^ i ^ " in pattern is undefined") + | Some(Base((params,t),Constructor,constraints,eft,bounds)) -> let t,dec_cs,_,_ = subst params false t constraints eft in - (match t.t with - | Tid id -> if pats = [] - then let t',ret_cs = type_consistent (Patt l) d_env Guarantee false t expect_t in - (P_aux(p,(l,cons_tag_annot t' Constructor dec_cs)), Envmap.empty,dec_cs@ret_cs,nob,t') - else typ_error l ("Constructor " ^ i ^ " does not expect arguments") - | Tfn(t1,t2,IP_none,ef) -> - let t',ret_cs = type_consistent (Patt l) d_env Guarantee false t2 expect_t in + (match t.t with + | Tid id -> if pats = [] + then let t',ret_cs = type_consistent (Patt l) d_env Guarantee false t expect_t in + (P_aux(p,(l,cons_tag_annot t' Constructor dec_cs)), Envmap.empty,dec_cs@ret_cs,nob,t') + else typ_error l ("Constructor " ^ i ^ " does not expect arguments") + | Tfn(t1,t2,IP_none,ef) -> + let t',ret_cs = type_consistent (Patt l) d_env Guarantee false t2 expect_t in (match pats with | [] -> let _ = type_consistent (Patt l) d_env Guarantee false unit_t t1 in (P_aux(P_app(id,[]),(l,cons_tag_annot t' Constructor dec_cs)), - Envmap.empty,dec_cs@ret_cs,nob,t') + Envmap.empty,dec_cs@ret_cs,nob,t') | [p] -> let (p',env,p_cs,bounds,u) = check_pattern envs emp_tag t1 p in (P_aux(P_app(id,[p']), - (l,cons_tag_annot t' Constructor dec_cs)),env,dec_cs@p_cs@ret_cs,bounds,t') + (l,cons_tag_annot t' Constructor dec_cs)),env,dec_cs@p_cs@ret_cs,bounds,t') | pats -> let (pats',env,p_cs,bounds,u) = match check_pattern envs emp_tag t1 (P_aux(P_tup(pats),(l,annot))) with | ((P_aux(P_tup(pats'),_)),env,constraints,bounds,u) -> (pats',env,constraints,bounds,u) | _ -> assert false in - (P_aux(P_app(id,pats'), - (l,cons_tag_annot t' Constructor dec_cs)),env,dec_cs@p_cs@ret_cs,bounds,t')) - | _ -> typ_error l ("Identifier " ^ i ^ " must be a union constructor")) - | Some(Base((params,t),tag,constraints,eft,bounds)) -> - typ_error l ("Identifier " ^ i ^ " used in pattern is not a union constructor")) + (P_aux(P_app(id,pats'), + (l,cons_tag_annot t' Constructor dec_cs)),env,dec_cs@p_cs@ret_cs,bounds,t')) + | _ -> typ_error l ("Identifier " ^ i ^ " must be a union constructor")) + | Some(Base((params,t),tag,constraints,eft,bounds)) -> + typ_error l ("Identifier " ^ i ^ " used in pattern is not a union 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,tannot,typ_pats) -> - (match tannot with - | (Base((vs,t),tag,cs,eft,bounds)) -> - let tup = {t = Ttup(List.map (fun (t,_,_,_) -> t) typ_pats)} in - let ft = {t = Tfn(tup,t, IP_none,pure_e) } in - let (ft_subst,cs,_,_) = subst vs false t cs pure_e in - let subst_rtyp,subst_typs = - match ft_subst.t with | Tfn({t=Ttup tups},rt,_,_) -> rt,tups - | _ -> raise (Reporting_basic.err_unreachable l "fields_to_rec gave a non function type") in - let pat_checks = - List.map2 (fun (_,id,l,pat) styp -> - let (pat,env,constraints,new_bounds,u) = check_pattern envs emp_tag styp pat in - let pat = FP_aux(FP_Fpat(id,pat),(l,Base(([],styp),tag,constraints,pure_e,new_bounds))) in - (pat,env,constraints,new_bounds)) typ_pats subst_typs in - let pats' = List.map (fun (a,_,_,_) -> a) pat_checks in - (*Need to check for variable duplication here*) - let env = List.fold_right (fun (_,env,_,_) env' -> Envmap.union env env') pat_checks Envmap.empty in - let constraints = (List.fold_right (fun (_,_,cs,_) cons -> cs@cons) pat_checks [])@cs in - let bounds = List.fold_right (fun (_,_,_,bounds) b_env -> merge_bounds bounds b_env) pat_checks nob in + | None -> typ_error l ("No struct exists with the listed fields") + | Some(id,tannot,typ_pats) -> + (match tannot with + | (Base((vs,t),tag,cs,eft,bounds)) -> + (*let tup = {t = Ttup(List.map (fun (t,_,_,_) -> t) typ_pats)} in*) + (*let ft = {t = Tfn(tup,t, IP_none,pure_e) } in*) + let (ft_subst,cs,_,_) = subst vs false t cs pure_e in + let subst_rtyp,subst_typs = + match ft_subst.t with | Tfn({t=Ttup tups},rt,_,_) -> rt,tups + | _ -> raise (Reporting_basic.err_unreachable l "fields_to_rec gave a non function type") in + let pat_checks = + List.map2 (fun (_,id,l,pat) styp -> + let (pat,env,constraints,new_bounds,u) = check_pattern envs emp_tag styp pat in + let pat = FP_aux(FP_Fpat(id,pat),(l,Base(([],styp),tag,constraints,pure_e,new_bounds))) in + (pat,env,constraints,new_bounds)) typ_pats subst_typs in + let pats' = List.map (fun (a,_,_,_) -> a) pat_checks in + (*Need to check for variable duplication here*) + let env = List.fold_right (fun (_,env,_,_) env' -> Envmap.union env env') pat_checks Envmap.empty in + let constraints = (List.fold_right (fun (_,_,cs,_) cons -> cs@cons) pat_checks [])@cs in + let bounds = List.fold_right (fun (_,_,_,bounds) b_env -> merge_bounds bounds b_env) pat_checks nob in let t',cs' = type_consistent (Patt l) d_env Guarantee false ft_subst expect_t in - (P_aux((P_record(pats',false)),(l,cons_tag_annot t' emp_tag (cs@cs'))),env,constraints@cs',bounds,t') - | _ -> raise (Reporting_basic.err_unreachable l "fields_to_rec returned a non Base tannot"))) + (P_aux((P_record(pats',false)),(l,cons_tag_annot t' emp_tag (cs@cs'))),env,constraints@cs',bounds,t') + | _ -> raise (Reporting_basic.err_unreachable l "fields_to_rec returned a non Base tannot"))) | P_vector pats -> let (item_t, base, rise, ord) = match expect_actual.t with - | Tapp("vector",[TA_nexp b;TA_nexp r;TA_ord o;TA_typ i]) -> (i,b,r,o) - | Tuvar _ -> (new_t (),new_n (),new_n(), d_env.default_o) + | Tapp("vector",[TA_nexp b;TA_nexp r;TA_ord o;TA_typ i]) -> (i,b,r,o) + | Tuvar _ -> (new_t (),new_n (),new_n(), d_env.default_o) | _ -> typ_error l ("Expected a " ^ t_to_string expect_actual ^ " but found a vector") in let (pats',ts,t_envs,constraints,bounds) = - List.fold_right - (fun pat (pats,ts,t_envs,constraints,bounds) -> - let (pat',t_env,cons,bs,t) = check_pattern envs emp_tag item_t pat in - ((pat'::pats),(t::ts),(t_env::t_envs),(cons@constraints),merge_bounds bs bounds)) - pats ([],[],[],[],nob) in + List.fold_right + (fun pat (pats,ts,t_envs,constraints,bounds) -> + let (pat',t_env,cons,bs,t) = check_pattern envs emp_tag item_t pat in + ((pat'::pats),(t::ts),(t_env::t_envs),(cons@constraints),merge_bounds bs bounds)) + pats ([],[],[],[],nob) 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 (u,cs) = List.fold_right (fun u (t,cs) -> let t',cs = type_consistent (Patt l) d_env Require true u t in t',cs) ts (item_t,[]) in let len = List.length ts in @@ -365,93 +366,93 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) (P_aux(P_vector(pats'),(l,cons_tag_annot t emp_tag cs)), env,cs@constraints,bounds,t) | P_vector_indexed(ipats) -> let item_t = match expect_actual.t with - | Tapp("vector",[b;r;o;TA_typ i]) -> i - | Tuvar _ -> new_t () + | Tapp("vector",[b;r;o;TA_typ i]) -> i + | Tuvar _ -> new_t () | _ -> typ_error l ("Expected a vector by pattern form, but a " ^ t_to_string expect_actual ^ " by type") in let (is,pats) = List.split ipats in let (fst,lst) = (List.hd is),(List.hd (List.rev is)) in let inc_or_dec = - if fst < lst then - (let _ = List.fold_left - (fun i1 i2 -> if i1 < i2 then i2 - else typ_error l "Indexed vector pattern was inconsistently increasing") fst (List.tl is) in - true) - else if lst < fst then - (let _ = List.fold_left - (fun i1 i2 -> if i1 > i2 then i2 - 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 + if fst < lst then + (let _ = List.fold_left + (fun i1 i2 -> if i1 < i2 then i2 + else typ_error l "Indexed vector pattern was inconsistently increasing") fst (List.tl is) in + true) + else if lst < fst then + (let _ = List.fold_left + (fun i1 i2 -> if i1 > i2 then i2 + 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 let (pats',ts,t_envs,constraints,bounds) = - List.fold_right - (fun (i,pat) (pats,ts,t_envs,constraints,bounds) -> - let (pat',env,cons,new_bounds,t) = check_pattern envs emp_tag item_t pat in - (((i,pat')::pats),(t::ts),(env::t_envs),(cons@constraints),merge_bounds new_bounds bounds)) - ipats ([],[],[],[],nob) in + List.fold_right + (fun (i,pat) (pats,ts,t_envs,constraints,bounds) -> + let (pat',env,cons,new_bounds,t) = check_pattern envs emp_tag item_t pat in + (((i,pat')::pats),(t::ts),(env::t_envs),(cons@constraints),merge_bounds new_bounds bounds)) + ipats ([],[],[],[],nob) in let co = Patt l in let env = List.fold_right (fun e env -> Envmap.union e env) t_envs Envmap.empty in (*TODO Need to check for non-duplication of variables*) let (u,cs) = List.fold_right (fun u (t,cs) -> type_consistent co d_env Require true u t) ts (item_t,[]) in let t = {t = Tapp("vector",[(TA_nexp base);(TA_nexp rise); - (TA_ord{order=(if inc_or_dec then Oinc else Odec)});(TA_typ u)])} in + (TA_ord{order=(if inc_or_dec then Oinc else Odec)});(TA_typ u)])} in let cs = if inc_or_dec - then [LtEq(co, Require, base, mk_c_int fst); GtEq(co,Require, rise, mk_c_int(lst-fst));]@cs - else [GtEq(co, Require, base, mk_c_int fst); LtEq(co,Require, rise, mk_c_int(fst -lst));]@cs in + then [LtEq(co, Require, base, mk_c_int fst); GtEq(co,Require, rise, mk_c_int(lst-fst));]@cs + else [GtEq(co, Require, base, mk_c_int fst); LtEq(co,Require, rise, mk_c_int(fst -lst));]@cs in (P_aux(P_vector_indexed(pats'),(l,cons_tag_annot t emp_tag cs)), env,constraints@cs,bounds,t) | P_tup(pats) -> let item_ts = match expect_actual.t with - | Ttup ts -> - if (List.length ts) = (List.length pats) - then ts - else typ_error l ("Expected a pattern with a tuple with " ^ (string_of_int (List.length ts)) ^ " elements") - | Tuvar _ -> List.map (fun _ -> new_t ()) pats + | Ttup ts -> + if (List.length ts) = (List.length pats) + then ts + else typ_error l ("Expected a pattern with a tuple with " ^ (string_of_int (List.length ts)) ^ " elements") + | Tuvar _ -> List.map (fun _ -> new_t ()) pats | _ -> typ_error l ("Expected a tuple by pattern form, but a " ^ (t_to_string expect_actual) ^ " by type") in let (pats',ts,t_envs,constraints,bounds) = - List.fold_right - (fun (pat,t) (pats,ts,t_envs,constraints,bounds) -> - let (pat',env,cons,new_bounds,t) = check_pattern envs emp_tag t pat in - ((pat'::pats),(t::ts),(env::t_envs),cons@constraints,merge_bounds new_bounds bounds)) - (List.combine pats item_ts) ([],[],[],[],nob) in + List.fold_right + (fun (pat,t) (pats,ts,t_envs,constraints,bounds) -> + let (pat',env,cons,new_bounds,t) = check_pattern envs emp_tag t pat in + ((pat'::pats),(t::ts),(env::t_envs),cons@constraints,merge_bounds new_bounds bounds)) + (List.combine pats item_ts) ([],[],[],[],nob) 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,tag_annot t emp_tag)), env,constraints,bounds,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 (), d_env.default_o in + 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 (), d_env.default_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,bounds) = - List.fold_right - (fun pat (pats,ts,t_envs,constraints,bounds) -> - let (pat',env,cons,new_bounds,t) = check_pattern envs emp_tag (vec_ti ()) pat in - (pat'::pats,t::ts,env::t_envs,cons@constraints,merge_bounds new_bounds bounds)) - pats ([],[],[],[],nob) in + List.fold_right + (fun pat (pats,ts,t_envs,constraints,bounds) -> + let (pat',env,cons,new_bounds,t) = check_pattern envs emp_tag (vec_ti ()) pat in + (pat'::pats,t::ts,env::t_envs,cons@constraints,merge_bounds new_bounds bounds)) + pats ([],[],[],[],nob) 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*) + 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 + | 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 let range_c = List.fold_right - (fun t rn -> - match t.t with - | Tapp("vector",[(TA_nexp b);(TA_nexp r);(TA_ord o);(TA_typ u)]) -> mk_add r rn - | _ -> raise (Reporting_basic.err_unreachable l "vector concat pattern impossibility") ) (List.tl ts) r1 in + (fun t rn -> + match t.t with + | Tapp("vector",[(TA_nexp b);(TA_nexp r);(TA_ord o);(TA_typ u)]) -> mk_add r rn + | _ -> raise (Reporting_basic.err_unreachable l "vector concat pattern impossibility") ) (List.tl ts) r1 in let cs = [Eq((Patt l),rise,range_c)]@cs in (P_aux(P_vector_concat(pats'),(l,cons_tag_annot t emp_tag cs)), env,constraints@cs,bounds,t) | P_list(pats) -> let item_t = match expect_actual.t with - | Tapp("list",[TA_typ i]) -> i - | Tuvar _ -> new_t () + | Tapp("list",[TA_typ i]) -> i + | Tuvar _ -> new_t () | _ -> typ_error l ("Expected a list here by pattern form, but expected a " ^ t_to_string expect_actual ^ " by type") in let (pats',ts,envs,constraints,bounds) = - List.fold_right - (fun pat (pats,ts,t_envs,constraints,bounds) -> - let (pat',env,cons,new_bounds,t) = check_pattern envs emp_tag item_t pat in - (pat'::pats,t::ts,env::t_envs,cons@constraints,merge_bounds new_bounds bounds)) - pats ([],[],[],[],nob) in + List.fold_right + (fun pat (pats,ts,t_envs,constraints,bounds) -> + let (pat',env,cons,new_bounds,t) = check_pattern envs emp_tag item_t pat in + (pat'::pats,t::ts,env::t_envs,cons@constraints,merge_bounds new_bounds bounds)) + pats ([],[],[],[],nob) in let env = List.fold_right (fun e env -> Envmap.union e env) envs Envmap.empty in (*TODO 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 Require true u t in t',cs@cs') ts (item_t,[]) in let t = {t = Tapp("list",[TA_typ u])} in @@ -469,18 +470,18 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): (E_aux(E_block(exps'),(l,annot')),t,Envmap.empty,sc,nob,ef) | E_nondet exps -> let (ces, sc, ef) = - List.fold_right (fun e (es,sc,ef) -> let (e,_,_,sc',_,ef') = (check_exp envs imp_param unit_t e) in - (e::es,sc@sc',union_effects ef ef')) exps ([],[],pure_e) in - let _,cs = type_consistent (Expr l) d_env Require false unit_t expect_t in + List.fold_right (fun e (es,sc,ef) -> let (e,_,_,sc',_,ef') = (check_exp envs imp_param unit_t e) in + (e::es,sc@sc',union_effects ef ef')) exps ([],[],pure_e) in + let _,_ = type_consistent (Expr l) d_env Require false unit_t expect_t in (E_aux (E_nondet ces,(l,cons_ef_annot unit_t sc ef)),unit_t,t_env,sc,nob,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,bounds)) -> - let t,cs,ef,_ = subst params false t cs ef in + let t,cs,ef,_ = subst params false t cs ef in (match t.t with | Tfn({t = Tid "unit"},t',IP_none,ef) -> - let e = E_aux(E_app(id, []), (l, (Base(([],{t=Tfn(unit_t,t',IP_none,ef)}), Constructor, cs, ef, bounds)))) in + let e = E_aux(E_app(id, []), (l, (Base(([],{t=Tfn(unit_t,t',IP_none,ef)}), Constructor, cs, ef, bounds)))) in let t',cs',ef',e' = type_coerce (Expr l) d_env Require false false b_env t' e expect_t in (e',t',t_env,cs@cs',nob,union_effects ef ef') | Tfn(t1,t',IP_none,e) -> @@ -489,16 +490,16 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Some(Base((params,t),(Enum max),cs,ef,bounds)) -> let t',cs,_,_ = subst params false t cs ef in let t',cs',ef',e' = - type_coerce (Expr l) d_env Require false false b_env t' (rebuild (cons_tag_annot t' (Enum max) cs)) expect_t in + type_coerce (Expr l) d_env Require false false b_env t' (rebuild (cons_tag_annot t' (Enum max) cs)) expect_t in (e',t',t_env,cs@cs',nob,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(Base((params,t),tag,cs,ef,bounds)) -> - let ((t,cs,ef,_),is_alias) = - match tag with | Emp_global | External _ -> (subst params false t cs ef),false - | Alias -> (t,cs, add_effect (BE_aux(BE_rreg, Parse_ast.Unknown)) ef, Envmap.empty),true - | _ -> (t,cs,ef,Envmap.empty),false - in + let ((t,cs,ef,_),is_alias) = + match tag with | Emp_global | External _ -> (subst params false t cs ef),false + | Alias -> (t,cs, add_effect (BE_aux(BE_rreg, Parse_ast.Unknown)) ef, Envmap.empty),true + | _ -> (t,cs,ef,Envmap.empty),false + in let t,cs' = get_abbrev d_env t in let cs = cs@cs' in let t_actual,expect_actual = match t.t,expect_t.t with @@ -506,20 +507,21 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Tabbrev(_,t),_ -> t,expect_t | _,Tabbrev(_,e) -> t,e | _,_ -> t,expect_t in - (*let _ = Printf.eprintf "On general id check, expect_t %s, t %s, tactual %s, expect_actual %s\n" (t_to_string expect_t) (t_to_string t) (t_to_string t_actual) (t_to_string expect_actual) in*) + (*let _ = Printf.eprintf "On general id check, expect_t %s, t %s, tactual %s, expect_actual %s\n" + (t_to_string expect_t) (t_to_string t) (t_to_string t_actual) (t_to_string expect_actual) in*) (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 = Base(([],t),Emp_global,cs,ef,bounds) in - let t',cs' = type_consistent (Expr l) d_env Require false t' expect_t' in + let t',cs' = type_consistent (Expr l) d_env Require false t' expect_t' in (rebuild tannot,t,t_env,cs@cs',bounds,ef) | Tapp("register",[TA_typ(t')]),Tuvar _ -> - let ef' = add_effect (BE_aux(BE_rreg,l)) ef in + let ef' = add_effect (BE_aux(BE_rreg,l)) ef in let tannot = Base(([],t),(if is_alias then Alias else External (Some i)),cs,ef',bounds) in let t',cs',_,e' = type_coerce (Expr l) d_env Require false false b_env t' (rebuild tannot) expect_actual in (e',t,t_env,cs@cs',bounds,ef') | Tapp("register",[TA_typ(t')]),_ -> - let ef' = add_effect (BE_aux(BE_rreg,l)) ef in + let ef' = add_effect (BE_aux(BE_rreg,l)) ef in let tannot = Base(([],t),(if is_alias then Alias else External (Some i)),cs,ef',bounds) in let t',cs',_,e' = type_coerce (Expr l) d_env Require false false b_env t' (rebuild tannot) expect_actual in (e',t',t_env,cs@cs',bounds,ef') @@ -529,30 +531,30 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): (e',t',t_env,cs@cs',bounds,pure_e) | _ -> let t',cs',ef',e' = - type_coerce (Expr l) d_env Require false false b_env t (rebuild (Base(([],t),tag,cs,pure_e,bounds))) expect_t in + type_coerce (Expr l) d_env Require false false b_env t (rebuild (Base(([],t),tag,cs,pure_e,bounds))) expect_t in (e',t',t_env,cs@cs',bounds,union_effects ef ef') ) | Some NoTyp | Some Overload _ | None -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is unbound")) | E_lit (L_aux(lit,l')) -> let e,cs,effect = (match lit with | L_unit -> (rebuild (simple_annot unit_t)),[],pure_e - | L_zero -> + | L_zero -> (match expect_t.t with | Tid "bool" -> simp_exp (E_lit(L_aux(L_zero,l'))) l bool_t,[],pure_e | _ -> simp_exp e l bit_t,[],pure_e) - | L_one -> + | L_one -> (match expect_t.t with | Tid "bool" -> simp_exp (E_lit(L_aux(L_one,l'))) l bool_t,[],pure_e | _ -> simp_exp e l bit_t,[],pure_e) - | L_true -> simp_exp e l bool_t,[],pure_e - | L_false -> simp_exp e l bool_t,[],pure_e - | L_num i -> - (*let _ = Printf.eprintf "expected type of number literal %i is %s\n" i (t_to_string expect_t) in*) + | L_true -> simp_exp e l bool_t,[],pure_e + | L_false -> simp_exp e l bool_t,[],pure_e + | L_num i -> + (*let _ = Printf.eprintf "expected type of number literal %i is %s\n" i (t_to_string expect_t) in*) (match expect_t.t with | Tid "bit" | Toptions({t=Tid"bit"},_) -> if i = 0 then simp_exp (E_lit(L_aux(L_zero,l'))) l bit_t,[],pure_e - else if i = 1 then simp_exp (E_lit(L_aux(L_one,l'))) l bit_t,[],pure_e - else typ_error l ("Expected a bit, found " ^ string_of_int i) + else if i = 1 then simp_exp (E_lit(L_aux(L_one,l'))) l bit_t,[],pure_e + else typ_error l ("Expected a bit, found " ^ string_of_int i) | Tid "bool" | Toptions({t=Tid"bool"},_)-> if i = 0 then simp_exp (E_lit(L_aux(L_zero,l'))) l bit_t,[],pure_e else if i = 1 then simp_exp (E_lit(L_aux(L_one,l'))) l bit_t ,[],pure_e @@ -562,38 +564,42 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let t = {t=Tapp("atom", [TA_nexp n;])} in let cs = [LtEq(Expr l,Guarantee,n,mk_sub (mk_2n rise) n_one)] in let f = match o.order with | Oinc -> "to_vec_inc" | Odec -> "to_vec_dec" | _ -> "to_vec_inc" in - (*let _ = Printf.eprintf "adding a call to to_vec_*: bounds are %s\n" (bounds_to_string b_env) in*) - let internal_tannot = (l,(cons_bs_annot {t = Tapp("implicit",[TA_nexp rise])} [] b_env)) in - let tannot = (l,cons_tag_annot expect_t (External (Some f)) cs) in + (*let _ = Printf.eprintf "adding a call to to_vec_*: bounds are %s\n" (bounds_to_string b_env) in*) + let internal_tannot = (l,(cons_bs_annot {t = Tapp("implicit",[TA_nexp rise])} [] b_env)) in + let tannot = (l,cons_tag_annot expect_t (External (Some f)) cs) in E_aux(E_app((Id_aux((Id f),l)), - [(E_aux (E_internal_exp(internal_tannot), tannot));simp_exp e l t]),tannot),cs,pure_e + [(E_aux (E_internal_exp(internal_tannot), tannot));simp_exp e l t]),tannot),cs,pure_e | _ -> simp_exp e l {t = Tapp("atom", [TA_nexp (mk_c_int i)])},[],pure_e) - | L_hex s -> - let size = (String.length s) * 4 in - let start = match d_env.default_o.order with | Oinc -> n_zero | Odec -> mk_c_int (size - 1) in - simp_exp e l {t = Tapp("vector", - [TA_nexp start; - TA_nexp (mk_c_int size); - TA_ord d_env.default_o;TA_typ{t = Tid "bit"}])},[],pure_e - | L_bin s -> - let size = String.length s in - let start = match d_env.default_o.order with | Oinc -> n_zero | Odec -> mk_c_int (size -1) in - simp_exp e l {t = Tapp("vector", - [TA_nexp start; - TA_nexp (mk_c_int size); - TA_ord d_env.default_o ;TA_typ{t = Tid"bit"}])},[],pure_e - | L_string s -> simp_exp e l {t = Tid "string"},[],pure_e - | L_undef -> - let ef = {effect=Eset[BE_aux(BE_undef,l)]} in + | L_hex s -> + let size = (String.length s) * 4 in + let start = match d_env.default_o.order with + | Oinc -> n_zero | Odec -> mk_c_int (size - 1) | _ -> n_zero in + simp_exp e l {t = Tapp("vector", + [TA_nexp start; + TA_nexp (mk_c_int size); + TA_ord d_env.default_o;TA_typ{t = Tid "bit"}])},[],pure_e + | L_bin s -> + let size = String.length s in + let start = match d_env.default_o.order with + | Oinc -> n_zero | Odec -> mk_c_int (size -1) | _ -> n_zero in + simp_exp e l {t = Tapp("vector", + [TA_nexp start; + TA_nexp (mk_c_int size); + TA_ord d_env.default_o ;TA_typ{t = Tid"bit"}])},[],pure_e + | L_string s -> simp_exp e l {t = Tid "string"},[],pure_e + | L_undef -> + let ef = {effect=Eset[BE_aux(BE_undef,l)]} in (match expect_t.t with | Tapp ("vector",[TA_nexp base;TA_nexp {nexp = rise};TA_ord o;(TA_typ {t=Tid "bit"})]) - | Tapp ("register",[TA_typ {t=Tapp ("vector",[TA_nexp base;TA_nexp { nexp = rise}; - TA_ord o;(TA_typ {t=Tid "bit"})])}])-> + | Tapp ("register",[TA_typ {t=Tapp ("vector",[TA_nexp base;TA_nexp { nexp = rise}; + TA_ord o;(TA_typ {t=Tid "bit"})])}])-> let f = match o.order with | Oinc -> "to_vec_inc" | Odec -> "to_vec_dec" - | _ -> (match d_env.default_o.order with | Oinc -> "to_vec_inc" | Odec -> "to_vec_dec") in - let tannot = (l,Base(([],expect_t),External (Some f),[],ef,b_env)) in + | _ -> (match d_env.default_o.order with + | Oinc -> "to_vec_inc" | Odec -> "to_vec_dec" + | _ -> "to_vec_inc") in + let tannot = (l,Base(([],expect_t),External (Some f),[],ef,b_env)) in E_aux(E_app((Id_aux((Id f),l)), - [(E_aux (E_internal_exp(tannot), tannot));simp_exp e l bit_t]),tannot),[],ef + [(E_aux (E_internal_exp(tannot), tannot));simp_exp e l bit_t]),tannot),[],ef | _ -> simp_exp e l (new_t ()),[],ef)) in let t',cs',_,e' = type_coerce (Expr l) d_env Require false true b_env (get_e_typ e) e expect_t in (e',t',t_env,cs@cs',nob,effect) @@ -603,9 +609,11 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let cast_t = typ_subst tp_env false cast_t in let ct = {t = Toptions(cast_t,None)} in let (e',u,t_env,cs,bounds,ef) = check_exp envs imp_param ct e in - (*let _ = Printf.eprintf "Type checking cast: cast_t is %s constraints after checking e are %s\n" (t_to_string cast_t) (constraints_to_string cs) in*) + (*let _ = Printf.eprintf "Type checking cast: cast_t is %s constraints after checking e are %s\n" + (t_to_string cast_t) (constraints_to_string cs) in*) let t',cs2,ef',e' = type_coerce (Expr l) d_env Require true false b_env u e' cast_t in - (*let _ = Printf.eprintf "Type checking cast: after first coerce with u at %s, and final t' %s is and constraints are %s\n" (t_to_string u) (t_to_string t') (constraints_to_string cs2) in*) + (*let _ = Printf.eprintf "Type checking cast: after first coerce with u at %s, and final t' %s is and constraints are %s\n" + (t_to_string u) (t_to_string t') (constraints_to_string cs2) in*) let t',cs3,ef'',e'' = type_coerce (Expr l) d_env Guarantee false false b_env cast_t e' expect_t in (*let _ = Printf.eprintf "Type checking cast: after second coerce expect_t is %s, t' %s is and constraints are %s\n" (t_to_string expect_t) (t_to_string t') (constraints_to_string cs3) in*) (e'',t',t_env,cs_a@cs@cs2@cs3,bounds,union_effects ef' (union_effects ef'' ef)) @@ -613,7 +621,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let i = id_to_string id in let check_parms p_typ parms = (match parms with | [] | [(E_aux (E_lit (L_aux (L_unit,_)),_))] - -> let (_,cs') = type_consistent (Expr l) d_env Require false unit_t p_typ in [],unit_t,cs',pure_e + -> let (_,cs') = type_consistent (Expr l) d_env Require false unit_t p_typ in [],unit_t,cs',pure_e | [parm] -> let (parm',arg_t,t_env,cs',_,ef_p) = check_exp envs imp_param p_typ parm in [parm'],arg_t,cs',ef_p | parms -> (match check_exp envs imp_param p_typ (E_aux (E_tuple parms,(l,NoTyp))) with @@ -621,46 +629,48 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | _ -> raise (Reporting_basic.err_unreachable l "check_exp, given a tuple and a tuple type, didn't return a tuple"))) in let coerce_parms arg_t parms expect_arg_t = - (match parms with - | [] | [(E_aux (E_lit (L_aux(L_unit, _)), _))] -> [],pure_e,[] - | [parm] -> - let _,cs,ef,parm' = - type_coerce (Expr l) d_env Guarantee false false b_env arg_t parm expect_arg_t in [parm'],ef,cs - | parms -> + (match parms with + | [] | [(E_aux (E_lit (L_aux(L_unit, _)), _))] -> [],pure_e,[] + | [parm] -> + let _,cs,ef,parm' = + type_coerce (Expr l) d_env Guarantee false false b_env arg_t parm expect_arg_t in [parm'],ef,cs + | parms -> (match - type_coerce (Expr l) d_env Guarantee false false b_env arg_t (E_aux (E_tuple parms,(l,NoTyp))) expect_arg_t - with + type_coerce (Expr l) d_env Guarantee false false b_env arg_t (E_aux (E_tuple parms,(l,NoTyp))) expect_arg_t + with | (_,cs,ef,(E_aux(E_tuple parms',tannot'))) -> (parms',ef,cs) | _ -> raise (Reporting_basic.err_unreachable l "type coerce given tuple and tuple type returned non-tuple"))) in let check_result ret imp tag cs ef parms = - match (imp,imp_param) with - | (IP_length n ,None) | (IP_user n,None) | (IP_start n,None) -> - (*let _ = Printf.eprintf "implicit length or var required, no imp_param %s\n!" (n_to_string n) in*) - let internal_exp = - let _ = set_imp_param n in - let implicit = {t= Tapp("implicit",[TA_nexp n])} in - let annot_i = Base(([],implicit),Emp_local,[],pure_e,b_env) in - E_aux(E_internal_exp((l,annot_i)),(l,simple_annot nat_t)) in + match (imp,imp_param) with + | (IP_length n ,None) | (IP_user n,None) | (IP_start n,None) -> + (*let _ = Printf.eprintf "implicit length or var required, no imp_param %s\n!" (n_to_string n) in*) + let internal_exp = + let _ = set_imp_param n in + let implicit = {t= Tapp("implicit",[TA_nexp n])} in + let annot_i = Base(([],implicit),Emp_local,[],pure_e,b_env) in + E_aux(E_internal_exp((l,annot_i)),(l,simple_annot nat_t)) in + type_coerce (Expr l) d_env Require false false b_env ret + (E_aux (E_app(id, internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t + | (IP_length n ,Some ne) | (IP_user n,Some ne) | (IP_start n,Some ne) -> + (*let _ = Printf.eprintf "implicit length or var required %s with imp_param %s\n" + (n_to_string n) (n_to_string ne) in + let _ = Printf.eprintf "and expected type is %s and return type is %s\n" + (t_to_string expect_t) (t_to_string ret) in*) + let _ = set_imp_param n; set_imp_param ne in + let internal_exp = + let implicit_user = {t = Tapp("implicit",[TA_nexp ne])} in + let implicit = {t= Tapp("implicit",[TA_nexp n])} in + let annot_iu = Base(([],implicit_user),Emp_local,[],pure_e,b_env)in + let annot_i = Base(([],implicit),Emp_local,[],pure_e,b_env) in + E_aux (E_internal_exp_user((l, annot_iu),(l,annot_i)), (l,simple_annot nat_t)) + in type_coerce (Expr l) d_env Require false false b_env ret - (E_aux (E_app(id, internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t - | (IP_length n ,Some ne) | (IP_user n,Some ne) | (IP_start n,Some ne) -> - (*let _ = Printf.eprintf "implicit length or var required %s with imp_param %s\n" (n_to_string n) (n_to_string ne) in - let _ = Printf.eprintf "and expected type is %s and return type is %s\n" (t_to_string expect_t) (t_to_string ret) in*) - let _ = set_imp_param n; set_imp_param ne in - let internal_exp = - let implicit_user = {t = Tapp("implicit",[TA_nexp ne])} in - let implicit = {t= Tapp("implicit",[TA_nexp n])} in - let annot_iu = Base(([],implicit_user),Emp_local,[],pure_e,b_env)in - let annot_i = Base(([],implicit),Emp_local,[],pure_e,b_env) in - E_aux (E_internal_exp_user((l, annot_iu),(l,annot_i)), (l,simple_annot nat_t)) - in - type_coerce (Expr l) d_env Require false false b_env ret - (E_aux (E_app(id,internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t + (E_aux (E_app(id,internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t | (IP_none,_) -> - (*let _ = Printf.printf "no implicit length or var required\n" in*) + (*let _ = Printf.printf "no implicit length or var required\n" in*) type_coerce (Expr l) d_env Require false false b_env ret - (E_aux (E_app(id, parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t + (E_aux (E_app(id, parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t in (match Envmap.apply t_env i with | Some(Base(tp,Enum _,_,_,_)) -> @@ -668,50 +678,52 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Some(Base(tp,Default,_,_,_)) -> typ_error l ("Function " ^ i ^ " must be specified, not just declared as a default, before use") | Some(Base((params,t),tag,cs,ef,bounds)) -> - (*let _ = Printf.eprintf "Going to check a function call %s with unsubstituted types %s and constraints %s \n" i (t_to_string t) (constraints_to_string cs) in*) + (*let _ = Printf.eprintf "Going to check a function call %s with unsubstituted types %s and constraints %s \n" i (t_to_string t) (constraints_to_string cs) in*) let t,cs,ef,_ = subst params false t cs ef in (match t.t with | Tfn(arg,ret,imp,ef') -> - (*let _ = Printf.eprintf "Checking funcation call of %s\n" i in - let _ = Printf.eprintf "Substituted types and constraints are %s and %s\n" (t_to_string t) (constraints_to_string cs) in*) + (*let _ = Printf.eprintf "Checking funcation call of %s\n" i in + let _ = Printf.eprintf "Substituted types and constraints are %s and %s\n" (t_to_string t) (constraints_to_string cs) in*) let parms,arg_t,cs_p,ef_p = check_parms arg parms in - (*let _ = Printf.eprintf "Checked parms of %s\n" i in*) + (*let _ = Printf.eprintf "Checked parms of %s\n" i in*) let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef' parms in - (*let _ = Printf.eprintf "Checked result of %s and constraints are %s\n" i (constraints_to_string cs_r) in*) + (*let _ = Printf.eprintf "Checked result of %s and constraints are %s\n" i (constraints_to_string cs_r) in*) (e',ret_t,t_env,cs@cs_p@cs_r, bounds,union_effects ef' (union_effects ef_p ef_r)) - | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) + | _ -> 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,_),overload_return,variants)) -> - let t_p,cs_p,ef_p,_ = subst params false t cs ef in - let args,arg_t,arg_cs,arg_ef = - (match t_p.t with - | Tfn(arg,ret,_,ef') -> check_parms arg parms - | _ -> - 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 true overload_return variants arg_t) with - | [] -> typ_error l - ("No function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t)) - | [Base((params,t),tag,cs,ef,bounds)] -> - (match t.t with - | Tfn(arg,ret,imp,ef') -> - let args',arg_ef',arg_cs' = coerce_parms arg_t args arg in - let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef' args' in - (e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,nob, - union_effects ef_r (union_effects ef_p (union_effects (union_effects arg_ef' arg_ef) ef'))) - | _ -> raise (Reporting_basic.err_unreachable l "Overloaded variant not a function")) - | variants' -> - (match select_overload_variant d_env false true variants' expect_t with - | [] -> - typ_error l ("No function found with name " ^ i ^ ", expecting parameters " ^ (t_to_string arg_t) ^ " and returning " ^ (t_to_string expect_t)) - | [Base((params,t),tag,cs,ef,bounds)] -> - (match t.t with - |Tfn(arg,ret,imp,ef') -> - let args',arg_ef',arg_cs' = coerce_parms arg_t args arg in - let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef' args' in - (e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,nob, - union_effects ef_r (union_effects ef_p (union_effects (union_effects arg_ef arg_ef') ef'))) - | _ -> raise (Reporting_basic.err_unreachable l "Overloaded variant not a function")) - | _ -> + let t_p,cs_p,ef_p,_ = subst params false t cs ef in + let args,arg_t,arg_cs,arg_ef = + (match t_p.t with + | Tfn(arg,ret,_,ef') -> check_parms arg parms + | _ -> + 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 true overload_return variants arg_t) with + | [] -> typ_error l + ("No function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t)) + | [Base((params,t),tag,cs,ef,bounds)] -> + (match t.t with + | Tfn(arg,ret,imp,ef') -> + let args',arg_ef',arg_cs' = coerce_parms arg_t args arg in + let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef' args' in + (e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,nob, + union_effects ef_r (union_effects ef_p (union_effects (union_effects arg_ef' arg_ef) ef'))) + | _ -> raise (Reporting_basic.err_unreachable l "Overloaded variant not a function")) + | variants' -> + (match select_overload_variant d_env false true variants' expect_t with + | [] -> + typ_error l ("No function found with name " ^ i ^ ", expecting parameters " ^ (t_to_string arg_t) ^ " and returning " ^ (t_to_string expect_t)) + | [Base((params,t),tag,cs,ef,bounds)] -> + (match t.t with + |Tfn(arg,ret,imp,ef') -> + let args',arg_ef',arg_cs' = coerce_parms arg_t args arg in + let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef' args' in + (e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,nob, + union_effects ef_r (union_effects ef_p (union_effects (union_effects arg_ef arg_ef') ef'))) + | _ -> raise (Reporting_basic.err_unreachable l "Overloaded variant not a function")) + | _ -> typ_error l ("More than one definition of " ^ i ^ " found with type " ^ (t_to_string arg_t) ^ " -> " ^ (t_to_string expect_t) ^ ". A cast may be required"))) | _ -> typ_error l ("Unbound function " ^ i)) | E_app_infix(lft,op,rht) -> @@ -720,19 +732,19 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): match check_exp envs imp_param arg_t (E_aux(E_tuple [lft;rht],(l,NoTyp))) with | ((E_aux(E_tuple [lft';rht'],_)),arg_t,_,cs',_,ef') -> (lft',rht',arg_t,cs',ef') | _ -> - raise (Reporting_basic.err_unreachable l "check exp given tuple and tuple type and returned non-tuple") + raise (Reporting_basic.err_unreachable l "check exp given tuple and tuple type and returned non-tuple") in let check_result ret imp tag cs ef lft rht = match imp with | _ -> (*implicit isn't allowed at the moment on any infix functions *) type_coerce (Expr l) d_env Require false false b_env ret - (E_aux (E_app_infix(lft,op,rht),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t + (E_aux (E_app_infix(lft,op,rht),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t in (match Envmap.apply t_env i with | Some(Base(tp,Enum _,cs,ef,b)) -> - typ_error l ("Expected function with name " ^ i ^ " but found an enumeration identifier") + typ_error l ("Expected function with name " ^ i ^ " but found an enumeration identifier") | Some(Base(tp,Default,cs,ef,b)) -> - typ_error l ("Function " ^ i ^ " must be defined, not just declared as default, before use") + typ_error l ("Function " ^ i ^ " must be defined, not just declared as default, before use") | Some(Base((params,t),tag,cs,ef,b)) -> let t,cs,ef,_ = subst params false t cs ef in (match t.t with @@ -741,53 +753,55 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let ret_t,cs_r',ef_r,e' = check_result ret imp tag cs ef lft' rht' in (e',ret_t,t_env,cs@cs_p@cs_r',nob,union_effects ef (union_effects ef_p ef_r)) | _ -> - typ_error l ("Expected a function, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) + typ_error l ("Expected a function, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) | Some(Overload(Base((params,t),tag,cs,ef,_),overload_return,variants)) -> - let t_p,cs_p,ef_p,_ = subst params false t cs ef in - let lft',rht',arg_t,arg_cs,arg_ef = - (match t_p.t with - | Tfn(arg,ret,_,ef') -> check_parms arg lft rht - | _ -> typ_error l ("Expected a function, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in - (*let _ = Printf.eprintf "Looking for overloaded function %s, generic type is %s, arg_t is %s\n" i (t_to_string t_p) (t_to_string arg_t) in*) - (match (select_overload_variant d_env true overload_return variants arg_t) with - | [] -> - typ_error l ("No function found with name " ^ i ^ - " that expects parameters " ^ (t_to_string arg_t)) - | [Base((params,t),tag,cs,ef,b)] -> + let t_p,cs_p,ef_p,_ = subst params false t cs ef in + let lft',rht',arg_t,arg_cs,arg_ef = + (match t_p.t with + | Tfn(arg,ret,_,ef') -> check_parms arg lft rht + | _ -> typ_error l ("Expected a function, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in + (*let _ = Printf.eprintf "Looking for overloaded function %s, generic type is %s, arg_t is %s\n" + i (t_to_string t_p) (t_to_string arg_t) in*) + (match (select_overload_variant d_env true overload_return variants arg_t) with + | [] -> + typ_error l ("No function found with name " ^ i ^ + " that expects parameters " ^ (t_to_string arg_t)) + | [Base((params,t),tag,cs,ef,b)] -> (*let _ = Printf.eprintf "Selected an overloaded function for %s, - variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*) - (match t.t with - | Tfn(arg,ret,imp,ef') -> + variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*) + (match t.t with + | Tfn(arg,ret,imp,ef') -> (match arg.t,arg_t.t with | Ttup([tlft;trght]),Ttup([tlft_t;trght_t]) -> - let (lft',rht',arg_t,cs_p,ef_p) = check_parms arg lft rht in + let (lft',rht',arg_t,cs_p,ef_p) = check_parms arg lft rht in (*let (_,cs_lft,ef_lft,lft') = type_coerce (Expr l) d_env false tlft_t lft' tlft in - let (_,cs_rght,ef_rght,rht') = type_coerce (Expr l) d_env false trght_t rht' trght in*) - let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef lft' rht' in - (e',ret_t,t_env,cs_p@arg_cs@cs@cs_r,nob, - union_effects ef_r (union_effects ef_p (union_effects arg_ef ef'))) + let (_,cs_rght,ef_rght,rht') = type_coerce (Expr l) d_env false trght_t rht' trght in*) + let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef lft' rht' in + (e',ret_t,t_env,cs_p@arg_cs@cs@cs_r,nob, + union_effects ef_r (union_effects ef_p (union_effects arg_ef ef'))) |_ -> raise (Reporting_basic.err_unreachable l "function no longer has tuple type")) - | _ -> raise (Reporting_basic.err_unreachable l "overload variant does not have function")) - | variants -> - (*let _ = Printf.eprintf "Number of variants found before looking at return value %i\n%!" (List.length variants) in*) - (match (select_overload_variant d_env false true variants expect_t) with - | [] -> - typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ - (t_to_string arg_t) ^ " returning " ^ (t_to_string expect_t)) - | [Base((params,t),tag,cs,ef,b)] -> + | _ -> raise (Reporting_basic.err_unreachable l "overload variant does not have function")) + | variants -> + (*let _ = Printf.eprintf "Number of variants found before looking at return value %i\n%!" + (List.length variants) in*) + (match (select_overload_variant d_env false true variants expect_t) with + | [] -> + typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ + (t_to_string arg_t) ^ " returning " ^ (t_to_string expect_t)) + | [Base((params,t),tag,cs,ef,b)] -> (*let _ = Printf.eprintf "Selected an overloaded function for %s, - variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*) - (match t.t with - | Tfn(arg,ret,imp,ef') -> - (match arg.t,arg_t.t with - | Ttup([tlft;trght]),Ttup([tlft_t;trght_t]) -> - let (lft',rht',arg_t,cs_p,ef_p) = check_parms arg lft rht in - let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef lft' rht' in - (e',ret_t,t_env,cs_p@arg_cs@cs@cs_r,nob, - union_effects ef_r (union_effects ef_p (union_effects arg_ef ef'))) - |_ -> raise (Reporting_basic.err_unreachable l "function no longer has tuple type")) - | _ -> raise (Reporting_basic.err_unreachable l "overload variant does not have function")) - | _ -> + variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*) + (match t.t with + | Tfn(arg,ret,imp,ef') -> + (match arg.t,arg_t.t with + | Ttup([tlft;trght]),Ttup([tlft_t;trght_t]) -> + let (lft',rht',arg_t,cs_p,ef_p) = check_parms arg lft rht in + let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef lft' rht' in + (e',ret_t,t_env,cs_p@arg_cs@cs@cs_r,nob, + union_effects ef_r (union_effects ef_p (union_effects arg_ef ef'))) + |_ -> raise (Reporting_basic.err_unreachable l "function no longer has tuple type")) + | _ -> raise (Reporting_basic.err_unreachable l "overload variant does not have function")) + | _ -> typ_error l ("More than one variant of " ^ i ^ " found with type " ^ (t_to_string arg_t) ^ " -> " ^ (t_to_string expect_t) ^ ". A cast may be required"))) | _ -> typ_error l ("Unbound infix function " ^ i)) | E_tuple(exps) -> @@ -798,8 +812,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): if tl = el then let exps,typs,consts,effect = List.fold_right2 - (fun e t (exps,typs,consts,effect) -> - let (e',t',_,c,_,ef) = check_exp envs imp_param t e in ((e'::exps),(t'::typs),c@consts,union_effects ef effect)) + (fun e t (exps,typs,consts,effect) -> + let (e',t',_,c,_,ef) = check_exp envs imp_param 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,simple_annot t)),t,t_env,consts,nob,effect) @@ -807,14 +821,14 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | _ -> let exps,typs,consts,effect = List.fold_right - (fun e (exps,typs,consts,effect) -> - let (e',t,_,c,_,ef) = check_exp envs imp_param (new_t ()) e in - ((e'::exps),(t::typs),c@consts,union_effects ef effect)) - exps ([],[],[],pure_e) in + (fun e (exps,typs,consts,effect) -> + let (e',t,_,c,_,ef) = check_exp envs imp_param (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',ef',e' = - type_coerce (Expr l) d_env Guarantee false false b_env - t (E_aux(E_tuple(exps),(l,simple_annot t))) expect_t in + type_coerce (Expr l) d_env Guarantee false false b_env + t (E_aux(E_tuple(exps),(l,simple_annot t))) expect_t in (e',t',t_env,consts@cs',nob,union_effects ef' effect)) | E_if(cond,then_,else_) -> let (cond',_,_,c1,_,ef1) = check_exp envs imp_param bit_t cond in @@ -823,16 +837,16 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Tuvar _ -> let then',then_t,then_env,then_c,then_bs,then_ef = check_exp envs imp_param (new_t ()) then_ in let else',else_t,else_env,else_c,else_bs,else_ef = check_exp envs imp_param (new_t ()) else_ in - (*TOTHINK Possibly I should first consistency check else and then, with Guarantee, then check against expect_t with Require*) + (*TOTHINK Possibly I should first consistency check else and then, with Guarantee, then check against expect_t with Require*) let then_t',then_c' = type_consistent (Expr l) d_env Require true then_t expect_t in let else_t',else_c' = type_consistent (Expr l) d_env Require true else_t expect_t in let t_cs = CondCons((Expr l),Positive,None,c1p,then_c@then_c') in let e_cs = CondCons((Expr l),Negative,None,c1n,else_c@else_c') in (E_aux(E_if(cond',then',else'),(l,simple_annot expect_t)), expect_t, - Envmap.intersect_merge (tannot_merge (Expr l) d_env true) then_env else_env, - [BranchCons(Expr l, None, [t_cs;e_cs])], - merge_bounds then_bs else_bs, (*TODO Should be an intersecting merge*) + Envmap.intersect_merge (tannot_merge (Expr l) d_env true) then_env else_env, + [BranchCons(Expr l, None, [t_cs;e_cs])], + merge_bounds then_bs else_bs, (*TODO Should be an intersecting merge*) union_effects ef1 (union_effects then_ef else_ef)) | _ -> let then',then_t,then_env,then_c,then_bs,then_ef = check_exp envs imp_param expect_t then_ in @@ -841,30 +855,30 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let e_cs = CondCons((Expr l),Negative,None,[],else_c) in (E_aux(E_if(cond',then',else'),(l,simple_annot expect_t)), expect_t,Envmap.intersect_merge (tannot_merge (Expr l) d_env true) then_env else_env, - [BranchCons(Expr l, None, [t_cs;e_cs])], - merge_bounds then_bs else_bs, + [BranchCons(Expr l, None, [t_cs;e_cs])], + merge_bounds then_bs else_bs, union_effects ef1 (union_effects then_ef else_ef))) | E_for(id,from,to_,step,order,block) -> (*TOTHINK Instead of making up new ns here, perhaps I should instead make sure they conform to range without coercion as these nu variables might be floating*) let fb,fr,tb,tr,sb,sr = new_n(),new_n(),new_n(),new_n(),new_n(),new_n() in let ft,tt,st = {t=Tapp("range",[TA_nexp fb;TA_nexp fr])}, - {t=Tapp("range",[TA_nexp tb;TA_nexp tr])},{t=Tapp("range",[TA_nexp sb;TA_nexp sr])} in + {t=Tapp("range",[TA_nexp tb;TA_nexp tr])},{t=Tapp("range",[TA_nexp sb;TA_nexp sr])} in let from',from_t,_,from_c,_,from_ef = check_exp envs imp_param ft from in let to_',to_t,_,to_c,_,to_ef = check_exp envs imp_param tt to_ in let step',step_t,_,step_c,_,step_ef = check_exp envs imp_param st step in let new_annot,local_cs = - match (aorder_to_ord order).order with - | Oinc -> - (simple_annot {t=Tapp("range",[TA_nexp fb;TA_nexp tr])}, - [LtEq((Expr l),Guarantee ,fr,tr);LtEq((Expr l),Guarantee,fb,tb)]) - | Odec -> - (simple_annot {t=Tapp("range",[TA_nexp tb; TA_nexp fr])}, - [GtEq((Expr l),Guarantee,fr,tr);GtEq((Expr l),Guarantee,fb,tb)]) - | _ -> (typ_error l "Order specification in a foreach loop must be either inc or dec, not polymorphic") + match (aorder_to_ord order).order with + | Oinc -> + (simple_annot {t=Tapp("range",[TA_nexp fb;TA_nexp tr])}, + [LtEq((Expr l),Guarantee ,fr,tr);LtEq((Expr l),Guarantee,fb,tb)]) + | Odec -> + (simple_annot {t=Tapp("range",[TA_nexp tb; TA_nexp fr])}, + [GtEq((Expr l),Guarantee,fr,tr);GtEq((Expr l),Guarantee,fb,tb)]) + | _ -> (typ_error l "Order specification in a foreach loop must be either inc or dec, not polymorphic") in (*TODO Might want to extend bounds here for the introduced variable*) let (block',b_t,_,b_c,_,b_ef)= - check_exp (Env(d_env,Envmap.insert t_env (id_to_string id,new_annot),b_env,tp_env)) imp_param expect_t block + check_exp (Env(d_env,Envmap.insert t_env (id_to_string id,new_annot),b_env,tp_env)) imp_param expect_t block in (E_aux(E_for(id,from',to_',step',order,block'),(l,constrained_annot b_t local_cs)),expect_t,Envmap.empty, b_c@from_c@to_c@step_c@local_cs,nob,(union_effects b_ef (union_effects step_ef (union_effects to_ef from_ef)))) @@ -873,8 +887,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Tapp("vector",[base;rise;TA_ord ord;TA_typ item_t]) -> item_t,ord | _ -> new_t (),d_env.default_o in let es,cs,effect = (List.fold_right - (fun (e,_,_,c,_,ef) (es,cs,effect) -> (e::es),(c@cs),union_effects ef effect) - (List.map (check_exp envs imp_param item_t) es) ([],[],pure_e)) in + (fun (e,_,_,c,_,ef) (es,cs,effect) -> (e::es),(c@cs),union_effects ef effect) + (List.map (check_exp envs imp_param item_t) es) ([],[],pure_e)) in let len = List.length es in let t = match ord.order,d_env.default_o.order with | (Oinc,_) | (Ouvar _,Oinc) | (Ovar _,Oinc) -> @@ -884,9 +898,9 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): {t = Tapp("vector",[TA_nexp (mk_c_int (len-1)); TA_nexp (mk_c_int len); TA_ord {order= Odec}; TA_typ item_t])} - | _ -> raise (Reporting_basic.err_unreachable l "Default order was neither inc or dec") in + | _ -> raise (Reporting_basic.err_unreachable l "Default order was neither inc or dec") in let t',cs',ef',e' = type_coerce (Expr l) d_env Guarantee false false b_env t - (E_aux(E_vector es,(l,simple_annot t))) expect_t in + (E_aux(E_vector es,(l,simple_annot t))) expect_t in (e',t',t_env,cs@cs',nob,union_effects effect ef') | E_vector_indexed(eis,(Def_val_aux(default,(ld,annot)))) -> let item_t,base_n,rise_n = match expect_t.t with @@ -895,38 +909,38 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let first,last = fst (List.hd eis), fst (List.hd (List.rev eis)) in let is_increasing = first <= last in let es,cs,effect,contains_skip,_ = (List.fold_right - (fun ((i,e),c,ef) (es,cs,effect,skips,prev) -> - (*let _ = Printf.eprintf "Checking increasing %b %i %i\n" is_increasing prev i in*) + (fun ((i,e),c,ef) (es,cs,effect,skips,prev) -> + (*let _ = Printf.eprintf "Checking increasing %b %i %i\n" is_increasing prev i in*) 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) + 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 imp_param item_t e) in ((i,e),cs,eft)) - eis) ([],[],pure_e,false,(if is_increasing then (last+1) else (last-1)))) in + (List.map (fun (i,e) -> let (e,_,_,cs,_,eft) = (check_exp envs imp_param item_t e) in ((i,e),cs,eft)) + 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,simple_annot item_t)),true,[],pure_e) + | (Def_val_empty,false) -> (Def_val_aux(Def_val_empty,(ld,simple_annot item_t)),true,[],pure_e) | (Def_val_empty,true) -> let ef = add_effect (BE_aux(BE_unspec,l)) pure_e in - let (de,_,_,_,_,ef_d) = check_exp envs imp_param item_t (E_aux(E_lit (L_aux(L_undef,l)), (l,NoTyp))) in + let (de,_,_,_,_,ef_d) = check_exp envs imp_param item_t (E_aux(E_lit (L_aux(L_undef,l)), (l,NoTyp))) in (Def_val_aux(Def_val_dec de, (l, cons_ef_annot item_t [] ef)),false,[],ef) - | (Def_val_dec e,_) -> let (de,t,_,cs_d,_,ef_d) = (check_exp envs imp_param item_t e) in - (*Check that ef_d doesn't write to memory or registers? *) - (Def_val_aux(Def_val_dec de,(ld,cons_ef_annot item_t cs_d ef_d)),false,cs_d,ef_d) in + | (Def_val_dec e,_) -> let (de,t,_,cs_d,_,ef_d) = (check_exp envs imp_param item_t e) in + (*Check that ef_d doesn't write to memory or registers? *) + (Def_val_aux(Def_val_dec de,(ld,cons_ef_annot item_t cs_d ef_d)),false,cs_d,ef_d) in let (base_bound,length_bound,cs_bounds) = - if fully_enumerate - then (mk_c_int first, mk_c_int (List.length eis),[]) - else (base_n,rise_n,[LtEq(Expr l,Require, base_n,mk_c_int first); - GtEq(Expr l,Require, rise_n,mk_c_int (List.length eis))]) - in + if fully_enumerate + then (mk_c_int first, mk_c_int (List.length eis),[]) + else (base_n,rise_n,[LtEq(Expr l,Require, base_n,mk_c_int first); + GtEq(Expr l,Require, rise_n,mk_c_int (List.length eis))]) + in let t = {t = Tapp("vector", - [TA_nexp(base_bound);TA_nexp length_bound; - TA_ord({order= if is_increasing then Oinc else Odec});TA_typ item_t])} in + [TA_nexp(base_bound);TA_nexp length_bound; + TA_ord({order= if is_increasing then Oinc else Odec});TA_typ item_t])} in let t',cs',ef',e' = type_coerce (Expr l) d_env Require false false b_env t - (E_aux (E_vector_indexed(es,default'),(l,simple_annot t))) expect_t in + (E_aux (E_vector_indexed(es,default'),(l,simple_annot t))) expect_t in (e',t',t_env,cs@cs_d@cs_bounds@cs',nob,union_effects ef_d (union_effects ef' effect)) | E_vector_access(vec,i) -> let base,len,ord = new_n(),new_n(),new_o() in @@ -942,22 +956,23 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let oinc_max_access = mk_sub (mk_add base len) n_one in let odec_min_access = mk_sub base len in let cs_loc = - match (ord.order,d_env.default_o.order) with - | (Oinc,_) -> - [LtEq((Expr l),Require,base,min); - LtEq((Expr l),Require, max,oinc_max_access); LtEq((Expr l),Require, min,oinc_max_access)] - | (Odec,_) -> - [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require,min,odec_min_access); LtEq((Expr l),Require,max,odec_min_access)] - | (_,Oinc) -> - [LtEq((Expr l),Require,base,min); - LtEq((Expr l),Require, max,oinc_max_access); LtEq((Expr l),Require, min,oinc_max_access)] - | (_,Odec) -> - [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require,min,odec_min_access); LtEq((Expr l),Require,max,odec_min_access)] - | _ -> typ_error l "A vector must be either increasing or decreasing to access a single element" + match (ord.order,d_env.default_o.order) with + | (Oinc,_) -> + [LtEq((Expr l),Require,base,min); + LtEq((Expr l),Require, max,oinc_max_access); LtEq((Expr l),Require, min,oinc_max_access)] + | (Odec,_) -> + [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require,min,odec_min_access); LtEq((Expr l),Require,max,odec_min_access)] + | (_,Oinc) -> + [LtEq((Expr l),Require,base,min); + LtEq((Expr l),Require, max,oinc_max_access); LtEq((Expr l),Require, min,oinc_max_access)] + | (_,Odec) -> + [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require,min,odec_min_access); LtEq((Expr l),Require,max,odec_min_access)] + | _ -> typ_error l "A vector must be either increasing or decreasing to access a single element" in - (*let _ = Printf.eprintf "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 _ = Printf.eprintf "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',ef',e'=type_coerce (Expr l) d_env Require false false b_env item_t - (E_aux(E_vector_access(vec',i'),(l,simple_annot item_t))) expect_t in + (E_aux(E_vector_access(vec',i'),(l,simple_annot item_t))) expect_t in (e',t',t_env,cs_loc@cs_i@cs@cs',nob,union_effects ef (union_effects ef' ef_i)) | E_vector_subrange(vec,i1,i2) -> (*let _ = Printf.eprintf "checking e_vector_subrange: expect_t is %s\n" (t_to_string expect_t) in*) @@ -966,8 +981,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let n1_start = new_n() in let n2_end = new_n() in let item_t = match expect_t.t with - | Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> item_t - | _ -> new_t() in + | Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> item_t + | _ -> new_t() in let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp length;TA_ord ord;TA_typ item_t])} in let (vec',vt',_,cs,_,ef) = check_exp envs imp_param vt vec in let i1t = {t=Tapp("atom",[TA_nexp n1_start])} in @@ -975,68 +990,68 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let i2t = {t=Tapp("atom",[TA_nexp n2_end])} in let (i2', ti2, _,cs_i2,_,ef_i2) = check_exp envs imp_param i2t i2 in let cs_loc = - match (ord.order,d_env.default_o.order) with - | (Oinc,_) -> - [LtEq((Expr l), Require, base, n1_start); - LtEq((Expr l), Require, n1_start, n2_end); - LtEq((Expr l), Require, n2_end, mk_sub (mk_add base length) n_one); - Eq((Expr l), new_length, mk_add (mk_sub n2_end n1_start) n_one)] - | (Odec,_) -> - [GtEq((Expr l), Require, base, n1_start); - GtEq((Expr l), Require, n1_start, n2_end); - GtEq((Expr l), Require, n2_end, mk_add (mk_sub base length) n_one); - Eq((Expr l), new_length, mk_add (mk_sub n1_start n2_end) n_one)] - | (_,Oinc) -> - [LtEq((Expr l), Require, base, n1_start); - LtEq((Expr l), Require, n1_start, n2_end); - LtEq((Expr l), Require, n2_end, mk_sub (mk_add base length) n_one); - Eq((Expr l), new_length, mk_add (mk_sub n2_end n1_start) n_one)] - | (_,Odec) -> - [GtEq((Expr l), Require, base, n1_start); - GtEq((Expr l), Require, n1_start, n2_end); - GtEq((Expr l), Require, n2_end, mk_add (mk_sub base length) n_one); - Eq((Expr l), new_length, mk_add (mk_sub n1_start n2_end) n_one)] - | _ -> typ_error l "A vector must be either increasing or decreasing to access a slice" in + match (ord.order,d_env.default_o.order) with + | (Oinc,_) -> + [LtEq((Expr l), Require, base, n1_start); + LtEq((Expr l), Require, n1_start, n2_end); + LtEq((Expr l), Require, n2_end, mk_sub (mk_add base length) n_one); + Eq((Expr l), new_length, mk_add (mk_sub n2_end n1_start) n_one)] + | (Odec,_) -> + [GtEq((Expr l), Require, base, n1_start); + GtEq((Expr l), Require, n1_start, n2_end); + GtEq((Expr l), Require, n2_end, mk_add (mk_sub base length) n_one); + Eq((Expr l), new_length, mk_add (mk_sub n1_start n2_end) n_one)] + | (_,Oinc) -> + [LtEq((Expr l), Require, base, n1_start); + LtEq((Expr l), Require, n1_start, n2_end); + LtEq((Expr l), Require, n2_end, mk_sub (mk_add base length) n_one); + Eq((Expr l), new_length, mk_add (mk_sub n2_end n1_start) n_one)] + | (_,Odec) -> + [GtEq((Expr l), Require, base, n1_start); + GtEq((Expr l), Require, n1_start, n2_end); + GtEq((Expr l), Require, n2_end, mk_add (mk_sub base length) n_one); + Eq((Expr l), new_length, mk_add (mk_sub n1_start n2_end) n_one)] + | _ -> typ_error l "A vector must be either increasing or decreasing to access a slice" in let nt = {t = Tapp("vector", [TA_nexp n1_start; TA_nexp new_length; TA_ord ord; TA_typ item_t]) } in let (t,cs3,ef3,e') = - type_coerce (Expr l) d_env Require false false b_env nt - (E_aux(E_vector_subrange(vec',i1',i2'),(l,constrained_annot nt cs_loc))) expect_t in + type_coerce (Expr l) d_env Require false false b_env nt + (E_aux(E_vector_subrange(vec',i1',i2'),(l,constrained_annot nt cs_loc))) expect_t in (e',t,t_env,cs3@cs@cs_i1@cs_i2@cs_loc,nob,(union_effects ef (union_effects ef3 (union_effects ef_i1 ef_i2)))) | E_vector_update(vec,i,e) -> let base,rise,ord = new_n(),new_n(),new_o() in let min,m_rise = new_n(),new_n() in let item_t = match expect_t.t with - | Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> item_t - | _ -> new_t() in + | Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> item_t + | _ -> new_t() in let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ item_t])} in let (vec',t',_,cs,_,ef) = check_exp envs imp_param vt vec in let it = {t=Tapp("range",[TA_nexp min;TA_nexp m_rise])} in let (i', ti, _,cs_i,_,ef_i) = check_exp envs imp_param it i in let (e', te, _,cs_e,_,ef_e) = check_exp envs imp_param item_t e in let cs_loc = - match (ord.order,d_env.default_o.order) with - | (Oinc,_) -> - [LtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise,mk_add base rise)] - | (Odec,_) -> - [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise,mk_sub base rise)] - | (_,Oinc) -> - [LtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise, mk_add base rise)] - | (_,Odec) -> - [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise,mk_sub base rise)] - | _ -> typ_error l "A vector must be either increasing or decreasing to change a single element" + match (ord.order,d_env.default_o.order) with + | (Oinc,_) -> + [LtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise,mk_add base rise)] + | (Odec,_) -> + [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise,mk_sub base rise)] + | (_,Oinc) -> + [LtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise, mk_add base rise)] + | (_,Odec) -> + [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise,mk_sub base rise)] + | _ -> typ_error l "A vector must be either increasing or decreasing to change a single element" in let nt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise; TA_ord ord;TA_typ item_t])} in let (t,cs3,ef3,e') = - type_coerce (Expr l) d_env Require false false b_env nt - (E_aux(E_vector_update(vec',i',e'),(l,constrained_annot nt cs_loc))) expect_t in + type_coerce (Expr l) d_env Require false false b_env nt + (E_aux(E_vector_update(vec',i',e'),(l,constrained_annot nt cs_loc))) expect_t in (e',t,t_env,cs3@cs@cs_i@cs_e@cs_loc,nob,(union_effects ef (union_effects ef3 (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 let min1,m_rise1 = new_n(),new_n() in let min2,m_rise2 = new_n(),new_n() in let item_t = match expect_t.t with - | Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> item_t - | _ -> new_t() in + | Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> item_t + | _ -> new_t() in let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ item_t])} in let (vec',t',_,cs,_,ef) = check_exp envs imp_param vt vec in let i1t = {t=Tapp("range",[TA_nexp min1;TA_nexp m_rise1])} in @@ -1044,31 +1059,31 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let i2t = {t=Tapp("range",[TA_nexp min2;TA_nexp m_rise2])} in let (i2', ti2, _,cs_i2,_,ef_i2) = check_exp envs imp_param i2t i2 in let (e',item_t',_,cs_e,_,ef_e) = - try check_exp envs imp_param item_t e with - | _ -> - let (base_e,rise_e) = new_n(),new_n() in - let (e',ti',env_e,cs_e,bs_e,ef_e) = - check_exp envs imp_param {t=Tapp("vector",[TA_nexp base_e;TA_nexp rise_e;TA_ord ord;TA_typ item_t])} e - in - let cs_add = [Eq((Expr l),base_e,min1);LtEq((Expr l),Guarantee,rise,m_rise2)] in - (e',ti',env_e,cs_e@cs_add,bs_e,ef_e) in + try check_exp envs imp_param item_t e with + | _ -> + let (base_e,rise_e) = new_n(),new_n() in + let (e',ti',env_e,cs_e,bs_e,ef_e) = + check_exp envs imp_param {t=Tapp("vector",[TA_nexp base_e;TA_nexp rise_e;TA_ord ord;TA_typ item_t])} e + in + let cs_add = [Eq((Expr l),base_e,min1);LtEq((Expr l),Guarantee,rise,m_rise2)] in + (e',ti',env_e,cs_e@cs_add,bs_e,ef_e) in let cs_loc = - match (ord.order,d_env.default_o.order) with - | (Oinc,_) -> - [LtEq((Expr l),Require,base,min1); LtEq((Expr l),Require,mk_add min1 m_rise1,mk_add min2 m_rise2); - LtEq((Expr l),Require,mk_add min2 m_rise2,mk_add base rise);] - | (Odec,_) -> - [GtEq((Expr l),Require,base,mk_add min1 m_rise1); - GtEq((Expr l),Require,mk_add min1 m_rise1,mk_add min2 m_rise2); - GtEq((Expr l),Require,mk_add min2 m_rise2,mk_sub base rise);] - | (_,Oinc) -> - [LtEq((Expr l),Require,base,min1); LtEq((Expr l),Require,mk_add min1 m_rise1,mk_add min2 m_rise2); - LtEq((Expr l),Require,mk_add min2 m_rise2,mk_add base rise);] - | (_,Odec) -> - [GtEq((Expr l),Require,base,mk_add min1 m_rise1); - GtEq((Expr l),Require,mk_add min1 m_rise1,mk_add min2 m_rise2); - GtEq((Expr l),Require,mk_add min2 m_rise2,mk_sub base rise);] - | _ -> typ_error l "A vector must be either increasing or decreasing to modify a slice" in + match (ord.order,d_env.default_o.order) with + | (Oinc,_) -> + [LtEq((Expr l),Require,base,min1); LtEq((Expr l),Require,mk_add min1 m_rise1,mk_add min2 m_rise2); + LtEq((Expr l),Require,mk_add min2 m_rise2,mk_add base rise);] + | (Odec,_) -> + [GtEq((Expr l),Require,base,mk_add min1 m_rise1); + GtEq((Expr l),Require,mk_add min1 m_rise1,mk_add min2 m_rise2); + GtEq((Expr l),Require,mk_add min2 m_rise2,mk_sub base rise);] + | (_,Oinc) -> + [LtEq((Expr l),Require,base,min1); LtEq((Expr l),Require,mk_add min1 m_rise1,mk_add min2 m_rise2); + LtEq((Expr l),Require,mk_add min2 m_rise2,mk_add base rise);] + | (_,Odec) -> + [GtEq((Expr l),Require,base,mk_add min1 m_rise1); + GtEq((Expr l),Require,mk_add min1 m_rise1,mk_add min2 m_rise2); + GtEq((Expr l),Require,mk_add min2 m_rise2,mk_sub base rise);] + | _ -> 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,ef3,e') = type_coerce (Expr l) d_env Require false false b_env nt (E_aux(E_vector_update_subrange(vec',i1',i2',e'),(l,constrained_annot nt cs_loc))) expect_t in @@ -1077,166 +1092,166 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let item_t,ord = match expect_t.t with | Tapp("vector",[_;_;TA_ord o;TA_typ i]) -> i,o | Tapp("range",_) -> bit_t,new_o () - | Tapp("atom",_) -> bit_t, new_o () + | Tapp("atom",_) -> bit_t, new_o () | _ -> new_t (),new_o () in let base1,rise1 = new_n(), new_n() in let base2,rise2 = new_n(),new_n() in let (v1',t1',_,cs_1,_,ef_1) = - check_exp envs imp_param {t=Tapp("vector",[TA_nexp base1;TA_nexp rise1;TA_ord ord;TA_typ item_t])} v1 in + check_exp envs imp_param {t=Tapp("vector",[TA_nexp base1;TA_nexp rise1;TA_ord ord;TA_typ item_t])} v1 in let (v2',t2',_,cs_2,_,ef_2) = - check_exp envs imp_param {t=Tapp("vector",[TA_nexp base2;TA_nexp rise2;TA_ord ord;TA_typ item_t])} v2 in + check_exp envs imp_param {t=Tapp("vector",[TA_nexp base2;TA_nexp rise2;TA_ord ord;TA_typ item_t])} v2 in let ti = {t=Tapp("vector",[TA_nexp base1;TA_nexp (mk_add rise1 rise2);TA_ord ord; TA_typ item_t])} in let cs_loc = match ord.order with | Odec -> [GtEq((Expr l),Require,base1,mk_add rise1 rise2)] | _ -> [] in let (t,cs_c,ef_c,e') = type_coerce (Expr l) d_env Require false false b_env ti - (E_aux(E_vector_append(v1',v2'),(l,constrained_annot ti cs_loc))) expect_t in + (E_aux(E_vector_append(v1',v2'),(l,constrained_annot ti cs_loc))) expect_t in (e',t,t_env,cs_loc@cs_1@cs_2,nob,(union_effects ef_c (union_effects ef_1 ef_2))) | E_list(es) -> let item_t = match expect_t.t with - | Tapp("list",[TA_typ i]) -> i - | _ -> new_t() in + | Tapp("list",[TA_typ i]) -> i + | _ -> new_t() in let es,cs,effect = - (List.fold_right (fun (e,_,_,c,_,ef) (es,cs,effect) -> (e::es),(c@cs),union_effects ef effect) - (List.map (check_exp envs imp_param item_t) es) ([],[],pure_e)) in + (List.fold_right (fun (e,_,_,c,_,ef) (es,cs,effect) -> (e::es),(c@cs),union_effects ef effect) + (List.map (check_exp envs imp_param item_t) es) ([],[],pure_e)) in let t = {t = Tapp("list",[TA_typ item_t])} in let t',cs',ef',e' = type_coerce (Expr l) d_env Require false false b_env t - (E_aux(E_list es,(l,simple_annot t))) expect_t in + (E_aux(E_list es,(l,simple_annot t))) expect_t in (e',t',t_env,cs@cs',nob,union_effects ef' effect) | E_cons(ls,i) -> let item_t = match expect_t.t with - | Tapp("list",[TA_typ i]) -> i - | _ -> new_t() in + | Tapp("list",[TA_typ i]) -> i + | _ -> new_t() in let lt = {t=Tapp("list",[TA_typ item_t])} in let (ls',t',_,cs,_,ef) = check_exp envs imp_param lt ls in let (i', ti, _,cs_i,_,ef_i) = check_exp envs imp_param item_t i in let (t',cs',ef',e') = - type_coerce (Expr l) d_env Require false false b_env lt (E_aux(E_cons(ls',i'),(l,simple_annot lt))) expect_t in + type_coerce (Expr l) d_env Require false false b_env lt (E_aux(E_cons(ls',i'),(l,simple_annot lt))) expect_t in (e',t',t_env,cs@cs'@cs_i,nob,union_effects ef' (union_effects ef ef_i)) | E_record(FES_aux(FES_Fexps(fexps,_),l')) -> let u,_ = get_abbrev d_env expect_t in let u_actual = match u.t with | Tabbrev(_, u) -> u | _ -> u in let field_walker r subst_env bounds tag n = - (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 -> - typ_error l ("Expected a struct of type " ^ n ^ ", which should not have a field " ^ i) + (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 -> + typ_error l ("Expected a struct of type " ^ n ^ ", which should not have a field " ^ i) | Some(ft) -> - let ft = typ_subst subst_env false ft in - let (e,t',_,c,_,ef) = check_exp envs imp_param ft exp in - (FE_aux(FE_Fexp(id,e),(l,Base(([],t'),tag,c,ef,bounds)))::fexps,cons@c,union_effects ef ef')) in + let ft = typ_subst subst_env false ft in + let (e,t',_,c,_,ef) = check_exp envs imp_param ft exp in + (FE_aux(FE_Fexp(id,e),(l,Base(([],t'),tag,c,ef,bounds)))::fexps,cons@c,union_effects ef ef')) in (match u_actual.t with - | Tid(n) | Tapp(n,_)-> - (match lookup_record_typ n d_env.rec_env with - | Some(((i,Record,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) -> - let (ts,cs,eft,subst_env) = subst params false t cs eft in - if (List.length fexps = List.length fields) - then let fexps,cons,ef = List.fold_right (field_walker r subst_env bounds tag n) fexps ([],[],pure_e) in - let e = E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,simple_annot u)) in - let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in - (e',t',t_env,cs@cons@cs',nob,union_effects ef ef') - else typ_error l ("Expected a struct of type " ^ n ^ ", which should have " ^ string_of_int (List.length fields) ^ " fields") - | Some(i,Register,tannot,fields) -> typ_error l ("Expected a value with register type, found a struct") - | _ -> typ_error l ("Expected a value of type " ^ n ^ " but found a struct")) - | Tuvar _ -> - let field_names = List.map (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) -> id_to_string id) fexps in - (match lookup_record_fields field_names d_env.rec_env with - | Some(((i,Record,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) -> - let (ts,cs,eft,subst_env) = subst params false t cs eft in - let fexps,cons,ef = List.fold_right (field_walker r subst_env bounds tag i) fexps ([],[],pure_e) in - let e = E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,simple_annot ts)) in - let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in - (e',t',t_env,cs@cons@cs',nob,union_effects ef ef') - | Some(i,Register,tannot,fields) -> typ_error l "Expected a value with register type, found a struct" - | _ -> typ_error l "No struct type matches the set of fields given") - | _ -> typ_error l ("Expected an expression of type " ^ t_to_string expect_t ^ " but found a struct")) + | Tid(n) | Tapp(n,_)-> + (match lookup_record_typ n d_env.rec_env with + | Some(((i,Record,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) -> + let (ts,cs,eft,subst_env) = subst params false t cs eft in + if (List.length fexps = List.length fields) + then let fexps,cons,ef = List.fold_right (field_walker r subst_env bounds tag n) fexps ([],[],pure_e) in + let e = E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,simple_annot u)) in + let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in + (e',t',t_env,cs@cons@cs',nob,union_effects ef ef') + else typ_error l ("Expected a struct of type " ^ n ^ ", which should have " ^ string_of_int (List.length fields) ^ " fields") + | Some(i,Register,tannot,fields) -> typ_error l ("Expected a value with register type, found a struct") + | _ -> typ_error l ("Expected a value of type " ^ n ^ " but found a struct")) + | Tuvar _ -> + let field_names = List.map (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) -> id_to_string id) fexps in + (match lookup_record_fields field_names d_env.rec_env with + | Some(((i,Record,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) -> + let (ts,cs,eft,subst_env) = subst params false t cs eft in + let fexps,cons,ef = List.fold_right (field_walker r subst_env bounds tag i) fexps ([],[],pure_e) in + let e = E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,simple_annot ts)) in + let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in + (e',t',t_env,cs@cons@cs',nob,union_effects ef ef') + | Some(i,Register,tannot,fields) -> typ_error l "Expected a value with register type, found a struct" + | _ -> typ_error l "No struct type matches the set of fields given") + | _ -> 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')) -> let (e',t',_,c,_,ef) = check_exp envs imp_param expect_t exp in let field_walker r subst_env bounds tag i = - (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 -> typ_error l ("Expected a struct with type " ^ i ^ ", which does not have a field " ^ fi) + (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 -> typ_error l ("Expected a struct with type " ^ i ^ ", which does not have a field " ^ fi) | Some ft -> - let ft = typ_subst subst_env false ft in - let (e,t',_,c,_,ef) = check_exp envs imp_param ft exp in - (FE_aux(FE_Fexp(id,e),(l,Base(([],t'),tag,c,ef,bounds)))::fexps,cons@c,union_effects ef ef')) in + let ft = typ_subst subst_env false ft in + let (e,t',_,c,_,ef) = check_exp envs imp_param ft exp in + (FE_aux(FE_Fexp(id,e),(l,Base(([],t'),tag,c,ef,bounds)))::fexps,cons@c,union_effects ef ef')) in (match t'.t with - | Tid i | Tabbrev(_, {t=Tid i}) | Tapp(i,_) -> - (match lookup_record_typ i d_env.rec_env with - | Some((i,Register,tannot,fields)) -> typ_error l "Expected a struct for this update, instead found a register" - | Some(((i,Record,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) -> - if (List.length fexps <= List.length fields) - then - let (ts,cs,eft,subst_env) = subst params false t cs eft in - let fexps,cons,ef = List.fold_right (field_walker r subst_env bounds tag i) fexps ([],[],pure_e) in - let e = E_aux(E_record_update(e',FES_aux(FES_Fexps(fexps,false),l')), (l,simple_annot ts)) in - let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in - (e',t',t_env,cs@cons@cs',nob,union_effects ef ef') - else typ_error l ("Expected fields from struct " ^ i ^ ", given more fields than struct includes") - | _ -> - typ_error l ("Expected a struct or register for this access, instead found an expression with type " ^ i)) - | Tuvar _ -> - let field_names = List.map (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) -> id_to_string id) fexps in - (match lookup_possible_records field_names d_env.rec_env with - | [] -> typ_error l "No struct matches the set of fields given for this struct update" - | [(((i,Record,(Base((params,t),tag,cs,eft,bounds)),fields) as r))] -> - let (ts,cs,eft,subst_env) = subst params false t cs eft in - let fexps,cons,ef = List.fold_right (field_walker r subst_env bounds tag i) fexps ([],[],pure_e) in - let e = E_aux(E_record_update(e',FES_aux(FES_Fexps(fexps,false),l')), (l,simple_annot ts)) in - let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in - (e',t',t_env,cs@cons@cs',nob,union_effects ef ef') - | [(i,Register,tannot,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)) + | Tid i | Tabbrev(_, {t=Tid i}) | Tapp(i,_) -> + (match lookup_record_typ i d_env.rec_env with + | Some((i,Register,tannot,fields)) -> typ_error l "Expected a struct for this update, instead found a register" + | Some(((i,Record,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) -> + if (List.length fexps <= List.length fields) + then + let (ts,cs,eft,subst_env) = subst params false t cs eft in + let fexps,cons,ef = List.fold_right (field_walker r subst_env bounds tag i) fexps ([],[],pure_e) in + let e = E_aux(E_record_update(e',FES_aux(FES_Fexps(fexps,false),l')), (l,simple_annot ts)) in + let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in + (e',t',t_env,cs@cons@cs',nob,union_effects ef ef') + else typ_error l ("Expected fields from struct " ^ i ^ ", given more fields than struct includes") + | _ -> + typ_error l ("Expected a struct or register for this access, instead found an expression with type " ^ i)) + | Tuvar _ -> + let field_names = List.map (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) -> id_to_string id) fexps in + (match lookup_possible_records field_names d_env.rec_env with + | [] -> typ_error l "No struct matches the set of fields given for this struct update" + | [(((i,Record,(Base((params,t),tag,cs,eft,bounds)),fields) as r))] -> + let (ts,cs,eft,subst_env) = subst params false t cs eft in + let fexps,cons,ef = List.fold_right (field_walker r subst_env bounds tag i) fexps ([],[],pure_e) in + let e = E_aux(E_record_update(e',FES_aux(FES_Fexps(fexps,false),l')), (l,simple_annot ts)) in + let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in + (e',t',t_env,cs@cons@cs',nob,union_effects ef ef') + | [(i,Register,tannot,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)) | E_field(exp,id) -> let (e',t',_,c_sub,_,ef_sub) = check_exp envs imp_param (new_t()) exp in let fi = id_to_string id in (match t'.t with | Tabbrev({t=Tid i}, _) | Tabbrev({t=Tapp(i,_)},_) | Tid i | Tapp(i,_) -> - (match lookup_record_typ i d_env.rec_env with - | Some(((i,rec_kind,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) -> - let (ts,cs,eft,subst_env) = subst params false t cs eft in - (match lookup_field_type fi r with - | None -> typ_error l ("Type " ^ i ^ " does not have a field " ^ fi) + (match lookup_record_typ i d_env.rec_env with + | Some(((i,rec_kind,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) -> + let (ts,cs,eft,subst_env) = subst params false t cs eft in + (match lookup_field_type fi r with + | None -> typ_error l ("Type " ^ i ^ " does not have a field " ^ fi) | Some t -> - let ft = typ_subst subst_env false t in - let (_,cs_sub') = type_consistent (Expr l) d_env Guarantee false ts t' in - let (et',c',ef',acc) = - type_coerce (Expr l) d_env Require false false b_env ft - (E_aux(E_field(e',id),(l,Base(([],ft),tag,cs,eft,bounds)))) expect_t in - (acc,et',t_env,cs@c'@c_sub@cs_sub',nob,union_effects ef' ef_sub)) - | _ -> - typ_error l ("Expected a struct or register for this access, instead found an expression with type " ^ i)) - | Tuvar _ -> - (match lookup_possible_records [fi] d_env.rec_env with - | [] -> typ_error l ("No struct or register has a field " ^ fi) - | [(((i,rkind,(Base((params,t),tag,cs,eft,bounds)),fields) as r))] -> - let (ts,cs,eft,subst_env) = subst params false t cs eft in - (match lookup_field_type fi r with - | None -> - raise (Reporting_basic.err_unreachable l "lookup_possible_records returned a record that didn't include the field") + let ft = typ_subst subst_env false t in + let (_,cs_sub') = type_consistent (Expr l) d_env Guarantee false ts t' in + let (et',c',ef',acc) = + type_coerce (Expr l) d_env Require false false b_env ft + (E_aux(E_field(e',id),(l,Base(([],ft),tag,cs,eft,bounds)))) expect_t in + (acc,et',t_env,cs@c'@c_sub@cs_sub',nob,union_effects ef' ef_sub)) + | _ -> + typ_error l ("Expected a struct or register for this access, instead found an expression with type " ^ i)) + | Tuvar _ -> + (match lookup_possible_records [fi] d_env.rec_env with + | [] -> typ_error l ("No struct or register has a field " ^ fi) + | [(((i,rkind,(Base((params,t),tag,cs,eft,bounds)),fields) as r))] -> + let (ts,cs,eft,subst_env) = subst params false t cs eft in + (match lookup_field_type fi r with + | None -> + raise (Reporting_basic.err_unreachable l "lookup_possible_records returned a record that didn't include the field") | Some t -> - let ft = typ_subst subst_env false t in - let (_,cs_sub') = type_consistent (Expr l) d_env Guarantee false ts t' in - let (et',c',ef',acc) = - type_coerce (Expr l) d_env Require false false b_env ft - (E_aux(E_field(e',id),(l,Base(([],ft),tag,cs,eft,bounds)))) expect_t in - (acc,et',t_env,cs@c'@c_sub@cs_sub',nob,union_effects ef' ef_sub)) - | records -> typ_error l ("Multiple structs or registers 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')) + let ft = typ_subst subst_env false t in + let (_,cs_sub') = type_consistent (Expr l) d_env Guarantee false ts t' in + let (et',c',ef',acc) = + type_coerce (Expr l) d_env Require false false b_env ft + (E_aux(E_field(e',id),(l,Base(([],ft),tag,cs,eft,bounds)))) expect_t in + (acc,et',t_env,cs@c'@c_sub@cs_sub',nob,union_effects ef' ef_sub)) + | records -> typ_error l ("Multiple structs or registers 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')) | E_case(exp,pexps) -> let (e',t',_,cs,_,ef) = check_exp envs imp_param (new_t()) exp in (*let _ = Printf.eprintf "Type of pattern after expression check %s\n" (t_to_string t') in*) let t' = - match t'.t with - | Tapp("register",[TA_typ t]) -> t - | _ -> t' in + match t'.t with + | Tapp("register",[TA_typ t]) -> t + | _ -> t' in (*let _ = Printf.eprintf "Type of pattern after register check %s\n" (t_to_string t') in*) let (pexps',t,cs',ef') = - check_cases envs imp_param t' expect_t (if (List.length pexps) = 1 then Solo else Switch) pexps in + check_cases envs imp_param t' expect_t (if (List.length pexps) = 1 then Solo else Switch) pexps in (*let _ = Printf.eprintf "Type of pattern after exps check %s\n%!" (t_to_string t') in let _ = Printf.eprintf "Type of expected after exps check %s\n%!" (t_to_string t) in let _ = Printf.eprintf "Pattern constraints : %s\n%!" (constraints_to_string cs) in*) @@ -1244,7 +1259,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | E_let(lbind,body) -> let (lb',t_env',cs,b_env',ef) = (check_lbind envs imp_param false Emp_local lbind) in let new_env = - (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env false) t_env t_env', merge_bounds b_env' b_env,tp_env)) + (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env false) t_env t_env', merge_bounds b_env' b_env,tp_env)) in let (e,t,_,cs',_,ef') = check_exp new_env imp_param expect_t body in (E_aux(E_let(lb',e),(l,simple_annot t)),t,t_env,cs@cs',nob,union_effects ef ef') @@ -1258,7 +1273,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): (E_aux (E_exit e',(l,(simple_annot expect_t))),expect_t,t_env,[],nob,pure_e) | E_internal_cast _ | E_internal_exp _ | E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker") - + and check_block envs imp_param expect_t exps:((tannot exp) list * tannot * nexp_range list * t * effect) = let Env(d_env,t_env,b_env,tp_env) = envs in match exps with @@ -1270,8 +1285,8 @@ and check_block envs imp_param expect_t exps:((tannot exp) list * tannot * nexp_ let (e',t',t_env',sc,b_env',ef') = check_exp envs imp_param unit_t e in let (exps',annot',sc',t,ef) = check_block (Env(d_env, - Envmap.union_merge (tannot_merge (Expr Parse_ast.Unknown) d_env false) t_env t_env', - merge_bounds b_env' b_env, tp_env)) imp_param expect_t exps in + Envmap.union_merge (tannot_merge (Expr Parse_ast.Unknown) d_env false) t_env t_env', + merge_bounds b_env' b_env, tp_env)) imp_param expect_t exps in ((e'::exps'),annot',sc@sc',t,union_effects ef ef') and check_cases envs imp_param check_t expect_t kind pexps : ((tannot pexp) list * typ * nexp_range list * effect) = @@ -1281,17 +1296,17 @@ and check_cases envs imp_param check_t expect_t kind pexps : ((tannot pexp) list | [(Pat_aux(Pat_exp(pat,exp),(l,annot)))] -> let pat',env,cs_p,bounds,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 true) t_env env, - merge_bounds b_env bounds, tp_env)) imp_param expect_t exp in + check_exp (Env(d_env, + Envmap.union_merge (tannot_merge (Expr l) d_env true) t_env env, + merge_bounds b_env bounds, tp_env)) imp_param expect_t exp in let cs = [CondCons(Expr l,kind,None, cs_p, cs_e)] in [Pat_aux(Pat_exp(pat',e),(l,cons_ef_annot t cs ef))],t,cs,ef | ((Pat_aux(Pat_exp(pat,exp),(l,annot)))::pexps) -> let pat',env,cs_p,bounds,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 true) t_env env, - merge_bounds b_env bounds, tp_env)) imp_param expect_t exp in + check_exp (Env(d_env, + Envmap.union_merge (tannot_merge (Expr l) d_env true) t_env env, + merge_bounds b_env bounds, tp_env)) imp_param expect_t exp in let cs = CondCons(Expr l,kind,None,cs_p,cs_e) in let (pes,tl,csl,efl) = check_cases envs imp_param check_t expect_t kind pexps in ((Pat_aux(Pat_exp(pat',e),(l,cons_ef_annot t [cs] ef)))::pes,tl,cs::csl,union_effects efl ef) @@ -1303,233 +1318,236 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) | LEXP_id id -> let i = id_to_string id in (match Envmap.apply t_env i with - (*TODO Should change this to use the default as the expected type*) - | Some(Base((parms,t),Default,_,_,_)) -> - typ_error l ("Identifier " ^ i ^ " cannot be assigned when only a default specification exists") + (*TODO Should change this to use the default as the expected type*) + | Some(Base((parms,t),Default,_,_,_)) -> + typ_error l ("Identifier " ^ i ^ " cannot be assigned when only a default specification exists") | Some(Base(([],t),Alias,_,_,_)) -> - let ef = {effect = Eset[BE_aux(BE_wreg,l)]} in + let ef = {effect = Eset[BE_aux(BE_wreg,l)]} in (match Envmap.apply d_env.alias_env i with | Some(OneReg(reg, (Base(([],t'),_,_,_,_)))) -> (LEXP_aux(lexp,(l,(Base(([],t'),Alias,[],ef,nob)))), t, false, Envmap.empty, External (Some reg),[],nob,ef) | Some(TwoReg(reg1,reg2, (Base(([],t'),_,_,_,_)))) -> - let u = match t.t with - | Tapp("register", [TA_typ u]) -> u - | _ -> raise (Reporting_basic.err_unreachable l "TwoReg didn't contain a register type") in + let u = match t.t with + | Tapp("register", [TA_typ u]) -> u + | _ -> raise (Reporting_basic.err_unreachable l "TwoReg didn't contain a register type") in (LEXP_aux(lexp,(l,Base(([],t'),Alias,[],ef,nob))), u, false, Envmap.empty, External None,[],nob,ef) | _ -> assert false) - | Some(Base((parms,t),tag,cs,_,b)) -> - let t,cs,_,_ = - match tag with | External _ | Emp_global -> subst parms false t cs pure_e | _ -> t,cs,pure_e,Envmap.empty - in - let t,cs' = get_abbrev d_env t in + | Some(Base((parms,t),tag,cs,_,b)) -> + let t,cs,_,_ = + match tag with | External _ | Emp_global -> subst parms false t cs pure_e | _ -> t,cs,pure_e,Envmap.empty + in + let t,cs' = get_abbrev d_env t in let t_actual = match t.t with | Tabbrev(i,t) -> t | _ -> t in - let cs_o = cs@cs' in + let cs_o = cs@cs' in (*let _ = Printf.eprintf "Assigning to %s, t is %s\n" i (t_to_string t_actual) in*) - (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,(Base(([],t),External (Some i),cs_o,ef,nob)))),u,false, - Envmap.empty,External (Some i),[],nob,ef) - | Tapp("reg",[TA_typ u]),_ -> - (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs_o,pure_e,b)))),u,false, - Envmap.empty,Emp_local,[],nob,pure_e) - | Tapp("vector",_),false -> - (LEXP_aux(lexp,(l,(Base(([],t),tag,cs_o,pure_e,b)))),t,true,Envmap.empty,Emp_local,[],nob,pure_e) - | (Tfn _ ,_) -> - (match tag with - | External _ | Spec | Emp_global -> - let u = new_t() in - let t = {t = Tapp("reg",[TA_typ u])} in - let bounds = extract_bounds d_env i t in - let tannot = (Base(([],t),Emp_local,[],pure_e,bounds)) in - (LEXP_aux(lexp,(l,tannot)),u,false,Envmap.from_list [i,tannot],Emp_local,[],bounds,pure_e) - | _ -> - typ_error l ("Cannot assign to " ^ i ^" with type " ^ t_to_string t ^ - ". Assignment must be to registers or non-parameter, non-let-bound local variables.")) - | _,_ -> - if is_top - then - typ_error l ("Cannot assign to " ^ i ^" with type " ^ t_to_string t ^ - ". Assignment must be to registers or non-parameter, non-let-bound local variables.") - else - (LEXP_aux(lexp,(l,constrained_annot t cs_o)),t,true,Envmap.empty,Emp_local,[],nob,pure_e)) - | _ -> - let u = new_t() in - let t = {t=Tapp("reg",[TA_typ u])} in - let bounds = extract_bounds d_env i u in - let tannot = (Base(([],t),Emp_local,[],pure_e,bounds)) in - (LEXP_aux(lexp,(l,tannot)),u,false,Envmap.from_list [i,tannot],Emp_local,[],bounds,pure_e)) + (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,(Base(([],t),External (Some i),cs_o,ef,nob)))),u,false, + Envmap.empty,External (Some i),[],nob,ef) + | Tapp("reg",[TA_typ u]),_ -> + (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs_o,pure_e,b)))),u,false, + Envmap.empty,Emp_local,[],nob,pure_e) + | Tapp("vector",_),false -> + (LEXP_aux(lexp,(l,(Base(([],t),tag,cs_o,pure_e,b)))),t,true,Envmap.empty,Emp_local,[],nob,pure_e) + | (Tfn _ ,_) -> + (match tag with + | External _ | Spec | Emp_global -> + let u = new_t() in + let t = {t = Tapp("reg",[TA_typ u])} in + let bounds = extract_bounds d_env i t in + let tannot = (Base(([],t),Emp_local,[],pure_e,bounds)) in + (LEXP_aux(lexp,(l,tannot)),u,false,Envmap.from_list [i,tannot],Emp_local,[],bounds,pure_e) + | _ -> + typ_error l ("Cannot assign to " ^ i ^" with type " ^ t_to_string t ^ + ". Assignment must be to registers or non-parameter, non-let-bound local variables.")) + | _,_ -> + if is_top + then + typ_error l ("Cannot assign to " ^ i ^" with type " ^ t_to_string t ^ + ". Assignment must be to registers or non-parameter, non-let-bound local variables.") + else + (LEXP_aux(lexp,(l,constrained_annot t cs_o)),t,true,Envmap.empty,Emp_local,[],nob,pure_e)) + | _ -> + let u = new_t() in + let t = {t=Tapp("reg",[TA_typ u])} in + let bounds = extract_bounds d_env i u in + let tannot = (Base(([],t),Emp_local,[],pure_e,bounds)) in + (LEXP_aux(lexp,(l,tannot)),u,false,Envmap.from_list [i,tannot],Emp_local,[],bounds,pure_e)) | LEXP_memory(id,exps) -> let i = id_to_string id in (match Envmap.apply t_env i with - | Some(Base((parms,t),tag,cs,ef,_)) -> - let is_external = match tag with | External any -> true | _ -> false in - let t,cs,ef,_ = subst parms false t cs ef in - (match t.t with - | Tfn(apps,out,_,ef') -> - (match ef'.effect with - | Eset effects -> - let mem_write = List.exists (fun (BE_aux(b,_)) -> match b with | BE_wmem -> true | _ -> false) effects in - let memv_write = List.exists (fun (BE_aux(b,_)) -> match b with |BE_wmv -> true | _ -> false) effects in - let reg_write = List.exists (fun (BE_aux(b,_)) -> match b with | BE_wreg -> true | _ -> false) effects in - if (mem_write || memv_write || reg_write) - then + | Some(Base((parms,t),tag,cs,ef,_)) -> + (*let is_external = match tag with | External any -> true | _ -> false in*) + let t,cs,ef,_ = subst parms false t cs ef in + (match t.t with + | Tfn(apps,out,_,ef') -> + (match ef'.effect with + | Eset effects -> + let mem_write = List.exists (fun (BE_aux(b,_)) -> + match b with | BE_wmem -> true | _ -> false) effects in + let memv_write = List.exists (fun (BE_aux(b,_)) -> + match b with |BE_wmv -> true | _ -> false) effects in + let reg_write = List.exists (fun (BE_aux(b,_)) -> + match b with | BE_wreg -> true | _ -> false) effects in + if (mem_write || memv_write || reg_write) + then let app,cs_a = get_abbrev d_env apps in let out,cs_o = get_abbrev d_env out in - let cs_call = cs@cs_o@cs_a in + let cs_call = cs@cs_o@cs_a in (match app.t with - | Ttup ts | Tabbrev(_,{t=Ttup ts}) -> - let (args,item_t) = ((fun ts -> (List.rev (List.tl ts), List.hd ts)) (List.rev ts)) in - let args_t = {t = Ttup args} in - let (es, cs_es, ef_es) = - match args,exps with - | [],[] -> ([],[],pure_e) - | [],[e] -> let (e',_,_,cs_e,_,ef_e) = check_exp envs imp_param unit_t e in ([e'],cs_e,ef_e) - | [],es -> typ_error l ("Expected no arguments for assignment function " ^ i) - | args,[] -> - typ_error l ("Expected arguments with types " ^ (t_to_string args_t) ^ - "for assignment function " ^ i) - | args,es -> - (match check_exp envs imp_param args_t (E_aux (E_tuple exps,(l,NoTyp))) with - | (E_aux(E_tuple es,(l',tannot)),_,_,cs_e,_,ef_e) -> (es,cs_e,ef_e) - | _ -> - raise (Reporting_basic.err_unreachable l - "Gave check_exp a tuple, didn't get a tuple back")) - in - let ef_all = union_effects ef' ef_es in - (LEXP_aux(LEXP_memory(id,es),(l,Base(([],out),tag,cs_call,ef',nob))), - item_t,false,Envmap.empty,tag,cs_call@cs_es,nob,ef_all) - | _ -> - let e = match exps with - | [] -> E_aux(E_lit(L_aux(L_unit,l)),(l,NoTyp)) - | [(E_aux(E_lit(L_aux(L_unit,_)),(_,NoTyp)) as e)] -> e - | es -> typ_error l ("Expected no arguments for assignment function " ^ i) in - let (e,_,_,cs_e,_,ef_e) = check_exp envs imp_param apps e in - let ef_all = union_effects ef ef_e in - (LEXP_aux(LEXP_memory(id,[e]),(l,Base(([],out),tag,cs_call,ef,nob))), - app,false,Envmap.empty,tag,cs_call@cs_e,nob,ef_all)) - else typ_error l ("Assignments require functions with a wmem, wmv, or wreg effect") - | _ -> typ_error l ("Assignments require functions with a wmem, wmv, or wreg effect")) - | _ -> typ_error l ("Assignments require a function here, found " ^ i ^ " which has type " ^ (t_to_string t))) - | _ -> typ_error l ("Unbound identifier " ^ i)) + | Ttup ts | Tabbrev(_,{t=Ttup ts}) -> + let (args,item_t) = ((fun ts -> (List.rev (List.tl ts), List.hd ts)) (List.rev ts)) in + let args_t = {t = Ttup args} in + let (es, cs_es, ef_es) = + match args,exps with + | [],[] -> ([],[],pure_e) + | [],[e] -> let (e',_,_,cs_e,_,ef_e) = check_exp envs imp_param unit_t e in ([e'],cs_e,ef_e) + | [],es -> typ_error l ("Expected no arguments for assignment function " ^ i) + | args,[] -> + typ_error l ("Expected arguments with types " ^ (t_to_string args_t) ^ + "for assignment function " ^ i) + | args,es -> + (match check_exp envs imp_param args_t (E_aux (E_tuple exps,(l,NoTyp))) with + | (E_aux(E_tuple es,(l',tannot)),_,_,cs_e,_,ef_e) -> (es,cs_e,ef_e) + | _ -> + raise (Reporting_basic.err_unreachable l + "Gave check_exp a tuple, didn't get a tuple back")) + in + let ef_all = union_effects ef' ef_es in + (LEXP_aux(LEXP_memory(id,es),(l,Base(([],out),tag,cs_call,ef',nob))), + item_t,false,Envmap.empty,tag,cs_call@cs_es,nob,ef_all) + | _ -> + let e = match exps with + | [] -> E_aux(E_lit(L_aux(L_unit,l)),(l,NoTyp)) + | [(E_aux(E_lit(L_aux(L_unit,_)),(_,NoTyp)) as e)] -> e + | es -> typ_error l ("Expected no arguments for assignment function " ^ i) in + let (e,_,_,cs_e,_,ef_e) = check_exp envs imp_param apps e in + let ef_all = union_effects ef ef_e in + (LEXP_aux(LEXP_memory(id,[e]),(l,Base(([],out),tag,cs_call,ef,nob))), + app,false,Envmap.empty,tag,cs_call@cs_e,nob,ef_all)) + else typ_error l ("Assignments require functions with a wmem, wmv, or wreg effect") + | _ -> typ_error l ("Assignments require functions with a wmem, wmv, or wreg effect")) + | _ -> typ_error l ("Assignments require a function here, found " ^ i ^ " which has type " ^ (t_to_string t))) + | _ -> typ_error l ("Unbound identifier " ^ i)) | LEXP_cast(typ,id) -> let i = id_to_string id in let ty = typ_to_t false false typ in let ty = typ_subst tp_env false ty in let new_bounds = extract_bounds d_env i ty in (match Envmap.apply t_env i with - | Some(Base((parms,t),tag,cs,_,bounds)) -> - let t,cs,_,_ = - match tag with | External _ | Emp_global -> subst parms false t cs pure_e | _ -> t,cs,pure_e,Envmap.empty - in - let t,cs' = get_abbrev d_env t in + | Some(Base((parms,t),tag,cs,_,bounds)) -> + let t,cs,_,_ = + match tag with | External _ | Emp_global -> subst parms false t cs pure_e | _ -> t,cs,pure_e,Envmap.empty + in + let t,cs' = get_abbrev d_env t in let t_actual = match t.t with | Tabbrev(_,t) -> t | _ -> t in - let bs = merge_bounds bounds new_bounds in - (match t_actual.t,is_top with - | Tapp("register",[TA_typ u]),_ -> - let t',cs = type_consistent (Expr l) d_env Require false ty u in - let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in - (LEXP_aux(lexp,(l,(Base(([],t),External (Some i),cs,ef,nob)))),ty,false, - Envmap.empty,External (Some i),[],nob,ef) - | Tapp("reg",[TA_typ u]),_ -> - let t',cs = type_consistent (Expr l) d_env Require false ty u in - (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,bs)))),ty,false, - Envmap.empty,Emp_local,[],bs,pure_e) - | Tapp("vector",_),false -> - (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,bs)))),ty,true,Envmap.empty,Emp_local,[],bs,pure_e) - | Tuvar _,_ -> - let u' = {t=Tapp("reg",[TA_typ ty])} in - equate_t t u'; - (LEXP_aux(lexp,(l,(Base((([],u'),Emp_local,cs,pure_e,bs))))),ty,false,Envmap.empty,Emp_local,[],bs,pure_e) - | (Tfn _ ,_) -> - (match tag with - | External _ | Spec | Emp_global -> - let tannot = (Base(([],ty),Emp_local,[],pure_e,new_bounds)) in - (LEXP_aux(lexp,(l,tannot)),ty,false,Envmap.from_list [i,tannot],Emp_local,[],new_bounds,pure_e) - | _ -> - typ_error l ("Cannot assign to " ^ i ^ " with type " ^ t_to_string t)) - | _,_ -> - if is_top - then typ_error l - ("Cannot assign to " ^ i ^ " with type " ^ t_to_string t ^ - ". May only assign to registers, and non-paremeter, non-let bound local variables") - else - (* TODO, make sure this is a record *) - (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,nob)))),ty,false,Envmap.empty,Emp_local,[],nob,pure_e)) - | _ -> - let t = {t=Tapp("reg",[TA_typ ty])} in - let tannot = (Base(([],t),Emp_local,[],pure_e,new_bounds)) in - (LEXP_aux(lexp,(l,tannot)),ty,false,Envmap.from_list [i,tannot],Emp_local,[],new_bounds,pure_e)) + let bs = merge_bounds bounds new_bounds in + (match t_actual.t,is_top with + | Tapp("register",[TA_typ u]),_ -> + let t',cs = type_consistent (Expr l) d_env Require false ty u in + let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in + (LEXP_aux(lexp,(l,(Base(([],t),External (Some i),cs,ef,nob)))),ty,false, + Envmap.empty,External (Some i),[],nob,ef) + | Tapp("reg",[TA_typ u]),_ -> + let t',cs = type_consistent (Expr l) d_env Require false ty u in + (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,bs)))),ty,false, + Envmap.empty,Emp_local,[],bs,pure_e) + | Tapp("vector",_),false -> + (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,bs)))),ty,true,Envmap.empty,Emp_local,[],bs,pure_e) + | Tuvar _,_ -> + let u' = {t=Tapp("reg",[TA_typ ty])} in + equate_t t u'; + (LEXP_aux(lexp,(l,(Base((([],u'),Emp_local,cs,pure_e,bs))))),ty,false,Envmap.empty,Emp_local,[],bs,pure_e) + | (Tfn _ ,_) -> + (match tag with + | External _ | Spec | Emp_global -> + let tannot = (Base(([],ty),Emp_local,[],pure_e,new_bounds)) in + (LEXP_aux(lexp,(l,tannot)),ty,false,Envmap.from_list [i,tannot],Emp_local,[],new_bounds,pure_e) + | _ -> + typ_error l ("Cannot assign to " ^ i ^ " with type " ^ t_to_string t)) + | _,_ -> + if is_top + then typ_error l + ("Cannot assign to " ^ i ^ " with type " ^ t_to_string t ^ + ". May only assign to registers, and non-paremeter, non-let bound local variables") + else + (* TODO, make sure this is a record *) + (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,nob)))),ty,false,Envmap.empty,Emp_local,[],nob,pure_e)) + | _ -> + let t = {t=Tapp("reg",[TA_typ ty])} in + let tannot = (Base(([],t),Emp_local,[],pure_e,new_bounds)) in + (LEXP_aux(lexp,(l,tannot)),ty,false,Envmap.from_list [i,tannot],Emp_local,[],new_bounds,pure_e)) | LEXP_vector(vec,acc) -> let (vec',vec_t,reg_required,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in let vec_t,cs' = get_abbrev d_env vec_t in let vec_actual = match vec_t.t with | Tabbrev(_,t) -> t | _ -> vec_t in (match vec_actual.t with - | Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ item_t]) -> - let acc_t = match ord.order with - | Oinc -> {t = Tapp("range",[TA_nexp base;TA_nexp (mk_sub (mk_add base rise) n_one)])} - | Odec -> {t = Tapp("range",[TA_nexp (mk_sub rise (mk_add base n_one)); TA_nexp base])} - | _ -> typ_error l ("Assignment to one vector element requires a non-polymorphic order") - in - let (e,acc_t',_,cs',_,ef_e) = check_exp envs imp_param acc_t acc in - let item_t,add_reg_write,reg_still_required = - match item_t.t with - | Tapp("register",[TA_typ t]) | Tabbrev(_,{t=Tapp("register",[TA_typ t])}) -> t,true,false - | Tapp("reg",[TA_typ t]) -> t,false,false - | _ -> item_t,false,true in - let ef = if add_reg_write then add_effect (BE_aux(BE_wreg,l)) ef else ef in - if is_top && reg_still_required && reg_required - then typ_error l "Assignment expected a register or non-parameter non-letbound identifier to mutate" - else - (LEXP_aux(LEXP_vector(vec',e),(l,Base(([],item_t),tag,csi,ef,nob))),item_t,reg_required && reg_still_required, - env,tag,csi@cs',bounds,union_effects ef ef_e) - | Tuvar _ -> - typ_error l "Assignment expected a vector with a known order, try adding an annotation." - | _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string vec_t))) + | Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ item_t]) -> + let acc_t = match ord.order with + | Oinc -> {t = Tapp("range",[TA_nexp base;TA_nexp (mk_sub (mk_add base rise) n_one)])} + | Odec -> {t = Tapp("range",[TA_nexp (mk_sub rise (mk_add base n_one)); TA_nexp base])} + | _ -> typ_error l ("Assignment to one vector element requires a non-polymorphic order") + in + let (e,acc_t',_,cs',_,ef_e) = check_exp envs imp_param acc_t acc in + let item_t,add_reg_write,reg_still_required = + match item_t.t with + | Tapp("register",[TA_typ t]) | Tabbrev(_,{t=Tapp("register",[TA_typ t])}) -> t,true,false + | Tapp("reg",[TA_typ t]) -> t,false,false + | _ -> item_t,false,true in + let ef = if add_reg_write then add_effect (BE_aux(BE_wreg,l)) ef else ef in + if is_top && reg_still_required && reg_required + then typ_error l "Assignment expected a register or non-parameter non-letbound identifier to mutate" + else + (LEXP_aux(LEXP_vector(vec',e),(l,Base(([],item_t),tag,csi,ef,nob))),item_t,reg_required && reg_still_required, + env,tag,csi@cs',bounds,union_effects ef ef_e) + | Tuvar _ -> + typ_error l "Assignment expected a vector with a known order, try adding an annotation." + | _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string vec_t))) | LEXP_vector_range(vec,e1,e2)-> let (vec',vec_t,reg_required,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in let vec_t,cs = get_abbrev d_env vec_t in let vec_actual = match vec_t.t with | Tabbrev(_,t) -> t | _ -> vec_t in let vec_actual,add_reg_write,reg_still_required,cs = - match vec_actual.t with - | Tapp("register",[TA_typ t]) -> - (match get_abbrev d_env t with | {t=Tabbrev(_,t)},cs' | t,cs' -> t,true,false,cs@cs') - | Tapp("reg",[TA_typ t]) -> - (match get_abbrev d_env t with | {t=Tabbrev(_,t)},cs' | t,cs' -> t,false,false,cs@cs') - | _ -> vec_actual,false,true,cs in + match vec_actual.t with + | Tapp("register",[TA_typ t]) -> + (match get_abbrev d_env t with | {t=Tabbrev(_,t)},cs' | t,cs' -> t,true,false,cs@cs') + | Tapp("reg",[TA_typ t]) -> + (match get_abbrev d_env t with | {t=Tabbrev(_,t)},cs' | t,cs' -> t,false,false,cs@cs') + | _ -> vec_actual,false,true,cs in (match vec_actual.t with - | Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ t]) -> - let size_e1,size_e2 = new_n(),new_n() in - let e1_t = {t=Tapp("atom",[TA_nexp size_e1])} in - let e2_t = {t=Tapp("atom",[TA_nexp size_e2])} in - let (e1',e1_t',_,cs1,_,ef_e) = check_exp envs imp_param e1_t e1 in - let (e2',e2_t',_,cs2,_,ef_e') = check_exp envs imp_param e2_t e2 in - let len = new_n() in - let needs_reg = match t.t with - | Tapp("reg",_) -> false - | Tapp("register",_) -> false - | _ -> true in - let cs_t,res_t = match ord.order with - | Oinc -> ([LtEq((Expr l),Require,base,size_e1); - LtEq((Expr l),Require,size_e1, size_e2); - LtEq((Expr l),Require,size_e2, rise); + | Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ t]) -> + let size_e1,size_e2 = new_n(),new_n() in + let e1_t = {t=Tapp("atom",[TA_nexp size_e1])} in + let e2_t = {t=Tapp("atom",[TA_nexp size_e2])} in + let (e1',e1_t',_,cs1,_,ef_e) = check_exp envs imp_param e1_t e1 in + let (e2',e2_t',_,cs2,_,ef_e') = check_exp envs imp_param e2_t e2 in + let len = new_n() in + let needs_reg = match t.t with + | Tapp("reg",_) -> false + | Tapp("register",_) -> false + | _ -> true in + let cs_t,res_t = match ord.order with + | Oinc -> ([LtEq((Expr l),Require,base,size_e1); + LtEq((Expr l),Require,size_e1, size_e2); + LtEq((Expr l),Require,size_e2, rise); Eq((Expr l),len, mk_add (mk_sub size_e2 size_e1) n_one)], - {t=Tapp("vector",[TA_nexp size_e1;TA_nexp len;TA_ord ord;TA_typ t])}) - | Odec -> ([GtEq((Expr l),Require,base,size_e1); - GtEq((Expr l),Require,size_e1,size_e2); - GtEq((Expr l),Require,size_e2,mk_sub base rise); + {t=Tapp("vector",[TA_nexp size_e1;TA_nexp len;TA_ord ord;TA_typ t])}) + | Odec -> ([GtEq((Expr l),Require,base,size_e1); + GtEq((Expr l),Require,size_e1,size_e2); + GtEq((Expr l),Require,size_e2,mk_sub base rise); Eq((Expr l),len, mk_add (mk_sub size_e1 size_e2) n_one)], {t=Tapp("vector",[TA_nexp size_e1;TA_nexp len;TA_ord ord; TA_typ t])}) - | _ -> typ_error l ("Assignment to a range of vector elements requires either inc or dec order") - in - let cs = cs_t@cs@cs1@cs2 in - let ef = union_effects ef (union_effects ef_e ef_e') in - if is_top && reg_required && reg_still_required && needs_reg - then typ_error l "Assignment requires a register or a non-parameter, non-letbound local identifier" - else (LEXP_aux(LEXP_vector_range(vec',e1',e2'),(l,Base(([],res_t),tag,cs,ef,nob))), - res_t,reg_required&®_still_required && needs_reg,env,tag,cs,bounds,ef) - | Tuvar _ -> typ_error l "Assignement to a range of elements requires a vector with a known order, try adding an annotation." - | _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string vec_t))) + | _ -> typ_error l ("Assignment to a range of vector elements requires either inc or dec order") + in + let cs = cs_t@cs@cs1@cs2 in + let ef = union_effects ef (union_effects ef_e ef_e') in + if is_top && reg_required && reg_still_required && needs_reg + then typ_error l "Assignment requires a register or a non-parameter, non-letbound local identifier" + else (LEXP_aux(LEXP_vector_range(vec',e1',e2'),(l,Base(([],res_t),tag,cs,ef,nob))), + res_t,reg_required&®_still_required && needs_reg,env,tag,cs,bounds,ef) + | Tuvar _ -> typ_error l "Assignement to a range of elements requires a vector with a known order, try adding an annotation." + | _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string vec_t))) | LEXP_field(vec,id)-> let (vec',item_t,reg_required,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in let vec_t = match vec' with @@ -1537,19 +1555,19 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) | _ -> item_t in let fi = id_to_string id in (match vec_t.t with - | Tid i | Tabbrev({t=Tid i},_) | Tabbrev({t=Tapp(i,_)},_) | Tapp(i,_)-> - (match lookup_record_typ i d_env.rec_env with - | Some(((i,rec_kind,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) -> - let (ts,cs,eft,subst_env) = subst params false t cs eft in - (match lookup_field_type fi r with - | None -> typ_error l ("Type " ^ i ^ " does not have a field " ^ fi) + | Tid i | Tabbrev({t=Tid i},_) | Tabbrev({t=Tapp(i,_)},_) | Tapp(i,_)-> + (match lookup_record_typ i d_env.rec_env with + | Some(((i,rec_kind,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) -> + let (ts,cs,eft,subst_env) = subst params false t cs eft in + (match lookup_field_type fi r with + | None -> typ_error l ("Type " ^ i ^ " does not have a field " ^ fi) | Some t -> - let ft = typ_subst subst_env false t in - let (_,cs_sub') = type_consistent (Expr l) d_env Guarantee false ts vec_t in - (LEXP_aux(LEXP_field(vec',id),(l,(Base(([],ft),tag,csi@cs,eft,nob)))),ft,false,env,tag,csi@cs@cs_sub',bounds,ef)) - | _ -> - typ_error l ("Expected a register or struct for this update, instead found an expression with type " ^ i)) - | _ -> typ_error l ("Expected a register binding here, found " ^ (t_to_string item_t))) + let ft = typ_subst subst_env false t in + let (_,cs_sub') = type_consistent (Expr l) d_env Guarantee false ts vec_t in + (LEXP_aux(LEXP_field(vec',id),(l,(Base(([],ft),tag,csi@cs,eft,nob)))),ft,false,env,tag,csi@cs@cs_sub',bounds,ef)) + | _ -> + typ_error l ("Expected a register or struct for this update, instead found an expression with type " ^ i)) + | _ -> typ_error l ("Expected a register binding here, found " ^ (t_to_string item_t))) and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * nexp_range list * bounds_env * effect = let Env(d_env,t_env,b_env,tp_env) = envs in @@ -1562,24 +1580,29 @@ and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) : let envs' = (Env(d_env,t_env,b_env,Envmap.union tp_env tp_env')) in let (pat',env,cs1,bounds,u) = check_pattern envs' emp_tag t pat in let (e,t,_,cs2,_,ef2) = check_exp envs' imp_param t e in - let cs = if is_top_level then resolve_constraints cs@cs1@cs2 else cs@cs1@cs2 in + let (cs,map) = if is_top_level then resolve_constraints (cs@cs1@cs2) else (cs@cs1@cs2,None) in let ef = union_effects ef ef2 in (*let _ = Printf.eprintf "checking tannot in let1\n" in*) - let tannot = if is_top_level - then check_tannot l (Base((params,t),tag,cs,ef,bounds)) None cs ef (*in top level, must be pure_e*) - else (Base ((params,t),tag,cs,ef,bounds)) + let tannot = + if is_top_level + then check_tannot l (Base((params,t),tag,cs,ef, + match map with | None -> bounds | Some m -> add_map_to_bounds m bounds)) + None cs ef (*in top level, must be pure_e*) + else (Base ((params,t),tag,cs,ef,bounds)) in (*let _ = Printf.eprintf "done checking tannot in let1\n" in*) (LB_aux (LB_val_explicit(typ,pat',e),(l,tannot)),env,cs,merge_bounds b_env bounds,ef) | NoTyp | Overload _ -> raise (Reporting_basic.err_unreachable l "typschm_to_tannot failed to produce a Base")) | LB_val_implicit(pat,e) -> - let t = new_t () in let (pat',env,cs1,bounds,u) = check_pattern envs emp_tag (new_t ()) pat in let (e,t',_,cs2,_,ef) = check_exp envs imp_param u e in - let cs = if is_top_level then resolve_constraints cs1@cs2 else cs1@cs2 in + let (cs,map) = if is_top_level then resolve_constraints (cs1@cs2) else (cs1@cs2),None in (*let _ = Printf.eprintf "checking tannot in let2\n" in*) let tannot = - if is_top_level then check_tannot l (Base(([],t'),emp_tag,cs,ef,bounds)) None cs ef (* see above *) + if is_top_level + then check_tannot l (Base(([],t'),emp_tag,cs,ef, + match map with | None -> bounds | Some m -> add_map_to_bounds m bounds)) + None cs ef (* see above *) else (Base (([],t'),emp_tag,cs,ef,merge_bounds bounds b_env)) in (*let _ = Printf.eprintf "done checking tannot in let2\n" in*) @@ -1609,11 +1632,11 @@ let check_type_def envs (TD_aux(td,(l,annot))) = let tyannot = Base((params,ty),Constructor,constraints,pure_e,nob) in let arm_t input = Base((params,{t=Tfn(input,ty,IP_none,pure_e)}),Constructor,constraints,pure_e,nob) in let arms' = List.map - (fun (Tu_aux(tu,l')) -> - match tu with - | Tu_id i -> ((id_to_string i),(arm_t unit_t)) - | Tu_ty_id(typ,i)-> ((id_to_string i),(arm_t (typ_to_t false false typ)))) - arms in + (fun (Tu_aux(tu,l')) -> + match tu with + | Tu_id i -> ((id_to_string i),(arm_t unit_t)) + | Tu_ty_id(typ,i)-> ((id_to_string i),(arm_t (typ_to_t false false typ)))) + arms in let t_env = List.fold_right (fun (id,tann) t_env -> Envmap.insert t_env (id,tann)) arms' t_env in (TD_aux(td,(l,tyannot)),(Env (d_env,t_env,b_env,tp_env))) | TD_enum(id,nmscm,ids,_) -> @@ -1629,93 +1652,95 @@ let check_type_def envs (TD_aux(td,(l,annot))) = let basei = normalize_nexp(anexp_to_nexp base) in let topi = normalize_nexp(anexp_to_nexp top) in match basei.nexp,topi.nexp with - | Nconst b, Nconst t -> - if (le_big_int b t) then ( - let ty = {t = Tapp("vector",[TA_nexp basei; TA_nexp (mk_c(add_big_int (sub_big_int t b) (big_int_of_int 1))); - TA_ord({order = Oinc}); TA_typ({t = Tid "bit"});])} in - let rec range_to_type_inc (BF_aux(idx,l)) = - (match idx with - | BF_single i -> - if (le_big_int b (big_int_of_int i)) && (le_big_int (big_int_of_int i) t) - then {t = Tid "bit"}, i, 1 - else typ_error l - ("register type declaration " ^ id' ^ - " contains a field specification outside of the declared register size") - | BF_range(i1,i2) -> - if i1<i2 - then - if (le_big_int b (big_int_of_int i1)) && (le_big_int (big_int_of_int i2) t) - then let size = i2 - i1 + 1 in - ({t=Tapp("vector",[TA_nexp (mk_c_int i1); TA_nexp (mk_c_int size); - TA_ord({order=Oinc}); TA_typ {t=Tid "bit"}])}, i1, size) - else typ_error l ("register type declaration " ^ id' - ^ " contains a field specification outside of the declared register size") - else typ_error l ("register type declaration " ^ id' ^ " is not consistently increasing") - | BF_concat(bf1, bf2) -> - (match (range_to_type_inc bf1, range_to_type_inc bf2) with - | ({t = Tid "bit"}, start, size1),({t= Tid "bit"}, start2, size2) - | (({t = Tid "bit"}, start, size1), ({t= Tapp("vector", _)}, start2, size2)) - | (({t=Tapp("vector", _)}, start, size1), ({t=Tid "bit"}, start2, size2)) - | (({t=Tapp("vector",_)}, start, size1), ({t=Tapp("vector",_)}, start2, size2)) -> - if start < start2 - then let size = size1 + size2 in - ({t=Tapp("vector", [TA_nexp (mk_c_int start); TA_nexp (mk_c_int size); - TA_ord({order = Oinc}); TA_typ {t=Tid"bit"}])}, start, size) - else typ_error l ("register type declaration " ^ id' ^ " is not consistently increasing"))) - in - let franges = - List.map - (fun (bf,id) -> - let (bf_t, _, _) = range_to_type_inc bf in ((id_to_string id),bf_t)) - ranges - in - let tannot = into_register d_env (Base(([],ty),Emp_global,[],pure_e,nob)) in - (TD_aux(td,(l,tannot)), - Env({d_env with rec_env = ((id',Register,tannot,franges)::d_env.rec_env); - abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env,b_env,tp_env))) - else ( - let ty = {t = Tapp("vector",[TA_nexp basei; TA_nexp (mk_c(add_big_int (sub_big_int b t) one)); - TA_ord({order = Odec}); TA_typ({t = Tid "bit"});])} in - let rec range_to_type_dec (BF_aux(idx,l)) = - (match idx with - | BF_single i -> - if (ge_big_int b (big_int_of_int i)) && (ge_big_int (big_int_of_int i) t) - then {t = Tid "bit"}, i, 1 - else typ_error l - ("register type declaration " ^ id' ^ - " contains a field specification outside of the declared register size") - | BF_range(i1,i2) -> - if i1>i2 - then - if (ge_big_int b (big_int_of_int i1)) && (ge_big_int (big_int_of_int i2) t) - then let size = (i1 - i2) + 1 in - ({t=Tapp("vector",[TA_nexp (mk_c_int i1); TA_nexp (mk_c_int size); - TA_ord({order=Odec}); TA_typ {t=Tid "bit"}])}, i1, size) - else typ_error l ("register type declaration " ^ id' - ^ " contains a field specification outside of the declared register size") - else typ_error l ("register type declaration " ^ id' ^ " is not consistently decreasing") - | BF_concat(bf1, bf2) -> - (match (range_to_type_dec bf1, range_to_type_dec bf2) with - | ({t = Tid "bit"}, start, size1),({t= Tid "bit"}, start2, size2) - | (({t = Tid "bit"}, start, size1), ({t= Tapp("vector", _)}, start2, size2)) - | (({t=Tapp("vector", _)}, start, size1), ({t=Tid "bit"}, start2, size2)) - | (({t=Tapp("vector",_)}, start, size1), ({t=Tapp("vector",_)}, start2, size2)) -> - if start > start2 - then let size = size1 + size2 in - ({t=Tapp("vector", [TA_nexp (mk_c_int start); TA_nexp (mk_c_int size); - TA_ord({order = Oinc}); TA_typ {t=Tid"bit"}])}, start, size) - else typ_error l ("register type declaration " ^ id' ^ " is not consistently decreasing"))) - in - let franges = - List.map - (fun (bf,id) -> let (bf_t, _, _) = range_to_type_dec bf in (id_to_string id, bf_t)) - ranges - in - let tannot = into_register d_env (Base(([],ty),Emp_global,[],pure_e,nob)) in - (TD_aux(td,(l,tannot)), - Env({d_env with rec_env = (id',Register,tannot,franges)::d_env.rec_env; - abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env,b_env,tp_env))) - | _,_ -> raise (Reporting_basic.err_unreachable l "Nexps in register declaration do not evaluate to constants") + | Nconst b, Nconst t -> + if (le_big_int b t) then ( + let ty = {t = Tapp("vector",[TA_nexp basei; TA_nexp (mk_c(add_big_int (sub_big_int t b) (big_int_of_int 1))); + TA_ord({order = Oinc}); TA_typ({t = Tid "bit"});])} in + let rec range_to_type_inc (BF_aux(idx,l)) = + (match idx with + | BF_single i -> + if (le_big_int b (big_int_of_int i)) && (le_big_int (big_int_of_int i) t) + then {t = Tid "bit"}, i, 1 + else typ_error l + ("register type declaration " ^ id' ^ + " contains a field specification outside of the declared register size") + | BF_range(i1,i2) -> + if i1<i2 + then + if (le_big_int b (big_int_of_int i1)) && (le_big_int (big_int_of_int i2) t) + then let size = i2 - i1 + 1 in + ({t=Tapp("vector",[TA_nexp (mk_c_int i1); TA_nexp (mk_c_int size); + TA_ord({order=Oinc}); TA_typ {t=Tid "bit"}])}, i1, size) + else typ_error l ("register type declaration " ^ id' + ^ " contains a field specification outside of the declared register size") + else typ_error l ("register type declaration " ^ id' ^ " is not consistently increasing") + | BF_concat(bf1, bf2) -> + (match (range_to_type_inc bf1, range_to_type_inc bf2) with + | ({t = Tid "bit"}, start, size1),({t= Tid "bit"}, start2, size2) + | (({t = Tid "bit"}, start, size1), ({t= Tapp("vector", _)}, start2, size2)) + | (({t=Tapp("vector", _)}, start, size1), ({t=Tid "bit"}, start2, size2)) + | (({t=Tapp("vector",_)}, start, size1), ({t=Tapp("vector",_)}, start2, size2)) -> + if start < start2 + then let size = size1 + size2 in + ({t=Tapp("vector", [TA_nexp (mk_c_int start); TA_nexp (mk_c_int size); + TA_ord({order = Oinc}); TA_typ {t=Tid"bit"}])}, start, size) + else typ_error l ("register type declaration " ^ id' ^ " is not consistently increasing") + | _ -> raise (Reporting_basic.err_unreachable l "range_to_type returned something odd"))) + in + let franges = + List.map + (fun (bf,id) -> + let (bf_t, _, _) = range_to_type_inc bf in ((id_to_string id),bf_t)) + ranges + in + let tannot = into_register d_env (Base(([],ty),Emp_global,[],pure_e,nob)) in + (TD_aux(td,(l,tannot)), + Env({d_env with rec_env = ((id',Register,tannot,franges)::d_env.rec_env); + abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env,b_env,tp_env))) + else ( + let ty = {t = Tapp("vector",[TA_nexp basei; TA_nexp (mk_c(add_big_int (sub_big_int b t) one)); + TA_ord({order = Odec}); TA_typ({t = Tid "bit"});])} in + let rec range_to_type_dec (BF_aux(idx,l)) = + (match idx with + | BF_single i -> + if (ge_big_int b (big_int_of_int i)) && (ge_big_int (big_int_of_int i) t) + then {t = Tid "bit"}, i, 1 + else typ_error l + ("register type declaration " ^ id' ^ + " contains a field specification outside of the declared register size") + | BF_range(i1,i2) -> + if i1>i2 + then + if (ge_big_int b (big_int_of_int i1)) && (ge_big_int (big_int_of_int i2) t) + then let size = (i1 - i2) + 1 in + ({t=Tapp("vector",[TA_nexp (mk_c_int i1); TA_nexp (mk_c_int size); + TA_ord({order=Odec}); TA_typ {t=Tid "bit"}])}, i1, size) + else typ_error l ("register type declaration " ^ id' + ^ " contains a field specification outside of the declared register size") + else typ_error l ("register type declaration " ^ id' ^ " is not consistently decreasing") + | BF_concat(bf1, bf2) -> + (match (range_to_type_dec bf1, range_to_type_dec bf2) with + | ({t = Tid "bit"}, start, size1),({t= Tid "bit"}, start2, size2) + | (({t = Tid "bit"}, start, size1), ({t= Tapp("vector", _)}, start2, size2)) + | (({t=Tapp("vector", _)}, start, size1), ({t=Tid "bit"}, start2, size2)) + | (({t=Tapp("vector",_)}, start, size1), ({t=Tapp("vector",_)}, start2, size2)) -> + if start > start2 + then let size = size1 + size2 in + ({t=Tapp("vector", [TA_nexp (mk_c_int start); TA_nexp (mk_c_int size); + TA_ord({order = Oinc}); TA_typ {t=Tid"bit"}])}, start, size) + else typ_error l ("register type declaration " ^ id' ^ " is not consistently decreasing") + | _ -> raise (Reporting_basic.err_unreachable l "range_to_type has returned something odd"))) + in + let franges = + List.map + (fun (bf,id) -> let (bf_t, _, _) = range_to_type_dec bf in (id_to_string id, bf_t)) + ranges + in + let tannot = into_register d_env (Base(([],ty),Emp_global,[],pure_e,nob)) in + (TD_aux(td,(l,tannot)), + Env({d_env with rec_env = (id',Register,tannot,franges)::d_env.rec_env; + abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env,b_env,tp_env))) + | _,_ -> raise (Reporting_basic.err_unreachable l "Nexps in register declaration do not evaluate to constants") let check_val_spec envs (VS_aux(vs,(l,annot))) = let (Env(d_env,t_env,b_env,tp_env)) = envs in @@ -1750,14 +1775,14 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let _ = reset_fresh () in let is_rec = match recopt with | Rec_aux(Rec_nonrec,_) -> false - | Rec_aux(Rec_rec,_) -> true in + | Rec_aux(Rec_rec,_) -> true in let id = match (List.fold_right - (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) id' -> - match id' with - | Some(id') -> if id' = id_to_string id then Some(id') - else typ_error l ("Function declaration expects all definitions to have the same name, " - ^ id_to_string id ^ " differs from other definitions of " ^ id') - | None -> Some(id_to_string id)) funcls None) with + (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) id' -> + match id' with + | Some(id') -> if id' = id_to_string id then Some(id') + else typ_error l ("Function declaration expects all definitions to have the same name, " + ^ id_to_string id ^ " differs from other definitions of " ^ id') + | None -> Some(id_to_string id)) funcls None) with | Some id -> id | None -> raise (Reporting_basic.err_unreachable l "funcl list might be empty") in let in_env = Envmap.apply t_env id in @@ -1777,17 +1802,20 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let check t_env tp_env imp_param = List.split (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,_))) -> - (*let _ = Printf.eprintf "checking function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) - let (pat',t_env',cs_p,b_env',t') = check_pattern (Env(d_env,t_env,b_env,tp_env)) Emp_local param_t pat in - let t', _ = type_consistent (Patt l) d_env Require false param_t t' in - let exp',_,_,cs_e,_,ef = - check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env true) t_env t_env', - merge_bounds b_env b_env',tp_env)) imp_param ret_t exp in - (*let _ = Printf.eprintf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in - let _ = Printf.eprintf "constraints were pattern: %s\n expression: %s\n" (constraints_to_string cs_p) (constraints_to_string cs_e) in*) - let cs = CondCons(Fun l,cond_kind,None,cs_p,cs_e) in - (FCL_aux((FCL_Funcl(id,pat',exp')),(l,(Base(([],ret_t),Emp_global,[cs],ef,nob)))),(cs,ef))) funcls) in - let update_pattern var (FCL_aux ((FCL_Funcl(id,(P_aux(pat,t)),exp)),annot)) = + (*let _ = Printf.eprintf "checking function %s : %s -> %s\n" + (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) + let (pat',t_env',cs_p,b_env',t') = check_pattern (Env(d_env,t_env,b_env,tp_env)) Emp_local param_t pat in + let _, _ = type_consistent (Patt l) d_env Require false param_t t' in + let exp',_,_,cs_e,_,ef = + check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env true) t_env t_env', + merge_bounds b_env b_env',tp_env)) imp_param ret_t exp in + (*let _ = Printf.eprintf "checked function %s : %s -> %s\n" + (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in + let _ = Printf.eprintf "constraints were pattern: %s\n expression: %s\n" + (constraints_to_string cs_p) (constraints_to_string cs_e) in*) + let cs = CondCons(Fun l,cond_kind,None,cs_p,cs_e) in + (FCL_aux((FCL_Funcl(id,pat',exp')),(l,(Base(([],ret_t),Emp_global,[cs],ef,nob)))),(cs,ef))) funcls) in + let update_pattern var (FCL_aux ((FCL_Funcl(id,(P_aux(pat,t)),exp)),annot)) = let pat' = match pat with | P_lit (L_aux (L_unit,l')) -> P_aux(P_id (Id_aux (Id var, l')), t) | P_tup pats -> P_aux(P_tup ((P_aux (P_id (Id_aux (Id var, l)), t))::pats), t) @@ -1797,27 +1825,28 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, match (in_env,tannot) with | 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,t_param_env_spec = subst params true u constraints eft in - let t_param_cs = type_param_consistent l t_param_env_spec t_param_env in + let u,constraints,eft,t_param_env = subst_with_env t_param_env true u constraints eft in let _,cs_decs = type_consistent (Specc l) d_env Require false t u in - (*let _ = Printf.eprintf "valspec consistent with declared type for %s, %s ~< %s with %s derived constraints and %s stated and %s from environment consistency\n" id (t_to_string t) (t_to_string u) (constraints_to_string cs_decs) (constraints_to_string (constraints@c')) (constraints_to_string t_param_cs) in*) + (*let _ = Printf.eprintf "valspec consistent with declared type for %s, %s ~< %s with %s derived constraints and %s stated\n" id (t_to_string t) (t_to_string u) (constraints_to_string cs_decs) (constraints_to_string (constraints@c')) in*) let imp_param = match u.t with - | Tfn(_,_,IP_user n,_) -> Some n - | _ -> None in + | Tfn(_,_,IP_user n,_) -> Some n + | _ -> None in let (t_env,orig_env) = if is_rec then (t_env,t_env) else (Envmap.remove t_env id,t_env) in - let funcls,cs_ef = check t_env t_param_env_spec imp_param in + let funcls,cs_ef = check t_env t_param_env imp_param in let cses,ef = ((fun (cses,efses) -> - cses,(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in + cses,(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in let cs = if List.length funcls = 1 then cses else [BranchCons(Fun l,None, cses)] in - let cs' = resolve_constraints (cs@cs_decs@constraints@c'@t_param_cs) in + let cs',map = resolve_constraints (cs@cs_decs@constraints@c') in + let tannot = + check_tannot l (match map with | None -> tannot | Some m -> add_map_tannot m tannot) imp_param cs' ef in (*let _ = Printf.eprintf "remaining constraints are: %s\n" (constraints_to_string cs') in*) - let tannot = check_tannot l tannot imp_param cs' ef in - (*let _ = Printf.eprintf "check_tannot ok for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in*) + (*let _ = Printf.eprintf "check_tannot ok for %s val type %s derived type %s \n" + id (t_to_string u) (t_to_string t) in*) let funcls = match imp_param with - | Some {nexp = Nvar i} -> List.map (update_pattern i) funcls - | _ -> funcls + | Some {nexp = Nvar i} -> List.map (update_pattern i) funcls + | _ -> funcls in - (*let _ = Printf.eprintf "done funcheck case 1\n" in*) + (*let _ = Printf.eprintf "done funcheck case 1 of %s\n%!" id in*) (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))), Env(d_env,orig_env (*Envmap.insert t_env (id,tannot)*),b_env,tp_env) | _ , _-> @@ -1827,9 +1856,12 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let cses,ef = ((fun (cses,efses) -> (cses,(List.fold_right union_effects efses pure_e))) (List.split cs_ef)) in let cs = if List.length funcls = 1 then cses else [BranchCons(Fun l, None, cses)] in (*let _ = Printf.eprintf "unresolved constraints are %s\n%!" (constraints_to_string cs) in*) - let cs' = resolve_constraints cs in - (*let _ = Printf.eprintf "checking tannot for %s 2 remaining constraints are %s\n" id (constraints_to_string cs') in*) - let tannot = check_tannot l tannot None cs' ef in + let (cs',map) = resolve_constraints cs in + (*let _ = Printf.eprintf "checking tannot for %s 2 remaining constraints are %s\n" + id (constraints_to_string cs') in*) + let tannot = check_tannot l + (match map with | None -> tannot | Some m -> add_map_tannot m tannot) + None cs' ef in (*let _ = Printf.eprintf "done funcheck case2\n" in*) (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))), Env(d_env,(if is_rec then t_env else Envmap.insert t_env (id,tannot)),b_env,tp_env) @@ -1841,82 +1873,82 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ = let i = id_to_string id in (match Envmap.apply t_env i with | Some(Base(([],t), External (Some j), [], _,_)) -> - let t,_ = get_abbrev d_env t in + let t,_ = get_abbrev d_env t in let t_actual,t_id = match t.t with | Tabbrev(i,t) -> t,i | _ -> t,t in - (match t_actual.t with - | Tapp("register",[TA_typ t']) -> - if i = j then (i,(RI_aux (RI_id id, (l,Base(([],t),External (Some j), [], pure_e,nob)))),t_id,t') - else assert false - | _ -> typ_error l - ("register alias " ^ alias ^ " to " ^ i ^ " expected a register, found " ^ (t_to_string t))) + (match t_actual.t with + | Tapp("register",[TA_typ t']) -> + if i = j then (i,(RI_aux (RI_id id, (l,Base(([],t),External (Some j), [], pure_e,nob)))),t_id,t') + else assert false + | _ -> typ_error l + ("register alias " ^ alias ^ " to " ^ i ^ " expected a register, found " ^ (t_to_string t))) | _ -> typ_error l ("register alias " ^ alias ^ " to " ^ i ^ " exepcted a register.")) in match al with | AL_subreg(reg_a,subreg) -> let (reg,reg_a,reg_t,t) = check_reg reg_a in (match reg_t.t with - | Tid i -> - (match lookup_record_typ i d_env.rec_env with - | None -> typ_error l ("Expected a register with bit fields, given " ^ i) - | Some(((i,rec_kind,tannot,fields) as r)) -> - let fi = id_to_string subreg in - (match lookup_field_type fi r with - | None -> typ_error l ("Type " ^ i ^ " does not have a field " ^ fi) + | Tid i -> + (match lookup_record_typ i d_env.rec_env with + | None -> typ_error l ("Expected a register with bit fields, given " ^ i) + | Some(((i,rec_kind,tannot,fields) as r)) -> + let fi = id_to_string subreg in + (match lookup_field_type fi r with + | None -> typ_error l ("Type " ^ i ^ " does not have a field " ^ fi) | Some et -> - let tannot = Base(([],et),Alias,[],pure_e,nob) in - let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in - (AL_aux(AL_subreg(reg_a,subreg),(l,tannot)),tannot,d_env))) - | _ -> typ_error l ("Expected a register with fields, given " ^ (t_to_string reg_t))) + let tannot = Base(([],et),Alias,[],pure_e,nob) in + let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in + (AL_aux(AL_subreg(reg_a,subreg),(l,tannot)),tannot,d_env))) + | _ -> typ_error l ("Expected a register with fields, given " ^ (t_to_string reg_t))) | AL_bit(reg_a,bit) -> let (reg,reg_a,reg_t,t) = check_reg reg_a in let (E_aux(bit,(le,eannot)),_,_,_,_,_) = check_exp envs None (new_t ()) bit in (match t.t with - | Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord order;TA_typ item_t]) -> - (match (base.nexp,len.nexp,order.order, bit) with - | (Nconst i,Nconst j,Oinc, E_lit (L_aux((L_num k), ll))) -> - if (int_of_big_int i) <= k && ((int_of_big_int i) + (int_of_big_int j)) >= k - then let tannot = Base(([],item_t),Alias,[],pure_e,nob) in - let d_env = - {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in - (AL_aux(AL_bit(reg_a,(E_aux(bit,(le,eannot)))), (l,tannot)), tannot,d_env) - else typ_error ll ("Alias bit lookup must be in the range of the vector in the register") - | _ -> typ_error l ("Alias bit lookup must have a constant index")) - | _ -> typ_error l ("Alias bit lookup must refer to a register with type vector, found " ^ (t_to_string t))) + | Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord order;TA_typ item_t]) -> + (match (base.nexp,len.nexp,order.order, bit) with + | (Nconst i,Nconst j,Oinc, E_lit (L_aux((L_num k), ll))) -> + if (int_of_big_int i) <= k && ((int_of_big_int i) + (int_of_big_int j)) >= k + then let tannot = Base(([],item_t),Alias,[],pure_e,nob) in + let d_env = + {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in + (AL_aux(AL_bit(reg_a,(E_aux(bit,(le,eannot)))), (l,tannot)), tannot,d_env) + else typ_error ll ("Alias bit lookup must be in the range of the vector in the register") + | _ -> typ_error l ("Alias bit lookup must have a constant index")) + | _ -> typ_error l ("Alias bit lookup must refer to a register with type vector, found " ^ (t_to_string t))) | AL_slice(reg_a,sl1,sl2) -> let (reg,reg_a,reg_t,t) = check_reg reg_a in let (E_aux(sl1,(le1,eannot1)),_,_,_,_,_) = check_exp envs None (new_t ()) sl1 in let (E_aux(sl2,(le2,eannot2)),_,_,_,_,_) = check_exp envs None (new_t ()) sl2 in (match t.t with - | Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord order;TA_typ item_t]) -> - (match (base.nexp,len.nexp,order.order, sl1,sl2) with - | (Nconst i,Nconst j,Oinc, E_lit (L_aux((L_num k), ll)),E_lit (L_aux((L_num k2), ll2))) -> - if (int_of_big_int i) <= k && ((int_of_big_int i) + (int_of_big_int j)) >= k2 && k < k2 - then let t = {t = Tapp("vector",[TA_nexp (int_to_nexp k);TA_nexp (int_to_nexp ((k2-k) +1)); - TA_ord order; TA_typ item_t])} in - let tannot = Base(([],t),Alias,[],pure_e,nob) in - let d_env = - {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in - (AL_aux(AL_slice(reg_a,(E_aux(sl1,(le1,eannot1))),(E_aux(sl2,(le2,eannot2)))), - (l,tannot)), tannot,d_env) - else typ_error ll ("Alias slices must be in the range of the vector in the register") - | _ -> typ_error l ("Alias slices must have constant slices")) - | _ -> typ_error l ("Alias slices must point to a register with a vector type: found " ^ (t_to_string t))) + | Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord order;TA_typ item_t]) -> + (match (base.nexp,len.nexp,order.order, sl1,sl2) with + | (Nconst i,Nconst j,Oinc, E_lit (L_aux((L_num k), ll)),E_lit (L_aux((L_num k2), ll2))) -> + if (int_of_big_int i) <= k && ((int_of_big_int i) + (int_of_big_int j)) >= k2 && k < k2 + then let t = {t = Tapp("vector",[TA_nexp (int_to_nexp k);TA_nexp (int_to_nexp ((k2-k) +1)); + TA_ord order; TA_typ item_t])} in + let tannot = Base(([],t),Alias,[],pure_e,nob) in + let d_env = + {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in + (AL_aux(AL_slice(reg_a,(E_aux(sl1,(le1,eannot1))),(E_aux(sl2,(le2,eannot2)))), + (l,tannot)), tannot,d_env) + else typ_error ll ("Alias slices must be in the range of the vector in the register") + | _ -> typ_error l ("Alias slices must have constant slices")) + | _ -> typ_error l ("Alias slices must point to a register with a vector type: found " ^ (t_to_string t))) | AL_concat(reg1_a,reg2_a) -> let (reg1,reg1_a,reg_t,t1) = check_reg reg1_a in let (reg2,reg2_a,reg_t,t2) = check_reg reg2_a in (match (t1.t,t2.t) with - | (Tapp("vector",[TA_nexp b1;TA_nexp r; TA_ord {order = Oinc}; TA_typ item_t]), - Tapp("vector",[TA_nexp _ ;TA_nexp r2; TA_ord {order = Oinc}; TA_typ item_t2])) -> - let _ = type_consistent (Specc l) d_env Guarantee false item_t item_t2 in - let t = {t= Tapp("register", - [TA_typ {t= Tapp("vector",[TA_nexp b1; TA_nexp (mk_add r r2); - TA_ord {order = Oinc}; TA_typ item_t])}])} in - let tannot = Base(([],t),Alias,[],pure_e,nob) in - let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, TwoReg(reg1,reg2,tannot))} in - (AL_aux (AL_concat(reg1_a,reg2_a), (l,tannot)), tannot, d_env) - | _ -> typ_error l - ("Alias concatentaion must connect two registers with vector type, found " ^ t_to_string t1 ^ " and " ^ t_to_string t2)) + | (Tapp("vector",[TA_nexp b1;TA_nexp r; TA_ord {order = Oinc}; TA_typ item_t]), + Tapp("vector",[TA_nexp _ ;TA_nexp r2; TA_ord {order = Oinc}; TA_typ item_t2])) -> + let _ = type_consistent (Specc l) d_env Guarantee false item_t item_t2 in + let t = {t= Tapp("register", + [TA_typ {t= Tapp("vector",[TA_nexp b1; TA_nexp (mk_add r r2); + TA_ord {order = Oinc}; TA_typ item_t])}])} in + let tannot = Base(([],t),Alias,[],pure_e,nob) in + let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, TwoReg(reg1,reg2,tannot))} in + (AL_aux (AL_concat(reg1_a,reg2_a), (l,tannot)), tannot, d_env) + | _ -> typ_error l + ("Alias concatentaion must connect two registers with vector type, found " ^ t_to_string t1 ^ " and " ^ t_to_string t2)) (*val check_def : envs -> tannot def -> (tannot def) envs_out*) let check_def envs def = @@ -1943,7 +1975,7 @@ let check_def envs def = (*let _ = Printf.eprintf "checked spec\n" in*) (DEF_spec vs, envs) | DEF_default default -> let ds,envs = check_default envs default in - (DEF_default ds,envs) + (DEF_default ds,envs) | DEF_reg_dec(DEC_aux(DEC_reg(typ,id), (l,annot))) -> (*let _ = Printf.eprintf "checking reg dec\n" in *) let t = (typ_to_t false false typ) in @@ -1972,5 +2004,5 @@ let rec check envs (Defs defs) = match defs with | [] -> (Defs []) | def::defs -> let (def, envs) = check_def envs def in - let (Defs defs) = check envs (Defs defs) in - (Defs (def::defs)) + let (Defs defs) = check envs (Defs defs) in + (Defs (def::defs)) diff --git a/src/type_internal.ml b/src/type_internal.ml index a04528d8..aa9c1202 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -52,7 +52,8 @@ and nexp_aux = | Nneg of nexp (* Unary minus for representing new vector sizes after vector slicing *) | Ninexact (*Result of +inf + -inf which is neither less than nor greater than other numbers really *) | Nuvar of n_uvar -and n_uvar = { nindex : int; mutable nsubst : nexp option; mutable nin : bool; mutable leave_var : bool} +and n_uvar = + { nindex : int; mutable nsubst : nexp option; mutable nin : bool; mutable leave_var : bool; orig_var : string option} and effect = { mutable effect : effect_aux } and effect_aux = | Evar of string @@ -137,6 +138,8 @@ end module Var_set = Set.Make(NexpM) module Nexpmap = Finite_map.Fmap_map(NexpM) +type nexp_map = nexp Nexpmap.t + type constraint_origin = | Patt of Parse_ast.l | Expr of Parse_ast.l @@ -170,7 +173,7 @@ type variable_range = type bounds_env = | No_bounds - | Bounds of variable_range list + | Bounds of variable_range list * nexp_map option type t_params = (string * kind) list type tannot = @@ -218,6 +221,11 @@ let mk_p_inf () = {nexp = Npos_inf; imp_param = false} let mk_n_inf () = {nexp = Nneg_inf; imp_param = false} let mk_inexact () = {nexp = Ninexact; imp_param = false} +let merge_option_maps m1 m2 = match m1,m2 with + | None,None -> None + | None,m | m, None -> m + | Some m1, Some m2 -> Some (Nexpmap.union m1 m2) + (*Getters*) let get_index n = @@ -361,7 +369,7 @@ let variable_range_to_string v = match v with let bounds_to_string b = match b with | No_bounds -> "Nobounds" - | Bounds vs -> "Bounds(" ^ string_of_list "; " variable_range_to_string vs ^ ")" + | Bounds(vs,map)-> "Bounds(" ^ string_of_list "; " variable_range_to_string vs ^ ")" let rec tannot_to_string = function | NoTyp -> "No tannot" @@ -448,6 +456,25 @@ let rec contains_const n = | Nneg n -> contains_const n | Nmult(n1,n2) | Nadd(n1,n2) | Nsub(n1,n2) -> (contains_const n1) || (contains_const n2) +let rec is_all_nuvar n = + match n.nexp with + | Nuvar { nsubst = None } -> true + | Nuvar { nsubst = Some n } -> is_all_nuvar n + | _ -> false + +let rec first_non_nu n = + match n.nexp with + | Nuvar {nsubst = None } -> None + | Nuvar { nsubst = Some n} -> first_non_nu n + | _ -> Some n + +let rec change_nuvar_base n new_base = + match n.nexp with + | Nuvar {nsubst = Some ({nexp= Nuvar _} as in_n)} -> change_nuvar_base in_n new_base + | Nuvar ({nsubst = Some _} as nu) -> nu.nsubst <- Some new_base; true + | Nuvar {nsubst = None } -> false + | _ -> false + let rec get_var n = match n.nexp with | Nvar _ | Nuvar _ | N2n _ -> Some n @@ -513,6 +540,7 @@ let rec nexp_negative n = | Yes -> if odd i then Yes else No | No -> No | Maybe -> if odd i then Maybe else No) + | _ -> Maybe let rec normalize_n_rec recur_ok n = (*let _ = Printf.eprintf "Working on normalizing %s\n" (n_to_string n) in *) @@ -798,7 +826,15 @@ let new_t _ = let new_n _ = let i = !n_count in n_count := i + 1; - let n = { nexp = Nuvar { nindex = i; nsubst = None ; nin = false ; leave_var = false}; imp_param = false} in + let n = { nexp = Nuvar { nindex = i; nsubst = None ; nin = false ; leave_var = false; orig_var = None}; + imp_param = false} in + nuvars := n::!nuvars; + n +let new_nv s = + let i = !n_count in + n_count := i + 1; + let n = { nexp = Nuvar { nindex = i; nsubst = None ; nin = false ; leave_var = false ; orig_var = Some s}; + imp_param = false} in nuvars := n::!nuvars; n let leave_nuvar n = match n.nexp with @@ -1012,11 +1048,17 @@ let rec occurs_in_pending_subst n_box n : bool = if n'.nexp == n.nexp then true else occurs_in_pending_subst n' n - | Nuvar( { nsubst = None } ) -> false + | Nuvar( { nsubst = None } ) -> + (match n.nexp with + | Nuvar( { nsubst = None }) | Nvar _ | Nconst _ | Npos_inf | Nneg_inf | Ninexact -> false + | Nadd(n1,n2) | Nsub(n1,n2) | Nmult(n1,n2) -> occurs_in_nexp n_box n1 || occurs_in_nexp n_box n2 + | Nneg n1 | N2n(n1,_) | Npow(n1,_) -> occurs_in_nexp n_box n1 + | Nuvar( { nsubst = Some n'}) -> occurs_in_pending_subst n_box n') | _ -> occurs_in_nexp n_box n and occurs_in_nexp n_box nuvar : bool = - (*let _ = Printf.eprintf "occurs_in_nexp given n_box %s nuvar %s eq? %b\n" (n_to_string n_box) (n_to_string nuvar) (n_box.nexp == nuvar.nexp) in*) +(* let _ = Printf.eprintf "occurs_in_nexp given n_box %s nuvar %s eq? %b\n" + (n_to_string n_box) (n_to_string nuvar) (n_box.nexp == nuvar.nexp) in*) if n_box.nexp == nuvar.nexp then true else match n_box.nexp with | Nuvar _ -> occurs_in_pending_subst n_box nuvar @@ -1034,7 +1076,9 @@ let rec reduce_n_unifications n = (match nu.nsubst with | None -> () | Some(nexp) -> - reduce_n_unifications(nexp); if nu.leave_var then ignore(leave_nuvar(nexp)) else (); n.nexp <- nexp.nexp)); + reduce_n_unifications(nexp); + if nu.leave_var then ignore(leave_nuvar(nexp)) else (); + n.nexp <- nexp.nexp)); (*let _ = Printf.eprintf "n reduced to %s\n" (n_to_string n) in*) () let rec leave_nu_as_var n = @@ -1050,18 +1094,24 @@ let equate_n (n_box : nexp) (n : nexp) : bool = if n_box.nexp == n.nexp then true else let n = resolve_nsubst n in - if occurs_in_pending_subst n_box n || occurs_in_pending_subst n n_box then true - else - (*let _ = Printf.eprintf "equate_n has does not occur in %s and %s\n" (n_to_string n_box) (n_to_string n) in *) - let rec set_bottom_nsubst swap u new_bot = - match u.nsubst with - | None -> u.nsubst <- Some(new_bot); true - | Some({nexp = Nuvar(u)}) -> set_bottom_nsubst swap u new_bot - | Some(n_new) -> - if swap - then set_bottom_nsubst false (match new_bot.nexp with | Nuvar u -> u | _ -> assert false) n_new - else if nexp_eq n_new new_bot then true - else false in + let n_box = resolve_nsubst n_box in + let occur_nbox_n = occurs_in_pending_subst n_box n in + let occur_n_nbox = occurs_in_pending_subst n n_box in + let rec set_bottom_nsubst swap u new_bot = + match u.nsubst with + | None -> u.nsubst <- Some(new_bot); true + | Some({nexp = Nuvar(u)}) -> set_bottom_nsubst swap u new_bot + | Some(n_new) -> + if swap + then set_bottom_nsubst false (match new_bot.nexp with | Nuvar u -> u | _ -> assert false) n_new + else if nexp_eq n_new new_bot then true + else false in + match (occur_nbox_n,occur_n_nbox) with + | true,true -> false + | true,false | false,true -> true + | false,false -> + (*let _ = Printf.eprintf "equate_n has does not occur in %s and %s\n" + (n_to_string n_box) (n_to_string n) in *) match n_box.nexp,n.nexp with | Nuvar(u), Nuvar _ -> set_bottom_nsubst true u n | Nuvar(u), _ -> set_bottom_nsubst false u n @@ -1115,9 +1165,14 @@ let rec fresh_tvar bindings t = let rec fresh_nvar bindings n = (*let _ = Printf.eprintf "fresh_nvar for %s\n" (n_to_string n) in*) match n.nexp with - | Nuvar { nindex = i;nsubst = None } -> + | Nuvar { nindex = i;nsubst = None ; orig_var = None } -> fresh_var "nv" i (fun v add -> n.nexp <- (Nvar v); -(*(Printf.eprintf "fresh nvar set %i to %s : %s\n" i v (n_to_string n));*) if add then Some(v,{k=K_Nat}) else None) bindings + (*(Printf.eprintf "fresh nvar set %i to %s : %s\n" i v (n_to_string n));*) + if add then Some(v,{k=K_Nat}) else None) bindings + | Nuvar { nindex = i;nsubst = None ; orig_var = Some v } -> + fresh_var v 0 (fun v add -> n.nexp <- (Nvar v); + (*(Printf.eprintf "fresh nvar set %i to %s : %s\n" i v (n_to_string n));*) + if add then Some(v,{k=K_Nat}) else None) bindings | Nuvar { nindex = i; nsubst = Some({nexp=Nuvar _} as n')} -> let kv = fresh_nvar bindings n' in n.nexp <- n'.nexp; @@ -2061,18 +2116,21 @@ let rec cs_subst t_env cs = CondCons(l,kind,None,cs_subst t_env cs_p,cs_subst t_env cs_e)::(cs_subst t_env cs) | BranchCons(l,_,bs)::cs -> BranchCons(l,None,cs_subst t_env bs)::(cs_subst t_env cs) +let subst_with_env env leave_imp t cs e = + (typ_subst env leave_imp t, cs_subst env cs, e_subst env e, env) + let subst (k_env : (Envmap.k * kind) list) (leave_imp:bool) (t : t) (cs : nexp_range list) (e : effect) : (t * nexp_range list * effect * t_arg emap) = let subst_env = Envmap.from_list (List.map (fun (id,k) -> (id, match k.k with | K_Typ -> TA_typ (new_t ()) - | K_Nat -> TA_nexp (new_n ()) + | K_Nat -> TA_nexp (new_n id) | K_Ord -> TA_ord (new_o ()) | K_Efct -> TA_eft (new_e ()) | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "substitution given an environment with a non-base-kind kind"))) k_env) in - (typ_subst subst_env leave_imp t, cs_subst subst_env cs, e_subst subst_env e, subst_env) + subst_with_env subst_env leave_imp t cs e let rec typ_param_eq l spec_param fun_param = match (spec_param,fun_param) with @@ -2237,7 +2295,7 @@ let rec get_abbrev d_env t = let is_enum_typ d_env t = let t,_ = get_abbrev d_env t in let t_actual = match t.t with | Tabbrev(_,ta) -> ta | _ -> t in - match t.t with + match t_actual.t with | Tid i -> (match Envmap.apply d_env.enum_env i with | Some(ns) -> Some(List.length ns) | _ -> None) @@ -2319,7 +2377,8 @@ let build_variable_range d_env v typ = let t_actual = match t.t with | Tabbrev(_,t) -> t | _ -> t in match t_actual.t with | Tapp("atom", [TA_nexp n]) -> Some(VR_eq(v,n)) - | Tapp("range", [TA_nexp base;TA_nexp top]) -> Some(VR_range(v,[LtEq((Patt Unknown),Require,base,top)])) + | Tapp("range", [TA_nexp base;TA_nexp top]) -> + Some(VR_range(v,[LtEq((Patt Parse_ast.Unknown),Require,base,top)])) | Tapp("vector", [TA_nexp start; TA_nexp rise; _; _]) -> Some(VR_vec_eq(v,rise)) | Tuvar _ -> Some(VR_recheck(v,t_actual)) | _ -> None @@ -2332,16 +2391,35 @@ let compare_variable_range v1 v2 = compare (get_vr_var v1) (get_vr_var v2) let extract_bounds d_env v typ = match build_variable_range d_env v typ with | None -> No_bounds - | Some vb -> Bounds [vb] + | Some vb -> Bounds([vb], None) let find_bounds v bounds = match bounds with | No_bounds -> None - | Bounds bs -> + | Bounds(bs,maps) -> let rec find_rec bs = match bs with | [] -> None | b::bs -> if (get_vr_var b) = v then Some(b) else find_rec bs in find_rec bs +let add_map_to_bounds m bounds = match bounds with + | No_bounds -> Bounds([],Some m) + | Bounds(bs,None) -> Bounds(bs,Some m) + | Bounds(bs,Some m') -> Bounds(bs,Some (Nexpmap.union m m')) + +let rec add_map_tannot m tannot = match tannot with + | NoTyp -> NoTyp + | Base(params,tag,cs,ef,bounds) -> Base(params,tag,cs,ef,add_map_to_bounds m bounds) + | Overload(t,r,ts) -> Overload(add_map_tannot m t,r,ts) + +let get_map_bounds = function + | No_bounds -> None + | Bounds(_,m) -> m + +let get_map_tannot = function + | NoTyp -> None + | Base(_,_,_,_,bounds) -> get_map_bounds bounds + | Overload _ -> None + let rec expand_nexp n = match n.nexp with | Nvar _ | Nconst _ | Nuvar _ | Npos_inf | Nneg_inf | Ninexact -> [n] | Nadd (n1,n2) | Nsub (n1,n2) | Nmult (n1,n2) -> n::((expand_nexp n1)@(expand_nexp n2)) @@ -2354,25 +2432,35 @@ let find_var_from_nexp n bounds = if is_nconst n then None else match bounds with | No_bounds -> None - | Bounds bs -> - let rec find_rec bs = match bs with + | Bounds(bs,map) -> + let rec find_rec bs n = match bs with | [] -> None | b::bs -> (match b with | VR_eq(ev,n1) -> (*let _ = Printf.eprintf "checking if %s is eq to %s, to bind to %s, eq? %b\n" (n_to_string n) (n_to_string n1) ev (nexp_eq_check n1 n) in*) - if nexp_eq_check n1 n then Some (None,ev) else find_rec bs + if nexp_eq_check n1 n then Some (None,ev) else find_rec bs n | VR_vec_eq (ev,n1)-> (*let _ = Printf.eprintf "checking if %s is eq to %s, to bind to %s, eq? %b\n" (n_to_string n) (n_to_string n1) ev (nexp_eq_check n1 n) in*) - if nexp_eq_check n1 n then Some (Some "length",ev) else find_rec bs - | _ -> find_rec bs) in - find_rec bs + if nexp_eq_check n1 n then Some (Some "length",ev) else find_rec bs n + | _ -> find_rec bs n) in + match find_rec bs n,map with + | None, None -> None + | None, Some map -> + (match Nexpmap.apply map n with + | None -> None + | Some n' -> find_rec bs n') + | s,_ -> s let merge_bounds b1 b2 = match b1,b2 with | No_bounds,b | b,No_bounds -> b - | Bounds b1s,Bounds b2s -> + | Bounds(b1s,map1),Bounds(b2s,map2) -> + let merged_map = match map1,map2 with + | None, None -> None + | None, m | m, None -> m + | Some m1, Some m2 -> Some (Nexpmap.union m1 m2) in let b1s = List.sort compare_variable_range b1s in let b2s = List.sort compare_variable_range b2s in let rec merge b1s b2s = match (b1s,b2s) with @@ -2383,17 +2471,17 @@ let merge_bounds b1 b2 = | 1 -> b2::(merge (b1::b1s) b2s) | _ -> (match b1,b2 with | VR_eq(v,n1),VR_eq(_,n2) -> - if nexp_eq n1 n2 then b1 else VR_range(v,[Eq((Patt Unknown),n1,n2)]) + if nexp_eq n1 n2 then b1 else VR_range(v,[Eq((Patt Parse_ast.Unknown),n1,n2)]) | VR_eq(v,n),VR_range(_,ranges) | - VR_range(v,ranges),VR_eq(_,n) -> VR_range(v,(Eq((Patt Unknown),n,n))::ranges) + VR_range(v,ranges),VR_eq(_,n) -> VR_range(v,(Eq((Patt Parse_ast.Unknown),n,n))::ranges) | VR_range(v,ranges1),VR_range(_,ranges2) -> VR_range(v,ranges1@ranges2) | VR_vec_eq(v,n1),VR_vec_eq(_,n2) -> - if nexp_eq n1 n2 then b1 else VR_vec_r(v,[Eq((Patt Unknown),n1,n2)]) + if nexp_eq n1 n2 then b1 else VR_vec_r(v,[Eq((Patt Parse_ast.Unknown),n1,n2)]) | VR_vec_eq(v,n),VR_vec_r(_,ranges) | - VR_vec_r(v,ranges),VR_vec_eq(_,n) -> VR_vec_r(v,(Eq((Patt Unknown),n,n)::ranges)) + VR_vec_r(v,ranges),VR_vec_eq(_,n) -> VR_vec_r(v,(Eq((Patt Parse_ast.Unknown),n,n)::ranges)) | _ -> b1 )::(merge b1s b2s) in - Bounds (merge b1s b2s) + Bounds ((merge b1s b2s),merged_map) let rec conforms_to_t d_env loosely within_coercion spec actual = (*let _ = Printf.printf "conforms_to_t called, evaluated loosely? %b, with %s and %s\n" @@ -2422,13 +2510,15 @@ let rec conforms_to_t d_env loosely within_coercion spec actual = conforms_to_n true within_coercion le_big_int bs n && conforms_to_n true within_coercion ge_big_int rs n && conforms_to_n true within_coercion ge_big_int bs n *) | (Tapp(is,tas), Tapp(ia, taa),_) -> -(* let _ = Printf.printf "conforms to given two apps: %b, %b\n" (is = ia) (List.length tas = List.length taa) in*) - (is = ia) && (List.length tas = List.length taa) && (List.for_all2 (conforms_to_ta d_env loosely within_coercion) tas taa) +(* let _ = Printf.eprintf "conforms to given two apps: %b, %b\n" + (is = ia) (List.length tas = List.length taa) in*) + (is = ia) && (List.length tas = List.length taa) && + (List.for_all2 (conforms_to_ta d_env loosely within_coercion) tas taa) | (Tabbrev(_,s),a,_) -> conforms_to_t d_env loosely within_coercion s actual | (s,Tabbrev(_,a),_) -> conforms_to_t d_env loosely within_coercion spec a | (_,_,_) -> false and conforms_to_ta d_env loosely within_coercion spec actual = -(*let _ = Printf.printf "conforms_to_ta called, evaluated loosely? %b, with %s and %s\n" +(*let _ = Printf.eprintf "conforms_to_ta called, evaluated loosely? %b, with %s and %s\n" loosely (targ_to_string spec) (targ_to_string actual) in*) match spec,actual with | TA_typ s, TA_typ a -> conforms_to_t d_env loosely within_coercion s a @@ -2452,7 +2542,7 @@ and conforms_to_e loosely spec actual = | (Euvar _,_,true) -> true | (_,Euvar _,true) -> false | _ -> - try begin ignore (effects_eq (Specc Unknown) spec actual); true end with + try begin ignore (effects_eq (Specc Parse_ast.Unknown) spec actual); true end with | _ -> false (*Is checking for structural equality amongst the types, building constraints for kind Nat. @@ -2460,7 +2550,8 @@ and conforms_to_e loosely spec actual = When considering two atom type applications, will expand into a range encompasing both when widen is true *) let rec type_consistent_internal co d_env enforce widen t1 cs1 t2 cs2 = -(* let _ = Printf.eprintf "type_consistent_internal called with %s and %s\n" (t_to_string t1) (t_to_string t2) in*) +(* let _ = Printf.eprintf "type_consistent_internal called with %s and %s\n" + (t_to_string t1) (t_to_string t2) in*) let l = get_c_loc co in let t1,cs1' = get_abbrev d_env t1 in let t2,cs2' = get_abbrev d_env t2 in @@ -2610,7 +2701,6 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e let cs = csp@[Eq(co,r1,r2)] in let t',cs' = type_consistent co d_env enforce widen t1i t2i in let tannot = Base(([],t2),Emp_local,cs@cs',pure_e,nob) in - (*let _ = Printf.eprintf "looking at vector vector coerce, t1 %s, t2 %s\n" (t_to_string t1) (t_to_string t2) in*) let e' = E_aux(E_internal_cast ((l,(Base(([],t2),Emp_local,[],pure_e,nob))),e),(l,tannot)) in (t2,cs@cs',pure_e,e') | _ -> raise (Reporting_basic.err_unreachable l "vector is not properly kinded")) @@ -2888,8 +2978,12 @@ let rec subst_nuvars_cs nus cs = | BranchCons(l,possible_invars,bs)::cs -> BranchCons(l,possible_invars,subst_nuvars_cs nus bs)::(subst_nuvars_cs nus cs) -let freshen_constraints cs = - let nuvars = Var_set.fold (fun n map -> Nexpmap.insert map (n,new_n())) (get_all_nuvars_cs cs) Nexpmap.empty in +let freshen_constraints cs = + let nuvars = + Var_set.fold (fun n map -> + let ne = new_n() in + (*let _ = Printf.eprintf "mapping %s to %s\n%!" (n_to_string n) (n_to_string ne) in*) + Nexpmap.insert map (n,ne)) (get_all_nuvars_cs cs) Nexpmap.empty in (subst_nuvars_cs nuvars cs,nuvars) let rec prepare_constraints = function @@ -2897,72 +2991,110 @@ let rec prepare_constraints = function | CondCons(l,(Positive|Negative|Switch as kind),None,cs_p,cs_e)::cs -> let (new_pred_cs,my_substs) = freshen_constraints cs_p in let new_expr_cs = subst_nuvars_cs my_substs cs_e in - CondCons(l,kind,Some(my_substs),cs_p,cs_e)::(prepare_constraints cs) + CondCons(l,kind,Some(my_substs),cs_p,(prepare_constraints new_expr_cs))::(prepare_constraints cs) + | CondCons(l,Solo,None,cs_p,cs_e)::cs -> + CondCons(l,Solo,None,cs_p,(prepare_constraints cs_e))::(prepare_constraints cs) | BranchCons(l,_,bs)::cs -> BranchCons(l,None, prepare_constraints bs)::(prepare_constraints cs) | c::cs -> c::(prepare_constraints cs) +let nexpmap_to_string nmap = + Nexpmap.fold (fun acc k v -> + match v with + | One n -> "(" ^ n_to_string k ^ " |-> " ^ n_to_string n ^ ") " ^ acc + | Two(n1,n2) -> "(" ^ n_to_string k ^ " |-> (" ^ n_to_string n1 ^ ", or " ^ n_to_string n2 ^ ")) " ^ acc + | Many ns -> "(" ^ n_to_string k ^ " |-> (" ^ string_of_list ", " n_to_string ns ^ ")) " ^ acc) "" nmap + let rec make_merged_constraints acc = function | [] -> acc | c::cs -> + (* let _ = Printf.eprintf "merging constraints acc thus far is %s\n%!" (nexpmap_to_string acc) in*) make_merged_constraints (Nexpmap.fold - (fun acc k v -> - match Nexpmap.apply acc k with - | None -> Nexpmap.insert acc (k, One v) - | Some(One v') -> Nexpmap.insert (Nexpmap.remove acc k) (k, Two(v,v')) - | Some(Two(v',v'')) -> Nexpmap.insert (Nexpmap.remove acc k) (k,Many [v;v';v'']) - | Some(Many vs) -> Nexpmap.insert (Nexpmap.remove acc k) (k,Many (v::vs))) acc c) + (fun acc k v -> +(* let _ = Printf.eprintf "folding over c: we have %s |-> %s for acc of %s\n%!" + (n_to_string k) (n_to_string v) (nexpmap_to_string acc) in*) + match Nexpmap.apply acc k with + | None -> Nexpmap.insert acc (k, One v) + | Some(One v') -> Nexpmap.insert (Nexpmap.remove acc k) (k, Two(v,v')) + | Some(Two(v',v'')) -> Nexpmap.insert (Nexpmap.remove acc k) (k,Many [v;v';v'']) + | Some(Many vs) -> Nexpmap.insert (Nexpmap.remove acc k) (k,Many (v::vs))) acc c) cs - + let merge_branch_constraints merge_nuvars constraint_sets = - (*let _ = Printf.eprintf "merge branch constraints\n%!" in*) (*Separate variables into only occurs in one set, or occurs in multiple sets*) + let conditionally_set k n = + (occurs_in_nexp k n) || (occurs_in_nexp n k) || equate_n k n in + let set_nuvars_on_merge k n = + let def_try_set = merge_nuvars && is_all_nuvar n in + if def_try_set + then (conditionally_set n k),[],None + else if merge_nuvars + then match first_non_nu n with + | Some n' -> + if change_nuvar_base n k + then (true, [Eq(Patt(Parse_ast.Unknown),k,n')], None) + else (false, [Eq(Patt(Parse_ast.Unknown),k,n')], Some(Nexpmap.from_list [n',k])) + | None -> (false, [Eq(Patt(Parse_ast.Unknown),k,n)], None) + else (false,[],None) in let merged_constraints = make_merged_constraints Nexpmap.empty constraint_sets in + (*let _ = Printf.eprintf "merge branch constraints: found these shared var mappings %s\n%!" + (nexpmap_to_string merged_constraints) in*) let shared_path_distinct_constraints = Nexpmap.fold - (fun sc k v -> match v with - (*Variables only in one path get the assignments (other than nuvars) made on the path*) - | One n -> - (*let _ = Printf.eprintf "Variables in one path: merge_nuvars %b, key %s, one %s\n%!" merge_nuvars (n_to_string k) (n_to_string n) in*) - begin (match (k.nexp, n.nexp) with - | Nuvar _, Nuvar _ -> if merge_nuvars then ignore(equate_n n k) else () - | _ -> let occurs = (occurs_in_nexp k n) || (occurs_in_nexp n k) in - if not(occurs) then ignore(equate_n k n) else ()); - (*(Printf.eprintf "After setting key %s, one %s\n%!" (n_to_string k) (n_to_string n));*) - sc end - (*Variables on two paths get the assignment if they're the same, skipped if both nuvars, kept otherwise for later*) + (fun (sc,new_cs,new_map) k v -> match v with + | One n -> + (*let _ = Printf.eprintf "Variables in one path: merge_nuvars %b, key %s, one %s\n%!" + merge_nuvars (n_to_string k) (n_to_string n) in*) + let (_,new_cs',nm) = + (match (k.nexp, n.nexp) with + | Nuvar _, Nuvar _ -> set_nuvars_on_merge k n + | _ -> (conditionally_set k n,[],None)) in + (sc,new_cs'@new_cs,merge_option_maps nm new_map) | Two(n1,n2) -> - (*let _ = Printf.eprintf "Variables in two paths: merge_nuvars %b, key %s, n1 %s, n2 %s\n%!" merge_nuvars (n_to_string k) (n_to_string n1) (n_to_string n2) in*) + (*let _ = Printf.eprintf "Variables in two paths: merge_nuvars %b, key %s, n1 %s, n2 %s\n%!" + merge_nuvars (n_to_string k) (n_to_string n1) (n_to_string n2) in*) (match n1.nexp,n2.nexp with - | Nuvar _, Nuvar _ -> - if merge_nuvars && equate_n n1 k && equate_n n2 k - then sc - else sc - | _ -> - if nexp_eq n1 n2 - then if equate_n k n1 - then sc - else assert false (*There shouldn't be a reason that equate_n didn't work here*) - else Nexpmap.insert sc (k,v)) - (*Same as on two paths but more complicated logic*) + | Nuvar _, Nuvar _ -> + let (set1,ncs1,nm1) = set_nuvars_on_merge k n1 in + let (set2,ncs2,nm2) = set_nuvars_on_merge k n2 in + if (set1 && set2) + then (sc,ncs1@ncs2@new_cs,merge_option_maps new_map (merge_option_maps nm1 nm2)) + else (Nexpmap.insert sc (k,v),new_cs,merge_option_maps new_map (merge_option_maps nm1 nm2)) + | Nuvar _, _ -> + let (_,cs1, nm1) = set_nuvars_on_merge k n1 in + (Nexpmap.insert sc (k,v),cs1@new_cs,merge_option_maps new_map nm1) + | _, Nuvar _ -> + let (_,cs2, nm2) = set_nuvars_on_merge k n2 in + (Nexpmap.insert sc (k,v),cs2@new_cs,merge_option_maps new_map nm2) + | _ -> + if nexp_eq n1 n2 && conditionally_set k n1 && conditionally_set k n2 + then (sc,new_cs,new_map) + else (Nexpmap.insert sc (k,v),new_cs,new_map)) | Many ns -> - (*let _ = Printf.eprintf "Variables in many paths: merge_nuvars %b, key %s, [" merge_nuvars (n_to_string k) in + (*let _ = Printf.eprintf "Variables in many paths: merge_nuvars %b, key %s, [" + merge_nuvars (n_to_string k) in let _ = List.iter (fun n -> Printf.eprintf "%s " (n_to_string n)) ns in - let _ = Printf.eprintf "\n%!" in*) - if List.for_all (fun n -> match n.nexp with | Nuvar _ -> true | _ -> false) ns - then begin (List.iter (fun n -> ignore(merge_nuvars && equate_n n k)) ns); sc end + let _ = Printf.eprintf "\n%!" in*) + let sets = List.map (set_nuvars_on_merge k) ns in + let css = (List.flatten (List.map (fun (_,c,_) -> c) sets))@ new_cs in + let map = List.fold_right merge_option_maps (List.map (fun (_,_,m) -> m) sets) new_map in + if List.for_all (fun (b,_,_) -> b) sets + then (sc,css,map) else let rec all_eq = function | [] | [_] -> true | n1::n2::ns -> (nexp_eq n1 n2) && all_eq ns in - if all_eq ns && not(ns = []) - then if equate_n k (List.hd ns) then sc - else assert false (*Shouldn't happen, as above*) - else Nexpmap.insert sc (k,v)) Nexpmap.empty merged_constraints in - (*Find the variables in multiple sets, if not set the same then either skip, or if IN varaiables, check that assignments consistent with ranges; if not IN variables and set to constants, then send these out because they're essentially new IN variables and need to work in any seen range afterwards; if not IN variables, not set to constants, and not set to nuvars then these might be errors or parts that are too hard for the constraint solver. - *) + if (all_eq ns) && not(ns = []) + then if List.for_all (conditionally_set k) ns + then (sc,css, map) + else (Nexpmap.insert sc (k,v),css, map) + else (Nexpmap.insert sc (k,v),css, map)) + (Nexpmap.empty,[],None) merged_constraints in + (*let _ = if merge_nuvars then + Printf.eprintf "merge branch constraints: shared var mappings after merge %s\n%!" + (nexpmap_to_string merged_constraints) in *) shared_path_distinct_constraints let rec extract_path_substs = function @@ -2976,7 +3108,7 @@ let rec extract_path_substs = function Nexpmap.fold (fun substs key newvar -> match key.nexp with | Nuvar _ -> Nexpmap.insert substs (key,newvar) - | _ -> begin set key newvar; substs end) substs Nexpmap.empty in + | _ -> begin set key newvar; substs end) Nexpmap.empty substs in let (substs, cs_rest) = extract_path_substs cs in (updated_substs::substs, CondCons(l,k,Some(updated_substs),ps,es)::cs_rest) | c::cs -> @@ -2984,12 +3116,22 @@ let rec extract_path_substs = function (substs,c::cs_rest) let rec merge_paths merge_nuvars = function - | [] -> [] + | [] -> [],None | BranchCons(co,_,branches)::cs -> - let path_substs,branches_up = extract_path_substs branches in - let shared_vars = merge_branch_constraints merge_nuvars path_substs in - BranchCons(co,Some(shared_vars),branches_up)::(merge_paths merge_nuvars cs) - | c::cs -> c::merge_paths merge_nuvars cs + let branches_merged,new_map = merge_paths merge_nuvars branches in + let path_substs,branches_up = extract_path_substs branches_merged in + let (shared_vars,new_cs,nm) = merge_branch_constraints merge_nuvars path_substs in + let (rest_cs,rest_map) = merge_paths merge_nuvars cs in + let out_map = merge_option_maps (merge_option_maps new_map nm) rest_map in + (BranchCons(co,Some(shared_vars),branches_up)::(new_cs@rest_cs), out_map) + | CondCons(co,k,substs,ps,es)::cs -> + let (new_es,nm) = merge_paths merge_nuvars es in + let (rest_cs,rest_map) = merge_paths merge_nuvars cs in + (CondCons(co,k,substs,ps,new_es)::rest_cs, + merge_option_maps nm rest_map) + | c::cs -> + let (rest_cs, rest_map) = merge_paths merge_nuvars cs in + (c::rest_cs, rest_map) let rec equate_nuvars in_env cs = (*let _ = Printf.eprintf "equate_nuvars\n" in*) @@ -3006,13 +3148,13 @@ let rec equate_nuvars in_env cs = if (equate_n n1 n2) then equate cs else c::equate cs end else c::equate cs | _ -> c::equate cs) - | (CondCons(co,kind,None,pats,exps) as c):: cs -> + | CondCons(co,kind,substs,pats,exps):: cs -> (*let _ = Printf.eprintf "equate_nuvars: condcons: %s\n%!" (constraints_to_string [c]) in*) let pats' = equate pats in let exps' = equate exps in (match pats',exps' with | [],[] -> equate cs - | _ -> CondCons(co,kind,None,pats',exps')::(equate cs)) + | _ -> CondCons(co,kind,substs,pats',exps')::(equate cs)) | BranchCons(co,sv,branches)::cs -> let b' = equate branches in if [] = b' @@ -3030,7 +3172,7 @@ let rec constraint_size = function let rec simple_constraint_check in_env cs = let check = simple_constraint_check in_env in -(* let _ = Printf.eprintf "simple_constraint_check of %i constraints\n%!" (constraint_size cs) in*) + (*let _ = Printf.eprintf "simple_constraint_check of %i constraints\n%!" (constraint_size cs) in*) match cs with | [] -> [] | Eq(co,n1,n2)::cs -> @@ -3149,7 +3291,8 @@ let rec simple_constraint_check in_env cs = | None -> (check cs) | Some(c) -> c::(check cs)) | GtEq(co,enforce,n1,n2)::cs -> - (*let _ = Printf.eprintf ">= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *) + (*let _ = Printf.eprintf ">= check, about to normalize_nexp of %s, %s\n" + (n_to_string n1) (n_to_string n2) in *) let n1',n2' = normalize_nexp n1,normalize_nexp n2 in (*let _ = Printf.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in*) (match n1'.nexp,n2'.nexp with @@ -3188,7 +3331,8 @@ let rec simple_constraint_check in_env cs = ^ n_to_string new_n ^ " to be greater than or equal to 0, not " ^ string_of_big_int i) | _ -> GtEq(co,enforce,n1',n2')::(check cs)))) | Gt(co,enforce,n1,n2)::cs -> - (*let _ = Printf.eprintf "> check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *) + (*let _ = Printf.eprintf "> check, about to normalize_nexp of %s, %s\n" + (n_to_string n1) (n_to_string n2) in *) let n1',n2' = normalize_nexp n1,normalize_nexp n2 in (*let _ = Printf.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in*) (match nexp_gt n1' n2' with @@ -3207,7 +3351,8 @@ let rec simple_constraint_check in_env cs = ^ n_to_string new_n ^ " to be greater than or equal to 0, not " ^ string_of_big_int i) | _ -> Gt(co,enforce,n1',n2')::(check cs))) | LtEq(co,enforce,n1,n2)::cs -> - (*let _ = Printf.eprintf "<= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *) + (*let _ = Printf.eprintf "<= check, about to normalize_nexp of %s, %s\n" + (n_to_string n1) (n_to_string n2) in *) let n1',n2' = normalize_nexp n1,normalize_nexp n2 in (*let _ = Printf.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in *) (match n1'.nexp,n2'.nexp with @@ -3225,7 +3370,8 @@ let rec simple_constraint_check in_env cs = " to be less than or equal to " ^ (n_to_string n2)) | Maybe -> LtEq(co,enforce,n1',n2')::(check cs))) | Lt(co,enforce,n1,n2)::cs -> - (*let _ = Printf.eprintf "< check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *) + (*let _ = Printf.eprintf "< check, about to normalize_nexp of %s, %s\n" + (n_to_string n1) (n_to_string n2) in *) let n1',n2' = normalize_nexp n1,normalize_nexp n2 in (*let _ = Printf.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in *) (match n1'.nexp,n2'.nexp with @@ -3246,7 +3392,8 @@ let rec simple_constraint_check in_env cs = (*let _ = Printf.eprintf "Condcons check length pats %i, length exps %i\n" (List.length pats) (List.length exps) in*) let pats' = check pats in let exps' = check exps in - (*let _ = Printf.eprintf "Condcons after check length pats' %i, length exps' %i\n" (List.length pats') (List.length exps') in*) + (*let _ = Printf.eprintf "Condcons after check length pats' %i, length exps' %i\n" + (List.length pats') (List.length exps') in*) (match pats',exps' with | [],[] -> check cs | _ -> CondCons(co,kind,substs,pats',exps')::(check cs)) @@ -3257,6 +3404,7 @@ let rec simple_constraint_check in_env cs = if [] = b then check cs else BranchCons(co,sv,b)::(check cs) + | Predicate _::cs -> check cs | x::cs -> (*let _ = Printf.eprintf "In default case with %s\n%!" (constraints_to_string [x]) in*) x::(check cs) @@ -3285,28 +3433,25 @@ let do_resolve_constraints = ref true let resolve_constraints cs = (*let _ = Printf.eprintf "called resolve constraints with %i constraints\n" (constraint_size cs) in*) if not !do_resolve_constraints - then cs + then (cs,None) else let rec fix checker len cs = - (*let _ = Printf.eprintf "Calling fix check thunk, fix check point is %i\n%!" len in*) + (*let _ = Printf.eprintf "Calling fix check thunk, fix check point is %i\n%!" len in *) let cs' = checker (in_constraint_env cs) cs in let len' = constraint_size cs' in - (*let _ = Printf.eprintf "after checker, fix check point is %i\n%!" len' in*) if len > len' then fix checker len' cs' else cs' in (* let _ = Printf.eprintf "Original constraints are %s\n%!" (constraints_to_string cs) in*) let branch_freshened = prepare_constraints cs in - (*let _ = Printf.eprintf "Prepared constraints are %s\n%!" (constraints_to_string branch_freshened) in*) let nuvar_equated = fix equate_nuvars (constraint_size branch_freshened) branch_freshened in - (*let _ = Printf.eprintf "Nuvar_equated constraints are %s\n%!" (constraints_to_string nuvar_equated) in*) - let complex_constraints = - fix (fun in_env cs -> merge_paths false (simple_constraint_check in_env cs)) + let complex_constraints = + fix (fun in_env cs -> let (ncs,_) = merge_paths false (simple_constraint_check in_env cs) in ncs) (constraint_size nuvar_equated) nuvar_equated in - (*let _ = Printf.eprintf "simple and merge_pathed %s\n%!" (constraints_to_string complex_constraints) in*) - let complex_constraints = merge_paths true complex_constraints in - (*let _ = Printf.eprintf "Resolved as many constraints as possible, leaving %i\n" (constraint_size complex_constraints) in*) + let (complex_constraints,map) = merge_paths true complex_constraints in + (*let _ = Printf.eprintf "Resolved as many constraints as possible, leaving %i\n" + (constraint_size complex_constraints) in*) (*let _ = Printf.eprintf "%s\n" (constraints_to_string complex_constraints) in*) - complex_constraints + (complex_constraints,map) let check_tannot l annot imp_param constraints efs = diff --git a/src/type_internal.mli b/src/type_internal.mli index e753117b..78ca63e7 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -73,6 +73,7 @@ and t_arg = | TA_ord of order module Nexpmap : Finite_map.Fmap with type k = nexp +type nexp_map = nexp Nexpmap.t type tag = | Emp_local (* Standard value, variable, expression *) @@ -142,7 +143,7 @@ type variable_range = type bounds_env = | No_bounds - | Bounds of variable_range list + | Bounds of variable_range list * nexp_map option type t_params = (string * kind) list type tannot = @@ -213,6 +214,7 @@ val equate_t : t -> t -> unit val typ_subst : t_arg emap -> bool -> t -> t val subst : (Envmap.k * kind) list -> bool -> t -> nexp_range list -> effect -> t * nexp_range list * effect * t_arg emap +val subst_with_env : t_arg emap -> bool -> t -> nexp_range list -> effect -> t * nexp_range list * effect * t_arg emap val type_param_consistent : Parse_ast.l -> t_arg emap -> t_arg emap -> nexp_range list val get_abbrev : def_envs -> t -> (t * nexp_range list) @@ -222,6 +224,10 @@ val is_enum_typ : def_envs -> t -> int option val extract_bounds : def_envs -> string -> t -> bounds_env val merge_bounds : bounds_env -> bounds_env -> bounds_env val find_var_from_nexp : nexp -> bounds_env -> (string option * string) option +val add_map_to_bounds : nexp_map -> bounds_env -> bounds_env +val add_map_tannot : nexp_map -> tannot -> tannot +val get_map_tannot : tannot -> nexp_map option +val merge_option_maps : nexp_map option -> nexp_map option -> nexp_map option val expand_nexp : nexp -> nexp list val normalize_nexp : nexp -> nexp @@ -233,7 +239,7 @@ val select_overload_variant : def_envs -> bool -> bool -> tannot list -> t -> ta val split_conditional_constraints : nexp_range list -> (nexp_range list * nexp_range list) (*May raise an exception if a contradiction is found*) -val resolve_constraints : nexp_range list -> nexp_range list +val resolve_constraints : nexp_range list -> (nexp_range list * nexp_map option) (* whether to actually perform constraint resolution or not *) val do_resolve_constraints : bool ref |