diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 529 | ||||
| -rw-r--r-- | plugins/micromega/micromega.ml | 623 | ||||
| -rw-r--r-- | plugins/micromega/micromega.mli | 293 | ||||
| -rw-r--r-- | plugins/micromega/zify.ml | 59 |
4 files changed, 1081 insertions, 423 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 0f8d941b41..44bc20e55f 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -86,20 +86,30 @@ type 'cst formula = type 'cst clause = ('cst Mc.nFormula, tag * EConstr.constr) Mc.clause type 'cst cnf = ('cst Mc.nFormula, tag * EConstr.constr) Mc.cnf +let pp_kind o = function + | Mc.IsProp -> output_string o "Prop" + | Mc.IsBool -> output_string o "bool" + +let kind_is_prop = function Mc.IsProp -> true | Mc.IsBool -> false + let rec pp_formula o (f : 'cst formula) = Mc.( match f with - | TT -> output_string o "tt" - | FF -> output_string o "ff" - | X c -> output_string o "X " - | A (_, (t, _)) -> Printf.fprintf o "A(%a)" Tag.pp t - | Cj (f1, f2) -> Printf.fprintf o "C(%a,%a)" pp_formula f1 pp_formula f2 - | D (f1, f2) -> Printf.fprintf o "D(%a,%a)" pp_formula f1 pp_formula f2 - | I (f1, n, f2) -> - Printf.fprintf o "I(%a,%s,%a)" pp_formula f1 + | TT k -> output_string o (if kind_is_prop k then "True" else "true") + | FF k -> output_string o (if kind_is_prop k then "False" else "false") + | X (k, c) -> Printf.fprintf o "X %a" pp_kind k + | A (_, _, (t, _)) -> Printf.fprintf o "A(%a)" Tag.pp t + | AND (_, f1, f2) -> + Printf.fprintf o "AND(%a,%a)" pp_formula f1 pp_formula f2 + | OR (_, f1, f2) -> Printf.fprintf o "OR(%a,%a)" pp_formula f1 pp_formula f2 + | IMPL (_, f1, n, f2) -> + Printf.fprintf o "IMPL(%a,%s,%a)" pp_formula f1 (match n with Some id -> Names.Id.to_string id | None -> "") pp_formula f2 - | N f -> Printf.fprintf o "N(%a)" pp_formula f) + | NOT (_, f) -> Printf.fprintf o "NOT(%a)" pp_formula f + | IFF (_, f1, f2) -> + Printf.fprintf o "IFF(%a,%a)" pp_formula f1 pp_formula f2 + | EQ (f1, f2) -> Printf.fprintf o "EQ(%a,%a)" pp_formula f1 pp_formula f2) (** * Given a set of integers s=\{i0,...,iN\} and a list m, return the list of @@ -142,6 +152,14 @@ module M = struct let coq_iff = lazy (constr_of_ref "core.iff.type") let coq_True = lazy (constr_of_ref "core.True.type") let coq_False = lazy (constr_of_ref "core.False.type") + let coq_bool = lazy (constr_of_ref "core.bool.type") + let coq_true = lazy (constr_of_ref "core.bool.true") + let coq_false = lazy (constr_of_ref "core.bool.false") + let coq_andb = lazy (constr_of_ref "core.bool.andb") + let coq_orb = lazy (constr_of_ref "core.bool.orb") + let coq_implb = lazy (constr_of_ref "core.bool.implb") + let coq_eqb = lazy (constr_of_ref "core.bool.eqb") + let coq_negb = lazy (constr_of_ref "core.bool.negb") let coq_cons = lazy (constr_of_ref "core.list.cons") let coq_nil = lazy (constr_of_ref "core.list.nil") let coq_list = lazy (constr_of_ref "core.list.type") @@ -186,11 +204,18 @@ module M = struct let coq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof") let coq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof") let coq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof") + let coq_IsProp = lazy (constr_of_ref "micromega.kind.isProp") + let coq_IsBool = lazy (constr_of_ref "micromega.kind.isBool") let coq_Zgt = lazy (constr_of_ref "num.Z.gt") let coq_Zge = lazy (constr_of_ref "num.Z.ge") let coq_Zle = lazy (constr_of_ref "num.Z.le") let coq_Zlt = lazy (constr_of_ref "num.Z.lt") - let coq_Eq = lazy (constr_of_ref "core.eq.type") + let coq_Zgtb = lazy (constr_of_ref "num.Z.gtb") + let coq_Zgeb = lazy (constr_of_ref "num.Z.geb") + let coq_Zleb = lazy (constr_of_ref "num.Z.leb") + let coq_Zltb = lazy (constr_of_ref "num.Z.ltb") + let coq_Zeqb = lazy (constr_of_ref "num.Z.eqb") + let coq_eq = lazy (constr_of_ref "core.eq.type") let coq_Zplus = lazy (constr_of_ref "num.Z.add") let coq_Zminus = lazy (constr_of_ref "num.Z.sub") let coq_Zopp = lazy (constr_of_ref "num.Z.opp") @@ -248,13 +273,16 @@ module M = struct let coq_TT = lazy (constr_of_ref "micromega.GFormula.TT") let coq_FF = lazy (constr_of_ref "micromega.GFormula.FF") - let coq_And = lazy (constr_of_ref "micromega.GFormula.Cj") - let coq_Or = lazy (constr_of_ref "micromega.GFormula.D") - let coq_Neg = lazy (constr_of_ref "micromega.GFormula.N") + let coq_AND = lazy (constr_of_ref "micromega.GFormula.AND") + let coq_OR = lazy (constr_of_ref "micromega.GFormula.OR") + let coq_NOT = lazy (constr_of_ref "micromega.GFormula.NOT") let coq_Atom = lazy (constr_of_ref "micromega.GFormula.A") let coq_X = lazy (constr_of_ref "micromega.GFormula.X") - let coq_Impl = lazy (constr_of_ref "micromega.GFormula.I") + let coq_IMPL = lazy (constr_of_ref "micromega.GFormula.IMPL") + let coq_IFF = lazy (constr_of_ref "micromega.GFormula.IFF") + let coq_EQ = lazy (constr_of_ref "micromega.GFormula.EQ") let coq_Formula = lazy (constr_of_ref "micromega.BFormula.type") + let coq_eKind = lazy (constr_of_ref "micromega.eKind") (** * Initialization : a few Caml symbols are derived from other libraries; @@ -557,52 +585,56 @@ module M = struct (List.find (fun (x', y) -> EConstr.eq_constr sigma x (Lazy.force x')) l) with Not_found -> raise ParseError - let zop_table = + let zop_table_prop = [ (coq_Zgt, Mc.OpGt) ; (coq_Zge, Mc.OpGe) ; (coq_Zlt, Mc.OpLt) ; (coq_Zle, Mc.OpLe) ] - let rop_table = + let zop_table_bool = + [ (coq_Zgtb, Mc.OpGt) + ; (coq_Zgeb, Mc.OpGe) + ; (coq_Zltb, Mc.OpLt) + ; (coq_Zleb, Mc.OpLe) + ; (coq_Zeqb, Mc.OpEq) ] + + let rop_table_prop = [ (coq_Rgt, Mc.OpGt) ; (coq_Rge, Mc.OpGe) ; (coq_Rlt, Mc.OpLt) ; (coq_Rle, Mc.OpLe) ] - let qop_table = [(coq_Qlt, Mc.OpLt); (coq_Qle, Mc.OpLe); (coq_Qeq, Mc.OpEq)] + let rop_table_bool = [] + + let qop_table_prop = + [(coq_Qlt, Mc.OpLt); (coq_Qle, Mc.OpLe); (coq_Qeq, Mc.OpEq)] + + let qop_table_bool = [] type gl = {env : Environ.env; sigma : Evd.evar_map} let is_convertible gl t1 t2 = Reductionops.is_conv gl.env gl.sigma t1 t2 - let parse_zop gl (op, args) = + let parse_operator table_prop table_bool has_equality typ gl k (op, args) = let sigma = gl.sigma in match args with - | [|a1; a2|] -> (assoc_const sigma op zop_table, a1, a2) + | [|a1; a2|] -> + ( assoc_const sigma op + (match k with Mc.IsProp -> table_prop | Mc.IsBool -> table_bool) + , a1 + , a2 ) | [|ty; a1; a2|] -> if - EConstr.eq_constr sigma op (Lazy.force coq_Eq) - && is_convertible gl ty (Lazy.force coq_Z) + has_equality + && EConstr.eq_constr sigma op (Lazy.force coq_eq) + && is_convertible gl ty (Lazy.force typ) then (Mc.OpEq, args.(1), args.(2)) else raise ParseError | _ -> raise ParseError - let parse_rop gl (op, args) = - let sigma = gl.sigma in - match args with - | [|a1; a2|] -> (assoc_const sigma op rop_table, a1, a2) - | [|ty; a1; a2|] -> - if - EConstr.eq_constr sigma op (Lazy.force coq_Eq) - && is_convertible gl ty (Lazy.force coq_R) - then (Mc.OpEq, a1, a2) - else raise ParseError - | _ -> raise ParseError - - let parse_qop gl (op, args) = - if Array.length args = 2 then - (assoc_const gl.sigma op qop_table, args.(0), args.(1)) - else raise ParseError + let parse_zop = parse_operator zop_table_prop zop_table_bool true coq_Z + let parse_rop = parse_operator rop_table_prop [] true coq_R + let parse_qop = parse_operator qop_table_prop [] false coq_R type 'a op = | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr) @@ -622,7 +654,7 @@ module M = struct module Env = struct type t = - { vars : EConstr.t list + { vars : (EConstr.t * Mc.kind) list ; (* The list represents a mapping from EConstr.t to indexes. *) gl : gl (* The evar_map may be updated due to unification of universes *) } @@ -642,16 +674,16 @@ module M = struct | exception Univ.UniverseInconsistency _ -> None ) | None -> None - let compute_rank_add env v = + let compute_rank_add env v is_prop = let rec _add gl vars n v = match vars with - | [] -> (gl, [v], n) - | e :: l -> ( + | [] -> (gl, [(v, is_prop)], n) + | (e, b) :: l -> ( match eq_constr gl e v with | Some gl' -> (gl', vars, n) | None -> let gl, l', n = _add gl l (n + 1) v in - (gl, e :: l', n) ) + (gl, (e, b) :: l', n) ) in let gl', vars', n = _add env.gl env.vars 1 v in ({vars = vars'; gl = gl'}, CamlToCoq.positive n) @@ -661,7 +693,7 @@ module M = struct let rec _get_rank env n = match env with | [] -> raise (Invalid_argument "get_rank") - | e :: l -> ( + | (e, _) :: l -> ( match eq_constr gl e v with Some _ -> n | None -> _get_rank l (n + 1) ) in @@ -682,7 +714,7 @@ module M = struct let pp gl env = let ppl = List.mapi - (fun i e -> + (fun i (e, _) -> Pp.str "x" ++ Pp.int (i + 1) ++ Pp.str ":" @@ -703,7 +735,7 @@ module M = struct Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env gl.env gl.sigma term); let parse_variable env term = - let env, n = Env.compute_rank_add env term in + let env, n = Env.compute_rank_add env term Mc.IsBool in (Mc.PEX n, env) in let rec parse_expr env term = @@ -730,13 +762,13 @@ module M = struct (power, env) with ParseError -> (* if the exponent is a variable *) - let env, n = Env.compute_rank_add env term in + let env, n = Env.compute_rank_add env term Mc.IsBool in (Mc.PEX n, env) ) | Ukn s -> if debug then ( Printf.printf "unknown op: %s\n" s; flush stdout ); - let env, n = Env.compute_rank_add env term in + let env, n = Env.compute_rank_add env term Mc.IsBool in (Mc.PEX n, env) ) | _ -> parse_variable env term ) | _ -> parse_variable env term ) @@ -878,7 +910,7 @@ module M = struct Mc.PEpow (expr, exp)) rop_spec - let parse_arith parse_op parse_expr env cstr gl = + let parse_arith parse_op parse_expr (k : Mc.kind) env cstr gl = let sigma = gl.sigma in if debug then Feedback.msg_debug @@ -887,7 +919,7 @@ module M = struct ++ fnl () ); match EConstr.kind sigma cstr with | App (op, args) -> - let op, lhs, rhs = parse_op gl (op, args) in + let op, lhs, rhs = parse_op gl k (op, args) in let e1, env = parse_expr gl env lhs in let e2, env = parse_expr gl env rhs in ({Mc.flhs = e1; Mc.fop = op; Mc.frhs = e2}, env) @@ -899,13 +931,16 @@ module M = struct (* generic parsing of arithmetic expressions *) - let mkC f1 f2 = Mc.Cj (f1, f2) - let mkD f1 f2 = Mc.D (f1, f2) - let mkIff f1 f2 = Mc.Cj (Mc.I (f1, None, f2), Mc.I (f2, None, f1)) - let mkI f1 f2 = Mc.I (f1, None, f2) + let mkAND b f1 f2 = Mc.AND (b, f1, f2) + let mkOR b f1 f2 = Mc.OR (b, f1, f2) + let mkIff b f1 f2 = Mc.IFF (b, f1, f2) + let mkIMPL b f1 f2 = Mc.IMPL (b, f1, None, f2) + let mkEQ f1 f2 = Mc.EQ (f1, f2) - let mkformula_binary g term f1 f2 = - match (f1, f2) with Mc.X _, Mc.X _ -> Mc.X term | _ -> g f1 f2 + let mkformula_binary b g term f1 f2 = + match (f1, f2) with + | Mc.X (b1, _), Mc.X (b2, _) -> Mc.X (b, term) + | _ -> g f1 f2 (** * This is the big generic function for formula parsers. @@ -915,83 +950,129 @@ module M = struct let sort = Retyping.get_sort_of env sigma term in Sorts.is_prop sort + type formula_op = + { op_and : EConstr.t + ; op_or : EConstr.t + ; op_iff : EConstr.t + ; op_not : EConstr.t + ; op_tt : EConstr.t + ; op_ff : EConstr.t } + + let prop_op = + lazy + { op_and = Lazy.force coq_and + ; op_or = Lazy.force coq_or + ; op_iff = Lazy.force coq_iff + ; op_not = Lazy.force coq_not + ; op_tt = Lazy.force coq_True + ; op_ff = Lazy.force coq_False } + + let bool_op = + lazy + { op_and = Lazy.force coq_andb + ; op_or = Lazy.force coq_orb + ; op_iff = Lazy.force coq_eqb + ; op_not = Lazy.force coq_negb + ; op_tt = Lazy.force coq_true + ; op_ff = Lazy.force coq_false } + let parse_formula gl parse_atom env tg term = let sigma = gl.sigma in - let is_prop term = is_prop gl.env gl.sigma term in - let parse_atom env tg t = + let parse_atom b env tg t = try - let at, env = parse_atom env t gl in - (Mc.A (at, (tg, t)), env, Tag.next tg) - with ParseError -> - if is_prop t then (Mc.X t, env, tg) else raise ParseError + let at, env = parse_atom b env t gl in + (Mc.A (b, at, (tg, t)), env, Tag.next tg) + with ParseError -> (Mc.X (b, t), env, tg) in - let rec xparse_formula env tg term = + let prop_op = Lazy.force prop_op in + let bool_op = Lazy.force bool_op in + let eq = Lazy.force coq_eq in + let bool = Lazy.force coq_bool in + let rec xparse_formula op k env tg term = match EConstr.kind sigma term with | App (l, rst) -> ( match rst with - | [|a; b|] when EConstr.eq_constr sigma l (Lazy.force coq_and) -> - let f, env, tg = xparse_formula env tg a in - let g, env, tg = xparse_formula env tg b in - (mkformula_binary mkC term f g, env, tg) - | [|a; b|] when EConstr.eq_constr sigma l (Lazy.force coq_or) -> - let f, env, tg = xparse_formula env tg a in - let g, env, tg = xparse_formula env tg b in - (mkformula_binary mkD term f g, env, tg) - | [|a|] when EConstr.eq_constr sigma l (Lazy.force coq_not) -> - let f, env, tg = xparse_formula env tg a in - (Mc.N f, env, tg) - | [|a; b|] when EConstr.eq_constr sigma l (Lazy.force coq_iff) -> - let f, env, tg = xparse_formula env tg a in - let g, env, tg = xparse_formula env tg b in - (mkformula_binary mkIff term f g, env, tg) - | _ -> parse_atom env tg term ) + | [|a; b|] when EConstr.eq_constr sigma l op.op_and -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary k (mkAND k) term f g, env, tg) + | [|a; b|] when EConstr.eq_constr sigma l op.op_or -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary k (mkOR k) term f g, env, tg) + | [|a; b|] when EConstr.eq_constr sigma l op.op_iff -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary k (mkIff k) term f g, env, tg) + | [|ty; a; b|] + when EConstr.eq_constr sigma l eq && is_convertible gl ty bool -> + let f, env, tg = xparse_formula bool_op Mc.IsBool env tg a in + let g, env, tg = xparse_formula bool_op Mc.IsBool env tg b in + (mkformula_binary Mc.IsProp mkEQ term f g, env, tg) + | [|a|] when EConstr.eq_constr sigma l op.op_not -> + let f, env, tg = xparse_formula op k env tg a in + (Mc.NOT (k, f), env, tg) + | _ -> parse_atom k env tg term ) | Prod (typ, a, b) - when typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b -> - let f, env, tg = xparse_formula env tg a in - let g, env, tg = xparse_formula env tg b in - (mkformula_binary mkI term f g, env, tg) + when kind_is_prop k + && (typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b) + -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary Mc.IsProp (mkIMPL Mc.IsProp) term f g, env, tg) | _ -> - if EConstr.eq_constr sigma term (Lazy.force coq_True) then - (Mc.TT, env, tg) - else if EConstr.eq_constr sigma term (Lazy.force coq_False) then - Mc.(FF, env, tg) - else if is_prop term then (Mc.X term, env, tg) - else raise ParseError + if EConstr.eq_constr sigma term op.op_tt then (Mc.TT k, env, tg) + else if EConstr.eq_constr sigma term op.op_ff then Mc.(FF k, env, tg) + else (Mc.X (k, term), env, tg) in - xparse_formula env tg (*Reductionops.whd_zeta*) term + xparse_formula prop_op Mc.IsProp env tg (*Reductionops.whd_zeta*) term + + (* let dump_bool b = Lazy.force (if b then coq_true else coq_false)*) + + let dump_kind k = + Lazy.force (match k with Mc.IsProp -> coq_IsProp | Mc.IsBool -> coq_IsBool) let dump_formula typ dump_atom f = let app_ctor c args = EConstr.mkApp ( Lazy.force c , Array.of_list - ( typ :: EConstr.mkProp :: Lazy.force coq_unit + ( typ :: Lazy.force coq_eKind :: Lazy.force coq_unit :: Lazy.force coq_unit :: args ) ) in let rec xdump f = match f with - | Mc.TT -> app_ctor coq_TT [] - | Mc.FF -> app_ctor coq_FF [] - | Mc.Cj (x, y) -> app_ctor coq_And [xdump x; xdump y] - | Mc.D (x, y) -> app_ctor coq_Or [xdump x; xdump y] - | Mc.I (x, _, y) -> - app_ctor coq_Impl - [ xdump x + | Mc.TT k -> app_ctor coq_TT [dump_kind k] + | Mc.FF k -> app_ctor coq_FF [dump_kind k] + | Mc.AND (k, x, y) -> app_ctor coq_AND [dump_kind k; xdump x; xdump y] + | Mc.OR (k, x, y) -> app_ctor coq_OR [dump_kind k; xdump x; xdump y] + | Mc.IMPL (k, x, _, y) -> + app_ctor coq_IMPL + [ dump_kind k + ; xdump x ; EConstr.mkApp (Lazy.force coq_None, [|Lazy.force coq_unit|]) ; xdump y ] - | Mc.N x -> app_ctor coq_Neg [xdump x] - | Mc.A (x, _) -> app_ctor coq_Atom [dump_atom x; Lazy.force coq_tt] - | Mc.X t -> app_ctor coq_X [t] + | Mc.NOT (k, x) -> app_ctor coq_NOT [dump_kind k; xdump x] + | Mc.IFF (k, x, y) -> app_ctor coq_IFF [dump_kind k; xdump x; xdump y] + | Mc.EQ (x, y) -> app_ctor coq_EQ [xdump x; xdump y] + | Mc.A (k, x, _) -> + app_ctor coq_Atom [dump_kind k; dump_atom x; Lazy.force coq_tt] + | Mc.X (k, t) -> app_ctor coq_X [dump_kind k; t] in xdump f let prop_env_of_formula gl form = Mc.( let rec doit env = function - | TT | FF | A (_, _) -> env - | X t -> fst (Env.compute_rank_add env t) - | Cj (f1, f2) | D (f1, f2) | I (f1, _, f2) -> doit (doit env f1) f2 - | N f -> doit env f + | TT _ | FF _ | A (_, _, _) -> env + | X (b, t) -> fst (Env.compute_rank_add env t b) + | AND (b, f1, f2) + |OR (b, f1, f2) + |IMPL (b, f1, _, f2) + |IFF (b, f1, f2) -> + doit (doit env f1) f2 + | NOT (b, f) -> doit env f + | EQ (f1, f2) -> doit (doit env f1) f2 in doit (Env.empty gl) form) @@ -1008,11 +1089,15 @@ module M = struct in Mc.( let rec doit = function - | TT | FF | X _ -> ISet.empty - | A (a, (t, c)) -> vars_of_atom a - | Cj (f1, f2) | D (f1, f2) | I (f1, _, f2) -> + | TT _ | FF _ | X _ -> ISet.empty + | A (_, a, (t, c)) -> vars_of_atom a + | AND (_, f1, f2) + |OR (_, f1, f2) + |IMPL (_, f1, _, f2) + |IFF (_, f1, f2) + |EQ (f1, f2) -> ISet.union (doit f1) (doit f2) - | N f -> doit f + | NOT (_, f) -> doit f in doit form) @@ -1026,7 +1111,8 @@ module M = struct ; dump_mul : EConstr.constr ; dump_pow : EConstr.constr ; dump_pow_arg : Mc.n -> EConstr.constr - ; dump_op : (Mc.op2 * EConstr.constr) list } + ; dump_op_prop : (Mc.op2 * EConstr.constr) list + ; dump_op_bool : (Mc.op2 * EConstr.constr) list } let dump_zexpr = lazy @@ -1038,7 +1124,9 @@ module M = struct ; dump_mul = Lazy.force coq_Zmult ; dump_pow = Lazy.force coq_Zpower ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))) - ; dump_op = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table } + ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_prop + ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_bool + } let dump_qexpr = lazy @@ -1050,7 +1138,9 @@ module M = struct ; dump_mul = Lazy.force coq_Qmult ; dump_pow = Lazy.force coq_Qpower ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))) - ; dump_op = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table } + ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_prop + ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_bool + } let rec dump_Rcst_as_R cst = match cst with @@ -1087,7 +1177,9 @@ module M = struct ; dump_mul = Lazy.force coq_Rmult ; dump_pow = Lazy.force coq_Rpower ; dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n))) - ; dump_op = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table } + ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_prop + ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_bool + } let prodn n env b = let rec prodrec = function @@ -1105,6 +1197,10 @@ module M = struct *) + let eKind = function + | Mc.IsProp -> EConstr.mkProp + | Mc.IsBool -> Lazy.force coq_bool + let make_goal_of_formula gl dexpr form = let vars_idx = List.mapi @@ -1120,7 +1216,7 @@ module M = struct in let props_n = List.mapi - (fun i _ -> (fresh_prop "__p" (i + 1), EConstr.mkProp)) + (fun i (_, k) -> (fresh_prop "__p" (i + 1), eKind k)) (Env.elements props) in let var_name_pos = @@ -1129,8 +1225,7 @@ module M = struct let dump_expr i e = let rec dump_expr = function | Mc.PEX n -> - EConstr.mkRel - (i + CList.assoc_f Int.equal (CoqToCaml.positive n) vars_idx) + EConstr.mkRel (i + List.assoc (CoqToCaml.positive n) vars_idx) | Mc.PEc z -> dexpr.dump_cst z | Mc.PEadd (e1, e2) -> EConstr.mkApp (dexpr.dump_add, [|dump_expr e1; dump_expr e2|]) @@ -1144,31 +1239,70 @@ module M = struct in dump_expr e in - let mkop op e1 e2 = - try - EConstr.mkApp - (CList.assoc_f Mutils.Hash.eq_op2 op dexpr.dump_op, [|e1; e2|]) + let mkop_prop op e1 e2 = + try EConstr.mkApp (List.assoc op dexpr.dump_op_prop, [|e1; e2|]) + with Not_found -> + EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|]) + in + let dump_cstr_prop i {Mc.flhs; Mc.fop; Mc.frhs} = + mkop_prop fop (dump_expr i flhs) (dump_expr i frhs) + in + let mkop_bool op e1 e2 = + try EConstr.mkApp (List.assoc op dexpr.dump_op_bool, [|e1; e2|]) with Not_found -> - EConstr.mkApp (Lazy.force coq_Eq, [|dexpr.interp_typ; e1; e2|]) + EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|]) in - let dump_cstr i {Mc.flhs; Mc.fop; Mc.frhs} = - mkop fop (dump_expr i flhs) (dump_expr i frhs) + let dump_cstr_bool i {Mc.flhs; Mc.fop; Mc.frhs} = + mkop_bool fop (dump_expr i flhs) (dump_expr i frhs) in - let rec xdump pi xi f = + let rec xdump_prop pi xi f = match f with - | Mc.TT -> Lazy.force coq_True - | Mc.FF -> Lazy.force coq_False - | Mc.Cj (x, y) -> - EConstr.mkApp (Lazy.force coq_and, [|xdump pi xi x; xdump pi xi y|]) - | Mc.D (x, y) -> - EConstr.mkApp (Lazy.force coq_or, [|xdump pi xi x; xdump pi xi y|]) - | Mc.I (x, _, y) -> - EConstr.mkArrow (xdump pi xi x) Sorts.Relevant - (xdump (pi + 1) (xi + 1) y) - | Mc.N x -> - EConstr.mkArrow (xdump pi xi x) Sorts.Relevant (Lazy.force coq_False) - | Mc.A (x, _) -> dump_cstr xi x - | Mc.X t -> + | Mc.TT _ -> Lazy.force coq_True + | Mc.FF _ -> Lazy.force coq_False + | Mc.AND (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_and, [|xdump_prop pi xi x; xdump_prop pi xi y|]) + | Mc.OR (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_or, [|xdump_prop pi xi x; xdump_prop pi xi y|]) + | Mc.IFF (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_iff, [|xdump_prop pi xi x; xdump_prop pi xi y|]) + | Mc.IMPL (_, x, _, y) -> + EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant + (xdump_prop (pi + 1) (xi + 1) y) + | Mc.NOT (_, x) -> + EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant + (Lazy.force coq_False) + | Mc.EQ (x, y) -> + EConstr.mkApp + ( Lazy.force coq_eq + , [|Lazy.force coq_bool; xdump_bool pi xi x; xdump_bool pi xi y|] ) + | Mc.A (_, x, _) -> dump_cstr_prop xi x + | Mc.X (_, t) -> + let idx = Env.get_rank props t in + EConstr.mkRel (pi + idx) + and xdump_bool pi xi f = + match f with + | Mc.TT _ -> Lazy.force coq_true + | Mc.FF _ -> Lazy.force coq_false + | Mc.AND (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_andb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.OR (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_orb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.IFF (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_eqb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.IMPL (_, x, _, y) -> + EConstr.mkApp + (Lazy.force coq_implb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.NOT (_, x) -> + EConstr.mkApp (Lazy.force coq_negb, [|xdump_bool pi xi x|]) + | Mc.EQ (x, y) -> assert false + | Mc.A (_, x, _) -> dump_cstr_bool xi x + | Mc.X (_, t) -> let idx = Env.get_rank props t in EConstr.mkRel (pi + idx) in @@ -1179,12 +1313,12 @@ module M = struct let idx = Env.get_rank props p in EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx)) in - let form' = Mc.mapX subst_prop form in + let form' = Mc.mapX (fun _ p -> subst_prop p) Mc.IsProp form in ( prodn nb_props (List.map (fun (x, y) -> (Name.Name x, y)) props_n) (prodn nb_vars (List.map (fun (x, y) -> (Name.Name x, y)) vars_n) - (xdump (List.length vars_n) 0 form)) + (xdump_prop (List.length vars_n) 0 form)) , List.rev props_n , List.rev var_name_pos , form' ) @@ -1339,7 +1473,9 @@ let qq_domain_spec = ; coeff_eq = Mc.qeq_bool } let max_tag f = - 1 + Tag.to_int (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) f (Tag.from 0)) + 1 + + Tag.to_int + (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) Mc.IsProp f (Tag.from 0)) (** Naive topological sort of constr according to the subterm-ordering *) @@ -1364,7 +1500,9 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*) (set [ ( "__ff" , ff - , EConstr.mkApp (Lazy.force coq_Formula, [|formula_typ|]) ) + , EConstr.mkApp + ( Lazy.force coq_Formula + , [|formula_typ; Lazy.force coq_IsProp|] ) ) ; ( "__varmap" , vm , EConstr.mkApp (Lazy.force coq_VarMap, [|spec.typ|]) ) @@ -1527,37 +1665,73 @@ let abstract_formula : TagSet.t -> 'a formula -> 'a formula = fun hyps f -> let to_constr = Mc. - { mkTT = Lazy.force coq_True - ; mkFF = Lazy.force coq_False - ; mkA = (fun a (tg, t) -> t) - ; mkCj = + { mkTT = + (let coq_True = Lazy.force coq_True in + let coq_true = Lazy.force coq_true in + function Mc.IsProp -> coq_True | Mc.IsBool -> coq_true) + ; mkFF = + (let coq_False = Lazy.force coq_False in + let coq_false = Lazy.force coq_false in + function Mc.IsProp -> coq_False | Mc.IsBool -> coq_false) + ; mkA = (fun k a (tg, t) -> t) + ; mkAND = (let coq_and = Lazy.force coq_and in - fun x y -> EConstr.mkApp (coq_and, [|x; y|])) - ; mkD = + let coq_andb = Lazy.force coq_andb in + fun k x y -> + EConstr.mkApp + ( (match k with Mc.IsProp -> coq_and | Mc.IsBool -> coq_andb) + , [|x; y|] )) + ; mkOR = (let coq_or = Lazy.force coq_or in - fun x y -> EConstr.mkApp (coq_or, [|x; y|])) - ; mkI = (fun x y -> EConstr.mkArrow x Sorts.Relevant y) - ; mkN = + let coq_orb = Lazy.force coq_orb in + fun k x y -> + EConstr.mkApp + ( (match k with Mc.IsProp -> coq_or | Mc.IsBool -> coq_orb) + , [|x; y|] )) + ; mkIMPL = + (fun k x y -> + match k with + | Mc.IsProp -> EConstr.mkArrow x Sorts.Relevant y + | Mc.IsBool -> EConstr.mkApp (Lazy.force coq_implb, [|x; y|])) + ; mkIFF = + (let coq_iff = Lazy.force coq_iff in + let coq_eqb = Lazy.force coq_eqb in + fun k x y -> + EConstr.mkApp + ( (match k with Mc.IsProp -> coq_iff | Mc.IsBool -> coq_eqb) + , [|x; y|] )) + ; mkNOT = (let coq_not = Lazy.force coq_not in - fun x -> EConstr.mkApp (coq_not, [|x|])) } + let coq_negb = Lazy.force coq_negb in + fun k x -> + EConstr.mkApp + ( (match k with Mc.IsProp -> coq_not | Mc.IsBool -> coq_negb) + , [|x|] )) + ; mkEQ = + (let coq_eq = Lazy.force coq_eq in + fun x y -> EConstr.mkApp (coq_eq, [|Lazy.force coq_bool; x; y|])) } in - Mc.abst_form to_constr (fun (t, _) -> TagSet.mem t hyps) true f + Mc.abst_form to_constr (fun (t, _) -> TagSet.mem t hyps) true Mc.IsProp f (* [abstract_wrt_formula] is used in contexts whre f1 is already an abstraction of f2 *) let rec abstract_wrt_formula f1 f2 = Mc.( match (f1, f2) with - | X c, _ -> X c + | X (b, c), _ -> X (b, c) | A _, A _ -> f2 - | Cj (a, b), Cj (a', b') -> - Cj (abstract_wrt_formula a a', abstract_wrt_formula b b') - | D (a, b), D (a', b') -> - D (abstract_wrt_formula a a', abstract_wrt_formula b b') - | I (a, _, b), I (a', x, b') -> - I (abstract_wrt_formula a a', x, abstract_wrt_formula b b') - | FF, FF -> FF - | TT, TT -> TT - | N x, N y -> N (abstract_wrt_formula x y) + | AND (b, f1, f2), AND (_, f1', f2') -> + AND (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2') + | OR (b, f1, f2), OR (_, f1', f2') -> + OR (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2') + | IMPL (b, f1, _, f2), IMPL (_, f1', x, f2') -> + IMPL (b, abstract_wrt_formula f1 f1', x, abstract_wrt_formula f2 f2') + | IFF (b, f1, f2), IFF (_, f1', f2') -> + IFF (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2') + | EQ (f1, f2), EQ (f1', f2') -> + EQ (abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2') + | FF b, FF _ -> FF b + | TT b, TT _ -> TT b + | NOT (b, x), NOT (_, y) -> NOT (b, abstract_wrt_formula x y) | _ -> failwith "abstract_wrt_formula") (** @@ -1577,7 +1751,7 @@ let formula_hyps_concl hyps concl = (fun (id, f) (cc, ids) -> match f with | Mc.X _ -> (cc, ids) - | _ -> (Mc.I (f, Some id, cc), id :: ids)) + | _ -> (Mc.IMPL (Mc.IsProp, f, Some id, cc), id :: ids)) hyps (concl, []) (* let time str f x = @@ -1595,7 +1769,7 @@ let micromega_tauto pre_process cnf spec prover env let mt = CamlToCoq.positive (max_tag ff) in (* Construction of cnf *) let pre_ff = pre_process mt (ff : 'a formula) in - let cnf_ff, cnf_ff_tags = cnf pre_ff in + let cnf_ff, cnf_ff_tags = cnf Mc.IsProp pre_ff in match witness_list_tags prover cnf_ff with | Model m -> Model m | Unknown -> Unknown @@ -1621,7 +1795,7 @@ let micromega_tauto pre_process cnf spec prover env in let ff' = abstract_formula deps ff in let pre_ff' = pre_process mt ff' in - let cnf_ff', _ = cnf pre_ff' in + let cnf_ff', _ = cnf Mc.IsProp pre_ff' in if debug then begin output_string stdout "\n"; Printf.printf "TForm : %a\n" pp_formula ff; @@ -1647,7 +1821,7 @@ let micromega_tauto pre_process cnf spec prover env | Some res -> () end ; *) let res' = compact_proofs spec.coeff_eq cnf_ff res cnf_ff' in - let ff', res', ids = (ff', res', Mc.ids_of_formula ff') in + let ff', res', ids = (ff', res', Mc.ids_of_formula Mc.IsProp ff') in let res' = dump_list spec.proof_typ spec.dump_proof res' in Prf (ids, ff', res') @@ -1719,9 +1893,11 @@ let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac = env' ff_arith ] in let goal_props = - List.rev (Env.elements (prop_env_of_formula gl0 ff')) + List.rev (List.map fst (Env.elements (prop_env_of_formula gl0 ff'))) + in + let goal_vars = + List.map (fun (_, i) -> fst (List.nth env (i - 1))) vars in - let goal_vars = List.map (fun (_, i) -> List.nth env (i - 1)) vars in let arith_args = goal_props @ goal_vars in let kill_arith = Tacticals.New.tclTHEN tac_arith tac in (* @@ -1773,7 +1949,9 @@ let micromega_order_changer cert env ff = (set [ ( "__ff" , ff - , EConstr.mkApp (Lazy.force coq_Formula, [|formula_typ|]) ) + , EConstr.mkApp + ( Lazy.force coq_Formula + , [|formula_typ; Lazy.force coq_IsProp|] ) ) ; ("__varmap", vm, EConstr.mkApp (Lazy.force coq_VarMap, [|typ|])) ; ("__wit", cert, cert_typ) ] (Tacmach.New.pf_concl gl)) @@ -1805,11 +1983,16 @@ let micromega_genr prover tac = let hyps' = List.map (fun (n, f) -> - (n, Mc.map_bformula (Micromega.map_Formula Micromega.q_of_Rcst) f)) + ( n + , Mc.map_bformula Mc.IsProp + (Micromega.map_Formula Micromega.q_of_Rcst) + f )) hyps in let concl' = - Mc.map_bformula (Micromega.map_Formula Micromega.q_of_Rcst) concl + Mc.map_bformula Mc.IsProp + (Micromega.map_Formula Micromega.q_of_Rcst) + concl in match micromega_tauto @@ -1847,9 +2030,11 @@ let micromega_genr prover tac = ; micromega_order_changer res' env' ff_arith ] in let goal_props = - List.rev (Env.elements (prop_env_of_formula gl0 ff')) + List.rev (List.map fst (Env.elements (prop_env_of_formula gl0 ff'))) + in + let goal_vars = + List.map (fun (_, i) -> fst (List.nth env (i - 1))) vars in - let goal_vars = List.map (fun (_, i) -> List.nth env (i - 1)) vars in let arith_args = goal_props @ goal_vars in let kill_arith = Tacticals.New.tclTHEN tac_arith tac in (* Tacticals.New.tclTHEN diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index d17a0aabb7..b231779c7b 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -967,39 +967,49 @@ let rec norm_aux cO cI cadd cmul csub copp ceqb = function ppow_N cO cI cadd cmul ceqb (fun p -> p) (norm_aux cO cI cadd cmul csub copp ceqb pe1) n0 +type kind = +| IsProp +| IsBool + type ('tA, 'tX, 'aA, 'aF) gFormula = -| TT -| FF -| X of 'tX -| A of 'tA * 'aA -| Cj of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula -| D of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula -| N of ('tA, 'tX, 'aA, 'aF) gFormula -| I of ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option +| TT of kind +| FF of kind +| X of kind * 'tX +| A of kind * 'tA * 'aA +| AND of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula +| OR of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula +| NOT of kind * ('tA, 'tX, 'aA, 'aF) gFormula +| IMPL of kind * ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option * ('tA, 'tX, 'aA, 'aF) gFormula +| IFF of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula +| EQ of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula (** val mapX : - ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) - gFormula **) - -let rec mapX f = function -| X x -> X (f x) -| Cj (f1, f2) -> Cj ((mapX f f1), (mapX f f2)) -| D (f1, f2) -> D ((mapX f f1), (mapX f f2)) -| N f1 -> N (mapX f f1) -| I (f1, o, f2) -> I ((mapX f f1), o, (mapX f f2)) + (kind -> 'a2 -> 'a2) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, + 'a2, 'a3, 'a4) gFormula **) + +let rec mapX f _ = function +| X (k0, x) -> X (k0, (f k0 x)) +| AND (k0, f1, f2) -> AND (k0, (mapX f k0 f1), (mapX f k0 f2)) +| OR (k0, f1, f2) -> OR (k0, (mapX f k0 f1), (mapX f k0 f2)) +| NOT (k0, f1) -> NOT (k0, (mapX f k0 f1)) +| IMPL (k0, f1, o, f2) -> IMPL (k0, (mapX f k0 f1), o, (mapX f k0 f2)) +| IFF (k0, f1, f2) -> IFF (k0, (mapX f k0 f1), (mapX f k0 f2)) +| EQ (f1, f2) -> EQ ((mapX f IsBool f1), (mapX f IsBool f2)) | x -> x (** val foldA : - ('a5 -> 'a3 -> 'a5) -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 **) + ('a5 -> 'a3 -> 'a5) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 **) -let rec foldA f f0 acc = +let rec foldA f _ f0 acc = match f0 with - | A (_, an) -> f acc an - | Cj (f1, f2) -> foldA f f1 (foldA f f2 acc) - | D (f1, f2) -> foldA f f1 (foldA f f2 acc) - | N f1 -> foldA f f1 acc - | I (f1, _, f2) -> foldA f f1 (foldA f f2 acc) + | A (_, _, an) -> f acc an + | AND (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) + | OR (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) + | NOT (k0, f1) -> foldA f k0 f1 acc + | IMPL (k0, f1, _, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) + | IFF (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) + | EQ (f1, f2) -> foldA f IsBool f1 (foldA f IsBool f2 acc) | _ -> acc (** val cons_id : 'a1 option -> 'a1 list -> 'a1 list **) @@ -1009,37 +1019,50 @@ let cons_id id l = | Some id0 -> id0::l | None -> l -(** val ids_of_formula : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list **) +(** val ids_of_formula : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list **) -let rec ids_of_formula = function -| I (_, id, f') -> cons_id id (ids_of_formula f') +let rec ids_of_formula _ = function +| IMPL (k0, _, id, f') -> cons_id id (ids_of_formula k0 f') | _ -> [] -(** val collect_annot : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list **) +(** val collect_annot : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list **) -let rec collect_annot = function -| A (_, a) -> a::[] -| Cj (f1, f2) -> app (collect_annot f1) (collect_annot f2) -| D (f1, f2) -> app (collect_annot f1) (collect_annot f2) -| N f0 -> collect_annot f0 -| I (f1, _, f2) -> app (collect_annot f1) (collect_annot f2) +let rec collect_annot _ = function +| A (_, _, a) -> a::[] +| AND (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) +| OR (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) +| NOT (k0, f0) -> collect_annot k0 f0 +| IMPL (k0, f1, _, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) +| IFF (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) +| EQ (f1, f2) -> app (collect_annot IsBool f1) (collect_annot IsBool f2) | _ -> [] -type 'a bFormula = ('a, __, unit0, unit0) gFormula +type rtyp = __ + +type eKind = __ + +type 'a bFormula = ('a, eKind, unit0, unit0) gFormula (** val map_bformula : - ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, 'a5) - gFormula **) - -let rec map_bformula fct = function -| TT -> TT -| FF -> FF -| X p -> X p -| A (a, t0) -> A ((fct a), t0) -| Cj (f1, f2) -> Cj ((map_bformula fct f1), (map_bformula fct f2)) -| D (f1, f2) -> D ((map_bformula fct f1), (map_bformula fct f2)) -| N f0 -> N (map_bformula fct f0) -| I (f1, a, f2) -> I ((map_bformula fct f1), a, (map_bformula fct f2)) + kind -> ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, + 'a5) gFormula **) + +let rec map_bformula _ fct = function +| TT k -> TT k +| FF k -> FF k +| X (k, p) -> X (k, p) +| A (k, a, t0) -> A (k, (fct a), t0) +| AND (k0, f1, f2) -> + AND (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2)) +| OR (k0, f1, f2) -> + OR (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2)) +| NOT (k0, f0) -> NOT (k0, (map_bformula k0 fct f0)) +| IMPL (k0, f1, a, f2) -> + IMPL (k0, (map_bformula k0 fct f1), a, (map_bformula k0 fct f2)) +| IFF (k0, f1, f2) -> + IFF (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2)) +| EQ (f1, f2) -> + EQ ((map_bformula IsBool fct f1), (map_bformula IsBool fct f2)) type ('x, 'annot) clause = ('x * 'annot) list @@ -1147,7 +1170,7 @@ let is_cnf_ff = function let and_cnf_opt f1 f2 = if if is_cnf_ff f1 then true else is_cnf_ff f2 then cnf_ff - else and_cnf f1 f2 + else if is_cnf_tt f2 then f1 else and_cnf f1 f2 (** val or_cnf_opt : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, @@ -1158,36 +1181,89 @@ let or_cnf_opt unsat deduce f1 f2 = then cnf_tt else if is_cnf_ff f2 then f1 else or_cnf unsat deduce f1 f2 -(** val xcnf : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) - cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) - tFormula -> ('a2, 'a3) cnf **) - -let rec xcnf unsat deduce normalise1 negate0 pol0 = function -| TT -> if pol0 then cnf_tt else cnf_ff -| FF -> if pol0 then cnf_ff else cnf_tt -| X _ -> cnf_ff -| A (x, t0) -> if pol0 then normalise1 x t0 else negate0 x t0 -| Cj (e1, e2) -> +(** val mk_and : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, + 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) + +let mk_and unsat deduce rEC k pol0 f1 f2 = if pol0 - then and_cnf_opt (xcnf unsat deduce normalise1 negate0 pol0 e1) - (xcnf unsat deduce normalise1 negate0 pol0 e2) - else or_cnf_opt unsat deduce (xcnf unsat deduce normalise1 negate0 pol0 e1) - (xcnf unsat deduce normalise1 negate0 pol0 e2) -| D (e1, e2) -> + then and_cnf_opt (rEC pol0 k f1) (rEC pol0 k f2) + else or_cnf_opt unsat deduce (rEC pol0 k f1) (rEC pol0 k f2) + +(** val mk_or : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, + 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) + +let mk_or unsat deduce rEC k pol0 f1 f2 = if pol0 - then or_cnf_opt unsat deduce (xcnf unsat deduce normalise1 negate0 pol0 e1) - (xcnf unsat deduce normalise1 negate0 pol0 e2) - else and_cnf_opt (xcnf unsat deduce normalise1 negate0 pol0 e1) - (xcnf unsat deduce normalise1 negate0 pol0 e2) -| N e -> xcnf unsat deduce normalise1 negate0 (negb pol0) e -| I (e1, _, e2) -> + then or_cnf_opt unsat deduce (rEC pol0 k f1) (rEC pol0 k f2) + else and_cnf_opt (rEC pol0 k f1) (rEC pol0 k f2) + +(** val mk_impl : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, + 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) + +let mk_impl unsat deduce rEC k pol0 f1 f2 = if pol0 - then or_cnf_opt unsat deduce - (xcnf unsat deduce normalise1 negate0 (negb pol0) e1) - (xcnf unsat deduce normalise1 negate0 pol0 e2) - else and_cnf_opt (xcnf unsat deduce normalise1 negate0 (negb pol0) e1) - (xcnf unsat deduce normalise1 negate0 pol0 e2) + then or_cnf_opt unsat deduce (rEC (negb pol0) k f1) (rEC pol0 k f2) + else and_cnf_opt (rEC (negb pol0) k f1) (rEC pol0 k f2) + +(** val mk_iff : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, + 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) + +let mk_iff unsat deduce rEC k pol0 f1 f2 = + or_cnf_opt unsat deduce + (and_cnf_opt (rEC (negb pol0) k f1) (rEC false k f2)) + (and_cnf_opt (rEC pol0 k f1) (rEC true k f2)) + +(** val is_bool : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool option **) + +let is_bool _ = function +| TT _ -> Some true +| FF _ -> Some false +| _ -> None + +(** val xcnf : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) + cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4, + 'a5) tFormula -> ('a2, 'a3) cnf **) + +let rec xcnf unsat deduce normalise1 negate0 pol0 _ = function +| TT _ -> if pol0 then cnf_tt else cnf_ff +| FF _ -> if pol0 then cnf_ff else cnf_tt +| X (_, _) -> cnf_ff +| A (_, x, t0) -> if pol0 then normalise1 x t0 else negate0 x t0 +| AND (k0, e1, e2) -> + mk_and unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2 +| OR (k0, e1, e2) -> + mk_or unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2 +| NOT (k0, e) -> xcnf unsat deduce normalise1 negate0 (negb pol0) k0 e +| IMPL (k0, e1, _, e2) -> + mk_impl unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2 +| IFF (k0, e1, e2) -> + (match is_bool k0 e2 with + | Some isb -> + xcnf unsat deduce normalise1 negate0 (if isb then pol0 else negb pol0) + k0 e1 + | None -> + mk_iff unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2) +| EQ (e1, e2) -> + (match is_bool IsBool e2 with + | Some isb -> + xcnf unsat deduce normalise1 negate0 (if isb then pol0 else negb pol0) + IsBool e1 + | None -> + mk_iff unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) IsBool pol0 e1 e2) (** val radd_term : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) @@ -1271,141 +1347,311 @@ let ror_cnf_opt unsat deduce f1 f2 = let ratom c a = if if is_cnf_ff c then true else is_cnf_tt c then c,(a::[]) else c,[] -(** val rxcnf : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) - cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) - tFormula -> ('a2, 'a3) cnf * 'a3 list **) - -let rec rxcnf unsat deduce normalise1 negate0 polarity = function -| TT -> if polarity then cnf_tt,[] else cnf_ff,[] -| FF -> if polarity then cnf_ff,[] else cnf_tt,[] -| X _ -> cnf_ff,[] -| A (x, t0) -> ratom (if polarity then normalise1 x t0 else negate0 x t0) t0 -| Cj (e1, e2) -> - let e3,t1 = rxcnf unsat deduce normalise1 negate0 polarity e1 in - let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in +(** val rxcnf_and : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind -> + ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, + 'a3) cnf * 'a3 list **) + +let rxcnf_and unsat deduce rXCNF polarity k e1 e2 = + let e3,t1 = rXCNF polarity k e1 in + let e4,t2 = rXCNF polarity k e2 in if polarity then (and_cnf_opt e3 e4),(rev_append t1 t2) else let f',t' = ror_cnf_opt unsat deduce e3 e4 in f',(rev_append t1 (rev_append t2 t')) -| D (e1, e2) -> - let e3,t1 = rxcnf unsat deduce normalise1 negate0 polarity e1 in - let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in + +(** val rxcnf_or : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind -> + ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, + 'a3) cnf * 'a3 list **) + +let rxcnf_or unsat deduce rXCNF polarity k e1 e2 = + let e3,t1 = rXCNF polarity k e1 in + let e4,t2 = rXCNF polarity k e2 in if polarity then let f',t' = ror_cnf_opt unsat deduce e3 e4 in f',(rev_append t1 (rev_append t2 t')) else (and_cnf_opt e3 e4),(rev_append t1 t2) -| N e -> rxcnf unsat deduce normalise1 negate0 (negb polarity) e -| I (e1, _, e2) -> - let e3,t1 = rxcnf unsat deduce normalise1 negate0 (negb polarity) e1 in + +(** val rxcnf_impl : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind -> + ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, + 'a3) cnf * 'a3 list **) + +let rxcnf_impl unsat deduce rXCNF polarity k e1 e2 = + let e3,t1 = rXCNF (negb polarity) k e1 in if polarity then if is_cnf_ff e3 - then rxcnf unsat deduce normalise1 negate0 polarity e2 - else let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in + then rXCNF polarity k e2 + else let e4,t2 = rXCNF polarity k e2 in let f',t' = ror_cnf_opt unsat deduce e3 e4 in f',(rev_append t1 (rev_append t2 t')) - else let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in + else let e4,t2 = rXCNF polarity k e2 in (and_cnf_opt e3 e4),(rev_append t1 t2) -type ('term, 'annot, 'tX) to_constrT = { mkTT : 'tX; mkFF : 'tX; - mkA : ('term -> 'annot -> 'tX); - mkCj : ('tX -> 'tX -> 'tX); - mkD : ('tX -> 'tX -> 'tX); - mkI : ('tX -> 'tX -> 'tX); - mkN : ('tX -> 'tX) } +(** val rxcnf_iff : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind -> + ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, + 'a3) cnf * 'a3 list **) + +let rxcnf_iff unsat deduce rXCNF polarity k e1 e2 = + let c1,t1 = rXCNF (negb polarity) k e1 in + let c2,t2 = rXCNF false k e2 in + let c3,t3 = rXCNF polarity k e1 in + let c4,t4 = rXCNF true k e2 in + let f',t' = ror_cnf_opt unsat deduce (and_cnf_opt c1 c2) (and_cnf_opt c3 c4) + in + f',(rev_append t1 (rev_append t2 (rev_append t3 (rev_append t4 t')))) + +(** val rxcnf : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) + cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4, + 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list **) + +let rec rxcnf unsat deduce normalise1 negate0 polarity _ = function +| TT _ -> if polarity then cnf_tt,[] else cnf_ff,[] +| FF _ -> if polarity then cnf_ff,[] else cnf_tt,[] +| X (_, _) -> cnf_ff,[] +| A (_, x, t0) -> + ratom (if polarity then normalise1 x t0 else negate0 x t0) t0 +| AND (k0, e1, e2) -> + rxcnf_and unsat deduce (fun x x0 x1 -> + rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2 +| OR (k0, e1, e2) -> + rxcnf_or unsat deduce (fun x x0 x1 -> + rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2 +| NOT (k0, e) -> rxcnf unsat deduce normalise1 negate0 (negb polarity) k0 e +| IMPL (k0, e1, _, e2) -> + rxcnf_impl unsat deduce (fun x x0 x1 -> + rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2 +| IFF (k0, e1, e2) -> + rxcnf_iff unsat deduce (fun x x0 x1 -> + rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2 +| EQ (e1, e2) -> + rxcnf_iff unsat deduce (fun x x0 x1 -> + rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity IsBool e1 e2 + +type ('term, 'annot, 'tX) to_constrT = { mkTT : (kind -> 'tX); + mkFF : (kind -> 'tX); + mkA : (kind -> 'term -> 'annot -> + 'tX); + mkAND : (kind -> 'tX -> 'tX -> 'tX); + mkOR : (kind -> 'tX -> 'tX -> 'tX); + mkIMPL : (kind -> 'tX -> 'tX -> 'tX); + mkIFF : (kind -> 'tX -> 'tX -> 'tX); + mkNOT : (kind -> 'tX -> 'tX); + mkEQ : ('tX -> 'tX -> 'tX) } (** val aformula : - ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 **) - -let rec aformula to_constr = function -| TT -> to_constr.mkTT -| FF -> to_constr.mkFF -| X p -> p -| A (x, t0) -> to_constr.mkA x t0 -| Cj (f1, f2) -> - to_constr.mkCj (aformula to_constr f1) (aformula to_constr f2) -| D (f1, f2) -> to_constr.mkD (aformula to_constr f1) (aformula to_constr f2) -| N f0 -> to_constr.mkN (aformula to_constr f0) -| I (f1, _, f2) -> - to_constr.mkI (aformula to_constr f1) (aformula to_constr f2) - -(** val is_X : ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option **) - -let is_X = function -| X p -> Some p + ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 **) + +let rec aformula to_constr _ = function +| TT b -> to_constr.mkTT b +| FF b -> to_constr.mkFF b +| X (_, p) -> p +| A (b, x, t0) -> to_constr.mkA b x t0 +| AND (k0, f1, f2) -> + to_constr.mkAND k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2) +| OR (k0, f1, f2) -> + to_constr.mkOR k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2) +| NOT (k0, f0) -> to_constr.mkNOT k0 (aformula to_constr k0 f0) +| IMPL (k0, f1, _, f2) -> + to_constr.mkIMPL k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2) +| IFF (k0, f1, f2) -> + to_constr.mkIFF k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2) +| EQ (f1, f2) -> + to_constr.mkEQ (aformula to_constr IsBool f1) (aformula to_constr IsBool f2) + +(** val is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option **) + +let is_X _ = function +| X (_, p) -> Some p | _ -> None (** val abs_and : - ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, - 'a3, 'a4) tFormula -> (('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, - 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) - gFormula **) - -let abs_and to_constr f1 f2 c = - match is_X f1 with - | Some _ -> X (aformula to_constr (c f1 f2)) + ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> + ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> + ('a1, 'a3, 'a2, 'a4) gFormula **) + +let abs_and to_constr k f1 f2 c = + match is_X k f1 with + | Some _ -> X (k, (aformula to_constr k (c k f1 f2))) | None -> - (match is_X f2 with - | Some _ -> X (aformula to_constr (c f1 f2)) - | None -> c f1 f2) + (match is_X k f2 with + | Some _ -> X (k, (aformula to_constr k (c k f1 f2))) + | None -> c k f1 f2) (** val abs_or : - ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, - 'a3, 'a4) tFormula -> (('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, - 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) - gFormula **) + ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> + ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> + ('a1, 'a3, 'a2, 'a4) gFormula **) -let abs_or to_constr f1 f2 c = - match is_X f1 with +let abs_or to_constr k f1 f2 c = + match is_X k f1 with | Some _ -> - (match is_X f2 with - | Some _ -> X (aformula to_constr (c f1 f2)) - | None -> c f1 f2) - | None -> c f1 f2 + (match is_X k f2 with + | Some _ -> X (k, (aformula to_constr k (c k f1 f2))) + | None -> c k f1 f2) + | None -> c k f1 f2 + +(** val abs_not : + ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> + (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) + -> ('a1, 'a3, 'a2, 'a4) gFormula **) + +let abs_not to_constr k f1 c = + match is_X k f1 with + | Some _ -> X (k, (aformula to_constr k (c k f1))) + | None -> c k f1 (** val mk_arrow : - 'a4 option -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) - tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **) + 'a4 option -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, + 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **) -let mk_arrow o f1 f2 = +let mk_arrow o k f1 f2 = match o with - | Some _ -> (match is_X f1 with - | Some _ -> f2 - | None -> I (f1, o, f2)) - | None -> I (f1, None, f2) + | Some _ -> + (match is_X k f1 with + | Some _ -> f2 + | None -> IMPL (k, f1, o, f2)) + | None -> IMPL (k, f1, None, f2) + +(** val abst_simpl : + ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> kind -> ('a1, 'a2, 'a3, + 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **) + +let rec abst_simpl to_constr needA _ = function +| A (k, x, t0) -> + if needA t0 then A (k, x, t0) else X (k, (to_constr.mkA k x t0)) +| AND (k0, f1, f2) -> + AND (k0, (abst_simpl to_constr needA k0 f1), + (abst_simpl to_constr needA k0 f2)) +| OR (k0, f1, f2) -> + OR (k0, (abst_simpl to_constr needA k0 f1), + (abst_simpl to_constr needA k0 f2)) +| NOT (k0, f0) -> NOT (k0, (abst_simpl to_constr needA k0 f0)) +| IMPL (k0, f1, o, f2) -> + IMPL (k0, (abst_simpl to_constr needA k0 f1), o, + (abst_simpl to_constr needA k0 f2)) +| IFF (k0, f1, f2) -> + IFF (k0, (abst_simpl to_constr needA k0 f1), + (abst_simpl to_constr needA k0 f2)) +| EQ (f1, f2) -> + EQ ((abst_simpl to_constr needA IsBool f1), + (abst_simpl to_constr needA IsBool f2)) +| x -> x -(** val abst_form : - ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> ('a1, 'a2, 'a3, - 'a4) tFormula -> ('a1, 'a3, 'a2, 'a4) gFormula **) - -let rec abst_form to_constr needA pol0 = function -| TT -> if pol0 then TT else X to_constr.mkTT -| FF -> if pol0 then X to_constr.mkFF else FF -| X p -> X p -| A (x, t0) -> if needA t0 then A (x, t0) else X (to_constr.mkA x t0) -| Cj (f1, f2) -> - let f3 = abst_form to_constr needA pol0 f1 in - let f4 = abst_form to_constr needA pol0 f2 in +(** val abst_and : + ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) + tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2, + 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, + 'a4) tFormula **) + +let abst_and to_constr rEC pol0 k f1 f2 = if pol0 - then abs_and to_constr f3 f4 (fun x x0 -> Cj (x, x0)) - else abs_or to_constr f3 f4 (fun x x0 -> Cj (x, x0)) -| D (f1, f2) -> - let f3 = abst_form to_constr needA pol0 f1 in - let f4 = abst_form to_constr needA pol0 f2 in + then abs_and to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> + AND (x, x0, x1)) + else abs_or to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> AND + (x, x0, x1)) + +(** val abst_or : + ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) + tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2, + 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, + 'a4) tFormula **) + +let abst_or to_constr rEC pol0 k f1 f2 = if pol0 - then abs_or to_constr f3 f4 (fun x x0 -> D (x, x0)) - else abs_and to_constr f3 f4 (fun x x0 -> D (x, x0)) -| N f0 -> - let f1 = abst_form to_constr needA (negb pol0) f0 in - (match is_X f1 with - | Some a -> X (to_constr.mkN a) - | None -> N f1) -| I (f1, o, f2) -> - let f3 = abst_form to_constr needA (negb pol0) f1 in - let f4 = abst_form to_constr needA pol0 f2 in + then abs_or to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> OR + (x, x0, x1)) + else abs_and to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> OR + (x, x0, x1)) + +(** val abst_impl : + ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) + tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> 'a4 option -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> + ('a1, 'a2, 'a3, 'a4) tFormula **) + +let abst_impl to_constr rEC pol0 o k f1 f2 = if pol0 - then abs_or to_constr f3 f4 (mk_arrow o) - else abs_and to_constr f3 f4 (mk_arrow o) + then abs_or to_constr k (rEC (negb pol0) k f1) (rEC pol0 k f2) (mk_arrow o) + else abs_and to_constr k (rEC (negb pol0) k f1) (rEC pol0 k f2) (mk_arrow o) + +(** val or_is_X : + kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> + bool **) + +let or_is_X k f1 f2 = + match is_X k f1 with + | Some _ -> true + | None -> (match is_X k f2 with + | Some _ -> true + | None -> false) + +(** val abs_iff : + ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> + ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, + 'a2, 'a3, 'a4) tFormula -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, + 'a2, 'a3, 'a4) tFormula **) + +let abs_iff to_constr k nf1 ff2 f1 tf2 r def = + if (&&) (or_is_X k nf1 ff2) (or_is_X k f1 tf2) + then X (r, (aformula to_constr r def)) + else def + +(** val abst_iff : + ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, + 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> + ('a1, 'a2, 'a3, 'a4) tFormula **) + +let abst_iff to_constr needA rEC pol0 k f1 f2 = + abs_iff to_constr k (rEC (negb pol0) k f1) (rEC false k f2) (rEC pol0 k f1) + (rEC true k f2) k (IFF (k, (abst_simpl to_constr needA k f1), + (abst_simpl to_constr needA k f2))) + +(** val abst_eq : + ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, + 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> + ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, + 'a2, 'a3, 'a4) tFormula **) + +let abst_eq to_constr needA rEC pol0 f1 f2 = + abs_iff to_constr IsBool (rEC (negb pol0) IsBool f1) (rEC false IsBool f2) + (rEC pol0 IsBool f1) (rEC true IsBool f2) IsProp (EQ + ((abst_simpl to_constr needA IsBool f1), + (abst_simpl to_constr needA IsBool f2))) + +(** val abst_form : + ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> kind -> ('a1, 'a2, + 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **) + +let rec abst_form to_constr needA pol0 _ = function +| TT k -> if pol0 then TT k else X (k, (to_constr.mkTT k)) +| FF k -> if pol0 then X (k, (to_constr.mkFF k)) else FF k +| X (k, p) -> X (k, p) +| A (k, x, t0) -> + if needA t0 then A (k, x, t0) else X (k, (to_constr.mkA k x t0)) +| AND (k0, f1, f2) -> + abst_and to_constr (abst_form to_constr needA) pol0 k0 f1 f2 +| OR (k0, f1, f2) -> + abst_or to_constr (abst_form to_constr needA) pol0 k0 f1 f2 +| NOT (k0, f0) -> + abs_not to_constr k0 (abst_form to_constr needA (negb pol0) k0 f0) + (fun x x0 -> NOT (x, x0)) +| IMPL (k0, f1, o, f2) -> + abst_impl to_constr (abst_form to_constr needA) pol0 o k0 f1 f2 +| IFF (k0, f1, f2) -> + abst_iff to_constr needA (abst_form to_constr needA) pol0 k0 f1 f2 +| EQ (f1, f2) -> + abst_eq to_constr needA (abst_form to_constr needA) pol0 f1 f2 (** val cnf_checker : (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool **) @@ -1421,10 +1667,10 @@ let rec cnf_checker checker f l = (** val tauto_checker : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> - bool) -> ('a1, __, 'a3, unit0) gFormula -> 'a4 list -> bool **) + bool) -> ('a1, rtyp, 'a3, unit0) gFormula -> 'a4 list -> bool **) let tauto_checker unsat deduce normalise1 negate0 checker f w = - cnf_checker checker (xcnf unsat deduce normalise1 negate0 true f) w + cnf_checker checker (xcnf unsat deduce normalise1 negate0 true IsProp f) w (** val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool **) @@ -1969,10 +2215,11 @@ let negate t0 tg = if zunsat f then cnf_tt else cnf_of_list0 tg (xnegate0 f) (** val cnfZ : - (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 list **) + kind -> (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) + cnf * 'a1 list **) -let cnfZ f = - rxcnf zunsat zdeduce normalise0 negate true f +let cnfZ k f = + rxcnf zunsat zdeduce normalise0 negate true k f (** val ceiling : z -> z -> z **) @@ -2178,10 +2425,11 @@ let normQ = qminus qopp qeq_bool (** val cnfQ : - (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) cnf * 'a1 list **) + kind -> (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) + cnf * 'a1 list **) -let cnfQ f = - rxcnf qunsat qdeduce qnormalise qnegate true f +let cnfQ k f = + rxcnf qunsat qdeduce qnormalise qnegate true k f (** val qTautoChecker : q formula bFormula -> qWitness list -> bool **) @@ -2255,4 +2503,5 @@ let rdeduce = let rTautoChecker f w = tauto_checker runsat rdeduce rnormalise rnegate (fun cl -> - rWeakChecker (map fst cl)) (map_bformula (map_Formula q_of_Rcst) f) w + rWeakChecker (map fst cl)) + (map_bformula IsProp (map_Formula q_of_Rcst) f) w diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli index 4200c80574..53f62e0f5b 100644 --- a/plugins/micromega/micromega.mli +++ b/plugins/micromega/micromega.mli @@ -88,6 +88,15 @@ end val zeq_bool : z -> z -> bool +type 'c pExpr = + | PEc of 'c + | PEX of positive + | PEadd of 'c pExpr * 'c pExpr + | PEsub of 'c pExpr * 'c pExpr + | PEmul of 'c pExpr * 'c pExpr + | PEopp of 'c pExpr + | PEpow of 'c pExpr * n + type 'c pol = | Pc of 'c | Pinj of positive * 'c pol @@ -209,15 +218,6 @@ val psquare : -> 'a1 pol -> 'a1 pol -type 'c pExpr = - | PEc of 'c - | PEX of positive - | PEadd of 'c pExpr * 'c pExpr - | PEsub of 'c pExpr * 'c pExpr - | PEmul of 'c pExpr * 'c pExpr - | PEopp of 'c pExpr - | PEpow of 'c pExpr * n - val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol val ppow_pos : @@ -254,29 +254,46 @@ val norm_aux : -> 'a1 pExpr -> 'a1 pol +type kind = IsProp | IsBool + type ('tA, 'tX, 'aA, 'aF) gFormula = - | TT - | FF - | X of 'tX - | A of 'tA * 'aA - | Cj of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula - | D of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula - | N of ('tA, 'tX, 'aA, 'aF) gFormula - | I of - ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option * ('tA, 'tX, 'aA, 'aF) gFormula + | TT of kind + | FF of kind + | X of kind * 'tX + | A of kind * 'tA * 'aA + | AND of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula + | OR of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula + | NOT of kind * ('tA, 'tX, 'aA, 'aF) gFormula + | IMPL of + kind + * ('tA, 'tX, 'aA, 'aF) gFormula + * 'aF option + * ('tA, 'tX, 'aA, 'aF) gFormula + | IFF of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula + | EQ of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula val mapX : - ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula + (kind -> 'a2 -> 'a2) + -> kind + -> ('a1, 'a2, 'a3, 'a4) gFormula + -> ('a1, 'a2, 'a3, 'a4) gFormula + +val foldA : + ('a5 -> 'a3 -> 'a5) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 -val foldA : ('a5 -> 'a3 -> 'a5) -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 val cons_id : 'a1 option -> 'a1 list -> 'a1 list -val ids_of_formula : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list -val collect_annot : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list +val ids_of_formula : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list +val collect_annot : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list -type 'a bFormula = ('a, __, unit0, unit0) gFormula +type rtyp = __ +type eKind = __ +type 'a bFormula = ('a, eKind, unit0, unit0) gFormula val map_bformula : - ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, 'a5) gFormula + kind + -> ('a1 -> 'a2) + -> ('a1, 'a3, 'a4, 'a5) gFormula + -> ('a2, 'a3, 'a4, 'a5) gFormula type ('x, 'annot) clause = ('x * 'annot) list type ('x, 'annot) cnf = ('x, 'annot) clause list @@ -334,12 +351,55 @@ val or_cnf_opt : -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf +val mk_and : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) + -> kind + -> bool + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf + +val mk_or : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) + -> kind + -> bool + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf + +val mk_impl : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) + -> kind + -> bool + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf + +val mk_iff : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) + -> kind + -> bool + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf + +val is_bool : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool option + val xcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool + -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf @@ -387,49 +447,199 @@ val ror_cnf_opt : val ratom : ('a1, 'a2) cnf -> 'a2 -> ('a1, 'a2) cnf * 'a2 list +val rxcnf_and : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> ( bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list) + -> bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list + +val rxcnf_or : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> ( bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list) + -> bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list + +val rxcnf_impl : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> ( bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list) + -> bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list + +val rxcnf_iff : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> ( bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list) + -> bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list + val rxcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool + -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list type ('term, 'annot, 'tX) to_constrT = - { mkTT : 'tX - ; mkFF : 'tX - ; mkA : 'term -> 'annot -> 'tX - ; mkCj : 'tX -> 'tX -> 'tX - ; mkD : 'tX -> 'tX -> 'tX - ; mkI : 'tX -> 'tX -> 'tX - ; mkN : 'tX -> 'tX } + { mkTT : kind -> 'tX + ; mkFF : kind -> 'tX + ; mkA : kind -> 'term -> 'annot -> 'tX + ; mkAND : kind -> 'tX -> 'tX -> 'tX + ; mkOR : kind -> 'tX -> 'tX -> 'tX + ; mkIMPL : kind -> 'tX -> 'tX -> 'tX + ; mkIFF : kind -> 'tX -> 'tX -> 'tX + ; mkNOT : kind -> 'tX -> 'tX + ; mkEQ : 'tX -> 'tX -> 'tX } val aformula : - ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 + ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 -val is_X : ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option +val is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option val abs_and : ('a1, 'a2, 'a3) to_constrT + -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula - -> ( ('a1, 'a2, 'a3, 'a4) tFormula + -> ( kind + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula val abs_or : ('a1, 'a2, 'a3) to_constrT + -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula - -> ( ('a1, 'a2, 'a3, 'a4) tFormula + -> ( kind + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula +val abs_not : + ('a1, 'a2, 'a3) to_constrT + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) + -> ('a1, 'a3, 'a2, 'a4) gFormula + val mk_arrow : 'a4 option + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + +val abst_simpl : + ('a1, 'a2, 'a3) to_constrT + -> ('a2 -> bool) + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + +val abst_and : + ('a1, 'a2, 'a3) to_constrT + -> ( bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula) + -> bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + +val abst_or : + ('a1, 'a2, 'a3) to_constrT + -> ( bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula) + -> bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + +val abst_impl : + ('a1, 'a2, 'a3) to_constrT + -> ( bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula) + -> bool + -> 'a4 option + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + +val or_is_X : + kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool + +val abs_iff : + ('a1, 'a2, 'a3) to_constrT + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + +val abst_iff : + ('a1, 'a2, 'a3) to_constrT + -> ('a2 -> bool) + -> ( bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula) + -> bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + +val abst_eq : + ('a1, 'a2, 'a3) to_constrT + -> ('a2 -> bool) + -> ( bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula) + -> bool -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula @@ -438,8 +648,9 @@ val abst_form : ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula - -> ('a1, 'a3, 'a2, 'a4) gFormula val cnf_checker : (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool @@ -450,7 +661,7 @@ val tauto_checker : -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) - -> ('a1, __, 'a3, unit0) gFormula + -> ('a1, rtyp, 'a3, unit0) gFormula -> 'a4 list -> bool @@ -661,7 +872,9 @@ val xnegate0 : z nFormula -> z nFormula list val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf val cnfZ : - (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 list + kind + -> (z formula, 'a1, 'a2, 'a3) tFormula + -> (z nFormula, 'a1) cnf * 'a1 list val ceiling : z -> z -> z @@ -698,7 +911,9 @@ val qdeduce : q nFormula -> q nFormula -> q nFormula option val normQ : q pExpr -> q pol val cnfQ : - (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) cnf * 'a1 list + kind + -> (q formula, 'a1, 'a2, 'a3) tFormula + -> (q nFormula, 'a1) cnf * 'a1 list val qTautoChecker : q formula bFormula -> qWitness list -> bool diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 41579d5792..fa7b4aa480 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -248,10 +248,12 @@ module EBinOpT = struct source1 : EConstr.t ; source2 : EConstr.t ; source3 : EConstr.t - ; target : EConstr.t - ; inj1 : EInjT.t (* InjTyp source1 target *) - ; inj2 : EInjT.t (* InjTyp source2 target *) - ; inj3 : EInjT.t (* InjTyp source3 target *) + ; target1 : EConstr.t + ; target2 : EConstr.t + ; target3 : EConstr.t + ; inj1 : EInjT.t (* InjTyp source1 target1 *) + ; inj2 : EInjT.t (* InjTyp source2 target2 *) + ; inj3 : EInjT.t (* InjTyp source3 target3 *) ; bop : EConstr.t (* BOP *) ; tbop : EConstr.t (* TBOP *) ; tbopinj : EConstr.t (* TBOpInj *) @@ -272,7 +274,8 @@ module EUnOpT = struct type t = { source1 : EConstr.t ; source2 : EConstr.t - ; target : EConstr.t + ; target1 : EConstr.t + ; target2 : EConstr.t ; uop : EConstr.t ; inj1_t : EInjT.t ; inj2_t : EInjT.t @@ -392,24 +395,26 @@ module EBinOp = struct let table = table let mk_elt evd i a = - let i1 = get_inj evd a.(5) in - let i2 = get_inj evd a.(6) in - let i3 = get_inj evd a.(7) in - let tbop = a.(8) in + let i1 = get_inj evd a.(7) in + let i2 = get_inj evd a.(8) in + let i3 = get_inj evd a.(9) in + let tbop = a.(10) in { source1 = a.(0) ; source2 = a.(1) ; source3 = a.(2) - ; target = a.(3) + ; target1 = a.(3) + ; target2 = a.(4) + ; target3 = a.(5) ; inj1 = i1 ; inj2 = i2 ; inj3 = i3 - ; bop = a.(4) - ; tbop = a.(8) - ; tbopinj = a.(9) + ; bop = a.(6) + ; tbop + ; tbopinj = a.(11) ; classify_binop = - classify_op (mkconvert_binop i1 i2 i3) i1.EInjT.inj a.(4) tbop } + classify_op (mkconvert_binop i1 i2 i3) i3.EInjT.inj a.(6) tbop } - let get_key = 4 + let get_key = 6 let cast x = BinOp x let dest = function BinOp x -> Some x | _ -> None end @@ -452,23 +457,24 @@ module EUnOp = struct let dest = function UnOp x -> Some x | _ -> None let mk_elt evd i a = - let i1 = get_inj evd a.(4) in - let i2 = get_inj evd a.(5) in - let uop = a.(3) in - let tuop = a.(6) in + let i1 = get_inj evd a.(5) in + let i2 = get_inj evd a.(6) in + let uop = a.(4) in + let tuop = a.(7) in { source1 = a.(0) ; source2 = a.(1) - ; target = a.(2) + ; target1 = a.(2) + ; target2 = a.(3) ; uop ; inj1_t = i1 ; inj2_t = i2 ; tuop - ; tuopinj = a.(7) + ; tuopinj = a.(8) ; is_construct = EConstr.isConstruct evd uop - ; classify_unop = classify_op (mkconvert_unop i1 i2) i1.EInjT.inj uop tuop + ; classify_unop = classify_op (mkconvert_unop i1 i2) i2.EInjT.inj uop tuop } - let get_key = 3 + let get_key = 4 end module EBinRel = struct @@ -788,7 +794,8 @@ let app_unop evd src unop arg prf = ( force mkapp , [| unop.source1 ; unop.source2 - ; unop.target + ; unop.target1 + ; unop.target2 ; unop.uop ; unop.inj1_t.EInjT.inj ; unop.inj2_t.EInjT.inj @@ -859,7 +866,9 @@ let app_binop evd src binop arg1 prf1 arg2 prf2 = , [| binop.source1 ; binop.source2 ; binop.source3 - ; binop.target + ; binop.target1 + ; binop.target2 + ; binop.target3 ; binop.bop ; binop.inj1.EInjT.inj ; binop.inj2.EInjT.inj |