diff options
Diffstat (limited to 'plugins/micromega/micromega.ml')
-rw-r--r-- | plugins/micromega/micromega.ml | 342 |
1 files changed, 153 insertions, 189 deletions
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index 5cf1da8e..52c6ef98 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -1,3 +1,4 @@ + (** val negb : bool -> bool **) let negb = function @@ -34,8 +35,7 @@ module Coq__1 = struct | O -> m | S p -> S (add p m) end -let add = Coq__1.add - +include Coq__1 type positive = | XI of positive @@ -82,11 +82,10 @@ module Coq_Pos = | XI q0 -> XI (add p q0) | XO q0 -> XO (add p q0) | XH -> XI p) - | XH -> - (match y with - | XI q0 -> XO (succ q0) - | XO q0 -> XI q0 - | XH -> XO XH) + | XH -> (match y with + | XI q0 -> XO (succ q0) + | XO q0 -> XI q0 + | XH -> XO XH) (** val add_carry : positive -> positive -> positive **) @@ -154,10 +153,9 @@ module Coq_Pos = | XI q0 -> succ_double_mask (sub_mask_carry p q0) | XO q0 -> double_mask (sub_mask p q0) | XH -> IsPos (pred_double p)) - | XH -> - (match y with - | XH -> IsNul - | _ -> IsNeg) + | XH -> (match y with + | XH -> IsNul + | _ -> IsNeg) (** val sub_mask_carry : positive -> positive -> mask **) @@ -197,8 +195,7 @@ module Coq_Pos = | XO p2 -> S (size_nat p2) | XH -> S O - (** val compare_cont : - comparison -> positive -> positive -> comparison **) + (** val compare_cont : comparison -> positive -> positive -> comparison **) let rec compare_cont r x y = match x with @@ -212,10 +209,9 @@ module Coq_Pos = | XI q0 -> compare_cont Lt p q0 | XO q0 -> compare_cont r p q0 | XH -> Gt) - | XH -> - (match y with - | XH -> r - | _ -> Lt) + | XH -> (match y with + | XH -> r + | _ -> Lt) (** val compare : positive -> positive -> comparison **) @@ -277,14 +273,12 @@ let rec pow_pos rmul x = function let rec nth n0 l default = match n0 with - | O -> - (match l with - | [] -> default - | x::_ -> x) - | S m -> - (match l with - | [] -> default - | _::t0 -> nth m t0 default) + | O -> (match l with + | [] -> default + | x::_ -> x) + | S m -> (match l with + | [] -> default + | _::t0 -> nth m t0 default) (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **) @@ -389,15 +383,13 @@ module Z = let compare x y = match x with - | Z0 -> - (match y with - | Z0 -> Eq - | Zpos _ -> Lt - | Zneg _ -> Gt) - | Zpos x' -> - (match y with - | Zpos y' -> Coq_Pos.compare x' y' - | _ -> Gt) + | Z0 -> (match y with + | Z0 -> Eq + | Zpos _ -> Lt + | Zneg _ -> Gt) + | Zpos x' -> (match y with + | Zpos y' -> Coq_Pos.compare x' y' + | _ -> Gt) | Zneg x' -> (match y with | Zneg y' -> compOpp (Coq_Pos.compare x' y') @@ -533,10 +525,9 @@ let p1 cI = let rec peq ceqb p p' = match p with - | Pc c -> - (match p' with - | Pc c' -> ceqb c c' - | _ -> false) + | Pc c -> (match p' with + | Pc c' -> ceqb c c' + | _ -> false) | Pinj (j, q0) -> (match p' with | Pinj (j', q') -> @@ -568,8 +559,7 @@ let mkPinj_pred j p = | XH -> p (** val mkPX : - 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 - pol **) + 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) let mkPX cO ceqb p i q0 = match p with @@ -631,8 +621,8 @@ let rec paddI cadd pop q0 j = function | XH -> PX (p2, i, (pop q' q0))) (** val psubI : - ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) - -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) + ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> + 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) let rec psubI cadd copp pop q0 j = function | Pc c -> mkPinj j (paddC cadd (popp copp q0) c) @@ -644,13 +634,12 @@ let rec psubI cadd copp pop q0 j = function | PX (p2, i, q') -> (match j with | XI j0 -> PX (p2, i, (psubI cadd copp pop q0 (XO j0) q')) - | XO j0 -> - PX (p2, i, (psubI cadd copp pop q0 (Coq_Pos.pred_double j0) q')) + | XO j0 -> PX (p2, i, (psubI cadd copp pop q0 (Coq_Pos.pred_double j0) q')) | XH -> PX (p2, i, (pop q' q0))) (** val paddX : - 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 - pol -> positive -> 'a1 pol -> 'a1 pol **) + 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol + -> positive -> 'a1 pol -> 'a1 pol **) let rec paddX cO ceqb pop p' i' p = match p with | Pc _ -> PX (p', i', p) @@ -666,16 +655,15 @@ let rec paddX cO ceqb pop p' i' p = match p with | Zneg k -> mkPX cO ceqb (paddX cO ceqb pop p' k p2) i q') (** val psubX : - 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> - 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) + 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 + pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) let rec psubX cO copp ceqb pop p' i' p = match p with | Pc _ -> PX ((popp copp p'), i', p) | Pinj (j, q') -> (match j with | XI j0 -> PX ((popp copp p'), i', (Pinj ((XO j0), q'))) - | XO j0 -> - PX ((popp copp p'), i', (Pinj ((Coq_Pos.pred_double j0), q'))) + | XO j0 -> PX ((popp copp p'), i', (Pinj ((Coq_Pos.pred_double j0), q'))) | XH -> PX ((popp copp p'), i', q')) | PX (p2, i, q') -> (match Z.pos_sub i i' with @@ -684,8 +672,8 @@ let rec psubX cO copp ceqb pop p' i' p = match p with | Zneg k -> mkPX cO ceqb (psubX cO copp ceqb pop p' k p2) i q') (** val padd : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 - pol -> 'a1 pol **) + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol + -> 'a1 pol **) let rec padd cO cadd ceqb p = function | Pc c' -> paddC cadd p c' @@ -703,8 +691,7 @@ let rec padd cO cadd ceqb p = function | PX (p2, i, q0) -> (match Z.pos_sub i i' with | Z0 -> - mkPX cO ceqb (padd cO cadd ceqb p2 p'0) i - (padd cO cadd ceqb q0 q') + mkPX cO ceqb (padd cO cadd ceqb p2 p'0) i (padd cO cadd ceqb q0 q') | Zpos k -> mkPX cO ceqb (padd cO cadd ceqb (PX (p2, k, (p0 cO))) p'0) i' (padd cO cadd ceqb q0 q') @@ -713,8 +700,8 @@ let rec padd cO cadd ceqb p = function (padd cO cadd ceqb q0 q'))) (** val psub : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> - ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 + -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) let rec psub cO cadd csub copp ceqb p = function | Pc c' -> psubC csub p c' @@ -729,39 +716,36 @@ let rec psub cO cadd csub copp ceqb p = function (psub cO cadd csub copp ceqb (Pinj ((XO j0), q0)) q')) | XO j0 -> PX ((popp copp p'0), i', - (psub cO cadd csub copp ceqb (Pinj ((Coq_Pos.pred_double j0), - q0)) q')) - | XH -> - PX ((popp copp p'0), i', (psub cO cadd csub copp ceqb q0 q'))) + (psub cO cadd csub copp ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) + q')) + | XH -> PX ((popp copp p'0), i', (psub cO cadd csub copp ceqb q0 q'))) | PX (p2, i, q0) -> (match Z.pos_sub i i' with | Z0 -> mkPX cO ceqb (psub cO cadd csub copp ceqb p2 p'0) i (psub cO cadd csub copp ceqb q0 q') | Zpos k -> - mkPX cO ceqb - (psub cO cadd csub copp ceqb (PX (p2, k, (p0 cO))) p'0) i' - (psub cO cadd csub copp ceqb q0 q') + mkPX cO ceqb (psub cO cadd csub copp ceqb (PX (p2, k, (p0 cO))) p'0) + i' (psub cO cadd csub copp ceqb q0 q') | Zneg k -> mkPX cO ceqb (psubX cO copp ceqb (psub cO cadd csub copp ceqb) p'0 k p2) i (psub cO cadd csub copp ceqb q0 q'))) (** val pmulC_aux : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 - -> 'a1 pol **) + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> + 'a1 pol **) let rec pmulC_aux cO cmul ceqb p c = match p with | Pc c' -> Pc (cmul c' c) | Pinj (j, q0) -> mkPinj j (pmulC_aux cO cmul ceqb q0 c) | PX (p2, i, q0) -> - mkPX cO ceqb (pmulC_aux cO cmul ceqb p2 c) i - (pmulC_aux cO cmul ceqb q0 c) + mkPX cO ceqb (pmulC_aux cO cmul ceqb p2 c) i (pmulC_aux cO cmul ceqb q0 c) (** val pmulC : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol - -> 'a1 -> 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> + 'a1 -> 'a1 pol **) let pmulC cO cI cmul ceqb p c = if ceqb c cO @@ -769,8 +753,8 @@ let pmulC cO cI cmul ceqb p c = else if ceqb c cI then p else pmulC_aux cO cmul ceqb p c (** val pmulI : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol - -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> + 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) let rec pmulI cO cI cmul ceqb pmul0 q0 j = function | Pc c -> mkPinj j (pmulC cO cI cmul ceqb q0 c) @@ -791,13 +775,12 @@ let rec pmulI cO cI cmul ceqb pmul0 q0 j = function mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 XH p') i' (pmul0 q' q0)) (** val pmul : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> - 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) let rec pmul cO cI cadd cmul ceqb p p'' = match p'' with | Pc c -> pmulC cO cI cmul ceqb p c -| Pinj (j', q') -> - pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' j' p +| Pinj (j', q') -> pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' j' p | PX (p', i', q') -> (match p with | Pc c -> pmulC cO cI cmul ceqb p'' c @@ -806,24 +789,22 @@ let rec pmul cO cI cadd cmul ceqb p p'' = match p'' with match j with | XI j0 -> pmul cO cI cadd cmul ceqb (Pinj ((XO j0), q0)) q' | XO j0 -> - pmul cO cI cadd cmul ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) - q' + pmul cO cI cadd cmul ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) q' | XH -> pmul cO cI cadd cmul ceqb q0 q' in mkPX cO ceqb (pmul cO cI cadd cmul ceqb p p') i' qQ' | PX (p2, i, q0) -> let qQ' = pmul cO cI cadd cmul ceqb q0 q' in - let pQ' = pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' XH p2 - in + let pQ' = pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' XH p2 in let qP' = pmul cO cI cadd cmul ceqb (mkPinj XH q0) p' in let pP' = pmul cO cI cadd cmul ceqb p2 p' in padd cO cadd ceqb - (mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb pP' i (p0 cO)) qP') - i' (p0 cO)) (mkPX cO ceqb pQ' i qQ')) + (mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb pP' i (p0 cO)) qP') i' + (p0 cO)) (mkPX cO ceqb pQ' i qQ')) (** val psquare : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> - 'a1 -> bool) -> 'a1 pol -> 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> bool) -> 'a1 pol -> 'a1 pol **) let rec psquare cO cI cadd cmul ceqb = function | Pc c -> Pc (cmul c c) @@ -852,9 +833,9 @@ let mk_X cO cI j = mkPinj_pred j (mkX cO cI) (** val ppow_pos : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> - 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive - -> 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 + pol **) let rec ppow_pos cO cI cadd cmul ceqb subst_l res p = function | XI p3 -> @@ -868,17 +849,16 @@ let rec ppow_pos cO cI cadd cmul ceqb subst_l res p = function | XH -> subst_l (pmul cO cI cadd cmul ceqb res p) (** val ppow_N : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> - 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol **) let ppow_N cO cI cadd cmul ceqb subst_l p = function | N0 -> p1 cI | Npos p2 -> ppow_pos cO cI cadd cmul ceqb subst_l (p1 cI) p p2 (** val norm_aux : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> - 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> - 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **) let rec norm_aux cO cI cadd cmul csub copp ceqb = function | PEc c -> Pc c @@ -899,8 +879,7 @@ let rec norm_aux cO cI cadd cmul csub copp ceqb = function padd cO cadd ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) (norm_aux cO cI cadd cmul csub copp ceqb pe2))) | PEsub (pe1, pe2) -> - psub cO cadd csub copp ceqb - (norm_aux cO cI cadd cmul csub copp ceqb pe1) + psub cO cadd csub copp ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) (norm_aux cO cI cadd cmul csub copp ceqb pe2) | PEmul (pe1, pe2) -> pmul cO cI cadd cmul ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) @@ -947,8 +926,8 @@ let ff = []::[] (** val add_term : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> - 'a1 clause option **) + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> 'a1 + clause option **) let rec add_term unsat deduce t0 = function | [] -> @@ -969,8 +948,8 @@ let rec add_term unsat deduce t0 = function | None -> None)) (** val or_clause : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 - clause -> 'a1 clause option **) + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 clause + -> 'a1 clause option **) let rec or_clause unsat deduce cl1 cl2 = match cl1 with @@ -981,8 +960,8 @@ let rec or_clause unsat deduce cl1 cl2 = | None -> None) (** val or_clause_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf - -> 'a1 cnf **) + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf -> + 'a1 cnf **) let or_clause_cnf unsat deduce t0 f = fold_right (fun e acc -> @@ -991,8 +970,8 @@ let or_clause_cnf unsat deduce t0 f = | None -> acc) [] f (** val or_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 cnf -> 'a1 cnf -> - 'a1 cnf **) + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 cnf -> 'a1 cnf -> 'a1 + cnf **) let rec or_cnf unsat deduce f f' = match f with @@ -1002,12 +981,12 @@ let rec or_cnf unsat deduce f f' = (** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **) -let and_cnf f1 f2 = - app f1 f2 +let and_cnf = + app (** val xcnf : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> - ('a1 -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf **) + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 + -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf **) let rec xcnf unsat deduce normalise0 negate0 pol0 = function | TT -> if pol0 then tt else ff @@ -1047,9 +1026,9 @@ let rec cnf_checker checker f l = | c::l0 -> if checker e c then cnf_checker checker f0 l0 else false) (** val tauto_checker : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> - ('a1 -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 bFormula -> 'a3 - list -> bool **) + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 + -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 bFormula -> 'a3 list -> + bool **) let tauto_checker unsat deduce normalise0 negate0 checker f w = cnf_checker checker (xcnf unsat deduce normalise0 negate0 true f) w @@ -1085,10 +1064,9 @@ let opMult o o' = | Equal -> Some Equal | NonEqual -> Some NonEqual | _ -> None) - | Strict -> - (match o' with - | NonEqual -> None - | _ -> Some o') + | Strict -> (match o' with + | NonEqual -> None + | _ -> Some o') | NonStrict -> (match o' with | Equal -> Some Equal @@ -1100,14 +1078,12 @@ let opMult o o' = let opAdd o o' = match o with | Equal -> Some o' - | NonEqual -> - (match o' with - | Equal -> Some NonEqual - | _ -> None) - | Strict -> - (match o' with - | NonEqual -> None - | _ -> Some Strict) + | NonEqual -> (match o' with + | Equal -> Some NonEqual + | _ -> None) + | Strict -> (match o' with + | NonEqual -> None + | _ -> Some Strict) | NonStrict -> (match o' with | Equal -> Some NonStrict @@ -1134,15 +1110,14 @@ let map_option f = function let map_option2 f o o' = match o with - | Some x -> - (match o' with - | Some x' -> f x x' - | None -> None) + | Some x -> (match o' with + | Some x' -> f x x' + | None -> None) | None -> None (** val pexpr_times_nformula : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> - 'a1 -> bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option **) let pexpr_times_nformula cO cI cplus ctimes ceqb e = function | ef,o -> @@ -1151,8 +1126,8 @@ let pexpr_times_nformula cO cI cplus ctimes ceqb e = function | _ -> None) (** val nformula_times_nformula : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> - 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option **) let nformula_times_nformula cO cI cplus ctimes ceqb f1 f2 = let e1,o1 = f1 in @@ -1161,8 +1136,8 @@ let nformula_times_nformula cO cI cplus ctimes ceqb f1 f2 = (opMult o1 o2) (** val nformula_plus_nformula : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> - 'a1 nFormula -> 'a1 nFormula option **) + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 + nFormula -> 'a1 nFormula option **) let nformula_plus_nformula cO cplus ceqb f1 f2 = let e1,o1 = f1 in @@ -1170,9 +1145,9 @@ let nformula_plus_nformula cO cplus ceqb f1 f2 = map_option (fun x -> Some ((padd cO cplus ceqb e1 e2),x)) (opAdd o1 o2) (** val eval_Psatz : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> - 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz - -> 'a1 nFormula option **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1 + nFormula option **) let rec eval_Psatz cO cI cplus ctimes ceqb cleb l = function | PsatzIn n0 -> Some (nth n0 l ((Pc cO),Equal)) @@ -1207,9 +1182,8 @@ let check_inconsistent cO ceqb cleb = function | _ -> false) (** val check_normalised_formulas : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> - 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz - -> bool **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool **) let check_normalised_formulas cO cI cplus ctimes ceqb cleb l cm = match eval_Psatz cO cI cplus ctimes ceqb cleb l cm with @@ -1227,31 +1201,30 @@ type op2 = type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr } (** val norm : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> - 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> - 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **) -let norm cO cI cplus ctimes cminus copp ceqb = - norm_aux cO cI cplus ctimes cminus copp ceqb +let norm = + norm_aux (** val psub0 : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> - ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 + -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) -let psub0 cO cplus cminus copp ceqb = - psub cO cplus cminus copp ceqb +let psub0 = + psub (** val padd0 : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 - pol -> 'a1 pol **) + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol + -> 'a1 pol **) -let padd0 cO cplus ceqb = - padd cO cplus ceqb +let padd0 = + padd (** val xnormalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> - 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> - 'a1 nFormula list **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 + nFormula list **) let xnormalise cO cI cplus ctimes cminus copp ceqb t0 = let { flhs = lhs; fop = o; frhs = rhs } = t0 in @@ -1259,11 +1232,9 @@ let xnormalise cO cI cplus ctimes cminus copp ceqb t0 = let rhs0 = norm cO cI cplus ctimes cminus copp ceqb rhs in (match o with | OpEq -> - ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::(((psub0 cO - cplus + ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::(((psub0 cO cplus cminus copp - ceqb rhs0 - lhs0),Strict)::[]) + ceqb rhs0 lhs0),Strict)::[]) | OpNEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Equal)::[] | OpLe -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::[] | OpGe -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),Strict)::[] @@ -1271,17 +1242,17 @@ let xnormalise cO cI cplus ctimes cminus copp ceqb t0 = | OpGt -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),NonStrict)::[]) (** val cnf_normalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> - 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> - 'a1 nFormula cnf **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 + nFormula cnf **) let cnf_normalise cO cI cplus ctimes cminus copp ceqb t0 = map (fun x -> x::[]) (xnormalise cO cI cplus ctimes cminus copp ceqb t0) (** val xnegate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> - 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> - 'a1 nFormula list **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 + nFormula list **) let xnegate cO cI cplus ctimes cminus copp ceqb t0 = let { flhs = lhs; fop = o; frhs = rhs } = t0 in @@ -1290,20 +1261,18 @@ let xnegate cO cI cplus ctimes cminus copp ceqb t0 = (match o with | OpEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Equal)::[] | OpNEq -> - ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::(((psub0 cO - cplus + ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::(((psub0 cO cplus cminus copp - ceqb rhs0 - lhs0),Strict)::[]) + ceqb rhs0 lhs0),Strict)::[]) | OpLe -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),NonStrict)::[] | OpGe -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),NonStrict)::[] | OpLt -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),Strict)::[] | OpGt -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::[]) (** val cnf_negate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> - 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> - 'a1 nFormula cnf **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 + nFormula cnf **) let cnf_negate cO cI cplus ctimes cminus copp ceqb t0 = map (fun x -> x::[]) (xnegate cO cI cplus ctimes cminus copp ceqb t0) @@ -1340,8 +1309,8 @@ let map_Formula c_of_S f = { flhs = (map_PExpr c_of_S l); fop = o; frhs = (map_PExpr c_of_S r) } (** val simpl_cone : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz - -> 'a1 psatz **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz -> + 'a1 psatz **) let simpl_cone cO cI ctimes ceqb e = match e with | PsatzSquare t0 -> @@ -1379,8 +1348,7 @@ let simpl_cone cO cI ctimes ceqb e = match e with | PsatzC p2 -> PsatzMulE ((PsatzC (ctimes c p2)), x) | _ -> if ceqb cI c then t2 else PsatzMulE (t1, t2))) | PsatzAdd (y, z0) -> - PsatzAdd ((PsatzMulE ((PsatzC c), y)), (PsatzMulE ((PsatzC c), - z0))) + PsatzAdd ((PsatzMulE ((PsatzC c), y)), (PsatzMulE ((PsatzC c), z0))) | PsatzC c0 -> PsatzC (ctimes c c0) | PsatzZ -> PsatzZ | _ -> if ceqb cI c then t2 else PsatzMulE (t1, t2)) @@ -1393,10 +1361,9 @@ let simpl_cone cO cI ctimes ceqb e = match e with | PsatzAdd (t1, t2) -> (match t1 with | PsatzZ -> t2 - | _ -> - (match t2 with - | PsatzZ -> t1 - | _ -> PsatzAdd (t1, t2))) + | _ -> (match t2 with + | PsatzZ -> t1 + | _ -> PsatzAdd (t1, t2))) | _ -> e type q = { qnum : z; qden : positive } @@ -1422,8 +1389,7 @@ let qle_bool x y = (** val qplus : q -> q -> q **) let qplus x y = - { qnum = - (Z.add (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))); + { qnum = (Z.add (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))); qden = (Coq_Pos.mul x.qden y.qden) } (** val qmult : q -> q -> q **) @@ -1635,8 +1601,7 @@ let genCuttingPlane = function then None else Some ((makeCuttingPlane e),Equal) | NonEqual -> Some ((e,Z0),op) - | Strict -> - Some ((makeCuttingPlane (psubC Z.sub e (Zpos XH))),NonStrict) + | Strict -> Some ((makeCuttingPlane (psubC Z.sub e (Zpos XH))),NonStrict) | NonStrict -> Some ((makeCuttingPlane e),NonStrict)) (** val nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula **) @@ -1647,10 +1612,9 @@ let nformula_of_cutting_plane = function (** val is_pol_Z0 : z polC -> bool **) let is_pol_Z0 = function -| Pc z0 -> - (match z0 with - | Z0 -> true - | _ -> false) +| Pc z0 -> (match z0 with + | Z0 -> true + | _ -> false) | _ -> false (** val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option **) @@ -1730,8 +1694,8 @@ let qnormalise = (** val qnegate : q formula -> q nFormula cnf **) let qnegate = - cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } - qplus qmult qminus qopp qeq_bool + cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus + qmult qminus qopp qeq_bool (** val qunsat : q nFormula -> bool **) @@ -1789,8 +1753,8 @@ let rnormalise = (** val rnegate : q formula -> q nFormula cnf **) let rnegate = - cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } - qplus qmult qminus qopp qeq_bool + cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus + qmult qminus qopp qeq_bool (** val runsat : q nFormula -> bool **) |