diff options
| -rw-r--r-- | src/type_check.ml | 8 | ||||
| -rw-r--r-- | src/type_internal.ml | 20 |
2 files changed, 16 insertions, 12 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 3c38ab83..674e6a4a 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -359,7 +359,8 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) ((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 (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 let t = match (ord.order,d_env.default_o.order) with @@ -374,8 +375,9 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) TA_ord{order=Odec}; TA_typ u;])} | _ -> raise (Reporting_basic.err_unreachable l "Default order not set") in + let _,v_cs = type_consistent (Patt l) d_env Guarantee true t expect_t in (*TODO Should gather the constraints here, with regard to the expected base and rise, and potentially reset them above*) - (P_aux(P_vector(pats'),(l,cons_tag_annot t emp_tag cs)), env,cs@constraints,bounds,t) + (P_aux(P_vector(pats'),(l,cons_tag_annot t emp_tag (cs@v_cs))), env,cs@v_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 @@ -2079,7 +2081,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let funcls,cs_ef = check t_env t_param_env None in 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 _ = Printf.eprintf "unresolved constraints are %s\n%!" (constraints_to_string cs) 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*) diff --git a/src/type_internal.ml b/src/type_internal.ml index 51b03883..9fcfa3e7 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -3748,21 +3748,23 @@ let merge_branch_constraints merge_nuvars constraint_sets = then (sc,new_cs,new_map) else (Nexpmap.insert sc (k,v),new_cs,new_map) else - let sets = List.map (conditionally_lift_to_nuvars_on_merge k) ns in - let css = (List.flatten (List.map fst sets))@ new_cs in - let map = List.fold_right merge_option_maps (List.map snd sets) new_map in let rec all_eq = function | [] | [_] -> true - | n1::n2::ns -> - (nexp_eq n1 n2) && all_eq ns + | n1::n2::ns -> + (*let _ = Printf.eprintf "all_eq with %s and %s returning %b\n" (n_to_string n1) (n_to_string n2) (nexp_eq n1 n2) in*) + (nexp_eq n1 n2) && all_eq (n2::ns) in - if (all_eq ns) && not(ns = []) + if (all_eq ns) && not(ns=[]) then if List.for_all (conditionally_set k) ns - then (sc,new_cs,new_map) + then (sc,new_cs,new_map) else (Nexpmap.insert sc (k,v),new_cs,new_map) - else (Nexpmap.insert sc (k,v),css, map)) + else + let sets = List.map (conditionally_lift_to_nuvars_on_merge k) ns in + let css = (List.flatten (List.map fst sets))@ new_cs in + let map = List.fold_right merge_option_maps (List.map snd sets) new_map in + (Nexpmap.insert sc (k,v),css, map)) (Nexpmap.empty,[],None) merged_constraints in - (*let _ = if merge_nuvars then + (* 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 |