diff options
Diffstat (limited to 'contrib/setoid_ring/newring.ml4')
| -rw-r--r-- | contrib/setoid_ring/newring.ml4 | 1009 |
1 files changed, 719 insertions, 290 deletions
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index bc2bcb0c..daa2fedb 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: newring.ml4 8878 2006-05-30 16:44:25Z herbelin $ i*) +(*i $Id: newring.ml4 9302 2006-10-27 21:21:17Z barras $ i*) open Pp open Util @@ -16,6 +16,7 @@ open Names open Term open Closure open Environ +open Libnames open Tactics open Rawterm open Tacticals @@ -27,139 +28,53 @@ open Setoid_replace open Proof_type open Coqlib open Tacmach -open Ppconstr open Mod_subst open Tacinterp open Libobject open Printer - -(****************************************************************************) -(* Library linking *) - -let contrib_name = "setoid_ring" - - -let ring_dir = ["Coq";contrib_name] -let setoids_dir = ["Coq";"Setoids"] -let ring_modules = - [ring_dir@["BinList"];ring_dir@["Ring_th"];ring_dir@["Pol"]; - ring_dir@["Ring_tac"];ring_dir@["ZRing_th"]] -let stdlib_modules = [setoids_dir@["Setoid"]] - -let coq_constant c = - lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c) -let ring_constant c = - lazy (Coqlib.gen_constant_in_modules "Ring" ring_modules c) -let ringtac_constant m c = - lazy (Coqlib.gen_constant_in_modules "Ring" [ring_dir@["ZRing_th";m]] c) - -let new_ring_path = - make_dirpath (List.map id_of_string ["Ring_tac";contrib_name;"Coq"]) -let ltac s = - lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s)) -let znew_ring_path = - make_dirpath (List.map id_of_string ["ZRing_th";contrib_name;"Coq"]) -let zltac s = - lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s)) -let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c) - -let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);; -let pol_cst s = mk_cst [contrib_name;"Pol"] s ;; - -let ic c = - let env = Global.env() and sigma = Evd.empty in - Constrintern.interp_constr sigma env c - - -(* Ring theory *) - -(* almost_ring defs *) -let coq_almost_ring_theory = ring_constant "almost_ring_theory" -let coq_ring_lemma1 = ring_constant "ring_correct" -let coq_ring_lemma2 = ring_constant "Pphi_dev_ok'" -let ring_comp1 = ring_constant "ring_id_correct" -let ring_comp2 = ring_constant "ring_rw_id_correct'" -let ring_abs1 = ringtac_constant "Zpol" "ring_gen_correct" -let ring_abs2 = ringtac_constant "Zpol" "ring_rw_gen_correct'" -let sring_abs1 = ringtac_constant "Npol" "ring_gen_correct" -let sring_abs2 = ringtac_constant "Npol" "ring_rw_gen_correct'" - -(* setoid and morphism utilities *) -let coq_mk_Setoid = coq_constant "Build_Setoid_Theory" -let coq_eq_setoid = ring_constant "Eqsth" -let coq_eq_morph = ring_constant "Eq_ext" - -(* ring -> almost_ring utilities *) -let coq_ring_theory = ring_constant "ring_theory" -let coq_ring_morph = ring_constant "ring_morph" -let coq_Rth_ARth = ring_constant "Rth_ARth" -let coq_mk_reqe = ring_constant "mk_reqe" - -(* semi_ring -> almost_ring utilities *) -let coq_semi_ring_theory = ring_constant "semi_ring_theory" -let coq_SRth_ARth = ring_constant "SRth_ARth" -let coq_sring_morph = ring_constant "semi_morph" -let coq_SRmorph_Rmorph = ring_constant "SRmorph_Rmorph" -let coq_mk_seqe = ring_constant "mk_seqe" -let coq_SRsub = ring_constant "SRsub" -let coq_SRopp = ring_constant "SRopp" -let coq_SReqe_Reqe = ring_constant "SReqe_Reqe" - -let ltac_setoid_ring = ltac"Make_ring_tac" -let ltac_setoid_ring_rewrite = ltac"Make_ring_rw_list" -let ltac_inv_morphZ = zltac"inv_gen_phiZ" -let ltac_inv_morphN = zltac"inv_gen_phiN" - -let coq_cons = ring_constant "cons" -let coq_nil = ring_constant "nil" - -let lapp f args = mkApp(Lazy.force f,args) - -let dest_rel t = - match kind_of_term t with - App(f,args) when Array.length args >= 2 -> - mkApp(f,Array.sub args 0 (Array.length args - 2)) - | _ -> failwith "cannot find relation" +open Declare +open Decl_kinds +open Entries (****************************************************************************) (* controlled reduction *) -let mark_arg i c = mkEvar(i,[|c|]);; +let mark_arg i c = mkEvar(i,[|c|]) let unmark_arg f c = match destEvar c with | (i,[|c|]) -> f i c - | _ -> assert false;; + | _ -> assert false -type protect_flag = Eval|Prot|Rec ;; +type protect_flag = Eval|Prot|Rec -let tag_arg tag_rec map i c = +let tag_arg tag_rec map subs i c = match map i with - Eval -> inject c + Eval -> mk_clos subs c | Prot -> mk_atom c - | Rec -> if i = -1 then inject c else tag_rec c + | Rec -> if i = -1 then mk_clos subs c else tag_rec c -let rec mk_clos_but f_map t = +let rec mk_clos_but f_map subs t = match f_map t with - | Some map -> tag_arg (mk_clos_but f_map) map (-1) t + | 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 f args 0 - (* unspecified constants are evaluated *) - | _ -> inject t) + 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 f args n = - if n >= Array.length args then inject(mkApp(f, args)) +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 f' with Some map -> mk_clos_deep - (fun _ -> unmark_arg (tag_arg (mk_clos_but f_map) map)) - (Esubst.ESID 0) + (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 f args (n+1) -;; + | None -> mk_clos_app_but f_map subs f args (n+1) + let interp_map l c = try @@ -174,98 +89,320 @@ let interp_map l c = let interp_map l t = try Some(List.assoc t l) with Not_found -> None -let arg_map = - [mk_cst [contrib_name;"BinList"] "cons",(function -1->Eval|2->Rec|_->Prot); - mk_cst [contrib_name;"BinList"] "nil", (function -1->Eval|_ -> Prot); - (* Pphi_dev: evaluate polynomial and coef operations, protect - ring operations and make recursive call on morphism and var map *) - pol_cst "Pphi_dev", (function -1|6|7|8|11->Eval|9|10->Rec|_->Prot); - (* PEeval: evaluate polynomial, protect ring operations - and make recursive call on morphism and var map *) - pol_cst "PEeval", (function -1|9->Eval|7|8->Rec|_->Prot); - (* Do not evaluate ring operations... *) - ring_constant "gen_phiZ", (function -1|6->Eval|_->Prot); - ring_constant "gen_phiN", (function -1|5->Eval|_->Prot); -];; +let protect_maps = ref ([]:(string*(constr->'a)) list) +let add_map s m = protect_maps := (s,m) :: !protect_maps +let lookup_map map = + try List.assoc map !protect_maps + with Not_found -> + errorlabstrm"lookup_map"(str"map "++qs map++str"not found") -(* Equality: do not evaluate but make recursive call on both sides *) -let is_ring_thm req = - interp_map - ((req,(function -1->Prot|_->Rec)):: - List.map (fun (c,map) -> (Lazy.force c,map)) arg_map) -;; - -let protect_red env sigma c = - let req = dest_rel c in +let protect_red map env sigma c = kl (create_clos_infos betadeltaiota env) - (mk_clos_but (is_ring_thm req) c);; + (mk_clos_but (lookup_map map c) (Esubst.ESID 0) c);; -let protect_tac = - Tactics.reduct_option (protect_red,DEFAULTcast) None ;; +let protect_tac map = + Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; -let protect_tac_in id = - Tactics.reduct_option (protect_red,DEFAULTcast) (Some(([],id),InHyp));; +let protect_tac_in map id = + Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(([],id),InHyp));; TACTIC EXTEND protect_fv - [ "protect_fv" "in" ident(id) ] -> - [ protect_tac_in id ] -| [ "protect_fv" ] -> - [ protect_tac ] + [ "protect_fv" string(map) "in" ident(id) ] -> + [ protect_tac_in map id ] +| [ "protect_fv" string(map) ] -> + [ protect_tac map ] END;; (****************************************************************************) -(* Ring database *) + +let closed_term t l = + let l = List.map 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) "]" ] -> + [ closed_term t l ] +END +;; +(* +let closed_term_ast l = + TacFun([Some(id_of_string"t")], + TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term", + [Genarg.in_gen Genarg.wit_constr (mkVar(id_of_string"t")); + Genarg.in_gen (Genarg.wit_list1 Genarg.wit_ref) l]))) +*) +let closed_term_ast l = + let l = List.map (fun gr -> ArgArg(dummy_loc,gr)) l in + TacFun([Some(id_of_string"t")], + TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term", + [Genarg.in_gen Genarg.globwit_constr (RVar(dummy_loc,id_of_string"t"),None); + Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l]))) +(* +let _ = add_tacdef false ((dummy_loc,id_of_string"ring_closed_term" +*) + +(****************************************************************************) + +let ic c = + let env = Global.env() and sigma = Evd.empty in + Constrintern.interp_constr sigma env c let ty c = Typing.type_of (Global.env()) Evd.empty c +let decl_constant na c = + mkConst(declare_constant (id_of_string na) (DefinitionEntry + { const_entry_body = c; + const_entry_type = None; + const_entry_opaque = true; + const_entry_boxed = true}, + IsProof Lemma)) + +let ltac_call tac args = + TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)) + +let ltac_lcall tac args = + TacArg(TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args)) + +let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c) + +let dummy_goal env = + {Evd.it= + {Evd.evar_concl=mkProp; + Evd.evar_hyps=named_context_val env; + Evd.evar_body=Evd.Evar_empty; + Evd.evar_extra=None}; + Evd.sigma=Evd.empty} + +let exec_tactic env n f args = + let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in + let res = ref [||] in + let get_res ist = + let l = List.map (fun id -> List.assoc id ist.lfun) lid in + res := Array.of_list l; + TacId[] in + let getter = + Tacexp(TacFun(List.map(fun id -> Some id) lid, + glob_tactic(tacticIn get_res))) in + let _ = + Tacinterp.eval_tactic(ltac_call f (args@[getter])) (dummy_goal env) in + !res + +let constr_of = function + | VConstr c -> c + | _ -> failwith "Ring.exec_tactic: anomaly" + +let stdlib_modules = + [["Coq";"Setoids";"Setoid"]; + ["Coq";"Lists";"List"] + ] + +let coq_constant c = + lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c) + +let coq_mk_Setoid = coq_constant "Build_Setoid_Theory" +let coq_cons = coq_constant "cons" +let coq_nil = coq_constant "nil" + +let lapp f args = mkApp(Lazy.force f,args) + +let rec dest_rel 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)" + | Prod(_,_,c) -> dest_rel c + | _ -> error "ring: cannot find relation" + +(****************************************************************************) +(* Library linking *) + +let contrib_name = "setoid_ring" + +let cdir = ["Coq";contrib_name] +let contrib_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" contrib_modules c) + +let new_ring_path = + make_dirpath (List.map id_of_string ["Ring_tac";contrib_name;"Coq"]) +let ltac s = + lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s)) +let znew_ring_path = + make_dirpath (List.map id_of_string ["InitialRing";contrib_name;"Coq"]) +let zltac s = + lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s)) + +let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);; +let pol_cst s = mk_cst [contrib_name;"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_constant "Eqsth" +let coq_eq_morph = my_constant "Eq_ext" +let coq_eq_smorph = my_constant "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_morphZ = zltac"inv_gen_phiZ" +let ltac_inv_morphN = zltac"inv_gen_phiN" + +let coq_abstract = my_constant"Abstract" +let coq_comp = my_constant"Computational" +let coq_morph = my_constant"Morphism" + +(* 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 + ((req,(function -1->Prot|_->Rec)):: + 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|6|7|8|9|11->Eval|10->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->Eval|8->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_lemma1 : constr; - ring_lemma2 : constr } + ring_lemma2 : constr; + ring_pre_tac : glob_tactic_expr; + ring_post_tac : glob_tactic_expr } module Cmap = Map.Make(struct type t = constr let compare = compare end) let from_carrier = ref Cmap.empty let from_relation = ref Cmap.empty +let from_name = ref Spmap.empty + +let ring_for_carrier r = Cmap.find r !from_carrier +let ring_for_relation rel = Cmap.find rel !from_relation +let ring_lookup_by_name ref = + Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref))) !from_name + + +let find_ring_structure env sigma l cl oname = + match oname, l with + Some rf, _ -> + (try ring_lookup_by_name rf + with Not_found -> + errorlabstrm "ring" + (str "found no ring named "++pr_reference rf)) + | None, 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"\"")) + | None, [] -> + let (req,_,_) = dest_rel cl in + (try ring_for_relation req + with Not_found -> + errorlabstrm "ring" + (str"cannot find a declared ring structure for equality"++ + spc()++str"\""++pr_constr req++str"\"")) let _ = Summary.declare_summary "tactic-new-ring-table" - { Summary.freeze_function = (fun () -> !from_carrier,!from_relation); + { Summary.freeze_function = + (fun () -> !from_carrier,!from_relation,!from_name); Summary.unfreeze_function = - (fun (ct,rt) -> from_carrier := ct; from_relation := rt); + (fun (ct,rt,nt) -> + from_carrier := ct; from_relation := rt; from_name := nt); Summary.init_function = - (fun () -> from_carrier := Cmap.empty; from_relation := Cmap.empty); + (fun () -> + from_carrier := Cmap.empty; from_relation := Cmap.empty; + from_name := Spmap.empty); Summary.survive_module = false; Summary.survive_section = false } -let add_entry _ e = - let _ = ty e.ring_lemma1 in +let add_entry (sp,_kn) e = +(* let _ = ty e.ring_lemma1 in let _ = ty e.ring_lemma2 in +*) from_carrier := Cmap.add e.ring_carrier e !from_carrier; - from_relation := Cmap.add e.ring_req e !from_relation + from_relation := Cmap.add e.ring_req e !from_relation; + 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'= subst_tactic subst th.ring_cst_tac in + let pretac'= subst_tactic subst th.ring_pre_tac in + let posttac'= subst_tactic subst th.ring_post_tac in if c' == th.ring_carrier && eq' == th.ring_req && + 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 then th + tac' == th.ring_cst_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_lemma1 = thm1'; - ring_lemma2 = thm2' } + ring_lemma2 = thm2'; + ring_pre_tac = pretac'; + ring_post_tac = posttac' } let (theory_to_obj, obj_to_theory) = @@ -280,10 +417,6 @@ let (theory_to_obj, obj_to_theory) = export_function = export_th } -let ring_for_carrier r = Cmap.find r !from_carrier - -let ring_for_relation rel = Cmap.find rel !from_relation - let setoid_of_relation r = lapp coq_mk_Setoid [|r.rel_a; r.rel_aeq; @@ -293,43 +426,19 @@ 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_SReqe_Reqe - [| r;add;mul;req;lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]|] - -let sr_sub r add = lapp coq_SRsub [|r;add|] -let sr_opp r = lapp coq_SRopp [|r|] + lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |] -let dest_morphism kind th sth = - let th_typ = Retyping.get_type_of (Global.env()) Evd.empty th in - match kind_of_term th_typ with - App(f,[|_;_;_;_;_;_;_;_;c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) - when f = Lazy.force coq_ring_morph -> - (th,[|c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) - | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|]) - when f = Lazy.force coq_sring_morph && kind=Some true-> - let th = - lapp coq_SRmorph_Rmorph - [|r;zero;one;add;mul;req;sth;c;czero;cone;cadd;cmul;ceqb;phi;th|]in - (th,[|c;czero;cone;cadd;cmul;cadd;sr_opp c;ceqb;phi|]) - | _ -> failwith "bad ring_morph lemma" - -let dest_eq_test th = - let th_typ = Retyping.get_type_of (Global.env()) Evd.empty th in - match decompose_prod th_typ with - (_,h)::_,_ -> - (match snd(destApplication h) with - [|_;lhs;_|] -> fst(destApplication lhs) - | _ -> failwith "bad lemma for decidability of equality") - | _ -> failwith "bad lemma for decidability of equality" - -let default_ring_equality is_semi (r,add,mul,opp,req) = +let default_ring_equality (r,add,mul,opp,req) = let is_setoid = function {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _} -> true | _ -> false in match default_relation_for_carrier ~filter:is_setoid r with Leibniz _ -> let setoid = lapp coq_eq_setoid [|r|] in - let op_morph = lapp coq_eq_morph [|r;add;mul;opp|] 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 @@ -347,8 +456,12 @@ let default_ring_equality is_semi (r,add,mul,opp,req) = with Not_found -> error "ring multiplication should be declared as a morphism" in let op_morph = - if is_semi <> Some true then - (let opp_m = default_morphism ~filter:is_endomorphism opp in + 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 @@ -358,7 +471,7 @@ let default_ring_equality is_semi (r,add,mul,opp,req) = str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ str"\""); op_morph) - else + | None -> (msgnl (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ str"and morphisms \""++pr_constr add_m.morphism_theory++ @@ -367,159 +480,475 @@ let default_ring_equality is_semi (r,add,mul,opp,req) = op_smorph r add mul req add_m.lem mul_m.lem) in (setoid,op_morph) -let build_setoid_params is_semi r add mul opp req eqth = +let build_setoid_params r add mul opp req eqth = match eqth with Some th -> th - | None -> default_ring_equality is_semi (r,add,mul,opp,req) + | None -> default_ring_equality (r,add,mul,opp,req) -let dest_ring th_spec = - let th_typ = Retyping.get_type_of (Global.env()) Evd.empty th_spec in +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 f = Lazy.force coq_almost_ring_theory -> - (None,r,zero,one,add,mul,sub,opp,req) + (None,r,zero,one,add,mul,Some sub,Some opp,req) | App(f,[|r;zero;one;add;mul;req|]) when f = Lazy.force coq_semi_ring_theory -> - (Some true,r,zero,one,add,mul,sr_sub r add,sr_opp r,req) + (Some true,r,zero,one,add,mul,None,None,req) | App(f,[|r;zero;one;add;mul;sub;opp;req|]) when f = Lazy.force coq_ring_theory -> - (Some false,r,zero,one,add,mul,sub,opp,req) + (Some false,r,zero,one,add,mul,Some sub,Some opp,req) | _ -> error "bad ring structure" -let build_almost_ring kind r zero one add mul sub opp req sth morph th = - match kind with - None -> th - | Some true -> - lapp coq_SRth_ARth [|r;zero;one;add;mul;req;sth;th|] - | Some false -> - lapp coq_Rth_ARth [|r;zero;one;add;mul;sub;opp;req;sth;morph;th|] - type 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 constr list - - -let add_theory name rth eqth morphth cst_tac = - Coqlib.check_required_library ["Coq";"setoid_ring";"Ring_tac"]; - let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring rth in - let (sth,morph) = build_setoid_params kind r add mul opp req eqth in - let args0 = [|r;zero;one;add;mul;sub;opp;req;sth;morph|] in - let (lemma1,lemma2) = - match morphth with - | Computational c -> - let reqb = dest_eq_test c in - let rth = - build_almost_ring - kind r zero one add mul sub opp req sth morph rth in - let args = Array.append args0 [|rth;reqb;c|] in - (lapp ring_comp1 args, lapp ring_comp2 args) - | Morphism m -> - let (m,args1) = dest_morphism kind m sth in - let rth = - build_almost_ring - kind r zero one add mul sub opp req sth morph rth in - let args = Array.concat [args0;[|rth|]; args1; [|m|]] in - (lapp coq_ring_lemma1 args, lapp coq_ring_lemma2 args) - | Abstract -> - Coqlib.check_required_library ["Coq";"setoid_ring";"ZRing_th"]; - let args1 = Array.append args0 [|rth|] in - (match kind with - None -> error "an almost_ring cannot be abstract" - | Some true -> - (lapp sring_abs1 args1, lapp sring_abs2 args1) - | Some false -> - (lapp ring_abs1 args1, lapp ring_abs2 args1)) in - let cst_tac = match cst_tac with + | Closed of reference list + +let interp_cst_tac kind (zero,one,add,mul,opp) cst_tac = + match cst_tac with Some (CstTac t) -> Tacinterp.glob_tactic t - | Some (Closed lc) -> failwith "TODO" + | Some (Closed lc) -> closed_term_ast (List.map Nametab.global lc) | None -> - (match kind with - Some true -> + (match opp, kind with + None, _ -> let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul])) - | Some false -> + | Some opp, Some _ -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) - | _ -> error"a tactic must be specified for an almost_ring") in + | _ -> error"a tactic must be specified for an almost_ring") + +let add_theory name rth eqth morphth cst_tac (pre,post) = + let env = Global.env() in + let sigma = Evd.empty in + let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in + let (sth,ext) = build_setoid_params r add mul opp req eqth in + let rk = reflect_coeff morphth in + let params = + exec_tactic env 5 (zltac"ring_lemmas") (List.map carg[sth;ext;rth;rk]) in + let lemma1 = constr_of params.(3) in + let lemma2 = constr_of params.(4) in + + let lemma1 = decl_constant (string_of_id name^"_ring_lemma1") lemma1 in + let lemma2 = decl_constant (string_of_id name^"_ring_lemma2") lemma2 in + let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in + let pretac = + match pre with + Some t -> Tacinterp.glob_tactic t + | _ -> TacId [] in + let posttac = + match post with + Some t -> Tacinterp.glob_tactic t + | _ -> TacId [] in let _ = Lib.add_leaf name (theory_to_obj { ring_carrier = r; ring_req = req; + ring_setoid = sth; + ring_ext = constr_of params.(1); + ring_morph = constr_of params.(2); + ring_th = constr_of params.(0); ring_cst_tac = cst_tac; ring_lemma1 = lemma1; - ring_lemma2 = lemma2 }) in + ring_lemma2 = lemma2; + ring_pre_tac = pretac; + ring_post_tac = posttac }) in () -VERNAC ARGUMENT EXTEND ring_coefs -| [ "Computational" constr(c)] -> [ Computational (ic c) ] -| [ "Abstract" ] -> [ Abstract ] -| [ "Coefficients" constr(m)] -> [ Morphism (ic m) ] -| [ ] -> [ Abstract ] +type ring_mod = + Ring_kind of coeff_spec + | Const_tac of cst_tac_spec + | Pre_tac of raw_tactic_expr + | Post_tac of raw_tactic_expr + | Setoid of Topconstr.constr_expr * Topconstr.constr_expr + +VERNAC ARGUMENT EXTEND ring_mod + | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational (ic eq_test)) ] + | [ "abstract" ] -> [ Ring_kind Abstract ] + | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism (ic 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) ] END -VERNAC ARGUMENT EXTEND ring_cst_tac -| [ "Constant" tactic(c)] -> [ Some(CstTac c) ] -| [ "[" ne_constr_list(l) "]" ] -> [ Some(Closed (List.map ic l)) ] -| [ ] -> [ None ] -END +let set_once s r v = + if !r = None 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 + List.iter(function + Ring_kind k -> set_once "ring kind" kind 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 sth,ic ext)) l; + let k = match !kind with Some k -> k | None -> Abstract in + (k, !set, !cst_tac, !pre, !post) VERNAC COMMAND EXTEND AddSetoidRing -| [ "Add" "New" "Ring" ident(id) ":" constr(t) ring_coefs(c) - "Setoid" constr(e) constr(m) ring_cst_tac(tac) ] -> - [ add_theory id (ic t) (Some (ic e, ic m)) c tac ] -| [ "Add" "New" "Ring" ident(id) ":" constr(t) ring_coefs(c) - ring_cst_tac(tac) ] -> - [ add_theory id (ic t) None c tac ] + | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> + [ let (k,set,cst,pre,post) = process_ring_mods l in + add_theory id (ic t) set k cst (pre,post) ] END - (*****************************************************************************) (* The tactics consist then only in a lookup in the ring database and call the appropriate ltac. *) -let ring gl = - let req = dest_rel (pf_concl gl) in - let e = - try ring_for_relation req - with Not_found -> - errorlabstrm "ring" - (str"cannot find a declared ring structure for equality"++ - spc()++str"\""++pr_constr req++str"\"") in - Tacinterp.eval_tactic - (TacArg(TacCall(dummy_loc, - ArgArg(dummy_loc, Lazy.force ltac_setoid_ring), - Tacexp e.ring_cst_tac:: - List.map carg [e.ring_lemma1;e.ring_lemma2;e.ring_req]))) - gl - -let ring_rewrite rl = - let ty = Retyping.get_type_of (Global.env()) Evd.empty (List.hd rl) in - let e = - try ring_for_carrier ty - with Not_found -> - errorlabstrm "ring" - (str"cannot find a declared ring structure over"++ - spc()++str"\""++pr_constr ty++str"\"") in - let rl = List.fold_right (fun x l -> lapp coq_cons [|ty;x;l|]) rl - (lapp coq_nil [|ty|]) in +let make_term_list carrier rl gl = + let rl = + match rl with + [] -> let (_,t1,t2) = dest_rel (pf_concl gl) in [t1;t2] + | _ -> rl in + List.fold_right + (fun x l -> lapp coq_cons [|carrier;x;l|]) rl + (lapp coq_nil [|carrier|]) + +let ring_lookup (f:glob_tactic_expr) rl gl = + let env = pf_env gl in + let sigma = project gl in + let e = find_ring_structure env sigma rl (pf_concl gl) None in + let rl = carg (make_term_list e.ring_carrier rl gl) in + 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 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 Tacinterp.eval_tactic - (TacArg(TacCall(dummy_loc, - ArgArg(dummy_loc, Lazy.force ltac_setoid_ring_rewrite), - Tacexp e.ring_cst_tac::List.map carg [e.ring_lemma2;e.ring_req;rl]))) + (TacLetIn + ([(dummy_loc,id_of_string"f"),None,Tacexp f], + ltac_lcall "f" + [req;sth;ext;morph;th;cst_tac;lemma1;lemma2;pretac;posttac;rl])) gl + +TACTIC EXTEND ring_lookup +| [ "ring_lookup" tactic(f) constr_list(l) ] -> [ ring_lookup (fst f) l ] +END + +(***********************************************************************) + +let new_field_path = + make_dirpath (List.map id_of_string ["Field_tac";contrib_name;"Coq"]) + +let field_ltac s = + lazy(make_kn (MPfile new_field_path) (make_dirpath []) (mk_label 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_constant "display_linear", + (function -1|7|8|9|10|12|13->Eval|11->Rec|_->Prot); + (* Pphi_dev: evaluate polynomial and coef operations, protect + ring operations and make recursive call on the var map *) + my_constant "Pphi_dev", (function -1|6|7|8|9|11->Eval|10->Rec|_->Prot); + (* PEeval: evaluate morphism and polynomial, protect ring + operations and make recursive call on the var map *) + my_constant "FEeval", (function -1|9|11->Eval|10->Rec|_->Prot)]);; + + +let _ = add_map "field_cond" + (map_with_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_constant "PCond", (function -1|8|10->Eval|9->Rec|_->Prot)]);; + + +let afield_theory = my_constant "almost_field_theory" +let field_theory = my_constant "field_theory" +let sfield_theory = my_constant "semi_field_theory" +let af_ar = my_constant"AF_AR" +let f_r = my_constant"F_R" +let sf_sr = my_constant"SF_SR" +let dest_field 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;div;inv;req|]) + when f = Lazy.force afield_theory -> + let rth = lapp 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 f = Lazy.force field_theory -> + let rth = + lapp 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 f = Lazy.force sfield_theory -> + let rth = lapp 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_ok : constr; + field_simpl_eq_ok : constr; + field_simpl_ok : constr; + field_cond : constr; + field_pre_tac : glob_tactic_expr; + field_post_tac : glob_tactic_expr } + +let field_from_carrier = ref Cmap.empty +let field_from_relation = ref Cmap.empty +let field_from_name = ref Spmap.empty + + +let field_for_carrier r = Cmap.find r !field_from_carrier +let field_for_relation rel = Cmap.find rel !field_from_relation +let field_lookup_by_name ref = + Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref))) + !field_from_name + + +let find_field_structure env sigma l cl oname = + check_required_library (cdir@["Field_tac"]); + match oname, l with + Some rf, _ -> + (try field_lookup_by_name rf + with Not_found -> + errorlabstrm "field" + (str "found no field named "++pr_reference rf)) + | None, 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"\"")) + | None, [] -> + let (req,_,_) = dest_rel cl in + (try field_for_relation req + with Not_found -> + errorlabstrm "field" + (str"cannot find a declared field structure for equality"++ + spc()++str"\""++pr_constr req++str"\"")) + +let _ = + Summary.declare_summary "tactic-new-field-table" + { Summary.freeze_function = + (fun () -> !field_from_carrier,!field_from_relation,!field_from_name); + Summary.unfreeze_function = + (fun (ct,rt,nt) -> + field_from_carrier := ct; field_from_relation := rt; + field_from_name := nt); + Summary.init_function = + (fun () -> + field_from_carrier := Cmap.empty; field_from_relation := Cmap.empty; + field_from_name := Spmap.empty); + Summary.survive_module = false; + Summary.survive_section = false } + +let add_field_entry (sp,_kn) e = +(* + let _ = ty e.field_ok in + let _ = ty e.field_simpl_eq_ok in + let _ = ty e.field_simpl_ok in + let _ = ty e.field_cond in +*) + field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier; + field_from_relation := Cmap.add e.field_req e !field_from_relation; + 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_cond in + let tac'= subst_tactic subst th.field_cst_tac in + let pretac'= subst_tactic subst th.field_pre_tac in + let posttac'= 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_cond && + tac' == th.field_cst_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_ok = thm1'; + field_simpl_eq_ok = thm2'; + field_simpl_ok = thm3'; + field_cond = thm4'; + field_pre_tac = pretac'; + field_post_tac = posttac' } + +let (ftheory_to_obj, obj_to_ftheory) = + let cache_th (name,th) = add_field_entry name th + and export_th x = Some x in + declare_object + {(default_object "tactic-new-field-theory") with + open_function = (fun i o -> if i=1 then cache_th o); + cache_function = cache_th; + subst_function = subst_th; + classify_function = (fun (_,x) -> Substitute x); + export_function = export_th } -let setoid_ring = function - | [] -> ring - | l -> ring_rewrite l +let default_field_equality r inv req = + let is_setoid = function + {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _} -> true + | _ -> false in + match default_relation_for_carrier ~filter:is_setoid r with + Leibniz _ -> + mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|]) + | Relation rel -> + let is_endomorphism = function + { args=args } -> List.for_all + (function (var,Relation rel) -> + var=None && eq_constr req rel + | _ -> false) args in + let inv_m = + try default_morphism ~filter:is_endomorphism inv + with Not_found -> + error "field inverse should be declared as a morphism" in + inv_m.lem + +let add_field_theory name fth eqth morphth cst_tac inj (pre,post) = + let env = Global.env() in + let sigma = Evd.empty in + let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) = + dest_field env sigma fth in + let (sth,ext) = build_setoid_params r add mul opp req eqth in + let eqth = Some(sth,ext) in + let _ = add_theory name rth eqth morphth cst_tac (None,None) in + let inv_m = default_field_equality r inv req in + let rk = reflect_coeff morphth in + let params = + exec_tactic env 8 (field_ltac"field_lemmas") + (List.map carg[sth;ext;inv_m;fth;rk]) in + let lemma1 = constr_of params.(3) in + let lemma2 = constr_of params.(4) in + let lemma3 = constr_of params.(5) in + let cond_lemma = + match inj with + | Some thm -> mkApp(constr_of params.(7),[|thm|]) + | None -> constr_of params.(6) in + let lemma1 = decl_constant (string_of_id name^"_field_lemma1") lemma1 in + let lemma2 = decl_constant (string_of_id name^"_field_lemma2") lemma2 in + let lemma3 = decl_constant (string_of_id name^"_field_lemma3") lemma3 in + let cond_lemma = decl_constant (string_of_id name^"_lemma4") cond_lemma in + let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in + let pretac = + match pre with + Some t -> Tacinterp.glob_tactic t + | _ -> TacId [] in + let posttac = + match post with + Some t -> Tacinterp.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_ok = lemma1; + field_simpl_eq_ok = lemma2; + field_simpl_ok = lemma3; + field_cond = cond_lemma; + field_pre_tac = pretac; + field_post_tac = posttac }) in () + +type field_mod = + Ring_mod of ring_mod + | Inject of Topconstr.constr_expr + +VERNAC ARGUMENT EXTEND field_mod + | [ ring_mod(m) ] -> [ Ring_mod m ] + | [ "infinite" constr(inj) ] -> [ Inject inj ] +END -TACTIC EXTEND setoid_ring - [ "setoid" "ring" constr_list(l) ] -> [ setoid_ring l ] +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 + List.iter(function + Ring_mod(Ring_kind k) -> set_once "field kind" kind 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 sth,ic ext) + | Inject i -> set_once "infinite property" inj (ic i)) l; + let k = match !kind with Some k -> k | None -> Abstract in + (k, !set, !inj, !cst_tac, !pre, !post) + +VERNAC COMMAND EXTEND AddSetoidField +| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> + [ let (k,set,inj,cst_tac,pre,post) = process_field_mods l in + add_field_theory id (ic t) set k cst_tac inj (pre,post) ] END +let field_lookup (f:glob_tactic_expr) rl gl = + let env = pf_env gl in + let sigma = project gl in + let e = find_field_structure env sigma rl (pf_concl gl) None in + let rl = carg (make_term_list e.field_carrier rl gl) in + let req = carg e.field_req in + let cst_tac = Tacexp e.field_cst_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 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 + Tacinterp.eval_tactic + (TacLetIn + ([(dummy_loc,id_of_string"f"),None,Tacexp f], + ltac_lcall "f" + [req;cst_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;cond_ok; + pretac;posttac;rl])) gl + +TACTIC EXTEND field_lookup +| [ "field_lookup" tactic(f) constr_list(l) ] -> [ field_lookup (fst f) l ] +END |