From d2f702da3b5cc9934f8cd3ea457f93c6ce2b6c12 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 12 Jun 2019 17:25:47 +0100 Subject: Add AST for greater-than and less-than constraints Mostly to make constraints sent to the SMT solver and Coq nicer, but also makes it easy to remove uninformative constraints in the Coq back-end. --- src/ast_util.ml | 34 ++++++++++++++++++++++++++++++++++ src/constraint.ml | 2 ++ src/initial_check.ml | 4 ++-- src/monomorphise.ml | 4 ++++ src/pretty_print_coq.ml | 16 ++++++++++++++++ src/pretty_print_sail.ml | 2 ++ src/slice.ml | 2 +- src/specialize.ml | 2 ++ src/type_check.ml | 22 ++++++++++++++++++++-- 9 files changed, 83 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index 1f550c73..2bde4ee4 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -335,6 +335,14 @@ let rec constraint_simp (NC_aux (nc_aux, l)) = | _, _ -> NC_bounded_ge (nexp1, nexp2) end + | NC_bounded_gt (nexp1, nexp2) -> + let nexp1, nexp2 = nexp_simp nexp1, nexp_simp nexp2 in + begin match nexp1, nexp2 with + | Nexp_aux (Nexp_constant c1, _), Nexp_aux (Nexp_constant c2, _) -> + if Big_int.greater c1 c2 then NC_true else NC_false + | _, _ -> NC_bounded_gt (nexp1, nexp2) + end + | NC_bounded_le (nexp1, nexp2) -> let nexp1, nexp2 = nexp_simp nexp1, nexp_simp nexp2 in begin match nexp1, nexp2 with @@ -343,6 +351,14 @@ let rec constraint_simp (NC_aux (nc_aux, l)) = | _, _ -> NC_bounded_le (nexp1, nexp2) end + | NC_bounded_lt (nexp1, nexp2) -> + let nexp1, nexp2 = nexp_simp nexp1, nexp_simp nexp2 in + begin match nexp1, nexp2 with + | Nexp_aux (Nexp_constant c1, _), Nexp_aux (Nexp_constant c2, _) -> + if Big_int.less c1 c2 then NC_true else NC_false + | _, _ -> NC_bounded_lt (nexp1, nexp2) + end + | _ -> nc_aux in NC_aux (nc_aux, l) @@ -414,7 +430,9 @@ let nc_int_set kid ints = mk_nc (NC_set (kid, List.map Big_int.of_int ints)) let nc_eq n1 n2 = mk_nc (NC_equal (n1, n2)) let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2)) let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown) +let nc_lt n1 n2 = NC_aux (NC_bounded_lt (n1, n2), Parse_ast.Unknown) let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown) +let nc_gt n1 n2 = NC_aux (NC_bounded_gt (n1, n2), Parse_ast.Unknown) let nc_lt n1 n2 = nc_lteq (nsum n1 (nint 1)) n2 let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nint 1)) let nc_var kid = mk_nc (NC_var kid) @@ -841,7 +859,9 @@ and string_of_n_constraint = function | NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " == " ^ string_of_nexp n2 | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2 | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2 + | NC_aux (NC_bounded_gt (n1, n2), _) -> string_of_nexp n1 ^ " > " ^ string_of_nexp n2 | NC_aux (NC_bounded_le (n1, n2), _) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2 + | NC_aux (NC_bounded_lt (n1, n2), _) -> string_of_nexp n1 ^ " < " ^ string_of_nexp n2 | NC_aux (NC_or (nc1, nc2), _) -> "(" ^ string_of_n_constraint nc1 ^ " | " ^ string_of_n_constraint nc2 ^ ")" | NC_aux (NC_and (nc1, nc2), _) -> @@ -1113,7 +1133,9 @@ let rec nc_compare (NC_aux (nc1,_)) (NC_aux (nc2,_)) = match nc1, nc2 with | NC_equal (n1,n2), NC_equal (n3,n4) | NC_bounded_ge (n1,n2), NC_bounded_ge (n3,n4) + | NC_bounded_gt (n1,n2), NC_bounded_gt (n3,n4) | NC_bounded_le (n1,n2), NC_bounded_le (n3,n4) + | NC_bounded_lt (n1,n2), NC_bounded_lt (n3,n4) | NC_not_equal (n1,n2), NC_not_equal (n3,n4) -> lex_ord Nexp.compare Nexp.compare n1 n3 n2 n4 | NC_set (k1,s1), NC_set (k2,s2) -> @@ -1130,7 +1152,9 @@ let rec nc_compare (NC_aux (nc1,_)) (NC_aux (nc2,_)) = -> 0 | NC_equal _, _ -> -1 | _, NC_equal _ -> 1 | NC_bounded_ge _, _ -> -1 | _, NC_bounded_ge _ -> 1 + | NC_bounded_gt _, _ -> -1 | _, NC_bounded_gt _ -> 1 | NC_bounded_le _, _ -> -1 | _, NC_bounded_le _ -> 1 + | NC_bounded_lt _, _ -> -1 | _, NC_bounded_lt _ -> 1 | NC_not_equal _, _ -> -1 | _, NC_not_equal _ -> 1 | NC_set _, _ -> -1 | _, NC_set _ -> 1 | NC_or _, _ -> -1 | _, NC_or _ -> 1 @@ -1336,7 +1360,9 @@ let rec kopts_of_constraint (NC_aux (nc, _)) = match nc with | NC_equal (nexp1, nexp2) | NC_bounded_ge (nexp1, nexp2) + | NC_bounded_gt (nexp1, nexp2) | NC_bounded_le (nexp1, nexp2) + | NC_bounded_lt (nexp1, nexp2) | NC_not_equal (nexp1, nexp2) -> KOptSet.union (kopts_of_nexp nexp1) (kopts_of_nexp nexp2) | NC_set (kid, _) -> KOptSet.singleton (mk_kopt K_int kid) @@ -1393,7 +1419,9 @@ let rec tyvars_of_constraint (NC_aux (nc, _)) = match nc with | NC_equal (nexp1, nexp2) | NC_bounded_ge (nexp1, nexp2) + | NC_bounded_gt (nexp1, nexp2) | NC_bounded_le (nexp1, nexp2) + | NC_bounded_lt (nexp1, nexp2) | NC_not_equal (nexp1, nexp2) -> KidSet.union (tyvars_of_nexp nexp1) (tyvars_of_nexp nexp2) | NC_set (kid, _) -> KidSet.singleton kid @@ -1679,7 +1707,9 @@ let rec locate_nc f (NC_aux (nc_aux, l)) = let nc_aux = match nc_aux with | NC_equal (nexp1, nexp2) -> NC_equal (locate_nexp f nexp1, locate_nexp f nexp2) | NC_bounded_ge (nexp1, nexp2) -> NC_bounded_ge (locate_nexp f nexp1, locate_nexp f nexp2) + | NC_bounded_gt (nexp1, nexp2) -> NC_bounded_gt (locate_nexp f nexp1, locate_nexp f nexp2) | NC_bounded_le (nexp1, nexp2) -> NC_bounded_le (locate_nexp f nexp1, locate_nexp f nexp2) + | NC_bounded_lt (nexp1, nexp2) -> NC_bounded_lt (locate_nexp f nexp1, locate_nexp f nexp2) | NC_not_equal (nexp1, nexp2) -> NC_not_equal (locate_nexp f nexp1, locate_nexp f nexp2) | NC_set (kid, nums) -> NC_set (locate_kid f kid, nums) | NC_or (nc1, nc2) -> NC_or (locate_nc f nc1, locate_nc f nc2) @@ -1886,7 +1916,9 @@ let rec constraint_subst sv subst (NC_aux (nc, l)) = NC_aux (constraint_subst_au and constraint_subst_aux l sv subst = function | NC_equal (n1, n2) -> NC_equal (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_bounded_ge (n1, n2) -> NC_bounded_ge (nexp_subst sv subst n1, nexp_subst sv subst n2) + | NC_bounded_gt (n1, n2) -> NC_bounded_gt (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2) + | NC_bounded_lt (n1, n2) -> NC_bounded_lt (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_not_equal (n1, n2) -> NC_not_equal (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_set (kid, ints) as set_nc -> begin match subst with @@ -1987,7 +2019,9 @@ let subst_kids_nc, subst_kids_typ, subst_kids_typ_arg = match nc with | NC_equal (n1,n2) -> re (NC_equal (snexp n1, snexp n2)) | NC_bounded_ge (n1,n2) -> re (NC_bounded_ge (snexp n1, snexp n2)) + | NC_bounded_gt (n1,n2) -> re (NC_bounded_gt (snexp n1, snexp n2)) | NC_bounded_le (n1,n2) -> re (NC_bounded_le (snexp n1, snexp n2)) + | NC_bounded_lt (n1,n2) -> re (NC_bounded_lt (snexp n1, snexp n2)) | NC_not_equal (n1,n2) -> re (NC_not_equal (snexp n1, snexp n2)) | NC_set (kid,is) -> begin diff --git a/src/constraint.ml b/src/constraint.ml index 1a4129ff..6c34bc9b 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -192,7 +192,9 @@ let to_smt l vars constr = match aux with | NC_equal (nexp1, nexp2) -> sfun "=" [smt_nexp nexp1; smt_nexp nexp2] | NC_bounded_le (nexp1, nexp2) -> sfun "<=" [smt_nexp nexp1; smt_nexp nexp2] + | NC_bounded_lt (nexp1, nexp2) -> sfun "<" [smt_nexp nexp1; smt_nexp nexp2] | NC_bounded_ge (nexp1, nexp2) -> sfun ">=" [smt_nexp nexp1; smt_nexp nexp2] + | NC_bounded_gt (nexp1, nexp2) -> sfun ">" [smt_nexp nexp1; smt_nexp nexp2] | NC_not_equal (nexp1, nexp2) -> sfun "not" [sfun "=" [smt_nexp nexp1; smt_nexp nexp2]] | NC_set (v, ints) -> sfun "or" (List.map (fun i -> sfun "=" [smt_var v; Atom (Big_int.to_string i)]) ints) diff --git a/src/initial_check.ml b/src/initial_check.ml index 8a61134c..903941e3 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -238,8 +238,8 @@ and to_ast_constraint ctx (P.ATyp_aux (aux, l) as atyp) = | "!=" -> NC_not_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2) | ">=" -> NC_bounded_ge (to_ast_nexp ctx t1, to_ast_nexp ctx t2) | "<=" -> NC_bounded_le (to_ast_nexp ctx t1, to_ast_nexp ctx t2) - | ">" -> NC_bounded_ge (to_ast_nexp ctx t1, nsum (to_ast_nexp ctx t2) (nint 1)) - | "<" -> NC_bounded_le (nsum (to_ast_nexp ctx t1) (nint 1), to_ast_nexp ctx t2) + | ">" -> NC_bounded_gt (to_ast_nexp ctx t1, to_ast_nexp ctx t2) + | "<" -> NC_bounded_lt (to_ast_nexp ctx t1, to_ast_nexp ctx t2) | "&" -> NC_and (to_ast_constraint ctx t1, to_ast_constraint ctx t2) | "|" -> NC_or (to_ast_constraint ctx t1, to_ast_constraint ctx t2) | _ -> diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 8670139f..8374fb3e 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -1866,7 +1866,9 @@ let rec deps_of_nc kid_deps (NC_aux (nc,l)) = match nc with | NC_equal (nexp1,nexp2) | NC_bounded_ge (nexp1,nexp2) + | NC_bounded_gt (nexp1,nexp2) | NC_bounded_le (nexp1,nexp2) + | NC_bounded_lt (nexp1,nexp2) | NC_not_equal (nexp1,nexp2) -> dmerge (deps_of_nexp l kid_deps [] nexp1) (deps_of_nexp l kid_deps [] nexp2) | NC_set (kid,_) -> @@ -3604,7 +3606,9 @@ let rewrite_toplevel_nexps (Defs defs) = match nc with | NC_equal (n1, n2) -> rewrap (NC_equal (aux_nexp n1, aux_nexp n2)) | NC_bounded_ge (n1, n2) -> rewrap (NC_bounded_ge (aux_nexp n1, aux_nexp n2)) + | NC_bounded_gt (n1, n2) -> rewrap (NC_bounded_gt (aux_nexp n1, aux_nexp n2)) | NC_bounded_le (n1, n2) -> rewrap (NC_bounded_le (aux_nexp n1, aux_nexp n2)) + | NC_bounded_lt (n1, n2) -> rewrap (NC_bounded_lt (aux_nexp n1, aux_nexp n2)) | NC_not_equal (n1, n2) -> rewrap (NC_not_equal (aux_nexp n1, aux_nexp n2)) | NC_or (nc1, nc2) -> rewrap (NC_or (aux_nconstraint nc1, aux_nconstraint nc2)) | NC_and (nc1, nc2) -> rewrap (NC_and (aux_nconstraint nc1, aux_nconstraint nc2)) diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 9dcbe2db..d72e7573 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -303,7 +303,9 @@ let rec orig_nc (NC_aux (nc, l) as full_nc) = match nc with | NC_equal (nexp1, nexp2) -> rewrap (NC_equal (orig_nexp nexp1, orig_nexp nexp2)) | NC_bounded_ge (nexp1, nexp2) -> rewrap (NC_bounded_ge (orig_nexp nexp1, orig_nexp nexp2)) + | NC_bounded_gt (nexp1, nexp2) -> rewrap (NC_bounded_gt (orig_nexp nexp1, orig_nexp nexp2)) | NC_bounded_le (nexp1, nexp2) -> rewrap (NC_bounded_le (orig_nexp nexp1, orig_nexp nexp2)) + | NC_bounded_lt (nexp1, nexp2) -> rewrap (NC_bounded_lt (orig_nexp nexp1, orig_nexp nexp2)) | NC_not_equal (nexp1, nexp2) -> rewrap (NC_not_equal (orig_nexp nexp1, orig_nexp nexp2)) | NC_set (kid,s) -> rewrap (NC_set (orig_kid kid, s)) | NC_or (nc1, nc2) -> rewrap (NC_or (orig_nc nc1, orig_nc nc2)) @@ -431,7 +433,9 @@ let rec count_nc_vars (NC_aux (nc,_)) = -> KBindings.singleton kid 1 | NC_equal (n1,n2) | NC_bounded_ge (n1,n2) + | NC_bounded_gt (n1,n2) | NC_bounded_le (n1,n2) + | NC_bounded_lt (n1,n2) | NC_not_equal (n1,n2) -> merge_kid_count (count_nexp_vars n1) (count_nexp_vars n2) | NC_true | NC_false @@ -462,8 +466,12 @@ let simplify_atom_bool l kopts nc atom_nc = | NC_equal (_, Nexp_aux (Nexp_var kid,_)) when KBindings.mem kid lin_ty_vars -> Some kid | NC_bounded_ge (Nexp_aux (Nexp_var kid,_), _) when KBindings.mem kid lin_ty_vars -> Some kid | NC_bounded_ge (_, Nexp_aux (Nexp_var kid,_)) when KBindings.mem kid lin_ty_vars -> Some kid + | NC_bounded_gt (Nexp_aux (Nexp_var kid,_), _) when KBindings.mem kid lin_ty_vars -> Some kid + | NC_bounded_gt (_, Nexp_aux (Nexp_var kid,_)) when KBindings.mem kid lin_ty_vars -> Some kid | NC_bounded_le (Nexp_aux (Nexp_var kid,_), _) when KBindings.mem kid lin_ty_vars -> Some kid | NC_bounded_le (_, Nexp_aux (Nexp_var kid,_)) when KBindings.mem kid lin_ty_vars -> Some kid + | NC_bounded_lt (Nexp_aux (Nexp_var kid,_), _) when KBindings.mem kid lin_ty_vars -> Some kid + | NC_bounded_lt (_, Nexp_aux (Nexp_var kid,_)) when KBindings.mem kid lin_ty_vars -> Some kid | NC_not_equal (Nexp_aux (Nexp_var kid,_), _) when KBindings.mem kid lin_ty_vars -> Some kid | NC_not_equal (_, Nexp_aux (Nexp_var kid,_)) when KBindings.mem kid lin_ty_vars -> Some kid | NC_set (kid, _::_) when KBindings.mem kid lin_ty_vars -> Some kid @@ -769,7 +777,9 @@ and doc_nc_prop ?(top = true) ctx env nc = | NC_equal (ne1, ne2) -> doc_op equals (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_var kid -> doc_op equals (doc_nexp ctx (nvar kid)) (string "true") | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=") (doc_nexp ctx ne1) (doc_nexp ctx ne2) + | NC_bounded_gt (ne1, ne2) -> doc_op (string ">") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_bounded_le (ne1, ne2) -> doc_op (string "<=") (doc_nexp ctx ne1) (doc_nexp ctx ne2) + | NC_bounded_lt (ne1, ne2) -> doc_op (string "<") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_not_equal (ne1, ne2) -> doc_op (string "<>") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | _ -> l10 nc_full and l10 (NC_aux (nc,_) as nc_full) = @@ -791,7 +801,9 @@ and doc_nc_prop ?(top = true) ctx env nc = | NC_and _ | NC_equal _ | NC_bounded_ge _ + | NC_bounded_gt _ | NC_bounded_le _ + | NC_bounded_lt _ | NC_not_equal _ -> parens (l85 nc_full) in if top then newnc l85 nc else newnc l0 nc @@ -820,7 +832,9 @@ let rec doc_nc_exp ctx env nc = match nc with | NC_equal (ne1, ne2) -> doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) + | NC_bounded_gt (ne1, ne2) -> doc_op (string ">?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_bounded_le (ne1, ne2) -> doc_op (string "<=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) + | NC_bounded_lt (ne1, ne2) -> doc_op (string " l50 nc_full and l50 (NC_aux (nc,_) as nc_full) = match nc with @@ -843,7 +857,9 @@ let rec doc_nc_exp ctx env nc = | NC_var kid -> doc_nexp ctx (nvar kid) | NC_equal _ | NC_bounded_ge _ + | NC_bounded_gt _ | NC_bounded_le _ + | NC_bounded_lt _ | NC_or _ | NC_and _ -> parens (l70 nc_full) in newnc l70 nc diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index a0ac73a6..5dbb6cd5 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -136,7 +136,9 @@ let rec doc_nc nc = | NC_equal (n1, n2) -> nc_op "==" n1 n2 | NC_not_equal (n1, n2) -> nc_op "!=" n1 n2 | NC_bounded_ge (n1, n2) -> nc_op ">=" n1 n2 + | NC_bounded_gt (n1, n2) -> nc_op ">" n1 n2 | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2 + | NC_bounded_lt (n1, n2) -> nc_op "<" n1 n2 | NC_set (kid, ints) -> separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)] | NC_app (id, args) -> diff --git a/src/slice.ml b/src/slice.ml index 9dee4761..1bbbca1e 100644 --- a/src/slice.ml +++ b/src/slice.ml @@ -104,7 +104,7 @@ let builtins = let rec constraint_ids' (NC_aux (aux, _)) = match aux with - | NC_equal (n1, n2) | NC_bounded_le (n1, n2) | NC_bounded_ge (n1, n2) | NC_not_equal (n1, n2) -> + | NC_equal (n1, n2) | NC_bounded_le (n1, n2) | NC_bounded_ge (n1, n2) | NC_bounded_lt (n1, n2) | NC_bounded_gt (n1, n2) | NC_not_equal (n1, n2) -> IdSet.union (nexp_ids' n1) (nexp_ids' n2) | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> IdSet.union (constraint_ids' nc1) (constraint_ids' nc2) diff --git a/src/specialize.ml b/src/specialize.ml index 815514d1..d749bc53 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -186,7 +186,9 @@ let string_of_instantiation instantiation = | NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2 | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2 | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2 + | NC_aux (NC_bounded_gt (n1, n2), _) -> string_of_nexp n1 ^ " > " ^ string_of_nexp n2 | NC_aux (NC_bounded_le (n1, n2), _) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2 + | NC_aux (NC_bounded_lt (n1, n2), _) -> string_of_nexp n1 ^ " < " ^ string_of_nexp n2 | NC_aux (NC_or (nc1, nc2), _) -> "(" ^ string_of_n_constraint nc1 ^ " | " ^ string_of_n_constraint nc2 ^ ")" | NC_aux (NC_and (nc1, nc2), _) -> diff --git a/src/type_check.ml b/src/type_check.ml index 02e32f4d..e5141bcb 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -202,7 +202,9 @@ and strip_nexp = function and strip_n_constraint_aux = function | NC_equal (nexp1, nexp2) -> NC_equal (strip_nexp nexp1, strip_nexp nexp2) | NC_bounded_ge (nexp1, nexp2) -> NC_bounded_ge (strip_nexp nexp1, strip_nexp nexp2) + | NC_bounded_gt (nexp1, nexp2) -> NC_bounded_gt (strip_nexp nexp1, strip_nexp nexp2) | NC_bounded_le (nexp1, nexp2) -> NC_bounded_le (strip_nexp nexp1, strip_nexp nexp2) + | NC_bounded_lt (nexp1, nexp2) -> NC_bounded_lt (strip_nexp nexp1, strip_nexp nexp2) | NC_not_equal (nexp1, nexp2) -> NC_not_equal (strip_nexp nexp1, strip_nexp nexp2) | NC_set (kid, nums) -> NC_set (strip_kid kid, nums) | NC_or (nc1, nc2) -> NC_or (strip_n_constraint nc1, strip_n_constraint nc2) @@ -294,7 +296,7 @@ and typ_arg_nexps (A_aux (typ_arg_aux, l)) = | A_order ord -> [] and constraint_nexps (NC_aux (nc_aux, l)) = match nc_aux with - | NC_equal (n1, n2) | NC_bounded_ge (n1, n2) | NC_bounded_le (n1, n2) | NC_not_equal (n1, n2) -> + | NC_equal (n1, n2) | NC_bounded_ge (n1, n2) | NC_bounded_le (n1, n2) | NC_bounded_gt (n1, n2) | NC_bounded_lt (n1, n2) | NC_not_equal (n1, n2) -> [n1; n2] | NC_set _ | NC_true | NC_false | NC_var _ -> [] | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> constraint_nexps nc1 @ constraint_nexps nc2 @@ -668,7 +670,9 @@ end = struct | NC_equal (n1, n2) -> NC_aux (NC_equal (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) | NC_not_equal (n1, n2) -> NC_aux (NC_not_equal (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) | NC_bounded_le (n1, n2) -> NC_aux (NC_bounded_le (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) + | NC_bounded_lt (n1, n2) -> NC_aux (NC_bounded_lt (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) | NC_bounded_ge (n1, n2) -> NC_aux (NC_bounded_ge (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) + | NC_bounded_gt (n1, n2) -> NC_aux (NC_bounded_gt (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) | NC_app (id, args) -> (try begin match get_typ_synonym id env l env args with @@ -862,7 +866,9 @@ end = struct | NC_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 | NC_not_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 | NC_bounded_ge (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 + | NC_bounded_gt (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 | NC_bounded_le (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 + | NC_bounded_lt (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 | NC_set (kid, _) when KidSet.mem kid exs -> () | NC_set (kid, _) -> begin match get_typ_var kid env with @@ -1567,7 +1573,9 @@ let rec nc_identical (NC_aux (nc1, _)) (NC_aux (nc2, _)) = | NC_equal (n1a, n1b), NC_equal (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b | NC_not_equal (n1a, n1b), NC_not_equal (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b | NC_bounded_ge (n1a, n1b), NC_bounded_ge (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b + | NC_bounded_gt (n1a, n1b), NC_bounded_gt (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b | NC_bounded_le (n1a, n1b), NC_bounded_le (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b + | NC_bounded_lt (n1a, n1b), NC_bounded_lt (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b | NC_or (nc1a, nc1b), NC_or (nc2a, nc2b) -> nc_identical nc1a nc2a && nc_identical nc1b nc2b | NC_and (nc1a, nc1b), NC_and (nc2a, nc2b) -> nc_identical nc1a nc2a && nc_identical nc1b nc2b | NC_true, NC_true -> true @@ -1706,8 +1714,12 @@ and unify_constraint l env goals (NC_aux (aux1, _) as nc1) (NC_aux (aux2, _) as merge_uvars l (unify_nexp l env goals n1a n1b) (unify_nexp l env goals n2a n2b) | NC_bounded_ge (n1a, n2a), NC_bounded_ge (n1b, n2b) -> merge_uvars l (unify_nexp l env goals n1a n1b) (unify_nexp l env goals n2a n2b) + | NC_bounded_gt (n1a, n2a), NC_bounded_gt (n1b, n2b) -> + merge_uvars l (unify_nexp l env goals n1a n1b) (unify_nexp l env goals n2a n2b) | NC_bounded_le (n1a, n2a), NC_bounded_le (n1b, n2b) -> merge_uvars l (unify_nexp l env goals n1a n1b) (unify_nexp l env goals n2a n2b) + | NC_bounded_lt (n1a, n2a), NC_bounded_lt (n1b, n2b) -> + merge_uvars l (unify_nexp l env goals n1a n1b) (unify_nexp l env goals n2a n2b) | NC_true, NC_true -> KBindings.empty | NC_false, NC_false -> KBindings.empty | _, _ -> unify_error l ("Could not unify constraints " ^ string_of_n_constraint nc1 ^ " and " ^ string_of_n_constraint nc2) @@ -1878,7 +1890,9 @@ and ambiguous_nc_vars (NC_aux (aux, _)) = match aux with | NC_and (nc1, nc2) -> KidSet.union (tyvars_of_constraint nc1) (tyvars_of_constraint nc2) | NC_bounded_le (n1, n2) -> KidSet.union (tyvars_of_nexp n1) (tyvars_of_nexp n2) + | NC_bounded_lt (n1, n2) -> KidSet.union (tyvars_of_nexp n1) (tyvars_of_nexp n2) | NC_bounded_ge (n1, n2) -> KidSet.union (tyvars_of_nexp n1) (tyvars_of_nexp n2) + | NC_bounded_gt (n1, n2) -> KidSet.union (tyvars_of_nexp n1) (tyvars_of_nexp n2) | NC_equal (n1, n2) | NC_not_equal (n1, n2) -> KidSet.union (ambiguous_nexp_vars n1) (ambiguous_nexp_vars n2) | _ -> KidSet.empty @@ -1962,7 +1976,9 @@ and kid_order_constraint kind_map (NC_aux (aux, l) as nc) = ([mk_kopt (unaux_kind (KBindings.find kid kind_map)) kid], KBindings.remove kid kind_map) | NC_var _ | NC_set _ -> ([], kind_map) | NC_true | NC_false -> ([], kind_map) - | NC_equal (n1, n2) | NC_not_equal (n1, n2) | NC_bounded_le (n1, n2) | NC_bounded_ge (n1, n2) -> + | NC_equal (n1, n2) | NC_not_equal (n1, n2) + | NC_bounded_le (n1, n2) | NC_bounded_ge (n1, n2) + | NC_bounded_lt (n1, n2) | NC_bounded_gt (n1, n2) -> let ord1, kind_map = kid_order_nexp kind_map n1 in let ord2, kind_map = kid_order_nexp kind_map n2 in (ord1 @ ord2, kind_map) @@ -2251,7 +2267,9 @@ and rewrite_nc_aux l env = let mk_exp exp = mk_exp ~loc:l exp in function | NC_bounded_ge (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id ">=", mk_exp (E_sizeof n2)) + | NC_bounded_gt (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id ">", mk_exp (E_sizeof n2)) | NC_bounded_le (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "<=", mk_exp (E_sizeof n2)) + | NC_bounded_lt (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "<", mk_exp (E_sizeof n2)) | NC_equal (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "==", mk_exp (E_sizeof n2)) | NC_not_equal (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "!=", mk_exp (E_sizeof n2)) | NC_and (nc1, nc2) -> E_app_infix (rewrite_nc env nc1, mk_id "&", rewrite_nc env nc2) -- cgit v1.2.3