diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/correctness/pcic.ml | 2 | ||||
| -rw-r--r-- | contrib/correctness/ptactic.ml | 20 | ||||
| -rw-r--r-- | contrib/extraction/Extraction.v | 86 | ||||
| -rw-r--r-- | contrib/extraction/extract_env.ml | 119 | ||||
| -rw-r--r-- | contrib/extraction/extract_env.mli | 9 | ||||
| -rw-r--r-- | contrib/extraction/table.ml | 84 | ||||
| -rw-r--r-- | contrib/extraction/table.mli | 17 | ||||
| -rw-r--r-- | contrib/fourier/fourierR.ml | 6 | ||||
| -rw-r--r-- | contrib/omega/coq_omega.ml | 49 | ||||
| -rw-r--r-- | contrib/ring/quote.ml | 14 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 198 | ||||
| -rw-r--r-- | contrib/romega/refl_omega.ml | 5 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.mli | 4 |
13 files changed, 184 insertions, 429 deletions
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml index e6f6891f73..ffcb7c648e 100644 --- a/contrib/correctness/pcic.ml +++ b/contrib/correctness/pcic.ml @@ -52,7 +52,7 @@ let tuple_n n = (fun i -> let id = id_of_string ("proj_" ^ string_of_int n ^ "_" ^ string_of_int i) in - (false, (id, true, Ast.nvar (id_of_string ("T" ^ string_of_int i))))) + (false, Vernacexpr.AssumExpr (id, Ast.nvar (id_of_string ("T" ^ string_of_int i))))) l1n in let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index c7f1fc2ed7..d191b58ebf 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -220,6 +220,14 @@ let reduce_open_constr (em0,c) = let em = existential_map_of_constr c in (em,c) +let register id n = + let id' = match n with None -> id | Some id' -> id' in + Penv.register id id' + +let correctness_hook _ ref = + let pf_id = Nameops.basename (Nametab.sp_of_global (Global.env()) ref) in + register pf_id None + let correctness s p opttac = Pmisc.reset_names(); let p,oc,cty,v = coqast_of_prog p in @@ -228,14 +236,14 @@ let correctness s p opttac = let sigma = Evd.empty in let cty = Reduction.nf_betaiota cty in let id = id_of_string s in - start_proof id Declare.NeverDischarge sign cty; + start_proof id (false,Nametab.NeverDischarge) sign cty correctness_hook; Penv.new_edited id (v,p); if !debug then show_open_subgoals(); deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ()); let oc = reduce_open_constr oc in deb_mess (str"AFTER REDUCTION:" ++ fnl ()); deb_mess (Printer.prterm_env (Global.env()) (snd oc)); - let tac = (tclTHEN (Refine.refine_tac oc) automatic) in + let tac = (tclTHEN (Extratactics.refine_tac oc) automatic) in let tac = match opttac with | None -> tac | Some t -> tclTHEN tac t @@ -245,15 +253,11 @@ let correctness s p opttac = (* On redéfinit la commande "Save" pour enregistrer les nouveaux programmes *) - +(* open Vernacinterp let add = Vernacinterp.overwriting_vinterp_add -let register id n = - let id' = match n with None -> id | Some id' -> id' in - Penv.register id id' - let _ = let current_save = Vernacinterp.vinterp_map "SaveNamed" in add "SaveNamed" @@ -282,4 +286,4 @@ let _ = let pf_id = Pfedit.get_current_proof_name () in current_saveanonymous l (); register pf_id (Some id))) - +*) diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v deleted file mode 100644 index 0f69bce4a4..0000000000 --- a/contrib/extraction/Extraction.v +++ /dev/null @@ -1,86 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -Grammar vernac vernac : ast := - -(* Extraction in the Coq toplevel *) - extr_constr [ "Extraction" constrarg($c) "." ] -> - [ (Extraction $c) ] -| extr_list [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] -> - [ (ExtractionRec ($LIST $l)) ] - -(* Monolithic extraction to a file *) -| extr_file - [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] - -> [ (ExtractionFile $f ($LIST $l)) ] - -(* Modular extraction (one Coq module = one ML module) *) -| extr_module - [ "Extraction" "Module" identarg($m) "." ] - -> [ (ExtractionModule $m) ] -| rec_extr_module - [ "Recursive" "Extraction" "Module" identarg($m) "." ] - -> [ (RecursiveExtractionModule $m) ] - -(* Target Language *) - -| extr_language - [ "Extraction" "Language" extraction_language($l) "." ] - -> [ (ExtractionLang $l) ] - -(* Custom inlining directives *) -| inline_constant - [ "Extraction" "Inline" ne_qualidarg_list($l) "." ] - -> [ (ExtractionInline ($LIST $l)) ] - -| no_inline_constant - [ "Extraction" "NoInline" ne_qualidarg_list($l) "." ] - -> [ (ExtractionNoInline ($LIST $l)) ] - -| print_inline_constant - [ "Print" "Extraction" "Inline" "."] - -> [ (PrintExtractionInline) ] - -| reset_inline_constant - [ "Reset" "Extraction" "Inline" "."] - -> [ (ResetExtractionInline) ] - -(* Overriding of a Coq object by an ML one *) -| extract_constant - [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ] - -> [ (ExtractConstant $x $y) ] - -| extract_inlined_constant - [ "Extract" "Inlined" "Constant" qualidarg($x) - "=>" idorstring($y) "." ] - -> [ (ExtractInlinedConstant $x $y) ] - -| extract_inductive - [ "Extract" "Inductive" qualidarg($x) "=>" mindnames($y) "."] - -> [ (ExtractInductive $x $y) ] - -(* Utility entries *) -with mindnames : ast := - mlconstr [ idorstring($id) "[" idorstring_list($idl) "]" ] - -> [(VERNACARGLIST $id ($LIST $idl))] - -with idorstring_list: ast list := - ids_nil [ ] -> [ ] -| ids_cons [ idorstring($x) idorstring_list($l) ] -> [ $x ($LIST $l) ] - -with idorstring : ast := - ids_ident [ identarg($id) ] -> [ $id ] -| ids_string [ stringarg($s) ] -> [ $s ] - -with extraction_language : ast := - ocaml [ "Ocaml" ] -> [ "Ocaml" ] -| haskell [ "Haskell" ] -> [ "Haskell" ] -| toplevel [ "Toplevel" ] -> [ "Toplevel" ] - -. - diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index ecfd5e2ea8..db2e7d4f93 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -241,40 +241,33 @@ let extract_reference r = else List.find (decl_in_r r) decls in msgnl (pp_decl d) -let _ = - vinterp_add "Extraction" - (function - | [VARG_CONSTR ast] -> - (fun () -> - set_globals (); - let c = Astterm.interp_constr Evd.empty (Global.env()) ast in - match kind_of_term c with - (* If it is a global reference, then output the declaration *) - | Const sp -> extract_reference (ConstRef sp) - | Ind ind -> extract_reference (IndRef ind) - | Construct cs -> extract_reference (ConstructRef cs) - (* Otherwise, output the ML type or expression *) - | _ -> - match extract_constr (Global.env()) c with - | Emltype (t,_,_) -> msgnl (pp_type t ++ fnl ()) - | Emlterm a -> msgnl (pp_ast (normalize a) ++ fnl ())) - | _ -> assert false) +let extraction rawconstr = + set_globals (); + let c = Astterm.interp_constr Evd.empty (Global.env()) rawconstr in + match kind_of_term c with + (* If it is a global reference, then output the declaration *) + | Const sp -> extract_reference (ConstRef sp) + | Ind ind -> extract_reference (IndRef ind) + | Construct cs -> extract_reference (ConstructRef cs) + (* Otherwise, output the ML type or expression *) + | _ -> + match extract_constr (Global.env()) c with + | Emltype (t,_,_) -> msgnl (pp_type t ++ fnl ()) + | Emlterm a -> msgnl (pp_ast (normalize a) ++ fnl ()) (*s Recursive extraction in the Coq toplevel. The vernacular command is \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env] to get the saturated environment to extract. *) let mono_extraction (f,m) vl = - let refs = refs_of_vargl vl in + let refs = List.map Nametab.global vl in let prm = {modular=false; mod_name = m; to_appear= refs} in let decls = decl_of_refs refs in let decls = add_ml_decls prm decls in let decls = optimize prm decls in extract_to_file f prm decls -let _ = - vinterp_add "ExtractionRec" - (fun vl () -> mono_extraction (None,id_of_string "Main") vl) +let extraction_rec = mono_extraction (None,id_of_string "Main") (*s Extraction to a file (necessarily recursive). The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn]. @@ -297,14 +290,9 @@ let lang_error () = ++ fnl () ++ str "You should use Extraction Language Ocaml or Haskell before.") -let _ = - vinterp_add "ExtractionFile" - (function - | VARG_STRING f :: vl -> - (fun () -> - if lang () = Toplevel then lang_error () - else mono_extraction (filename f) vl) - | _ -> assert false) +let extraction_file f vl = + if lang () = Toplevel then lang_error () + else mono_extraction (filename f) vl (*s Extraction of a module. The vernacular command is \verb!Extraction Module! [M]. *) @@ -322,48 +310,37 @@ let module_file_name m = match lang () with | Haskell -> (String.capitalize (string_of_id m)) ^ ".hs" | Toplevel -> assert false -let _ = - vinterp_add "ExtractionModule" - (function - | [VARG_IDENTIFIER m] -> - (fun () -> - if lang () = Toplevel then lang_error () - else - let dir_m = module_of_id m in - let f = module_file_name m in - let prm = {modular=true; mod_name=m; to_appear=[]} in - let rl = extract_module dir_m in - let decls = optimize prm (decl_of_refs rl) in - let decls = add_ml_decls prm decls in - check_one_module dir_m decls; - let decls = List.filter (decl_in_m dir_m) decls in - extract_to_file (Some f) prm decls) - | _ -> assert false) +let extraction_module m = + if lang () = Toplevel then lang_error () + else + let dir_m = module_of_id m in + let f = module_file_name m in + let prm = {modular=true; mod_name=m; to_appear=[]} in + let rl = extract_module dir_m in + let decls = optimize prm (decl_of_refs rl) in + let decls = add_ml_decls prm decls in + check_one_module dir_m decls; + let decls = List.filter (decl_in_m dir_m) decls in + extract_to_file (Some f) prm decls (*s Recursive Extraction of all the modules [M] depends on. The vernacular command is \verb!Recursive Extraction Module! [M]. *) -let _ = - vinterp_add "RecursiveExtractionModule" - (function - | [VARG_IDENTIFIER m] -> - (fun () -> - if lang () = Toplevel then lang_error () - else - let dir_m = module_of_id m in - let modules,refs = - modules_extract_env dir_m in - check_modules modules; - let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in - let decls = optimize dummy_prm (decl_of_refs refs) in - let decls = add_ml_decls dummy_prm decls in - Dirset.iter - (fun m -> - let short_m = snd (split_dirpath m) in - let f = module_file_name short_m in - let prm = {modular=true;mod_name=short_m;to_appear=[]} in - let decls = List.filter (decl_in_m m) decls in - if decls <> [] then extract_to_file (Some f) prm decls) - modules) - | _ -> assert false) - +let recursive_extraction_module m = + if lang () = Toplevel then lang_error () + else + let dir_m = module_of_id m in + let modules,refs = + modules_extract_env dir_m in + check_modules modules; + let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in + let decls = optimize dummy_prm (decl_of_refs refs) in + let decls = add_ml_decls dummy_prm decls in + Dirset.iter + (fun m -> + let short_m = snd (split_dirpath m) in + let f = module_file_name short_m in + let prm = {modular=true;mod_name=short_m;to_appear=[]} in + let decls = List.filter (decl_in_m m) decls in + if decls <> [] then extract_to_file (Some f) prm decls) + modules diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli index 710e801d12..1cdb5c02c3 100644 --- a/contrib/extraction/extract_env.mli +++ b/contrib/extraction/extract_env.mli @@ -10,3 +10,12 @@ (*s This module declares the extraction commands. *) +open Util +open Names +open Nametab + +val extraction : Genarg.constr_ast -> unit +val extraction_rec : qualid located list -> unit +val extraction_file : string -> qualid located list -> unit +val extraction_module : identifier -> unit +val recursive_extraction_module : identifier -> unit diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 896203486b..ee7267f3f6 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -13,6 +13,7 @@ open Lib open Libobject open Goptions open Vernacinterp +open Extend open Names open Util open Pp @@ -66,21 +67,25 @@ let check_constant r = else errorlabstrm "extract_constant" (Printer.pr_global r ++ spc () ++ str "is not a constant.") +(* let string_of_varg = function | VARG_IDENTIFIER id -> string_of_id id | VARG_STRING s -> s | _ -> assert false +*) let no_such_reference q = errorlabstrm "reference_of_varg" (str "There is no such reference " ++ Nametab.pr_qualid q ++ str ".") +(* let reference_of_varg = function | VARG_QUALID q -> (try Nametab.locate q with Not_found -> no_such_reference q) | _ -> assert false let refs_of_vargl = List.map reference_of_varg +*) (*s Target Language *) @@ -103,18 +108,7 @@ let _ = declare_summary "Extraction Lang" init_function = (fun () -> lang_ref := Ocaml); survive_section = true } -let lang_to_lang = function - "Ocaml" -> Ocaml - | "Haskell" -> Haskell - | "Toplevel" -> Toplevel - | _ -> assert false - -let _ = - vinterp_add "ExtractionLang" - (function - [VARG_STRING l] -> - (fun () -> add_anonymous_leaf (extr_lang (lang_to_lang l))) - | _ -> assert false) +let extraction_language x = add_anonymous_leaf (extr_lang x) (*s Table for custom inlining *) @@ -150,21 +144,13 @@ let _ = declare_summary "Extraction Inline" (*s Grammar entries. *) -let _ = - vinterp_add "ExtractionInline" - (fun vl () -> - let refs = List.map check_constant (refs_of_vargl vl) in - add_anonymous_leaf (inline_extraction (true,refs))) - -let _ = - vinterp_add "ExtractionNoInline" - (fun vl () -> - let refs = List.map check_constant (refs_of_vargl vl) in - add_anonymous_leaf (inline_extraction (false,refs))) +let extraction_inline b vl = + let refs = List.map (fun x -> check_constant (Nametab.global x)) vl in + add_anonymous_leaf (inline_extraction (true,refs)) (*s Printing part *) -let print_inline () = +let print_extraction_inline () = let (i,n)= !inline_table in let i'= Refset.filter is_constant i in msg @@ -177,9 +163,6 @@ let print_inline () = (fun r p -> (p ++ str " " ++ Printer.pr_global r ++ fnl ())) n (mt ())) -let _ = vinterp_add "PrintExtractionInline" (fun _ -> print_inline) - - (*s Reset part *) let (reset_inline,_) = @@ -189,10 +172,8 @@ let (reset_inline,_) = load_function = (fun (_,_)-> inline_table := empty_inline_table); open_function = (fun _ -> ()); export_function = (fun x -> Some x) }) - -let _ = vinterp_add "ResetExtractionInline" - (fun _ () -> add_anonymous_leaf (reset_inline ())) - + +let reset_extraction_inline () = add_anonymous_leaf (reset_inline ()) (*s Table for direct ML extractions. *) @@ -235,30 +216,13 @@ let _ = declare_summary "ML extractions" (*s Grammar entries. *) -let _ = - vinterp_add "ExtractConstant" - (function - | [id; vs] -> - (fun () -> - let r = check_constant (reference_of_varg id) in - let s = string_of_varg vs in - add_anonymous_leaf (inline_extraction (false,[r])); - add_anonymous_leaf (in_ml_extraction (r,s))) - | _ -> assert false) - -let _ = - vinterp_add "ExtractInlinedConstant" - (function - | [id; vs] -> - (fun () -> - let r = check_constant (reference_of_varg id) in - let s = string_of_varg vs in - add_anonymous_leaf (inline_extraction (true,[r])); - add_anonymous_leaf (in_ml_extraction (r,s))) - | _ -> assert false) - - -let extract_inductive r (id2,l2) = match r with +let extract_constant_inline inline qid s = + let r = check_constant (Nametab.global qid) in + add_anonymous_leaf (inline_extraction (inline,[r])); + add_anonymous_leaf (in_ml_extraction (r,s)) + +let extract_inductive r (id2,l2) = + let r = Nametab.global r in match r with | IndRef ((sp,i) as ip) -> let mib = Global.lookup_mind sp in let n = Array.length mib.mind_packets.(i).mind_consnames in @@ -273,13 +237,3 @@ let extract_inductive r (id2,l2) = match r with | _ -> errorlabstrm "extract_inductive" (Printer.pr_global r ++ spc () ++ str "is not an inductive type.") - -let _ = - vinterp_add "ExtractInductive" - (function - | [q1; VARG_VARGLIST (id2 :: l2)] -> - (fun () -> - extract_inductive (reference_of_varg q1) - (string_of_varg id2, List.map string_of_varg l2)) - | _ -> assert false) - diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index a6cde3c5f2..9fa7142ce8 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -28,7 +28,7 @@ module Refset : Set.S with type elt = global_reference val check_constant : global_reference -> global_reference -val refs_of_vargl : vernac_arg list -> global_reference list +(*val refs_of_vargl : Extend.vernac_arg list -> global_reference list*) (*s Target language. *) @@ -52,3 +52,18 @@ val ml_extractions : unit -> Refset.t val sorted_ml_extractions : unit -> (global_reference * string) list +(*s Extraction commands. *) + +open Util + +val extraction_language : lang -> unit + +val extraction_inline : bool -> qualid located list -> unit + +val print_extraction_inline : unit -> unit + +val reset_extraction_inline : unit -> unit + +val extract_constant_inline : bool -> qualid located -> string -> unit + +val extract_inductive : qualid located -> string * string list -> unit diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index 74a58b11d4..c877dc47bb 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -18,8 +18,10 @@ open Term open Tactics open Clenv open Names +open Tacticals open Tacmach open Fourier +open Contradiction (****************************************************************************** Opérations sur les combinaisons linéaires affines. @@ -68,6 +70,7 @@ let flin_emult a f = ;; (*****************************************************************************) +open Vernacexpr let parse_ast = Pcoq.parse_string Pcoq.Constr.constr;; let parse s = Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);; let pf_parse_constr gl s = @@ -550,10 +553,11 @@ let rec fourier gl= ;; +(* let fourier_tac x gl = fourier gl ;; let v_fourier = add_tactic "Fourier" fourier_tac - +*) diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 6df04bd37d..a8b9651148 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -28,6 +28,7 @@ open Declarations open Environ open Sign open Inductive +open Tacticals open Tacmach open Evar_refiner open Tactics @@ -35,6 +36,7 @@ open Clenv open Logic open Nametab open Omega +open Contradiction (* Added by JCF, 09/03/98 *) @@ -48,6 +50,46 @@ let display_system_flag = ref false let display_action_flag = ref false let old_style_flag = ref false +let read f () = !f +let write f x = f:=x + +open Goptions + +(* Obsolete, subsumed by Time Omega +let _ = + declare_bool_option + { optsync = false; + optname = "Omega time displaying flag"; + optkey = SecondaryTable ("Omega","Time"); + optread = read display_time_flag; + optwrite = write display_time_flag } +*) + +let _ = + declare_bool_option + { optsync = false; + optname = "Omega system time displaying flag"; + optkey = SecondaryTable ("Omega","System"); + optread = read display_system_flag; + optwrite = write display_system_flag } + +let _ = + declare_bool_option + { optsync = false; + optname = "Omega action display flag"; + optkey = SecondaryTable ("Omega","Action"); + optread = read display_action_flag; + optwrite = write display_action_flag } + +let _ = + declare_bool_option + { optsync = false; + optname = "Omega old style flag"; + optkey = SecondaryTable ("Omega","OldStyle"); + optread = read old_style_flag; + optwrite = write old_style_flag } + + let all_time = timing "Omega " let solver_time = timing "Solver " let exact_time = timing "Rewrites " @@ -70,7 +112,8 @@ let new_identifier_var = let rec mk_then = function [t] -> t | (t::l) -> (tclTHEN (t) (mk_then l)) | [] -> tclIDTAC -let exists_tac c = constructor_tac (Some 1) 1 [Com,c] +let exists_tac c = constructor_tac (Some 1) 1 (Rawterm.ImplicitBindings [c]) + let generalize_tac t = generalize_time (generalize t) let elim t = elim_time (simplest_elim t) let exact t = exact_time (Tactics.refine t) @@ -1822,7 +1865,3 @@ let omega_solver gl = (* if !display_time_flag then begin text_time (); flush Pervasives.stdout end; *) result - -let omega = hide_atomic_tactic "Omega" omega_solver - - diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 669fd21c50..bcd8ee5f94 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -112,7 +112,7 @@ open Pattern open Tacmach open Tactics open Proof_trees -open Proof_type +open Tacexpr (*i*) (*s First, we need to access some Coq constants @@ -452,18 +452,6 @@ let quote f lid gl = | None -> Tactics.convert_concl (mkApp (f, [| p |])) gl | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) gl -(*i*) -let dyn_quote = function - | [Identifier f] -> quote f [] - | Identifier f :: lid -> quote f - (List.map (function - | Identifier id -> id - | other -> bad_tactic_args "Quote" [other]) lid) - | l -> bad_tactic_args "Quote" l - -let h_quote = hide_tactic "Quote" dyn_quote -(*i*) - (*i Just testing ... diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index e6635c441b..25c3f74917 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -17,12 +17,14 @@ open Term open Names open Nameops open Reductionops +open Tacticals +open Tacexpr open Tacmach -open Proof_type open Proof_trees open Printer open Equality open Vernacinterp +open Vernacexpr open Libobject open Closure open Tacred @@ -227,34 +229,34 @@ let unbox = function (* Add a Ring or a Semi-Ring to the database after a type verification *) +let implement_theory env t th args = + is_conv env Evd.empty (Typing.type_of env Evd.empty t) (mkLApp (th, args)) + let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus amult aone azero aopp aeq t cset = if theories_map_mem a then errorlabstrm "Add Semi Ring" (str "A (Semi-)(Setoid-)Ring Structure is already declared for " ++ prterm a); let env = Global.env () in if (want_ring & want_setoid & - (not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) - (mkLApp (coq_Setoid_Ring_Theory, - [| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|])))) & - (not (is_conv env Evd.empty (Typing.type_of env Evd.empty (unbox asetth)) - (mkLApp (coq_Setoid_Theory, [| a; (unbox aequiv) |]))))) then + not (implement_theory env t coq_Setoid_Ring_Theory + [| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|]) + & + not (implement_theory env (unbox asetth) coq_Setoid_Theory + [| a; (unbox aequiv) |])) then errorlabstrm "addring" (str "Not a valid Setoid-Ring theory"); if (not want_ring & want_setoid & - (not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) - (mkLApp (coq_Semi_Setoid_Ring_Theory, - [| a; (unbox aequiv); aplus; amult; aone; azero; aeq|])))) & - (not (is_conv env Evd.empty (Typing.type_of env Evd.empty (unbox asetth)) - (mkLApp (coq_Setoid_Theory, [| a; (unbox aequiv) |]))))) then + not (implement_theory env t coq_Semi_Setoid_Ring_Theory + [| a; (unbox aequiv); aplus; amult; aone; azero; aeq|]) & + not (implement_theory env (unbox asetth) coq_Setoid_Theory + [| a; (unbox aequiv) |])) then errorlabstrm "addring" (str "Not a valid Semi-Setoid-Ring theory"); if (want_ring & not want_setoid & - not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) - (mkLApp (coq_Ring_Theory, - [| a; aplus; amult; aone; azero; (unbox aopp); aeq |])))) then + not (implement_theory env t coq_Ring_Theory + [| a; aplus; amult; aone; azero; (unbox aopp); aeq |])) then errorlabstrm "addring" (str "Not a valid Ring theory"); if (not want_ring & not want_setoid & - not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) - (mkLApp (coq_Semi_Ring_Theory, - [| a; aplus; amult; aone; azero; aeq |])))) then + not (implement_theory env t coq_Semi_Ring_Theory + [| a; aplus; amult; aone; azero; aeq |])) then errorlabstrm "addring" (str "Not a valid Semi-Ring theory"); Lib.add_anonymous_leaf (theory_to_obj @@ -274,151 +276,6 @@ let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus th_t = t; th_closed = cset })) -(* The vernac commands "Add Ring" and "Add Semi Ring" *) -(* see file Ring.v for examples of this command *) - -let constr_of_comarg = function - | VARG_CONSTR c -> constr_of c - | _ -> anomaly "Add (Semi) (Setoid) Ring" - -let cset_of_comarg_list l = - List.fold_right ConstrSet.add (List.map constr_of_comarg l) ConstrSet.empty - -let _ = - vinterp_add "AddSemiRing" - (function - | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult) - ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aeq) - ::(VARG_CONSTR t)::l -> - (fun () -> (add_theory false false false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - None - (constr_of aeq) - (constr_of t) - (cset_of_comarg_list l))) - | _ -> anomaly "AddSemiRing") - -let _ = - vinterp_add "AddRing" - (function - | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult) - ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp) - ::(VARG_CONSTR aeq)::(VARG_CONSTR t)::l -> - (fun () -> (add_theory true false false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - (Some (constr_of aopp)) - (constr_of aeq) - (constr_of t) - (cset_of_comarg_list l))) - | _ -> anomaly "AddRing") - -let _ = - vinterp_add "AddSetoidRing" - (function - | (VARG_CONSTR a)::(VARG_CONSTR aequiv)::(VARG_CONSTR asetth)::(VARG_CONSTR aplus) - ::(VARG_CONSTR amult)::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp) - ::(VARG_CONSTR aeq)::(VARG_CONSTR pm)::(VARG_CONSTR mm)::(VARG_CONSTR om) - ::(VARG_CONSTR t)::l -> - (fun () -> (add_theory true false true - (constr_of a) - (Some (constr_of aequiv)) - (Some (constr_of asetth)) - (Some { - plusm = (constr_of pm); - multm = (constr_of mm); - oppm = Some (constr_of om)}) - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - (Some (constr_of aopp)) - (constr_of aeq) - (constr_of t) - (cset_of_comarg_list l))) - | _ -> anomaly "AddSetoidRing") - -let _ = - vinterp_add "AddSemiSetoidRing" - (function - | (VARG_CONSTR a)::(VARG_CONSTR aequiv)::(VARG_CONSTR asetth)::(VARG_CONSTR aplus) - ::(VARG_CONSTR amult)::(VARG_CONSTR aone)::(VARG_CONSTR azero) - ::(VARG_CONSTR aeq)::(VARG_CONSTR pm)::(VARG_CONSTR mm) - ::(VARG_CONSTR t)::l -> - (fun () -> (add_theory false false true - (constr_of a) - (Some (constr_of aequiv)) - (Some (constr_of asetth)) - (Some { - plusm = (constr_of pm); - multm = (constr_of mm); - oppm = None}) - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - None - (constr_of aeq) - (constr_of t) - (cset_of_comarg_list l))) - | _ -> anomaly "AddSemiSetoidRing") - -let _ = - vinterp_add "AddAbstractSemiRing" - (function - | [VARG_CONSTR a; VARG_CONSTR aplus; - VARG_CONSTR amult; VARG_CONSTR aone; - VARG_CONSTR azero; VARG_CONSTR aeq; VARG_CONSTR t] -> - (fun () -> (add_theory false true false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - None - (constr_of aeq) - (constr_of t) - ConstrSet.empty)) - | _ -> anomaly "AddAbstractSemiRing") - -let _ = - vinterp_add "AddAbstractRing" - (function - | [ VARG_CONSTR a; VARG_CONSTR aplus; - VARG_CONSTR amult; VARG_CONSTR aone; - VARG_CONSTR azero; VARG_CONSTR aopp; - VARG_CONSTR aeq; VARG_CONSTR t ] -> - (fun () -> (add_theory true true false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - (Some (constr_of aopp)) - (constr_of aeq) - (constr_of t) - ConstrSet.empty)) - | _ -> anomaly "AddAbstractRing") - (******** The tactic itself *********) (* @@ -894,14 +751,13 @@ let guess_eq_tac th = (tclTHEN (* Normalized sums associate on the right *) (tclREPEAT - (tclTHENST + (tclTHENFIRST (apply (mkApp(build_coq_f_equal2 (), [| th.th_a; th.th_a; th.th_a; th.th_plus |]))) - [reflexivity] - tclIDTAC)) + reflexivity)) (tclTRY - (tclTHENL + (tclTHENLAST (apply (mkApp(build_coq_f_equal2 (), [| th.th_a; th.th_a; th.th_a; th.th_plus |]))) @@ -964,13 +820,3 @@ let polynom lc gl = errorlabstrm "Ring :" (str" All terms must have the same type"); (tclTHEN (raw_polynom th None lc) polynom_unfold_tac) gl - -let dyn_polynom ltacargs gl = - polynom (List.map - (function - | Command c -> pf_interp_constr gl c - | Constr c -> c - | _ -> anomaly "dyn_polynom") - ltacargs) gl - -let v_polynom = add_tactic "Ring" dyn_polynom diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml index 9ff41f0b52..788d3338cf 100644 --- a/contrib/romega/refl_omega.ml +++ b/contrib/romega/refl_omega.ml @@ -596,7 +596,9 @@ let coq_omega gl = with Omega.NO_CONTRADICTION -> Util.error "Omega can't solve this system" end +(* let refl_omega = Tacmach.hide_atomic_tactic "StepOmega" coq_omega +*) (* \section{Encapsulation ROMEGA} *) @@ -614,6 +616,7 @@ open Term open Environ open Sign open Inductive +open Tacticals open Tacmach open Tactics open Tacticals @@ -832,5 +835,7 @@ let omega_solver gl = in (loop concl) gl +(* let omega = hide_atomic_tactic "ReflOmega" omega_solver +*) diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli index 6d8250ef76..07335ea6a5 100644 --- a/contrib/xml/xmlcommand.mli +++ b/contrib/xml/xmlcommand.mli @@ -28,7 +28,7 @@ (* Note: it is printed only (and directly) the most cooked available *) (* form of the definition (all the parameters are *) (* lambda-abstracted, but the object can still refer to variables) *) -val print : Nametab.qualid -> string option -> unit +val print : Nametab.qualid Util.located -> string option -> unit (* show dest *) (* where dest is either None (for stdout) or (Some filename) *) @@ -46,7 +46,7 @@ val printAll : unit -> unit (* and terms of the module d *) (* Note: the terms are printed in their uncooked form plus the informations *) (* on the parameters of their most cooked form *) -val printModule : Nametab.qualid -> string option -> unit +val printModule : Nametab.qualid Util.located -> string option -> unit (* printSection identifier directory_name *) (* where identifier is the name of a closed section d *) |