diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_expr.mli | 32 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 12 | ||||
| -rw-r--r-- | plugins/decl_mode/ppdecl_proof.ml | 169 | ||||
| -rw-r--r-- | plugins/decl_mode/ppdecl_proof.mli | 14 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/g_newring.ml4 | 90 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml (renamed from plugins/setoid_ring/newring.ml4) | 138 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.mli | 78 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring_ast.mli | 63 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring_plugin.mllib | 1 |
10 files changed, 366 insertions, 233 deletions
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 7467604a60..3c4cacbc54 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -46,23 +46,23 @@ type ('constr,'tac) casee = Real of 'constr | Virtual of ('constr statement,'constr,'tac) cut -type ('hyp,'constr,'pat,'tac) bare_proof_instr = - | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr - | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr - | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr +type ('var,'constr,'pat,'tac) bare_proof_instr = + | Pthen of ('var,'constr,'pat,'tac) bare_proof_instr + | Pthus of ('var,'constr,'pat,'tac) bare_proof_instr + | Phence of ('var,'constr,'pat,'tac) bare_proof_instr | Pcut of ('constr or_thesis statement,'constr,'tac) cut | Prew of side * ('constr statement,'constr,'tac) cut - | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut - | Passume of ('hyp,'constr) hyp list - | Plet of ('hyp,'constr) hyp list - | Pgiven of ('hyp,'constr) hyp list - | Pconsider of 'constr*('hyp,'constr) hyp list + | Psuffices of ((('var,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut + | Passume of ('var,'constr) hyp list + | Plet of ('var,'constr) hyp list + | Pgiven of ('var,'constr) hyp list + | Pconsider of 'constr*('var,'constr) hyp list | Pclaim of 'constr statement | Pfocus of 'constr statement - | Pdefine of Id.t * 'hyp list * 'constr + | Pdefine of Id.t * 'var list * 'constr | Pcast of Id.t or_thesis * 'constr - | Psuppose of ('hyp,'constr) hyp list - | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list) + | Psuppose of ('var,'constr) hyp list + | Pcase of 'var list*'pat*(('var,'constr or_thesis) hyp list) | Ptake of 'constr list | Pper of elim_type * ('constr,'tac) casee | Pend of block_type @@ -70,19 +70,19 @@ type ('hyp,'constr,'pat,'tac) bare_proof_instr = type emphasis = int -type ('hyp,'constr,'pat,'tac) gen_proof_instr= +type ('var,'constr,'pat,'tac) gen_proof_instr= {emph: emphasis; - instr: ('hyp,'constr,'pat,'tac) bare_proof_instr } + instr: ('var,'constr,'pat,'tac) bare_proof_instr } type raw_proof_instr = - ((Id.t*(Constrexpr.constr_expr option)) Loc.located, + ((Id.t * (Constrexpr.constr_expr option)) Loc.located, Constrexpr.constr_expr, Constrexpr.cases_pattern_expr, raw_tactic_expr) gen_proof_instr type glob_proof_instr = - ((Id.t*(Tacexpr.glob_constr_and_expr option)) Loc.located, + ((Id.t * (Tacexpr.glob_constr_and_expr option)) Loc.located, Tacexpr.glob_constr_and_expr, Constrexpr.cases_pattern_expr, Tacexpr.glob_tactic_expr) gen_proof_instr diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 03929b3b86..ef9d3159d2 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -19,6 +19,7 @@ open Tok (* necessary for camlp4 *) open Pcoq.Constr open Pcoq.Tactic +open Ppdecl_proof let pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in @@ -43,15 +44,6 @@ let pr_open_subgoals () = pr_subgoals close_cmd sigma goals *) -let pr_raw_proof_instr _ _ _ instr = - Errors.anomaly (Pp.str "Cannot print a proof_instr") - (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller - dans cette direction - Ppdecl_proof.pr_proof_instr (Global.env()) instr - *) -let pr_proof_instr _ _ _ instr = Empty.abort instr -let pr_glob_proof_instr _ _ _ instr = Empty.abort instr - let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= Decl_interp.interp_proof_instr (Decl_mode.get_info sigma gl) @@ -92,7 +84,7 @@ let vernac_proof_instr instr = (* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *) (* Only declared at raw level, because only used in vernac commands. *) -let wit_proof_instr : (raw_proof_instr, Empty.t, Empty.t) Genarg.genarg_type = +let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type = Genarg.make0 None "proof_instr" (* We create a new parser entry [proof_mode]. The Declarative proof mode diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 27308666d2..b3198dbf24 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -12,41 +12,35 @@ open Decl_expr open Names open Nameops -let pr_constr = Printer.pr_constr_env -let pr_tac = Pptactic.pr_glob_tactic -let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr - let pr_label = function Anonymous -> mt () | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () -let pr_constr env c = pr_constr env Evd.empty c - -let pr_justification_items env = function +let pr_justification_items pr_constr = function Some [] -> mt () | Some (_::_ as l) -> spc () ++ str "by" ++ spc () ++ - prlist_with_sep (fun () -> str ",") (pr_constr env) l + prlist_with_sep (fun () -> str ",") pr_constr l | None -> spc () ++ str "by *" -let pr_justification_method env = function +let pr_justification_method pr_tac = function None -> mt () | Some tac -> - spc () ++ str "using" ++ spc () ++ pr_tac env tac + spc () ++ str "using" ++ spc () ++ pr_tac tac -let pr_statement pr_it env st = - pr_label st.st_label ++ pr_it env st.st_it +let pr_statement pr_constr st = + pr_label st.st_label ++ pr_constr st.st_it -let pr_or_thesis pr_this env = function +let pr_or_thesis pr_this = function Thesis Plain -> str "thesis" | Thesis (For id) -> str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id - | This c -> pr_this env c + | This c -> pr_this c -let pr_cut pr_it env c = - hov 1 (pr_it env c.cut_stat) ++ - pr_justification_items env c.cut_by ++ - pr_justification_method env c.cut_using +let pr_cut pr_constr pr_tac pr_it c = + hov 1 (pr_it c.cut_stat) ++ + pr_justification_items pr_constr c.cut_by ++ + pr_justification_method pr_tac c.cut_using let type_or_thesis = function Thesis _ -> Term.mkProp @@ -54,128 +48,127 @@ let type_or_thesis = function let _I x = x -let rec print_hyps pconstr gtyp env sep _be _have hyps = +let rec pr_hyps pr_var pr_constr gtyp sep _be _have hyps = let pr_sep = if sep then str "and" ++ spc () else mt () in match hyps with (Hvar _ ::_) as rest -> spc () ++ pr_sep ++ str _have ++ - print_vars pconstr gtyp env false _be _have rest + pr_vars pr_var pr_constr gtyp false _be _have rest | Hprop st :: rest -> begin - let nenv = - match st.st_label with - Anonymous -> env - | Name id -> Environ.push_named (id,None,gtyp st.st_it) env in - spc() ++ pr_sep ++ pr_statement pconstr env st ++ - print_hyps pconstr gtyp nenv true _be _have rest + (* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*) + spc() ++ pr_sep ++ pr_statement pr_constr st ++ + pr_hyps pr_var pr_constr gtyp true _be _have rest end | [] -> mt () -and print_vars pconstr gtyp env sep _be _have vars = +and pr_vars pr_var pr_constr gtyp sep _be _have vars = match vars with Hvar st :: rest -> begin - let nenv = - match st.st_label with - Anonymous -> anomaly (Pp.str "anonymous variable") - | Name id -> Environ.push_named (id,None,st.st_it) env in + (* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*) let pr_sep = if sep then pr_comma () else mt () in spc() ++ pr_sep ++ - pr_statement pr_constr env st ++ - print_vars pconstr gtyp nenv true _be _have rest + pr_var st ++ + pr_vars pr_var pr_constr gtyp true _be _have rest end | (Hprop _ :: _) as rest -> let _st = if _be then str "be such that" else str "such that" in - spc() ++ _st ++ print_hyps pconstr gtyp env false _be _have rest + spc() ++ _st ++ pr_hyps pr_var pr_constr gtyp false _be _have rest | [] -> mt () -let pr_suffices_clause env (hyps,c) = - print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++ - str "to show" ++ spc () ++ pr_or_thesis pr_constr env c +let pr_suffices_clause pr_var pr_constr (hyps,c) = + pr_hyps pr_var pr_constr _I false false "to have" hyps ++ spc () ++ + str "to show" ++ spc () ++ pr_or_thesis pr_constr c let pr_elim_type = function ET_Case_analysis -> str "cases" | ET_Induction -> str "induction" -let pr_casee env =function - Real c -> str "on" ++ spc () ++ pr_constr env c - | Virtual cut -> str "of" ++ spc () ++ pr_cut (pr_statement pr_constr) env cut +let pr_block_type = function + B_elim et -> pr_elim_type et + | B_proof -> str "proof" + | B_claim -> str "claim" + | B_focus -> str "focus" + +let pr_casee pr_constr pr_tac =function + Real c -> str "on" ++ spc () ++ pr_constr c + | Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) cut let pr_side = function Lhs -> str "=~" | Rhs -> str "~=" -let rec pr_bare_proof_instr _then _thus env = function +let rec pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then _thus = function | Pescape -> str "escape" - | Pthen i -> pr_bare_proof_instr true _thus env i - | Pthus i -> pr_bare_proof_instr _then true env i - | Phence i -> pr_bare_proof_instr true true env i + | Pthen i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true _thus i + | Pthus i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then true i + | Phence i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true true i | Pcut c -> begin match _then,_thus with false,false -> str "have" ++ spc () ++ - pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c | false,true -> str "thus" ++ spc () ++ - pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c | true,false -> str "then" ++ spc () ++ - pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c | true,true -> str "hence" ++ spc () ++ - pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c end | Psuffices c -> - str "suffices" ++ pr_cut pr_suffices_clause env c + str "suffices" ++ pr_cut pr_constr pr_tac (pr_suffices_clause pr_var pr_constr) c | Prew (sid,c) -> (if _thus then str "thus" else str " ") ++ spc () ++ - pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c + pr_side sid ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) c | Passume hyps -> - str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps + str "assume" ++ pr_hyps pr_var pr_constr _I false false "we have" hyps | Plet hyps -> - str "let" ++ print_vars pr_constr _I env false true "let" hyps + str "let" ++ pr_vars pr_var pr_constr _I false true "let" hyps | Pclaim st -> - str "claim" ++ spc () ++ pr_statement pr_constr env st + str "claim" ++ spc () ++ pr_statement pr_constr st | Pfocus st -> - str "focus on" ++ spc () ++ pr_statement pr_constr env st + str "focus on" ++ spc () ++ pr_statement pr_constr st | Pconsider (id,hyps) -> - str "consider" ++ print_vars pr_constr _I env false false "consider" hyps - ++ spc () ++ str "from " ++ pr_constr env id + str "consider" ++ pr_vars pr_var pr_constr _I false false "consider" hyps + ++ spc () ++ str "from " ++ pr_constr id | Pgiven hyps -> - str "given" ++ print_vars pr_constr _I env false false "given" hyps + str "given" ++ pr_vars pr_var pr_constr _I false false "given" hyps | Ptake witl -> str "take" ++ spc () ++ - prlist_with_sep pr_comma (pr_constr env) witl + prlist_with_sep pr_comma pr_constr witl | Pdefine (id,args,body) -> str "define" ++ spc () ++ pr_id id ++ spc () ++ prlist_with_sep spc (fun st -> str "(" ++ - pr_statement pr_constr env st ++ str ")") args ++ spc () ++ - str "as" ++ (pr_constr env body) + pr_var st ++ str ")") args ++ spc () ++ + str "as" ++ (pr_constr body) | Pcast (id,typ) -> str "reconsider" ++ spc () ++ - pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++ - str "as" ++ spc () ++ (pr_constr env typ) + pr_or_thesis pr_id id ++ spc () ++ + str "as" ++ spc () ++ (pr_constr typ) | Psuppose hyps -> str "suppose" ++ - print_hyps pr_constr _I env false false "we have" hyps + pr_hyps pr_var pr_constr _I false false "we have" hyps | Pcase (params,pat,hyps) -> str "suppose it is" ++ spc () ++ pr_pat pat ++ (if params = [] then mt () else (spc () ++ str "with" ++ spc () ++ prlist_with_sep spc (fun st -> str "(" ++ - pr_statement pr_constr env st ++ str ")") params ++ spc ())) + pr_var st ++ str ")") params ++ spc ())) ++ (if hyps = [] then mt () else (spc () ++ str "and" ++ - print_hyps (pr_or_thesis pr_constr) type_or_thesis - env false false "we have" hyps)) - | Pper (et,c) -> + pr_hyps pr_var (pr_or_thesis pr_constr) type_or_thesis + false false "we have" hyps)) + | Pper (et,c) -> str "per" ++ spc () ++ pr_elim_type et ++ spc () ++ - pr_casee env c - | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et - | _ -> anomaly (Pp.str "unprintable instruction") + pr_casee pr_constr pr_tac c + | Pend blk -> str "end" ++ spc () ++ pr_block_type blk let pr_emph = function 0 -> str " " @@ -184,7 +177,39 @@ let pr_emph = function | 3 -> str "*** " | _ -> anomaly (Pp.str "unknown emphasis") -let pr_proof_instr env instr = +let pr_gen_proof_instr pr_var pr_constr pr_pat pr_tac instr = pr_emph instr.emph ++ spc () ++ - pr_bare_proof_instr false false env instr.instr + pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac false false instr.instr + + +let pr_raw_proof_instr pconstr1 pconstr2 ptac (instr : raw_proof_instr) = + pr_gen_proof_instr + (fun (_,(id,otyp)) -> + match otyp with + None -> pr_id id + | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")" + ) + pconstr2 + Ppconstr.pr_cases_pattern_expr + (ptac Pptactic.ltop) + instr + +let pr_glob_proof_instr pconstr1 pconstr2 ptac (instr : glob_proof_instr) = + pr_gen_proof_instr + (fun (_,(id,otyp)) -> + match otyp with + None -> pr_id id + | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")") + pconstr2 + Ppconstr.pr_cases_pattern_expr + (ptac Pptactic.ltop) + instr + +let pr_proof_instr pconstr1 pconstr2 ptac (instr : proof_instr) = + pr_gen_proof_instr + (fun st -> pr_statement pconstr1 st) + pconstr2 + (fun mpat -> Ppconstr.pr_cases_pattern_expr mpat.pat_expr) + (ptac Pptactic.ltop) + instr diff --git a/plugins/decl_mode/ppdecl_proof.mli b/plugins/decl_mode/ppdecl_proof.mli index fd6fb66376..678fc07688 100644 --- a/plugins/decl_mode/ppdecl_proof.mli +++ b/plugins/decl_mode/ppdecl_proof.mli @@ -1,2 +1,14 @@ -val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds +open Decl_expr +open Pptactic + +val pr_gen_proof_instr : + ('var -> Pp.std_ppcmds) -> + ('constr -> Pp.std_ppcmds) -> + ('pat -> Pp.std_ppcmds) -> + ('tac -> Pp.std_ppcmds) -> + ('var,'constr,'pat,'tac) gen_proof_instr -> Pp.std_ppcmds + +val pr_raw_proof_instr : raw_proof_instr raw_extra_genarg_printer +val pr_glob_proof_instr : glob_proof_instr glob_extra_genarg_printer +val pr_proof_instr : proof_instr extra_genarg_printer diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b1cbea51c8..5c74d74f89 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1309,7 +1309,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp tclFIRST[ tclTHEN (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))) - e_assumption; + (Proofview.V82.of_tactic e_assumption); Eauto.eauto_with_bases (true,5) [Evd.empty,Lazy.force refl_equal] diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 new file mode 100644 index 0000000000..856ec0db5f --- /dev/null +++ b/plugins/setoid_ring/g_newring.ml4 @@ -0,0 +1,90 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) + +(*i camlp4deps: "grammar/grammar.cma" i*) + +open Pp +open Util +open Libnames +open Printer +open Newring_ast +open Newring + +DECLARE PLUGIN "newring_plugin" + +TACTIC EXTEND protect_fv + [ "protect_fv" string(map) "in" ident(id) ] -> + [ Proofview.V82.tactic (protect_tac_in map id) ] +| [ "protect_fv" string(map) ] -> + [ Proofview.V82.tactic (protect_tac map) ] +END + +TACTIC EXTEND closed_term + [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] -> + [ Proofview.V82.tactic (closed_term t l) ] +END + +VERNAC ARGUMENT EXTEND ring_mod + | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ] + | [ "abstract" ] -> [ Ring_kind Abstract ] + | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ] + | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ] + | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ] + | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ] + | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ] + | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ] + | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ] + | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] -> + [ Pow_spec (Closed l, pow_spec) ] + | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] -> + [ Pow_spec (CstTac cst_tac, pow_spec) ] + | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ] +END + +VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF + | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> + [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in + add_theory id (ic t) set k cst (pre,post) power sign div] + | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ + msg_notice (strbrk "The following ring structures have been declared:"); + Spmap.iter (fun fn fi -> + msg_notice (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr fi.ring_carrier++spc()++ + str"and equivalence relation "++ pr_constr fi.ring_req)) + ) !from_name ] +END + +TACTIC EXTEND ring_lookup +| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> + [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t] +END + +VERNAC ARGUMENT EXTEND field_mod + | [ ring_mod(m) ] -> [ Ring_mod m ] + | [ "completeness" constr(inj) ] -> [ Inject inj ] +END + +VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF +| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> + [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in + add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div] +| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ + msg_notice (strbrk "The following field structures have been declared:"); + Spmap.iter (fun fn fi -> + msg_notice (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr fi.field_carrier++spc()++ + str"and equivalence relation "++ pr_constr fi.field_req)) + ) !field_from_name ] +END + +TACTIC EXTEND field_lookup +| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> + [ let (t,l) = List.sep_last lt in field_lookup f lH l t ] +END diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml index 2f9e8509c2..7844a36c16 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml @@ -30,8 +30,7 @@ open Declare open Decl_kinds open Entries open Misctypes - -DECLARE PLUGIN "newring_plugin" +open Newring_ast (****************************************************************************) (* controlled reduction *) @@ -105,13 +104,6 @@ let protect_tac_in map id = Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));; -TACTIC EXTEND protect_fv - [ "protect_fv" string(map) "in" ident(id) ] -> - [ Proofview.V82.tactic (protect_tac_in map id) ] -| [ "protect_fv" string(map) ] -> - [ Proofview.V82.tactic (protect_tac map) ] -END;; - (****************************************************************************) let closed_term t l = @@ -120,12 +112,6 @@ let closed_term t l = if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt()) ;; -TACTIC EXTEND closed_term - [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] -> - [ Proofview.V82.tactic (closed_term t l) ] -END -;; - (* TACTIC EXTEND echo | [ "echo" constr(t) ] -> [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ] @@ -143,6 +129,10 @@ let closed_term_ast l = mltac_plugin = "newring_plugin"; mltac_tactic = "closed_term"; } in + let tacname = { + mltac_name = tacname; + mltac_index = 0; + } in let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in TacFun([Some(Id.of_string"t")], TacML(Loc.ghost,tacname, @@ -350,20 +340,6 @@ let _ = add_map "ring" (****************************************************************************) (* Ring database *) -type ring_info = - { ring_carrier : types; - ring_req : constr; - ring_setoid : constr; - ring_ext : constr; - ring_morph : constr; - ring_th : constr; - ring_cst_tac : glob_tactic_expr; - ring_pow_tac : glob_tactic_expr; - ring_lemma1 : constr; - ring_lemma2 : constr; - ring_pre_tac : glob_tactic_expr; - ring_post_tac : glob_tactic_expr } - module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" @@ -595,13 +571,6 @@ let dest_morph env sigma m_spec = (c,czero,cone,cadd,cmul,None,None,ceqb,phi) | _ -> error "bad morphism structure" - -type 'constr coeff_spec = - Computational of 'constr (* equality test *) - | Abstract (* coeffs = Z *) - | Morphism of 'constr (* general morphism *) - - let reflect_coeff rkind = (* We build an ill-typed terms on purpose... *) match rkind with @@ -609,10 +578,6 @@ let reflect_coeff rkind = | Computational c -> lapp coq_comp [|c|] | Morphism m -> lapp coq_morph [|m|] -type cst_tac_spec = - CstTac of raw_tactic_expr - | Closed of reference list - let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = match cst_tac with Some (CstTac t) -> Tacintern.glob_tactic t @@ -716,41 +681,12 @@ let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div = ring_post_tac = posttac }) in () -type 'constr ring_mod = - Ring_kind of 'constr coeff_spec - | Const_tac of cst_tac_spec - | Pre_tac of raw_tactic_expr - | Post_tac of raw_tactic_expr - | Setoid of Constrexpr.constr_expr * Constrexpr.constr_expr - | Pow_spec of cst_tac_spec * Constrexpr.constr_expr - (* Syntaxification tactic , correctness lemma *) - | Sign_spec of Constrexpr.constr_expr - | Div_spec of Constrexpr.constr_expr - - let ic_coeff_spec = function | Computational t -> Computational (ic_unsafe t) | Morphism t -> Morphism (ic_unsafe t) | Abstract -> Abstract -VERNAC ARGUMENT EXTEND ring_mod - | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ] - | [ "abstract" ] -> [ Ring_kind Abstract ] - | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ] - | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ] - | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ] - | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ] - | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ] - | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ] - | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ] - | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] -> - [ Pow_spec (Closed l, pow_spec) ] - | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] -> - [ Pow_spec (CstTac cst_tac, pow_spec) ] - | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ] -END - let set_once s r v = if Option.is_empty !r then r := Some v else error (s^" cannot be set twice") @@ -775,20 +711,6 @@ let process_ring_mods l = let k = match !kind with Some k -> k | None -> Abstract in (k, !set, !cst_tac, !pre, !post, !power, !sign, !div) -VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF - | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> - [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in - add_theory id (ic t) set k cst (pre,post) power sign div] - | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ - msg_notice (strbrk "The following ring structures have been declared:"); - Spmap.iter (fun fn fi -> - msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.ring_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.ring_req)) - ) !from_name ] -END - (*****************************************************************************) (* The tactics consist then only in a lookup in the ring database and call the appropriate ltac. *) @@ -834,13 +756,6 @@ let ring_lookup (f:glob_tactic_expr) lH rl t = with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end -TACTIC EXTEND ring_lookup -| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> - [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t] -END - - - (***********************************************************************) let new_field_path = @@ -914,19 +829,6 @@ let dest_field env evd th_spec = (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth) | _ -> error "bad field structure" -type field_info = - { field_carrier : types; - field_req : constr; - field_cst_tac : glob_tactic_expr; - field_pow_tac : glob_tactic_expr; - field_ok : constr; - field_simpl_eq_ok : constr; - field_simpl_ok : constr; - field_simpl_eq_in_ok : constr; - field_cond : constr; - field_pre_tac : glob_tactic_expr; - field_post_tac : glob_tactic_expr } - let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table" let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table" @@ -1073,15 +975,6 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power field_pre_tac = pretac; field_post_tac = posttac }) in () -type 'constr field_mod = - Ring_mod of 'constr ring_mod - | Inject of Constrexpr.constr_expr - -VERNAC ARGUMENT EXTEND field_mod - | [ ring_mod(m) ] -> [ Ring_mod m ] - | [ "completeness" constr(inj) ] -> [ Inject inj ] -END - let process_field_mods l = let kind = ref None in let set = ref None in @@ -1106,21 +999,6 @@ let process_field_mods l = let k = match !kind with Some k -> k | None -> Abstract in (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div) -VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF -| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> - [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in - add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div] -| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ - msg_notice (strbrk "The following field structures have been declared:"); - Spmap.iter (fun fn fi -> - msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.field_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.field_req)) - ) !field_from_name ] -END - - let ltac_field_structure e = let req = carg e.field_req in let cst_tac = Tacexp e.field_cst_tac in @@ -1149,9 +1027,3 @@ let field_lookup (f:glob_tactic_expr) lH rl t = Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end - - -TACTIC EXTEND field_lookup -| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> - [ let (t,l) = List.sep_last lt in field_lookup f lH l t ] -END diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli new file mode 100644 index 0000000000..4bd3383d65 --- /dev/null +++ b/plugins/setoid_ring/newring.mli @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) + +open Names +open Constr +open Libnames +open Globnames +open Constrexpr +open Tacexpr +open Proof_type +open Newring_ast + +val protect_tac_in : string -> Id.t -> tactic + +val protect_tac : string -> tactic + +val closed_term : constr -> global_reference list -> tactic + +val process_ring_mods : + constr_expr ring_mod list -> + constr coeff_spec * (constr * constr) option * + cst_tac_spec option * raw_tactic_expr option * + raw_tactic_expr option * + (cst_tac_spec * constr_expr) option * + constr_expr option * constr_expr option + +val add_theory : + Id.t -> + Evd.evar_map * constr -> + (constr * constr) option -> + constr coeff_spec -> + cst_tac_spec option -> + raw_tactic_expr option * raw_tactic_expr option -> + (cst_tac_spec * constr_expr) option -> + constr_expr option -> + constr_expr option -> unit + +val ic : constr_expr -> Evd.evar_map * constr + +val from_name : ring_info Spmap.t ref + +val ring_lookup : + glob_tactic_expr -> + constr list -> + constr list -> constr -> unit Proofview.tactic + +val process_field_mods : + constr_expr field_mod list -> + constr coeff_spec * + (constr * constr) option * constr option * + cst_tac_spec option * raw_tactic_expr option * + raw_tactic_expr option * + (cst_tac_spec * constr_expr) option * + constr_expr option * constr_expr option + +val add_field_theory : + Id.t -> + Evd.evar_map * constr -> + (constr * constr) option -> + constr coeff_spec -> + cst_tac_spec option -> + constr option -> + raw_tactic_expr option * raw_tactic_expr option -> + (cst_tac_spec * constr_expr) option -> + constr_expr option -> + constr_expr option -> unit + +val field_from_name : field_info Spmap.t ref + +val field_lookup : + glob_tactic_expr -> + constr list -> + constr list -> constr -> unit Proofview.tactic diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli new file mode 100644 index 0000000000..c26fcc8d1f --- /dev/null +++ b/plugins/setoid_ring/newring_ast.mli @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) + +open Constr +open Libnames +open Constrexpr +open Tacexpr + +type 'constr coeff_spec = + Computational of 'constr (* equality test *) + | Abstract (* coeffs = Z *) + | Morphism of 'constr (* general morphism *) + +type cst_tac_spec = + CstTac of raw_tactic_expr + | Closed of reference list + +type 'constr ring_mod = + Ring_kind of 'constr coeff_spec + | Const_tac of cst_tac_spec + | Pre_tac of raw_tactic_expr + | Post_tac of raw_tactic_expr + | Setoid of constr_expr * constr_expr + | Pow_spec of cst_tac_spec * constr_expr + (* Syntaxification tactic , correctness lemma *) + | Sign_spec of constr_expr + | Div_spec of constr_expr + +type 'constr field_mod = + Ring_mod of 'constr ring_mod + | Inject of constr_expr + +type ring_info = + { ring_carrier : types; + ring_req : constr; + ring_setoid : constr; + ring_ext : constr; + ring_morph : constr; + ring_th : constr; + ring_cst_tac : glob_tactic_expr; + ring_pow_tac : glob_tactic_expr; + ring_lemma1 : constr; + ring_lemma2 : constr; + ring_pre_tac : glob_tactic_expr; + ring_post_tac : glob_tactic_expr } + +type field_info = + { field_carrier : types; + field_req : constr; + field_cst_tac : glob_tactic_expr; + field_pow_tac : glob_tactic_expr; + field_ok : constr; + field_simpl_eq_ok : constr; + field_simpl_ok : constr; + field_simpl_eq_in_ok : constr; + field_cond : constr; + field_pre_tac : glob_tactic_expr; + field_post_tac : glob_tactic_expr } diff --git a/plugins/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib index a98392f1e0..7d6c495889 100644 --- a/plugins/setoid_ring/newring_plugin.mllib +++ b/plugins/setoid_ring/newring_plugin.mllib @@ -1,2 +1,3 @@ Newring Newring_plugin_mod +G_newring |