diff options
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/MExtraction.v | 10 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 349 | ||||
| -rw-r--r-- | plugins/micromega/g_micromega.ml4 | 1 | ||||
| -rw-r--r-- | plugins/micromega/micromega.ml | 1809 | ||||
| -rw-r--r-- | plugins/micromega/micromega.mli | 522 | ||||
| -rw-r--r-- | plugins/micromega/vo.itarget | 15 |
6 files changed, 178 insertions, 2528 deletions
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index d28bb82863..4d5c3b1d5b 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -38,17 +38,17 @@ Extract Inductive sumor => option [ Some None ]. Let's rather use the ocaml && *) Extract Inlined Constant andb => "(&&)". -Require Import Reals. +Import Reals.Rdefinitions. -Extract Constant R => "int". -Extract Constant R0 => "0". -Extract Constant R1 => "1". +Extract Constant R => "int". +Extract Constant R0 => "0". +Extract Constant R1 => "1". Extract Constant Rplus => "( + )". Extract Constant Rmult => "( * )". Extract Constant Ropp => "fun x -> - x". Extract Constant Rinv => "fun x -> 1 / x". -Extraction "micromega.ml" +Extraction "plugins/micromega/micromega.ml" List.map simpl_cone (*map_cone indexes*) denorm Qpower vm_add n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 7497aae3ca..fba1966df3 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -16,11 +16,11 @@ (* *) (************************************************************************) +open API open Pp open Mutils open Goptions - -module Term = EConstr +open Names (** * Debug flag @@ -109,8 +109,8 @@ type 'cst atom = 'cst Micromega.formula type 'cst formula = | TT | FF - | X of Term.constr - | A of 'cst atom * tag * Term.constr + | X of EConstr.constr + | A of 'cst atom * tag * EConstr.constr | C of 'cst formula * 'cst formula | D of 'cst formula * 'cst formula | N of 'cst formula @@ -328,9 +328,6 @@ let selecti s m = module M = struct - open Constr - open EConstr - (** * Location of the Coq libraries. *) @@ -602,10 +599,10 @@ struct let get_left_construct sigma term = match EConstr.kind sigma term with - | Constr.Construct((_,i),_) -> (i,[| |]) - | Constr.App(l,rst) -> + | Term.Construct((_,i),_) -> (i,[| |]) + | Term.App(l,rst) -> (match EConstr.kind sigma l with - | Constr.Construct((_,i),_) -> (i,rst) + | Term.Construct((_,i),_) -> (i,rst) | _ -> raise ParseError ) | _ -> raise ParseError @@ -626,7 +623,7 @@ struct let rec dump_nat x = match x with | Mc.O -> Lazy.force coq_O - | Mc.S p -> Term.mkApp(Lazy.force coq_S,[| dump_nat p |]) + | Mc.S p -> EConstr.mkApp(Lazy.force coq_S,[| dump_nat p |]) let rec parse_positive sigma term = let (i,c) = get_left_construct sigma term in @@ -639,28 +636,28 @@ struct let rec dump_positive x = match x with | Mc.XH -> Lazy.force coq_xH - | Mc.XO p -> Term.mkApp(Lazy.force coq_xO,[| dump_positive p |]) - | Mc.XI p -> Term.mkApp(Lazy.force coq_xI,[| dump_positive p |]) + | Mc.XO p -> EConstr.mkApp(Lazy.force coq_xO,[| dump_positive p |]) + | Mc.XI p -> EConstr.mkApp(Lazy.force coq_xI,[| dump_positive p |]) let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x) let dump_n x = match x with | Mc.N0 -> Lazy.force coq_N0 - | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p|]) + | Mc.Npos p -> EConstr.mkApp(Lazy.force coq_Npos,[| dump_positive p|]) let rec dump_index x = match x with | Mc.XH -> Lazy.force coq_xH - | Mc.XO p -> Term.mkApp(Lazy.force coq_xO,[| dump_index p |]) - | Mc.XI p -> Term.mkApp(Lazy.force coq_xI,[| dump_index p |]) + | Mc.XO p -> EConstr.mkApp(Lazy.force coq_xO,[| dump_index p |]) + | Mc.XI p -> EConstr.mkApp(Lazy.force coq_xI,[| dump_index p |]) let pp_index o x = Printf.fprintf o "%i" (CoqToCaml.index x) let pp_n o x = output_string o (string_of_int (CoqToCaml.n x)) let dump_pair t1 t2 dump_t1 dump_t2 (x,y) = - Term.mkApp(Lazy.force coq_pair,[| t1 ; t2 ; dump_t1 x ; dump_t2 y|]) + EConstr.mkApp(Lazy.force coq_pair,[| t1 ; t2 ; dump_t1 x ; dump_t2 y|]) let parse_z sigma term = let (i,c) = get_left_construct sigma term in @@ -673,23 +670,23 @@ struct let dump_z x = match x with | Mc.Z0 ->Lazy.force coq_ZERO - | Mc.Zpos p -> Term.mkApp(Lazy.force coq_POS,[| dump_positive p|]) - | Mc.Zneg p -> Term.mkApp(Lazy.force coq_NEG,[| dump_positive p|]) + | Mc.Zpos p -> EConstr.mkApp(Lazy.force coq_POS,[| dump_positive p|]) + | Mc.Zneg p -> EConstr.mkApp(Lazy.force coq_NEG,[| dump_positive p|]) let pp_z o x = Printf.fprintf o "%s" (Big_int.string_of_big_int (CoqToCaml.z_big_int x)) let dump_num bd1 = - Term.mkApp(Lazy.force coq_Qmake, - [|dump_z (CamlToCoq.bigint (numerator bd1)) ; - dump_positive (CamlToCoq.positive_big_int (denominator bd1)) |]) + EConstr.mkApp(Lazy.force coq_Qmake, + [|dump_z (CamlToCoq.bigint (numerator bd1)) ; + dump_positive (CamlToCoq.positive_big_int (denominator bd1)) |]) let dump_q q = - Term.mkApp(Lazy.force coq_Qmake, - [| dump_z q.Micromega.qnum ; dump_positive q.Micromega.qden|]) + EConstr.mkApp(Lazy.force coq_Qmake, + [| dump_z q.Micromega.qnum ; dump_positive q.Micromega.qden|]) let parse_q sigma term = match EConstr.kind sigma term with - | Constr.App(c, args) -> if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then + | Term.App(c, args) -> if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then {Mc.qnum = parse_z sigma args.(0) ; Mc.qden = parse_positive sigma args.(1) } else raise ParseError | _ -> raise ParseError @@ -712,13 +709,13 @@ struct match cst with | Mc.C0 -> Lazy.force coq_C0 | Mc.C1 -> Lazy.force coq_C1 - | Mc.CQ q -> Term.mkApp(Lazy.force coq_CQ, [| dump_q q |]) - | Mc.CZ z -> Term.mkApp(Lazy.force coq_CZ, [| dump_z z |]) - | Mc.CPlus(x,y) -> Term.mkApp(Lazy.force coq_CPlus, [| dump_Rcst x ; dump_Rcst y |]) - | Mc.CMinus(x,y) -> Term.mkApp(Lazy.force coq_CMinus, [| dump_Rcst x ; dump_Rcst y |]) - | Mc.CMult(x,y) -> Term.mkApp(Lazy.force coq_CMult, [| dump_Rcst x ; dump_Rcst y |]) - | Mc.CInv t -> Term.mkApp(Lazy.force coq_CInv, [| dump_Rcst t |]) - | Mc.COpp t -> Term.mkApp(Lazy.force coq_COpp, [| dump_Rcst t |]) + | Mc.CQ q -> EConstr.mkApp(Lazy.force coq_CQ, [| dump_q q |]) + | Mc.CZ z -> EConstr.mkApp(Lazy.force coq_CZ, [| dump_z z |]) + | Mc.CPlus(x,y) -> EConstr.mkApp(Lazy.force coq_CPlus, [| dump_Rcst x ; dump_Rcst y |]) + | Mc.CMinus(x,y) -> EConstr.mkApp(Lazy.force coq_CMinus, [| dump_Rcst x ; dump_Rcst y |]) + | Mc.CMult(x,y) -> EConstr.mkApp(Lazy.force coq_CMult, [| dump_Rcst x ; dump_Rcst y |]) + | Mc.CInv t -> EConstr.mkApp(Lazy.force coq_CInv, [| dump_Rcst t |]) + | Mc.COpp t -> EConstr.mkApp(Lazy.force coq_COpp, [| dump_Rcst t |]) let rec parse_Rcst sigma term = let (i,c) = get_left_construct sigma term in @@ -745,8 +742,8 @@ struct let rec dump_list typ dump_elt l = match l with - | [] -> Term.mkApp(Lazy.force coq_nil,[| typ |]) - | e :: l -> Term.mkApp(Lazy.force coq_cons, + | [] -> EConstr.mkApp(Lazy.force coq_nil,[| typ |]) + | e :: l -> EConstr.mkApp(Lazy.force coq_cons, [| typ; dump_elt e;dump_list typ dump_elt l|]) let pp_list op cl elt o l = @@ -776,27 +773,27 @@ struct let dump_expr typ dump_z e = let rec dump_expr e = match e with - | Mc.PEX n -> mkApp(Lazy.force coq_PEX,[| typ; dump_var n |]) - | Mc.PEc z -> mkApp(Lazy.force coq_PEc,[| typ ; dump_z z |]) - | Mc.PEadd(e1,e2) -> mkApp(Lazy.force coq_PEadd, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEsub(e1,e2) -> mkApp(Lazy.force coq_PEsub, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEopp e -> mkApp(Lazy.force coq_PEopp, - [| typ; dump_expr e|]) - | Mc.PEmul(e1,e2) -> mkApp(Lazy.force coq_PEmul, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEpow(e,n) -> mkApp(Lazy.force coq_PEpow, - [| typ; dump_expr e; dump_n n|]) + | Mc.PEX n -> EConstr.mkApp(Lazy.force coq_PEX,[| typ; dump_var n |]) + | Mc.PEc z -> EConstr.mkApp(Lazy.force coq_PEc,[| typ ; dump_z z |]) + | Mc.PEadd(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEadd, + [| typ; dump_expr e1;dump_expr e2|]) + | Mc.PEsub(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEsub, + [| typ; dump_expr e1;dump_expr e2|]) + | Mc.PEopp e -> EConstr.mkApp(Lazy.force coq_PEopp, + [| typ; dump_expr e|]) + | Mc.PEmul(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEmul, + [| typ; dump_expr e1;dump_expr e2|]) + | Mc.PEpow(e,n) -> EConstr.mkApp(Lazy.force coq_PEpow, + [| typ; dump_expr e; dump_n n|]) in dump_expr e let dump_pol typ dump_c e = let rec dump_pol e = match e with - | Mc.Pc n -> mkApp(Lazy.force coq_Pc, [|typ ; dump_c n|]) - | Mc.Pinj(p,pol) -> mkApp(Lazy.force coq_Pinj , [| typ ; dump_positive p ; dump_pol pol|]) - | Mc.PX(pol1,p,pol2) -> mkApp(Lazy.force coq_PX, [| typ ; dump_pol pol1 ; dump_positive p ; dump_pol pol2|]) in + | Mc.Pc n -> EConstr.mkApp(Lazy.force coq_Pc, [|typ ; dump_c n|]) + | Mc.Pinj(p,pol) -> EConstr.mkApp(Lazy.force coq_Pinj , [| typ ; dump_positive p ; dump_pol pol|]) + | Mc.PX(pol1,p,pol2) -> EConstr.mkApp(Lazy.force coq_PX, [| typ ; dump_pol pol1 ; dump_positive p ; dump_pol pol2|]) in dump_pol e let pp_pol pp_c o e = @@ -815,17 +812,17 @@ struct let z = Lazy.force typ in let rec dump_cone e = match e with - | Mc.PsatzIn n -> mkApp(Lazy.force coq_PsatzIn,[| z; dump_nat n |]) - | Mc.PsatzMulC(e,c) -> mkApp(Lazy.force coq_PsatzMultC, - [| z; dump_pol z dump_z e ; dump_cone c |]) - | Mc.PsatzSquare e -> mkApp(Lazy.force coq_PsatzSquare, - [| z;dump_pol z dump_z e|]) - | Mc.PsatzAdd(e1,e2) -> mkApp(Lazy.force coq_PsatzAdd, - [| z; dump_cone e1; dump_cone e2|]) - | Mc.PsatzMulE(e1,e2) -> mkApp(Lazy.force coq_PsatzMulE, - [| z; dump_cone e1; dump_cone e2|]) - | Mc.PsatzC p -> mkApp(Lazy.force coq_PsatzC,[| z; dump_z p|]) - | Mc.PsatzZ -> mkApp( Lazy.force coq_PsatzZ,[| z|]) in + | Mc.PsatzIn n -> EConstr.mkApp(Lazy.force coq_PsatzIn,[| z; dump_nat n |]) + | Mc.PsatzMulC(e,c) -> EConstr.mkApp(Lazy.force coq_PsatzMultC, + [| z; dump_pol z dump_z e ; dump_cone c |]) + | Mc.PsatzSquare e -> EConstr.mkApp(Lazy.force coq_PsatzSquare, + [| z;dump_pol z dump_z e|]) + | Mc.PsatzAdd(e1,e2) -> EConstr.mkApp(Lazy.force coq_PsatzAdd, + [| z; dump_cone e1; dump_cone e2|]) + | Mc.PsatzMulE(e1,e2) -> EConstr.mkApp(Lazy.force coq_PsatzMulE, + [| z; dump_cone e1; dump_cone e2|]) + | Mc.PsatzC p -> EConstr.mkApp(Lazy.force coq_PsatzC,[| z; dump_z p|]) + | Mc.PsatzZ -> EConstr.mkApp(Lazy.force coq_PsatzZ,[| z|]) in dump_cone e let pp_psatz pp_z o e = @@ -868,10 +865,10 @@ struct Printf.fprintf o"(%a %a %a)" (pp_expr pp_z) l pp_op op (pp_expr pp_z) r let dump_cstr typ dump_constant {Mc.flhs = e1 ; Mc.fop = o ; Mc.frhs = e2} = - Term.mkApp(Lazy.force coq_Build, - [| typ; dump_expr typ dump_constant e1 ; - dump_op o ; - dump_expr typ dump_constant e2|]) + EConstr.mkApp(Lazy.force coq_Build, + [| typ; dump_expr typ dump_constant e1 ; + dump_op o ; + dump_expr typ dump_constant e2|]) let assoc_const sigma x l = try @@ -905,8 +902,8 @@ struct let parse_zop gl (op,args) = let sigma = gl.sigma in match EConstr.kind sigma op with - | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1)) - | Ind((n,0),_) -> + | Term.Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1)) + | Term.Ind((n,0),_) -> if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_Z) then (Mc.OpEq, args.(1), args.(2)) else raise ParseError @@ -915,8 +912,8 @@ struct let parse_rop gl (op,args) = let sigma = gl.sigma in match EConstr.kind sigma op with - | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1)) - | Ind((n,0),_) -> + | Term.Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1)) + | Term.Ind((n,0),_) -> if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_R) then (Mc.OpEq, args.(1), args.(2)) else raise ParseError @@ -927,7 +924,7 @@ struct let is_constant sigma t = (* This is an approx *) match EConstr.kind sigma t with - | Construct(i,_) -> true + | Term.Construct(i,_) -> true | _ -> false type 'a op = @@ -948,14 +945,14 @@ struct module Env = struct - type t = constr list + type t = EConstr.constr list let compute_rank_add env sigma v = let rec _add env n v = match env with | [] -> ([v],n) | e::l -> - if eq_constr sigma e v + if EConstr.eq_constr sigma e v then (env,n) else let (env,n) = _add l ( n+1) v in @@ -969,7 +966,7 @@ struct match env with | [] -> raise (Invalid_argument "get_rank") | e::l -> - if eq_constr sigma e v + if EConstr.eq_constr sigma e v then n else _get_rank l (n+1) in _get_rank env 1 @@ -1010,10 +1007,10 @@ struct try (Mc.PEc (parse_constant term) , env) with ParseError -> match EConstr.kind sigma term with - | App(t,args) -> + | Term.App(t,args) -> ( match EConstr.kind sigma t with - | Const c -> + | Term.Const c -> ( match assoc_ops sigma t ops_spec with | Binop f -> combine env f (args.(0),args.(1)) | Opp -> let (expr,env) = parse_expr env args.(0) in @@ -1076,13 +1073,13 @@ struct let rec rconstant sigma term = match EConstr.kind sigma term with - | Const x -> + | Term.Const x -> if EConstr.eq_constr sigma term (Lazy.force coq_R0) then Mc.C0 else if EConstr.eq_constr sigma term (Lazy.force coq_R1) then Mc.C1 else raise ParseError - | App(op,args) -> + | Term.App(op,args) -> begin try (* the evaluation order is important in the following *) @@ -1151,7 +1148,7 @@ struct if debug then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ()); match EConstr.kind sigma cstr with - | App(op,args) -> + | Term.App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in let (e1,env) = parse_expr sigma env lhs in let (e2,env) = parse_expr sigma env rhs in @@ -1206,29 +1203,29 @@ struct let rec xparse_formula env tg term = match EConstr.kind sigma term with - | App(l,rst) -> + | Term.App(l,rst) -> (match rst with - | [|a;b|] when eq_constr sigma l (Lazy.force coq_and) -> + | [|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 eq_constr sigma l (Lazy.force coq_or) -> + | [|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 eq_constr sigma l (Lazy.force coq_not) -> + | [|a|] when EConstr.eq_constr sigma l (Lazy.force coq_not) -> let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg) - | [|a;b|] when eq_constr sigma l (Lazy.force coq_iff) -> + | [|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) - | Prod(typ,a,b) when Vars.noccurn sigma 1 b -> + | Term.Prod(typ,a,b) when 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 eq_constr sigma term (Lazy.force coq_True) -> (TT,env,tg) - | _ when eq_constr sigma term (Lazy.force coq_False) -> (FF,env,tg) + | _ when EConstr.eq_constr sigma term (Lazy.force coq_True) -> (TT,env,tg) + | _ when EConstr.eq_constr sigma term (Lazy.force coq_False) -> (FF,env,tg) | _ when is_prop term -> X(term),env,tg | _ -> raise ParseError in @@ -1237,14 +1234,14 @@ struct let dump_formula typ dump_atom f = let rec xdump f = match f with - | TT -> mkApp(Lazy.force coq_TT,[|typ|]) - | FF -> mkApp(Lazy.force coq_FF,[|typ|]) - | C(x,y) -> mkApp(Lazy.force coq_And,[|typ ; xdump x ; xdump y|]) - | D(x,y) -> mkApp(Lazy.force coq_Or,[|typ ; xdump x ; xdump y|]) - | I(x,_,y) -> mkApp(Lazy.force coq_Impl,[|typ ; xdump x ; xdump y|]) - | N(x) -> mkApp(Lazy.force coq_Neg,[|typ ; xdump x|]) - | A(x,_,_) -> mkApp(Lazy.force coq_Atom,[|typ ; dump_atom x|]) - | X(t) -> mkApp(Lazy.force coq_X,[|typ ; t|]) in + | TT -> EConstr.mkApp(Lazy.force coq_TT,[|typ|]) + | FF -> EConstr.mkApp(Lazy.force coq_FF,[|typ|]) + | C(x,y) -> EConstr.mkApp(Lazy.force coq_And,[|typ ; xdump x ; xdump y|]) + | D(x,y) -> EConstr.mkApp(Lazy.force coq_Or,[|typ ; xdump x ; xdump y|]) + | I(x,_,y) -> EConstr.mkApp(Lazy.force coq_Impl,[|typ ; xdump x ; xdump y|]) + | N(x) -> EConstr.mkApp(Lazy.force coq_Neg,[|typ ; xdump x|]) + | A(x,_,_) -> EConstr.mkApp(Lazy.force coq_Atom,[|typ ; dump_atom x|]) + | X(t) -> EConstr.mkApp(Lazy.force coq_X,[|typ ; t|]) in xdump f @@ -1284,15 +1281,15 @@ struct type 'cst dump_expr = (* 'cst is the type of the syntactic constants *) { - interp_typ : constr; - dump_cst : 'cst -> constr; - dump_add : constr; - dump_sub : constr; - dump_opp : constr; - dump_mul : constr; - dump_pow : constr; - dump_pow_arg : Mc.n -> constr; - dump_op : (Mc.op2 * Term.constr) list + interp_typ : EConstr.constr; + dump_cst : 'cst -> EConstr.constr; + dump_add : EConstr.constr; + dump_sub : EConstr.constr; + dump_opp : EConstr.constr; + dump_mul : EConstr.constr; + dump_pow : EConstr.constr; + dump_pow_arg : Mc.n -> EConstr.constr; + dump_op : (Mc.op2 * EConstr.constr) list } let dump_zexpr = lazy @@ -1326,8 +1323,8 @@ let dump_qexpr = lazy let add = Lazy.force coq_Rplus in let one = Lazy.force coq_R1 in - let mk_add x y = mkApp(add,[|x;y|]) in - let mk_mult x y = mkApp(mult,[|x;y|]) in + let mk_add x y = EConstr.mkApp(add,[|x;y|]) in + let mk_mult x y = EConstr.mkApp(mult,[|x;y|]) in let two = mk_add one one in @@ -1350,13 +1347,13 @@ let rec dump_Rcst_as_R cst = match cst with | Mc.C0 -> Lazy.force coq_R0 | Mc.C1 -> Lazy.force coq_R1 - | Mc.CQ q -> Term.mkApp(Lazy.force coq_IQR, [| dump_q q |]) - | Mc.CZ z -> Term.mkApp(Lazy.force coq_IZR, [| dump_z z |]) - | Mc.CPlus(x,y) -> Term.mkApp(Lazy.force coq_Rplus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) - | Mc.CMinus(x,y) -> Term.mkApp(Lazy.force coq_Rminus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) - | Mc.CMult(x,y) -> Term.mkApp(Lazy.force coq_Rmult, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) - | Mc.CInv t -> Term.mkApp(Lazy.force coq_Rinv, [| dump_Rcst_as_R t |]) - | Mc.COpp t -> Term.mkApp(Lazy.force coq_Ropp, [| dump_Rcst_as_R t |]) + | Mc.CQ q -> EConstr.mkApp(Lazy.force coq_IQR, [| dump_q q |]) + | Mc.CZ z -> EConstr.mkApp(Lazy.force coq_IZR, [| dump_z z |]) + | Mc.CPlus(x,y) -> EConstr.mkApp(Lazy.force coq_Rplus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) + | Mc.CMinus(x,y) -> EConstr.mkApp(Lazy.force coq_Rminus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) + | Mc.CMult(x,y) -> EConstr.mkApp(Lazy.force coq_Rmult, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) + | Mc.CInv t -> EConstr.mkApp(Lazy.force coq_Rinv, [| dump_Rcst_as_R t |]) + | Mc.COpp t -> EConstr.mkApp(Lazy.force coq_Ropp, [| dump_Rcst_as_R t |]) let dump_rexpr = lazy @@ -1385,7 +1382,7 @@ let dump_rexpr = lazy let prodn n env b = let rec prodrec = function | (0, env, b) -> b - | (n, ((v,t)::l), b) -> prodrec (n-1, l, mkProd (v,t,b)) + | (n, ((v,t)::l), b) -> prodrec (n-1, l, EConstr.mkProd (v,t,b)) | _ -> assert false in prodrec (n,env,b) @@ -1399,32 +1396,32 @@ let make_goal_of_formula sigma dexpr form = let props = prop_env_of_formula sigma form in - let vars_n = List.map (fun (_,i) -> (Names.id_of_string (Printf.sprintf "__x%i" i)) , dexpr.interp_typ) vars_idx in - let props_n = List.mapi (fun i _ -> (Names.id_of_string (Printf.sprintf "__p%i" (i+1))) , Term.mkProp) props in + let vars_n = List.map (fun (_,i) -> (Names.Id.of_string (Printf.sprintf "__x%i" i)) , dexpr.interp_typ) vars_idx in + let props_n = List.mapi (fun i _ -> (Names.Id.of_string (Printf.sprintf "__p%i" (i+1))) , EConstr.mkProp) props in let var_name_pos = List.map2 (fun (idx,_) (id,_) -> id,idx) vars_idx vars_n in let dump_expr i e = let rec dump_expr = function - | Mc.PEX n -> mkRel (i+(List.assoc (CoqToCaml.positive n) vars_idx)) + | Mc.PEX n -> EConstr.mkRel (i+(List.assoc (CoqToCaml.positive n) vars_idx)) | Mc.PEc z -> dexpr.dump_cst z - | Mc.PEadd(e1,e2) -> mkApp(dexpr.dump_add, + | Mc.PEadd(e1,e2) -> EConstr.mkApp(dexpr.dump_add, [| dump_expr e1;dump_expr e2|]) - | Mc.PEsub(e1,e2) -> mkApp(dexpr.dump_sub, + | Mc.PEsub(e1,e2) -> EConstr.mkApp(dexpr.dump_sub, [| dump_expr e1;dump_expr e2|]) - | Mc.PEopp e -> mkApp(dexpr.dump_opp, - [| dump_expr e|]) - | Mc.PEmul(e1,e2) -> mkApp(dexpr.dump_mul, - [| dump_expr e1;dump_expr e2|]) - | Mc.PEpow(e,n) -> mkApp(dexpr.dump_pow, - [| dump_expr e; dexpr.dump_pow_arg n|]) + | Mc.PEopp e -> EConstr.mkApp(dexpr.dump_opp, + [| dump_expr e|]) + | Mc.PEmul(e1,e2) -> EConstr.mkApp(dexpr.dump_mul, + [| dump_expr e1;dump_expr e2|]) + | Mc.PEpow(e,n) -> EConstr.mkApp(dexpr.dump_pow, + [| dump_expr e; dexpr.dump_pow_arg n|]) in dump_expr e in let mkop op e1 e2 = try - Term.mkApp(List.assoc op dexpr.dump_op, [| e1; e2|]) + EConstr.mkApp(List.assoc op dexpr.dump_op, [| e1; e2|]) with Not_found -> - Term.mkApp(Lazy.force coq_Eq,[|dexpr.interp_typ ; e1 ;e2|]) in + 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) in @@ -1433,13 +1430,13 @@ let make_goal_of_formula sigma dexpr form = match f with | TT -> Lazy.force coq_True | FF -> Lazy.force coq_False - | C(x,y) -> mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|]) - | D(x,y) -> mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|]) - | I(x,_,y) -> mkArrow (xdump pi xi x) (xdump (pi+1) (xi+1) y) - | N(x) -> mkArrow (xdump pi xi x) (Lazy.force coq_False) + | C(x,y) -> EConstr.mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|]) + | D(x,y) -> EConstr.mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|]) + | I(x,_,y) -> EConstr.mkArrow (xdump pi xi x) (xdump (pi+1) (xi+1) y) + | N(x) -> EConstr.mkArrow (xdump pi xi x) (Lazy.force coq_False) | A(x,_,_) -> dump_cstr xi x | X(t) -> let idx = Env.get_rank props sigma t in - mkRel (pi+idx) in + EConstr.mkRel (pi+idx) in let nb_vars = List.length vars_n in let nb_props = List.length props_n in @@ -1448,12 +1445,12 @@ let make_goal_of_formula sigma dexpr form = let subst_prop p = let idx = Env.get_rank props sigma p in - mkVar (Names.id_of_string (Printf.sprintf "__p%i" idx)) in + EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx)) in let form' = map_prop subst_prop form in - (prodn nb_props (List.map (fun (x,y) -> Names.Name x,y) props_n) - (prodn nb_vars (List.map (fun (x,y) -> Names.Name x,y) vars_n) + (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)), List.rev props_n, List.rev var_name_pos,form') @@ -1468,7 +1465,7 @@ let make_goal_of_formula sigma dexpr form = | [] -> acc | (e::l) -> let (name,expr,typ) = e in - xset (Term.mkNamedLetIn + xset (EConstr.mkNamedLetIn (Names.Id.of_string name) expr typ acc) l in xset concl l @@ -1544,10 +1541,10 @@ let coq_VarMap = let rec dump_varmap typ m = match m with - | Mc.Empty -> Term.mkApp(Lazy.force coq_Empty,[| typ |]) - | Mc.Leaf v -> Term.mkApp(Lazy.force coq_Leaf,[| typ; v|]) + | Mc.Empty -> EConstr.mkApp(Lazy.force coq_Empty,[| typ |]) + | Mc.Leaf v -> EConstr.mkApp(Lazy.force coq_Leaf,[| typ; v|]) | Mc.Node(l,o,r) -> - Term.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |]) + EConstr.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |]) let vm_of_list env = @@ -1569,15 +1566,15 @@ let rec pp_varmap o vm = let rec dump_proof_term = function | Micromega.DoneProof -> Lazy.force coq_doneProof | Micromega.RatProof(cone,rst) -> - Term.mkApp(Lazy.force coq_ratProof, [| dump_psatz coq_Z dump_z cone; dump_proof_term rst|]) + EConstr.mkApp(Lazy.force coq_ratProof, [| dump_psatz coq_Z dump_z cone; dump_proof_term rst|]) | Micromega.CutProof(cone,prf) -> - Term.mkApp(Lazy.force coq_cutProof, + EConstr.mkApp(Lazy.force coq_cutProof, [| dump_psatz coq_Z dump_z cone ; dump_proof_term prf|]) | Micromega.EnumProof(c1,c2,prfs) -> - Term.mkApp (Lazy.force coq_enumProof, - [| dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ; - dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |]) + EConstr.mkApp (Lazy.force coq_enumProof, + [| dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ; + dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |]) let rec size_of_psatz = function @@ -1637,11 +1634,11 @@ let parse_goal gl parse_arith env hyps term = * The datastructures that aggregate theory-dependent proof values. *) type ('synt_c, 'prf) domain_spec = { - typ : Term.constr; (* is the type of the interpretation domain - Z, Q, R*) - coeff : Term.constr ; (* is the type of the syntactic coeffs - Z , Q , Rcst *) - dump_coeff : 'synt_c -> Term.constr ; - proof_typ : Term.constr ; - dump_proof : 'prf -> Term.constr + typ : EConstr.constr; (* is the type of the interpretation domain - Z, Q, R*) + coeff : EConstr.constr ; (* is the type of the syntactic coeffs - Z , Q , Rcst *) + dump_coeff : 'synt_c -> EConstr.constr ; + proof_typ : EConstr.constr ; + dump_proof : 'prf -> EConstr.constr } let zz_domain_spec = lazy { @@ -1668,8 +1665,6 @@ let rcst_domain_spec = lazy { dump_proof = dump_psatz coq_Q dump_q } -open Proofview.Notations - (** Naive topological sort of constr according to the subterm-ordering *) (* An element is minimal x is minimal w.r.t y if @@ -1708,23 +1703,23 @@ let topo_sort_constr l = let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*) = (* let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *) - let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in + let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in let vm = dump_varmap (spec.typ) (vm_of_list env) in (* todo : directly generate the proof term - or generalize before conversion? *) - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> Tacticals.New.tclTHENLIST [ Tactics.change_concl (set [ - ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); - ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|])); + ("__ff", ff, EConstr.mkApp(Lazy.force coq_Formula, [|formula_typ |])); + ("__varmap", vm, EConstr.mkApp(Lazy.force coq_VarMap, [|spec.typ|])); ("__wit", cert, cert_typ) ] (Tacmach.New.pf_concl gl)) ] - end } + end (** @@ -1843,20 +1838,20 @@ let abstract_formula hyps f = | A(a,t,term) -> if TagSet.mem t hyps then A(a,t,term) else X(term) | C(f1,f2) -> (match xabs f1 , xabs f2 with - | X a1 , X a2 -> X (Term.mkApp(Lazy.force coq_and, [|a1;a2|])) + | X a1 , X a2 -> X (EConstr.mkApp(Lazy.force coq_and, [|a1;a2|])) | f1 , f2 -> C(f1,f2) ) | D(f1,f2) -> (match xabs f1 , xabs f2 with - | X a1 , X a2 -> X (Term.mkApp(Lazy.force coq_or, [|a1;a2|])) + | X a1 , X a2 -> X (EConstr.mkApp(Lazy.force coq_or, [|a1;a2|])) | f1 , f2 -> D(f1,f2) ) | N(f) -> (match xabs f with - | X a -> X (Term.mkApp(Lazy.force coq_not, [|a|])) + | X a -> X (EConstr.mkApp(Lazy.force coq_not, [|a|])) | f -> N f) | I(f1,hyp,f2) -> (match xabs f1 , hyp, xabs f2 with | X a1 , Some _ , af2 -> af2 - | X a1 , None , X a2 -> X (Term.mkArrow a1 a2) + | X a1 , None , X a2 -> X (EConstr.mkArrow a1 a2) | af1 , _ , af2 -> I(af1,hyp,af2) ) | FF -> FF @@ -1910,7 +1905,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 if debug then begin Feedback.msg_notice (Pp.str "Formula....\n") ; - let formula_typ = (Term.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in + let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.typ spec.dump_coeff) ff in Feedback.msg_notice (Printer.pr_leconstr ff); @@ -1935,7 +1930,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 if debug then begin Feedback.msg_notice (Pp.str "\nAFormula\n") ; - let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in + let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in let ff' = dump_formula formula_typ (dump_cstr spec.typ spec.dump_coeff) ff' in Feedback.msg_notice (Printer.pr_leconstr ff'); @@ -1972,7 +1967,7 @@ let micromega_gen (normalise:'cst atom -> 'cst mc_cnf) unsat deduce spec dumpexpr prover tac = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in @@ -1993,11 +1988,11 @@ let micromega_gen let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in - let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in + let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; micromega_order_change spec res' - (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env' ff_arith ] in + (EConstr.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env' ff_arith ] in let goal_props = List.rev (prop_env_of_formula sigma ff') in @@ -2016,8 +2011,8 @@ let micromega_gen [ kill_arith; (Tacticals.New.tclTHENLIST - [(Tactics.generalize (List.map Term.mkVar ids)); - Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args)) + [(Tactics.generalize (List.map EConstr.mkVar ids)); + Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args)) ] ) ] with @@ -2029,7 +2024,7 @@ let micromega_gen ^ "the use of a specialized external tool called csdp. \n\n" ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) - end } + end let micromega_gen parse_arith (negate:'cst atom -> 'cst mc_cnf) @@ -2045,19 +2040,19 @@ let micromega_order_changer cert env ff = let coeff = Lazy.force coq_Rcst in let dump_coeff = dump_Rcst in let typ = Lazy.force coq_R in - let cert_typ = (Term.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in + let cert_typ = (EConstr.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in - let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in + let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[| coeff|])) in let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) (vm_of_list env) in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> Tacticals.New.tclTHENLIST [ (Tactics.change_concl (set [ - ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); - ("__varmap", vm, Term.mkApp + ("__ff", ff, EConstr.mkApp(Lazy.force coq_Formula, [|formula_typ |])); + ("__varmap", vm, EConstr.mkApp (gen_constant_in_modules "VarMap" [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|])); ("__wit", cert, cert_typ) @@ -2065,7 +2060,7 @@ let micromega_order_changer cert env ff = (Tacmach.New.pf_concl gl))); (* Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)*) ] - end } + end let micromega_genr prover tac = let parse_arith = parse_rarith in @@ -2080,7 +2075,7 @@ let micromega_genr prover tac = proof_typ = Lazy.force coq_QWitness ; dump_proof = dump_psatz coq_Q dump_q } in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in @@ -2108,7 +2103,7 @@ let micromega_genr prover tac = let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in - let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in + let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; micromega_order_changer res' env' ff_arith ] in @@ -2130,8 +2125,8 @@ let micromega_genr prover tac = [ kill_arith; (Tacticals.New.tclTHENLIST - [(Tactics.generalize (List.map Term.mkVar ids)); - Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args)) + [(Tactics.generalize (List.map EConstr.mkVar ids)); + Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args)) ] ) ] @@ -2144,7 +2139,7 @@ let micromega_genr prover tac = ^ "the use of a specialized external tool called csdp. \n\n" ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) - end } + end diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index ccb6daa116..d803c75549 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -16,6 +16,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open API open Ltac_plugin open Stdarg open Tacarg diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml deleted file mode 100644 index 5cf1da8ea8..0000000000 --- a/plugins/micromega/micromega.ml +++ /dev/null @@ -1,1809 +0,0 @@ -(** val negb : bool -> bool **) - -let negb = function -| true -> false -| false -> true - -type nat = -| O -| S of nat - -(** val app : 'a1 list -> 'a1 list -> 'a1 list **) - -let rec app l m = - match l with - | [] -> m - | a::l1 -> a::(app l1 m) - -type comparison = -| Eq -| Lt -| Gt - -(** val compOpp : comparison -> comparison **) - -let compOpp = function -| Eq -> Eq -| Lt -> Gt -| Gt -> Lt - -module Coq__1 = struct - (** val add : nat -> nat -> nat **) - let rec add n0 m = - match n0 with - | O -> m - | S p -> S (add p m) -end -let add = Coq__1.add - - -type positive = -| XI of positive -| XO of positive -| XH - -type n = -| N0 -| Npos of positive - -type z = -| Z0 -| Zpos of positive -| Zneg of positive - -module Pos = - struct - type mask = - | IsNul - | IsPos of positive - | IsNeg - end - -module Coq_Pos = - struct - (** val succ : positive -> positive **) - - let rec succ = function - | XI p -> XO (succ p) - | XO p -> XI p - | XH -> XO XH - - (** val add : positive -> positive -> positive **) - - let rec add x y = - match x with - | XI p -> - (match y with - | XI q0 -> XO (add_carry p q0) - | XO q0 -> XI (add p q0) - | XH -> XO (succ p)) - | XO p -> - (match y with - | 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) - - (** val add_carry : positive -> positive -> positive **) - - and add_carry x y = - match x with - | XI p -> - (match y with - | XI q0 -> XI (add_carry p q0) - | XO q0 -> XO (add_carry p q0) - | XH -> XI (succ p)) - | XO p -> - (match y with - | XI q0 -> XO (add_carry p q0) - | XO q0 -> XI (add p q0) - | XH -> XO (succ p)) - | XH -> - (match y with - | XI q0 -> XI (succ q0) - | XO q0 -> XO (succ q0) - | XH -> XI XH) - - (** val pred_double : positive -> positive **) - - let rec pred_double = function - | XI p -> XI (XO p) - | XO p -> XI (pred_double p) - | XH -> XH - - type mask = Pos.mask = - | IsNul - | IsPos of positive - | IsNeg - - (** val succ_double_mask : mask -> mask **) - - let succ_double_mask = function - | IsNul -> IsPos XH - | IsPos p -> IsPos (XI p) - | IsNeg -> IsNeg - - (** val double_mask : mask -> mask **) - - let double_mask = function - | IsPos p -> IsPos (XO p) - | x0 -> x0 - - (** val double_pred_mask : positive -> mask **) - - let double_pred_mask = function - | XI p -> IsPos (XO (XO p)) - | XO p -> IsPos (XO (pred_double p)) - | XH -> IsNul - - (** val sub_mask : positive -> positive -> mask **) - - let rec sub_mask x y = - match x with - | XI p -> - (match y with - | XI q0 -> double_mask (sub_mask p q0) - | XO q0 -> succ_double_mask (sub_mask p q0) - | XH -> IsPos (XO p)) - | XO p -> - (match y with - | 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) - - (** val sub_mask_carry : positive -> positive -> mask **) - - and sub_mask_carry x y = - match x with - | XI p -> - (match y with - | XI q0 -> succ_double_mask (sub_mask_carry p q0) - | XO q0 -> double_mask (sub_mask p q0) - | XH -> IsPos (pred_double p)) - | XO p -> - (match y with - | XI q0 -> double_mask (sub_mask_carry p q0) - | XO q0 -> succ_double_mask (sub_mask_carry p q0) - | XH -> double_pred_mask p) - | XH -> IsNeg - - (** val sub : positive -> positive -> positive **) - - let sub x y = - match sub_mask x y with - | IsPos z0 -> z0 - | _ -> XH - - (** val mul : positive -> positive -> positive **) - - let rec mul x y = - match x with - | XI p -> add y (XO (mul p y)) - | XO p -> XO (mul p y) - | XH -> y - - (** val size_nat : positive -> nat **) - - let rec size_nat = function - | XI p2 -> S (size_nat p2) - | XO p2 -> S (size_nat p2) - | XH -> S O - - (** val compare_cont : - comparison -> positive -> positive -> comparison **) - - let rec compare_cont r x y = - match x with - | XI p -> - (match y with - | XI q0 -> compare_cont r p q0 - | XO q0 -> compare_cont Gt p q0 - | XH -> Gt) - | XO p -> - (match y with - | XI q0 -> compare_cont Lt p q0 - | XO q0 -> compare_cont r p q0 - | XH -> Gt) - | XH -> - (match y with - | XH -> r - | _ -> Lt) - - (** val compare : positive -> positive -> comparison **) - - let compare = - compare_cont Eq - - (** val gcdn : nat -> positive -> positive -> positive **) - - let rec gcdn n0 a b = - match n0 with - | O -> XH - | S n1 -> - (match a with - | XI a' -> - (match b with - | XI b' -> - (match compare a' b' with - | Eq -> a - | Lt -> gcdn n1 (sub b' a') a - | Gt -> gcdn n1 (sub a' b') b) - | XO b0 -> gcdn n1 a b0 - | XH -> XH) - | XO a0 -> - (match b with - | XI _ -> gcdn n1 a0 b - | XO b0 -> XO (gcdn n1 a0 b0) - | XH -> XH) - | XH -> XH) - - (** val gcd : positive -> positive -> positive **) - - let gcd a b = - gcdn (Coq__1.add (size_nat a) (size_nat b)) a b - - (** val of_succ_nat : nat -> positive **) - - let rec of_succ_nat = function - | O -> XH - | S x -> succ (of_succ_nat x) - end - -module N = - struct - (** val of_nat : nat -> n **) - - let of_nat = function - | O -> N0 - | S n' -> Npos (Coq_Pos.of_succ_nat n') - end - -(** val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 **) - -let rec pow_pos rmul x = function -| XI i0 -> let p = pow_pos rmul x i0 in rmul x (rmul p p) -| XO i0 -> let p = pow_pos rmul x i0 in rmul p p -| XH -> x - -(** val nth : nat -> 'a1 list -> 'a1 -> 'a1 **) - -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) - -(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **) - -let rec map f = function -| [] -> [] -| a::t0 -> (f a)::(map f t0) - -(** val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 **) - -let rec fold_right f a0 = function -| [] -> a0 -| b::t0 -> f b (fold_right f a0 t0) - -module Z = - struct - (** val double : z -> z **) - - let double = function - | Z0 -> Z0 - | Zpos p -> Zpos (XO p) - | Zneg p -> Zneg (XO p) - - (** val succ_double : z -> z **) - - let succ_double = function - | Z0 -> Zpos XH - | Zpos p -> Zpos (XI p) - | Zneg p -> Zneg (Coq_Pos.pred_double p) - - (** val pred_double : z -> z **) - - let pred_double = function - | Z0 -> Zneg XH - | Zpos p -> Zpos (Coq_Pos.pred_double p) - | Zneg p -> Zneg (XI p) - - (** val pos_sub : positive -> positive -> z **) - - let rec pos_sub x y = - match x with - | XI p -> - (match y with - | XI q0 -> double (pos_sub p q0) - | XO q0 -> succ_double (pos_sub p q0) - | XH -> Zpos (XO p)) - | XO p -> - (match y with - | XI q0 -> pred_double (pos_sub p q0) - | XO q0 -> double (pos_sub p q0) - | XH -> Zpos (Coq_Pos.pred_double p)) - | XH -> - (match y with - | XI q0 -> Zneg (XO q0) - | XO q0 -> Zneg (Coq_Pos.pred_double q0) - | XH -> Z0) - - (** val add : z -> z -> z **) - - let add x y = - match x with - | Z0 -> y - | Zpos x' -> - (match y with - | Z0 -> x - | Zpos y' -> Zpos (Coq_Pos.add x' y') - | Zneg y' -> pos_sub x' y') - | Zneg x' -> - (match y with - | Z0 -> x - | Zpos y' -> pos_sub y' x' - | Zneg y' -> Zneg (Coq_Pos.add x' y')) - - (** val opp : z -> z **) - - let opp = function - | Z0 -> Z0 - | Zpos x0 -> Zneg x0 - | Zneg x0 -> Zpos x0 - - (** val sub : z -> z -> z **) - - let sub m n0 = - add m (opp n0) - - (** val mul : z -> z -> z **) - - let mul x y = - match x with - | Z0 -> Z0 - | Zpos x' -> - (match y with - | Z0 -> Z0 - | Zpos y' -> Zpos (Coq_Pos.mul x' y') - | Zneg y' -> Zneg (Coq_Pos.mul x' y')) - | Zneg x' -> - (match y with - | Z0 -> Z0 - | Zpos y' -> Zneg (Coq_Pos.mul x' y') - | Zneg y' -> Zpos (Coq_Pos.mul x' y')) - - (** val compare : z -> z -> comparison **) - - 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) - | Zneg x' -> - (match y with - | Zneg y' -> compOpp (Coq_Pos.compare x' y') - | _ -> Lt) - - (** val leb : z -> z -> bool **) - - let leb x y = - match compare x y with - | Gt -> false - | _ -> true - - (** val ltb : z -> z -> bool **) - - let ltb x y = - match compare x y with - | Lt -> true - | _ -> false - - (** val gtb : z -> z -> bool **) - - let gtb x y = - match compare x y with - | Gt -> true - | _ -> false - - (** val max : z -> z -> z **) - - let max n0 m = - match compare n0 m with - | Lt -> m - | _ -> n0 - - (** val abs : z -> z **) - - let abs = function - | Zneg p -> Zpos p - | x -> x - - (** val to_N : z -> n **) - - let to_N = function - | Zpos p -> Npos p - | _ -> N0 - - (** val pos_div_eucl : positive -> z -> z * z **) - - let rec pos_div_eucl a b = - match a with - | XI a' -> - let q0,r = pos_div_eucl a' b in - let r' = add (mul (Zpos (XO XH)) r) (Zpos XH) in - if ltb r' b - then (mul (Zpos (XO XH)) q0),r' - else (add (mul (Zpos (XO XH)) q0) (Zpos XH)),(sub r' b) - | XO a' -> - let q0,r = pos_div_eucl a' b in - let r' = mul (Zpos (XO XH)) r in - if ltb r' b - then (mul (Zpos (XO XH)) q0),r' - else (add (mul (Zpos (XO XH)) q0) (Zpos XH)),(sub r' b) - | XH -> if leb (Zpos (XO XH)) b then Z0,(Zpos XH) else (Zpos XH),Z0 - - (** val div_eucl : z -> z -> z * z **) - - let div_eucl a b = - match a with - | Z0 -> Z0,Z0 - | Zpos a' -> - (match b with - | Z0 -> Z0,Z0 - | Zpos _ -> pos_div_eucl a' b - | Zneg b' -> - let q0,r = pos_div_eucl a' (Zpos b') in - (match r with - | Z0 -> (opp q0),Z0 - | _ -> (opp (add q0 (Zpos XH))),(add b r))) - | Zneg a' -> - (match b with - | Z0 -> Z0,Z0 - | Zpos _ -> - let q0,r = pos_div_eucl a' b in - (match r with - | Z0 -> (opp q0),Z0 - | _ -> (opp (add q0 (Zpos XH))),(sub b r)) - | Zneg b' -> let q0,r = pos_div_eucl a' (Zpos b') in q0,(opp r)) - - (** val div : z -> z -> z **) - - let div a b = - let q0,_ = div_eucl a b in q0 - - (** val gcd : z -> z -> z **) - - let gcd a b = - match a with - | Z0 -> abs b - | Zpos a0 -> - (match b with - | Z0 -> abs a - | Zpos b0 -> Zpos (Coq_Pos.gcd a0 b0) - | Zneg b0 -> Zpos (Coq_Pos.gcd a0 b0)) - | Zneg a0 -> - (match b with - | Z0 -> abs a - | Zpos b0 -> Zpos (Coq_Pos.gcd a0 b0) - | Zneg b0 -> Zpos (Coq_Pos.gcd a0 b0)) - end - -(** val zeq_bool : z -> z -> bool **) - -let zeq_bool x y = - match Z.compare x y with - | Eq -> true - | _ -> false - -type 'c pol = -| Pc of 'c -| Pinj of positive * 'c pol -| PX of 'c pol * positive * 'c pol - -(** val p0 : 'a1 -> 'a1 pol **) - -let p0 cO = - Pc cO - -(** val p1 : 'a1 -> 'a1 pol **) - -let p1 cI = - Pc cI - -(** val peq : ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> bool **) - -let rec peq ceqb p p' = - match p with - | Pc c -> - (match p' with - | Pc c' -> ceqb c c' - | _ -> false) - | Pinj (j, q0) -> - (match p' with - | Pinj (j', q') -> - (match Coq_Pos.compare j j' with - | Eq -> peq ceqb q0 q' - | _ -> false) - | _ -> false) - | PX (p2, i, q0) -> - (match p' with - | PX (p'0, i', q') -> - (match Coq_Pos.compare i i' with - | Eq -> if peq ceqb p2 p'0 then peq ceqb q0 q' else false - | _ -> false) - | _ -> false) - -(** val mkPinj : positive -> 'a1 pol -> 'a1 pol **) - -let mkPinj j p = match p with -| Pc _ -> p -| Pinj (j', q0) -> Pinj ((Coq_Pos.add j j'), q0) -| PX (_, _, _) -> Pinj (j, p) - -(** val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol **) - -let mkPinj_pred j p = - match j with - | XI j0 -> Pinj ((XO j0), p) - | XO j0 -> Pinj ((Coq_Pos.pred_double j0), p) - | XH -> p - -(** val mkPX : - 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 - pol **) - -let mkPX cO ceqb p i q0 = - match p with - | Pc c -> if ceqb c cO then mkPinj XH q0 else PX (p, i, q0) - | Pinj (_, _) -> PX (p, i, q0) - | PX (p', i', q') -> - if peq ceqb q' (p0 cO) - then PX (p', (Coq_Pos.add i' i), q0) - else PX (p, i, q0) - -(** val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol **) - -let mkXi cO cI i = - PX ((p1 cI), i, (p0 cO)) - -(** val mkX : 'a1 -> 'a1 -> 'a1 pol **) - -let mkX cO cI = - mkXi cO cI XH - -(** val popp : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol **) - -let rec popp copp = function -| Pc c -> Pc (copp c) -| Pinj (j, q0) -> Pinj (j, (popp copp q0)) -| PX (p2, i, q0) -> PX ((popp copp p2), i, (popp copp q0)) - -(** val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol **) - -let rec paddC cadd p c = - match p with - | Pc c1 -> Pc (cadd c1 c) - | Pinj (j, q0) -> Pinj (j, (paddC cadd q0 c)) - | PX (p2, i, q0) -> PX (p2, i, (paddC cadd q0 c)) - -(** val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol **) - -let rec psubC csub p c = - match p with - | Pc c1 -> Pc (csub c1 c) - | Pinj (j, q0) -> Pinj (j, (psubC csub q0 c)) - | PX (p2, i, q0) -> PX (p2, i, (psubC csub q0 c)) - -(** val paddI : - ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> - positive -> 'a1 pol -> 'a1 pol **) - -let rec paddI cadd pop q0 j = function -| Pc c -> mkPinj j (paddC cadd q0 c) -| Pinj (j', q') -> - (match Z.pos_sub j' j with - | Z0 -> mkPinj j (pop q' q0) - | Zpos k -> mkPinj j (pop (Pinj (k, q')) q0) - | Zneg k -> mkPinj j' (paddI cadd pop q0 k q')) -| PX (p2, i, q') -> - (match j with - | XI j0 -> PX (p2, i, (paddI cadd pop q0 (XO j0) q')) - | XO j0 -> PX (p2, i, (paddI cadd pop q0 (Coq_Pos.pred_double j0) q')) - | 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 **) - -let rec psubI cadd copp pop q0 j = function -| Pc c -> mkPinj j (paddC cadd (popp copp q0) c) -| Pinj (j', q') -> - (match Z.pos_sub j' j with - | Z0 -> mkPinj j (pop q' q0) - | Zpos k -> mkPinj j (pop (Pinj (k, q')) q0) - | Zneg k -> mkPinj j' (psubI cadd copp pop q0 k q')) -| 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')) - | 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 **) - -let rec paddX cO ceqb pop p' i' p = match p with -| Pc _ -> PX (p', i', p) -| Pinj (j, q') -> - (match j with - | XI j0 -> PX (p', i', (Pinj ((XO j0), q'))) - | XO j0 -> PX (p', i', (Pinj ((Coq_Pos.pred_double j0), q'))) - | XH -> PX (p', i', q')) -| PX (p2, i, q') -> - (match Z.pos_sub i i' with - | Z0 -> mkPX cO ceqb (pop p2 p') i q' - | Zpos k -> mkPX cO ceqb (pop (PX (p2, k, (p0 cO))) p') i' q' - | 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 **) - -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'))) - | XH -> PX ((popp copp p'), i', q')) -| PX (p2, i, q') -> - (match Z.pos_sub i i' with - | Z0 -> mkPX cO ceqb (pop p2 p') i q' - | Zpos k -> mkPX cO ceqb (pop (PX (p2, k, (p0 cO))) p') i' q' - | 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 **) - -let rec padd cO cadd ceqb p = function -| Pc c' -> paddC cadd p c' -| Pinj (j', q') -> paddI cadd (padd cO cadd ceqb) q' j' p -| PX (p'0, i', q') -> - (match p with - | Pc c -> PX (p'0, i', (paddC cadd q' c)) - | Pinj (j, q0) -> - (match j with - | XI j0 -> PX (p'0, i', (padd cO cadd ceqb (Pinj ((XO j0), q0)) q')) - | XO j0 -> - PX (p'0, i', - (padd cO cadd ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) q')) - | XH -> PX (p'0, i', (padd cO cadd ceqb q0 q'))) - | 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') - | Zpos k -> - mkPX cO ceqb (padd cO cadd ceqb (PX (p2, k, (p0 cO))) p'0) i' - (padd cO cadd ceqb q0 q') - | Zneg k -> - mkPX cO ceqb (paddX cO ceqb (padd cO cadd ceqb) p'0 k p2) i - (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 **) - -let rec psub cO cadd csub copp ceqb p = function -| Pc c' -> psubC csub p c' -| Pinj (j', q') -> psubI cadd copp (psub cO cadd csub copp ceqb) q' j' p -| PX (p'0, i', q') -> - (match p with - | Pc c -> PX ((popp copp p'0), i', (paddC cadd (popp copp q') c)) - | Pinj (j, q0) -> - (match j with - | XI j0 -> - PX ((popp copp p'0), i', - (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'))) - | 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') - | 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 **) - -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) - -(** val pmulC : - '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 - then p0 cO - 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 **) - -let rec pmulI cO cI cmul ceqb pmul0 q0 j = function -| Pc c -> mkPinj j (pmulC cO cI cmul ceqb q0 c) -| Pinj (j', q') -> - (match Z.pos_sub j' j with - | Z0 -> mkPinj j (pmul0 q' q0) - | Zpos k -> mkPinj j (pmul0 (Pinj (k, q')) q0) - | Zneg k -> mkPinj j' (pmulI cO cI cmul ceqb pmul0 q0 k q')) -| PX (p', i', q') -> - (match j with - | XI j' -> - mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 j p') i' - (pmulI cO cI cmul ceqb pmul0 q0 (XO j') q') - | XO j' -> - mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 j p') i' - (pmulI cO cI cmul ceqb pmul0 q0 (Coq_Pos.pred_double j') q') - | XH -> - 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 **) - -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 -| PX (p', i', q') -> - (match p with - | Pc c -> pmulC cO cI cmul ceqb p'' c - | Pinj (j, q0) -> - let qQ' = - 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' - | 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 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')) - -(** val psquare : - '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) -| Pinj (j, q0) -> Pinj (j, (psquare cO cI cadd cmul ceqb q0)) -| PX (p2, i, q0) -> - let twoPQ = - pmul cO cI cadd cmul ceqb p2 - (mkPinj XH (pmulC cO cI cmul ceqb q0 (cadd cI cI))) - in - let q2 = psquare cO cI cadd cmul ceqb q0 in - let p3 = psquare cO cI cadd cmul ceqb p2 in - mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb p3 i (p0 cO)) twoPQ) i q2 - -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 **) - -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 **) - -let rec ppow_pos cO cI cadd cmul ceqb subst_l res p = function -| XI p3 -> - subst_l - (pmul cO cI cadd cmul ceqb - (ppow_pos cO cI cadd cmul ceqb subst_l - (ppow_pos cO cI cadd cmul ceqb subst_l res p p3) p p3) p) -| XO p3 -> - ppow_pos cO cI cadd cmul ceqb subst_l - (ppow_pos cO cI cadd cmul ceqb subst_l res p p3) p p3 -| 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 **) - -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 **) - -let rec norm_aux cO cI cadd cmul csub copp ceqb = function -| PEc c -> Pc c -| PEX j -> mk_X cO cI j -| PEadd (pe1, pe2) -> - (match pe1 with - | PEopp pe3 -> - psub cO cadd csub copp ceqb - (norm_aux cO cI cadd cmul csub copp ceqb pe2) - (norm_aux cO cI cadd cmul csub copp ceqb pe3) - | _ -> - (match pe2 with - | PEopp pe3 -> - 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 pe3) - | _ -> - 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) - (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) - (norm_aux cO cI cadd cmul csub copp ceqb pe2) -| PEopp pe1 -> popp copp (norm_aux cO cI cadd cmul csub copp ceqb pe1) -| PEpow (pe1, n0) -> - ppow_N cO cI cadd cmul ceqb (fun p -> p) - (norm_aux cO cI cadd cmul csub copp ceqb pe1) n0 - -type 'a bFormula = -| TT -| FF -| X -| A of 'a -| Cj of 'a bFormula * 'a bFormula -| D of 'a bFormula * 'a bFormula -| N of 'a bFormula -| I of 'a bFormula * 'a bFormula - -(** val map_bformula : ('a1 -> 'a2) -> 'a1 bFormula -> 'a2 bFormula **) - -let rec map_bformula fct = function -| TT -> TT -| FF -> FF -| X -> X -| A a -> A (fct a) -| 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, f2) -> I ((map_bformula fct f1), (map_bformula fct f2)) - -type 'x clause = 'x list - -type 'x cnf = 'x clause list - -(** val tt : 'a1 cnf **) - -let tt = - [] - -(** val ff : 'a1 cnf **) - -let ff = - []::[] - -(** val add_term : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> - 'a1 clause option **) - -let rec add_term unsat deduce t0 = function -| [] -> - (match deduce t0 t0 with - | Some u -> if unsat u then None else Some (t0::[]) - | None -> Some (t0::[])) -| t'::cl0 -> - (match deduce t0 t' with - | Some u -> - if unsat u - then None - else (match add_term unsat deduce t0 cl0 with - | Some cl' -> Some (t'::cl') - | None -> None) - | None -> - (match add_term unsat deduce t0 cl0 with - | Some cl' -> Some (t'::cl') - | None -> None)) - -(** val or_clause : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 - clause -> 'a1 clause option **) - -let rec or_clause unsat deduce cl1 cl2 = - match cl1 with - | [] -> Some cl2 - | t0::cl -> - (match add_term unsat deduce t0 cl2 with - | Some cl' -> or_clause unsat deduce cl cl' - | None -> None) - -(** val or_clause_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 -> - match or_clause unsat deduce t0 e with - | Some cl -> cl::acc - | None -> acc) [] f - -(** val or_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 cnf -> 'a1 cnf -> - 'a1 cnf **) - -let rec or_cnf unsat deduce f f' = - match f with - | [] -> tt - | e::rst -> - app (or_cnf unsat deduce rst f') (or_clause_cnf unsat deduce e f') - -(** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **) - -let and_cnf f1 f2 = - app f1 f2 - -(** val xcnf : - ('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 -| FF -> if pol0 then ff else tt -| X -> ff -| A x -> if pol0 then normalise0 x else negate0 x -| Cj (e1, e2) -> - if pol0 - then and_cnf (xcnf unsat deduce normalise0 negate0 pol0 e1) - (xcnf unsat deduce normalise0 negate0 pol0 e2) - else or_cnf unsat deduce (xcnf unsat deduce normalise0 negate0 pol0 e1) - (xcnf unsat deduce normalise0 negate0 pol0 e2) -| D (e1, e2) -> - if pol0 - then or_cnf unsat deduce (xcnf unsat deduce normalise0 negate0 pol0 e1) - (xcnf unsat deduce normalise0 negate0 pol0 e2) - else and_cnf (xcnf unsat deduce normalise0 negate0 pol0 e1) - (xcnf unsat deduce normalise0 negate0 pol0 e2) -| N e -> xcnf unsat deduce normalise0 negate0 (negb pol0) e -| I (e1, e2) -> - if pol0 - then or_cnf unsat deduce - (xcnf unsat deduce normalise0 negate0 (negb pol0) e1) - (xcnf unsat deduce normalise0 negate0 pol0 e2) - else and_cnf (xcnf unsat deduce normalise0 negate0 (negb pol0) e1) - (xcnf unsat deduce normalise0 negate0 pol0 e2) - -(** val cnf_checker : - ('a1 list -> 'a2 -> bool) -> 'a1 cnf -> 'a2 list -> bool **) - -let rec cnf_checker checker f l = - match f with - | [] -> true - | e::f0 -> - (match l with - | [] -> false - | 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 **) - -let tauto_checker unsat deduce normalise0 negate0 checker f w = - cnf_checker checker (xcnf unsat deduce normalise0 negate0 true f) w - -(** val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool **) - -let cneqb ceqb x y = - negb (ceqb x y) - -(** val cltb : - ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool **) - -let cltb ceqb cleb x y = - (&&) (cleb x y) (cneqb ceqb x y) - -type 'c polC = 'c pol - -type op1 = -| Equal -| NonEqual -| Strict -| NonStrict - -type 'c nFormula = 'c polC * op1 - -(** val opMult : op1 -> op1 -> op1 option **) - -let opMult o o' = - match o with - | Equal -> Some Equal - | NonEqual -> - (match o' with - | Equal -> Some Equal - | NonEqual -> Some NonEqual - | _ -> None) - | Strict -> - (match o' with - | NonEqual -> None - | _ -> Some o') - | NonStrict -> - (match o' with - | Equal -> Some Equal - | NonEqual -> None - | _ -> Some NonStrict) - -(** val opAdd : op1 -> op1 -> op1 option **) - -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) - | NonStrict -> - (match o' with - | Equal -> Some NonStrict - | NonEqual -> None - | x -> Some x) - -type 'c psatz = -| PsatzIn of nat -| PsatzSquare of 'c polC -| PsatzMulC of 'c polC * 'c psatz -| PsatzMulE of 'c psatz * 'c psatz -| PsatzAdd of 'c psatz * 'c psatz -| PsatzC of 'c -| PsatzZ - -(** val map_option : ('a1 -> 'a2 option) -> 'a1 option -> 'a2 option **) - -let map_option f = function -| Some x -> f x -| None -> None - -(** val map_option2 : - ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option **) - -let map_option2 f o o' = - match o with - | 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 **) - -let pexpr_times_nformula cO cI cplus ctimes ceqb e = function -| ef,o -> - (match o with - | Equal -> Some ((pmul cO cI cplus ctimes ceqb e ef),Equal) - | _ -> None) - -(** val nformula_times_nformula : - '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 - let e2,o2 = f2 in - map_option (fun x -> Some ((pmul cO cI cplus ctimes ceqb e1 e2),x)) - (opMult o1 o2) - -(** val nformula_plus_nformula : - '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 - let e2,o2 = f2 in - 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 **) - -let rec eval_Psatz cO cI cplus ctimes ceqb cleb l = function -| PsatzIn n0 -> Some (nth n0 l ((Pc cO),Equal)) -| PsatzSquare e0 -> Some ((psquare cO cI cplus ctimes ceqb e0),NonStrict) -| PsatzMulC (re, e0) -> - map_option (pexpr_times_nformula cO cI cplus ctimes ceqb re) - (eval_Psatz cO cI cplus ctimes ceqb cleb l e0) -| PsatzMulE (f1, f2) -> - map_option2 (nformula_times_nformula cO cI cplus ctimes ceqb) - (eval_Psatz cO cI cplus ctimes ceqb cleb l f1) - (eval_Psatz cO cI cplus ctimes ceqb cleb l f2) -| PsatzAdd (f1, f2) -> - map_option2 (nformula_plus_nformula cO cplus ceqb) - (eval_Psatz cO cI cplus ctimes ceqb cleb l f1) - (eval_Psatz cO cI cplus ctimes ceqb cleb l f2) -| PsatzC c -> if cltb ceqb cleb cO c then Some ((Pc c),Strict) else None -| PsatzZ -> Some ((Pc cO),Equal) - -(** val check_inconsistent : - 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> - bool **) - -let check_inconsistent cO ceqb cleb = function -| e,op -> - (match e with - | Pc c -> - (match op with - | Equal -> cneqb ceqb c cO - | NonEqual -> ceqb c cO - | Strict -> cleb c cO - | NonStrict -> cltb ceqb cleb c cO) - | _ -> 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 **) - -let check_normalised_formulas cO cI cplus ctimes ceqb cleb l cm = - match eval_Psatz cO cI cplus ctimes ceqb cleb l cm with - | Some f -> check_inconsistent cO ceqb cleb f - | None -> false - -type op2 = -| OpEq -| OpNEq -| OpLe -| OpGe -| OpLt -| OpGt - -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 **) - -let norm cO cI cplus ctimes cminus copp ceqb = - norm_aux cO cI cplus ctimes cminus copp ceqb - -(** val psub0 : - '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 - -(** val padd0 : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 - pol -> 'a1 pol **) - -let padd0 cO cplus ceqb = - padd cO cplus ceqb - -(** val xnormalise : - '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 - let lhs0 = norm cO cI cplus ctimes cminus copp ceqb lhs in - 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 - cminus copp - 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)::[] - | OpLt -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),NonStrict)::[] - | 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 **) - -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 **) - -let xnegate cO cI cplus ctimes cminus copp ceqb t0 = - let { flhs = lhs; fop = o; frhs = rhs } = t0 in - let lhs0 = norm cO cI cplus ctimes cminus copp ceqb lhs in - let rhs0 = norm cO cI cplus ctimes cminus copp ceqb rhs in - (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 - cminus copp - 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 **) - -let cnf_negate cO cI cplus ctimes cminus copp ceqb t0 = - map (fun x -> x::[]) (xnegate cO cI cplus ctimes cminus copp ceqb t0) - -(** val xdenorm : positive -> 'a1 pol -> 'a1 pExpr **) - -let rec xdenorm jmp = function -| Pc c -> PEc c -| Pinj (j, p2) -> xdenorm (Coq_Pos.add j jmp) p2 -| PX (p2, j, q0) -> - PEadd ((PEmul ((xdenorm jmp p2), (PEpow ((PEX jmp), (Npos j))))), - (xdenorm (Coq_Pos.succ jmp) q0)) - -(** val denorm : 'a1 pol -> 'a1 pExpr **) - -let denorm p = - xdenorm XH p - -(** val map_PExpr : ('a2 -> 'a1) -> 'a2 pExpr -> 'a1 pExpr **) - -let rec map_PExpr c_of_S = function -| PEc c -> PEc (c_of_S c) -| PEX p -> PEX p -| PEadd (e1, e2) -> PEadd ((map_PExpr c_of_S e1), (map_PExpr c_of_S e2)) -| PEsub (e1, e2) -> PEsub ((map_PExpr c_of_S e1), (map_PExpr c_of_S e2)) -| PEmul (e1, e2) -> PEmul ((map_PExpr c_of_S e1), (map_PExpr c_of_S e2)) -| PEopp e0 -> PEopp (map_PExpr c_of_S e0) -| PEpow (e0, n0) -> PEpow ((map_PExpr c_of_S e0), n0) - -(** val map_Formula : ('a2 -> 'a1) -> 'a2 formula -> 'a1 formula **) - -let map_Formula c_of_S f = - let { flhs = l; fop = o; frhs = r } = f in - { 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 **) - -let simpl_cone cO cI ctimes ceqb e = match e with -| PsatzSquare t0 -> - (match t0 with - | Pc c -> if ceqb cO c then PsatzZ else PsatzC (ctimes c c) - | _ -> PsatzSquare t0) -| PsatzMulE (t1, t2) -> - (match t1 with - | PsatzMulE (x, x0) -> - (match x with - | PsatzC p2 -> - (match t2 with - | PsatzC c -> PsatzMulE ((PsatzC (ctimes c p2)), x0) - | PsatzZ -> PsatzZ - | _ -> e) - | _ -> - (match x0 with - | PsatzC p2 -> - (match t2 with - | PsatzC c -> PsatzMulE ((PsatzC (ctimes c p2)), x) - | PsatzZ -> PsatzZ - | _ -> e) - | _ -> - (match t2 with - | PsatzC c -> if ceqb cI c then t1 else PsatzMulE (t1, t2) - | PsatzZ -> PsatzZ - | _ -> e))) - | PsatzC c -> - (match t2 with - | PsatzMulE (x, x0) -> - (match x with - | PsatzC p2 -> PsatzMulE ((PsatzC (ctimes c p2)), x0) - | _ -> - (match x0 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))) - | PsatzC c0 -> PsatzC (ctimes c c0) - | PsatzZ -> PsatzZ - | _ -> if ceqb cI c then t2 else PsatzMulE (t1, t2)) - | PsatzZ -> PsatzZ - | _ -> - (match t2 with - | PsatzC c -> if ceqb cI c then t1 else PsatzMulE (t1, t2) - | PsatzZ -> PsatzZ - | _ -> e)) -| PsatzAdd (t1, t2) -> - (match t1 with - | PsatzZ -> t2 - | _ -> - (match t2 with - | PsatzZ -> t1 - | _ -> PsatzAdd (t1, t2))) -| _ -> e - -type q = { qnum : z; qden : positive } - -(** val qnum : q -> z **) - -let qnum x = x.qnum - -(** val qden : q -> positive **) - -let qden x = x.qden - -(** val qeq_bool : q -> q -> bool **) - -let qeq_bool x y = - zeq_bool (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden)) - -(** val qle_bool : q -> q -> bool **) - -let qle_bool x y = - Z.leb (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden)) - -(** 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))); - qden = (Coq_Pos.mul x.qden y.qden) } - -(** val qmult : q -> q -> q **) - -let qmult x y = - { qnum = (Z.mul x.qnum y.qnum); qden = (Coq_Pos.mul x.qden y.qden) } - -(** val qopp : q -> q **) - -let qopp x = - { qnum = (Z.opp x.qnum); qden = x.qden } - -(** val qminus : q -> q -> q **) - -let qminus x y = - qplus x (qopp y) - -(** val qinv : q -> q **) - -let qinv x = - match x.qnum with - | Z0 -> { qnum = Z0; qden = XH } - | Zpos p -> { qnum = (Zpos x.qden); qden = p } - | Zneg p -> { qnum = (Zneg x.qden); qden = p } - -(** val qpower_positive : q -> positive -> q **) - -let qpower_positive = - pow_pos qmult - -(** val qpower : q -> z -> q **) - -let qpower q0 = function -| Z0 -> { qnum = (Zpos XH); qden = XH } -| Zpos p -> qpower_positive q0 p -| Zneg p -> qinv (qpower_positive q0 p) - -type 'a t = -| Empty -| Leaf of 'a -| Node of 'a t * 'a * 'a t - -(** val find : 'a1 -> 'a1 t -> positive -> 'a1 **) - -let rec find default vm p = - match vm with - | Empty -> default - | Leaf i -> i - | Node (l, e, r) -> - (match p with - | XI p2 -> find default r p2 - | XO p2 -> find default l p2 - | XH -> e) - -(** val singleton : 'a1 -> positive -> 'a1 -> 'a1 t **) - -let rec singleton default x v = - match x with - | XI p -> Node (Empty, default, (singleton default p v)) - | XO p -> Node ((singleton default p v), default, Empty) - | XH -> Leaf v - -(** val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t **) - -let rec vm_add default x v = function -| Empty -> singleton default x v -| Leaf vl -> - (match x with - | XI p -> Node (Empty, vl, (singleton default p v)) - | XO p -> Node ((singleton default p v), vl, Empty) - | XH -> Leaf v) -| Node (l, o, r) -> - (match x with - | XI p -> Node (l, o, (vm_add default p v r)) - | XO p -> Node ((vm_add default p v l), o, r) - | XH -> Node (l, v, r)) - -type zWitness = z psatz - -(** val zWeakChecker : z nFormula list -> z psatz -> bool **) - -let zWeakChecker = - check_normalised_formulas Z0 (Zpos XH) Z.add Z.mul zeq_bool Z.leb - -(** val psub1 : z pol -> z pol -> z pol **) - -let psub1 = - psub0 Z0 Z.add Z.sub Z.opp zeq_bool - -(** val padd1 : z pol -> z pol -> z pol **) - -let padd1 = - padd0 Z0 Z.add zeq_bool - -(** val norm0 : z pExpr -> z pol **) - -let norm0 = - norm Z0 (Zpos XH) Z.add Z.mul Z.sub Z.opp zeq_bool - -(** val xnormalise0 : z formula -> z nFormula list **) - -let xnormalise0 t0 = - let { flhs = lhs; fop = o; frhs = rhs } = t0 in - let lhs0 = norm0 lhs in - let rhs0 = norm0 rhs in - (match o with - | OpEq -> - ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::(((psub1 rhs0 - (padd1 lhs0 - (Pc (Zpos - XH)))),NonStrict)::[]) - | OpNEq -> ((psub1 lhs0 rhs0),Equal)::[] - | OpLe -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::[] - | OpGe -> ((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))),NonStrict)::[] - | OpLt -> ((psub1 lhs0 rhs0),NonStrict)::[] - | OpGt -> ((psub1 rhs0 lhs0),NonStrict)::[]) - -(** val normalise : z formula -> z nFormula cnf **) - -let normalise t0 = - map (fun x -> x::[]) (xnormalise0 t0) - -(** val xnegate0 : z formula -> z nFormula list **) - -let xnegate0 t0 = - let { flhs = lhs; fop = o; frhs = rhs } = t0 in - let lhs0 = norm0 lhs in - let rhs0 = norm0 rhs in - (match o with - | OpEq -> ((psub1 lhs0 rhs0),Equal)::[] - | OpNEq -> - ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::(((psub1 rhs0 - (padd1 lhs0 - (Pc (Zpos - XH)))),NonStrict)::[]) - | OpLe -> ((psub1 rhs0 lhs0),NonStrict)::[] - | OpGe -> ((psub1 lhs0 rhs0),NonStrict)::[] - | OpLt -> ((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))),NonStrict)::[] - | OpGt -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::[]) - -(** val negate : z formula -> z nFormula cnf **) - -let negate t0 = - map (fun x -> x::[]) (xnegate0 t0) - -(** val zunsat : z nFormula -> bool **) - -let zunsat = - check_inconsistent Z0 zeq_bool Z.leb - -(** val zdeduce : z nFormula -> z nFormula -> z nFormula option **) - -let zdeduce = - nformula_plus_nformula Z0 Z.add zeq_bool - -(** val ceiling : z -> z -> z **) - -let ceiling a b = - let q0,r = Z.div_eucl a b in - (match r with - | Z0 -> q0 - | _ -> Z.add q0 (Zpos XH)) - -type zArithProof = -| DoneProof -| RatProof of zWitness * zArithProof -| CutProof of zWitness * zArithProof -| EnumProof of zWitness * zWitness * zArithProof list - -(** val zgcdM : z -> z -> z **) - -let zgcdM x y = - Z.max (Z.gcd x y) (Zpos XH) - -(** val zgcd_pol : z polC -> z * z **) - -let rec zgcd_pol = function -| Pc c -> Z0,c -| Pinj (_, p2) -> zgcd_pol p2 -| PX (p2, _, q0) -> - let g1,c1 = zgcd_pol p2 in - let g2,c2 = zgcd_pol q0 in (zgcdM (zgcdM g1 c1) g2),c2 - -(** val zdiv_pol : z polC -> z -> z polC **) - -let rec zdiv_pol p x = - match p with - | Pc c -> Pc (Z.div c x) - | Pinj (j, p2) -> Pinj (j, (zdiv_pol p2 x)) - | PX (p2, j, q0) -> PX ((zdiv_pol p2 x), j, (zdiv_pol q0 x)) - -(** val makeCuttingPlane : z polC -> z polC * z **) - -let makeCuttingPlane p = - let g,c = zgcd_pol p in - if Z.gtb g Z0 - then (zdiv_pol (psubC Z.sub p c) g),(Z.opp (ceiling (Z.opp c) g)) - else p,Z0 - -(** val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option **) - -let genCuttingPlane = function -| e,op -> - (match op with - | Equal -> - let g,c = zgcd_pol e in - if (&&) (Z.gtb g Z0) - ((&&) (negb (zeq_bool c Z0)) (negb (zeq_bool (Z.gcd g c) g))) - then None - else Some ((makeCuttingPlane e),Equal) - | NonEqual -> Some ((e,Z0),op) - | 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 **) - -let nformula_of_cutting_plane = function -| e_z,o -> let e,z0 = e_z in (padd1 e (Pc z0)),o - -(** val is_pol_Z0 : z polC -> bool **) - -let is_pol_Z0 = function -| Pc z0 -> - (match z0 with - | Z0 -> true - | _ -> false) -| _ -> false - -(** val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option **) - -let eval_Psatz0 = - eval_Psatz Z0 (Zpos XH) Z.add Z.mul zeq_bool Z.leb - -(** val valid_cut_sign : op1 -> bool **) - -let valid_cut_sign = function -| Equal -> true -| NonStrict -> true -| _ -> false - -(** val zChecker : z nFormula list -> zArithProof -> bool **) - -let rec zChecker l = function -| DoneProof -> false -| RatProof (w, pf0) -> - (match eval_Psatz0 l w with - | Some f -> if zunsat f then true else zChecker (f::l) pf0 - | None -> false) -| CutProof (w, pf0) -> - (match eval_Psatz0 l w with - | Some f -> - (match genCuttingPlane f with - | Some cp -> zChecker ((nformula_of_cutting_plane cp)::l) pf0 - | None -> true) - | None -> false) -| EnumProof (w1, w2, pf0) -> - (match eval_Psatz0 l w1 with - | Some f1 -> - (match eval_Psatz0 l w2 with - | Some f2 -> - (match genCuttingPlane f1 with - | Some p -> - let p2,op3 = p in - let e1,z1 = p2 in - (match genCuttingPlane f2 with - | Some p3 -> - let p4,op4 = p3 in - let e2,z2 = p4 in - if (&&) ((&&) (valid_cut_sign op3) (valid_cut_sign op4)) - (is_pol_Z0 (padd1 e1 e2)) - then let rec label pfs lb ub = - match pfs with - | [] -> Z.gtb lb ub - | pf1::rsr -> - (&&) (zChecker (((psub1 e1 (Pc lb)),Equal)::l) pf1) - (label rsr (Z.add lb (Zpos XH)) ub) - in label pf0 (Z.opp z1) z2 - else false - | None -> true) - | None -> true) - | None -> false) - | None -> false) - -(** val zTautoChecker : z formula bFormula -> zArithProof list -> bool **) - -let zTautoChecker f w = - tauto_checker zunsat zdeduce normalise negate zChecker f w - -type qWitness = q psatz - -(** val qWeakChecker : q nFormula list -> q psatz -> bool **) - -let qWeakChecker = - check_normalised_formulas { qnum = Z0; qden = XH } { qnum = (Zpos XH); - qden = XH } qplus qmult qeq_bool qle_bool - -(** val qnormalise : q formula -> q nFormula cnf **) - -let qnormalise = - cnf_normalise { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } - qplus qmult qminus qopp qeq_bool - -(** 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 - -(** val qunsat : q nFormula -> bool **) - -let qunsat = - check_inconsistent { qnum = Z0; qden = XH } qeq_bool qle_bool - -(** val qdeduce : q nFormula -> q nFormula -> q nFormula option **) - -let qdeduce = - nformula_plus_nformula { qnum = Z0; qden = XH } qplus qeq_bool - -(** val qTautoChecker : q formula bFormula -> qWitness list -> bool **) - -let qTautoChecker f w = - tauto_checker qunsat qdeduce qnormalise qnegate qWeakChecker f w - -type rcst = -| C0 -| C1 -| CQ of q -| CZ of z -| CPlus of rcst * rcst -| CMinus of rcst * rcst -| CMult of rcst * rcst -| CInv of rcst -| COpp of rcst - -(** val q_of_Rcst : rcst -> q **) - -let rec q_of_Rcst = function -| C0 -> { qnum = Z0; qden = XH } -| C1 -> { qnum = (Zpos XH); qden = XH } -| CQ q0 -> q0 -| CZ z0 -> { qnum = z0; qden = XH } -| CPlus (r1, r2) -> qplus (q_of_Rcst r1) (q_of_Rcst r2) -| CMinus (r1, r2) -> qminus (q_of_Rcst r1) (q_of_Rcst r2) -| CMult (r1, r2) -> qmult (q_of_Rcst r1) (q_of_Rcst r2) -| CInv r0 -> qinv (q_of_Rcst r0) -| COpp r0 -> qopp (q_of_Rcst r0) - -type rWitness = q psatz - -(** val rWeakChecker : q nFormula list -> q psatz -> bool **) - -let rWeakChecker = - check_normalised_formulas { qnum = Z0; qden = XH } { qnum = (Zpos XH); - qden = XH } qplus qmult qeq_bool qle_bool - -(** val rnormalise : q formula -> q nFormula cnf **) - -let rnormalise = - cnf_normalise { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } - qplus qmult qminus qopp qeq_bool - -(** 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 - -(** val runsat : q nFormula -> bool **) - -let runsat = - check_inconsistent { qnum = Z0; qden = XH } qeq_bool qle_bool - -(** val rdeduce : q nFormula -> q nFormula -> q nFormula option **) - -let rdeduce = - nformula_plus_nformula { qnum = Z0; qden = XH } qplus qeq_bool - -(** val rTautoChecker : rcst formula bFormula -> rWitness list -> bool **) - -let rTautoChecker f w = - tauto_checker runsat rdeduce rnormalise rnegate rWeakChecker - (map_bformula (map_Formula q_of_Rcst) f) w diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli deleted file mode 100644 index beb042f49d..0000000000 --- a/plugins/micromega/micromega.mli +++ /dev/null @@ -1,522 +0,0 @@ -val negb : bool -> bool - -type nat = -| O -| S of nat - -val app : 'a1 list -> 'a1 list -> 'a1 list - -type comparison = -| Eq -| Lt -| Gt - -val compOpp : comparison -> comparison - -val add : nat -> nat -> nat - -type positive = -| XI of positive -| XO of positive -| XH - -type n = -| N0 -| Npos of positive - -type z = -| Z0 -| Zpos of positive -| Zneg of positive - -module Pos : - sig - type mask = - | IsNul - | IsPos of positive - | IsNeg - end - -module Coq_Pos : - sig - val succ : positive -> positive - - val add : positive -> positive -> positive - - val add_carry : positive -> positive -> positive - - val pred_double : positive -> positive - - type mask = Pos.mask = - | IsNul - | IsPos of positive - | IsNeg - - val succ_double_mask : mask -> mask - - val double_mask : mask -> mask - - val double_pred_mask : positive -> mask - - val sub_mask : positive -> positive -> mask - - val sub_mask_carry : positive -> positive -> mask - - val sub : positive -> positive -> positive - - val mul : positive -> positive -> positive - - val size_nat : positive -> nat - - val compare_cont : comparison -> positive -> positive -> comparison - - val compare : positive -> positive -> comparison - - val gcdn : nat -> positive -> positive -> positive - - val gcd : positive -> positive -> positive - - val of_succ_nat : nat -> positive - end - -module N : - sig - val of_nat : nat -> n - end - -val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 - -val nth : nat -> 'a1 list -> 'a1 -> 'a1 - -val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list - -val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 - -module Z : - sig - val double : z -> z - - val succ_double : z -> z - - val pred_double : z -> z - - val pos_sub : positive -> positive -> z - - val add : z -> z -> z - - val opp : z -> z - - val sub : z -> z -> z - - val mul : z -> z -> z - - val compare : z -> z -> comparison - - val leb : z -> z -> bool - - val ltb : z -> z -> bool - - val gtb : z -> z -> bool - - val max : z -> z -> z - - val abs : z -> z - - val to_N : z -> n - - val pos_div_eucl : positive -> z -> z * z - - val div_eucl : z -> z -> z * z - - val div : z -> z -> z - - val gcd : z -> z -> z - end - -val zeq_bool : z -> z -> bool - -type 'c pol = -| Pc of 'c -| Pinj of positive * 'c pol -| PX of 'c pol * positive * 'c pol - -val p0 : 'a1 -> 'a1 pol - -val p1 : 'a1 -> 'a1 pol - -val peq : ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> bool - -val mkPinj : positive -> 'a1 pol -> 'a1 pol - -val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol - -val mkPX : - 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol - -val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol - -val mkX : 'a1 -> 'a1 -> 'a1 pol - -val popp : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol - -val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol - -val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol - -val paddI : - ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> - positive -> 'a1 pol -> 'a1 pol - -val psubI : - ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) - -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol - -val paddX : - 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 - pol -> positive -> 'a1 pol -> 'a1 pol - -val psubX : - 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> - 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol - -val padd : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol - -> 'a1 pol - -val psub : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> - ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol - -val pmulC_aux : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> - 'a1 pol - -val pmulC : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> - 'a1 -> 'a1 pol - -val pmulI : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> - 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol - -val pmul : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol - -val psquare : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> '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 : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> - 'a1 pol - -val ppow_N : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol - -val norm_aux : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol - -type 'a bFormula = -| TT -| FF -| X -| A of 'a -| Cj of 'a bFormula * 'a bFormula -| D of 'a bFormula * 'a bFormula -| N of 'a bFormula -| I of 'a bFormula * 'a bFormula - -val map_bformula : ('a1 -> 'a2) -> 'a1 bFormula -> 'a2 bFormula - -type 'x clause = 'x list - -type 'x cnf = 'x clause list - -val tt : 'a1 cnf - -val ff : 'a1 cnf - -val add_term : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> 'a1 - clause option - -val or_clause : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 clause - -> 'a1 clause option - -val or_clause_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf -> - 'a1 cnf - -val or_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 cnf -> 'a1 cnf -> 'a1 - cnf - -val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf - -val xcnf : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 - -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf - -val cnf_checker : ('a1 list -> 'a2 -> bool) -> 'a1 cnf -> 'a2 list -> bool - -val tauto_checker : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 - -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 bFormula -> 'a3 list -> - bool - -val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool - -val cltb : - ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool - -type 'c polC = 'c pol - -type op1 = -| Equal -| NonEqual -| Strict -| NonStrict - -type 'c nFormula = 'c polC * op1 - -val opMult : op1 -> op1 -> op1 option - -val opAdd : op1 -> op1 -> op1 option - -type 'c psatz = -| PsatzIn of nat -| PsatzSquare of 'c polC -| PsatzMulC of 'c polC * 'c psatz -| PsatzMulE of 'c psatz * 'c psatz -| PsatzAdd of 'c psatz * 'c psatz -| PsatzC of 'c -| PsatzZ - -val map_option : ('a1 -> 'a2 option) -> 'a1 option -> 'a2 option - -val map_option2 : - ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option - -val pexpr_times_nformula : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option - -val nformula_times_nformula : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option - -val nformula_plus_nformula : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> - 'a1 nFormula -> 'a1 nFormula option - -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 - -val check_inconsistent : - 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> - bool - -val check_normalised_formulas : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> - bool - -type op2 = -| OpEq -| OpNEq -| OpLe -| OpGe -| OpLt -| OpGt - -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 - -val psub0 : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> - ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol - -val padd0 : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol - -> 'a1 pol - -val xnormalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 - nFormula list - -val cnf_normalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 - nFormula cnf - -val xnegate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 - nFormula list - -val cnf_negate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 - nFormula cnf - -val xdenorm : positive -> 'a1 pol -> 'a1 pExpr - -val denorm : 'a1 pol -> 'a1 pExpr - -val map_PExpr : ('a2 -> 'a1) -> 'a2 pExpr -> 'a1 pExpr - -val map_Formula : ('a2 -> 'a1) -> 'a2 formula -> 'a1 formula - -val simpl_cone : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz - -> 'a1 psatz - -type q = { qnum : z; qden : positive } - -val qnum : q -> z - -val qden : q -> positive - -val qeq_bool : q -> q -> bool - -val qle_bool : q -> q -> bool - -val qplus : q -> q -> q - -val qmult : q -> q -> q - -val qopp : q -> q - -val qminus : q -> q -> q - -val qinv : q -> q - -val qpower_positive : q -> positive -> q - -val qpower : q -> z -> q - -type 'a t = -| Empty -| Leaf of 'a -| Node of 'a t * 'a * 'a t - -val find : 'a1 -> 'a1 t -> positive -> 'a1 - -val singleton : 'a1 -> positive -> 'a1 -> 'a1 t - -val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t - -type zWitness = z psatz - -val zWeakChecker : z nFormula list -> z psatz -> bool - -val psub1 : z pol -> z pol -> z pol - -val padd1 : z pol -> z pol -> z pol - -val norm0 : z pExpr -> z pol - -val xnormalise0 : z formula -> z nFormula list - -val normalise : z formula -> z nFormula cnf - -val xnegate0 : z formula -> z nFormula list - -val negate : z formula -> z nFormula cnf - -val zunsat : z nFormula -> bool - -val zdeduce : z nFormula -> z nFormula -> z nFormula option - -val ceiling : z -> z -> z - -type zArithProof = -| DoneProof -| RatProof of zWitness * zArithProof -| CutProof of zWitness * zArithProof -| EnumProof of zWitness * zWitness * zArithProof list - -val zgcdM : z -> z -> z - -val zgcd_pol : z polC -> z * z - -val zdiv_pol : z polC -> z -> z polC - -val makeCuttingPlane : z polC -> z polC * z - -val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option - -val nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula - -val is_pol_Z0 : z polC -> bool - -val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option - -val valid_cut_sign : op1 -> bool - -val zChecker : z nFormula list -> zArithProof -> bool - -val zTautoChecker : z formula bFormula -> zArithProof list -> bool - -type qWitness = q psatz - -val qWeakChecker : q nFormula list -> q psatz -> bool - -val qnormalise : q formula -> q nFormula cnf - -val qnegate : q formula -> q nFormula cnf - -val qunsat : q nFormula -> bool - -val qdeduce : q nFormula -> q nFormula -> q nFormula option - -val qTautoChecker : q formula bFormula -> qWitness list -> bool - -type rcst = -| C0 -| C1 -| CQ of q -| CZ of z -| CPlus of rcst * rcst -| CMinus of rcst * rcst -| CMult of rcst * rcst -| CInv of rcst -| COpp of rcst - -val q_of_Rcst : rcst -> q - -type rWitness = q psatz - -val rWeakChecker : q nFormula list -> q psatz -> bool - -val rnormalise : q formula -> q nFormula cnf - -val rnegate : q formula -> q nFormula cnf - -val runsat : q nFormula -> bool - -val rdeduce : q nFormula -> q nFormula -> q nFormula option - -val rTautoChecker : rcst formula bFormula -> rWitness list -> bool diff --git a/plugins/micromega/vo.itarget b/plugins/micromega/vo.itarget deleted file mode 100644 index c9009ea4de..0000000000 --- a/plugins/micromega/vo.itarget +++ /dev/null @@ -1,15 +0,0 @@ -EnvRing.vo -Env.vo -OrderedRing.vo -Psatz.vo -QMicromega.vo -Refl.vo -RingMicromega.vo -RMicromega.vo -Tauto.vo -VarMap.vo -ZCoeff.vo -ZMicromega.vo -Lia.vo -Lqa.vo -Lra.vo |