summaryrefslogtreecommitdiff
path: root/plugins/micromega/micromega.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/micromega.ml')
-rw-r--r--plugins/micromega/micromega.ml342
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 **)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 04:54:12 +0000