summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/reporting_basic.ml14
-rw-r--r--src/reporting_basic.mli4
-rw-r--r--src/type_check.ml16
-rw-r--r--src/type_internal.ml214
-rw-r--r--src/type_internal.mli3
5 files changed, 196 insertions, 55 deletions
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index f3120833..0e2a2e17 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -125,13 +125,18 @@ let loc_to_string l =
let s = Format.flush_str_formatter () in
s
-type pos_or_loc = Loc of Parse_ast.l | Pos of Lexing.position
+type pos_or_loc = Loc of Parse_ast.l | LocD of Parse_ast.l * Parse_ast.l | Pos of Lexing.position
let print_err_internal fatal verb_loc p_l m1 m2 =
- let _ = (match p_l with Pos p -> print_err_pos p | Loc l -> print_err_loc l) in
+ let _ = (match p_l with Pos p -> print_err_pos p
+ | Loc l -> print_err_loc l
+ | LocD (l1,l2) ->
+ print_err_loc l1; Format.fprintf Format.err_formatter " and "; print_err_loc l2) in
let m12 = if String.length m2 = 0 then "" else ": " in
Format.eprintf " %s%s%s\n" m1 m12 m2;
- if verb_loc then (match p_l with Loc l -> format_loc_source Format.err_formatter l; Format.pp_print_newline Format.err_formatter (); | _ -> ());
+ if verb_loc then (match p_l with Loc l ->
+ format_loc_source Format.err_formatter l;
+ Format.pp_print_newline Format.err_formatter (); | _ -> ());
Format.pp_print_flush Format.err_formatter ();
if fatal then (exit 1) else ()
@@ -147,6 +152,7 @@ type error =
| Err_syntax_locn of Parse_ast.l * string
| Err_lex of Lexing.position * string
| Err_type of Parse_ast.l * string
+ | Err_type_dual of Parse_ast.l * Parse_ast.l * string
let dest_err = function
| Err_general (l, m) -> ("Error", false, Loc l, m)
@@ -156,6 +162,7 @@ let dest_err = function
| Err_syntax_locn (l, m) -> ("Syntax error", false, Loc l, m)
| Err_lex (p, s) -> ("Lexical error", false, Pos p, s)
| Err_type (l, m) -> ("Type error", false, Loc l, m)
+ | Err_type_dual(l1,l2,m) -> ("Type error", false, LocD (l1,l2), m)
exception Fatal_error of error
@@ -164,6 +171,7 @@ let err_todo l m = Fatal_error (Err_todo (l, m))
let err_unreachable l m = Fatal_error (Err_unreachable (l, m))
let err_general l m = Fatal_error (Err_general (l, m))
let err_typ l m = Fatal_error (Err_type (l,m))
+let err_typ_dual l1 l2 m = Fatal_error (Err_type_dual (l1,l2,m))
let report_error e =
let (m1, verb_pos, pos_l, m2) = dest_err e in
diff --git a/src/reporting_basic.mli b/src/reporting_basic.mli
index 462d2394..7362d44c 100644
--- a/src/reporting_basic.mli
+++ b/src/reporting_basic.mli
@@ -85,6 +85,7 @@ type error =
| Err_syntax_locn of Parse_ast.l * string
| Err_lex of Lexing.position * string
| Err_type of Parse_ast.l * string
+ | Err_type_dual of Parse_ast.l * Parse_ast.l * string
exception Fatal_error of error
@@ -100,6 +101,9 @@ val err_unreachable : Parse_ast.l -> string -> exn
(** [err_typ l m] is an abreviatiation for [Fatal_error (Err_type (l, m))] *)
val err_typ : Parse_ast.l -> string -> exn
+(** [err_typ_dual l1 l2 m] is an abreviatiation for [Fatal_error (Err_type_dual (l1, l2, m))] *)
+val err_typ_dual : Parse_ast.l -> Parse_ast.l -> string -> exn
+
(** Report error should only be used by main to print the error in the end. Everywhere else,
raising a [Fatal_error] exception is recommended. *)
val report_error : error -> 'a
diff --git a/src/type_check.ml b/src/type_check.ml
index 277b5790..1b320d5d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -874,7 +874,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
(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 true bit_t cond in
- let (c1p,c1n) = split_conditional_constraints c1 in
+ let (c1,c1p,c1n) = split_conditional_constraints c1 in
(match expect_t.t with
| Tuvar _ ->
let then',then_t,then_env,then_c,then_bs,then_ef = check_exp envs imp_param true (new_t ()) then_ in
@@ -889,7 +889,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
let resulting_env = Envmap.intersect_merge (tannot_merge (Expr l) d_env true) then_env else_env in
(E_aux(E_if(cond',then',else'),(l,simple_annot_efr expect_t sub_effects)),
expect_t, resulting_env,
- [BranchCons(Expr l, None, [t_cs;e_cs])],
+ c1@[BranchCons(Expr l, None, [t_cs;e_cs])],
merge_bounds then_bs else_bs, (*TODO Should be an intersecting merge*)
sub_effects)
| _ ->
@@ -900,7 +900,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
let sub_effects = union_effects ef1 (union_effects then_ef else_ef) in
(E_aux(E_if(cond',then',else'),(l,simple_annot_efr expect_t sub_effects)),
expect_t,Envmap.intersect_merge (tannot_merge (Expr l) d_env true) then_env else_env,
- [BranchCons(Expr l, None, [t_cs;e_cs])],
+ c1@[BranchCons(Expr l, None, [t_cs;e_cs])],
merge_bounds then_bs else_bs,
sub_effects))
| E_for(id,from,to_,step,order,block) ->
@@ -2057,19 +2057,19 @@ 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 _ = 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
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
+ (*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
+ (*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)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index eb5e7898..c4bdc902 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1546,79 +1546,152 @@ let rec refine_guarantees check_nvar max_lt min_gt id cs =
let no_match _ =
let (cs,max,min) = refine_guarantees check_nvar max_lt min_gt id cs in
curr::cs,max,min in
- (match nes.nexp,check_nvar,max_lt with
- | Nuvar _ ,false, None | Nvar _ , true, None ->
+ (*let _ = Printf.eprintf "refine_guarantee %s\n" (constraints_to_string [curr]) in*)
+ (match nes.nexp,neb.nexp,check_nvar,max_lt,min_gt with
+ | Nuvar _ , _, false, None, _ | Nvar _, _, true, None, _ ->
+ (*let _ = Printf.eprintf "in var nill case of <=\n" in *)
if nexp_eq id nes
then match neb.nexp with
| Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
| _ -> refine_guarantees check_nvar (Some(c,neb)) min_gt id cs (*new max*)
else no_match ()
- | Nuvar _, false, Some(cm, omax) | Nvar _ , true,Some(cm, omax) ->
+ | _ , Nuvar _, false, _, None | _,Nvar _, true, _, None ->
+ (*let _ = Printf.eprintf "in var nill case of <=\n" in *)
+ if nexp_eq id neb
+ then match nes.nexp with
+ | Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
+ | _ -> refine_guarantees check_nvar max_lt (Some(c,nes)) id cs (*new min*)
+ else no_match ()
+ | Nuvar _, _, false, Some(cm, omax), _ | Nvar _, _, true,Some(cm, omax), _ ->
+ (*let _ = Printf.eprintf "in var case of <=\n" in *)
if nexp_eq id nes
then match nexp_ge neb omax with
| Yes -> refine_guarantees check_nvar (Some(c,neb)) min_gt id cs (*replace old max*)
| No -> refine_guarantees check_nvar max_lt min_gt id cs (*remove redundant constraint *)
| Maybe -> no_match ()
- else no_match ()
- | _ -> no_match ())
+ else no_match ()
+ | _, Nuvar _, false, _, Some(cm, omin) | _, Nvar _, true,_, Some(cm, omin) ->
+ (*let _ = Printf.eprintf "in var case of <=\n" in *)
+ if nexp_eq id neb
+ then match nexp_le nes omin with
+ | Yes -> refine_guarantees check_nvar max_lt (Some(c,nes)) id cs (*replace old min*)
+ | No -> refine_guarantees check_nvar max_lt min_gt id cs (*remove redundant constraint *)
+ | Maybe -> no_match ()
+ else no_match ()
+ | _ -> no_match ())
| (Lt(c,Guarantee,nes,neb) as curr)::cs ->
let no_match _ =
let (cs,max,min) = refine_guarantees check_nvar max_lt min_gt id cs in
curr::cs,max,min in
- (match nes.nexp,check_nvar,max_lt with
- | Nuvar _, false, None | Nvar _, true, None->
+ (*let _ = Printf.eprintf "refine_guarantee %s\n" (constraints_to_string [curr]) in*)
+ (match nes.nexp,neb.nexp,check_nvar,max_lt,min_gt with
+ | Nuvar _, _, false, None, _ | Nvar _, _, true, None, _->
+ (*let _ = Printf.eprintf "in var, nil case of <\n" in *)
if nexp_eq id nes
then match neb.nexp with
| Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
| _ -> refine_guarantees check_nvar (Some(c,neb)) min_gt id cs (*new max*)
else no_match ()
- | Nuvar _, false, Some(cm, omax) | Nvar _, true, Some(cm, omax) ->
+ | _, Nuvar _, false, _, None | _, Nvar _, true, _, None->
+ (*let _ = Printf.eprintf "in var, nil case of <\n" in *)
+ if nexp_eq id neb
+ then match nes.nexp with
+ | Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
+ | _ -> refine_guarantees check_nvar max_lt (Some(c,nes)) id cs (*new max*)
+ else no_match ()
+ | Nuvar _, _, false, Some(cm, omax), _ | Nvar _, _, true, Some(cm, omax), _ ->
+ (*let _ = Printf.eprintf "in var case of <\n" in *)
if nexp_eq id nes
then match nexp_gt neb omax with
| Yes -> refine_guarantees check_nvar (Some(c,neb)) min_gt id cs (*replace old max*)
| No -> refine_guarantees check_nvar max_lt min_gt id cs (*remove redundant constraint*)
| Maybe -> no_match ()
else no_match ()
+ | _, Nuvar _, false, _, Some(cm, omin) | _, Nvar _, true, _, Some(cm, omin) ->
+ (*let _ = Printf.eprintf "in var case of <\n" in *)
+ if nexp_eq id neb
+ then match nexp_lt nes omin with
+ | Yes -> refine_guarantees check_nvar max_lt (Some(c,nes)) id cs (*replace old min*)
+ | No -> refine_guarantees check_nvar max_lt min_gt id cs (*remove redundant constraint*)
+ | Maybe -> no_match ()
+ else no_match ()
| _ -> no_match ())
| (GtEq(c,Guarantee,nes,neb) as curr)::cs ->
+ (*let _ = Printf.eprintf "refine_guarantee %s\n" (constraints_to_string [curr]) in*)
let no_match _ =
let (cs,max,min) = refine_guarantees check_nvar max_lt min_gt id cs in
curr::cs,max,min in
- (match nes.nexp,check_nvar,min_gt with
- | Nuvar _, false, None | Nvar _, true, None->
+ (match nes.nexp,neb.nexp,check_nvar,min_gt,max_lt with
+ | Nuvar _, _, false, None, _ | Nvar _, _, true, None, _->
+ (*let _ = Printf.eprintf "in var, nil case of >=\n" in *)
if nexp_eq id nes
then match neb.nexp with
| Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
| _ -> refine_guarantees check_nvar max_lt (Some(c,neb)) id cs (*new min*)
else no_match ()
- | Nuvar _, false, Some(cm, omin) | Nvar _, true, Some(cm, omin) ->
+ | _, Nuvar _, false, _, None | _, Nvar _, true, _, None->
+ (*let _ = Printf.eprintf "in var, nil case of >=\n" in *)
+ if nexp_eq id neb
+ then match nes.nexp with
+ | Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
+ | _ -> refine_guarantees check_nvar (Some(c,nes)) min_gt id cs (*new max*)
+ else no_match ()
+ | Nuvar _, _, false, Some(cm, omin), _ | Nvar _, _, true, Some(cm, omin), _ ->
+ (*let _ = Printf.eprintf "in var case of >=\n" in *)
if nexp_eq id nes
then match nexp_le neb omin with
| Yes -> refine_guarantees check_nvar max_lt (Some(c,neb)) id cs (*replace old min*)
| No -> refine_guarantees check_nvar max_lt min_gt id cs (*remove redundant constraint*)
| Maybe -> no_match ()
else no_match ()
+ | _, Nuvar _, false, _, Some(cm, omax) | _, Nvar _, true, _, Some(cm, omax) ->
+ (*let _ = Printf.eprintf "in var case of >=\n" in *)
+ if nexp_eq id neb
+ then match nexp_ge nes omax with
+ | Yes -> refine_guarantees check_nvar (Some(c,nes)) min_gt id cs (*replace old max*)
+ | No -> refine_guarantees check_nvar max_lt min_gt id cs (*remove redundant constraint*)
+ | Maybe -> no_match ()
+ else no_match ()
| _ -> no_match ())
| (Gt(c,Guarantee,nes,neb) as curr)::cs ->
let no_match _ =
let (cs,max,min) = refine_guarantees check_nvar max_lt min_gt id cs in
curr::cs,max,min in
- (match nes.nexp,check_nvar,min_gt with
- | Nuvar _, false, None | Nvar _, true, None->
+ (* let _ = Printf.eprintf "refine_guarantee %s\n" (constraints_to_string [curr]) in*)
+ (match nes.nexp,neb.nexp,check_nvar,min_gt,max_lt with
+ | Nuvar _,_, false, None,_ | Nvar _, _, true, None,_->
+ (*let _ = Printf.eprintf "in var, nil case of >\n" in *)
if nexp_eq id nes
then match neb.nexp with
| Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
| _ -> refine_guarantees check_nvar max_lt (Some(c,neb)) id cs (*new min*)
else no_match ()
- | Nuvar _, false, Some(cm, omin) | Nvar _, true, Some(cm, omin) ->
+ | _, Nuvar _, false, _, None | _, Nvar _, true, _, None ->
+ (*let _ = Printf.eprintf "in var, nil case of >\n" in *)
+ if nexp_eq id neb
+ then match nes.nexp with
+ | Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
+ | _ -> refine_guarantees check_nvar (Some(c,nes)) min_gt id cs (*new max*)
+ else no_match ()
+ | Nuvar _, _, false, Some(cm, omin), _ | Nvar _, _, true, Some(cm, omin), _ ->
+ (*let _ = Printf.eprintf "in var case of >\n" in *)
if nexp_eq id nes
then match nexp_lt neb omin with
| Yes -> refine_guarantees check_nvar max_lt (Some(c,neb)) id cs (*replace old min*)
| No -> refine_guarantees check_nvar max_lt min_gt id cs (*remove redundant constraint*)
| Maybe -> no_match ()
else no_match ()
- | _ -> no_match ())
+ | _, Nuvar _, false, _, Some(cm, omax) | _, Nvar _, true, _, Some(cm, omax) ->
+ (*let _ = Printf.eprintf "in var case of >\n" in *)
+ if nexp_eq id neb
+ then match nexp_gt nes omax with
+ | Yes -> refine_guarantees check_nvar (Some(c,nes)) min_gt id cs (*replace old min*)
+ | No -> refine_guarantees check_nvar max_lt min_gt id cs (*remove redundant constraint*)
+ | Maybe -> no_match ()
+ else no_match ()
+ | _ -> no_match ())
| c::cs ->
+ (*let _ = Printf.eprintf "refine_guarantee %s\n" (constraints_to_string [c]) in*)
let (cs,max,min) = refine_guarantees check_nvar max_lt min_gt id cs in
c::cs,max,min
@@ -1634,77 +1707,129 @@ let rec refine_requires check_nvar min_lt max_gt id cs =
let no_match _ =
let (cs,max,min) = refine_requires check_nvar min_lt max_gt id cs in
curr::cs,max,min in
- (match nes.nexp,check_nvar,min_lt with
- | Nuvar _, false, None | Nvar _, true, None ->
+ (match nes.nexp,neb.nexp,check_nvar,min_lt,max_gt with
+ | Nuvar _, _, false, None, _ | Nvar _, _, true, None, _ ->
if nexp_eq id nes
then match neb.nexp with
| Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
| _ -> refine_requires check_nvar (Some(c,neb)) max_gt id cs (*new min*)
else no_match ()
- | Nuvar _, false, Some(cm, omin) | Nvar _, true, Some(cm, omin) ->
+ | _, Nuvar _, false, _, None | _, Nvar _, true, _, None ->
+ if nexp_eq id neb
+ then match nes.nexp with
+ | Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
+ | _ -> refine_requires check_nvar min_lt (Some(c,neb)) id cs (*new max*)
+ else no_match ()
+ | Nuvar _, _, false, Some(cm, omin), _ | Nvar _, _, true, Some(cm, omin), _ ->
if nexp_eq id nes
then match nexp_le neb omin with
| Yes -> refine_requires check_nvar (Some(c,neb)) max_gt id cs (*replace old min*)
| No -> refine_requires check_nvar min_lt max_gt id cs (*remove redundant constraint*)
| Maybe -> no_match ()
else no_match()
+ | _, Nuvar _, false, _, Some(cm, omax) | _, Nvar _, true, _, Some(cm, omax) ->
+ if nexp_eq id neb
+ then match nexp_ge nes omax with
+ | Yes -> refine_requires check_nvar min_lt (Some(c,nes)) id cs (*replace old max*)
+ | No -> refine_requires check_nvar min_lt max_gt id cs (*remove redundant constraint*)
+ | Maybe -> no_match ()
+ else no_match()
| _ -> no_match())
| (Lt(c,Require,nes,neb) as curr)::cs ->
let no_match _ =
let (cs,max,min) = refine_requires check_nvar min_lt max_gt id cs in
curr::cs,max,min in
- (match nes.nexp,check_nvar,min_lt with
- | Nuvar _, false, None | Nvar _, true, None->
+ (match nes.nexp,neb.nexp,check_nvar,min_lt,max_gt with
+ | Nuvar _, _, false, None, _ | Nvar _, _, true, None, _->
if nexp_eq id nes
then match neb.nexp with
| Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
| _ -> refine_requires check_nvar(Some(c,neb)) max_gt id cs (*new min*)
else no_match ()
- | Nuvar _, false, Some(cm, omin) | Nvar _,true, Some(cm, omin) ->
+ | _, Nuvar _, false, _, None | _, Nvar _, true, _, None->
+ if nexp_eq id neb
+ then match nes.nexp with
+ | Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
+ | _ -> refine_requires check_nvar min_lt (Some(c,nes)) id cs (*new max*)
+ else no_match ()
+ | Nuvar _, _, false, Some(cm, omin), _ | Nvar _, _, true, Some(cm, omin), _ ->
if nexp_eq id nes
then match nexp_lt neb omin with
| Yes -> refine_requires check_nvar (Some(c,neb)) max_gt id cs (*replace old min*)
| No -> refine_requires check_nvar min_lt max_gt id cs (*remove redundant constraint*)
| Maybe -> no_match ()
else no_match ()
+ | _, Nuvar _, false, _, Some(cm, omax) | _, Nvar _,true, _, Some(cm, omax) ->
+ if nexp_eq id neb
+ then match nexp_gt nes omax with
+ | Yes -> refine_requires check_nvar min_lt (Some(c,nes)) id cs (*replace old max*)
+ | No -> refine_requires check_nvar min_lt max_gt id cs (*remove redundant constraint*)
+ | Maybe -> no_match ()
+ else no_match ()
| _ -> no_match())
| (GtEq(c,Require,nes,neb) as curr)::cs ->
let no_match _ =
let (cs,max,min) = refine_requires check_nvar min_lt max_gt id cs in
curr::cs,max,min in
- (match nes.nexp,check_nvar,max_gt with
- | Nuvar _, false, None | Nvar _, true, None ->
+ (match nes.nexp,neb.nexp,check_nvar,max_gt,min_lt with
+ | Nuvar _, _, false, None, _ | Nvar _, _, true, None, _ ->
if nexp_eq id nes
then match neb.nexp with
| Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
| _ -> refine_requires check_nvar min_lt (Some(c,neb)) id cs (*new max*)
else no_match ()
- | Nuvar _, false, Some(cm, omax) | Nvar _, true, Some(cm, omax) ->
+ | _, Nuvar _, false, _, None | _, Nvar _, true, _, None ->
+ if nexp_eq id neb
+ then match nes.nexp with
+ | Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
+ | _ -> refine_requires check_nvar (Some(c,nes)) max_gt id cs (*new min*)
+ else no_match ()
+ | Nuvar _, _, false, Some(cm, omax), _ | Nvar _, _, true, Some(cm, omax), _ ->
if nexp_eq id nes
then match nexp_ge neb omax with
| Yes -> refine_requires check_nvar min_lt (Some(c,neb)) id cs (*replace old max*)
| No -> refine_requires check_nvar min_lt max_gt id cs (*remove redundant constraint*)
| Maybe -> no_match ()
else no_match ()
+ | _, Nuvar _, false, _, Some(cm, omin) | _, Nvar _, true, _, Some(cm, omin) ->
+ if nexp_eq id neb
+ then match nexp_le nes omin with
+ | Yes -> refine_requires check_nvar (Some(c,neb)) max_gt id cs (*replace old min*)
+ | No -> refine_requires check_nvar min_lt max_gt id cs (*remove redundant constraint*)
+ | Maybe -> no_match ()
+ else no_match ()
| _ -> no_match ())
| (Gt(c,Require,nes,neb) as curr)::cs ->
let no_match _ =
let (cs,max,min) = refine_requires check_nvar min_lt max_gt id cs in
curr::cs,max,min in
- (match nes.nexp,check_nvar,max_gt with
- | Nuvar _, true, None | Nvar _, false, None->
+ (match nes.nexp,neb.nexp,check_nvar,max_gt,min_lt with
+ | Nuvar _, _, true, None, _ | Nvar _, _, false, None, _ ->
if nexp_eq id nes
then match neb.nexp with
| Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
| _ -> refine_requires check_nvar min_lt (Some(c,neb)) id cs (*new max*)
else refine_requires check_nvar min_lt max_gt id cs
- | Nuvar _, false, Some(cm, omax) | Nvar _, true, Some(cm, omax) ->
+ | _, Nuvar _, true, _, None | _, Nvar _, false, _, None->
+ if nexp_eq id neb
+ then match nes.nexp with
+ | Nuvar _ | Nvar _ -> no_match () (*Don't set a variable to a max/min*)
+ | _ -> refine_requires check_nvar (Some(c,nes)) max_gt id cs (*new min*)
+ else refine_requires check_nvar min_lt max_gt id cs
+ | Nuvar _, _, false, Some(cm, omax), _ | Nvar _, _, true, Some(cm, omax), _ ->
if nexp_eq id nes
then match nexp_gt neb omax with
| Yes -> refine_requires check_nvar min_lt (Some(c,neb)) id cs (*replace old max*)
| No -> refine_requires check_nvar min_lt max_gt id cs (* remove redundant constraint *)
| Maybe -> no_match ()
else no_match ()
+ | _, Nuvar _, false, _, Some(cm, omin) | _, Nvar _, true, _, Some(cm, omin) ->
+ if nexp_eq id neb
+ then match nexp_lt nes omin with
+ | Yes -> refine_requires check_nvar (Some(c,nes)) max_gt id cs (*replace old min*)
+ | No -> refine_requires check_nvar min_lt max_gt id cs (* remove redundant constraint *)
+ | Maybe -> no_match ()
+ else no_match ()
| _ -> no_match())
| c::cs ->
let (cs,min,max) = refine_requires check_nvar min_lt max_gt id cs in
@@ -2770,6 +2895,7 @@ let is_enum_typ d_env t =
| _ -> None
let eq_error l msg = raise (Reporting_basic.err_typ l msg)
+let multi_constraint_error l1 l2 msg = raise (Reporting_basic.err_typ_dual (get_c_loc l1) (get_c_loc l2) msg)
let compare_effect (BE_aux(e1,_)) (BE_aux(e2,_)) =
match e1,e2 with
@@ -3403,13 +3529,13 @@ let rec select_overload_variant d_env params_check get_all variants actual_type
| _ -> recur () )
let rec split_conditional_constraints = function
- | [] -> [],[]
+ | [] -> [],[],[]
| Predicate(co,cp,cn)::cs ->
- let (csp,csn) = split_conditional_constraints cs in
- (cp::csp, cn::csn)
+ let (csa,csp,csn) = split_conditional_constraints cs in
+ (csa,cp::csp, cn::csn)
| c::cs ->
- let (csp,csn) = split_conditional_constraints cs in
- (c::csp, csn)
+ let (csa,csp,csn) = split_conditional_constraints cs in
+ (c::csa,csp, csn)
let rec in_constraint_env = function
| [] -> []
@@ -4018,29 +4144,31 @@ let check_range_consistent require_lt require_gt guarantee_lt guarantee_gt =
| None,None,None,None
| Some _, None, None, None | None, Some _ , None, None | None, None, Some _ , None | None, None, None, Some _
| Some _, Some _,None,None | None,None,Some _,Some _ (*earlier check should ensure these*)
- -> let _ = Printf.eprintf "check_range_consistent in nil case\n" in ()
- | Some(crlt,rlt), Some(crgt,rgt), Some(cglt,glt), Some(cggt,ggt) ->
- let _ = Printf.eprintf "check_range_consistent is in the checking case\n" in
+ -> ()
+ | Some(crlt,rlt), Some(crgt,rgt), Some(cglt,glt), Some(cggt,ggt) -> () (*
if tri_to_bl (nexp_ge rlt glt) (*Can we guarantee the up is less than the required up*)
then if tri_to_bl (nexp_ge rlt ggt) (*Can we guarantee the lw is less than the required up*)
then if tri_to_bl (nexp_ge glt rgt) (*Can we guarantee the up is greater than the required lw*)
then if tri_to_bl (nexp_ge ggt rgt) (*Can we guarantee that the lw is greater than the required lw*)
then ()
- else assert false (*make a good two-location error, all the way down*)
- else assert false
- else assert false
- else assert false
+ else multi_constraint_error cggt crgt ("Constraints arising from these locations requires greater than "
+ ^ (n_to_string rgt) ^ " but best guarantee is " ^ (n_to_string ggt))
+ else multi_constraint_error cglt crgt ("Constraints arising from these locations guarantees a number no greather than " ^ (n_to_string glt) ^ " but requires a number greater than " ^ (n_to_string rgt))
+ else multi_constraint_error crlt cggt ("Constraints arising from these locations guarantees a number that is less than " ^ (n_to_string rlt) ^ " but best guarantee is " ^ (n_to_string ggt))
+ else multi_constraint_error crlt cglt ("Constraints arising from these locations require no more than " ^ (n_to_string rlt) ^ " but guarantee indicates it may be above " ^ (n_to_string glt)) *)
| _ ->
- let _ = Printf.eprintf "check_range_consistent is in the partial case\n" in
- assert false
+ (*let _ = Printf.eprintf "check_range_consistent is in the partial case\n" in*)
+ ()
let check_ranges cs =
- let _ = Printf.eprintf "In check_ranges with %i constraints\n" (constraint_size cs) in
+ (*let _ = Printf.eprintf "In check_ranges with %i constraints\n" (constraint_size cs) in*)
let nuvars = get_all_nuvars_cs cs in
+ (*let _ = Printf.eprintf "Have %i nuvars\n" (List.length (Var_set.elements nuvars)) in*)
let nus_with_cs = List.map (fun n -> (n,contains_nuvar n cs)) (Var_set.elements nuvars) in
let nus_with_iso_cs = List.map (fun (n,ncs) -> (n,isolate_constraint n ncs)) nus_with_cs in
let refined_cs = List.concat (List.map (fun (n,ncs) ->
- let guarantees,max_guarantee_lt,min_guarantee_gt = refine_guarantees false None None n ncs in
+ let guarantees,max_guarantee_lt,min_guarantee_gt =
+ refine_guarantees false None None n (flatten_constraints ncs) in
let require_cs,min_require_lt,max_require_gt = refine_requires false None None n guarantees in
check_range_consistent min_require_lt max_require_gt max_guarantee_lt min_guarantee_gt;
require_cs)
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 6504bed5..a44aa519 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -278,7 +278,8 @@ val get_all_nvar : nexp -> string list (*Pull out all of the contained nvar and
val select_overload_variant : def_envs -> bool -> bool -> tannot list -> t -> tannot list
-val split_conditional_constraints : constraints -> (constraints * constraints)
+(*splits constraints into always, positive, negative constraints; where positive and negative happen for predicates *)
+val split_conditional_constraints : constraints -> (constraints * constraints * constraints)
(*May raise an exception if a contradiction is found*)
val resolve_constraints : constraints -> (constraints * nexp_map option)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 12:25:05 +0000