Turn back on resolving branch nexp unification more than once. This is the right thing to do because otherwise the order of the resolution of branch constraints matters, and that's not easily controllable. This will require figuring out why it's infinite looping for ASL's checking rather than just turning it off.

2 files changed, 26 insertions, 15 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index 2221fa92..63942df8 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -298,7 +298,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
         | _ -> default)
     | P_app(id,pats) -> 
       let i = id_to_string id in
-      (*let _ = Printf.eprintf "checking constructor pattern %s\n" i in*)
+      (*let _ = Printf.eprintf "checking constructor pattern %s with expected type %s \n" i (t_to_string expect_t) 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 n,constraints,efl,efr,bounds)) -> 
@@ -315,12 +315,14 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
                       (P_aux(P_app(id,[]),(l,cons_tag_annot t' (Constructor n) dec_cs)),
                        Envmap.empty,dec_cs@ret_cs,nob,t')
               | [p] -> let (p',env,p_cs,bounds,u) = check_pattern envs emp_tag t1 p in
+                (*let _ = Printf.eprintf "return constraints are %s\n" (constraints_to_string ret_cs) in*)
                        (P_aux(P_app(id,[p']),
                               (l,cons_tag_annot t' (Constructor n) 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
+                (*let _ = Printf.eprintf "return constraints are %s\n" (constraints_to_string ret_cs) in*)
                         (P_aux(P_app(id,pats'),
                                (l,cons_tag_annot t' (Constructor n) dec_cs)),env,dec_cs@p_cs@ret_cs,bounds,t'))
             | _ -> typ_error l ("Identifier " ^ i ^ " must be a union constructor"))
@@ -2319,8 +2321,8 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       (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)
     | _ , _->
-      (*let _ = Printf.eprintf "checking %s, not in env\n%!" id in
-      let t_env = if is_rec then Envmap.insert t_env (id,tannot) else t_env in*)
+      (*let _ = Printf.eprintf "checking %s, not in env\n%!" id in*)
+      (*let t_env = if is_rec then Envmap.insert t_env (id,tannot) else t_env in*)
       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
@@ -2457,7 +2459,7 @@ let check_def envs def =
     let t = (typ_to_t envs false false typ) in
     let i = id_to_string id in
     let tannot = into_register d_env (Base(([],t),External (Some i),[],pure_e,pure_e,nob)) in
-   (* let _ = Printf.eprintf "done checking reg dec\n" in*)
+   (*let _ = Printf.eprintf "done checking reg dec\n" in*)
     (DEF_reg_dec(DEC_aux(DEC_reg(typ,id),(l,tannot))),(Env(d_env,Envmap.insert t_env (i,tannot),b_env, tp_env)))
   | DEF_reg_dec(DEC_aux(DEC_alias(id,aspec), (l,annot))) -> 
     (*let _ = Printf.eprintf "checking reg dec b\n" in*)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 2e440186..2770d827 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -328,6 +328,8 @@ and n_to_string n =
     if !debug_mode
     then
       let rec show_nuvar n = match n.nexp with
+        | Nuvar{insubst=None; nindex = i; orig_var = Some s} -> s^ "()"
+        | Nuvar{insubst=Some n; nindex = i; orig_var = Some s} -> s ^ "(" ^ show_nuvar n ^ ")"
         | Nuvar{insubst=None; nindex = i;} -> "Nu_" ^ string_of_int i ^ "()" 
         | Nuvar{insubst=Some n; nindex =i;} -> "Nu_" ^ string_of_int i ^ "(" ^ show_nuvar n ^ ")"
         | _ -> n_to_string n in
@@ -2808,7 +2810,8 @@ let rec typ_param_eq l spec_param fun_param =
     | (_,[]) -> 
       raise (Reporting_basic.err_typ l "Specification type variables and function definition variables must match")
     | ([],_) -> 
-      raise (Reporting_basic.err_typ l "Function definition declares more type variables than specification variables")
+      raise
+        (Reporting_basic.err_typ l "Function definition declares more type variables than specification variables")
     | ((ids,tas)::spec_param,(idf,taf)::fun_param) ->
       if ids=idf
       then match (tas,taf) with
@@ -2895,7 +2898,8 @@ let rec t_to_typ t =
     | Tvar i -> Typ_aux(Typ_var (Kid_aux((Var i),Parse_ast.Unknown)),Parse_ast.Unknown) 
     | Tfn(t1,t2,_,e) -> Typ_aux(Typ_fn (t_to_typ t1, t_to_typ t2, e_to_ef e),Parse_ast.Unknown)
     | Ttup ts -> Typ_aux(Typ_tup(List.map t_to_typ ts),Parse_ast.Unknown)
-    | Tapp(i,args) -> Typ_aux(Typ_app(Id_aux((Id i), Parse_ast.Unknown),List.map targ_to_typ_arg args),Parse_ast.Unknown)
+    | Tapp(i,args) ->
+      Typ_aux(Typ_app(Id_aux((Id i), Parse_ast.Unknown),List.map targ_to_typ_arg args),Parse_ast.Unknown)
     | Tabbrev(t,_) -> t_to_typ t
     | Tuvar _ | Toptions _ -> Typ_aux(Typ_var (Kid_aux((Var "fresh"),Parse_ast.Unknown)),Parse_ast.Unknown)
 and targ_to_typ_arg targ = 
@@ -3749,7 +3753,7 @@ let nexpmap_to_string nmap =
       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
+      | Many ns -> "(" ^ n_to_string k ^ " |-> (" ^ string_of_list ", " n_to_string ns ^ ") : " ^ (string_of_list ", " (fun n -> if is_all_nuvar n then "true" else "false") ns) ^ ") " ^ acc) "" nmap
 
 let rec make_merged_constraints acc =  function
   | [] -> acc
@@ -3772,11 +3776,11 @@ let merge_branch_constraints merge_nuvars constraint_sets =
   (*Separate variables into only occurs in one set, or occurs in multiple sets*)
   (*assumes k and n outermost and all nuvar*)
   let conditionally_set k n =
-    not(merge_nuvars) || ((occurs_in_nexp k n) || (occurs_in_nexp n k) || equate_n k n) in
+    not(merge_nuvars) || ((occurs_in_nexp k n) || (occurs_in_nexp n k) || equate_n k n || equate_n n k) in
   (*This function assumes n outermost and k all nuvar; 
     inserts a new nuvar at bottom, and an eq to k for non-nuvar*)
   let conditionally_lift_to_nuvars_on_merge k n =
-    if not(merge_nuvars) || is_all_nuvar n 
+    if not(merge_nuvars) || (is_all_nuvar n && conditionally_set k n)
     then [],None
     else
       let new_nuvar = new_n () in
@@ -3817,16 +3821,19 @@ let merge_branch_constraints merge_nuvars constraint_sets =
               else (Nexpmap.insert sc (k,v),new_cs,merge_option_maps new_map (merge_option_maps nm1 nm2))
             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 _ = List.iter (fun n -> Printf.eprintf "%s ;" (n_to_string n)) ns in
-      let _ = Printf.eprintf "]\n%!" in*)
+      (*(if merge_nuvars then
+        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
+        let _ = Printf.eprintf "Is all nuvar? %b\n%!" 
+        (List.for_all is_all_nuvar (List.map get_outer_most ns)) in ());*)
       let k, ns = get_outer_most k, List.map get_outer_most ns in
       let is_all_nuvars = List.for_all is_all_nuvar ns in
       if not(merge_nuvars)
       then Nexpmap.insert sc (k,v),new_cs,new_map
       else if is_all_nuvars
-      then if List.for_all (conditionally_set k) ns
+      then if List.for_all (fun i -> i) (List.map (conditionally_set k) ns)
         then (sc,new_cs,new_map)
         else (Nexpmap.insert sc (k,v),new_cs,new_map)
       else
@@ -3836,7 +3843,7 @@ let merge_branch_constraints merge_nuvars constraint_sets =
             (nexp_eq n1 n2) && all_eq (n2::ns) 
         in 
         if (all_eq ns) && not(ns=[])
-        then if List.for_all (conditionally_set k) ns
+        then if List.for_all (fun i -> i) (List.map (conditionally_set k) ns)
           then  (sc,new_cs,new_map)
           else (Nexpmap.insert sc (k,v),new_cs,new_map)
         else            
@@ -3848,6 +3855,8 @@ let merge_branch_constraints merge_nuvars constraint_sets =
   (*let _ = if merge_nuvars then
       Printf.eprintf "merge branch constraints: shared var mappings after merge %s\n%!"
         (nexpmap_to_string merged_constraints) in*)
+  if merge_nuvars then Nexpmap.fold merge_walker (Nexpmap.empty,[],None) merged_constraints
+  else 
   shared_path_distinct_constraints
 
 let rec extract_path_substs = function