diff options
| -rw-r--r-- | src/type_internal.ml | 70 | ||||
| -rw-r--r-- | src/type_internal.mli | 1 |
2 files changed, 61 insertions, 10 deletions
diff --git a/src/type_internal.ml b/src/type_internal.ml index 17728dd9..c4f009ac 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -48,6 +48,7 @@ and nexp_aux = | N2n of nexp * big_int option | Npow of nexp * int (* nexp raised to the int *) | 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; } and effect = { mutable effect : effect_aux } @@ -326,7 +327,7 @@ let rec contains_const n = let rec get_var n = match n.nexp with - | Nvar _ | Nuvar _ -> Some n + | Nvar _ | Nuvar _ | N2n _ -> Some n | Nneg n -> get_var n | Nmult (_,n1) -> get_var n1 | _ -> None @@ -341,11 +342,19 @@ let increment_factor n i = match n.nexp with | Nvar _ | Nuvar _ -> (match i.nexp with - | Nconst i -> {nexp = Nmult({nexp = Nconst (add_big_int i one)},n)} + | Nconst i -> + let ni = add_big_int i one in + if eq_big_int ni zero + then {nexp = Nconst zero } + else {nexp = Nmult({nexp = Nconst ni},n)} | _ -> {nexp = Nmult({nexp = Nadd(i,{nexp = Nconst one})},n)}) | Nmult(n1,n2) -> (match n1.nexp,i.nexp with - | Nconst i2,Nconst i -> { nexp = Nmult({nexp = Nconst (add_big_int i i2)},n2)} + | Nconst i2,Nconst i -> + let ni = add_big_int i i2 in + if eq_big_int ni zero + then {nexp = Nconst zero } + else { nexp = Nmult({nexp = Nconst (add_big_int i i2)},n2)} | _ -> { nexp = Nmult({ nexp = Nadd(n1,i)},n2)}) | _ -> assert false @@ -384,7 +393,7 @@ let rec normalize_nexp n = | Nadd(n1,n2) -> let n1',n2' = normalize_nexp n1, normalize_nexp n2 in (match n1'.nexp,n2'.nexp with - | Nneg_inf, Npos_inf | Npos_inf, Nneg_inf -> {nexp = Nconst zero } + | Nneg_inf, Npos_inf | Npos_inf, Nneg_inf -> {nexp = Ninexact } | Npos_inf, _ | _, Npos_inf -> { nexp = Npos_inf } | Nneg_inf, _ | _, Nneg_inf -> { nexp = Nneg_inf } | Nconst i1, Nconst i2 | Nconst i1, N2n(_,Some i2) | N2n(_,Some i2), Nconst i1 -> {nexp = Nconst (add_big_int i1 i2)} @@ -434,7 +443,19 @@ let rec normalize_nexp n = | _ -> {nexp = Nadd (n1',n2')}) | Some(nv1),None -> {nexp = Nadd (n2',n1')} | None,Some(nv2) -> {nexp = Nadd (n1',n2')} - | _ -> let _ = Printf.printf "One term does not have var in %s\n" (n_to_string n) in assert false) + | _ -> (match n1'.nexp,n2'.nexp with + | Nadd(n11',n12'), _ -> + (match compare_nexps n11' n2' with + | -1 -> {nexp = Nadd(n2',n1')} + | 1 -> { nexp = Nadd(n11', normalize_nexp { nexp = Nadd(n12',n2')}) } + | _ -> let _ = Printf.eprintf "Neither term has var but are the same? %s %s\n" (n_to_string n1') (n_to_string n2') in assert false) + | (_, Nadd(n21',n22')) -> + (match compare_nexps n1' n21' with + | -1 -> { nexp = Nadd(n21', normalize_nexp { nexp = Nadd(n1',n22')})} + | 1 -> { nexp = Nadd(n1',n2') } + | _ -> let _ = Printf.eprintf "pattern didn't match unexpextedly here %s %s\n" (n_to_string n1') (n_to_string n2') in assert false) + | _ -> let _ = Printf.eprintf "pattern didn't match here with no vars %s %s\n" (n_to_string n1') (n_to_string n2') in assert false) + ) | Nmult(n1,n2) -> let n1',n2' = normalize_nexp n1, normalize_nexp n2 in (match n1'.nexp,n2'.nexp with @@ -1697,11 +1718,13 @@ let rec simple_constraint_check in_env cs = let n1',n2' = normalize_nexp n1,normalize_nexp n2 in (* let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in *) (match n1'.nexp,n2'.nexp with + | Ninexact,nok | nok,Ninexact -> + eq_error (get_c_loc co) ("Type constraint arising from here requires " ^ n_to_string {nexp = nok} ^ " to be equal to +inf + -inf") | Npos_inf,Npos_inf | Nneg_inf, Nneg_inf -> None | Nconst i1, Nconst i2 | Nconst i1,N2n(_,Some(i2)) | N2n(_,Some(i1)),Nconst(i2) -> if eq_big_int i1 i2 then None - else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires " - ^ string_of_big_int i1 ^ " to equal " ^ string_of_big_int i2) + else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires (" ^ n_to_string n1 ^ "=" + ^ string_of_big_int i1 ^ ") to equal (" ^ n_to_string n2 ^ " = " ^ string_of_big_int i2) | Nconst i, Nuvar u -> if not(u.nin) && ok_to_set then begin equate_n n2' n1'; None end @@ -1714,7 +1737,25 @@ let rec simple_constraint_check in_env cs = if ok_to_set then begin ignore(resolve_nsubst n1); ignore(resolve_nsubst n2); equate_n n1' n2'; None end else Some(Eq(co,n1',n2')) - | _,_ -> Some(Eq(co,n1',n2'))) in + | _,_ -> + if nexp_eq_check n1' n2' + then None + else + let new_n = normalize_nexp (mk_sub n1' n2') in + (match new_n.nexp with + | Nconst i -> + if eq_big_int i zero + then None + else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires " + ^ n_to_string new_n ^ " to equal 0, not " ^ string_of_big_int i) + | Nuvar u1 -> + if ok_to_set + then begin ignore(resolve_nsubst new_n); equate_n new_n {nexp = Nconst zero}; None end + else Some(Eq(co,new_n,{nexp = Nconst zero})) + | Nadd(new_n1,new_n2) -> + (match new_n1.nexp, new_n2.nexp with + | _ -> Some(Eq(co,n1',n2'))) + | _ -> Some(Eq(co,n1',n2')))) in (match contains_in_vars in_env n1, contains_in_vars in_env n2 with | None,None -> (match check_eq true n1 n2 with @@ -1729,12 +1770,21 @@ let rec simple_constraint_check in_env cs = | Nconst i1, Nconst i2 | Nconst i1,N2n(_,Some(i2)) | N2n(_,Some(i1)),Nconst i2 -> if ge_big_int i1 i2 then check cs - else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires " + else eq_error (get_c_loc co) ("Type constraint mismatch: constraint of " ^ n_to_string n1 ^ " >= " ^ n_to_string n2 ^ " arising from here requires " ^ string_of_big_int i1 ^ " to be greater than or equal to " ^ string_of_big_int i2) | Npos_inf, Nconst _ | Npos_inf, Npos_inf | Nconst _, Nneg_inf | Nneg_inf, Nneg_inf -> check cs + | Ninexact, _ | _, Ninexact -> check cs | Nconst _ ,Npos_inf -> eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires " ^ (n_to_string n1') ^ " to be greater than infinity") - | _,_ -> GtEq(co,n1',n2')::(check cs)) + | _,_ -> + let new_n = normalize_nexp (mk_sub n1' n2') in + (match new_n.nexp with + | Nconst i -> + if ge_big_int i zero + then (check cs) + else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires " + ^ n_to_string new_n ^ " to be greater than or equal to 0, not " ^ string_of_big_int i) + | _ -> GtEq(co,n1',n2')::(check cs))) | LtEq(co,n1,n2)::cs -> (* let _ = Printf.printf "<= 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 diff --git a/src/type_internal.mli b/src/type_internal.mli index 2ebc62c7..59fd7d87 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -52,6 +52,7 @@ and nexp_aux = | N2n of nexp * big_int option (* Optionally contains the 2^n result for const n, for different constraint equations *) | Npow of nexp * int (* Does not appear in source *) | Nneg of nexp (* Does not appear in source *) + | Ninexact (*Does not appear in source*) | Nuvar of n_uvar (* Unification variable *) and effect = { mutable effect : effect_aux } and effect_aux = |