diff options
37 files changed, 1437 insertions, 3953 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 4bd11df8b..50c5b354e 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -21,6 +21,10 @@ open Sigma.Notations module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration +let safe_evar_info sigma evk = + try Some (Evd.find sigma evk) + with Not_found -> None + let safe_evar_value sigma ev = try Some (Evd.existential_value sigma ev) with NotInstantiatedEvar | Not_found -> None @@ -69,12 +73,14 @@ let rec flush_and_check_evars sigma c = let rec whd_evar sigma c = match kind_of_term c with - | Evar ev -> - let (evk, args) = ev in + | Evar (evk, args) -> + begin match safe_evar_info sigma evk with + | Some ({ evar_body = Evar_defined c } as info) -> let args = Array.map (fun c -> whd_evar sigma c) args in - (match safe_evar_value sigma (evk, args) with - Some c -> whd_evar sigma c - | None -> c) + let c = instantiate_evar_array info c args in + whd_evar sigma c + | _ -> c + end | Sort (Type u) -> let u' = Evd.normalize_universe sigma u in if u' == u then c else mkSort (Sorts.sort_of_univ u') @@ -372,16 +378,19 @@ let push_rel_context_to_named_context env typ = (* compute the instances relative to the named context and rel_context *) let open Context.Named.Declaration in let ids = List.map get_id (named_context env) in - let avoid = List.fold_right Id.Set.add ids Id.Set.empty in let inst_vars = List.map mkVar ids in - let inst_rels = List.rev (rel_list 0 (nb_rel env)) in - (* move the rel context to a named context and extend the named instance *) - (* with vars of the rel context *) - (* We do keep the instances corresponding to local definition (see above) *) - let (subst, vsubst, _, env) = - Context.Rel.fold_outside push_rel_decl_to_named_context - (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) in - (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst) + if List.is_empty (Environ.rel_context env) then + (named_context_val env, typ, inst_vars, empty_csubst, []) + else + let avoid = List.fold_right Id.Set.add ids Id.Set.empty in + let inst_rels = List.rev (rel_list 0 (nb_rel env)) in + (* move the rel context to a named context and extend the named instance *) + (* with vars of the rel context *) + (* We do keep the instances corresponding to local definition (see above) *) + let (subst, vsubst, _, env) = + Context.Rel.fold_outside push_rel_decl_to_named_context + (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) in + (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst) (*------------------------------------* * Entry points to define new evars * diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 5b6bad349..52f935bf6 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -447,7 +447,6 @@ object(self) | Processed, Some (id,sentence) -> log "Processed" id; remove_flag sentence `PROCESSING; - remove_flag sentence `ERROR; self#mark_as_needed sentence | ProcessingIn _, Some (id,sentence) -> log "ProcessingIn" id; @@ -561,13 +560,19 @@ object(self) condition returns true; it is fed with the number of phrases read and the iters enclosing the current sentence. *) method private fill_command_queue until queue = + let topstack = + if Doc.focused document then fst (Doc.context document) else [] in let rec loop n iter = match Sentence.find buffer iter with | None -> () | Some (start, stop) -> if until n start stop then begin () - end else if stop#backward_char#has_tag Tags.Script.processed then begin + end else if + List.exists (fun (_, s) -> + start#equal (buffer#get_iter_at_mark s.start) && + stop#equal (buffer#get_iter_at_mark s.stop)) topstack + then begin Queue.push (`Skip (start, stop)) queue; loop n stop end else begin diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 8ef7a0554..08f49ae5d 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -500,7 +500,7 @@ let loop () = let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in Feedback.set_logger (slave_logger xml_oc); - Feedback.set_feeder (slave_feeder xml_oc); + Feedback.add_feeder (slave_feeder xml_oc); (* We'll handle goal fetching and display in our own way *) Vernacentries.enable_goal_printing := false; Vernacentries.qed_display_script := false; diff --git a/ide/xml_printer.ml b/ide/xml_printer.ml index e7e4d0ceb..40ab4ce9c 100644 --- a/ide/xml_printer.ml +++ b/ide/xml_printer.ml @@ -17,65 +17,65 @@ type t = target let make x = x let buffer_pcdata tmp text = - let output = Buffer.add_string tmp in - let output' = Buffer.add_char tmp in + let puts = Buffer.add_string tmp in + let putc = Buffer.add_char tmp in let l = String.length text in for p = 0 to l-1 do match text.[p] with - | ' ' -> output " "; - | '>' -> output ">" - | '<' -> output "<" + | ' ' -> puts " "; + | '>' -> puts ">" + | '<' -> puts "<" | '&' -> if p < l - 1 && text.[p + 1] = '#' then - output' '&' + putc '&' else - output "&" - | '\'' -> output "'" - | '"' -> output """ - | c -> output' c + puts "&" + | '\'' -> puts "'" + | '"' -> puts """ + | c -> putc c done let buffer_attr tmp (n,v) = - let output = Buffer.add_string tmp in - let output' = Buffer.add_char tmp in - output' ' '; - output n; - output "=\""; + let puts = Buffer.add_string tmp in + let putc = Buffer.add_char tmp in + putc ' '; + puts n; + puts "=\""; let l = String.length v in for p = 0 to l - 1 do match v.[p] with - | '\\' -> output "\\\\" - | '"' -> output "\\\"" - | '<' -> output "<" - | '&' -> output "&" - | c -> output' c + | '\\' -> puts "\\\\" + | '"' -> puts "\\\"" + | '<' -> puts "<" + | '&' -> puts "&" + | c -> putc c done; - output' '"' + putc '"' let to_buffer tmp x = let pcdata = ref false in - let output = Buffer.add_string tmp in - let output' = Buffer.add_char tmp in + let puts = Buffer.add_string tmp in + let putc = Buffer.add_char tmp in let rec loop = function | Element (tag,alist,[]) -> - output' '<'; - output tag; + putc '<'; + puts tag; List.iter (buffer_attr tmp) alist; - output "/>"; + puts "/>"; pcdata := false; | Element (tag,alist,l) -> - output' '<'; - output tag; + putc '<'; + puts tag; List.iter (buffer_attr tmp) alist; - output' '>'; + putc '>'; pcdata := false; List.iter loop l; - output "</"; - output tag; - output' '>'; + puts "</"; + puts tag; + putc '>'; pcdata := false; | PCData text -> - if !pcdata then output' ' '; + if !pcdata then putc ' '; buffer_pcdata tmp text; pcdata := true; in @@ -93,42 +93,42 @@ let to_string x = let to_string_fmt x = let tmp = Buffer.create 200 in - let output = Buffer.add_string tmp in - let output' = Buffer.add_char tmp in + let puts = Buffer.add_string tmp in + let putc = Buffer.add_char tmp in let rec loop ?(newl=false) tab = function | Element (tag, alist, []) -> - output tab; - output' '<'; - output tag; + puts tab; + putc '<'; + puts tag; List.iter (buffer_attr tmp) alist; - output "/>"; - if newl then output' '\n'; + puts "/>"; + if newl then putc '\n'; | Element (tag, alist, [PCData text]) -> - output tab; - output' '<'; - output tag; + puts tab; + putc '<'; + puts tag; List.iter (buffer_attr tmp) alist; - output ">"; + puts ">"; buffer_pcdata tmp text; - output "</"; - output tag; - output' '>'; - if newl then output' '\n'; + puts "</"; + puts tag; + putc '>'; + if newl then putc '\n'; | Element (tag, alist, l) -> - output tab; - output' '<'; - output tag; + puts tab; + putc '<'; + puts tag; List.iter (buffer_attr tmp) alist; - output ">\n"; + puts ">\n"; List.iter (loop ~newl:true (tab^" ")) l; - output tab; - output "</"; - output tag; - output' '>'; - if newl then output' '\n'; + puts tab; + puts "</"; + puts tag; + putc '>'; + if newl then putc '\n'; | PCData text -> buffer_pcdata tmp text; - if newl then output' '\n'; + if newl then putc '\n'; in loop "" x; Buffer.contents tmp diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 3177b5fae..925214899 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -217,17 +217,9 @@ and eval_to_patch env (buff,pl,fv) = eval_tcode tc vm_env and val_of_constr env c = - let (_,fun_code,_ as ccfv) = - try match compile true env c with - | Some v -> v - | None -> assert false - with reraise -> - let reraise = CErrors.push reraise in - let () = print_string "can not compile \n" in - let () = Format.print_flush () in - iraise reraise - in - eval_to_patch env (to_memory ccfv) + match compile true env c with + | Some v -> eval_to_patch env (to_memory v) + | None -> assert false let set_transparent_const kn = () (* !?! *) let set_opaque_const kn = () (* !?! *) diff --git a/lib/feedback.ml b/lib/feedback.ml index 0ec3b2ebe..4bda936f2 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -125,8 +125,8 @@ let msg_error ?loc x = !logger ?loc Error x let msg_debug ?loc x = !logger ?loc Debug x (** Feeders *) -let feeder = ref ignore -let set_feeder f = feeder := f +let feeders = ref [] +let add_feeder f = feeders := f :: !feeders let feedback_id = ref (Edit 0) let feedback_route = ref default_route @@ -135,11 +135,12 @@ let set_id_for_feedback ?(route=default_route) i = feedback_id := i; feedback_route := route let feedback ?id ?route what = - !feeder { + let m = { contents = what; route = Option.default !feedback_route route; id = Option.default !feedback_id id; - } + } in + List.iter (fun f -> f m) !feeders let feedback_logger ?loc lvl msg = feedback ~route:!feedback_route ~id:!feedback_id diff --git a/lib/feedback.mli b/lib/feedback.mli index d72524e65..d19517bb9 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -83,8 +83,8 @@ val feedback_logger : logger val emacs_logger : logger -(** [set_feeder] A feeder processes the feedback, [ignore] by default *) -val set_feeder : (feedback -> unit) -> unit +(** [add_feeder] feeders observe the feedback *) +val add_feeder : (feedback -> unit) -> unit (** [feedback ?id ?route fb] produces feedback fb, with [route] and [id] set appropiatedly, if absent, it will use the defaults set by diff --git a/library/goptions.ml b/library/goptions.ml index 0459417fb..1cf25987b 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -365,8 +365,8 @@ let set_string_option_value = set_string_option_value_gen None let msg_option_value (name,v) = match v with - | BoolValue true -> str "true" - | BoolValue false -> str "false" + | BoolValue true -> str "on" + | BoolValue false -> str "off" | IntValue (Some n) -> int n | IntValue None -> str "undefined" | StringValue s -> str s diff --git a/library/summary.ml b/library/summary.ml index 4fef06438..6efa07f38 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -186,4 +186,29 @@ let ref ?(freeze=fun _ r -> r) ~name x = init_function = (fun () -> r := x) }; r +module Local = struct + +type 'a local_ref = ('a CEphemeron.key * string) ref + +let (:=) r v = r := (CEphemeron.create v, snd !r) + +let (!) r = + let key, name = !r in + try CEphemeron.get key + with CEphemeron.InvalidKey -> + let _, { init_function } = + Int.Map.find (String.hash (mangle name)) !summaries in + init_function (); + CEphemeron.get (fst !r) + +let ref ?(freeze=fun x -> x) ~name init = + let r = Pervasives.ref (CEphemeron.create init, name) in + declare_summary name + { freeze_function = (fun _ -> freeze !r); + unfreeze_function = ((:=) r); + init_function = (fun () -> r := init) }; + r + +end + let dump = Dyn.dump diff --git a/library/summary.mli b/library/summary.mli index 27889cab2..1b57613cb 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -42,6 +42,17 @@ val declare_summary : string -> 'a summary_declaration -> unit val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref +(* As [ref] but the value is local to a process, i.e. not sent to, say, proof + * workers. It is useful to implement a local cache for example. *) +module Local : sig + + type 'a local_ref + val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref + val (:=) : 'a local_ref -> 'a -> unit + val (!) : 'a local_ref -> 'a + +end + (** Special name for the summary of ML modules. This summary entry is special because its unfreeze may load ML code and hence add summary entries. Thus is has to be recognizable, and handled appropriately *) diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4 index 7a2097515..82b79c883 100644 --- a/ltac/g_rewrite.ml4 +++ b/ltac/g_rewrite.ml4 @@ -106,17 +106,11 @@ END let db_strat db = StratUnary (Topdown, StratHints (false, db)) let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db)) -let cl_rewrite_clause_db = - if Flags.profile then - let key = Profile.declare_profile "cl_rewrite_clause_db" in - Profile.profile3 key cl_rewrite_clause_db - else cl_rewrite_clause_db - TACTIC EXTEND rewrite_strat -| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ Proofview.V82.tactic (cl_rewrite_clause_strat s (Some id)) ] -| [ "rewrite_strat" rewstrategy(s) ] -> [ Proofview.V82.tactic (cl_rewrite_clause_strat s None) ] -| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ Proofview.V82.tactic (cl_rewrite_clause_db db (Some id)) ] -| [ "rewrite_db" preident(db) ] -> [ Proofview.V82.tactic (cl_rewrite_clause_db db None) ] +| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ cl_rewrite_clause_strat s (Some id) ] +| [ "rewrite_strat" rewstrategy(s) ] -> [ cl_rewrite_clause_strat s None ] +| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ cl_rewrite_clause_db db (Some id) ] +| [ "rewrite_db" preident(db) ] -> [ cl_rewrite_clause_db db None ] END let clsubstitute o c = @@ -125,7 +119,7 @@ let clsubstitute o c = (fun cl -> match cl with | Some id when is_tac id -> tclIDTAC - | _ -> cl_rewrite_clause c o AllOccurrences cl) + | _ -> Proofview.V82.of_tactic (cl_rewrite_clause c o AllOccurrences cl)) TACTIC EXTEND substitute | [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ Proofview.V82.tactic (clsubstitute o c) ] @@ -136,15 +130,15 @@ END TACTIC EXTEND setoid_rewrite [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ] - -> [ Proofview.V82.tactic (cl_rewrite_clause c o AllOccurrences None) ] + -> [ cl_rewrite_clause c o AllOccurrences None ] | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] -> - [ Proofview.V82.tactic (cl_rewrite_clause c o AllOccurrences (Some id))] + [ cl_rewrite_clause c o AllOccurrences (Some id) ] | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] -> - [ Proofview.V82.tactic (cl_rewrite_clause c o (occurrences_of occ) None)] + [ cl_rewrite_clause c o (occurrences_of occ) None ] | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] -> - [ Proofview.V82.tactic (cl_rewrite_clause c o (occurrences_of occ) (Some id))] + [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ] | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ)] -> - [ Proofview.V82.tactic (cl_rewrite_clause c o (occurrences_of occ) (Some id))] + [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ] END VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index fb71becfc..3661fe54f 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -11,6 +11,8 @@ open Pp open Printer open Util +module M = CString.Map + (** [is_profiling] and the profiling info ([stack]) should be synchronized with the document; the rest of the ref cells are either local to individual tactic invocations, or global flags, and need not be synchronized, since no @@ -21,10 +23,6 @@ let is_profiling = Flags.profile_ltac let set_profiling b = is_profiling := b let get_profiling () = !is_profiling -let new_call = ref false -let entered_call () = new_call := true -let is_new_call () = let b = !new_call in new_call := false; b - (** LtacProf cannot yet handle backtracking into multi-success tactics. To properly support this, we'd have to somehow recreate our location in the call-stack, and stop/restart the intervening timers. This is tricky and @@ -35,7 +33,7 @@ let encountered_multi_success_backtracking = ref false let warn_profile_backtracking = CWarnings.create ~name:"profile-backtracking" ~category:"ltac" (fun () -> strbrk "Ltac Profiler cannot yet handle backtracking \ - into multi-success tactics; profiling results may be wildly inaccurate.") + into multi-success tactics; profiling results may be wildly inaccurate.") let warn_encountered_multi_success_backtracking () = if !encountered_multi_success_backtracking then @@ -48,164 +46,92 @@ let encounter_multi_success_backtracking () = warn_encountered_multi_success_backtracking () end -type entry = { - mutable total : float; - mutable local : float; - mutable ncalls : int; - mutable max_total : float -} - -let empty_entry () = { total = 0.; local = 0.; ncalls = 0; max_total = 0. } -let add_entry e add_total { total; local; ncalls; max_total } = - if add_total then e.total <- e.total +. total; - e.local <- e.local +. local; - e.ncalls <- e.ncalls + ncalls; - if add_total then e.max_total <- max e.max_total max_total +(* *************** tree data structure for profiling ****************** *) type treenode = { - entry : entry; - children : (string, treenode) Hashtbl.t + name : M.key; + total : float; + local : float; + ncalls : int; + max_total : float; + children : treenode M.t } -let empty_treenode n = { entry = empty_entry (); children = Hashtbl.create n } - -(** Tobias Tebbi wrote some tricky code involving mutation. Rather than - rewriting it in a functional style, we simply freeze the state when we need - to by issuing a deep copy of the profiling data. *) -(** TODO: rewrite me in purely functional style *) -let deepcopy_entry { total; local; ncalls; max_total } = - { total; local; ncalls; max_total } - -let rec deepcopy_treenode { entry; children } = - let children' = Hashtbl.create (Hashtbl.length children) in - let iter key subtree = Hashtbl.add children' key (deepcopy_treenode subtree) in - let () = Hashtbl.iter iter children in - { entry = deepcopy_entry entry; children = children' } - -let stack = - let freeze _ = List.map deepcopy_treenode in - Summary.ref ~freeze [empty_treenode 20] ~name:"LtacProf-stack" - -let on_stack = Hashtbl.create 5 +let empty_treenode name = { + name; + total = 0.0; + local = 0.0; + ncalls = 0; + max_total = 0.0; + children = M.empty; +} -let get_node c table = - try Hashtbl.find table c - with Not_found -> - let new_node = empty_treenode 5 in - Hashtbl.add table c new_node; - new_node +let root = "root" -let rec add_node node node' = - add_entry node.entry true node'.entry; - Hashtbl.iter - (fun s node' -> add_node (get_node s node.children) node') - node'.children +module Local = Summary.Local -let time () = - let times = Unix.times () in - times.Unix.tms_utime +. times.Unix.tms_stime +let stack = Local.ref ~name:"LtacProf-stack" [empty_treenode root] -(* -let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) -let msgnl strm = msgnl_with !Pp_control.std_ft strm - -let rec print_treenode indent (tn : treenode) = - msgnl (str (indent^"{ entry = {")); - Feedback.msg_notice (str (indent^"total = ")); - msgnl (str (indent^(string_of_float (tn.entry.total)))); - Feedback.msg_notice (str (indent^"local = ")); - msgnl (str (indent^(string_of_float tn.entry.local))); - Feedback.msg_notice (str (indent^"ncalls = ")); - msgnl (str (indent^(string_of_int tn.entry.ncalls))); - Feedback.msg_notice (str (indent^"max_total = ")); - msgnl (str (indent^(string_of_float tn.entry.max_total))); - msgnl (str (indent^"}")); - msgnl (str (indent^"children = {")); - Hashtbl.iter - (fun s node -> - msgnl (str (indent^" "^s^" |-> ")); - print_treenode (indent^" ") node - ) - tn.children; - msgnl (str (indent^"} }")) - -let rec print_stack (st : treenode list) = match st with -| [] -> msgnl (str "[]") -| x :: xs -> print_treenode "" x; msgnl (str ("::")); print_stack xs -*) - -let string_of_call ck = - let s = - string_of_ppcmds - (match ck with - | Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s - | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst - | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id - | Tacexpr.LtacAtomCall te -> - (Pptactic.pr_glob_tactic (Global.env ()) - (Tacexpr.TacAtom (Loc.ghost, te))) - | Tacexpr.LtacConstrInterp (c, _) -> - pr_glob_constr_env (Global.env ()) c - | Tacexpr.LtacMLCall te -> - (Pptactic.pr_glob_tactic (Global.env ()) - te) - ) in - for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done; - let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in - CString.strip s - -let exit_tactic start_time add_total c = match !stack with -| [] | [_] -> - (* oops, our stack is invalid *) - encounter_multi_success_backtracking () -| node :: (parent :: _ as stack') -> - stack := stack'; - if add_total then Hashtbl.remove on_stack (string_of_call c); - let diff = time () -. start_time in - parent.entry.local <- parent.entry.local -. diff; - let node' = { total = diff; local = diff; ncalls = 1; max_total = diff } in - add_entry node.entry add_total node' - -let tclFINALLY tac (finally : unit Proofview.tactic) = - let open Proofview.Notations in - Proofview.tclIFCATCH - tac - (fun v -> finally <*> Proofview.tclUNIT v) - (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn) +let reset_profile () = + Local.(stack := [empty_treenode root]); + encountered_multi_success_backtracking := false -let do_profile s call_trace tac = - let open Proofview.Notations in - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - if !is_profiling && is_new_call () then - match call_trace with - | (_, c) :: _ -> - let s = string_of_call c in - let parent = List.hd !stack in - let node, add_total = try Hashtbl.find on_stack s, false - with Not_found -> - let node = get_node s parent.children in - Hashtbl.add on_stack s node; - node, true - in - if not add_total && node = List.hd !stack then None else ( - stack := node :: !stack; - let start_time = time () in - Some (start_time, add_total) - ) - | [] -> None - else None)) >>= function - | Some (start_time, add_total) -> - tclFINALLY - tac - (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - (match call_trace with - | (_, c) :: _ -> - exit_tactic start_time add_total c - | [] -> ())))) - | None -> tac +(* ************** XML Serialization ********************* *) +let rec of_ltacprof_tactic (name, t) = + assert (String.equal name t.name); + let open Xml_datatype in + let total = string_of_float t.total in + let local = string_of_float t.local in + let ncalls = string_of_int t.ncalls in + let max_total = string_of_float t.max_total in + let children = List.map of_ltacprof_tactic (M.bindings t.children) in + Element ("ltacprof_tactic", + [ ("name", name); ("total",total); ("local",local); + ("ncalls",ncalls); ("max_total",max_total)], + children) + +let of_ltacprof_results t = + let open Xml_datatype in + assert(String.equal t.name root); + let children = List.map of_ltacprof_tactic (M.bindings t.children) in + Element ("ltacprof", [("total_time", string_of_float t.total)], children) +let rec to_ltacprof_tactic m xml = + let open Xml_datatype in + match xml with + | Element ("ltacprof_tactic", + [("name", name); ("total",total); ("local",local); + ("ncalls",ncalls); ("max_total",max_total)], xs) -> + let node = { + name; + total = float_of_string total; + local = float_of_string local; + ncalls = int_of_string ncalls; + max_total = float_of_string max_total; + children = List.fold_left to_ltacprof_tactic M.empty xs; + } in + M.add name node m + | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof_tactic XML") + +let to_ltacprof_results xml = + let open Xml_datatype in + match xml with + | Element ("ltacprof", [("total_time", t)], xs) -> + { name = root; + total = float_of_string t; + ncalls = 0; + max_total = 0.0; + local = 0.0; + children = List.fold_left to_ltacprof_tactic M.empty xs } + | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML") + +let feedback_results results = + Feedback.(feedback + (Custom (Loc.dummy_loc, "ltacprof_results", of_ltacprof_results results))) + +(* ************** pretty printing ************************************* *) let format_sec x = (Printf.sprintf "%.3fs" x) let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x)) @@ -221,13 +147,12 @@ let rec list_iter_is_last f = function | x :: xs -> f false x :: list_iter_is_last f xs let header = - str " tactic self total calls max" ++ + str " tactic local total calls max" ++ fnl () ++ str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘" ++ fnl () -let rec print_node all_total indent prefix (s, n) = - let e = n.entry in +let rec print_node ~filter all_total indent prefix (s, e) = h 0 ( padr_with '-' 40 (prefix ^ s ^ " ") ++ padl 7 (format_ratio (e.local /. all_total)) @@ -235,123 +160,243 @@ let rec print_node all_total indent prefix (s, n) = ++ padl 8 (string_of_int e.ncalls) ++ padl 10 (format_sec (e.max_total)) ) ++ - print_table all_total indent false n.children + print_table ~filter all_total indent false e.children -and print_table all_total indent first_level table = - let fold s n l = if n.entry.total /. all_total < 0.02 then l else (s, n) :: l in - let ls = Hashtbl.fold fold table [] in +and print_table ~filter all_total indent first_level table = + let fold _ n l = + let s, total = n.name, n.total in + if filter s then (s, n) :: l else l in + let ls = M.fold fold table [] in match ls with | [s, n] when not first_level -> - print_node all_total indent (indent ^ "└") (s, n) + v 0 (print_node ~filter all_total indent (indent ^ "└") (s, n)) | _ -> - let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in + let ls = + List.sort (fun (_, { total = s1 }) (_, { total = s2}) -> + compare s2 s1) ls in let iter is_last = - let sep0 = if first_level then "" else if is_last then " " else " │" in - let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in - print_node all_total (indent ^ sep0) (indent ^ sep1) + let sep0 = if first_level then "" else if is_last then " " else " │" in + let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in + print_node ~filter all_total (indent ^ sep0) (indent ^ sep1) in prlist_with_sep fnl (fun pr -> pr) (list_iter_is_last iter ls) -let get_results_string () = - let tree = (List.hd !stack).children in - let all_total = -. (List.hd !stack).entry.local in - let global = Hashtbl.create 20 in - let rec cumulate table = - let iter s node = - let node' = get_node s global in - add_entry node'.entry true node.entry; - cumulate node.children +let to_string ~filter node = + let tree = node.children in + let all_total = M.fold (fun _ { total } a -> total +. a) node.children 0.0 in + let flat_tree = + let global = ref M.empty in + let find_tactic tname l = + try M.find tname !global + with Not_found -> + let e = empty_treenode tname in + global := M.add tname e !global; + e in + let add_tactic tname stats = global := M.add tname stats !global in + let sum_stats add_total + { name; total = t1; local = l1; ncalls = n1; max_total = m1 } + { total = t2; local = l2; ncalls = n2; max_total = m2 } = { + name; + total = if add_total then t1 +. t2 else t1; + local = l1 +. l2; + ncalls = n1 + n2; + max_total = if add_total then max m1 m2 else m1; + children = M.empty; + } in + let rec cumulate table = + let iter _ ({ name; children } as statistics) = + if filter name then begin + let stats' = find_tactic name global in + add_tactic name (sum_stats true stats' statistics); + end; + cumulate children + in + M.iter iter table in - Hashtbl.iter iter table + cumulate tree; + !global in - cumulate tree; warn_encountered_multi_success_backtracking (); let msg = h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++ fnl () ++ + fnl () ++ header ++ - print_table all_total "" true global ++ + print_table ~filter all_total "" true flat_tree ++ + fnl () ++ fnl () ++ header ++ - print_table all_total "" true tree + print_table ~filter all_total "" true tree in msg +(* ******************** profiling code ************************************** *) -type ltacprof_entry = {total : float; self : float; num_calls : int; max_total : float} -type ltacprof_tactic = {name: string; statistics : ltacprof_entry; tactics : ltacprof_tactic list} -type ltacprof_results = {total_time : float; tactics : ltacprof_tactic list} +let get_child name node = + try M.find name node.children + with Not_found -> empty_treenode name -let to_ltacprof_entry (e: entry) : ltacprof_entry = - {total=e.total; self=e.local; num_calls=e.ncalls; max_total=e.max_total} +let time () = + let times = Unix.times () in + times.Unix.tms_utime +. times.Unix.tms_stime -let rec to_ltacprof_tactic (name: string) (t: treenode) : ltacprof_tactic = - { name = name; statistics = to_ltacprof_entry t.entry; tactics = to_ltacprof_treenode t.children } -and to_ltacprof_treenode (table: (string, treenode) Hashtbl.t) : ltacprof_tactic list = - Hashtbl.fold (fun name' t' c -> to_ltacprof_tactic name' t'::c) table [] +let string_of_call ck = + let s = + string_of_ppcmds + (match ck with + | Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s + | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst + | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id + | Tacexpr.LtacAtomCall te -> + (Pptactic.pr_glob_tactic (Global.env ()) + (Tacexpr.TacAtom (Loc.ghost, te))) + | Tacexpr.LtacConstrInterp (c, _) -> + pr_glob_constr_env (Global.env ()) c + | Tacexpr.LtacMLCall te -> + (Pptactic.pr_glob_tactic (Global.env ()) + te) + ) in + for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done; + let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in + CString.strip s -let get_profiling_results() : ltacprof_results = - let tree = List.hd !stack in - { total_time = -. tree.entry.local; tactics = to_ltacprof_treenode tree.children } +let rec merge_sub_tree name tree acc = + try + let t = M.find name acc in + let t = { + name; + total = t.total +. tree.total; + ncalls = t.ncalls + tree.ncalls; + local = t.local +. tree.local; + max_total = max t.max_total tree.max_total; + children = M.fold merge_sub_tree tree.children t.children; + } in + M.add name t acc + with Not_found -> M.add name tree acc + +let merge_roots ?(disjoint=true) t1 t2 = + assert(String.equal t1.name t2.name); + { name = t1.name; + ncalls = t1.ncalls + t2.ncalls; + local = if disjoint then t1.local +. t2.local else t1.local; + total = if disjoint then t1.total +. t2.total else t1.total; + max_total = if disjoint then max t1.max_total t2.max_total else t1.max_total; + children = + M.fold merge_sub_tree t2.children t1.children } + +let rec find_in_stack what acc = function + | [] -> None + | { name } as x :: rest when String.equal name what -> Some(acc, x, rest) + | { name } as x :: rest -> find_in_stack what (x :: acc) rest + +let exit_tactic start_time c = + let diff = time () -. start_time in + match Local.(!stack) with + | [] | [_] -> + (* oops, our stack is invalid *) + encounter_multi_success_backtracking (); + reset_profile () + | node :: (parent :: rest as full_stack) -> + let name = string_of_call c in + if not (String.equal name node.name) then + (* oops, our stack is invalid *) + encounter_multi_success_backtracking (); + let node = { node with + total = node.total +. diff; + local = node.local +. diff; + ncalls = node.ncalls + 1; + max_total = max node.max_total diff; + } in + (* updating the stack *) + let parent = + match find_in_stack node.name [] full_stack with + | None -> + (* no rec-call, we graft the subtree *) + let parent = { parent with + local = parent.local -. diff; + children = M.add node.name node parent.children } in + Local.(stack := parent :: rest); + parent + | Some(to_update, self, rest) -> + (* we coalesce the rec-call and update the lower stack *) + let self = merge_roots ~disjoint:false self node in + let updated_stack = + List.fold_left (fun s x -> + (try M.find x.name (List.hd s).children + with Not_found -> x) :: s) (self :: rest) to_update in + Local.(stack := updated_stack); + List.hd Local.(!stack) + in + (* Calls are over, we reset the stack and send back data *) + if rest == [] && get_profiling () then begin + assert(String.equal root parent.name); + reset_profile (); + feedback_results parent + end -let rec of_ltacprof_tactic t = - let open Xml_datatype in - let total = string_of_float t.statistics.total in - let self = string_of_float t.statistics.self in - let num_calls = string_of_int t.statistics.num_calls in - let max_total = string_of_float t.statistics.max_total in - let children = List.map of_ltacprof_tactic t.tactics in - Element ("ltacprof_tactic", [("name", t.name); ("total",total); ("self",self); ("num_calls",num_calls); ("max_total",max_total)], children) - -let rec of_ltacprof_results t = - let open Xml_datatype in - let children = List.map of_ltacprof_tactic t.tactics in - Element ("ltacprof", [("total_time", string_of_float t.total_time)], children) +let tclFINALLY tac (finally : unit Proofview.tactic) = + let open Proofview.Notations in + Proofview.tclIFCATCH + tac + (fun v -> finally <*> Proofview.tclUNIT v) + (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn) + +let do_profile s call_trace tac = + let open Proofview.Notations in + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + if !is_profiling then + match call_trace, Local.(!stack) with + | (_, c) :: _, parent :: rest -> + let name = string_of_call c in + let node = get_child name parent in + Local.(stack := node :: parent :: rest); + Some (time ()) + | _ :: _, [] -> assert false + | _ -> None + else None)) >>= function + | Some start_time -> + tclFINALLY + tac + (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + (match call_trace with + | (_, c) :: _ -> exit_tactic start_time c + | [] -> ())))) + | None -> tac +(* ************** Accumulation of data from workers ************************* *) -let get_profile_xml() = - of_ltacprof_results (get_profiling_results()) +let get_local_profiling_results () = List.hd Local.(!stack) -let print_results () = - Feedback.msg_notice (get_results_string()); - Feedback.feedback (Feedback.Custom (Loc.dummy_loc, "ltacprof_results", get_profile_xml())) +module SM = Map.Make(Stateid.Self) - (* FOR DEBUGGING *) - (* ; - msgnl (str""); - print_stack (!stack) - *) +let data = ref SM.empty -let print_results_tactic tactic = - let tree = (List.hd !stack).children in - let table_tactic = Hashtbl.create 20 in - let rec cumulate table = - let iter s node = - if String.sub (s ^ ".") 0 (min (1 + String.length s) (String.length tactic)) = tactic - then add_node (get_node s table_tactic) node - else cumulate node.children - in - Hashtbl.iter iter table - in - cumulate tree; - let all_total = -. (List.hd !stack).entry.local in - let tactic_total = - Hashtbl.fold - (fun _ node all_total -> node.entry.total +. all_total) - table_tactic 0. in - warn_encountered_multi_success_backtracking (); - let msg = - h 0 (str"total time: " ++ padl 11 (format_sec (all_total))) ++ - h 0 (str"time spent in tactic: " ++ padl 11 (format_sec (tactic_total))) ++ - fnl () ++ - header ++ - print_table tactic_total "" true table_tactic - in - Feedback.msg_notice msg +let _ = + Feedback.(add_feeder (function + | { id = State s; contents = Custom (_, "ltacprof_results", xml) } -> + let results = to_ltacprof_results xml in + let other_results = (* Multi success can cause this *) + try SM.find s !data + with Not_found -> empty_treenode root in + data := SM.add s (merge_roots results other_results) !data + | _ -> ())) + +(* ******************** *) + +let print_results_filter ~filter = + let valid id _ = Stm.state_of_id id <> `Expired in + data := SM.filter valid !data; + let results = + SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in + let results = merge_roots results Local.(CList.last !stack) in + Feedback.msg_notice (to_string ~filter results) +;; + +let print_results () = print_results_filter ~filter:(fun _ -> true) -let reset_profile () = - stack := [empty_treenode 20]; - encountered_multi_success_backtracking := false +let print_results_tactic tactic = + print_results_filter ~filter:(fun s -> + String.(equal tactic (sub (s ^ ".") 0 (min (1+length s) (length tactic))))) let do_print_results_at_close () = if get_profiling () then print_results () diff --git a/ltac/profile_ltac.mli b/ltac/profile_ltac.mli index 8e029bb2e..8c4b47b8e 100644 --- a/ltac/profile_ltac.mli +++ b/ltac/profile_ltac.mli @@ -8,14 +8,12 @@ (** Ltac profiling primitives *) -val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> 'b Proofview.tactic -> 'b Proofview.tactic +val do_profile : + string -> ('a * Tacexpr.ltac_call_kind) list -> + 'b Proofview.tactic -> 'b Proofview.tactic val set_profiling : bool -> unit -val get_profiling : unit -> bool - -val entered_call : unit -> unit - val print_results : unit -> unit val print_results_tactic : string -> unit @@ -30,24 +28,20 @@ val do_print_results_at_close : unit -> unit * statistics of the two invocations combined, and also combined over all * invocations of 'aaa'. * total: time spent running this tactic and its subtactics (seconds) - * self: time spent running this tactic, minus its subtactics (seconds) - * num_calls: the number of invocations of this tactic that have been made + * local: time spent running this tactic, minus its subtactics (seconds) + * ncalls: the number of invocations of this tactic that have been made * max_total: the greatest running time of a single invocation (seconds) *) -type ltacprof_entry = {total : float; self : float; num_calls : int; max_total : float} -(* A profiling entry for a tactic and the tactics that it called - * name: name of the tactic - * statistics: profiling data collected - * tactics: profiling results for each tactic that this tactic invoked; - * multiple invocations of the same sub-tactic are combined together. - *) -type ltacprof_tactic = {name: string; statistics : ltacprof_entry; tactics : ltacprof_tactic list} -(* The full results of profiling - * total_time: time spent running tactics (seconds) - * tactics: the tactics that have been invoked since profiling was started or reset - *) -type ltacprof_results = {total_time : float; tactics : ltacprof_tactic list} - -(* Returns the profiling results for the currently-focused state. *) -val get_profiling_results : unit -> ltacprof_results +type treenode = { + name : CString.Map.key; + total : float; + local : float; + ncalls : int; + max_total : float; + children : treenode CString.Map.t +} + +(* Returns the profiling results known by the current process *) +val get_local_profiling_results : unit -> treenode +val feedback_results : treenode -> unit diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 153ca5bf5..b559864bd 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -15,7 +15,7 @@ open Namegen open Term open Vars open Reduction -open Tacticals +open Tacticals.New open Tacmach open Tactics open Pretype_errors @@ -628,7 +628,7 @@ let solve_remaining_by env sigma holes by = | Genarg.GenArg (Genarg.Glbwit tag, tac) -> Ftactic.run (Geninterp.interp tag ist tac) (fun _ -> Proofview.tclUNIT ()) in - let solve_tac = Tacticals.New.tclCOMPLETE solve_tac in + let solve_tac = tclCOMPLETE solve_tac in let solve sigma evk = let evi = try Some (Evd.find_undefined sigma evk) @@ -1579,7 +1579,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let gls = List.rev (Evd.fold_undefined fold undef []) in match clause, prf with | Some id, Some p -> - let tac = Tacticals.New.tclTHENLIST [ + let tac = tclTHENLIST [ Refine.refine ~unsafe:false { run = fun h -> Sigma.here p h }; beta_hyp id; Proofview.Unsafe.tclNEWGOALS gls; @@ -1635,23 +1635,25 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = end } let tactic_init_setoid () = - try init_setoid (); tclIDTAC - with e when CErrors.noncritical e -> tclFAIL 0 (str"Setoid library not loaded") + try init_setoid (); Proofview.tclUNIT () + with e when CErrors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Setoid library not loaded") let cl_rewrite_clause_strat progress strat clause = - tclTHEN (tactic_init_setoid ()) - ((if progress then tclWEAK_PROGRESS else fun x -> x) - (fun gl -> - try Proofview.V82.of_tactic (cl_rewrite_clause_newtac ~progress strat clause) gl - with RewriteFailure e -> - errorlabstrm "" (str"setoid rewrite failed: " ++ e) + tactic_init_setoid () <*> + (if progress then Proofview.tclPROGRESS else fun x -> x) + (Proofview.tclOR + (cl_rewrite_clause_newtac ~progress strat clause) + (fun (e, info) -> match e with + | RewriteFailure e -> + tclZEROMSG (str"setoid rewrite failed: " ++ e) | Refiner.FailError (n, pp) -> - tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl)) + tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) + | e -> Proofview.tclZERO ~info e)) (** Setoid rewriting when called with "setoid_rewrite" *) -let cl_rewrite_clause l left2right occs clause gl = +let cl_rewrite_clause l left2right occs clause = let strat = rewrite_with left2right (general_rewrite_unif_flags ()) l occs in - cl_rewrite_clause_strat true strat clause gl + cl_rewrite_clause_strat true strat clause (** Setoid rewriting when called with "rewrite_strat" *) let cl_rewrite_clause_strat strat clause = @@ -2031,12 +2033,12 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env = abs, sigma, res, Sorts.is_prop sort let get_hyp gl (c,l) clause l2r = - let evars = project gl in - let env = pf_env gl in + let evars = Tacmach.New.project gl in + let env = Tacmach.New.pf_env gl in let sigma, hi = decompose_applied_relation env evars (c,l) in let but = match clause with - | Some id -> pf_get_hyp_typ gl id - | None -> Evarutil.nf_evar evars (pf_concl gl) + | Some id -> Tacmach.New.pf_get_hyp_typ id gl + | None -> Evarutil.nf_evar evars (Tacmach.New.pf_concl gl) in unification_rewrite l2r hi.c1 hi.c2 sigma hi.prf hi.car hi.rel but env @@ -2046,7 +2048,8 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } (* let cl_rewrite_clause_tac = Profile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) (** Setoid rewriting when called with "rewrite" *) -let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = +let general_s_rewrite cl l2r occs (c,l) ~new_goals = + Proofview.Goal.nf_enter { enter = begin fun gl -> let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in let unify env evars t = unify_abs res l2r sort env evars t in let app = apply_rule unify occs in @@ -2057,31 +2060,25 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = (), res } in - let origsigma = project gl in - init_setoid (); - try - tclWEAK_PROGRESS + let origsigma = Tacmach.New.project gl in + tactic_init_setoid () <*> + Proofview.tclOR + (tclPROGRESS (tclTHEN - (Refiner.tclEVARS evd) - (Proofview.V82.of_tactic - (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl))) gl - with RewriteFailure e -> - tclFAIL 0 (str"setoid rewrite failed: " ++ e) gl - -let general_s_rewrite_clause x = - match x with - | None -> general_s_rewrite None - | Some id -> general_s_rewrite (Some id) - -let general_s_rewrite_clause x y z w ~new_goals = - Proofview.V82.tactic (general_s_rewrite_clause x y z w ~new_goals) + (Proofview.Unsafe.tclEVARS evd) + (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl))) + (fun (e, info) -> match e with + | RewriteFailure e -> + tclFAIL 0 (str"setoid rewrite failed: " ++ e) + | e -> Proofview.tclZERO ~info e) + end } -let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite_clause +let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite (** [setoid_]{reflexivity,symmetry,transitivity} tactics *) let not_declared env ty rel = - Tacticals.New.tclFAIL 0 + tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env Evd.empty rel ++ str" is not a declared " ++ str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library") @@ -2118,8 +2115,7 @@ let setoid_proof ty fn fallback = end } let tac_open ((evm,_), c) tac = - Proofview.V82.tactic - (tclTHEN (Refiner.tclEVARS evm) (tac c)) + (tclTHEN (Proofview.Unsafe.tclEVARS evm) (tac c)) let poly_proof getp gett env evm car rel = if Sorts.is_prop (sort_of_rel env evm rel) then @@ -2132,7 +2128,7 @@ let setoid_reflexivity = tac_open (poly_proof PropGlobal.get_reflexive_proof TypeGlobal.get_reflexive_proof env evm car rel) - (fun c -> tclCOMPLETE (Proofview.V82.of_tactic (apply c)))) + (fun c -> tclCOMPLETE (apply c))) (reflexivity_red true) let setoid_symmetry = @@ -2141,7 +2137,7 @@ let setoid_symmetry = tac_open (poly_proof PropGlobal.get_symmetric_proof TypeGlobal.get_symmetric_proof env evm car rel) - (fun c -> Proofview.V82.of_tactic (apply c))) + (fun c -> apply c)) (symmetry_red true) let setoid_transitivity c = @@ -2150,8 +2146,8 @@ let setoid_transitivity c = tac_open (poly_proof PropGlobal.get_transitive_proof TypeGlobal.get_transitive_proof env evm car rel) (fun proof -> match c with - | None -> Proofview.V82.of_tactic (eapply proof) - | Some c -> Proofview.V82.of_tactic (apply_with_bindings (proof,ImplicitBindings [ c ])))) + | None -> eapply proof + | Some c -> apply_with_bindings (proof,ImplicitBindings [ c ]))) (transitivity_red true c) let setoid_symmetry_in id = @@ -2169,9 +2165,9 @@ let setoid_symmetry_in id = let new_hyp' = mkApp (he, [| c2 ; c1 |]) in let new_hyp = it_mkProd_or_LetIn new_hyp' binders in Proofview.V82.of_tactic - (Tacticals.New.tclTHENLAST + (tclTHENLAST (Tactics.assert_after_replacing id new_hyp) - (Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ])) + (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ])) gl) let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity diff --git a/ltac/rewrite.mli b/ltac/rewrite.mli index 01709f29f..f448c8543 100644 --- a/ltac/rewrite.mli +++ b/ltac/rewrite.mli @@ -63,12 +63,12 @@ val map_strategy : ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast (** Entry point for user-level "rewrite_strat" *) -val cl_rewrite_clause_strat : strategy -> Id.t option -> tactic +val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic (** Entry point for user-level "setoid_rewrite" *) val cl_rewrite_clause : interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) -> - bool -> Locus.occurrences -> Id.t option -> tactic + bool -> Locus.occurrences -> Id.t option -> unit Proofview.tactic val is_applied_rewrite_relation : env -> evar_map -> Context.Rel.t -> constr -> types option diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 8b2e1ee1a..ddebac5ab 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -289,7 +289,7 @@ let constr_of_id env id = (* Some of the code further down depends on the fact that push_trace does not modify sigma (the evar map) *) let push_trace call ist = match TacStore.get ist.extra f_trace with | None -> Proofview.tclUNIT [call] -| Some trace -> Proofview.tclLIFT (Proofview.NonLogical.make Profile_ltac.entered_call) <*> Proofview.tclUNIT (call :: trace) +| Some trace -> Proofview.tclUNIT (call :: trace) let propagate_trace ist loc id v = let v = Value.normalize v in diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 0e74e6f0c..714e25f85 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -132,13 +132,13 @@ let grammar_delete e reinit (pos,rls) = let grammar_extend e reinit ext = let ext = of_coq_extend_statement ext in let undo () = grammar_delete e reinit ext in - let redo () = camlp4_verbose (maybe_uncurry (G.extend e)) ext in + let redo () = camlp4_verbosity false (maybe_uncurry (G.extend e)) ext in camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state; redo () let grammar_extend_sync e reinit ext = camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state; - camlp4_verbose (maybe_uncurry (G.extend e)) (of_coq_extend_statement ext) + camlp4_verbosity false (maybe_uncurry (G.extend e)) (of_coq_extend_statement ext) (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 90adb0c36..0fbe04b86 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -63,7 +63,7 @@ let _ = declare_bool_option { optsync = true; optdepr = false; - optname = "strict mode"; + optname = "strict proofs"; optkey = ["Strict";"Proofs"]; optread = get_strictness; optwrite = set_strictness } diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index 6974f8d99..47b6f7c7f 100644 --- a/plugins/micromega/Lia.v +++ b/plugins/micromega/Lia.v @@ -30,13 +30,13 @@ Ltac zchange := Ltac zchecker_no_abstract := zchange ; vm_compute ; reflexivity. -Ltac zchecker_abstract := abstract (zchange ; vm_cast_no_check (eq_refl true)). +Ltac zchecker_abstract := zchange ; vm_cast_no_check (eq_refl true). -Ltac zchecker := zchecker_abstract || zchecker_no_abstract . +Ltac zchecker := zchecker_no_abstract. -Ltac lia := preprocess; xlia ; zchecker. +Ltac lia := preprocess; xlia zchecker. -Ltac nia := preprocess; xnlia ; zchecker. +Ltac nia := preprocess; xnlia zchecker. (* Local Variables: *) diff --git a/plugins/micromega/Lqa.v b/plugins/micromega/Lqa.v index e3414b849..acd2751a0 100644 --- a/plugins/micromega/Lqa.v +++ b/plugins/micromega/Lqa.v @@ -25,23 +25,20 @@ Ltac rchange := apply (QTautoChecker_sound __ff __wit). Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity. -Ltac rchecker_abstract := abstract (rchange ; vm_cast_no_check (eq_refl true)). +Ltac rchecker_abstract := rchange ; vm_cast_no_check (eq_refl true). -Ltac rchecker := (rchecker_abstract || rchecker_no_abstract). +Ltac rchecker := rchecker_no_abstract. (** Here, lra stands for linear rational arithmetic *) -Ltac lra := lra_Q ; rchecker. +Ltac lra := lra_Q rchecker. (** Here, nra stands for non-linear rational arithmetic *) -Ltac nra := xnqa ; rchecker. +Ltac nra := xnqa rchecker. Ltac xpsatz dom d := let tac := lazymatch dom with | Q => - (sos_Q || psatz_Q d) ; - (* If csdp is not installed, the previous step might not produce any - progress: the rest of the tactical will then fail. Hence the 'try'. *) - try rchecker + ((sos_Q rchecker) || (psatz_Q d rchecker)) | _ => fail "Unsupported domain" end in tac. diff --git a/plugins/micromega/Lra.v b/plugins/micromega/Lra.v index 4d9cf22dd..5b97d8ed3 100644 --- a/plugins/micromega/Lra.v +++ b/plugins/micromega/Lra.v @@ -26,23 +26,20 @@ Ltac rchange := apply (RTautoChecker_sound __ff __wit). Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity. -Ltac rchecker_abstract := abstract (rchange ; vm_cast_no_check (eq_refl true)). +Ltac rchecker_abstract := rchange ; vm_cast_no_check (eq_refl true). -Ltac rchecker := rchecker_abstract || rchecker_no_abstract. +Ltac rchecker := rchecker_no_abstract. (** Here, lra stands for linear real arithmetic *) -Ltac lra := unfold Rdiv in * ; lra_R ; rchecker. +Ltac lra := unfold Rdiv in * ; lra_R rchecker. (** Here, nra stands for non-linear real arithmetic *) -Ltac nra := unfold Rdiv in * ; xnra ; rchecker. +Ltac nra := unfold Rdiv in * ; xnra rchecker. Ltac xpsatz dom d := let tac := lazymatch dom with | R => - (sos_R || psatz_R d) ; - (* If csdp is not installed, the previous step might not produce any - progress: the rest of the tactical will then fail. Hence the 'try'. *) - try rchecker + (sos_R rchecker) || (psatz_R d rchecker) | _ => fail "Unsupported domain" end in tac. diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 0a41af454..d28bb8286 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -50,7 +50,7 @@ Extract Constant Rinv => "fun x -> 1 / x". Extraction "micromega.ml" List.map simpl_cone (*map_cone indexes*) - denorm Qpower + denorm Qpower vm_add n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index c81c025a5..8acf0ff88 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -35,16 +35,10 @@ Ltac nia := Lia.nia. Ltac xpsatz dom d := let tac := lazymatch dom with | Z => - (sos_Z || psatz_Z d) ; Lia.zchecker + (sos_Z Lia.zchecker) || (psatz_Z d Lia.zchecker) | R => - (sos_R || psatz_R d) ; - (* If csdp is not installed, the previous step might not produce any - progress: the rest of the tactical will then fail. Hence the 'try'. *) - try Lra.rchecker - | Q => (sos_Q || psatz_Q d) ; - (* If csdp is not installed, the previous step might not produce any - progress: the rest of the tactical will then fail. Hence the 'try'. *) - try Lqa.rchecker + (sos_R Lra.rchecker) || (psatz_R d Lra.rchecker) + | Q => (sos_Q Lqa.rchecker) || (psatz_Q d Lqa.rchecker) | _ => fail "Unsupported domain" end in tac. diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v index 4981ddb30..2d2c0bc77 100644 --- a/plugins/micromega/VarMap.v +++ b/plugins/micromega/VarMap.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -26,6 +26,7 @@ Set Implicit Arguments. *) Section MakeVarMap. + Variable A : Type. Variable default : A. @@ -46,5 +47,29 @@ Section MakeVarMap. end. -End MakeVarMap. + Fixpoint singleton (x:positive) (v : A) : t := + match x with + | xH => Leaf v + | xO p => Node (singleton p v) default Empty + | xI p => Node Empty default (singleton p v) + end. + + Fixpoint vm_add (x: positive) (v : A) (m : t) {struct m} : t := + match m with + | Empty => singleton x v + | Leaf vl => + match x with + | xH => Leaf v + | xO p => Node (singleton p v) vl Empty + | xI p => Node Empty vl (singleton p v) + end + | Node l o r => + match x with + | xH => Node l v r + | xI p => Node l o (vm_add p v r) + | xO p => Node (vm_add p v l) o r + end + end. + +End MakeVarMap. diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index faf3b3e69..db8cbf231 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -147,6 +147,17 @@ let rec map_atoms fct f = | N f -> N(map_atoms fct f) | I(f1,o,f2) -> I(map_atoms fct f1, o , map_atoms fct f2) +let rec map_prop fct f = + match f with + | TT -> TT + | FF -> FF + | X x -> X (fct x) + | A (at,tg,cstr) -> A(at,tg,cstr) + | C (f1,f2) -> C(map_prop fct f1, map_prop fct f2) + | D (f1,f2) -> D(map_prop fct f1, map_prop fct f2) + | N f -> N(map_prop fct f) + | I(f1,o,f2) -> I(map_prop fct f1, o , map_prop fct f2) + (** * Collect the identifiers of a (string of) implications. Implication labels * are inherited from Coq/CoC's higher order dependent type constructor (Pi). @@ -292,7 +303,8 @@ let rec add_term t0 = function *) module ISet = Set.Make(Int) - +module IMap = Map.Make(Int) + (** * Given a set of integers s=\{i0,...,iN\} and a list m, return the list of * elements of m that are at position i0,...,iN. @@ -371,6 +383,8 @@ struct let coq_and = lazy (init_constant "and") let coq_or = lazy (init_constant "or") let coq_not = lazy (init_constant "not") + let coq_not_gl_ref = (Nametab.locate ( Libnames.qualid_of_string "Coq.Init.Logic.not")) + let coq_iff = lazy (init_constant "iff") let coq_True = lazy (init_constant "True") let coq_False = lazy (init_constant "False") @@ -949,6 +963,18 @@ struct let (env, n) = _add env 1 v in (env, CamlToCoq.idx n) + let get_rank env v = + + let rec _get_rank env n = + match env with + | [] -> raise (Invalid_argument "get_rank") + | e::l -> + if eq_constr e v + then n + else _get_rank l (n+1) in + _get_rank env 1 + + let empty = [] let elements env = env @@ -1173,33 +1199,32 @@ struct with e when CErrors.noncritical e -> (X(t),env,tg) in let is_prop term = - let ty = Typing.unsafe_type_of (Tacmach.pf_env gl) (Tacmach.project gl) term in - let sort = Typing.e_sort_of (Tacmach.pf_env gl) (ref (Tacmach.project gl)) ty in + let sort = Retyping.get_sort_of (Tacmach.pf_env gl) (Tacmach.project gl) term in Term.is_prop_sort sort in let rec xparse_formula env tg term = - match kind_of_term term with + match kind_of_term term with | App(l,rst) -> - (match rst with - | [|a;b|] when eq_constr 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 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 l (Lazy.force coq_not) -> - let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg) - | [|a;b|] when eq_constr 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 not (Termops.dependent (mkRel 1) b)-> + (match rst with + | [|a;b|] when eq_constr 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 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 l (Lazy.force coq_not) -> + let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg) + | [|a;b|] when eq_constr 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 mkI term f g,env,tg + mkformula_binary mkIff term f g,env,tg + | _ -> parse_atom env tg term) + | Prod(typ,a,b) when not (Termops.dependent (mkRel 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 term (Lazy.force coq_True) -> (TT,env,tg) | _ when eq_constr term (Lazy.force coq_False) -> (FF,env,tg) | _ when is_prop term -> X(term),env,tg @@ -1220,12 +1245,214 @@ struct | X(t) -> mkApp(Lazy.force coq_X,[|typ ; t|]) in xdump f - (** - * Given a conclusion and a list of affectations, rebuild a term prefixed by - * the appropriate letins. - * TODO: reverse the list of bindings! - *) + let prop_env_of_formula form = + let rec doit env = function + | TT | FF | A(_,_,_) -> env + | X t -> fst (Env.compute_rank_add env t) + | C(f1,f2) | D(f1,f2) | I(f1,_,f2) -> + doit (doit env f1) f2 + | N f -> doit env f in + + doit [] form + + let var_env_of_formula form = + + let rec vars_of_expr = function + | Mc.PEX n -> ISet.singleton (CoqToCaml.positive n) + | Mc.PEc z -> ISet.empty + | Mc.PEadd(e1,e2) | Mc.PEmul(e1,e2) | Mc.PEsub(e1,e2) -> + ISet.union (vars_of_expr e1) (vars_of_expr e2) + | Mc.PEopp e | Mc.PEpow(e,_)-> vars_of_expr e + in + + let vars_of_atom {Mc.flhs ; Mc.fop; Mc.frhs} = + ISet.union (vars_of_expr flhs) (vars_of_expr frhs) in + + let rec doit = function + | TT | FF | X _ -> ISet.empty + | A (a,t,c) -> vars_of_atom a + | C(f1,f2) | D(f1,f2) |I (f1,_,f2) -> ISet.union (doit f1) (doit f2) + | N f -> doit f in + + doit form + + + + + 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 + } + +let dump_zexpr = lazy + { + interp_typ = Lazy.force coq_Z; + dump_cst = dump_z; + dump_add = Lazy.force coq_Zplus; + dump_sub = Lazy.force coq_Zminus; + dump_opp = Lazy.force coq_Zopp; + dump_mul = Lazy.force coq_Zmult; + dump_pow = Lazy.force coq_Zpower; + dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))); + dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) zop_table + } + +let dump_qexpr = lazy + { + interp_typ = Lazy.force coq_Q; + dump_cst = dump_q; + dump_add = Lazy.force coq_Qplus; + dump_sub = Lazy.force coq_Qminus; + dump_opp = Lazy.force coq_Qopp; + dump_mul = Lazy.force coq_Qmult; + dump_pow = Lazy.force coq_Qpower; + dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))); + dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) qop_table + } + + let dump_positive_as_R p = + let mult = Lazy.force coq_Rmult in + 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 two = mk_add one one in + + let rec dump_positive p = + match p with + | Mc.XH -> one + | Mc.XO p -> mk_mult two (dump_positive p) + | Mc.XI p -> mk_add one (mk_mult two (dump_positive p)) in + + dump_positive p + +let dump_n_as_R n = + let z = CoqToCaml.n n in + if z = 0 + then Lazy.force coq_R0 + else dump_positive_as_R (CamlToCoq.positive z) + + +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 |]) + + +let dump_rexpr = lazy + { + interp_typ = Lazy.force coq_R; + dump_cst = dump_Rcst_as_R; + dump_add = Lazy.force coq_Rplus; + dump_sub = Lazy.force coq_Rminus; + dump_opp = Lazy.force coq_Ropp; + dump_mul = Lazy.force coq_Rmult; + dump_pow = Lazy.force coq_Rpower; + dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n))); + dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) rop_table + } + + + + +(** [make_goal_of_formula depxr vars props form] where + - vars is an environment for the arithmetic variables occuring in form + - props is an environment for the propositions occuring in form + @return a goal where all the variables and propositions of the formula are quantified + +*) + +let rec make_goal_of_formula dexpr form = + + let vars_idx = + List.mapi (fun i v -> (v, i+1)) (ISet.elements (var_env_of_formula form)) in + + (* List.iter (fun (v,i) -> Printf.fprintf stdout "var %i has index %i\n" v i) vars_idx ;*) + + let props = prop_env_of_formula 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 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.PEc z -> dexpr.dump_cst z + | Mc.PEadd(e1,e2) -> mkApp(dexpr.dump_add, + [| dump_expr e1;dump_expr e2|]) + | Mc.PEsub(e1,e2) -> 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|]) + in dump_expr e in + + let mkop op e1 e2 = + try + Term.mkApp(List.assoc op dexpr.dump_op, [| e1; e2|]) + with Not_found -> + Term.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 + + let rec xdump pi xi f = + 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) + | A(x,_,_) -> dump_cstr xi x + | X(t) -> let idx = Env.get_rank props t in + mkRel (pi+idx) in + + let nb_vars = List.length vars_n in + let nb_props = List.length props_n in + + (* Printf.fprintf stdout "NBProps : %i\n" nb_props ;*) + + let subst_prop p = + let idx = Env.get_rank props p in + mkVar (Names.id_of_string (Printf.sprintf "__p%i" idx)) in + + let form' = map_prop subst_prop form in + + (Term.prodn nb_props (List.map (fun (x,y) -> Names.Name x,y) props_n) + (Term.prodn nb_vars (List.map (fun (x,y) -> Names.Name x,y) vars_n) + (xdump (List.length vars_n) 0 form)), + List.rev props_n, List.rev var_name_pos,form') + + (** + * Given a conclusion and a list of affectations, rebuild a term prefixed by + * the appropriate letins. + * TODO: reverse the list of bindings! + *) + let set l concl = let rec xset acc = function | [] -> acc @@ -1290,39 +1517,35 @@ let rec apply_ids t ids = | [] -> t | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids -let coq_Node = lazy +let coq_Node = (Coqlib.gen_constant_in_modules "VarMap" [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node") -let coq_Leaf = lazy +let coq_Leaf = (Coqlib.gen_constant_in_modules "VarMap" [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf") -let coq_Empty = lazy +let coq_Empty = (Coqlib.gen_constant_in_modules "VarMap" [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty") -let btree_of_array typ a = - let size_of_a = Array.length a in - let semi_size_of_a = size_of_a lsr 1 in - let node = Lazy.force coq_Node - and leaf = Lazy.force coq_Leaf - and empty = Term.mkApp (Lazy.force coq_Empty, [| typ |]) in - let rec aux n = - if n > size_of_a - then empty - else if n > semi_size_of_a - then Term.mkApp (leaf, [| typ; a.(n-1) |]) - else Term.mkApp (node, [| typ; aux (2*n); a.(n-1); aux (2*n+1) |]) - in - aux 1 - -let btree_of_array typ a = - try - btree_of_array typ a - with x when CErrors.noncritical x -> - failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x)) - -let dump_varmap typ env = - btree_of_array typ (Array.of_list env) +let coq_VarMap = + (Coqlib.gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t") + + +let rec dump_varmap typ m = + match m with + | Mc.Empty -> Term.mkApp(coq_Empty,[| typ |]) + | Mc.Leaf v -> Term.mkApp(coq_Leaf,[| typ; v|]) + | Mc.Node(l,o,r) -> + Term.mkApp (coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |]) + + +let vm_of_list env = + match env with + | [] -> Mc.Empty + | (d,_)::_ -> + List.fold_left (fun vm (c,i) -> + Mc.vm_add d (CamlToCoq.positive i) c vm) Mc.Empty env let rec pp_varmap o vm = @@ -1473,10 +1696,10 @@ let topo_sort_constr l = mk_topo_order Termops.dependent 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 ("__z"^(string_of_int i)))) 0 env in + (* 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 ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in - let vm = dump_varmap (spec.typ) env 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 -> let gl = Tacmach.New.of_old (fun x -> x) gl in @@ -1486,15 +1709,10 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* (set [ ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); - ("__varmap", vm, Term.mkApp - (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|])); + ("__varmap", vm, Term.mkApp( coq_VarMap, [|spec.typ|])); ("__wit", cert, cert_typ) ] (Tacmach.pf_concl gl)) - ; - Tactics.generalize (topo_sort_constr env) ; - Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] end } @@ -1656,6 +1874,7 @@ let rec abstract_wrt_formula f1 f2 = exception CsdpNotFound + (** * This is the core of Micromega: apply the prover, analyze the result and * prune unused fomulas, and finally modify the proof state. @@ -1740,7 +1959,7 @@ let micromega_gen (negate:'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf) unsat deduce - spec prover = + spec dumpexpr prover tac = Proofview.Goal.nf_enter { enter = begin fun gl -> let gl = Tacmach.New.of_old (fun x -> x) gl in let concl = Tacmach.pf_concl gl in @@ -1749,16 +1968,39 @@ let micromega_gen let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in let env = Env.elements env in let spec = Lazy.force spec in + let dumpexpr = Lazy.force dumpexpr in match micromega_tauto negate normalise unsat deduce spec prover env hyps concl gl with | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") | Some (ids,ff',res') -> - (Tacticals.New.tclTHENLIST - [ - Tactics.generalize (List.map Term.mkVar ids) ; - micromega_order_change spec res' - (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff' - ]) + let (arith_goal,props,vars,ff_arith) = make_goal_of_formula dumpexpr ff' in + let intro (id,_) = Tactics.introduction id in + + let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in + let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in + let ipat_of_name id = Some (Loc.ghost, Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in + let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in + let env' = List.map (fun (id,i) -> Term.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 + + let kill_arith = + Tacticals.New.tclTHEN + (Tactics.keep []) + ((*Tactics.tclABSTRACT None*) + (Tacticals.New.tclTHEN tac_arith tac)) in + + Tacticals.New.tclTHEN + (Tactics.forward true (Some (Some kill_arith)) (ipat_of_name goal_name) arith_goal) + (Tacticals.New.tclTHENLIST + [(Tactics.generalize (List.map Term.mkVar ids)); + Tactics.unfold_constr coq_not_gl_ref; + (Tactics.apply (Term.applist (Term.mkVar goal_name,List.rev (prop_env_of_formula ff')))) + ]) + (*Tacticals.New.tclTRY(Tactics.apply_with_bindings_gen true false + [None,(Loc.ghost,((Term.mkVar goal_name) ,Misctypes.NoBindings))]*) with | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") @@ -1780,16 +2022,16 @@ let micromega_gen parse_arith let micromega_order_changer cert env ff = - let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__z"^(string_of_int i)))) 0 env in - 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 ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *) + 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 formula_typ = (Term.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) env in - Proofview.Goal.nf_enter { enter = begin fun gl -> + let formula_typ = (Term.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 -> let gl = Tacmach.New.of_old (fun x -> x) gl in Tacticals.New.tclTHENLIST [ @@ -1803,13 +2045,11 @@ let micromega_order_changer cert env ff = ("__wit", cert, cert_typ) ] (Tacmach.pf_concl gl))); - Tactics.generalize (topo_sort_constr env) ; - Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) + (* Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)*) ] end } - -let micromega_genr prover = +let micromega_genr prover tac = let parse_arith = parse_rarith in let negate = Mc.rnegate in let normalise = Mc.rnormalise in @@ -1826,6 +2066,7 @@ let micromega_genr prover = let gl = Tacmach.New.of_old (fun x -> x) gl in let concl = Tacmach.pf_concl gl in let hyps = Tacmach.pf_hyps_types gl in + try let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in let env = Env.elements env in @@ -1837,23 +2078,51 @@ let micromega_genr prover = match micromega_tauto negate normalise unsat deduce spec prover env hyps' concl' gl with | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") | Some (ids,ff',res') -> - let (ff,ids') = formula_hyps_concl + let (ff,ids) = formula_hyps_concl (List.filter (fun (n,_) -> List.mem n ids) hyps) concl in - (Tacticals.New.tclTHENLIST - [ - Tactics.generalize (List.map Term.mkVar ids) ; - micromega_order_changer res' env (abstract_wrt_formula ff' ff) - ]) - with - | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "TimeOut") - | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") - | CsdpNotFound -> - Tacticals.New.tclFAIL 0 (Pp.str - (" Skipping what remains of this tactic: the complexity of the goal requires " - ^ "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 } + let ff' = abstract_wrt_formula ff' ff in + + let (arith_goal,props,vars,ff_arith) = make_goal_of_formula (Lazy.force dump_rexpr) ff' in + let intro (id,_) = Tactics.introduction id in + + let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in + let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in + let ipat_of_name id = Some (Loc.ghost, Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in + let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in + let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in + + let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; + micromega_order_changer res' env' ff_arith ] in + + let kill_arith = + Tacticals.New.tclTHEN + (Tactics.keep []) + ((*Tactics.tclABSTRACT None*) + (Tacticals.New.tclTHEN tac_arith tac)) in + + + Tacticals.New.tclTHEN + (Tactics.forward true (Some (Some kill_arith)) (ipat_of_name goal_name) arith_goal) + + (Tacticals.New.tclTHENLIST + [(Tactics.generalize (List.map Term.mkVar ids)); + Tactics.unfold_constr coq_not_gl_ref; + (Tactics.apply (Term.applist (Term.mkVar goal_name,List.rev (prop_env_of_formula ff')))) + ] + ) + + with + | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") + | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") + | CsdpNotFound -> flush stdout ; + Tacticals.New.tclFAIL 0 (Pp.str + (" Skipping what remains of this tactic: the complexity of the goal requires " + ^ "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 } + + let micromega_genr prover = (micromega_genr prover) @@ -2129,11 +2398,11 @@ let tauto_lia ff = *) let lra_Q = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec + micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr [ linear_prover_Q ] let psatz_Q i = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec + micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] let lra_R = @@ -2144,15 +2413,15 @@ let psatz_R i = let psatz_Z i = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec + micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ] let sos_Z = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec + micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr [ non_linear_prover_Z "pure_sos" None ] let sos_Q = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec + micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr [ non_linear_prover_Q "pure_sos" None ] @@ -2160,18 +2429,18 @@ let sos_R = micromega_genr [ non_linear_prover_R "pure_sos" None ] -let xlia = micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec +let xlia = micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr [ linear_Z ] let xnlia = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec + micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr [ nlinear_Z ] let nra = micromega_genr [ nlinear_prover_R ] let nqa = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec + micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr [ nlinear_prover_R ] diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 974dcee87..027f690fc 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -20,56 +20,64 @@ open Constrarg DECLARE PLUGIN "micromega_plugin" +TACTIC EXTEND RED +| [ "myred" ] -> [ Tactics.red_in_concl ] +END + + + TACTIC EXTEND PsatzZ -| [ "psatz_Z" int_or_var(i) ] -> [ (Coq_micromega.psatz_Z i) ] -| [ "psatz_Z" ] -> [ (Coq_micromega.psatz_Z (-1)) ] +| [ "psatz_Z" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_Z i + (Tacinterp.tactic_of_value ist t)) + ] +| [ "psatz_Z" tactic(t)] -> [ (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) ] END TACTIC EXTEND Lia -[ "xlia" ] -> [ (Coq_micromega.xlia) ] +[ "xlia" tactic(t) ] -> [ (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) ] END TACTIC EXTEND Nia -[ "xnlia" ] -> [ (Coq_micromega.xnlia) ] +[ "xnlia" tactic(t) ] -> [ (Coq_micromega.xnlia (Tacinterp.tactic_of_value ist t)) ] END TACTIC EXTEND NRA -[ "xnra" ] -> [ (Coq_micromega.nra)] +[ "xnra" tactic(t) ] -> [ (Coq_micromega.nra (Tacinterp.tactic_of_value ist t))] END TACTIC EXTEND NQA -[ "xnqa" ] -> [ (Coq_micromega.nqa)] +[ "xnqa" tactic(t) ] -> [ (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))] END TACTIC EXTEND Sos_Z -| [ "sos_Z" ] -> [ (Coq_micromega.sos_Z) ] +| [ "sos_Z" tactic(t) ] -> [ (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) ] END TACTIC EXTEND Sos_Q -| [ "sos_Q" ] -> [ (Coq_micromega.sos_Q) ] +| [ "sos_Q" tactic(t) ] -> [ (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) ] END TACTIC EXTEND Sos_R -| [ "sos_R" ] -> [ (Coq_micromega.sos_R) ] +| [ "sos_R" tactic(t) ] -> [ (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) ] END TACTIC EXTEND LRA_Q -[ "lra_Q" ] -> [ (Coq_micromega.lra_Q) ] +[ "lra_Q" tactic(t) ] -> [ (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) ] END TACTIC EXTEND LRA_R -[ "lra_R" ] -> [ (Coq_micromega.lra_R) ] +[ "lra_R" tactic(t) ] -> [ (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) ] END TACTIC EXTEND PsatzR -| [ "psatz_R" int_or_var(i) ] -> [ (Coq_micromega.psatz_R i) ] -| [ "psatz_R" ] -> [ (Coq_micromega.psatz_R (-1)) ] +| [ "psatz_R" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) ] +| [ "psatz_R" tactic(t) ] -> [ (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) ] END TACTIC EXTEND PsatzQ -| [ "psatz_Q" int_or_var(i) ] -> [ (Coq_micromega.psatz_Q i) ] -| [ "psatz_Q" ] -> [ (Coq_micromega.psatz_Q (-1)) ] +| [ "psatz_Q" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) ] +| [ "psatz_Q" tactic(t) ] -> [ (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) ] END diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index 0537cdbe8..5cf1da8ea 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -1,6 +1,3 @@ -type __ = Obj.t -let __ = let rec f _ = Obj.repr f in Obj.repr f - (** val negb : bool -> bool **) let negb = function @@ -11,16 +8,6 @@ type nat = | O | S of nat -(** val fst : ('a1 * 'a2) -> 'a1 **) - -let fst = function -| x,y -> x - -(** val snd : ('a1 * 'a2) -> 'a2 **) - -let snd = function -| x,y -> y - (** val app : 'a1 list -> 'a1 list -> 'a1 list **) let rec app l m = @@ -40,42 +27,15 @@ let compOpp = function | Lt -> Gt | Gt -> Lt -type compareSpecT = -| CompEqT -| CompLtT -| CompGtT - -(** val compareSpec2Type : comparison -> compareSpecT **) - -let compareSpec2Type = function -| Eq -> CompEqT -| Lt -> CompLtT -| Gt -> CompGtT - -type 'a compSpecT = compareSpecT - -(** val compSpec2Type : 'a1 -> 'a1 -> comparison -> 'a1 compSpecT **) - -let compSpec2Type x y c = - compareSpec2Type c - -type 'a sig0 = - 'a - (* singleton inductive, whose constructor was exist *) - -(** val plus : nat -> nat -> nat **) - -let rec plus n0 m = - match n0 with - | O -> m - | S p -> S (plus p m) - -(** val nat_iter : nat -> ('a1 -> 'a1) -> 'a1 -> 'a1 **) +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 -let rec nat_iter n0 f x = - match n0 with - | O -> x - | S n' -> f (nat_iter n' f x) type positive = | XI of positive @@ -91,592 +51,25 @@ type z = | Zpos of positive | Zneg of positive -module type TotalOrder' = - sig - type t - end - -module MakeOrderTac = - functor (O:TotalOrder') -> - struct - - end - -module MaxLogicalProperties = - functor (O:TotalOrder') -> - functor (M:sig - val max : O.t -> O.t -> O.t - end) -> - struct - module T = MakeOrderTac(O) - end - -module Pos = - struct - type t = positive - - (** 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 - - (** val pred : positive -> positive **) - - let pred = function - | XI p -> XO p - | XO p -> pred_double p - | XH -> XH - - (** val pred_N : positive -> n **) - - let pred_N = function - | XI p -> Npos (XO p) - | XO p -> Npos (pred_double p) - | XH -> N0 - +module Pos = + struct type mask = | IsNul | IsPos of positive | IsNeg - - (** val mask_rect : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 **) - - let mask_rect f f0 f1 = function - | IsNul -> f - | IsPos x -> f0 x - | IsNeg -> f1 - - (** val mask_rec : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 **) - - let mask_rec f f0 f1 = function - | IsNul -> f - | IsPos x -> f0 x - | IsNeg -> f1 - - (** 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 pred_mask : mask -> mask **) - - let pred_mask = function - | IsPos q0 -> - (match q0 with - | XH -> IsNul - | _ -> IsPos (pred q0)) - | _ -> IsNeg - - (** 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 iter : positive -> ('a1 -> 'a1) -> 'a1 -> 'a1 **) - - let rec iter n0 f x = - match n0 with - | XI n' -> f (iter n' f (iter n' f x)) - | XO n' -> iter n' f (iter n' f x) - | XH -> f x - - (** val pow : positive -> positive -> positive **) - - let pow x y = - iter y (mul x) XH - - (** val div2 : positive -> positive **) - - let div2 = function - | XI p2 -> p2 - | XO p2 -> p2 - | XH -> XH - - (** val div2_up : positive -> positive **) - - let div2_up = function - | XI p2 -> succ p2 - | XO p2 -> p2 - | XH -> XH - - (** 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 size : positive -> positive **) - - let rec size = function - | XI p2 -> succ (size p2) - | XO p2 -> succ (size p2) - | XH -> XH - - (** val compare_cont : positive -> positive -> comparison -> comparison **) - - let rec compare_cont x y r = - match x with - | XI p -> - (match y with - | XI q0 -> compare_cont p q0 r - | XO q0 -> compare_cont p q0 Gt - | XH -> Gt) - | XO p -> - (match y with - | XI q0 -> compare_cont p q0 Lt - | XO q0 -> compare_cont p q0 r - | XH -> Gt) - | XH -> - (match y with - | XH -> r - | _ -> Lt) - - (** val compare : positive -> positive -> comparison **) - - let compare x y = - compare_cont x y Eq - - (** val min : positive -> positive -> positive **) - - let min p p' = - match compare p p' with - | Gt -> p' - | _ -> p - - (** val max : positive -> positive -> positive **) - - let max p p' = - match compare p p' with - | Gt -> p - | _ -> p' - - (** val eqb : positive -> positive -> bool **) - - let rec eqb p q0 = - match p with - | XI p2 -> - (match q0 with - | XI q1 -> eqb p2 q1 - | _ -> false) - | XO p2 -> - (match q0 with - | XO q1 -> eqb p2 q1 - | _ -> false) - | XH -> - (match q0 with - | XH -> true - | _ -> false) - - (** val leb : positive -> positive -> bool **) - - let leb x y = - match compare x y with - | Gt -> false - | _ -> true - - (** val ltb : positive -> positive -> bool **) - - let ltb x y = - match compare x y with - | Lt -> true - | _ -> false - - (** val sqrtrem_step : - (positive -> positive) -> (positive -> positive) -> (positive * mask) - -> positive * mask **) - - let sqrtrem_step f g = function - | s,y -> - (match y with - | IsPos r -> - let s' = XI (XO s) in - let r' = g (f r) in - if leb s' r' then (XI s),(sub_mask r' s') else (XO s),(IsPos r') - | _ -> (XO s),(sub_mask (g (f XH)) (XO (XO XH)))) - - (** val sqrtrem : positive -> positive * mask **) - - let rec sqrtrem = function - | XI p2 -> - (match p2 with - | XI p3 -> sqrtrem_step (fun x -> XI x) (fun x -> XI x) (sqrtrem p3) - | XO p3 -> sqrtrem_step (fun x -> XO x) (fun x -> XI x) (sqrtrem p3) - | XH -> XH,(IsPos (XO XH))) - | XO p2 -> - (match p2 with - | XI p3 -> sqrtrem_step (fun x -> XI x) (fun x -> XO x) (sqrtrem p3) - | XO p3 -> sqrtrem_step (fun x -> XO x) (fun x -> XO x) (sqrtrem p3) - | XH -> XH,(IsPos XH)) - | XH -> XH,IsNul - - (** val sqrt : positive -> positive **) - - let sqrt p = - fst (sqrtrem p) - - (** 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 p -> 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 (plus (size_nat a) (size_nat b)) a b - - (** val ggcdn : - nat -> positive -> positive -> positive * (positive * positive) **) - - let rec ggcdn n0 a b = - match n0 with - | O -> XH,(a,b) - | S n1 -> - (match a with - | XI a' -> - (match b with - | XI b' -> - (match compare a' b' with - | Eq -> a,(XH,XH) - | Lt -> - let g,p = ggcdn n1 (sub b' a') a in - let ba,aa = p in g,(aa,(add aa (XO ba))) - | Gt -> - let g,p = ggcdn n1 (sub a' b') b in - let ab,bb = p in g,((add bb (XO ab)),bb)) - | XO b0 -> - let g,p = ggcdn n1 a b0 in let aa,bb = p in g,(aa,(XO bb)) - | XH -> XH,(a,XH)) - | XO a0 -> - (match b with - | XI p -> - let g,p2 = ggcdn n1 a0 b in let aa,bb = p2 in g,((XO aa),bb) - | XO b0 -> let g,p = ggcdn n1 a0 b0 in (XO g),p - | XH -> XH,(a,XH)) - | XH -> XH,(XH,b)) - - (** val ggcd : positive -> positive -> positive * (positive * positive) **) - - let ggcd a b = - ggcdn (plus (size_nat a) (size_nat b)) a b - - (** val coq_Nsucc_double : n -> n **) - - let coq_Nsucc_double = function - | N0 -> Npos XH - | Npos p -> Npos (XI p) - - (** val coq_Ndouble : n -> n **) - - let coq_Ndouble = function - | N0 -> N0 - | Npos p -> Npos (XO p) - - (** val coq_lor : positive -> positive -> positive **) - - let rec coq_lor p q0 = - match p with - | XI p2 -> - (match q0 with - | XI q1 -> XI (coq_lor p2 q1) - | XO q1 -> XI (coq_lor p2 q1) - | XH -> p) - | XO p2 -> - (match q0 with - | XI q1 -> XI (coq_lor p2 q1) - | XO q1 -> XO (coq_lor p2 q1) - | XH -> XI p2) - | XH -> - (match q0 with - | XO q1 -> XI q1 - | _ -> q0) - - (** val coq_land : positive -> positive -> n **) - - let rec coq_land p q0 = - match p with - | XI p2 -> - (match q0 with - | XI q1 -> coq_Nsucc_double (coq_land p2 q1) - | XO q1 -> coq_Ndouble (coq_land p2 q1) - | XH -> Npos XH) - | XO p2 -> - (match q0 with - | XI q1 -> coq_Ndouble (coq_land p2 q1) - | XO q1 -> coq_Ndouble (coq_land p2 q1) - | XH -> N0) - | XH -> - (match q0 with - | XO q1 -> N0 - | _ -> Npos XH) - - (** val ldiff : positive -> positive -> n **) - - let rec ldiff p q0 = - match p with - | XI p2 -> - (match q0 with - | XI q1 -> coq_Ndouble (ldiff p2 q1) - | XO q1 -> coq_Nsucc_double (ldiff p2 q1) - | XH -> Npos (XO p2)) - | XO p2 -> - (match q0 with - | XI q1 -> coq_Ndouble (ldiff p2 q1) - | XO q1 -> coq_Ndouble (ldiff p2 q1) - | XH -> Npos p) - | XH -> - (match q0 with - | XO q1 -> Npos XH - | _ -> N0) - - (** val coq_lxor : positive -> positive -> n **) - - let rec coq_lxor p q0 = - match p with - | XI p2 -> - (match q0 with - | XI q1 -> coq_Ndouble (coq_lxor p2 q1) - | XO q1 -> coq_Nsucc_double (coq_lxor p2 q1) - | XH -> Npos (XO p2)) - | XO p2 -> - (match q0 with - | XI q1 -> coq_Nsucc_double (coq_lxor p2 q1) - | XO q1 -> coq_Ndouble (coq_lxor p2 q1) - | XH -> Npos (XI p2)) - | XH -> - (match q0 with - | XI q1 -> Npos (XO q1) - | XO q1 -> Npos (XI q1) - | XH -> N0) - - (** val shiftl_nat : positive -> nat -> positive **) - - let shiftl_nat p n0 = - nat_iter n0 (fun x -> XO x) p - - (** val shiftr_nat : positive -> nat -> positive **) - - let shiftr_nat p n0 = - nat_iter n0 div2 p - - (** val shiftl : positive -> n -> positive **) - - let shiftl p = function - | N0 -> p - | Npos n1 -> iter n1 (fun x -> XO x) p - - (** val shiftr : positive -> n -> positive **) - - let shiftr p = function - | N0 -> p - | Npos n1 -> iter n1 div2 p - - (** val testbit_nat : positive -> nat -> bool **) - - let rec testbit_nat p n0 = - match p with - | XI p2 -> - (match n0 with - | O -> true - | S n' -> testbit_nat p2 n') - | XO p2 -> - (match n0 with - | O -> false - | S n' -> testbit_nat p2 n') - | XH -> - (match n0 with - | O -> true - | S n1 -> false) - - (** val testbit : positive -> n -> bool **) - - let rec testbit p n0 = - match p with - | XI p2 -> - (match n0 with - | N0 -> true - | Npos n1 -> testbit p2 (pred_N n1)) - | XO p2 -> - (match n0 with - | N0 -> false - | Npos n1 -> testbit p2 (pred_N n1)) - | XH -> - (match n0 with - | N0 -> true - | Npos p2 -> false) - - (** val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1 **) - - let rec iter_op op p a = - match p with - | XI p2 -> op a (iter_op op p2 (op a a)) - | XO p2 -> iter_op op p2 (op a a) - | XH -> a - - (** val to_nat : positive -> nat **) - - let to_nat x = - iter_op plus x (S O) - - (** val of_nat : nat -> positive **) - - let rec of_nat = function - | O -> XH - | S x -> - (match x with - | O -> XH - | S n1 -> succ (of_nat x)) - - (** val of_succ_nat : nat -> positive **) - - let rec of_succ_nat = function - | O -> XH - | S x -> succ (of_succ_nat x) end -module Coq_Pos = - struct - module Coq__1 = struct - type t = positive - end - type t = Coq__1.t - +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 -> @@ -694,9 +87,9 @@ module Coq_Pos = | 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 -> @@ -714,78 +107,41 @@ module Coq_Pos = | 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 - - (** val pred : positive -> positive **) - - let pred = function - | XI p -> XO p - | XO p -> pred_double p - | XH -> XH - - (** val pred_N : positive -> n **) - - let pred_N = function - | XI p -> Npos (XO p) - | XO p -> Npos (pred_double p) - | XH -> N0 - + type mask = Pos.mask = | IsNul | IsPos of positive | IsNeg - - (** val mask_rect : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 **) - - let mask_rect f f0 f1 = function - | IsNul -> f - | IsPos x -> f0 x - | IsNeg -> f1 - - (** val mask_rec : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 **) - - let mask_rec f f0 f1 = function - | IsNul -> f - | IsPos x -> f0 x - | IsNeg -> f1 - + (** 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 pred_mask : mask -> mask **) - - let pred_mask = function - | IsPos q0 -> - (match q0 with - | XH -> IsNul - | _ -> IsPos (pred q0)) - | _ -> IsNeg - + (** val sub_mask : positive -> positive -> mask **) - + let rec sub_mask x y = match x with | XI p -> @@ -802,9 +158,9 @@ module Coq_Pos = (match y with | XH -> IsNul | _ -> IsNeg) - + (** val sub_mask_carry : positive -> positive -> mask **) - + and sub_mask_carry x y = match x with | XI p -> @@ -818,167 +174,56 @@ module Coq_Pos = | 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 iter : positive -> ('a1 -> 'a1) -> 'a1 -> 'a1 **) - - let rec iter n0 f x = - match n0 with - | XI n' -> f (iter n' f (iter n' f x)) - | XO n' -> iter n' f (iter n' f x) - | XH -> f x - - (** val pow : positive -> positive -> positive **) - - let pow x y = - iter y (mul x) XH - - (** val div2 : positive -> positive **) - - let div2 = function - | XI p2 -> p2 - | XO p2 -> p2 - | XH -> XH - - (** val div2_up : positive -> positive **) - - let div2_up = function - | XI p2 -> succ p2 - | XO p2 -> p2 - | XH -> XH - + (** 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 size : positive -> positive **) - - let rec size = function - | XI p2 -> succ (size p2) - | XO p2 -> succ (size p2) - | XH -> XH - - (** val compare_cont : positive -> positive -> comparison -> comparison **) - - let rec compare_cont x y r = + + (** 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 p q0 r - | XO q0 -> compare_cont p q0 Gt + | 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 p q0 Lt - | XO q0 -> compare_cont p q0 r + | 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 x y = - compare_cont x y Eq - - (** val min : positive -> positive -> positive **) - - let min p p' = - match compare p p' with - | Gt -> p' - | _ -> p - - (** val max : positive -> positive -> positive **) - - let max p p' = - match compare p p' with - | Gt -> p - | _ -> p' - - (** val eqb : positive -> positive -> bool **) - - let rec eqb p q0 = - match p with - | XI p2 -> - (match q0 with - | XI q1 -> eqb p2 q1 - | _ -> false) - | XO p2 -> - (match q0 with - | XO q1 -> eqb p2 q1 - | _ -> false) - | XH -> - (match q0 with - | XH -> true - | _ -> false) - - (** val leb : positive -> positive -> bool **) - - let leb x y = - match compare x y with - | Gt -> false - | _ -> true - - (** val ltb : positive -> positive -> bool **) - - let ltb x y = - match compare x y with - | Lt -> true - | _ -> false - - (** val sqrtrem_step : - (positive -> positive) -> (positive -> positive) -> (positive * mask) - -> positive * mask **) - - let sqrtrem_step f g = function - | s,y -> - (match y with - | IsPos r -> - let s' = XI (XO s) in - let r' = g (f r) in - if leb s' r' then (XI s),(sub_mask r' s') else (XO s),(IsPos r') - | _ -> (XO s),(sub_mask (g (f XH)) (XO (XO XH)))) - - (** val sqrtrem : positive -> positive * mask **) - - let rec sqrtrem = function - | XI p2 -> - (match p2 with - | XI p3 -> sqrtrem_step (fun x -> XI x) (fun x -> XI x) (sqrtrem p3) - | XO p3 -> sqrtrem_step (fun x -> XO x) (fun x -> XI x) (sqrtrem p3) - | XH -> XH,(IsPos (XO XH))) - | XO p2 -> - (match p2 with - | XI p3 -> sqrtrem_step (fun x -> XI x) (fun x -> XO x) (sqrtrem p3) - | XO p3 -> sqrtrem_step (fun x -> XO x) (fun x -> XO x) (sqrtrem p3) - | XH -> XH,(IsPos XH)) - | XH -> XH,IsNul - - (** val sqrt : positive -> positive **) - - let sqrt p = - fst (sqrtrem p) - + + let compare = + compare_cont Eq + (** val gcdn : nat -> positive -> positive -> positive **) - + let rec gcdn n0 a b = match n0 with | O -> XH @@ -995,1001 +240,30 @@ module Coq_Pos = | XH -> XH) | XO a0 -> (match b with - | XI p -> gcdn n1 a0 b + | 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 (plus (size_nat a) (size_nat b)) a b - - (** val ggcdn : - nat -> positive -> positive -> positive * (positive * positive) **) - - let rec ggcdn n0 a b = - match n0 with - | O -> XH,(a,b) - | S n1 -> - (match a with - | XI a' -> - (match b with - | XI b' -> - (match compare a' b' with - | Eq -> a,(XH,XH) - | Lt -> - let g,p = ggcdn n1 (sub b' a') a in - let ba,aa = p in g,(aa,(add aa (XO ba))) - | Gt -> - let g,p = ggcdn n1 (sub a' b') b in - let ab,bb = p in g,((add bb (XO ab)),bb)) - | XO b0 -> - let g,p = ggcdn n1 a b0 in let aa,bb = p in g,(aa,(XO bb)) - | XH -> XH,(a,XH)) - | XO a0 -> - (match b with - | XI p -> - let g,p2 = ggcdn n1 a0 b in let aa,bb = p2 in g,((XO aa),bb) - | XO b0 -> let g,p = ggcdn n1 a0 b0 in (XO g),p - | XH -> XH,(a,XH)) - | XH -> XH,(XH,b)) - - (** val ggcd : positive -> positive -> positive * (positive * positive) **) - - let ggcd a b = - ggcdn (plus (size_nat a) (size_nat b)) a b - - (** val coq_Nsucc_double : n -> n **) - - let coq_Nsucc_double = function - | N0 -> Npos XH - | Npos p -> Npos (XI p) - - (** val coq_Ndouble : n -> n **) - - let coq_Ndouble = function - | N0 -> N0 - | Npos p -> Npos (XO p) - - (** val coq_lor : positive -> positive -> positive **) - - let rec coq_lor p q0 = - match p with - | XI p2 -> - (match q0 with - | XI q1 -> XI (coq_lor p2 q1) - | XO q1 -> XI (coq_lor p2 q1) - | XH -> p) - | XO p2 -> - (match q0 with - | XI q1 -> XI (coq_lor p2 q1) - | XO q1 -> XO (coq_lor p2 q1) - | XH -> XI p2) - | XH -> - (match q0 with - | XO q1 -> XI q1 - | _ -> q0) - - (** val coq_land : positive -> positive -> n **) - - let rec coq_land p q0 = - match p with - | XI p2 -> - (match q0 with - | XI q1 -> coq_Nsucc_double (coq_land p2 q1) - | XO q1 -> coq_Ndouble (coq_land p2 q1) - | XH -> Npos XH) - | XO p2 -> - (match q0 with - | XI q1 -> coq_Ndouble (coq_land p2 q1) - | XO q1 -> coq_Ndouble (coq_land p2 q1) - | XH -> N0) - | XH -> - (match q0 with - | XO q1 -> N0 - | _ -> Npos XH) - - (** val ldiff : positive -> positive -> n **) - - let rec ldiff p q0 = - match p with - | XI p2 -> - (match q0 with - | XI q1 -> coq_Ndouble (ldiff p2 q1) - | XO q1 -> coq_Nsucc_double (ldiff p2 q1) - | XH -> Npos (XO p2)) - | XO p2 -> - (match q0 with - | XI q1 -> coq_Ndouble (ldiff p2 q1) - | XO q1 -> coq_Ndouble (ldiff p2 q1) - | XH -> Npos p) - | XH -> - (match q0 with - | XO q1 -> Npos XH - | _ -> N0) - - (** val coq_lxor : positive -> positive -> n **) - - let rec coq_lxor p q0 = - match p with - | XI p2 -> - (match q0 with - | XI q1 -> coq_Ndouble (coq_lxor p2 q1) - | XO q1 -> coq_Nsucc_double (coq_lxor p2 q1) - | XH -> Npos (XO p2)) - | XO p2 -> - (match q0 with - | XI q1 -> coq_Nsucc_double (coq_lxor p2 q1) - | XO q1 -> coq_Ndouble (coq_lxor p2 q1) - | XH -> Npos (XI p2)) - | XH -> - (match q0 with - | XI q1 -> Npos (XO q1) - | XO q1 -> Npos (XI q1) - | XH -> N0) - - (** val shiftl_nat : positive -> nat -> positive **) - - let shiftl_nat p n0 = - nat_iter n0 (fun x -> XO x) p - - (** val shiftr_nat : positive -> nat -> positive **) - - let shiftr_nat p n0 = - nat_iter n0 div2 p - - (** val shiftl : positive -> n -> positive **) - - let shiftl p = function - | N0 -> p - | Npos n1 -> iter n1 (fun x -> XO x) p - - (** val shiftr : positive -> n -> positive **) - - let shiftr p = function - | N0 -> p - | Npos n1 -> iter n1 div2 p - - (** val testbit_nat : positive -> nat -> bool **) - - let rec testbit_nat p n0 = - match p with - | XI p2 -> - (match n0 with - | O -> true - | S n' -> testbit_nat p2 n') - | XO p2 -> - (match n0 with - | O -> false - | S n' -> testbit_nat p2 n') - | XH -> - (match n0 with - | O -> true - | S n1 -> false) - - (** val testbit : positive -> n -> bool **) - - let rec testbit p n0 = - match p with - | XI p2 -> - (match n0 with - | N0 -> true - | Npos n1 -> testbit p2 (pred_N n1)) - | XO p2 -> - (match n0 with - | N0 -> false - | Npos n1 -> testbit p2 (pred_N n1)) - | XH -> - (match n0 with - | N0 -> true - | Npos p2 -> false) - - (** val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1 **) - - let rec iter_op op p a = - match p with - | XI p2 -> op a (iter_op op p2 (op a a)) - | XO p2 -> iter_op op p2 (op a a) - | XH -> a - - (** val to_nat : positive -> nat **) - - let to_nat x = - iter_op plus x (S O) - - (** val of_nat : nat -> positive **) - - let rec of_nat = function - | O -> XH - | S x -> - (match x with - | O -> XH - | S n1 -> succ (of_nat x)) - + 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) - - (** val eq_dec : positive -> positive -> bool **) - - let rec eq_dec p y0 = - match p with - | XI p2 -> - (match y0 with - | XI p3 -> eq_dec p2 p3 - | _ -> false) - | XO p2 -> - (match y0 with - | XO p3 -> eq_dec p2 p3 - | _ -> false) - | XH -> - (match y0 with - | XH -> true - | _ -> false) - - (** val peano_rect : 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> 'a1 **) - - let rec peano_rect a f p = - let f2 = peano_rect (f XH a) (fun p2 x -> f (succ (XO p2)) (f (XO p2) x)) - in - (match p with - | XI q0 -> f (XO q0) (f2 q0) - | XO q0 -> f2 q0 - | XH -> a) - - (** val peano_rec : 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> 'a1 **) - - let peano_rec = - peano_rect - - type coq_PeanoView = - | PeanoOne - | PeanoSucc of positive * coq_PeanoView - - (** val coq_PeanoView_rect : - 'a1 -> (positive -> coq_PeanoView -> 'a1 -> 'a1) -> positive -> - coq_PeanoView -> 'a1 **) - - let rec coq_PeanoView_rect f f0 p = function - | PeanoOne -> f - | PeanoSucc (p3, p4) -> f0 p3 p4 (coq_PeanoView_rect f f0 p3 p4) - - (** val coq_PeanoView_rec : - 'a1 -> (positive -> coq_PeanoView -> 'a1 -> 'a1) -> positive -> - coq_PeanoView -> 'a1 **) - - let rec coq_PeanoView_rec f f0 p = function - | PeanoOne -> f - | PeanoSucc (p3, p4) -> f0 p3 p4 (coq_PeanoView_rec f f0 p3 p4) - - (** val peanoView_xO : positive -> coq_PeanoView -> coq_PeanoView **) - - let rec peanoView_xO p = function - | PeanoOne -> PeanoSucc (XH, PeanoOne) - | PeanoSucc (p2, q1) -> - PeanoSucc ((succ (XO p2)), (PeanoSucc ((XO p2), (peanoView_xO p2 q1)))) - - (** val peanoView_xI : positive -> coq_PeanoView -> coq_PeanoView **) - - let rec peanoView_xI p = function - | PeanoOne -> PeanoSucc ((succ XH), (PeanoSucc (XH, PeanoOne))) - | PeanoSucc (p2, q1) -> - PeanoSucc ((succ (XI p2)), (PeanoSucc ((XI p2), (peanoView_xI p2 q1)))) - - (** val peanoView : positive -> coq_PeanoView **) - - let rec peanoView = function - | XI p2 -> peanoView_xI p2 (peanoView p2) - | XO p2 -> peanoView_xO p2 (peanoView p2) - | XH -> PeanoOne - - (** val coq_PeanoView_iter : - 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> coq_PeanoView -> 'a1 **) - - let rec coq_PeanoView_iter a f p = function - | PeanoOne -> a - | PeanoSucc (p2, q1) -> f p2 (coq_PeanoView_iter a f p2 q1) - - (** val switch_Eq : comparison -> comparison -> comparison **) - - let switch_Eq c = function - | Eq -> c - | x -> x - - (** val mask2cmp : mask -> comparison **) - - let mask2cmp = function - | IsNul -> Eq - | IsPos p2 -> Gt - | IsNeg -> Lt - - module T = - struct - - end - - module ORev = - struct - type t = Coq__1.t - end - - module MRev = - struct - (** val max : t -> t -> t **) - - let max x y = - min y x - end - - module MPRev = MaxLogicalProperties(ORev)(MRev) - - module P = - struct - (** val max_case_strong : - t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) - -> 'a1 **) - - let max_case_strong n0 m compat hl hr = - let c = compSpec2Type n0 m (compare n0 m) in - (match c with - | CompGtT -> compat n0 (max n0 m) __ (hl __) - | _ -> compat m (max n0 m) __ (hr __)) - - (** val max_case : - t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **) - - let max_case n0 m x x0 x1 = - max_case_strong n0 m x (fun _ -> x0) (fun _ -> x1) - - (** val max_dec : t -> t -> bool **) - - let max_dec n0 m = - max_case n0 m (fun x y _ h0 -> h0) true false - - (** val min_case_strong : - t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) - -> 'a1 **) - - let min_case_strong n0 m compat hl hr = - let c = compSpec2Type n0 m (compare n0 m) in - (match c with - | CompGtT -> compat m (min n0 m) __ (hr __) - | _ -> compat n0 (min n0 m) __ (hl __)) - - (** val min_case : - t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **) - - let min_case n0 m x x0 x1 = - min_case_strong n0 m x (fun _ -> x0) (fun _ -> x1) - - (** val min_dec : t -> t -> bool **) - - let min_dec n0 m = - min_case n0 m (fun x y _ h0 -> h0) true false - end - - (** val max_case_strong : t -> t -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) - - let max_case_strong n0 m x x0 = - P.max_case_strong n0 m (fun x1 y _ x2 -> x2) x x0 - - (** val max_case : t -> t -> 'a1 -> 'a1 -> 'a1 **) - - let max_case n0 m x x0 = - max_case_strong n0 m (fun _ -> x) (fun _ -> x0) - - (** val max_dec : t -> t -> bool **) - - let max_dec = - P.max_dec - - (** val min_case_strong : t -> t -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) - - let min_case_strong n0 m x x0 = - P.min_case_strong n0 m (fun x1 y _ x2 -> x2) x x0 - - (** val min_case : t -> t -> 'a1 -> 'a1 -> 'a1 **) - - let min_case n0 m x x0 = - min_case_strong n0 m (fun _ -> x) (fun _ -> x0) - - (** val min_dec : t -> t -> bool **) - - let min_dec = - P.min_dec end -module N = - struct - type t = n - - (** val zero : n **) - - let zero = - N0 - - (** val one : n **) - - let one = - Npos XH - - (** val two : n **) - - let two = - Npos (XO XH) - - (** val succ_double : n -> n **) - - let succ_double = function - | N0 -> Npos XH - | Npos p -> Npos (XI p) - - (** val double : n -> n **) - - let double = function - | N0 -> N0 - | Npos p -> Npos (XO p) - - (** val succ : n -> n **) - - let succ = function - | N0 -> Npos XH - | Npos p -> Npos (Coq_Pos.succ p) - - (** val pred : n -> n **) - - let pred = function - | N0 -> N0 - | Npos p -> Coq_Pos.pred_N p - - (** val succ_pos : n -> positive **) - - let succ_pos = function - | N0 -> XH - | Npos p -> Coq_Pos.succ p - - (** val add : n -> n -> n **) - - let add n0 m = - match n0 with - | N0 -> m - | Npos p -> - (match m with - | N0 -> n0 - | Npos q0 -> Npos (Coq_Pos.add p q0)) - - (** val sub : n -> n -> n **) - - let sub n0 m = - match n0 with - | N0 -> N0 - | Npos n' -> - (match m with - | N0 -> n0 - | Npos m' -> - (match Coq_Pos.sub_mask n' m' with - | Coq_Pos.IsPos p -> Npos p - | _ -> N0)) - - (** val mul : n -> n -> n **) - - let mul n0 m = - match n0 with - | N0 -> N0 - | Npos p -> - (match m with - | N0 -> N0 - | Npos q0 -> Npos (Coq_Pos.mul p q0)) - - (** val compare : n -> n -> comparison **) - - let compare n0 m = - match n0 with - | N0 -> - (match m with - | N0 -> Eq - | Npos m' -> Lt) - | Npos n' -> - (match m with - | N0 -> Gt - | Npos m' -> Coq_Pos.compare n' m') - - (** val eqb : n -> n -> bool **) - - let eqb n0 m = - match n0 with - | N0 -> - (match m with - | N0 -> true - | Npos p -> false) - | Npos p -> - (match m with - | N0 -> false - | Npos q0 -> Coq_Pos.eqb p q0) - - (** val leb : n -> n -> bool **) - - let leb x y = - match compare x y with - | Gt -> false - | _ -> true - - (** val ltb : n -> n -> bool **) - - let ltb x y = - match compare x y with - | Lt -> true - | _ -> false - - (** val min : n -> n -> n **) - - let min n0 n' = - match compare n0 n' with - | Gt -> n' - | _ -> n0 - - (** val max : n -> n -> n **) - - let max n0 n' = - match compare n0 n' with - | Gt -> n0 - | _ -> n' - - (** val div2 : n -> n **) - - let div2 = function - | N0 -> N0 - | Npos p2 -> - (match p2 with - | XI p -> Npos p - | XO p -> Npos p - | XH -> N0) - - (** val even : n -> bool **) - - let even = function - | N0 -> true - | Npos p -> - (match p with - | XO p2 -> true - | _ -> false) - - (** val odd : n -> bool **) - - let odd n0 = - negb (even n0) - - (** val pow : n -> n -> n **) - - let pow n0 = function - | N0 -> Npos XH - | Npos p2 -> - (match n0 with - | N0 -> N0 - | Npos q0 -> Npos (Coq_Pos.pow q0 p2)) - - (** val log2 : n -> n **) - - let log2 = function - | N0 -> N0 - | Npos p2 -> - (match p2 with - | XI p -> Npos (Coq_Pos.size p) - | XO p -> Npos (Coq_Pos.size p) - | XH -> N0) - - (** val size : n -> n **) - - let size = function - | N0 -> N0 - | Npos p -> Npos (Coq_Pos.size p) - - (** val size_nat : n -> nat **) - - let size_nat = function - | N0 -> O - | Npos p -> Coq_Pos.size_nat p - - (** val pos_div_eucl : positive -> n -> n * n **) - - let rec pos_div_eucl a b = - match a with - | XI a' -> - let q0,r = pos_div_eucl a' b in - let r' = succ_double r in - if leb b r' then (succ_double q0),(sub r' b) else (double q0),r' - | XO a' -> - let q0,r = pos_div_eucl a' b in - let r' = double r in - if leb b r' then (succ_double q0),(sub r' b) else (double q0),r' - | XH -> - (match b with - | N0 -> N0,(Npos XH) - | Npos p -> - (match p with - | XH -> (Npos XH),N0 - | _ -> N0,(Npos XH))) - - (** val div_eucl : n -> n -> n * n **) - - let div_eucl a b = - match a with - | N0 -> N0,N0 - | Npos na -> - (match b with - | N0 -> N0,a - | Npos p -> pos_div_eucl na b) - - (** val div : n -> n -> n **) - - let div a b = - fst (div_eucl a b) - - (** val modulo : n -> n -> n **) - - let modulo a b = - snd (div_eucl a b) - - (** val gcd : n -> n -> n **) - - let gcd a b = - match a with - | N0 -> b - | Npos p -> - (match b with - | N0 -> a - | Npos q0 -> Npos (Coq_Pos.gcd p q0)) - - (** val ggcd : n -> n -> n * (n * n) **) - - let ggcd a b = - match a with - | N0 -> b,(N0,(Npos XH)) - | Npos p -> - (match b with - | N0 -> a,((Npos XH),N0) - | Npos q0 -> - let g,p2 = Coq_Pos.ggcd p q0 in - let aa,bb = p2 in (Npos g),((Npos aa),(Npos bb))) - - (** val sqrtrem : n -> n * n **) - - let sqrtrem = function - | N0 -> N0,N0 - | Npos p -> - let s,m = Coq_Pos.sqrtrem p in - (match m with - | Coq_Pos.IsPos r -> (Npos s),(Npos r) - | _ -> (Npos s),N0) - - (** val sqrt : n -> n **) - - let sqrt = function - | N0 -> N0 - | Npos p -> Npos (Coq_Pos.sqrt p) - - (** val coq_lor : n -> n -> n **) - - let coq_lor n0 m = - match n0 with - | N0 -> m - | Npos p -> - (match m with - | N0 -> n0 - | Npos q0 -> Npos (Coq_Pos.coq_lor p q0)) - - (** val coq_land : n -> n -> n **) - - let coq_land n0 m = - match n0 with - | N0 -> N0 - | Npos p -> - (match m with - | N0 -> N0 - | Npos q0 -> Coq_Pos.coq_land p q0) - - (** val ldiff : n -> n -> n **) - - let ldiff n0 m = - match n0 with - | N0 -> N0 - | Npos p -> - (match m with - | N0 -> n0 - | Npos q0 -> Coq_Pos.ldiff p q0) - - (** val coq_lxor : n -> n -> n **) - - let coq_lxor n0 m = - match n0 with - | N0 -> m - | Npos p -> - (match m with - | N0 -> n0 - | Npos q0 -> Coq_Pos.coq_lxor p q0) - - (** val shiftl_nat : n -> nat -> n **) - - let shiftl_nat a n0 = - nat_iter n0 double a - - (** val shiftr_nat : n -> nat -> n **) - - let shiftr_nat a n0 = - nat_iter n0 div2 a - - (** val shiftl : n -> n -> n **) - - let shiftl a n0 = - match a with - | N0 -> N0 - | Npos a0 -> Npos (Coq_Pos.shiftl a0 n0) - - (** val shiftr : n -> n -> n **) - - let shiftr a = function - | N0 -> a - | Npos p -> Coq_Pos.iter p div2 a - - (** val testbit_nat : n -> nat -> bool **) - - let testbit_nat = function - | N0 -> (fun x -> false) - | Npos p -> Coq_Pos.testbit_nat p - - (** val testbit : n -> n -> bool **) - - let testbit a n0 = - match a with - | N0 -> false - | Npos p -> Coq_Pos.testbit p n0 - - (** val to_nat : n -> nat **) - - let to_nat = function - | N0 -> O - | Npos p -> Coq_Pos.to_nat p - +module N = + struct (** val of_nat : nat -> n **) - + let of_nat = function | O -> N0 | S n' -> Npos (Coq_Pos.of_succ_nat n') - - (** val iter : n -> ('a1 -> 'a1) -> 'a1 -> 'a1 **) - - let iter n0 f x = - match n0 with - | N0 -> x - | Npos p -> Coq_Pos.iter p f x - - (** val eq_dec : n -> n -> bool **) - - let eq_dec n0 m = - match n0 with - | N0 -> - (match m with - | N0 -> true - | Npos p -> false) - | Npos x -> - (match m with - | N0 -> false - | Npos p2 -> Coq_Pos.eq_dec x p2) - - (** val discr : n -> positive option **) - - let discr = function - | N0 -> None - | Npos p -> Some p - - (** val binary_rect : - 'a1 -> (n -> 'a1 -> 'a1) -> (n -> 'a1 -> 'a1) -> n -> 'a1 **) - - let binary_rect f0 f2 fS2 n0 = - let f2' = fun p -> f2 (Npos p) in - let fS2' = fun p -> fS2 (Npos p) in - (match n0 with - | N0 -> f0 - | Npos p -> - let rec f = function - | XI p3 -> fS2' p3 (f p3) - | XO p3 -> f2' p3 (f p3) - | XH -> fS2 N0 f0 - in f p) - - (** val binary_rec : - 'a1 -> (n -> 'a1 -> 'a1) -> (n -> 'a1 -> 'a1) -> n -> 'a1 **) - - let binary_rec = - binary_rect - - (** val peano_rect : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 **) - - let peano_rect f0 f n0 = - let f' = fun p -> f (Npos p) in - (match n0 with - | N0 -> f0 - | Npos p -> Coq_Pos.peano_rect (f N0 f0) f' p) - - (** val peano_rec : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 **) - - let peano_rec = - peano_rect - - module BootStrap = - struct - - end - - (** val recursion : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 **) - - let recursion x = - peano_rect x - - module OrderElts = - struct - type t = n - end - - module OrderTac = MakeOrderTac(OrderElts) - - module NZPowP = - struct - - end - - module NZSqrtP = - struct - - end - - (** val sqrt_up : n -> n **) - - let sqrt_up a = - match compare N0 a with - | Lt -> succ (sqrt (pred a)) - | _ -> N0 - - (** val log2_up : n -> n **) - - let log2_up a = - match compare (Npos XH) a with - | Lt -> succ (log2 (pred a)) - | _ -> N0 - - module NZDivP = - struct - - end - - (** val lcm : n -> n -> n **) - - let lcm a b = - mul a (div b (gcd a b)) - - (** val b2n : bool -> n **) - - let b2n = function - | true -> Npos XH - | false -> N0 - - (** val setbit : n -> n -> n **) - - let setbit a n0 = - coq_lor a (shiftl (Npos XH) n0) - - (** val clearbit : n -> n -> n **) - - let clearbit a n0 = - ldiff a (shiftl (Npos XH) n0) - - (** val ones : n -> n **) - - let ones n0 = - pred (shiftl (Npos XH) n0) - - (** val lnot : n -> n -> n **) - - let lnot a n0 = - coq_lxor a (ones n0) - - module T = - struct - - end - - module ORev = - struct - type t = n - end - - module MRev = - struct - (** val max : n -> n -> n **) - - let max x y = - min y x - end - - module MPRev = MaxLogicalProperties(ORev)(MRev) - - module P = - struct - (** val max_case_strong : - n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) - -> 'a1 **) - - let max_case_strong n0 m compat hl hr = - let c = compSpec2Type n0 m (compare n0 m) in - (match c with - | CompGtT -> compat n0 (max n0 m) __ (hl __) - | _ -> compat m (max n0 m) __ (hr __)) - - (** val max_case : - n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **) - - let max_case n0 m x x0 x1 = - max_case_strong n0 m x (fun _ -> x0) (fun _ -> x1) - - (** val max_dec : n -> n -> bool **) - - let max_dec n0 m = - max_case n0 m (fun x y _ h0 -> h0) true false - - (** val min_case_strong : - n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) - -> 'a1 **) - - let min_case_strong n0 m compat hl hr = - let c = compSpec2Type n0 m (compare n0 m) in - (match c with - | CompGtT -> compat m (min n0 m) __ (hr __) - | _ -> compat n0 (min n0 m) __ (hl __)) - - (** val min_case : - n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **) - - let min_case n0 m x x0 x1 = - min_case_strong n0 m x (fun _ -> x0) (fun _ -> x1) - - (** val min_dec : n -> n -> bool **) - - let min_dec n0 m = - min_case n0 m (fun x y _ h0 -> h0) true false - end - - (** val max_case_strong : n -> n -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) - - let max_case_strong n0 m x x0 = - P.max_case_strong n0 m (fun x1 y _ x2 -> x2) x x0 - - (** val max_case : n -> n -> 'a1 -> 'a1 -> 'a1 **) - - let max_case n0 m x x0 = - max_case_strong n0 m (fun _ -> x) (fun _ -> x0) - - (** val max_dec : n -> n -> bool **) - - let max_dec = - P.max_dec - - (** val min_case_strong : n -> n -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) - - let min_case_strong n0 m x x0 = - P.min_case_strong n0 m (fun x1 y _ x2 -> x2) x x0 - - (** val min_case : n -> n -> 'a1 -> 'a1 -> 'a1 **) - - let min_case n0 m x x0 = - min_case_strong n0 m (fun _ -> x) (fun _ -> x0) - - (** val min_dec : n -> n -> bool **) - - let min_dec = - P.min_dec end (** val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 **) @@ -2006,66 +280,49 @@ let rec nth n0 l default = | O -> (match l with | [] -> default - | x::l' -> x) + | x::_ -> x) | S m -> (match l with | [] -> default - | x::t1 -> nth m t1 default) + | _::t0 -> nth m t0 default) (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **) let rec map f = function | [] -> [] -| a::t1 -> (f a)::(map f t1) +| 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::t1 -> f b (fold_right f a0 t1) - -module Z = - struct - type t = z - - (** val zero : z **) - - let zero = - Z0 - - (** val one : z **) - - let one = - Zpos XH - - (** val two : z **) - - let two = - Zpos (XO XH) - +| 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 -> @@ -2083,9 +340,9 @@ module Z = | 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 @@ -2099,31 +356,21 @@ module Z = | 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 succ : z -> z **) - - let succ x = - add x (Zpos XH) - - (** val pred : z -> z **) - - let pred x = - add x (Zneg XH) - + (** 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 @@ -2137,28 +384,16 @@ module Z = | Z0 -> Z0 | Zpos y' -> Zneg (Coq_Pos.mul x' y') | Zneg y' -> Zpos (Coq_Pos.mul x' y')) - - (** val pow_pos : z -> positive -> z **) - - let pow_pos z0 n0 = - Coq_Pos.iter n0 (mul z0) (Zpos XH) - - (** val pow : z -> z -> z **) - - let pow x = function - | Z0 -> Zpos XH - | Zpos p -> pow_pos x p - | Zneg p -> Z0 - + (** val compare : z -> z -> comparison **) - + let compare x y = match x with | Z0 -> (match y with | Z0 -> Eq - | Zpos y' -> Lt - | Zneg y' -> Gt) + | Zpos _ -> Lt + | Zneg _ -> Gt) | Zpos x' -> (match y with | Zpos y' -> Coq_Pos.compare x' y' @@ -2167,151 +402,74 @@ module Z = (match y with | Zneg y' -> compOpp (Coq_Pos.compare x' y') | _ -> Lt) - - (** val sgn : z -> z **) - - let sgn = function - | Z0 -> Z0 - | Zpos p -> Zpos XH - | Zneg p -> Zneg XH - + (** val leb : z -> z -> bool **) - + let leb x y = match compare x y with | Gt -> false | _ -> true - - (** val geb : z -> z -> bool **) - - let geb x y = - match compare x y with - | Lt -> 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 eqb : z -> z -> bool **) - - let eqb x y = - match x with - | Z0 -> - (match y with - | Z0 -> true - | _ -> false) - | Zpos p -> - (match y with - | Zpos q0 -> Coq_Pos.eqb p q0 - | _ -> false) - | Zneg p -> - (match y with - | Zneg q0 -> Coq_Pos.eqb p q0 - | _ -> false) - + (** val max : z -> z -> z **) - + let max n0 m = match compare n0 m with | Lt -> m | _ -> n0 - - (** val min : z -> z -> z **) - - let min n0 m = - match compare n0 m with - | Gt -> m - | _ -> n0 - + (** val abs : z -> z **) - + let abs = function | Zneg p -> Zpos p | x -> x - - (** val abs_nat : z -> nat **) - - let abs_nat = function - | Z0 -> O - | Zpos p -> Coq_Pos.to_nat p - | Zneg p -> Coq_Pos.to_nat p - - (** val abs_N : z -> n **) - - let abs_N = function - | Z0 -> N0 - | Zpos p -> Npos p - | Zneg p -> Npos p - - (** val to_nat : z -> nat **) - - let to_nat = function - | Zpos p -> Coq_Pos.to_nat p - | _ -> O - + (** val to_N : z -> n **) - + let to_N = function | Zpos p -> Npos p | _ -> N0 - - (** val of_nat : nat -> z **) - - let of_nat = function - | O -> Z0 - | S n1 -> Zpos (Coq_Pos.of_succ_nat n1) - - (** val of_N : n -> z **) - - let of_N = function - | N0 -> Z0 - | Npos p -> Zpos p - - (** val iter : z -> ('a1 -> 'a1) -> 'a1 -> 'a1 **) - - let iter n0 f x = - match n0 with - | Zpos p -> Coq_Pos.iter p f x - | _ -> x - + (** 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 gtb b r' + 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 gtb b r' + 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 geb b (Zpos (XO XH)) then Z0,(Zpos XH) else (Zpos XH),Z0 - + | 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 p -> pos_div_eucl a' b + | Zpos _ -> pos_div_eucl a' b | Zneg b' -> let q0,r = pos_div_eucl a' (Zpos b') in (match r with @@ -2320,131 +478,20 @@ module Z = | Zneg a' -> (match b with | Z0 -> Z0,Z0 - | Zpos p -> + | 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,x = div_eucl a b in q0 - - (** val modulo : z -> z -> z **) - - let modulo a b = - let x,r = div_eucl a b in r - - (** val quotrem : z -> z -> z * z **) - - let quotrem a b = - match a with - | Z0 -> Z0,Z0 - | Zpos a0 -> - (match b with - | Z0 -> Z0,a - | Zpos b0 -> - let q0,r = N.pos_div_eucl a0 (Npos b0) in (of_N q0),(of_N r) - | Zneg b0 -> - let q0,r = N.pos_div_eucl a0 (Npos b0) in (opp (of_N q0)),(of_N r)) - | Zneg a0 -> - (match b with - | Z0 -> Z0,a - | Zpos b0 -> - let q0,r = N.pos_div_eucl a0 (Npos b0) in - (opp (of_N q0)),(opp (of_N r)) - | Zneg b0 -> - let q0,r = N.pos_div_eucl a0 (Npos b0) in (of_N q0),(opp (of_N r))) - - (** val quot : z -> z -> z **) - - let quot a b = - fst (quotrem a b) - - (** val rem : z -> z -> z **) - - let rem a b = - snd (quotrem a b) - - (** val even : z -> bool **) - - let even = function - | Z0 -> true - | Zpos p -> - (match p with - | XO p2 -> true - | _ -> false) - | Zneg p -> - (match p with - | XO p2 -> true - | _ -> false) - - (** val odd : z -> bool **) - - let odd = function - | Z0 -> false - | Zpos p -> - (match p with - | XO p2 -> false - | _ -> true) - | Zneg p -> - (match p with - | XO p2 -> false - | _ -> true) - - (** val div2 : z -> z **) - - let div2 = function - | Z0 -> Z0 - | Zpos p -> - (match p with - | XH -> Z0 - | _ -> Zpos (Coq_Pos.div2 p)) - | Zneg p -> Zneg (Coq_Pos.div2_up p) - - (** val quot2 : z -> z **) - - let quot2 = function - | Z0 -> Z0 - | Zpos p -> - (match p with - | XH -> Z0 - | _ -> Zpos (Coq_Pos.div2 p)) - | Zneg p -> - (match p with - | XH -> Z0 - | _ -> Zneg (Coq_Pos.div2 p)) - - (** val log2 : z -> z **) - - let log2 = function - | Zpos p2 -> - (match p2 with - | XI p -> Zpos (Coq_Pos.size p) - | XO p -> Zpos (Coq_Pos.size p) - | XH -> Z0) - | _ -> Z0 - - (** val sqrtrem : z -> z * z **) - - let sqrtrem = function - | Zpos p -> - let s,m = Coq_Pos.sqrtrem p in - (match m with - | Coq_Pos.IsPos r -> (Zpos s),(Zpos r) - | _ -> (Zpos s),Z0) - | _ -> Z0,Z0 - - (** val sqrt : z -> z **) - - let sqrt = function - | Zpos p -> Zpos (Coq_Pos.sqrt p) - | _ -> Z0 - + let q0,_ = div_eucl a b in q0 + (** val gcd : z -> z -> z **) - + let gcd a b = match a with | Z0 -> abs b @@ -2458,316 +505,6 @@ module Z = | Z0 -> abs a | Zpos b0 -> Zpos (Coq_Pos.gcd a0 b0) | Zneg b0 -> Zpos (Coq_Pos.gcd a0 b0)) - - (** val ggcd : z -> z -> z * (z * z) **) - - let ggcd a b = - match a with - | Z0 -> (abs b),(Z0,(sgn b)) - | Zpos a0 -> - (match b with - | Z0 -> (abs a),((sgn a),Z0) - | Zpos b0 -> - let g,p = Coq_Pos.ggcd a0 b0 in - let aa,bb = p in (Zpos g),((Zpos aa),(Zpos bb)) - | Zneg b0 -> - let g,p = Coq_Pos.ggcd a0 b0 in - let aa,bb = p in (Zpos g),((Zpos aa),(Zneg bb))) - | Zneg a0 -> - (match b with - | Z0 -> (abs a),((sgn a),Z0) - | Zpos b0 -> - let g,p = Coq_Pos.ggcd a0 b0 in - let aa,bb = p in (Zpos g),((Zneg aa),(Zpos bb)) - | Zneg b0 -> - let g,p = Coq_Pos.ggcd a0 b0 in - let aa,bb = p in (Zpos g),((Zneg aa),(Zneg bb))) - - (** val testbit : z -> z -> bool **) - - let testbit a = function - | Z0 -> odd a - | Zpos p -> - (match a with - | Z0 -> false - | Zpos a0 -> Coq_Pos.testbit a0 (Npos p) - | Zneg a0 -> negb (N.testbit (Coq_Pos.pred_N a0) (Npos p))) - | Zneg p -> false - - (** val shiftl : z -> z -> z **) - - let shiftl a = function - | Z0 -> a - | Zpos p -> Coq_Pos.iter p (mul (Zpos (XO XH))) a - | Zneg p -> Coq_Pos.iter p div2 a - - (** val shiftr : z -> z -> z **) - - let shiftr a n0 = - shiftl a (opp n0) - - (** val coq_lor : z -> z -> z **) - - let coq_lor a b = - match a with - | Z0 -> b - | Zpos a0 -> - (match b with - | Z0 -> a - | Zpos b0 -> Zpos (Coq_Pos.coq_lor a0 b0) - | Zneg b0 -> Zneg (N.succ_pos (N.ldiff (Coq_Pos.pred_N b0) (Npos a0)))) - | Zneg a0 -> - (match b with - | Z0 -> a - | Zpos b0 -> Zneg (N.succ_pos (N.ldiff (Coq_Pos.pred_N a0) (Npos b0))) - | Zneg b0 -> - Zneg - (N.succ_pos (N.coq_land (Coq_Pos.pred_N a0) (Coq_Pos.pred_N b0)))) - - (** val coq_land : z -> z -> z **) - - let coq_land a b = - match a with - | Z0 -> Z0 - | Zpos a0 -> - (match b with - | Z0 -> Z0 - | Zpos b0 -> of_N (Coq_Pos.coq_land a0 b0) - | Zneg b0 -> of_N (N.ldiff (Npos a0) (Coq_Pos.pred_N b0))) - | Zneg a0 -> - (match b with - | Z0 -> Z0 - | Zpos b0 -> of_N (N.ldiff (Npos b0) (Coq_Pos.pred_N a0)) - | Zneg b0 -> - Zneg - (N.succ_pos (N.coq_lor (Coq_Pos.pred_N a0) (Coq_Pos.pred_N b0)))) - - (** val ldiff : z -> z -> z **) - - let ldiff a b = - match a with - | Z0 -> Z0 - | Zpos a0 -> - (match b with - | Z0 -> a - | Zpos b0 -> of_N (Coq_Pos.ldiff a0 b0) - | Zneg b0 -> of_N (N.coq_land (Npos a0) (Coq_Pos.pred_N b0))) - | Zneg a0 -> - (match b with - | Z0 -> a - | Zpos b0 -> - Zneg (N.succ_pos (N.coq_lor (Coq_Pos.pred_N a0) (Npos b0))) - | Zneg b0 -> of_N (N.ldiff (Coq_Pos.pred_N b0) (Coq_Pos.pred_N a0))) - - (** val coq_lxor : z -> z -> z **) - - let coq_lxor a b = - match a with - | Z0 -> b - | Zpos a0 -> - (match b with - | Z0 -> a - | Zpos b0 -> of_N (Coq_Pos.coq_lxor a0 b0) - | Zneg b0 -> - Zneg (N.succ_pos (N.coq_lxor (Npos a0) (Coq_Pos.pred_N b0)))) - | Zneg a0 -> - (match b with - | Z0 -> a - | Zpos b0 -> - Zneg (N.succ_pos (N.coq_lxor (Coq_Pos.pred_N a0) (Npos b0))) - | Zneg b0 -> of_N (N.coq_lxor (Coq_Pos.pred_N a0) (Coq_Pos.pred_N b0))) - - (** val eq_dec : z -> z -> bool **) - - let eq_dec x y = - match x with - | Z0 -> - (match y with - | Z0 -> true - | _ -> false) - | Zpos x0 -> - (match y with - | Zpos p2 -> Coq_Pos.eq_dec x0 p2 - | _ -> false) - | Zneg x0 -> - (match y with - | Zneg p2 -> Coq_Pos.eq_dec x0 p2 - | _ -> false) - - module BootStrap = - struct - - end - - module OrderElts = - struct - type t = z - end - - module OrderTac = MakeOrderTac(OrderElts) - - (** val sqrt_up : z -> z **) - - let sqrt_up a = - match compare Z0 a with - | Lt -> succ (sqrt (pred a)) - | _ -> Z0 - - (** val log2_up : z -> z **) - - let log2_up a = - match compare (Zpos XH) a with - | Lt -> succ (log2 (pred a)) - | _ -> Z0 - - module NZDivP = - struct - - end - - module Quot2Div = - struct - (** val div : z -> z -> z **) - - let div = - quot - - (** val modulo : z -> z -> z **) - - let modulo = - rem - end - - module NZQuot = - struct - - end - - (** val lcm : z -> z -> z **) - - let lcm a b = - abs (mul a (div b (gcd a b))) - - (** val b2z : bool -> z **) - - let b2z = function - | true -> Zpos XH - | false -> Z0 - - (** val setbit : z -> z -> z **) - - let setbit a n0 = - coq_lor a (shiftl (Zpos XH) n0) - - (** val clearbit : z -> z -> z **) - - let clearbit a n0 = - ldiff a (shiftl (Zpos XH) n0) - - (** val lnot : z -> z **) - - let lnot a = - pred (opp a) - - (** val ones : z -> z **) - - let ones n0 = - pred (shiftl (Zpos XH) n0) - - module T = - struct - - end - - module ORev = - struct - type t = z - end - - module MRev = - struct - (** val max : z -> z -> z **) - - let max x y = - min y x - end - - module MPRev = MaxLogicalProperties(ORev)(MRev) - - module P = - struct - (** val max_case_strong : - z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) - -> 'a1 **) - - let max_case_strong n0 m compat hl hr = - let c = compSpec2Type n0 m (compare n0 m) in - (match c with - | CompGtT -> compat n0 (max n0 m) __ (hl __) - | _ -> compat m (max n0 m) __ (hr __)) - - (** val max_case : - z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **) - - let max_case n0 m x x0 x1 = - max_case_strong n0 m x (fun _ -> x0) (fun _ -> x1) - - (** val max_dec : z -> z -> bool **) - - let max_dec n0 m = - max_case n0 m (fun x y _ h0 -> h0) true false - - (** val min_case_strong : - z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) - -> 'a1 **) - - let min_case_strong n0 m compat hl hr = - let c = compSpec2Type n0 m (compare n0 m) in - (match c with - | CompGtT -> compat m (min n0 m) __ (hr __) - | _ -> compat n0 (min n0 m) __ (hl __)) - - (** val min_case : - z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **) - - let min_case n0 m x x0 x1 = - min_case_strong n0 m x (fun _ -> x0) (fun _ -> x1) - - (** val min_dec : z -> z -> bool **) - - let min_dec n0 m = - min_case n0 m (fun x y _ h0 -> h0) true false - end - - (** val max_case_strong : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) - - let max_case_strong n0 m x x0 = - P.max_case_strong n0 m (fun x1 y _ x2 -> x2) x x0 - - (** val max_case : z -> z -> 'a1 -> 'a1 -> 'a1 **) - - let max_case n0 m x x0 = - max_case_strong n0 m (fun _ -> x) (fun _ -> x0) - - (** val max_dec : z -> z -> bool **) - - let max_dec = - P.max_dec - - (** val min_case_strong : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) - - let min_case_strong n0 m x x0 = - P.min_case_strong n0 m (fun x1 y _ x2 -> x2) x x0 - - (** val min_case : z -> z -> 'a1 -> 'a1 -> 'a1 **) - - let min_case n0 m x x0 = - min_case_strong n0 m (fun _ -> x) (fun _ -> x0) - - (** val min_dec : z -> z -> bool **) - - let min_dec = - P.min_dec end (** val zeq_bool : z -> z -> bool **) @@ -2818,9 +555,9 @@ let rec peq ceqb p p' = (** val mkPinj : positive -> 'a1 pol -> 'a1 pol **) let mkPinj j p = match p with -| Pc c -> p +| Pc _ -> p | Pinj (j', q0) -> Pinj ((Coq_Pos.add j j'), q0) -| PX (p2, p3, p4) -> Pinj (j, p) +| PX (_, _, _) -> Pinj (j, p) (** val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol **) @@ -2831,12 +568,13 @@ let mkPinj_pred j p = | XH -> p (** val mkPX : - 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) + 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 + pol **) let mkPX cO ceqb p i q0 = match p with | Pc c -> if ceqb c cO then mkPinj XH q0 else PX (p, i, q0) - | Pinj (p2, p3) -> 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) @@ -2893,8 +631,8 @@ let rec paddI cadd pop q0 j = function | XH -> PX (p2, i, (pop q' q0))) (** val psubI : - ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> - 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) + ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) + -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) let rec psubI cadd copp pop q0 j = function | Pc c -> mkPinj j (paddC cadd (popp copp q0) c) @@ -2911,11 +649,11 @@ let rec psubI cadd copp pop q0 j = function | XH -> PX (p2, i, (pop q' q0))) (** val paddX : - 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol - -> positive -> 'a1 pol -> 'a1 pol **) + 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 + pol -> positive -> 'a1 pol -> 'a1 pol **) let rec paddX cO ceqb pop p' i' p = match p with -| Pc c -> PX (p', i', p) +| Pc _ -> PX (p', i', p) | Pinj (j, q') -> (match j with | XI j0 -> PX (p', i', (Pinj ((XO j0), q'))) @@ -2928,15 +666,16 @@ let rec paddX cO ceqb pop p' i' p = match p with | Zneg k -> mkPX cO ceqb (paddX cO ceqb pop p' k p2) i q') (** val psubX : - 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 - pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) + 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> + 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) let rec psubX cO copp ceqb pop p' i' p = match p with -| Pc c -> PX ((popp copp p'), i', p) +| Pc _ -> PX ((popp copp p'), i', p) | Pinj (j, q') -> (match j with | XI j0 -> PX ((popp copp p'), i', (Pinj ((XO j0), q'))) - | XO j0 -> PX ((popp copp p'), i', (Pinj ((Coq_Pos.pred_double j0), q'))) + | XO j0 -> + PX ((popp copp p'), i', (Pinj ((Coq_Pos.pred_double j0), q'))) | XH -> PX ((popp copp p'), i', q')) | PX (p2, i, q') -> (match Z.pos_sub i i' with @@ -2945,8 +684,8 @@ let rec psubX cO copp ceqb pop p' i' p = match p with | Zneg k -> mkPX cO ceqb (psubX cO copp ceqb pop p' k p2) i q') (** val padd : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol - -> 'a1 pol **) + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 + pol -> 'a1 pol **) let rec padd cO cadd ceqb p = function | Pc c' -> paddC cadd p c' @@ -2964,7 +703,8 @@ let rec padd cO cadd ceqb p = function | PX (p2, i, q0) -> (match Z.pos_sub i i' with | Z0 -> - mkPX cO ceqb (padd cO cadd ceqb p2 p'0) i (padd cO cadd ceqb q0 q') + mkPX cO ceqb (padd cO cadd ceqb p2 p'0) i + (padd cO cadd ceqb q0 q') | Zpos k -> mkPX cO ceqb (padd cO cadd ceqb (PX (p2, k, (p0 cO))) p'0) i' (padd cO cadd ceqb q0 q') @@ -2973,8 +713,8 @@ let rec padd cO cadd ceqb p = function (padd cO cadd ceqb q0 q'))) (** val psub : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 - -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> + ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) let rec psub cO cadd csub copp ceqb p = function | Pc c' -> psubC csub p c' @@ -2989,25 +729,27 @@ let rec psub cO cadd csub copp ceqb p = function (psub cO cadd csub copp ceqb (Pinj ((XO j0), q0)) q')) | XO j0 -> PX ((popp copp p'0), i', - (psub cO cadd csub copp ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) - q')) - | XH -> PX ((popp copp p'0), i', (psub cO cadd csub copp ceqb q0 q'))) + (psub cO cadd csub copp ceqb (Pinj ((Coq_Pos.pred_double j0), + q0)) q')) + | XH -> + PX ((popp copp p'0), i', (psub cO cadd csub copp ceqb q0 q'))) | PX (p2, i, q0) -> (match Z.pos_sub i i' with | Z0 -> mkPX cO ceqb (psub cO cadd csub copp ceqb p2 p'0) i (psub cO cadd csub copp ceqb q0 q') | Zpos k -> - mkPX cO ceqb (psub cO cadd csub copp ceqb (PX (p2, k, (p0 cO))) p'0) - i' (psub cO cadd csub copp ceqb q0 q') + mkPX cO ceqb + (psub cO cadd csub copp ceqb (PX (p2, k, (p0 cO))) p'0) i' + (psub cO cadd csub copp ceqb q0 q') | Zneg k -> mkPX cO ceqb (psubX cO copp ceqb (psub cO cadd csub copp ceqb) p'0 k p2) i (psub cO cadd csub copp ceqb q0 q'))) (** val pmulC_aux : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> - 'a1 pol **) + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 + -> 'a1 pol **) let rec pmulC_aux cO cmul ceqb p c = match p with @@ -3018,8 +760,8 @@ let rec pmulC_aux cO cmul ceqb p c = (pmulC_aux cO cmul ceqb q0 c) (** val pmulC : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> - 'a1 -> 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol + -> 'a1 -> 'a1 pol **) let pmulC cO cI cmul ceqb p c = if ceqb c cO @@ -3027,8 +769,8 @@ let pmulC cO cI cmul ceqb p c = else if ceqb c cI then p else pmulC_aux cO cmul ceqb p c (** val pmulI : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> - 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol + -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) let rec pmulI cO cI cmul ceqb pmul0 q0 j = function | Pc c -> mkPinj j (pmulC cO cI cmul ceqb q0 c) @@ -3049,12 +791,13 @@ let rec pmulI cO cI cmul ceqb pmul0 q0 j = function mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 XH p') i' (pmul0 q' q0)) (** val pmul : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) let rec pmul cO cI cadd cmul ceqb p p'' = match p'' with | Pc c -> pmulC cO cI cmul ceqb p c -| Pinj (j', q') -> pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' j' p +| Pinj (j', q') -> + pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' j' p | PX (p', i', q') -> (match p with | Pc c -> pmulC cO cI cmul ceqb p'' c @@ -3063,22 +806,24 @@ let rec pmul cO cI cadd cmul ceqb p p'' = match p'' with match j with | XI j0 -> pmul cO cI cadd cmul ceqb (Pinj ((XO j0), q0)) q' | XO j0 -> - pmul cO cI cadd cmul ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) q' + pmul cO cI cadd cmul ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) + q' | XH -> pmul cO cI cadd cmul ceqb q0 q' in mkPX cO ceqb (pmul cO cI cadd cmul ceqb p p') i' qQ' | PX (p2, i, q0) -> let qQ' = pmul cO cI cadd cmul ceqb q0 q' in - let pQ' = pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' XH p2 in + let pQ' = pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' XH p2 + in let qP' = pmul cO cI cadd cmul ceqb (mkPinj XH q0) p' in let pP' = pmul cO cI cadd cmul ceqb p2 p' in padd cO cadd ceqb - (mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb pP' i (p0 cO)) qP') i' - (p0 cO)) (mkPX cO ceqb pQ' i qQ')) + (mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb pP' i (p0 cO)) qP') + i' (p0 cO)) (mkPX cO ceqb pQ' i qQ')) (** val psquare : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> 'a1 pol -> 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1 -> bool) -> 'a1 pol -> 'a1 pol **) let rec psquare cO cI cadd cmul ceqb = function | Pc c -> Pc (cmul c c) @@ -3107,9 +852,9 @@ let mk_X cO cI j = mkPinj_pred j (mkX cO cI) (** val ppow_pos : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 - pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive + -> 'a1 pol **) let rec ppow_pos cO cI cadd cmul ceqb subst_l res p = function | XI p3 -> @@ -3123,16 +868,17 @@ let rec ppow_pos cO cI cadd cmul ceqb subst_l res p = function | XH -> subst_l (pmul cO cI cadd cmul ceqb res p) (** val ppow_N : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol **) let ppow_N cO cI cadd cmul ceqb subst_l p = function | N0 -> p1 cI | Npos p2 -> ppow_pos cO cI cadd cmul ceqb subst_l (p1 cI) p p2 (** val norm_aux : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> + 'a1 pol **) let rec norm_aux cO cI cadd cmul csub copp ceqb = function | PEc c -> Pc c @@ -3153,7 +899,8 @@ let rec norm_aux cO cI cadd cmul csub copp ceqb = function padd cO cadd ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) (norm_aux cO cI cadd cmul csub copp ceqb pe2))) | PEsub (pe1, pe2) -> - psub cO cadd csub copp ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) + psub cO cadd csub copp ceqb + (norm_aux cO cI cadd cmul csub copp ceqb pe1) (norm_aux cO cI cadd cmul csub copp ceqb pe2) | PEmul (pe1, pe2) -> pmul cO cI cadd cmul ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) @@ -3185,9 +932,9 @@ let rec map_bformula fct = function | N f0 -> N (map_bformula fct f0) | I (f1, f2) -> I ((map_bformula fct f1), (map_bformula fct f2)) -type 'term' clause = 'term' list +type 'x clause = 'x list -type 'term' cnf = 'term' clause list +type 'x cnf = 'x clause list (** val tt : 'a1 cnf **) @@ -3200,52 +947,52 @@ let ff = []::[] (** val add_term : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> 'a1 - clause option **) + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> + 'a1 clause option **) -let rec add_term unsat deduce t1 = function +let rec add_term unsat deduce t0 = function | [] -> - (match deduce t1 t1 with - | Some u -> if unsat u then None else Some (t1::[]) - | None -> Some (t1::[])) + (match deduce t0 t0 with + | Some u -> if unsat u then None else Some (t0::[]) + | None -> Some (t0::[])) | t'::cl0 -> - (match deduce t1 t' with + (match deduce t0 t' with | Some u -> if unsat u then None - else (match add_term unsat deduce t1 cl0 with + else (match add_term unsat deduce t0 cl0 with | Some cl' -> Some (t'::cl') | None -> None) | None -> - (match add_term unsat deduce t1 cl0 with + (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 **) + ('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 - | t1::cl -> - (match add_term unsat deduce t1 cl2 with + | 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 **) + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf + -> 'a1 cnf **) -let or_clause_cnf unsat deduce t1 f = +let or_clause_cnf unsat deduce t0 f = fold_right (fun e acc -> - match or_clause unsat deduce t1 e with + 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 **) + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 cnf -> 'a1 cnf -> + 'a1 cnf **) let rec or_cnf unsat deduce f f' = match f with @@ -3259,8 +1006,8 @@ 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 **) + ('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 @@ -3300,9 +1047,9 @@ let rec cnf_checker checker f l = | c::l0 -> if checker e c then cnf_checker checker f0 l0 else false) (** val tauto_checker : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 - -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 bFormula -> 'a3 list -> - bool **) + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> + ('a1 -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 bFormula -> 'a3 + list -> bool **) let tauto_checker unsat deduce normalise0 negate0 checker f w = cnf_checker checker (xcnf unsat deduce normalise0 negate0 true f) w @@ -3335,18 +1082,18 @@ let opMult o o' = | Equal -> Some Equal | NonEqual -> (match o' with - | Strict -> None - | NonStrict -> None - | x -> Some x) + | Equal -> Some Equal + | NonEqual -> Some NonEqual + | _ -> None) | Strict -> (match o' with | NonEqual -> None | _ -> Some o') | NonStrict -> (match o' with + | Equal -> Some Equal | NonEqual -> None - | Strict -> Some NonStrict - | x -> Some x) + | _ -> Some NonStrict) (** val opAdd : op1 -> op1 -> op1 option **) @@ -3394,8 +1141,8 @@ let map_option2 f o o' = | None -> None (** val pexpr_times_nformula : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1 -> bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option **) let pexpr_times_nformula cO cI cplus ctimes ceqb e = function | ef,o -> @@ -3404,8 +1151,8 @@ let pexpr_times_nformula cO cI cplus ctimes ceqb e = function | _ -> None) (** val nformula_times_nformula : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option **) let nformula_times_nformula cO cI cplus ctimes ceqb f1 f2 = let e1,o1 = f1 in @@ -3414,8 +1161,8 @@ let nformula_times_nformula cO cI cplus ctimes ceqb f1 f2 = (opMult o1 o2) (** val nformula_plus_nformula : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 - nFormula -> 'a1 nFormula option **) + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> + 'a1 nFormula -> 'a1 nFormula option **) let nformula_plus_nformula cO cplus ceqb f1 f2 = let e1,o1 = f1 in @@ -3423,9 +1170,9 @@ let nformula_plus_nformula cO cplus ceqb f1 f2 = map_option (fun x -> Some ((padd cO cplus ceqb e1 e2),x)) (opAdd o1 o2) (** val eval_Psatz : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1 - nFormula option **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz + -> 'a1 nFormula option **) let rec eval_Psatz cO cI cplus ctimes ceqb cleb l = function | PsatzIn n0 -> Some (nth n0 l ((Pc cO),Equal)) @@ -3460,9 +1207,9 @@ let check_inconsistent cO ceqb cleb = function | _ -> false) (** val check_normalised_formulas : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> - bool **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz + -> bool **) let check_normalised_formulas cO cI cplus ctimes ceqb cleb l cm = match eval_Psatz cO cI cplus ctimes ceqb cleb l cm with @@ -3479,51 +1226,41 @@ type op2 = type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr } -(** val flhs : 'a1 formula -> 'a1 pExpr **) - -let flhs x = x.flhs - -(** val fop : 'a1 formula -> op2 **) - -let fop x = x.fop - -(** val frhs : 'a1 formula -> 'a1 pExpr **) - -let frhs x = x.frhs - (** val norm : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> + 'a1 pol **) let norm cO cI cplus ctimes cminus copp ceqb = norm_aux cO cI cplus ctimes cminus copp ceqb (** val psub0 : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 - -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> + ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) let psub0 cO cplus cminus copp ceqb = psub cO cplus cminus copp ceqb (** val padd0 : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol - -> 'a1 pol **) + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 + pol -> 'a1 pol **) let padd0 cO cplus ceqb = padd cO cplus ceqb (** val xnormalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 - nFormula list **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> + 'a1 nFormula list **) -let xnormalise cO cI cplus ctimes cminus copp ceqb t1 = - let { flhs = lhs; fop = o; frhs = rhs } = t1 in +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 + ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::(((psub0 cO + cplus cminus copp ceqb rhs0 lhs0),Strict)::[]) @@ -3534,26 +1271,27 @@ let xnormalise cO cI cplus ctimes cminus copp ceqb t1 = | OpGt -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),NonStrict)::[]) (** val cnf_normalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 - nFormula cnf **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> + 'a1 nFormula cnf **) -let cnf_normalise cO cI cplus ctimes cminus copp ceqb t1 = - map (fun x -> x::[]) (xnormalise cO cI cplus ctimes cminus copp ceqb t1) +let cnf_normalise cO cI cplus ctimes cminus copp ceqb t0 = + map (fun x -> x::[]) (xnormalise cO cI cplus ctimes cminus copp ceqb t0) (** val xnegate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 - nFormula list **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> + 'a1 nFormula list **) -let xnegate cO cI cplus ctimes cminus copp ceqb t1 = - let { flhs = lhs; fop = o; frhs = rhs } = t1 in +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 + ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::(((psub0 cO + cplus cminus copp ceqb rhs0 lhs0),Strict)::[]) @@ -3563,12 +1301,12 @@ let xnegate cO cI cplus ctimes cminus copp ceqb t1 = | OpGt -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::[]) (** val cnf_negate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 - nFormula cnf **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> + 'a1 nFormula cnf **) -let cnf_negate cO cI cplus ctimes cminus copp ceqb t1 = - map (fun x -> x::[]) (xnegate cO cI cplus ctimes cminus copp ceqb t1) +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 **) @@ -3602,14 +1340,14 @@ let map_Formula c_of_S f = { flhs = (map_PExpr c_of_S l); fop = o; frhs = (map_PExpr c_of_S r) } (** val simpl_cone : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz -> - 'a1 psatz **) + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz + -> 'a1 psatz **) let simpl_cone cO cI ctimes ceqb e = match e with -| PsatzSquare t1 -> - (match t1 with +| PsatzSquare t0 -> + (match t0 with | Pc c -> if ceqb cO c then PsatzZ else PsatzC (ctimes c c) - | _ -> PsatzSquare t1) + | _ -> PsatzSquare t0) | PsatzMulE (t1, t2) -> (match t1 with | PsatzMulE (x, x0) -> @@ -3641,7 +1379,8 @@ let simpl_cone cO cI ctimes ceqb e = match e with | PsatzC p2 -> PsatzMulE ((PsatzC (ctimes c p2)), x) | _ -> if ceqb cI c then t2 else PsatzMulE (t1, t2))) | PsatzAdd (y, z0) -> - PsatzAdd ((PsatzMulE ((PsatzC c), y)), (PsatzMulE ((PsatzC c), z0))) + PsatzAdd ((PsatzMulE ((PsatzC c), y)), (PsatzMulE ((PsatzC c), + z0))) | PsatzC c0 -> PsatzC (ctimes c c0) | PsatzZ -> PsatzZ | _ -> if ceqb cI c then t2 else PsatzMulE (t1, t2)) @@ -3683,7 +1422,8 @@ let qle_bool x y = (** val qplus : q -> q -> q **) let qplus x y = - { qnum = (Z.add (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))); + { qnum = + (Z.add (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))); qden = (Coq_Pos.mul x.qden y.qden) } (** val qmult : q -> q -> q **) @@ -3711,8 +1451,8 @@ let qinv x = (** val qpower_positive : q -> positive -> q **) -let qpower_positive q0 p = - pow_pos qmult q0 p +let qpower_positive = + pow_pos qmult (** val qpower : q -> z -> q **) @@ -3721,12 +1461,12 @@ let qpower q0 = function | Zpos p -> qpower_positive q0 p | Zneg p -> qinv (qpower_positive q0 p) -type 'a t0 = +type 'a t = | Empty | Leaf of 'a -| Node of 'a t0 * 'a * 'a t0 +| Node of 'a t * 'a * 'a t -(** val find : 'a1 -> 'a1 t0 -> positive -> 'a1 **) +(** val find : 'a1 -> 'a1 t -> positive -> 'a1 **) let rec find default vm p = match vm with @@ -3738,6 +1478,29 @@ let rec find default vm p = | 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 **) @@ -3762,8 +1525,8 @@ let norm0 = (** val xnormalise0 : z formula -> z nFormula list **) -let xnormalise0 t1 = - let { flhs = lhs; fop = o; frhs = rhs } = t1 in +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 @@ -3780,13 +1543,13 @@ let xnormalise0 t1 = (** val normalise : z formula -> z nFormula cnf **) -let normalise t1 = - map (fun x -> x::[]) (xnormalise0 t1) +let normalise t0 = + map (fun x -> x::[]) (xnormalise0 t0) (** val xnegate0 : z formula -> z nFormula list **) -let xnegate0 t1 = - let { flhs = lhs; fop = o; frhs = rhs } = t1 in +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 @@ -3803,8 +1566,8 @@ let xnegate0 t1 = (** val negate : z formula -> z nFormula cnf **) -let negate t1 = - map (fun x -> x::[]) (xnegate0 t1) +let negate t0 = + map (fun x -> x::[]) (xnegate0 t0) (** val zunsat : z nFormula -> bool **) @@ -3839,8 +1602,8 @@ let zgcdM x y = let rec zgcd_pol = function | Pc c -> Z0,c -| Pinj (p2, p3) -> zgcd_pol p3 -| PX (p2, p3, q0) -> +| 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 @@ -3872,7 +1635,8 @@ let genCuttingPlane = function then None else Some ((makeCuttingPlane e),Equal) | NonEqual -> Some ((e,Z0),op) - | Strict -> Some ((makeCuttingPlane (psubC Z.sub e (Zpos XH))),NonStrict) + | Strict -> + Some ((makeCuttingPlane (psubC Z.sub e (Zpos XH))),NonStrict) | NonStrict -> Some ((makeCuttingPlane e),NonStrict)) (** val nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula **) @@ -3966,8 +1730,8 @@ let qnormalise = (** val qnegate : q formula -> q nFormula cnf **) let qnegate = - cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus - qmult qminus qopp qeq_bool + cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } + qplus qmult qminus qopp qeq_bool (** val qunsat : q nFormula -> bool **) @@ -4025,8 +1789,8 @@ let rnormalise = (** val rnegate : q formula -> q nFormula cnf **) let rnegate = - cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus - qmult qminus qopp qeq_bool + cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } + qplus qmult qminus qopp qeq_bool (** val runsat : q nFormula -> bool **) @@ -4043,4 +1807,3 @@ let rdeduce = 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 index bcd61f39b..beb042f49 100644 --- a/plugins/micromega/micromega.mli +++ b/plugins/micromega/micromega.mli @@ -1,15 +1,9 @@ -type __ = Obj.t - val negb : bool -> bool type nat = | O | S of nat -val fst : ('a1 * 'a2) -> 'a1 - -val snd : ('a1 * 'a2) -> 'a2 - val app : 'a1 list -> 'a1 list -> 'a1 list type comparison = @@ -19,24 +13,7 @@ type comparison = val compOpp : comparison -> comparison -type compareSpecT = -| CompEqT -| CompLtT -| CompGtT - -val compareSpec2Type : comparison -> compareSpecT - -type 'a compSpecT = compareSpecT - -val compSpec2Type : 'a1 -> 'a1 -> comparison -> 'a1 compSpecT - -type 'a sig0 = - 'a - (* singleton inductive, whose constructor was exist *) - -val plus : nat -> nat -> nat - -val nat_iter : nat -> ('a1 -> 'a1) -> 'a1 -> 'a1 +val add : nat -> nat -> nat type positive = | XI of positive @@ -52,560 +29,59 @@ type z = | Zpos of positive | Zneg of positive -module type TotalOrder' = - sig - type t - end - -module MakeOrderTac : - functor (O:TotalOrder') -> - sig - - end - -module MaxLogicalProperties : - functor (O:TotalOrder') -> - functor (M:sig - val max : O.t -> O.t -> O.t - end) -> - sig - module T : - sig - - end - end - -module Pos : - sig - type t = positive - - val succ : positive -> positive - - val add : positive -> positive -> positive - - val add_carry : positive -> positive -> positive - - val pred_double : positive -> positive - - val pred : positive -> positive - - val pred_N : positive -> n - +module Pos : + sig type mask = | IsNul | IsPos of positive | IsNeg - - val mask_rect : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 - - val mask_rec : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 - - val succ_double_mask : mask -> mask - - val double_mask : mask -> mask - - val double_pred_mask : positive -> mask - - val pred_mask : mask -> 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 iter : positive -> ('a1 -> 'a1) -> 'a1 -> 'a1 - - val pow : positive -> positive -> positive - - val div2 : positive -> positive - - val div2_up : positive -> positive - - val size_nat : positive -> nat - - val size : positive -> positive - - val compare_cont : positive -> positive -> comparison -> comparison - - val compare : positive -> positive -> comparison - - val min : positive -> positive -> positive - - val max : positive -> positive -> positive - - val eqb : positive -> positive -> bool - - val leb : positive -> positive -> bool - - val ltb : positive -> positive -> bool - - val sqrtrem_step : - (positive -> positive) -> (positive -> positive) -> (positive * mask) -> - positive * mask - - val sqrtrem : positive -> positive * mask - - val sqrt : positive -> positive - - val gcdn : nat -> positive -> positive -> positive - - val gcd : positive -> positive -> positive - - val ggcdn : nat -> positive -> positive -> positive * (positive * positive) - - val ggcd : positive -> positive -> positive * (positive * positive) - - val coq_Nsucc_double : n -> n - - val coq_Ndouble : n -> n - - val coq_lor : positive -> positive -> positive - - val coq_land : positive -> positive -> n - - val ldiff : positive -> positive -> n - - val coq_lxor : positive -> positive -> n - - val shiftl_nat : positive -> nat -> positive - - val shiftr_nat : positive -> nat -> positive - - val shiftl : positive -> n -> positive - - val shiftr : positive -> n -> positive - - val testbit_nat : positive -> nat -> bool - - val testbit : positive -> n -> bool - - val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1 - - val to_nat : positive -> nat - - val of_nat : nat -> positive - - val of_succ_nat : nat -> positive end -module Coq_Pos : - sig - module Coq__1 : sig - type t = positive - end - type t = Coq__1.t - +module Coq_Pos : + sig val succ : positive -> positive - + val add : positive -> positive -> positive - + val add_carry : positive -> positive -> positive - + val pred_double : positive -> positive - - val pred : positive -> positive - - val pred_N : positive -> n - + type mask = Pos.mask = | IsNul | IsPos of positive | IsNeg - - val mask_rect : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 - - val mask_rec : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 - + val succ_double_mask : mask -> mask - + val double_mask : mask -> mask - + val double_pred_mask : positive -> mask - - val pred_mask : mask -> 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 iter : positive -> ('a1 -> 'a1) -> 'a1 -> 'a1 - - val pow : positive -> positive -> positive - - val div2 : positive -> positive - - val div2_up : positive -> positive - + val size_nat : positive -> nat - - val size : positive -> positive - - val compare_cont : positive -> positive -> comparison -> comparison - + + val compare_cont : comparison -> positive -> positive -> comparison + val compare : positive -> positive -> comparison - - val min : positive -> positive -> positive - - val max : positive -> positive -> positive - - val eqb : positive -> positive -> bool - - val leb : positive -> positive -> bool - - val ltb : positive -> positive -> bool - - val sqrtrem_step : - (positive -> positive) -> (positive -> positive) -> (positive * mask) -> - positive * mask - - val sqrtrem : positive -> positive * mask - - val sqrt : positive -> positive - + val gcdn : nat -> positive -> positive -> positive - + val gcd : positive -> positive -> positive - - val ggcdn : nat -> positive -> positive -> positive * (positive * positive) - - val ggcd : positive -> positive -> positive * (positive * positive) - - val coq_Nsucc_double : n -> n - - val coq_Ndouble : n -> n - - val coq_lor : positive -> positive -> positive - - val coq_land : positive -> positive -> n - - val ldiff : positive -> positive -> n - - val coq_lxor : positive -> positive -> n - - val shiftl_nat : positive -> nat -> positive - - val shiftr_nat : positive -> nat -> positive - - val shiftl : positive -> n -> positive - - val shiftr : positive -> n -> positive - - val testbit_nat : positive -> nat -> bool - - val testbit : positive -> n -> bool - - val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1 - - val to_nat : positive -> nat - - val of_nat : nat -> positive - + val of_succ_nat : nat -> positive - - val eq_dec : positive -> positive -> bool - - val peano_rect : 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> 'a1 - - val peano_rec : 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> 'a1 - - type coq_PeanoView = - | PeanoOne - | PeanoSucc of positive * coq_PeanoView - - val coq_PeanoView_rect : - 'a1 -> (positive -> coq_PeanoView -> 'a1 -> 'a1) -> positive -> - coq_PeanoView -> 'a1 - - val coq_PeanoView_rec : - 'a1 -> (positive -> coq_PeanoView -> 'a1 -> 'a1) -> positive -> - coq_PeanoView -> 'a1 - - val peanoView_xO : positive -> coq_PeanoView -> coq_PeanoView - - val peanoView_xI : positive -> coq_PeanoView -> coq_PeanoView - - val peanoView : positive -> coq_PeanoView - - val coq_PeanoView_iter : - 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> coq_PeanoView -> 'a1 - - val switch_Eq : comparison -> comparison -> comparison - - val mask2cmp : mask -> comparison - - module T : - sig - - end - - module ORev : - sig - type t = Coq__1.t - end - - module MRev : - sig - val max : t -> t -> t - end - - module MPRev : - sig - module T : - sig - - end - end - - module P : - sig - val max_case_strong : - t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> - 'a1 - - val max_case : - t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 - - val max_dec : t -> t -> bool - - val min_case_strong : - t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> - 'a1 - - val min_case : - t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 - - val min_dec : t -> t -> bool - end - - val max_case_strong : t -> t -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 - - val max_case : t -> t -> 'a1 -> 'a1 -> 'a1 - - val max_dec : t -> t -> bool - - val min_case_strong : t -> t -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 - - val min_case : t -> t -> 'a1 -> 'a1 -> 'a1 - - val min_dec : t -> t -> bool end -module N : - sig - type t = n - - val zero : n - - val one : n - - val two : n - - val succ_double : n -> n - - val double : n -> n - - val succ : n -> n - - val pred : n -> n - - val succ_pos : n -> positive - - val add : n -> n -> n - - val sub : n -> n -> n - - val mul : n -> n -> n - - val compare : n -> n -> comparison - - val eqb : n -> n -> bool - - val leb : n -> n -> bool - - val ltb : n -> n -> bool - - val min : n -> n -> n - - val max : n -> n -> n - - val div2 : n -> n - - val even : n -> bool - - val odd : n -> bool - - val pow : n -> n -> n - - val log2 : n -> n - - val size : n -> n - - val size_nat : n -> nat - - val pos_div_eucl : positive -> n -> n * n - - val div_eucl : n -> n -> n * n - - val div : n -> n -> n - - val modulo : n -> n -> n - - val gcd : n -> n -> n - - val ggcd : n -> n -> n * (n * n) - - val sqrtrem : n -> n * n - - val sqrt : n -> n - - val coq_lor : n -> n -> n - - val coq_land : n -> n -> n - - val ldiff : n -> n -> n - - val coq_lxor : n -> n -> n - - val shiftl_nat : n -> nat -> n - - val shiftr_nat : n -> nat -> n - - val shiftl : n -> n -> n - - val shiftr : n -> n -> n - - val testbit_nat : n -> nat -> bool - - val testbit : n -> n -> bool - - val to_nat : n -> nat - +module N : + sig val of_nat : nat -> n - - val iter : n -> ('a1 -> 'a1) -> 'a1 -> 'a1 - - val eq_dec : n -> n -> bool - - val discr : n -> positive option - - val binary_rect : 'a1 -> (n -> 'a1 -> 'a1) -> (n -> 'a1 -> 'a1) -> n -> 'a1 - - val binary_rec : 'a1 -> (n -> 'a1 -> 'a1) -> (n -> 'a1 -> 'a1) -> n -> 'a1 - - val peano_rect : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 - - val peano_rec : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 - - module BootStrap : - sig - - end - - val recursion : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 - - module OrderElts : - sig - type t = n - end - - module OrderTac : - sig - - end - - module NZPowP : - sig - - end - - module NZSqrtP : - sig - - end - - val sqrt_up : n -> n - - val log2_up : n -> n - - module NZDivP : - sig - - end - - val lcm : n -> n -> n - - val b2n : bool -> n - - val setbit : n -> n -> n - - val clearbit : n -> n -> n - - val ones : n -> n - - val lnot : n -> n -> n - - module T : - sig - - end - - module ORev : - sig - type t = n - end - - module MRev : - sig - val max : n -> n -> n - end - - module MPRev : - sig - module T : - sig - - end - end - - module P : - sig - val max_case_strong : - n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> - 'a1 - - val max_case : - n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 - - val max_dec : n -> n -> bool - - val min_case_strong : - n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> - 'a1 - - val min_case : - n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 - - val min_dec : n -> n -> bool - end - - val max_case_strong : n -> n -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 - - val max_case : n -> n -> 'a1 -> 'a1 -> 'a1 - - val max_dec : n -> n -> bool - - val min_case_strong : n -> n -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 - - val min_case : n -> n -> 'a1 -> 'a1 -> 'a1 - - val min_dec : n -> n -> bool end val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 @@ -616,225 +92,45 @@ val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 -module Z : - sig - type t = z - - val zero : z - - val one : z - - val two : z - +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 succ : z -> z - - val pred : z -> z - + val sub : z -> z -> z - + val mul : z -> z -> z - - val pow_pos : z -> positive -> z - - val pow : z -> z -> z - + val compare : z -> z -> comparison - - val sgn : z -> z - + val leb : z -> z -> bool - - val geb : z -> z -> bool - + val ltb : z -> z -> bool - + val gtb : z -> z -> bool - - val eqb : z -> z -> bool - + val max : z -> z -> z - - val min : z -> z -> z - + val abs : z -> z - - val abs_nat : z -> nat - - val abs_N : z -> n - - val to_nat : z -> nat - + val to_N : z -> n - - val of_nat : nat -> z - - val of_N : n -> z - - val iter : z -> ('a1 -> 'a1) -> 'a1 -> 'a1 - + val pos_div_eucl : positive -> z -> z * z - + val div_eucl : z -> z -> z * z - + val div : z -> z -> z - - val modulo : z -> z -> z - - val quotrem : z -> z -> z * z - - val quot : z -> z -> z - - val rem : z -> z -> z - - val even : z -> bool - - val odd : z -> bool - - val div2 : z -> z - - val quot2 : z -> z - - val log2 : z -> z - - val sqrtrem : z -> z * z - - val sqrt : z -> z - + val gcd : z -> z -> z - - val ggcd : z -> z -> z * (z * z) - - val testbit : z -> z -> bool - - val shiftl : z -> z -> z - - val shiftr : z -> z -> z - - val coq_lor : z -> z -> z - - val coq_land : z -> z -> z - - val ldiff : z -> z -> z - - val coq_lxor : z -> z -> z - - val eq_dec : z -> z -> bool - - module BootStrap : - sig - - end - - module OrderElts : - sig - type t = z - end - - module OrderTac : - sig - - end - - val sqrt_up : z -> z - - val log2_up : z -> z - - module NZDivP : - sig - - end - - module Quot2Div : - sig - val div : z -> z -> z - - val modulo : z -> z -> z - end - - module NZQuot : - sig - - end - - val lcm : z -> z -> z - - val b2z : bool -> z - - val setbit : z -> z -> z - - val clearbit : z -> z -> z - - val lnot : z -> z - - val ones : z -> z - - module T : - sig - - end - - module ORev : - sig - type t = z - end - - module MRev : - sig - val max : z -> z -> z - end - - module MPRev : - sig - module T : - sig - - end - end - - module P : - sig - val max_case_strong : - z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> - 'a1 - - val max_case : - z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 - - val max_dec : z -> z -> bool - - val min_case_strong : - z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> - 'a1 - - val min_case : - z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 - - val min_dec : z -> z -> bool - end - - val max_case_strong : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 - - val max_case : z -> z -> 'a1 -> 'a1 -> 'a1 - - val max_dec : z -> z -> bool - - val min_case_strong : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 - - val min_case : z -> z -> 'a1 -> 'a1 -> 'a1 - - val min_dec : z -> z -> bool end val zeq_bool : z -> z -> bool @@ -872,44 +168,44 @@ val paddI : 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 + ('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 + '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 + '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 + '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 + '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 + '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 + '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 + '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 + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> bool) -> 'a1 pol -> 'a1 pol type 'c pExpr = | PEc of 'c @@ -923,16 +219,17 @@ type 'c pExpr = 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 + '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 + '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 + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol type 'a bFormula = | TT @@ -946,9 +243,9 @@ type 'a bFormula = val map_bformula : ('a1 -> 'a2) -> 'a1 bFormula -> 'a2 bFormula -type 'term' clause = 'term' list +type 'x clause = 'x list -type 'term' cnf = 'term' clause list +type 'x cnf = 'x clause list val tt : 'a1 cnf @@ -959,12 +256,12 @@ val add_term : clause option val or_clause : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 clause -> - 'a1 clause option + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 clause + -> 'a1 clause option val or_clause_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf -> 'a1 - cnf + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf -> + 'a1 cnf val or_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 cnf -> 'a1 cnf -> 'a1 @@ -973,18 +270,20 @@ val or_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 + ('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 + ('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 +val cltb : + ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool type 'c polC = 'c pol @@ -1015,28 +314,30 @@ 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 + '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 + '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 + '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 + '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 + '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 + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> + bool type op2 = | OpEq @@ -1048,43 +349,37 @@ type op2 = type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr } -val flhs : 'a1 formula -> 'a1 pExpr - -val fop : 'a1 formula -> op2 - -val frhs : 'a1 formula -> 'a1 pExpr - val norm : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> - 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol val psub0 : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 - -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> + ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol val padd0 : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> - 'a1 pol + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol + -> 'a1 pol val xnormalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> - 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula - list + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 + nFormula list val cnf_normalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> - 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula - cnf + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 + nFormula cnf val xnegate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> - 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula - list + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 + nFormula list val cnf_negate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> - 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula - cnf + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 + nFormula cnf val xdenorm : positive -> 'a1 pol -> 'a1 pExpr @@ -1095,8 +390,8 @@ 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 + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz + -> 'a1 psatz type q = { qnum : z; qden : positive } @@ -1122,12 +417,16 @@ val qpower_positive : q -> positive -> q val qpower : q -> z -> q -type 'a t0 = +type 'a t = | Empty | Leaf of 'a -| Node of 'a t0 * 'a * 'a t0 +| Node of 'a t * 'a * 'a t + +val find : 'a1 -> 'a1 t -> positive -> 'a1 -val find : 'a1 -> 'a1 t0 -> positive -> 'a1 +val singleton : 'a1 -> positive -> 'a1 -> 'a1 t + +val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t type zWitness = z psatz @@ -1221,4 +520,3 @@ 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 index cb4b2b8a5..c9009ea4d 100644 --- a/plugins/micromega/vo.itarget +++ b/plugins/micromega/vo.itarget @@ -12,4 +12,4 @@ ZCoeff.vo ZMicromega.vo Lia.vo Lqa.vo -Lra.vo
\ No newline at end of file +Lra.vo diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 2d1f725ef..49b51b171 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -299,10 +299,12 @@ module Make(T : Task) = struct Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc) let main_loop () = + (* We pass feedback to master *) let slave_feeder oc fb = Marshal.to_channel oc (RespFeedback fb) []; flush oc in - Feedback.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); + Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); Feedback.set_logger Feedback.feedback_logger; + (* We ask master to allocate universe identifiers *) Universes.set_remote_new_univ_level (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; match unmarshal_more_data (Option.get !slave_ic) with diff --git a/stm/lemmas.ml b/stm/lemmas.ml index cf4143dbb..6149e3a11 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -254,10 +254,14 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i, | Some body -> let body = norm body in let k = Kindops.logical_kind_of_goal_kind kind in - let body_i = match kind_of_term body with + let rec body_i t = match kind_of_term t with | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) | CoFix (0,decls) -> mkCoFix (i,decls) + | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) + | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) + | App (t, args) -> mkApp (body_i t, args) | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in + let body_i = body_i body in match locality with | Discharge -> let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p diff --git a/stm/stm.ml b/stm/stm.ml index 9f86597dc..cf9fa5492 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1437,8 +1437,8 @@ end = struct (* {{{ *) let check_task_aux extra name l i = let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in - msg_info( - str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name)); + Flags.if_verbose msg_info + (str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name)); VCS.restore document; let start = let rec aux cur = @@ -2089,13 +2089,13 @@ let known_state ?(redefine_qed=false) ~cache id = let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env () in - let rec pure_cherry_pick_non_pstate id = Future.purify (fun id -> + let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id -> prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); - reach id; + reach ~safe_id id; cherry_pick_non_pstate ()) id (* traverses the dag backward from nodes being already calculated *) - and reach ?(redefine_qed=false) ?(cache=cache) id = + and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id = prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); if not redefine_qed && State.is_cached ~cache id then begin Hooks.(call state_computed id ~in_cache:true); @@ -2240,13 +2240,13 @@ let known_state ?(redefine_qed=false) ~cache id = ), cache, true | `Sideff (`Id origin) -> (fun () -> reach view.next; - inject_non_pstate (pure_cherry_pick_non_pstate origin); + inject_non_pstate (pure_cherry_pick_non_pstate view.next origin); ), cache, true in let cache_step = if !Flags.async_proofs_cache = Some Flags.Force then `Yes else cache_step in - State.define + State.define ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in reach ~redefine_qed id @@ -2358,7 +2358,7 @@ let merge_proof_branch ?valid ?id qast keep brname = let id = VCS.new_node ?id () in VCS.merge id ~ours:(Qed (qed None)) brname; VCS.delete_branch brname; - if keep <> VtDrop then VCS.propagate_sideff None; + VCS.propagate_sideff None; `Ok | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } -> let ofp = @@ -2471,12 +2471,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty {x with verbose = true } with e when CErrors.noncritical e -> let e = CErrors.push e in - iraise (State.exn_on report_id e)); `Ok + iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok | VtQuery (false,(report_id,route)), VtNow -> (try vernac_interp report_id ~route x with e -> let e = CErrors.push e in - iraise (State.exn_on report_id e)); `Ok + iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok | VtQuery (true,(report_id,_)), w -> assert(Stateid.equal report_id Stateid.dummy); let id = VCS.new_node ~id:newtip () in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 2eca1e597..ba9a2d95c 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -29,9 +29,9 @@ open Proofview.Notations let eauto_unif_flags = auto_flags_of_state full_transparent_state let e_give_exact ?(flags=eauto_unif_flags) c = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let t1 = Tacmach.New.pf_unsafe_type_of gl c in - let t2 = Tacmach.New.pf_concl gl in + let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in if occur_existential t1 || occur_existential t2 then Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) else exact_check c diff --git a/test-suite/bugs/closed/5065.v b/test-suite/bugs/closed/5065.v new file mode 100644 index 000000000..6bd677ba6 --- /dev/null +++ b/test-suite/bugs/closed/5065.v @@ -0,0 +1,6 @@ +Inductive foo := C1 : bar -> foo with bar := C2 : foo -> bar. + +Lemma L1 : foo -> True with L2 : bar -> True. +intros; clear L1 L2; abstract (exact I). +intros; exact I. +Qed.
\ No newline at end of file diff --git a/test-suite/micromega/bertot.v b/test-suite/micromega/bertot.v index bcf222f92..29171aed9 100644 --- a/test-suite/micromega/bertot.v +++ b/test-suite/micromega/bertot.v @@ -11,6 +11,8 @@ Require Import Psatz. Open Scope Z_scope. + + Goal (forall x y n, ( ~ x < n /\ x <= n /\ 2 * y = x*(x+1) -> 2 * y = n*(n+1)) /\ diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index 89c08c770..12f72a580 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -11,6 +11,12 @@ Require Import Reals. Open Scope R_scope. + +Lemma cst_test : 5^5 = 5 * 5 * 5 *5 *5. +Proof. + lra. +Qed. + Lemma yplus_minus : forall x y, 0 = x + y -> 0 = x -y -> 0 = x /\ 0 = y. Proof. @@ -73,4 +79,5 @@ Qed. Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). intros; split_Rabs; lra. -Qed.
\ No newline at end of file +Qed. + diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v index 1f148becc..3f4c2407d 100644 --- a/test-suite/micromega/zomicron.v +++ b/test-suite/micromega/zomicron.v @@ -8,9 +8,10 @@ Proof. lia. Qed. + Lemma two_x_y_eq_1 : forall x y, 2 * x + 2 * y = 1 -> False. Proof. - intros. + intros. lia. Qed. @@ -20,6 +21,12 @@ Proof. lia. Qed. +Lemma unused : forall x y, y >= 0 /\ x = 1 -> x = 1. +Proof. + intros x y. + lia. +Qed. + Lemma omega_nightmare : forall x y, 27 <= 11 * x + 13 * y <= 45 -> -10 <= 7 * x - 9 * y <= 4 -> False. Proof. intros ; intuition auto. @@ -42,4 +49,37 @@ Proof. Unshelve. exact Z0. Qed. -
\ No newline at end of file + +Lemma unused_concl : forall x, + False -> x > 0 -> x < 0. +Proof. + intro. + lia. +Qed. + +Lemma unused_concl_match : forall (x:Z), + False -> match x with + | Z0 => True + | _ => x = x + end. +Proof. + intros. + lia. +Qed. + +Lemma fresh : forall (__arith : Prop), + __arith -> True. +Proof. + intros. + lia. +Qed. + +Class Foo {x : Z} := { T : Type ; dec : T -> Z }. +Goal forall bound {F : @Foo bound} (x y : T), 0 <= dec x < bound -> 0 <= dec y +< bound -> dec x + dec y >= bound -> dec x + dec y < 2 * bound. +Proof. + intros. + lia. +Qed. + + |