From 4e515c483e41f0362bf1102f8e8ae071fdcf04f7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 25 Jan 2015 13:40:13 +0100 Subject: Adding a proper interface to Newring. The ring ASTs were put in a separate interface, and only the extension-related code was put in a dedicated G_newring file. --- plugins/setoid_ring/g_newring.ml4 | 90 +++ plugins/setoid_ring/newring.ml | 1029 ++++++++++++++++++++++++++ plugins/setoid_ring/newring.ml4 | 1161 ------------------------------ plugins/setoid_ring/newring.mli | 78 ++ plugins/setoid_ring/newring_ast.mli | 63 ++ plugins/setoid_ring/newring_plugin.mllib | 1 + 6 files changed, 1261 insertions(+), 1161 deletions(-) create mode 100644 plugins/setoid_ring/g_newring.ml4 create mode 100644 plugins/setoid_ring/newring.ml delete mode 100644 plugins/setoid_ring/newring.ml4 create mode 100644 plugins/setoid_ring/newring.mli create mode 100644 plugins/setoid_ring/newring_ast.mli (limited to 'plugins') 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 *) +(* + [ 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.ml b/plugins/setoid_ring/newring.ml new file mode 100644 index 0000000000..7844a36c16 --- /dev/null +++ b/plugins/setoid_ring/newring.ml @@ -0,0 +1,1029 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* f (Evar.repr i) c + | _ -> assert false + +type protect_flag = Eval|Prot|Rec + +let tag_arg tag_rec map subs i c = + match map i with + Eval -> mk_clos subs c + | Prot -> mk_atom c + | Rec -> if Int.equal i (-1) then mk_clos subs c else tag_rec c + +let global_head_of_constr c = + let f, args = decompose_app c in + try global_of_constr f + with Not_found -> anomaly (str "global_head_of_constr") + +let global_of_constr_nofail c = + try global_of_constr c + with Not_found -> VarRef (Id.of_string "dummy") + +let rec mk_clos_but f_map subs t = + match f_map (global_of_constr_nofail t) with + | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t + | None -> + (match kind_of_term t with + App(f,args) -> mk_clos_app_but f_map subs f args 0 + | Prod _ -> mk_clos_deep (mk_clos_but f_map) subs t + | _ -> mk_atom t) + +and mk_clos_app_but f_map subs f args n = + if n >= Array.length args then mk_atom(mkApp(f, args)) + else + let fargs, args' = Array.chop n args in + let f' = mkApp(f,fargs) in + match f_map (global_of_constr_nofail f') with + Some map -> + mk_clos_deep + (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s')) + subs + (mkApp (mark_arg (-1) f', Array.mapi mark_arg args')) + | None -> mk_clos_app_but f_map subs f args (n+1) + +let interp_map l t = + try Some(List.assoc_f eq_gr t l) with Not_found -> None + +let protect_maps = ref String.Map.empty +let add_map s m = protect_maps := String.Map.add s m !protect_maps +let lookup_map map = + try String.Map.find map !protect_maps + with Not_found -> + errorlabstrm"lookup_map"(str"map "++qs map++str"not found") + +let protect_red map env sigma c = + kl (create_clos_infos betadeltaiota env) + (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);; + +let protect_tac map = + Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; + +let protect_tac_in map id = + Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));; + + +(****************************************************************************) + +let closed_term t l = + let l = List.map Universes.constr_of_global l in + let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in + if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt()) +;; + +(* TACTIC EXTEND echo +| [ "echo" constr(t) ] -> + [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ] +END;;*) + +(* +let closed_term_ast l = + TacFun([Some(Id.of_string"t")], + TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term", + [Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t")); + Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l]))) +*) +let closed_term_ast l = + let tacname = { + 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, + [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None); + Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l])) +(* +let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" +*) + +(****************************************************************************) + +let ic c = + let env = Global.env() and sigma = Evd.empty in + Constrintern.interp_open_constr env sigma c + +let ic_unsafe c = (*FIXME remove *) + let env = Global.env() and sigma = Evd.empty in + fst (Constrintern.interp_constr env sigma c) + +let ty c = Typing.type_of (Global.env()) Evd.empty c + +let decl_constant na ctx c = + let vars = Universes.universes_of_constr c in + let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in + mkConst(declare_constant (Id.of_string na) + (DefinitionEntry (definition_entry ~opaque:true + ~univs:(Univ.ContextSet.to_context ctx) c), + IsProof Lemma)) + +(* Calling a global tactic *) +let ltac_call tac (args:glob_tactic_arg list) = + TacArg(Loc.ghost,TacCall(Loc.ghost, ArgArg(Loc.ghost, Lazy.force tac),args)) + +(* Calling a locally bound tactic *) +let ltac_lcall tac args = + TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args)) + +let ltac_letin (x, e1) e2 = + TacLetIn(false,[(Loc.ghost,Id.of_string x),e1],e2) + +let ltac_apply (f:glob_tactic_expr) (args:glob_tactic_arg list) = + Tacinterp.eval_tactic + (ltac_letin ("F", Tacexp f) (ltac_lcall "F" args)) + +let ltac_record flds = + TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds) + + +let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c) + +let dummy_goal env sigma = + let (gl,_,sigma) = + Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in + {Evd.it = gl; Evd.sigma = sigma} + +let constr_of v = match Value.to_constr v with + | Some c -> c + | None -> failwith "Ring.exec_tactic: anomaly" + +let exec_tactic env evd n f args = + let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in + let res = ref [||] in + let get_res ist = + let l = List.map (fun id -> Id.Map.find id ist.lfun) lid in + res := Array.of_list l; + TacId[] in + let getter = + Tacexp(TacFun(List.map(fun id -> Some id) lid, + Tacintern.glob_tactic(tacticIn get_res))) in + let gl = dummy_goal env evd in + let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in + let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in + Array.map (fun x -> nf (constr_of x)) !res, Evd.universe_context evd + +let stdlib_modules = + [["Coq";"Setoids";"Setoid"]; + ["Coq";"Lists";"List"]; + ["Coq";"Init";"Datatypes"]; + ["Coq";"Init";"Logic"]; + ] + +let coq_constant c = + lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c) +let coq_reference c = + lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c) + +let coq_mk_Setoid = coq_constant "Build_Setoid_Theory" +let coq_None = coq_reference "None" +let coq_Some = coq_reference "Some" +let coq_eq = coq_constant "eq" + +let coq_cons = coq_reference "cons" +let coq_nil = coq_reference "nil" + +let lapp f args = mkApp(Lazy.force f,args) + +let plapp evd f args = + let fc = Evarutil.e_new_global evd (Lazy.force f) in + mkApp(fc,args) + +let dest_rel0 t = + match kind_of_term t with + | App(f,args) when Array.length args >= 2 -> + let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in + if closed0 rel then + (rel,args.(Array.length args - 2),args.(Array.length args - 1)) + else error "ring: cannot find relation (not closed)" + | _ -> error "ring: cannot find relation" + +let rec dest_rel t = + match kind_of_term t with + | Prod(_,_,c) -> dest_rel c + | _ -> dest_rel0 t + +(****************************************************************************) +(* Library linking *) + +let plugin_dir = "setoid_ring" + +let cdir = ["Coq";plugin_dir] +let plugin_modules = + List.map (fun d -> cdir@d) + [["Ring_theory"];["Ring_polynom"]; ["Ring_tac"];["InitialRing"]; + ["Field_tac"]; ["Field_theory"] + ] + +let my_constant c = + lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c) +let my_reference c = + lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) + +let new_ring_path = + DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"]) +let ltac s = + lazy(make_kn (MPfile new_ring_path) DirPath.empty (Label.make s)) +let znew_ring_path = + DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) +let zltac s = + lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s)) + +let mk_cst l s = lazy (Coqlib.gen_reference "newring" l s);; +let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; + +(* Ring theory *) + +(* almost_ring defs *) +let coq_almost_ring_theory = my_constant "almost_ring_theory" + +(* setoid and morphism utilities *) +let coq_eq_setoid = my_reference "Eqsth" +let coq_eq_morph = my_reference "Eq_ext" +let coq_eq_smorph = my_reference "Eq_s_ext" + +(* ring -> almost_ring utilities *) +let coq_ring_theory = my_constant "ring_theory" +let coq_mk_reqe = my_constant "mk_reqe" + +(* semi_ring -> almost_ring utilities *) +let coq_semi_ring_theory = my_constant "semi_ring_theory" +let coq_mk_seqe = my_constant "mk_seqe" + +let ltac_inv_morph_gen = zltac"inv_gen_phi" +let ltac_inv_morphZ = zltac"inv_gen_phiZ" +let ltac_inv_morphN = zltac"inv_gen_phiN" +let ltac_inv_morphNword = zltac"inv_gen_phiNword" +let coq_abstract = my_constant"Abstract" +let coq_comp = my_constant"Computational" +let coq_morph = my_constant"Morphism" + +(* morphism *) +let coq_ring_morph = my_constant "ring_morph" +let coq_semi_morph = my_constant "semi_morph" + +(* power function *) +let ltac_inv_morph_nothing = zltac"inv_morph_nothing" +let coq_pow_N_pow_N = my_constant "pow_N_pow_N" + +(* hypothesis *) +let coq_mkhypo = my_reference "mkhypo" +let coq_hypo = my_reference "hypo" + +(* Equality: do not evaluate but make recursive call on both sides *) +let map_with_eq arg_map c = + let (req,_,_) = dest_rel c in + interp_map + ((global_head_of_constr req,(function -1->Prot|_->Rec)):: + List.map (fun (c,map) -> (Lazy.force c,map)) arg_map) + +let map_without_eq arg_map _ = + interp_map (List.map (fun (c,map) -> (Lazy.force c,map)) arg_map) + +let _ = add_map "ring" + (map_with_eq + [coq_cons,(function -1->Eval|2->Rec|_->Prot); + coq_nil, (function -1->Eval|_ -> Prot); + (* Pphi_dev: evaluate polynomial and coef operations, protect + ring operations and make recursive call on the var map *) + pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); + pol_cst "Pphi_pow", + (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); + (* PEeval: evaluate morphism and polynomial, protect ring + operations and make recursive call on the var map *) + pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot)]) + +(****************************************************************************) +(* Ring database *) + +module Cmap = Map.Make(Constr) + +let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" +let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table" + +let ring_for_carrier r = Cmap.find r !from_carrier + +let find_ring_structure env sigma l = + match l with + | t::cl' -> + let ty = Retyping.get_type_of env sigma t in + let check c = + let ty' = Retyping.get_type_of env sigma c in + if not (Reductionops.is_conv env sigma ty ty') then + errorlabstrm "ring" + (str"arguments of ring_simplify do not have all the same type") + in + List.iter check cl'; + (try ring_for_carrier ty + with Not_found -> + errorlabstrm "ring" + (str"cannot find a declared ring structure over"++ + spc()++str"\""++pr_constr ty++str"\"")) + | [] -> assert false + +let add_entry (sp,_kn) e = + from_carrier := Cmap.add e.ring_carrier e !from_carrier; + from_name := Spmap.add sp e !from_name + + +let subst_th (subst,th) = + let c' = subst_mps subst th.ring_carrier in + let eq' = subst_mps subst th.ring_req in + let set' = subst_mps subst th.ring_setoid in + let ext' = subst_mps subst th.ring_ext in + let morph' = subst_mps subst th.ring_morph in + let th' = subst_mps subst th.ring_th in + let thm1' = subst_mps subst th.ring_lemma1 in + let thm2' = subst_mps subst th.ring_lemma2 in + let tac'= Tacsubst.subst_tactic subst th.ring_cst_tac in + let pow_tac'= Tacsubst.subst_tactic subst th.ring_pow_tac in + let pretac'= Tacsubst.subst_tactic subst th.ring_pre_tac in + let posttac'= Tacsubst.subst_tactic subst th.ring_post_tac in + if c' == th.ring_carrier && + eq' == th.ring_req && + eq_constr set' th.ring_setoid && + ext' == th.ring_ext && + morph' == th.ring_morph && + th' == th.ring_th && + thm1' == th.ring_lemma1 && + thm2' == th.ring_lemma2 && + tac' == th.ring_cst_tac && + pow_tac' == th.ring_pow_tac && + pretac' == th.ring_pre_tac && + posttac' == th.ring_post_tac then th + else + { ring_carrier = c'; + ring_req = eq'; + ring_setoid = set'; + ring_ext = ext'; + ring_morph = morph'; + ring_th = th'; + ring_cst_tac = tac'; + ring_pow_tac = pow_tac'; + ring_lemma1 = thm1'; + ring_lemma2 = thm2'; + ring_pre_tac = pretac'; + ring_post_tac = posttac' } + + +let theory_to_obj : ring_info -> obj = + let cache_th (name,th) = add_entry name th in + declare_object + {(default_object "tactic-new-ring-theory") with + open_function = (fun i o -> if Int.equal i 1 then cache_th o); + cache_function = cache_th; + subst_function = subst_th; + classify_function = (fun x -> Substitute x)} + + +let setoid_of_relation env evd a r = + try + let evm = !evd in + let evm, refl = Rewrite.get_reflexive_proof env evm a r in + let evm, sym = Rewrite.get_symmetric_proof env evm a r in + let evm, trans = Rewrite.get_transitive_proof env evm a r in + evd := evm; + lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |] + with Not_found -> + error "cannot find setoid relation" + +let op_morph r add mul opp req m1 m2 m3 = + lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |] + +let op_smorph r add mul req m1 m2 = + lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |] + +(* let default_ring_equality (r,add,mul,opp,req) = *) +(* let is_setoid = function *) +(* {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *) +(* eq_constr_nounivs req rel (\* Qu: use conversion ? *\) *) +(* | _ -> false in *) +(* match default_relation_for_carrier ~filter:is_setoid r with *) +(* Leibniz _ -> *) +(* let setoid = lapp coq_eq_setoid [|r|] in *) +(* let op_morph = *) +(* match opp with *) +(* Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] *) +(* | None -> lapp coq_eq_smorph [|r;add;mul|] in *) +(* (setoid,op_morph) *) +(* | Relation rel -> *) +(* let setoid = setoid_of_relation rel in *) +(* let is_endomorphism = function *) +(* { args=args } -> List.for_all *) +(* (function (var,Relation rel) -> *) +(* var=None && eq_constr_nounivs req rel *) +(* | _ -> false) args in *) +(* let add_m = *) +(* try default_morphism ~filter:is_endomorphism add *) +(* with Not_found -> *) +(* error "ring addition should be declared as a morphism" in *) +(* let mul_m = *) +(* try default_morphism ~filter:is_endomorphism mul *) +(* with Not_found -> *) +(* error "ring multiplication should be declared as a morphism" in *) +(* let op_morph = *) +(* match opp with *) +(* | Some opp -> *) +(* (let opp_m = *) +(* try default_morphism ~filter:is_endomorphism opp *) +(* with Not_found -> *) +(* error "ring opposite should be declared as a morphism" in *) +(* let op_morph = *) +(* op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in *) +(* msgnl *) +(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++ *) +(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *) +(* str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ *) +(* str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ *) +(* str"\""); *) +(* op_morph) *) +(* | None -> *) +(* (msgnl *) +(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ *) +(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *) +(* str"\""++spc()++str"and \""++ *) +(* pr_constr mul_m.morphism_theory++str"\""); *) +(* op_smorph r add mul req add_m.lem mul_m.lem) in *) +(* (setoid,op_morph) *) + +let ring_equality env evd (r,add,mul,opp,req) = + match kind_of_term req with + | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) -> + let setoid = plapp evd coq_eq_setoid [|r|] in + let op_morph = + match opp with + Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|] + | None -> plapp evd coq_eq_smorph [|r;add;mul|] in + let setoid = Typing.solve_evars env evd setoid in + let op_morph = Typing.solve_evars env evd op_morph in + (setoid,op_morph) + | _ -> + let setoid = setoid_of_relation (Global.env ()) evd r req in + let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in + let add_m, add_m_lem = + try Rewrite.default_morphism signature add + with Not_found -> + error "ring addition should be declared as a morphism" in + let mul_m, mul_m_lem = + try Rewrite.default_morphism signature mul + with Not_found -> + error "ring multiplication should be declared as a morphism" in + let op_morph = + match opp with + | Some opp -> + (let opp_m,opp_m_lem = + try Rewrite.default_morphism ([Some(r,Some req)],Some(r,Some req)) opp + with Not_found -> + error "ring opposite should be declared as a morphism" in + let op_morph = + op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in + Flags.if_verbose + msg_info + (str"Using setoid \""++pr_constr req++str"\""++spc()++ + str"and morphisms \""++pr_constr add_m_lem ++ + str"\","++spc()++ str"\""++pr_constr mul_m_lem++ + str"\""++spc()++str"and \""++pr_constr opp_m_lem++ + str"\""); + op_morph) + | None -> + (Flags.if_verbose + msg_info + (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ + str"and morphisms \""++pr_constr add_m_lem ++ + str"\""++spc()++str"and \""++ + pr_constr mul_m_lem++str"\""); + op_smorph r add mul req add_m_lem mul_m_lem) in + (setoid,op_morph) + +let build_setoid_params env evd r add mul opp req eqth = + match eqth with + Some th -> th + | None -> ring_equality env evd (r,add,mul,opp,req) + +let dest_ring env sigma th_spec = + let th_typ = Retyping.get_type_of env sigma th_spec in + match kind_of_term th_typ with + App(f,[|r;zero;one;add;mul;sub;opp;req|]) + when eq_constr_nounivs f (Lazy.force coq_almost_ring_theory) -> + (None,r,zero,one,add,mul,Some sub,Some opp,req) + | App(f,[|r;zero;one;add;mul;req|]) + when eq_constr_nounivs f (Lazy.force coq_semi_ring_theory) -> + (Some true,r,zero,one,add,mul,None,None,req) + | App(f,[|r;zero;one;add;mul;sub;opp;req|]) + when eq_constr_nounivs f (Lazy.force coq_ring_theory) -> + (Some false,r,zero,one,add,mul,Some sub,Some opp,req) + | _ -> error "bad ring structure" + + +let dest_morph env sigma m_spec = + let m_typ = Retyping.get_type_of env sigma m_spec in + match kind_of_term m_typ with + App(f,[|r;zero;one;add;mul;sub;opp;req; + c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) + when eq_constr_nounivs f (Lazy.force coq_ring_morph) -> + (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi) + | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|]) + when eq_constr_nounivs f (Lazy.force coq_semi_morph) -> + (c,czero,cone,cadd,cmul,None,None,ceqb,phi) + | _ -> error "bad morphism structure" + +let reflect_coeff rkind = + (* We build an ill-typed terms on purpose... *) + match rkind with + Abstract -> Lazy.force coq_abstract + | Computational c -> lapp coq_comp [|c|] + | Morphism m -> lapp coq_morph [|m|] + +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 + | Some (Closed lc) -> + closed_term_ast (List.map Smartlocate.global_with_alias lc) + | None -> + let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morph_nothing) in + TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])) + +let make_hyp env evd c = + let t = Retyping.get_type_of env !evd c in + plapp evd coq_mkhypo [|t;c|] + +let make_hyp_list env evd lH = + let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in + let l = + List.fold_right + (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH + (plapp evd coq_nil [|carrier|]) + in + let l' = Typing.solve_evars env evd l in + Evarutil.nf_evars_universes !evd l' + +let interp_power env evd pow = + let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in + match pow with + | None -> + let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in + (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), plapp evd coq_None [|carrier|]) + | Some (tac, spec) -> + let tac = + match tac with + | CstTac t -> Tacintern.glob_tactic t + | Closed lc -> + closed_term_ast (List.map Smartlocate.global_with_alias lc) in + let spec = make_hyp env evd (ic_unsafe spec) in + (tac, plapp evd coq_Some [|carrier; spec|]) + +let interp_sign env evd sign = + let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in + match sign with + | None -> plapp evd coq_None [|carrier|] + | Some spec -> + let spec = make_hyp env evd (ic_unsafe spec) in + plapp evd coq_Some [|carrier;spec|] + (* Same remark on ill-typed terms ... *) + +let interp_div env evd div = + let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in + match div with + | None -> plapp evd coq_None [|carrier|] + | Some spec -> + let spec = make_hyp env evd (ic_unsafe spec) in + plapp evd coq_Some [|carrier;spec|] + (* Same remark on ill-typed terms ... *) + +let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div = + check_required_library (cdir@["Ring_base"]); + let env = Global.env() in + let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in + let evd = ref sigma in + let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in + let (pow_tac, pspec) = interp_power env evd power in + let sspec = interp_sign env evd sign in + let dspec = interp_div env evd div in + let rk = reflect_coeff morphth in + let params,ctx = + exec_tactic env !evd 5 (zltac "ring_lemmas") + (List.map carg[sth;ext;rth;pspec;sspec;dspec;rk]) in + let lemma1 = params.(3) in + let lemma2 = params.(4) in + + let lemma1 = + decl_constant (Id.to_string name^"_ring_lemma1") ctx lemma1 in + let lemma2 = + decl_constant (Id.to_string name^"_ring_lemma2") ctx lemma2 in + let cst_tac = + interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in + let pretac = + match pre with + Some t -> Tacintern.glob_tactic t + | _ -> TacId [] in + let posttac = + match post with + Some t -> Tacintern.glob_tactic t + | _ -> TacId [] in + let _ = + Lib.add_leaf name + (theory_to_obj + { ring_carrier = r; + ring_req = req; + ring_setoid = sth; + ring_ext = params.(1); + ring_morph = params.(2); + ring_th = params.(0); + ring_cst_tac = cst_tac; + ring_pow_tac = pow_tac; + ring_lemma1 = lemma1; + ring_lemma2 = lemma2; + ring_pre_tac = pretac; + ring_post_tac = posttac }) in + () + +let ic_coeff_spec = function + | Computational t -> Computational (ic_unsafe t) + | Morphism t -> Morphism (ic_unsafe t) + | Abstract -> Abstract + + +let set_once s r v = + if Option.is_empty !r then r := Some v else error (s^" cannot be set twice") + +let process_ring_mods l = + let kind = ref None in + let set = ref None in + let cst_tac = ref None in + let pre = ref None in + let post = ref None in + let sign = ref None in + let power = ref None in + let div = ref None in + List.iter(function + Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec k) + | Const_tac t -> set_once "tactic recognizing constants" cst_tac t + | Pre_tac t -> set_once "preprocess tactic" pre t + | Post_tac t -> set_once "postprocess tactic" post t + | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext) + | Pow_spec(t,spec) -> set_once "power" power (t,spec) + | Sign_spec t -> set_once "sign" sign t + | Div_spec t -> set_once "div" div t) l; + let k = match !kind with Some k -> k | None -> Abstract in + (k, !set, !cst_tac, !pre, !post, !power, !sign, !div) + +(*****************************************************************************) +(* The tactics consist then only in a lookup in the ring database and + call the appropriate ltac. *) + +let make_args_list rl t = + match rl with + | [] -> let (_,t1,t2) = dest_rel0 t in [t1;t2] + | _ -> rl + +let make_term_list env evd carrier rl = + let l = List.fold_right + (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl + (plapp evd coq_nil [|carrier|]) + in Typing.solve_evars env evd l + +let ltac_ring_structure e = + let req = carg e.ring_req in + let sth = carg e.ring_setoid in + let ext = carg e.ring_ext in + let morph = carg e.ring_morph in + let th = carg e.ring_th in + let cst_tac = Tacexp e.ring_cst_tac in + let pow_tac = Tacexp e.ring_pow_tac in + let lemma1 = carg e.ring_lemma1 in + let lemma2 = carg e.ring_lemma2 in + let pretac = Tacexp(TacFun([None],e.ring_pre_tac)) in + let posttac = Tacexp(TacFun([None],e.ring_post_tac)) in + [req;sth;ext;morph;th;cst_tac;pow_tac; + lemma1;lemma2;pretac;posttac] + +let ring_lookup (f:glob_tactic_expr) lH rl t = + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + try (* find_ring_strucure can raise an exception *) + let evdref = ref sigma in + let rl = make_args_list rl t in + let e = find_ring_structure env sigma rl in + let rl = carg (make_term_list env evdref e.ring_carrier rl) in + let lH = carg (make_hyp_list env evdref lH) in + let ring = ltac_ring_structure e in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl])) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end + +(***********************************************************************) + +let new_field_path = + DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"]) + +let field_ltac s = + lazy(make_kn (MPfile new_field_path) DirPath.empty (Label.make s)) + + +let _ = add_map "field" + (map_with_eq + [coq_cons,(function -1->Eval|2->Rec|_->Prot); + coq_nil, (function -1->Eval|_ -> Prot); + (* display_linear: evaluate polynomials and coef operations, protect + field operations and make recursive call on the var map *) + my_reference "display_linear", + (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot); + my_reference "display_pow_linear", + (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot); + (* Pphi_dev: evaluate polynomial and coef operations, protect + ring operations and make recursive call on the var map *) + pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); + pol_cst "Pphi_pow", + (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); + (* PEeval: evaluate morphism and polynomial, protect ring + operations and make recursive call on the var map *) + pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot); + (* FEeval: evaluate morphism, protect field + operations and make recursive call on the var map *) + my_reference "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);; + +let _ = add_map "field_cond" + (map_without_eq + [coq_cons,(function -1->Eval|2->Rec|_->Prot); + coq_nil, (function -1->Eval|_ -> Prot); + (* PCond: evaluate morphism and denum list, protect ring + operations and make recursive call on the var map *) + my_reference "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);; +(* (function -1|9|11->Eval|10->Rec|_->Prot)]);;*) + + +let _ = Redexpr.declare_reduction "simpl_field_expr" + (protect_red "field") + + + +let afield_theory = my_reference "almost_field_theory" +let field_theory = my_reference "field_theory" +let sfield_theory = my_reference "semi_field_theory" +let af_ar = my_reference"AF_AR" +let f_r = my_reference"F_R" +let sf_sr = my_reference"SF_SR" +let dest_field env evd th_spec = + let th_typ = Retyping.get_type_of env !evd th_spec in + match kind_of_term th_typ with + | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) + when is_global (Lazy.force afield_theory) f -> + let rth = plapp evd af_ar + [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in + (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) + | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) + when is_global (Lazy.force field_theory) f -> + let rth = + plapp evd f_r + [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in + (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) + | App(f,[|r;zero;one;add;mul;div;inv;req|]) + when is_global (Lazy.force sfield_theory) f -> + let rth = plapp evd sf_sr + [|r;zero;one;add;mul;div;inv;req;th_spec|] in + (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth) + | _ -> error "bad field structure" + +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" + +let field_for_carrier r = Cmap.find r !field_from_carrier + +let find_field_structure env sigma l = + check_required_library (cdir@["Field_tac"]); + match l with + | t::cl' -> + let ty = Retyping.get_type_of env sigma t in + let check c = + let ty' = Retyping.get_type_of env sigma c in + if not (Reductionops.is_conv env sigma ty ty') then + errorlabstrm "field" + (str"arguments of field_simplify do not have all the same type") + in + List.iter check cl'; + (try field_for_carrier ty + with Not_found -> + errorlabstrm "field" + (str"cannot find a declared field structure over"++ + spc()++str"\""++pr_constr ty++str"\"")) + | [] -> assert false + +let add_field_entry (sp,_kn) e = + field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier; + field_from_name := Spmap.add sp e !field_from_name + +let subst_th (subst,th) = + let c' = subst_mps subst th.field_carrier in + let eq' = subst_mps subst th.field_req in + let thm1' = subst_mps subst th.field_ok in + let thm2' = subst_mps subst th.field_simpl_eq_ok in + let thm3' = subst_mps subst th.field_simpl_ok in + let thm4' = subst_mps subst th.field_simpl_eq_in_ok in + let thm5' = subst_mps subst th.field_cond in + let tac'= Tacsubst.subst_tactic subst th.field_cst_tac in + let pow_tac' = Tacsubst.subst_tactic subst th.field_pow_tac in + let pretac'= Tacsubst.subst_tactic subst th.field_pre_tac in + let posttac'= Tacsubst.subst_tactic subst th.field_post_tac in + if c' == th.field_carrier && + eq' == th.field_req && + thm1' == th.field_ok && + thm2' == th.field_simpl_eq_ok && + thm3' == th.field_simpl_ok && + thm4' == th.field_simpl_eq_in_ok && + thm5' == th.field_cond && + tac' == th.field_cst_tac && + pow_tac' == th.field_pow_tac && + pretac' == th.field_pre_tac && + posttac' == th.field_post_tac then th + else + { field_carrier = c'; + field_req = eq'; + field_cst_tac = tac'; + field_pow_tac = pow_tac'; + field_ok = thm1'; + field_simpl_eq_ok = thm2'; + field_simpl_ok = thm3'; + field_simpl_eq_in_ok = thm4'; + field_cond = thm5'; + field_pre_tac = pretac'; + field_post_tac = posttac' } + +let ftheory_to_obj : field_info -> obj = + let cache_th (name,th) = add_field_entry name th in + declare_object + {(default_object "tactic-new-field-theory") with + open_function = (fun i o -> if Int.equal i 1 then cache_th o); + cache_function = cache_th; + subst_function = subst_th; + classify_function = (fun x -> Substitute x) } + +let field_equality evd r inv req = + match kind_of_term req with + | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) -> + mkApp(Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr,[|r;r;inv|]) + | _ -> + let _setoid = setoid_of_relation (Global.env ()) evd r req in + let signature = [Some (r,Some req)],Some(r,Some req) in + let inv_m, inv_m_lem = + try Rewrite.default_morphism signature inv + with Not_found -> + error "field inverse should be declared as a morphism" in + inv_m_lem + +let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power sign odiv = + check_required_library (cdir@["Field_tac"]); + let env = Global.env() in + let evd = ref sigma in + let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) = + dest_field env evd fth in + let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in + let eqth = Some(sth,ext) in + let _ = add_theory name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in + let (pow_tac, pspec) = interp_power env evd power in + let sspec = interp_sign env evd sign in + let dspec = interp_div env evd odiv in + let inv_m = field_equality evd r inv req in + let rk = reflect_coeff morphth in + let params,ctx = + exec_tactic env !evd 9 (field_ltac"field_lemmas") + (List.map carg[sth;ext;inv_m;fth;pspec;sspec;dspec;rk]) in + let lemma1 = params.(3) in + let lemma2 = params.(4) in + let lemma3 = params.(5) in + let lemma4 = params.(6) in + let cond_lemma = + match inj with + | Some thm -> mkApp(params.(8),[|thm|]) + | None -> params.(7) in + let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") + ctx lemma1 in + let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") + ctx lemma2 in + let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") + ctx lemma3 in + let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") + ctx lemma4 in + let cond_lemma = decl_constant (Id.to_string name^"_lemma5") + ctx cond_lemma in + let cst_tac = + interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in + let pretac = + match pre with + Some t -> Tacintern.glob_tactic t + | _ -> TacId [] in + let posttac = + match post with + Some t -> Tacintern.glob_tactic t + | _ -> TacId [] in + let _ = + Lib.add_leaf name + (ftheory_to_obj + { field_carrier = r; + field_req = req; + field_cst_tac = cst_tac; + field_pow_tac = pow_tac; + field_ok = lemma1; + field_simpl_eq_ok = lemma2; + field_simpl_ok = lemma3; + field_simpl_eq_in_ok = lemma4; + field_cond = cond_lemma; + field_pre_tac = pretac; + field_post_tac = posttac }) in () + +let process_field_mods l = + let kind = ref None in + let set = ref None in + let cst_tac = ref None in + let pre = ref None in + let post = ref None in + let inj = ref None in + let sign = ref None in + let power = ref None in + let div = ref None in + List.iter(function + Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec k) + | Ring_mod(Const_tac t) -> + set_once "tactic recognizing constants" cst_tac t + | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t + | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t + | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext) + | Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec) + | Ring_mod(Sign_spec t) -> set_once "sign" sign t + | Ring_mod(Div_spec t) -> set_once "div" div t + | Inject i -> set_once "infinite property" inj (ic_unsafe i)) l; + let k = match !kind with Some k -> k | None -> Abstract in + (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div) + +let ltac_field_structure e = + let req = carg e.field_req in + let cst_tac = Tacexp e.field_cst_tac in + let pow_tac = Tacexp e.field_pow_tac in + let field_ok = carg e.field_ok in + let field_simpl_ok = carg e.field_simpl_ok in + let field_simpl_eq_ok = carg e.field_simpl_eq_ok in + let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in + let cond_ok = carg e.field_cond in + let pretac = Tacexp(TacFun([None],e.field_pre_tac)) in + let posttac = Tacexp(TacFun([None],e.field_post_tac)) in + [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; + field_simpl_eq_in_ok;cond_ok;pretac;posttac] + +let field_lookup (f:glob_tactic_expr) lH rl t = + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + try + let evdref = ref sigma in + let rl = make_args_list rl t in + let e = find_field_structure env sigma rl in + let rl = carg (make_term_list env evdref e.field_carrier rl) in + let lH = carg (make_hyp_list env evdref lH) in + let field = ltac_field_structure e in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 deleted file mode 100644 index 72ebfae486..0000000000 --- a/plugins/setoid_ring/newring.ml4 +++ /dev/null @@ -1,1161 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* f (Evar.repr i) c - | _ -> assert false - -type protect_flag = Eval|Prot|Rec - -let tag_arg tag_rec map subs i c = - match map i with - Eval -> mk_clos subs c - | Prot -> mk_atom c - | Rec -> if Int.equal i (-1) then mk_clos subs c else tag_rec c - -let global_head_of_constr c = - let f, args = decompose_app c in - try global_of_constr f - with Not_found -> anomaly (str "global_head_of_constr") - -let global_of_constr_nofail c = - try global_of_constr c - with Not_found -> VarRef (Id.of_string "dummy") - -let rec mk_clos_but f_map subs t = - match f_map (global_of_constr_nofail t) with - | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t - | None -> - (match kind_of_term t with - App(f,args) -> mk_clos_app_but f_map subs f args 0 - | Prod _ -> mk_clos_deep (mk_clos_but f_map) subs t - | _ -> mk_atom t) - -and mk_clos_app_but f_map subs f args n = - if n >= Array.length args then mk_atom(mkApp(f, args)) - else - let fargs, args' = Array.chop n args in - let f' = mkApp(f,fargs) in - match f_map (global_of_constr_nofail f') with - Some map -> - mk_clos_deep - (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s')) - subs - (mkApp (mark_arg (-1) f', Array.mapi mark_arg args')) - | None -> mk_clos_app_but f_map subs f args (n+1) - -let interp_map l t = - try Some(List.assoc_f eq_gr t l) with Not_found -> None - -let protect_maps = ref String.Map.empty -let add_map s m = protect_maps := String.Map.add s m !protect_maps -let lookup_map map = - try String.Map.find map !protect_maps - with Not_found -> - errorlabstrm"lookup_map"(str"map "++qs map++str"not found") - -let protect_red map env sigma c = - kl (create_clos_infos betadeltaiota env) - (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);; - -let protect_tac map = - Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; - -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 = - let l = List.map Universes.constr_of_global l in - let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in - 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 []) ] -END;;*) - -(* -let closed_term_ast l = - TacFun([Some(Id.of_string"t")], - TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term", - [Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t")); - Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l]))) -*) -let closed_term_ast l = - let tacname = { - 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, - [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None); - Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l])) -(* -let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" -*) - -(****************************************************************************) - -let ic c = - let env = Global.env() and sigma = Evd.empty in - Constrintern.interp_open_constr env sigma c - -let ic_unsafe c = (*FIXME remove *) - let env = Global.env() and sigma = Evd.empty in - fst (Constrintern.interp_constr env sigma c) - -let ty c = Typing.type_of (Global.env()) Evd.empty c - -let decl_constant na ctx c = - let vars = Universes.universes_of_constr c in - let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in - mkConst(declare_constant (Id.of_string na) - (DefinitionEntry (definition_entry ~opaque:true - ~univs:(Univ.ContextSet.to_context ctx) c), - IsProof Lemma)) - -(* Calling a global tactic *) -let ltac_call tac (args:glob_tactic_arg list) = - TacArg(Loc.ghost,TacCall(Loc.ghost, ArgArg(Loc.ghost, Lazy.force tac),args)) - -(* Calling a locally bound tactic *) -let ltac_lcall tac args = - TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args)) - -let ltac_letin (x, e1) e2 = - TacLetIn(false,[(Loc.ghost,Id.of_string x),e1],e2) - -let ltac_apply (f:glob_tactic_expr) (args:glob_tactic_arg list) = - Tacinterp.eval_tactic - (ltac_letin ("F", Tacexp f) (ltac_lcall "F" args)) - -let ltac_record flds = - TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds) - - -let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c) - -let dummy_goal env sigma = - let (gl,_,sigma) = - Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in - {Evd.it = gl; Evd.sigma = sigma} - -let constr_of v = match Value.to_constr v with - | Some c -> c - | None -> failwith "Ring.exec_tactic: anomaly" - -let exec_tactic env evd n f args = - let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in - let res = ref [||] in - let get_res ist = - let l = List.map (fun id -> Id.Map.find id ist.lfun) lid in - res := Array.of_list l; - TacId[] in - let getter = - Tacexp(TacFun(List.map(fun id -> Some id) lid, - Tacintern.glob_tactic(tacticIn get_res))) in - let gl = dummy_goal env evd in - let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in - let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in - Array.map (fun x -> nf (constr_of x)) !res, Evd.universe_context evd - -let stdlib_modules = - [["Coq";"Setoids";"Setoid"]; - ["Coq";"Lists";"List"]; - ["Coq";"Init";"Datatypes"]; - ["Coq";"Init";"Logic"]; - ] - -let coq_constant c = - lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c) -let coq_reference c = - lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c) - -let coq_mk_Setoid = coq_constant "Build_Setoid_Theory" -let coq_None = coq_reference "None" -let coq_Some = coq_reference "Some" -let coq_eq = coq_constant "eq" - -let coq_cons = coq_reference "cons" -let coq_nil = coq_reference "nil" - -let lapp f args = mkApp(Lazy.force f,args) - -let plapp evd f args = - let fc = Evarutil.e_new_global evd (Lazy.force f) in - mkApp(fc,args) - -let dest_rel0 t = - match kind_of_term t with - | App(f,args) when Array.length args >= 2 -> - let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in - if closed0 rel then - (rel,args.(Array.length args - 2),args.(Array.length args - 1)) - else error "ring: cannot find relation (not closed)" - | _ -> error "ring: cannot find relation" - -let rec dest_rel t = - match kind_of_term t with - | Prod(_,_,c) -> dest_rel c - | _ -> dest_rel0 t - -(****************************************************************************) -(* Library linking *) - -let plugin_dir = "setoid_ring" - -let cdir = ["Coq";plugin_dir] -let plugin_modules = - List.map (fun d -> cdir@d) - [["Ring_theory"];["Ring_polynom"]; ["Ring_tac"];["InitialRing"]; - ["Field_tac"]; ["Field_theory"] - ] - -let my_constant c = - lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c) -let my_reference c = - lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) - -let new_ring_path = - DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"]) -let ltac s = - lazy(make_kn (MPfile new_ring_path) DirPath.empty (Label.make s)) -let znew_ring_path = - DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) -let zltac s = - lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s)) - -let mk_cst l s = lazy (Coqlib.gen_reference "newring" l s);; -let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; - -(* Ring theory *) - -(* almost_ring defs *) -let coq_almost_ring_theory = my_constant "almost_ring_theory" - -(* setoid and morphism utilities *) -let coq_eq_setoid = my_reference "Eqsth" -let coq_eq_morph = my_reference "Eq_ext" -let coq_eq_smorph = my_reference "Eq_s_ext" - -(* ring -> almost_ring utilities *) -let coq_ring_theory = my_constant "ring_theory" -let coq_mk_reqe = my_constant "mk_reqe" - -(* semi_ring -> almost_ring utilities *) -let coq_semi_ring_theory = my_constant "semi_ring_theory" -let coq_mk_seqe = my_constant "mk_seqe" - -let ltac_inv_morph_gen = zltac"inv_gen_phi" -let ltac_inv_morphZ = zltac"inv_gen_phiZ" -let ltac_inv_morphN = zltac"inv_gen_phiN" -let ltac_inv_morphNword = zltac"inv_gen_phiNword" -let coq_abstract = my_constant"Abstract" -let coq_comp = my_constant"Computational" -let coq_morph = my_constant"Morphism" - -(* morphism *) -let coq_ring_morph = my_constant "ring_morph" -let coq_semi_morph = my_constant "semi_morph" - -(* power function *) -let ltac_inv_morph_nothing = zltac"inv_morph_nothing" -let coq_pow_N_pow_N = my_constant "pow_N_pow_N" - -(* hypothesis *) -let coq_mkhypo = my_reference "mkhypo" -let coq_hypo = my_reference "hypo" - -(* Equality: do not evaluate but make recursive call on both sides *) -let map_with_eq arg_map c = - let (req,_,_) = dest_rel c in - interp_map - ((global_head_of_constr req,(function -1->Prot|_->Rec)):: - List.map (fun (c,map) -> (Lazy.force c,map)) arg_map) - -let map_without_eq arg_map _ = - interp_map (List.map (fun (c,map) -> (Lazy.force c,map)) arg_map) - -let _ = add_map "ring" - (map_with_eq - [coq_cons,(function -1->Eval|2->Rec|_->Prot); - coq_nil, (function -1->Eval|_ -> Prot); - (* Pphi_dev: evaluate polynomial and coef operations, protect - ring operations and make recursive call on the var map *) - pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); - pol_cst "Pphi_pow", - (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); - (* PEeval: evaluate morphism and polynomial, protect ring - operations and make recursive call on the var map *) - pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot)]) - -(****************************************************************************) -(* 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" -let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table" - -let ring_for_carrier r = Cmap.find r !from_carrier - -let find_ring_structure env sigma l = - match l with - | t::cl' -> - let ty = Retyping.get_type_of env sigma t in - let check c = - let ty' = Retyping.get_type_of env sigma c in - if not (Reductionops.is_conv env sigma ty ty') then - errorlabstrm "ring" - (str"arguments of ring_simplify do not have all the same type") - in - List.iter check cl'; - (try ring_for_carrier ty - with Not_found -> - errorlabstrm "ring" - (str"cannot find a declared ring structure over"++ - spc()++str"\""++pr_constr ty++str"\"")) - | [] -> assert false - -let add_entry (sp,_kn) e = - from_carrier := Cmap.add e.ring_carrier e !from_carrier; - from_name := Spmap.add sp e !from_name - - -let subst_th (subst,th) = - let c' = subst_mps subst th.ring_carrier in - let eq' = subst_mps subst th.ring_req in - let set' = subst_mps subst th.ring_setoid in - let ext' = subst_mps subst th.ring_ext in - let morph' = subst_mps subst th.ring_morph in - let th' = subst_mps subst th.ring_th in - let thm1' = subst_mps subst th.ring_lemma1 in - let thm2' = subst_mps subst th.ring_lemma2 in - let tac'= Tacsubst.subst_tactic subst th.ring_cst_tac in - let pow_tac'= Tacsubst.subst_tactic subst th.ring_pow_tac in - let pretac'= Tacsubst.subst_tactic subst th.ring_pre_tac in - let posttac'= Tacsubst.subst_tactic subst th.ring_post_tac in - if c' == th.ring_carrier && - eq' == th.ring_req && - eq_constr set' th.ring_setoid && - ext' == th.ring_ext && - morph' == th.ring_morph && - th' == th.ring_th && - thm1' == th.ring_lemma1 && - thm2' == th.ring_lemma2 && - tac' == th.ring_cst_tac && - pow_tac' == th.ring_pow_tac && - pretac' == th.ring_pre_tac && - posttac' == th.ring_post_tac then th - else - { ring_carrier = c'; - ring_req = eq'; - ring_setoid = set'; - ring_ext = ext'; - ring_morph = morph'; - ring_th = th'; - ring_cst_tac = tac'; - ring_pow_tac = pow_tac'; - ring_lemma1 = thm1'; - ring_lemma2 = thm2'; - ring_pre_tac = pretac'; - ring_post_tac = posttac' } - - -let theory_to_obj : ring_info -> obj = - let cache_th (name,th) = add_entry name th in - declare_object - {(default_object "tactic-new-ring-theory") with - open_function = (fun i o -> if Int.equal i 1 then cache_th o); - cache_function = cache_th; - subst_function = subst_th; - classify_function = (fun x -> Substitute x)} - - -let setoid_of_relation env evd a r = - try - let evm = !evd in - let evm, refl = Rewrite.get_reflexive_proof env evm a r in - let evm, sym = Rewrite.get_symmetric_proof env evm a r in - let evm, trans = Rewrite.get_transitive_proof env evm a r in - evd := evm; - lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |] - with Not_found -> - error "cannot find setoid relation" - -let op_morph r add mul opp req m1 m2 m3 = - lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |] - -let op_smorph r add mul req m1 m2 = - lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |] - -(* let default_ring_equality (r,add,mul,opp,req) = *) -(* let is_setoid = function *) -(* {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *) -(* eq_constr_nounivs req rel (\* Qu: use conversion ? *\) *) -(* | _ -> false in *) -(* match default_relation_for_carrier ~filter:is_setoid r with *) -(* Leibniz _ -> *) -(* let setoid = lapp coq_eq_setoid [|r|] in *) -(* let op_morph = *) -(* match opp with *) -(* Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] *) -(* | None -> lapp coq_eq_smorph [|r;add;mul|] in *) -(* (setoid,op_morph) *) -(* | Relation rel -> *) -(* let setoid = setoid_of_relation rel in *) -(* let is_endomorphism = function *) -(* { args=args } -> List.for_all *) -(* (function (var,Relation rel) -> *) -(* var=None && eq_constr_nounivs req rel *) -(* | _ -> false) args in *) -(* let add_m = *) -(* try default_morphism ~filter:is_endomorphism add *) -(* with Not_found -> *) -(* error "ring addition should be declared as a morphism" in *) -(* let mul_m = *) -(* try default_morphism ~filter:is_endomorphism mul *) -(* with Not_found -> *) -(* error "ring multiplication should be declared as a morphism" in *) -(* let op_morph = *) -(* match opp with *) -(* | Some opp -> *) -(* (let opp_m = *) -(* try default_morphism ~filter:is_endomorphism opp *) -(* with Not_found -> *) -(* error "ring opposite should be declared as a morphism" in *) -(* let op_morph = *) -(* op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in *) -(* msgnl *) -(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++ *) -(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *) -(* str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ *) -(* str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ *) -(* str"\""); *) -(* op_morph) *) -(* | None -> *) -(* (msgnl *) -(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ *) -(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *) -(* str"\""++spc()++str"and \""++ *) -(* pr_constr mul_m.morphism_theory++str"\""); *) -(* op_smorph r add mul req add_m.lem mul_m.lem) in *) -(* (setoid,op_morph) *) - -let ring_equality env evd (r,add,mul,opp,req) = - match kind_of_term req with - | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) -> - let setoid = plapp evd coq_eq_setoid [|r|] in - let op_morph = - match opp with - Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|] - | None -> plapp evd coq_eq_smorph [|r;add;mul|] in - let setoid = Typing.solve_evars env evd setoid in - let op_morph = Typing.solve_evars env evd op_morph in - (setoid,op_morph) - | _ -> - let setoid = setoid_of_relation (Global.env ()) evd r req in - let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in - let add_m, add_m_lem = - try Rewrite.default_morphism signature add - with Not_found -> - error "ring addition should be declared as a morphism" in - let mul_m, mul_m_lem = - try Rewrite.default_morphism signature mul - with Not_found -> - error "ring multiplication should be declared as a morphism" in - let op_morph = - match opp with - | Some opp -> - (let opp_m,opp_m_lem = - try Rewrite.default_morphism ([Some(r,Some req)],Some(r,Some req)) opp - with Not_found -> - error "ring opposite should be declared as a morphism" in - let op_morph = - op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in - Flags.if_verbose - msg_info - (str"Using setoid \""++pr_constr req++str"\""++spc()++ - str"and morphisms \""++pr_constr add_m_lem ++ - str"\","++spc()++ str"\""++pr_constr mul_m_lem++ - str"\""++spc()++str"and \""++pr_constr opp_m_lem++ - str"\""); - op_morph) - | None -> - (Flags.if_verbose - msg_info - (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ - str"and morphisms \""++pr_constr add_m_lem ++ - str"\""++spc()++str"and \""++ - pr_constr mul_m_lem++str"\""); - op_smorph r add mul req add_m_lem mul_m_lem) in - (setoid,op_morph) - -let build_setoid_params env evd r add mul opp req eqth = - match eqth with - Some th -> th - | None -> ring_equality env evd (r,add,mul,opp,req) - -let dest_ring env sigma th_spec = - let th_typ = Retyping.get_type_of env sigma th_spec in - match kind_of_term th_typ with - App(f,[|r;zero;one;add;mul;sub;opp;req|]) - when eq_constr_nounivs f (Lazy.force coq_almost_ring_theory) -> - (None,r,zero,one,add,mul,Some sub,Some opp,req) - | App(f,[|r;zero;one;add;mul;req|]) - when eq_constr_nounivs f (Lazy.force coq_semi_ring_theory) -> - (Some true,r,zero,one,add,mul,None,None,req) - | App(f,[|r;zero;one;add;mul;sub;opp;req|]) - when eq_constr_nounivs f (Lazy.force coq_ring_theory) -> - (Some false,r,zero,one,add,mul,Some sub,Some opp,req) - | _ -> error "bad ring structure" - - -let dest_morph env sigma m_spec = - let m_typ = Retyping.get_type_of env sigma m_spec in - match kind_of_term m_typ with - App(f,[|r;zero;one;add;mul;sub;opp;req; - c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) - when eq_constr_nounivs f (Lazy.force coq_ring_morph) -> - (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi) - | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|]) - when eq_constr_nounivs f (Lazy.force coq_semi_morph) -> - (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 - Abstract -> Lazy.force coq_abstract - | 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 - | Some (Closed lc) -> - closed_term_ast (List.map Smartlocate.global_with_alias lc) - | None -> - let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morph_nothing) in - TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])) - -let make_hyp env evd c = - let t = Retyping.get_type_of env !evd c in - plapp evd coq_mkhypo [|t;c|] - -let make_hyp_list env evd lH = - let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in - let l = - List.fold_right - (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH - (plapp evd coq_nil [|carrier|]) - in - let l' = Typing.solve_evars env evd l in - Evarutil.nf_evars_universes !evd l' - -let interp_power env evd pow = - let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in - match pow with - | None -> - let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in - (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), plapp evd coq_None [|carrier|]) - | Some (tac, spec) -> - let tac = - match tac with - | CstTac t -> Tacintern.glob_tactic t - | Closed lc -> - closed_term_ast (List.map Smartlocate.global_with_alias lc) in - let spec = make_hyp env evd (ic_unsafe spec) in - (tac, plapp evd coq_Some [|carrier; spec|]) - -let interp_sign env evd sign = - let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in - match sign with - | None -> plapp evd coq_None [|carrier|] - | Some spec -> - let spec = make_hyp env evd (ic_unsafe spec) in - plapp evd coq_Some [|carrier;spec|] - (* Same remark on ill-typed terms ... *) - -let interp_div env evd div = - let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in - match div with - | None -> plapp evd coq_None [|carrier|] - | Some spec -> - let spec = make_hyp env evd (ic_unsafe spec) in - plapp evd coq_Some [|carrier;spec|] - (* Same remark on ill-typed terms ... *) - -let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div = - check_required_library (cdir@["Ring_base"]); - let env = Global.env() in - let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in - let evd = ref sigma in - let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in - let (pow_tac, pspec) = interp_power env evd power in - let sspec = interp_sign env evd sign in - let dspec = interp_div env evd div in - let rk = reflect_coeff morphth in - let params,ctx = - exec_tactic env !evd 5 (zltac "ring_lemmas") - (List.map carg[sth;ext;rth;pspec;sspec;dspec;rk]) in - let lemma1 = params.(3) in - let lemma2 = params.(4) in - - let lemma1 = - decl_constant (Id.to_string name^"_ring_lemma1") ctx lemma1 in - let lemma2 = - decl_constant (Id.to_string name^"_ring_lemma2") ctx lemma2 in - let cst_tac = - interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in - let pretac = - match pre with - Some t -> Tacintern.glob_tactic t - | _ -> TacId [] in - let posttac = - match post with - Some t -> Tacintern.glob_tactic t - | _ -> TacId [] in - let _ = - Lib.add_leaf name - (theory_to_obj - { ring_carrier = r; - ring_req = req; - ring_setoid = sth; - ring_ext = params.(1); - ring_morph = params.(2); - ring_th = params.(0); - ring_cst_tac = cst_tac; - ring_pow_tac = pow_tac; - ring_lemma1 = lemma1; - ring_lemma2 = lemma2; - ring_pre_tac = pretac; - 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") - -let process_ring_mods l = - let kind = ref None in - let set = ref None in - let cst_tac = ref None in - let pre = ref None in - let post = ref None in - let sign = ref None in - let power = ref None in - let div = ref None in - List.iter(function - Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec k) - | Const_tac t -> set_once "tactic recognizing constants" cst_tac t - | Pre_tac t -> set_once "preprocess tactic" pre t - | Post_tac t -> set_once "postprocess tactic" post t - | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext) - | Pow_spec(t,spec) -> set_once "power" power (t,spec) - | Sign_spec t -> set_once "sign" sign t - | Div_spec t -> set_once "div" div t) 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. *) - -let make_args_list rl t = - match rl with - | [] -> let (_,t1,t2) = dest_rel0 t in [t1;t2] - | _ -> rl - -let make_term_list env evd carrier rl = - let l = List.fold_right - (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl - (plapp evd coq_nil [|carrier|]) - in Typing.solve_evars env evd l - -let ltac_ring_structure e = - let req = carg e.ring_req in - let sth = carg e.ring_setoid in - let ext = carg e.ring_ext in - let morph = carg e.ring_morph in - let th = carg e.ring_th in - let cst_tac = Tacexp e.ring_cst_tac in - let pow_tac = Tacexp e.ring_pow_tac in - let lemma1 = carg e.ring_lemma1 in - let lemma2 = carg e.ring_lemma2 in - let pretac = Tacexp(TacFun([None],e.ring_pre_tac)) in - let posttac = Tacexp(TacFun([None],e.ring_post_tac)) in - [req;sth;ext;morph;th;cst_tac;pow_tac; - lemma1;lemma2;pretac;posttac] - -let ring_lookup (f:glob_tactic_expr) lH rl t = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - let env = Proofview.Goal.env gl in - try (* find_ring_strucure can raise an exception *) - let evdref = ref sigma in - let rl = make_args_list rl t in - let e = find_ring_structure env sigma rl in - let rl = carg (make_term_list env evdref e.ring_carrier rl) in - let lH = carg (make_hyp_list env evdref lH) in - let ring = ltac_ring_structure e in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl])) - 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 = - DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"]) - -let field_ltac s = - lazy(make_kn (MPfile new_field_path) DirPath.empty (Label.make s)) - - -let _ = add_map "field" - (map_with_eq - [coq_cons,(function -1->Eval|2->Rec|_->Prot); - coq_nil, (function -1->Eval|_ -> Prot); - (* display_linear: evaluate polynomials and coef operations, protect - field operations and make recursive call on the var map *) - my_reference "display_linear", - (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot); - my_reference "display_pow_linear", - (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot); - (* Pphi_dev: evaluate polynomial and coef operations, protect - ring operations and make recursive call on the var map *) - pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); - pol_cst "Pphi_pow", - (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); - (* PEeval: evaluate morphism and polynomial, protect ring - operations and make recursive call on the var map *) - pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot); - (* FEeval: evaluate morphism, protect field - operations and make recursive call on the var map *) - my_reference "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);; - -let _ = add_map "field_cond" - (map_without_eq - [coq_cons,(function -1->Eval|2->Rec|_->Prot); - coq_nil, (function -1->Eval|_ -> Prot); - (* PCond: evaluate morphism and denum list, protect ring - operations and make recursive call on the var map *) - my_reference "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);; -(* (function -1|9|11->Eval|10->Rec|_->Prot)]);;*) - - -let _ = Redexpr.declare_reduction "simpl_field_expr" - (protect_red "field") - - - -let afield_theory = my_reference "almost_field_theory" -let field_theory = my_reference "field_theory" -let sfield_theory = my_reference "semi_field_theory" -let af_ar = my_reference"AF_AR" -let f_r = my_reference"F_R" -let sf_sr = my_reference"SF_SR" -let dest_field env evd th_spec = - let th_typ = Retyping.get_type_of env !evd th_spec in - match kind_of_term th_typ with - | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when is_global (Lazy.force afield_theory) f -> - let rth = plapp evd af_ar - [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in - (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) - | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when is_global (Lazy.force field_theory) f -> - let rth = - plapp evd f_r - [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in - (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) - | App(f,[|r;zero;one;add;mul;div;inv;req|]) - when is_global (Lazy.force sfield_theory) f -> - let rth = plapp evd sf_sr - [|r;zero;one;add;mul;div;inv;req;th_spec|] in - (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" - -let field_for_carrier r = Cmap.find r !field_from_carrier - -let find_field_structure env sigma l = - check_required_library (cdir@["Field_tac"]); - match l with - | t::cl' -> - let ty = Retyping.get_type_of env sigma t in - let check c = - let ty' = Retyping.get_type_of env sigma c in - if not (Reductionops.is_conv env sigma ty ty') then - errorlabstrm "field" - (str"arguments of field_simplify do not have all the same type") - in - List.iter check cl'; - (try field_for_carrier ty - with Not_found -> - errorlabstrm "field" - (str"cannot find a declared field structure over"++ - spc()++str"\""++pr_constr ty++str"\"")) - | [] -> assert false - -let add_field_entry (sp,_kn) e = - field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier; - field_from_name := Spmap.add sp e !field_from_name - -let subst_th (subst,th) = - let c' = subst_mps subst th.field_carrier in - let eq' = subst_mps subst th.field_req in - let thm1' = subst_mps subst th.field_ok in - let thm2' = subst_mps subst th.field_simpl_eq_ok in - let thm3' = subst_mps subst th.field_simpl_ok in - let thm4' = subst_mps subst th.field_simpl_eq_in_ok in - let thm5' = subst_mps subst th.field_cond in - let tac'= Tacsubst.subst_tactic subst th.field_cst_tac in - let pow_tac' = Tacsubst.subst_tactic subst th.field_pow_tac in - let pretac'= Tacsubst.subst_tactic subst th.field_pre_tac in - let posttac'= Tacsubst.subst_tactic subst th.field_post_tac in - if c' == th.field_carrier && - eq' == th.field_req && - thm1' == th.field_ok && - thm2' == th.field_simpl_eq_ok && - thm3' == th.field_simpl_ok && - thm4' == th.field_simpl_eq_in_ok && - thm5' == th.field_cond && - tac' == th.field_cst_tac && - pow_tac' == th.field_pow_tac && - pretac' == th.field_pre_tac && - posttac' == th.field_post_tac then th - else - { field_carrier = c'; - field_req = eq'; - field_cst_tac = tac'; - field_pow_tac = pow_tac'; - field_ok = thm1'; - field_simpl_eq_ok = thm2'; - field_simpl_ok = thm3'; - field_simpl_eq_in_ok = thm4'; - field_cond = thm5'; - field_pre_tac = pretac'; - field_post_tac = posttac' } - -let ftheory_to_obj : field_info -> obj = - let cache_th (name,th) = add_field_entry name th in - declare_object - {(default_object "tactic-new-field-theory") with - open_function = (fun i o -> if Int.equal i 1 then cache_th o); - cache_function = cache_th; - subst_function = subst_th; - classify_function = (fun x -> Substitute x) } - -let field_equality evd r inv req = - match kind_of_term req with - | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) -> - mkApp(Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr,[|r;r;inv|]) - | _ -> - let _setoid = setoid_of_relation (Global.env ()) evd r req in - let signature = [Some (r,Some req)],Some(r,Some req) in - let inv_m, inv_m_lem = - try Rewrite.default_morphism signature inv - with Not_found -> - error "field inverse should be declared as a morphism" in - inv_m_lem - -let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power sign odiv = - check_required_library (cdir@["Field_tac"]); - let env = Global.env() in - let evd = ref sigma in - let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) = - dest_field env evd fth in - let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in - let eqth = Some(sth,ext) in - let _ = add_theory name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in - let (pow_tac, pspec) = interp_power env evd power in - let sspec = interp_sign env evd sign in - let dspec = interp_div env evd odiv in - let inv_m = field_equality evd r inv req in - let rk = reflect_coeff morphth in - let params,ctx = - exec_tactic env !evd 9 (field_ltac"field_lemmas") - (List.map carg[sth;ext;inv_m;fth;pspec;sspec;dspec;rk]) in - let lemma1 = params.(3) in - let lemma2 = params.(4) in - let lemma3 = params.(5) in - let lemma4 = params.(6) in - let cond_lemma = - match inj with - | Some thm -> mkApp(params.(8),[|thm|]) - | None -> params.(7) in - let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") - ctx lemma1 in - let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") - ctx lemma2 in - let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") - ctx lemma3 in - let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") - ctx lemma4 in - let cond_lemma = decl_constant (Id.to_string name^"_lemma5") - ctx cond_lemma in - let cst_tac = - interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in - let pretac = - match pre with - Some t -> Tacintern.glob_tactic t - | _ -> TacId [] in - let posttac = - match post with - Some t -> Tacintern.glob_tactic t - | _ -> TacId [] in - let _ = - Lib.add_leaf name - (ftheory_to_obj - { field_carrier = r; - field_req = req; - field_cst_tac = cst_tac; - field_pow_tac = pow_tac; - field_ok = lemma1; - field_simpl_eq_ok = lemma2; - field_simpl_ok = lemma3; - field_simpl_eq_in_ok = lemma4; - field_cond = cond_lemma; - 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 - let cst_tac = ref None in - let pre = ref None in - let post = ref None in - let inj = ref None in - let sign = ref None in - let power = ref None in - let div = ref None in - List.iter(function - Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec k) - | Ring_mod(Const_tac t) -> - set_once "tactic recognizing constants" cst_tac t - | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t - | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t - | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext) - | Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec) - | Ring_mod(Sign_spec t) -> set_once "sign" sign t - | Ring_mod(Div_spec t) -> set_once "div" div t - | Inject i -> set_once "infinite property" inj (ic_unsafe i)) 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 - let pow_tac = Tacexp e.field_pow_tac in - let field_ok = carg e.field_ok in - let field_simpl_ok = carg e.field_simpl_ok in - let field_simpl_eq_ok = carg e.field_simpl_eq_ok in - let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in - let cond_ok = carg e.field_cond in - let pretac = Tacexp(TacFun([None],e.field_pre_tac)) in - let posttac = Tacexp(TacFun([None],e.field_post_tac)) in - [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; - field_simpl_eq_in_ok;cond_ok;pretac;posttac] - -let field_lookup (f:glob_tactic_expr) lH rl t = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - let env = Proofview.Goal.env gl in - try - let evdref = ref sigma in - let rl = make_args_list rl t in - let e = find_field_structure env sigma rl in - let rl = carg (make_term_list env evdref e.field_carrier rl) in - let lH = carg (make_hyp_list env evdref lH) in - let field = ltac_field_structure e in - 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 *) +(* 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 *) +(*