Put conditional path information into constraint gathering so that checking uses appropriate information gleaned from pattern matching

6 files changed, 35 insertions, 27 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 709eb42b..9f1d46d2 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -676,7 +676,7 @@ let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (typ_env : tan
   List.iter 
     (fun (id,(d,k)) -> 
       (match !d with
-      | (d,false) -> typ_error Unknown "Scattered definition never ended" (Some id) None None
+      | (d,false) -> typ_error Parse_ast.Unknown "Scattered definition never ended" (Some id) None None
       | (_, true) -> ()))
     partial_defs;
   (Defs defs),k_env
diff --git a/src/parser.mly b/src/parser.mly
index 06b26765..3c3cf8e0 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -95,7 +95,7 @@ let mk_namesectn _ = Name_sect_aux(Name_sect_none,Unknown)
 let make_range_sugar_bounded typ1 typ2 =
   ATyp_app(Id_aux(Id("range"),Unknown),[typ1; typ2;])
 let make_range_sugar typ1 =
-  make_range_sugar_bounded typ1 (ATyp_aux(ATyp_constant(0), Unknown))
+  make_range_sugar_bounded (ATyp_aux(ATyp_constant(0), Unknown)) typ1
 
 let make_r bot top =
   match bot,top with
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index cfefd4d0..f0dea03f 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -357,7 +357,7 @@ let pp_def ppf d =
   | DEF_fundef(f_def) -> pp_fundef ppf f_def
   | DEF_val(lbind) -> fprintf ppf "@[<0>%a@]@\n" pp_let lbind
   | DEF_reg_dec(dec) -> pp_dec ppf dec
-  | _ -> raise (Reporting_basic.err_unreachable Unknown "initial_check didn't remove all scattered Defs")
+  | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs")
 
 let pp_defs ppf (Defs(defs)) =
   fprintf ppf "@[%a@]@\n" (list_pp pp_def pp_def) defs
@@ -592,9 +592,9 @@ let pp_format_nes nes =
        | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
        | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
        | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
-       | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) |InOpen(_,{nexp=Nvar i},ns)-> 
+       | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) -> 
 	 "(Nec_in \"" ^ i ^ "\" [" ^ (list_format "; " string_of_int ns)^ "])"
-       | InS(_,{nexp = Nuvar _},ns) | InOpen(_,{nexp = Nuvar _},ns) ->  
+       | InS(_,{nexp = Nuvar _},ns)  ->  
 	 "(Nec_in \"fresh\" [" ^ (list_format "; " string_of_int ns)^ "])"
      )
      nes) ^*) "]"
@@ -810,7 +810,7 @@ let pp_lem_def ppf d =
   | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a);" pp_lem_fundef f_def
   | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);" pp_lem_let lbind
   | DEF_reg_dec(dec) -> fprintf ppf "(DEF_reg_dec %a);" pp_lem_dec dec
-  | _ -> raise (Reporting_basic.err_unreachable Unknown "initial_check didn't remove all scattered Defs")
+  | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs")
 
 let pp_lem_defs ppf (Defs(defs)) =
   fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs
diff --git a/src/type_check.ml b/src/type_check.ml
index 2bb5700d..f8a5cb52 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -530,8 +530,10 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       let (cond',_,_,c1,ef1) = check_exp envs bool_t cond in
       let then',then_t,then_env,then_c,then_ef = check_exp envs expect_t then_ in
       let else',else_t,else_env,else_c,else_ef = check_exp envs expect_t else_ in
+      let t_cs = CondCons((Expr l),c1,then_c) in
+      let e_cs = CondCons((Expr l),[],else_c) in
       (E_aux(E_if(cond',then',else'),(l,Some(([],expect_t),Emp_local,[],pure_e))),
-       expect_t,Envmap.intersect_merge (tannot_merge (Expr l) d_env) then_env else_env,then_c@else_c@c1,
+       expect_t,Envmap.intersect_merge (tannot_merge (Expr l) d_env) then_env else_env,[t_cs;e_cs],
        union_effects ef1 (union_effects then_ef else_ef))
     | E_for(id,from,to_,step,order,block) -> 
       let fb,fr,tb,tr,sb,sr = new_n(),new_n(),new_n(),new_n(),new_n(),new_n() in
@@ -883,15 +885,17 @@ and check_cases envs check_t expect_t pexps : ((tannot pexp) list * typ * nexp_r
     | [] -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "switch with no cases found")
     | [(Pat_aux(Pat_exp(pat,exp),(l,annot)))] ->
       let pat',env,cs_p,u = check_pattern envs Emp_local check_t pat in
-      let (e,t,_,cs2,ef) = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env env)) expect_t exp in
-      [Pat_aux(Pat_exp(pat',e),(l,Some(([],t),Emp_local,cs_p@cs2,ef)))],t,cs_p@cs2,ef
+      let e,t,_,cs_e,ef = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env env)) expect_t exp in
+      let cs = [CondCons(Expr l, cs_p, cs_e)] in
+      [Pat_aux(Pat_exp(pat',e),(l,Some(([],t),Emp_local,cs,ef)))],t,cs,ef
     | ((Pat_aux(Pat_exp(pat,exp),(l,annot)))::pexps) ->
       let pat',env,cs_p,u = check_pattern envs Emp_local check_t pat in
-      let (e,t,_,cs2,ef) = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env env)) expect_t exp in
-      let (pes,tl,csl,efl) = check_cases envs check_t expect_t pexps in
-      ((Pat_aux(Pat_exp(pat',e),(l,(Some(([],t),Emp_local,(cs_p@cs2),ef)))))::pes,
+      let (e,t,_,cs_e,ef) = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env env)) expect_t exp in
+      let cs = CondCons(Expr l,cs_p,cs_e) in
+      let (pes,tl,csl,efl) = check_cases envs check_t expect_t pexps in      
+      ((Pat_aux(Pat_exp(pat',e),(l,(Some(([],t),Emp_local,[cs],ef)))))::pes,
        tl,
-       csl@cs_p@cs2,union_effects efl ef)
+       cs::csl,union_effects efl ef)
 
 and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot emap * tag *nexp_range list *effect ) =
   let (Env(d_env,t_env)) = envs in
@@ -1242,12 +1246,13 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
   let check t_env =
     List.split
       (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),l)) ->
-	let (pat',t_env',constraints',t') = check_pattern (Env(d_env,t_env)) Emp_local param_t pat in
+	let (pat',t_env',cs_p,t') = check_pattern (Env(d_env,t_env)) Emp_local param_t pat in
         (*let _ = Printf.printf "about to check that %s and %s are consistent\n" (t_to_string t') (t_to_string param_t) in*)
-	let exp',_,_,constraints,ef = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env t_env')) ret_t exp in
+	let exp',_,_,cs_e,ef = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env t_env')) ret_t exp in
         (*let _ = Printf.printf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) 
 	(*let _ = (Pretty_print.pp_exp Format.std_formatter) exp' in*)
-	(FCL_aux((FCL_Funcl(id,pat',exp')),l),((constraints'@constraints),ef))) funcls) in
+	let cs = [CondCons(Fun l,cs_p,cs_e)] in
+	(FCL_aux((FCL_Funcl(id,pat',exp')),l),(cs,ef))) funcls) in
   match (in_env,tannot) with
     | Some(Some( (params,u),Spec,constraints,eft)), Some( (p',t),_,c',eft') ->
       (*let _ = Printf.printf "Function %s is in env\n" id in*)
@@ -1256,7 +1261,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       let t_env = if is_rec then t_env else Envmap.remove t_env id in
       let funcls,cs_ef = check t_env in
       let cs,ef = ((fun (cses,efses) -> (List.concat cses),(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in
-      let cs' = resolve_constraints cs in
+      let cs' = resolve_constraints cs@constraints in
       let tannot = check_tannot l tannot cs' ef in
       (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))),
       Env(d_env,Envmap.insert t_env (id,tannot))
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 1aa31473..85537b83 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -70,7 +70,7 @@ type tag =
 type constraint_origin =
   | Patt of Parse_ast.l
   | Expr of Parse_ast.l
-  | Abre of Parse_ast.l
+  | Fun of Parse_ast.l
   | Specc of Parse_ast.l
 
 (* Constraints for nexps, plus the location which added the constraint *)
@@ -80,7 +80,7 @@ type nexp_range =
   | GtEq of constraint_origin * nexp * nexp
   | In of constraint_origin * string * int list
   | InS of constraint_origin * nexp * int list (* This holds the given value for string after a substitution *)
-  | InOpen of constraint_origin * nexp * int list (* This holds a non-exhaustive value/s for a var or nuvar during constraint gathering *)
+  | CondCons of constraint_origin * nexp_range list * nexp_range list
 
 type t_params = (string * kind) list
 type tannot = ((t_params * t) * tag * nexp_range list * effect) option
@@ -104,7 +104,7 @@ let get_index n =
    | _ -> assert false
 
 let get_c_loc = function
-  | Patt l | Expr l | Abre l | Specc l -> l
+  | Patt l | Expr l | Specc l -> l
 
 let rec string_of_list sep string_of = function
   | [] -> ""
@@ -675,8 +675,8 @@ let rec cs_subst t_env cs =
     | LtEq(l,n1,n2)::cs -> LtEq(l,n_subst t_env n1, n_subst t_env n2)::(cs_subst t_env cs)
     | In(l,s,ns)::cs -> InS(l,n_subst t_env {nexp=Nvar s},ns)::(cs_subst t_env cs)
     | InS(l,n,ns)::cs -> InS(l,n_subst t_env n,ns)::(cs_subst t_env cs)
-    | InOpen(l,n,ns)::cs -> InOpen(l,n_subst t_env n,ns)::(cs_subst t_env cs)
-
+    | CondCons(l, pats, exps)::cs -> CondCons(l, cs_subst t_env pats, cs_subst t_env exps)::(cs_subst t_env cs)
+      
 let subst k_env t cs e =
   let subst_env = Envmap.from_list
     (List.map (fun (id,k) -> (id, 
@@ -1076,9 +1076,12 @@ let rec simple_constraint_check in_env cs =
         then begin resolve_nsubst n1; resolve_nsubst n2; equate_n n1' n2'; None end
         else Some(Eq(co,n1',n2'))
       | _,_ -> Some(Eq(co,n1',n2'))) in
-    (match check_eq true n1 n2 with
-    | None -> (check cs)
-    | Some(c) -> c::(check cs))
+    (match contains_in_vars in_env n1, contains_in_vars in_env n2 with
+      | None,None ->	
+	(match check_eq true n1 n2 with
+	  | None -> (check cs)
+	  | Some(c) -> c::(check cs))
+      | _ -> (Eq(co,n1,n2)::(check cs)))
   | GtEq(co,n1,n2)::cs -> 
 (*    let _ = Printf.printf ">= check, about to eval_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *)
     let n1',n2' = eval_nexp n1,eval_nexp n2 in
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 07b0e746..04c5bf9c 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -65,7 +65,7 @@ type tag =
 type constraint_origin =
   | Patt of Parse_ast.l
   | Expr of Parse_ast.l
-  | Abre of Parse_ast.l
+  | Fun of Parse_ast.l
   | Specc of Parse_ast.l
 
 (* Constraints for nexps, plus the location which added the constraint *)
@@ -75,7 +75,7 @@ type nexp_range =
   | GtEq of constraint_origin * nexp * nexp
   | In of constraint_origin * string * int list
   | InS of constraint_origin * nexp * int list (* This holds the given value for string after a substitution *)
-  | InOpen of constraint_origin * nexp * int list (* This holds a non-exhaustive value/s for a var or nuvar during constraint gathering *)
+  | CondCons of constraint_origin * nexp_range list * nexp_range list (* Constraints from one path from a conditional (pattern or if) and the constraints from that conditional *)
 
 val get_c_loc : constraint_origin -> Parse_ast.l