diff options
author | 2015-01-25 14:42:51 +0100 | |
---|---|---|
committer | 2015-01-25 14:42:51 +0100 | |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /plugins/setoid_ring/newring.ml4 | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'plugins/setoid_ring/newring.ml4')
-rw-r--r-- | plugins/setoid_ring/newring.ml4 | 684 |
1 files changed, 339 insertions, 345 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index d1a5c0ab..2f9e8509 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -1,30 +1,27 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp +open Errors open Util open Names open Term +open Vars open Closure open Environ open Libnames -open Tactics +open Globnames open Glob_term open Tacticals open Tacexpr -open Pcoq -open Tactic -open Constr -open Proof_type open Coqlib -open Tacmach open Mod_subst open Tacinterp open Libobject @@ -32,14 +29,20 @@ open Printer open Declare open Decl_kinds open Entries +open Misctypes + +DECLARE PLUGIN "newring_plugin" (****************************************************************************) (* controlled reduction *) -let mark_arg i c = mkEvar(i,[|c|]) +(** ppedrot: something dubious here, we're obviously using evars the wrong + way. FIXME! *) + +let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|]) let unmark_arg f c = match destEvar c with - | (i,[|c|]) -> f i c + | (i,[|c|]) -> f (Evar.repr i) c | _ -> assert false type protect_flag = Eval|Prot|Rec @@ -48,10 +51,19 @@ let tag_arg tag_rec map subs i c = match map i with Eval -> mk_clos subs c | Prot -> mk_atom c - | Rec -> if i = -1 then mk_clos subs c else tag_rec 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 t with + 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 @@ -62,9 +74,9 @@ let rec mk_clos_but f_map subs 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 fargs, args' = Array.chop n args in let f' = mkApp(f,fargs) in - match f_map f' with + 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')) @@ -72,24 +84,13 @@ and mk_clos_app_but f_map subs f args n = (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 c = - try - let (im,am) = List.assoc c l in - Some(fun i -> - if List.mem i im then Eval - else if List.mem i am then Prot - else if i = -1 then Eval - else Rec) - with Not_found -> None - let interp_map l t = - try Some(list_assoc_f eq_constr t l) with Not_found -> None + try Some(List.assoc_f eq_gr t l) with Not_found -> None -let protect_maps = ref Stringmap.empty -let add_map s m = protect_maps := Stringmap.add s m !protect_maps +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 Stringmap.find map !protect_maps + try String.Map.find map !protect_maps with Not_found -> errorlabstrm"lookup_map"(str"map "++qs map++str"not found") @@ -101,112 +102,120 @@ 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, Termops.InHyp));; + Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));; TACTIC EXTEND protect_fv [ "protect_fv" string(map) "in" ident(id) ] -> - [ protect_tac_in map id ] + [ Proofview.V82.tactic (protect_tac_in map id) ] | [ "protect_fv" string(map) ] -> - [ protect_tac map ] + [ Proofview.V82.tactic (protect_tac map) ] END;; (****************************************************************************) let closed_term t l = - let l = List.map constr_of_global l in + 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) "]" ] -> - [ closed_term t l ] + [ Proofview.V82.tactic (closed_term t l) ] END ;; -TACTIC EXTEND echo +(* TACTIC EXTEND echo | [ "echo" constr(t) ] -> [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ] -END;; +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]))) + 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 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 (GVar(dummy_loc,id_of_string"t"),None); - Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l]))) + let tacname = { + mltac_plugin = "newring_plugin"; + mltac_tactic = "closed_term"; + } 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 ((dummy_loc,id_of_string"ring_closed_term" +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_constr sigma env c + 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 c = - mkConst(declare_constant (id_of_string na) (DefinitionEntry - { const_entry_body = c; - const_entry_secctx = None; - const_entry_type = None; - const_entry_opaque = true }, - IsProof Lemma)) +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(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)) + TacArg(Loc.ghost,TacCall(Loc.ghost, ArgArg(Loc.ghost, Lazy.force tac),args)) (* Calling a locally bound tactic *) let ltac_lcall tac args = - TacArg(dummy_loc,TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args)) + TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args)) let ltac_letin (x, e1) e2 = - TacLetIn(false,[(dummy_loc,id_of_string 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) + TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds) -let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c) +let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c) -let dummy_goal env = +let dummy_goal env sigma = let (gl,_,sigma) = - Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Store.empty in - {Evd.it = gl; - Evd.sigma = sigma} + Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in + {Evd.it = gl; Evd.sigma = sigma} -let exec_tactic env n f args = - let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in +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 -> List.assoc id ist.lfun) lid in + 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, - 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" + 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"]; @@ -217,16 +226,23 @@ let stdlib_modules = 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_cons = coq_constant "cons" -let coq_nil = coq_constant "nil" -let coq_None = coq_constant "None" -let coq_Some = coq_constant "Some" +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 -> @@ -255,17 +271,19 @@ let plugin_modules = 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 = - make_dirpath (List.map id_of_string ["Ring_tac";plugin_dir;"Coq"]) + DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"]) let ltac s = - lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s)) + lazy(make_kn (MPfile new_ring_path) DirPath.empty (Label.make s)) let znew_ring_path = - make_dirpath (List.map id_of_string ["InitialRing";plugin_dir;"Coq"]) + DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) let zltac s = - lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s)) + lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s)) -let mk_cst l s = lazy (Coqlib.gen_constant "newring" l 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 *) @@ -274,9 +292,9 @@ let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; 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" +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" @@ -303,16 +321,19 @@ 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_constant "mkhypo" -let coq_hypo = my_constant "hypo" +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 - ((req,(function -1->Prot|_->Rec)):: + ((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); @@ -343,15 +364,12 @@ type ring_info = ring_pre_tac : glob_tactic_expr; ring_post_tac : glob_tactic_expr } -module Cmap = Map.Make(struct type t = constr let compare = constr_ord end) +module Cmap = Map.Make(Constr) -let from_carrier = ref Cmap.empty -let from_relation = ref Cmap.empty -let from_name = ref Spmap.empty +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 ring_for_relation rel = Cmap.find rel !from_relation - let find_ring_structure env sigma l = match l with @@ -370,32 +388,9 @@ let find_ring_structure env sigma l = (str"cannot find a declared ring structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false -(* - 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,!from_name); - Summary.unfreeze_function = - (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; - from_name := Spmap.empty) } 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_name := Spmap.add sp e !from_name @@ -408,10 +403,10 @@ let subst_th (subst,th) = 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 pow_tac'= subst_tactic subst th.ring_pow_tac in - let pretac'= subst_tactic subst th.ring_pre_tac in - let posttac'= subst_tactic subst th.ring_post_tac 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 && @@ -443,20 +438,20 @@ 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 i=1 then cache_th o); + 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 a r = - let evm = Evd.empty in +let setoid_of_relation env evd a r = try - lapp coq_mk_Setoid - [|a ; r ; - Rewrite.get_reflexive_proof env evm a r ; - Rewrite.get_symmetric_proof env evm a r ; - Rewrite.get_transitive_proof env evm a r |] + 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" @@ -469,7 +464,7 @@ let op_smorph 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 req rel (\* Qu: use conversion ? *\) *) +(* eq_constr_nounivs req rel (\* Qu: use conversion ? *\) *) (* | _ -> false in *) (* match default_relation_for_carrier ~filter:is_setoid r with *) (* Leibniz _ -> *) @@ -484,7 +479,7 @@ let op_smorph r add mul req m1 m2 = (* let is_endomorphism = function *) (* { args=args } -> List.for_all *) (* (function (var,Relation rel) -> *) -(* var=None && eq_constr req rel *) +(* var=None && eq_constr_nounivs req rel *) (* | _ -> false) args in *) (* let add_m = *) (* try default_morphism ~filter:is_endomorphism add *) @@ -519,17 +514,19 @@ let op_smorph r add mul req m1 m2 = (* op_smorph r add mul req add_m.lem mul_m.lem) in *) (* (setoid,op_morph) *) -let ring_equality (r,add,mul,opp,req) = +let ring_equality env evd (r,add,mul,opp,req) = match kind_of_term req with - | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) -> - let setoid = lapp coq_eq_setoid [|r|] in + | 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 -> lapp coq_eq_morph [|r;add;mul;opp|] - | None -> lapp coq_eq_smorph [|r;add;mul|] in + 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 ()) r req in + 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 @@ -549,7 +546,7 @@ let ring_equality (r,add,mul,opp,req) = let op_morph = op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in Flags.if_verbose - msgnl + 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++ @@ -558,7 +555,7 @@ let ring_equality (r,add,mul,opp,req) = op_morph) | None -> (Flags.if_verbose - msgnl + msg_info (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ str"and morphisms \""++pr_constr add_m_lem ++ str"\""++spc()++str"and \""++ @@ -566,22 +563,22 @@ let ring_equality (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 r add mul opp req eqth = +let build_setoid_params env evd r add mul opp req eqth = match eqth with Some th -> th - | None -> ring_equality (r,add,mul,opp,req) + | 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 f (Lazy.force coq_almost_ring_theory) -> + 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 f (Lazy.force coq_semi_ring_theory) -> + 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 f (Lazy.force coq_ring_theory) -> + 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" @@ -591,18 +588,18 @@ let dest_morph env sigma m_spec = 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 f (Lazy.force coq_ring_morph) -> + 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 f (Lazy.force coq_semi_morph) -> + when eq_constr_nounivs f (Lazy.force coq_semi_morph) -> (c,czero,cone,cadd,cmul,None,None,ceqb,phi) | _ -> error "bad morphism structure" -type coeff_spec = - Computational of constr (* equality test *) +type 'constr coeff_spec = + Computational of 'constr (* equality test *) | Abstract (* coeffs = Z *) - | Morphism of constr (* general morphism *) + | Morphism of 'constr (* general morphism *) let reflect_coeff rkind = @@ -618,101 +615,89 @@ type cst_tac_spec = let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = match cst_tac with - Some (CstTac t) -> Tacinterp.glob_tactic t + Some (CstTac t) -> Tacintern.glob_tactic t | Some (Closed lc) -> closed_term_ast (List.map Smartlocate.global_with_alias lc) | None -> - (match rk, opp, kind with - Abstract, None, _ -> - let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in - TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul])) - | Abstract, Some opp, Some _ -> - let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in - TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) - | Abstract, Some opp, None -> - let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in - TacArg - (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) - | Computational _,_,_ -> - let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in - TacArg - (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;zero;one])) - | Morphism mth,_,_ -> - let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in - let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in - TacArg - (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone]))) - -let make_hyp env c = - let t = Retyping.get_type_of env Evd.empty c in - lapp coq_mkhypo [|t;c|] - -let make_hyp_list env lH = - let carrier = Lazy.force coq_hypo in - List.fold_right - (fun c l -> lapp coq_cons [|carrier; (make_hyp env c); l|]) lH - (lapp coq_nil [|carrier|]) - -let interp_power env pow = - let carrier = Lazy.force coq_hypo in + 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(dummy_loc, Lazy.force ltac_inv_morph_nothing) in - (TacArg(dummy_loc,TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|]) + 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 -> Tacinterp.glob_tactic t + | CstTac t -> Tacintern.glob_tactic t | Closed lc -> closed_term_ast (List.map Smartlocate.global_with_alias lc) in - let spec = make_hyp env (ic spec) in - (tac, lapp coq_Some [|carrier; spec|]) + let spec = make_hyp env evd (ic_unsafe spec) in + (tac, plapp evd coq_Some [|carrier; spec|]) -let interp_sign env sign = - let carrier = Lazy.force coq_hypo in +let interp_sign env evd sign = + let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in match sign with - | None -> lapp coq_None [|carrier|] + | None -> plapp evd coq_None [|carrier|] | Some spec -> - let spec = make_hyp env (ic spec) in - lapp coq_Some [|carrier;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 div = - let carrier = Lazy.force coq_hypo in +let interp_div env evd div = + let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in match div with - | None -> lapp coq_None [|carrier|] + | None -> plapp evd coq_None [|carrier|] | Some spec -> - let spec = make_hyp env (ic spec) in - lapp coq_Some [|carrier;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 rth eqth morphth cst_tac (pre,post) power sign div = +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 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 (pow_tac, pspec) = interp_power env power in - let sspec = interp_sign env sign in - let dspec = interp_div env div 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 = - exec_tactic env 5 (zltac "ring_lemmas") + let params,ctx = + exec_tactic env !evd 5 (zltac "ring_lemmas") (List.map carg[sth;ext;rth;pspec;sspec;dspec;rk]) in - let lemma1 = constr_of params.(3) in - let lemma2 = constr_of params.(4) in + let lemma1 = params.(3) in + let lemma2 = 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 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 -> Tacinterp.glob_tactic t + Some t -> Tacintern.glob_tactic t | _ -> TacId [] in let posttac = match post with - Some t -> Tacinterp.glob_tactic t + Some t -> Tacintern.glob_tactic t | _ -> TacId [] in let _ = Lib.add_leaf name @@ -720,9 +705,9 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div = { 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_ext = params.(1); + ring_morph = params.(2); + ring_th = params.(0); ring_cst_tac = cst_tac; ring_pow_tac = pow_tac; ring_lemma1 = lemma1; @@ -731,22 +716,28 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div = ring_post_tac = posttac }) in () -type ring_mod = - Ring_kind of coeff_spec +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 Topconstr.constr_expr * Topconstr.constr_expr - | Pow_spec of cst_tac_spec * Topconstr.constr_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 Topconstr.constr_expr - | Div_spec of Topconstr.constr_expr + | 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 (ic eq_test)) ] + | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ] | [ "abstract" ] -> [ Ring_kind Abstract ] - | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism (ic morph)) ] + | [ "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 ] @@ -761,7 +752,7 @@ VERNAC ARGUMENT EXTEND ring_mod END let set_once s r v = - if !r = None then r := Some v else error (s^" cannot be set twice") + 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 @@ -773,21 +764,29 @@ let process_ring_mods l = let power = ref None in let div = ref None in List.iter(function - Ring_kind k -> set_once "ring kind" kind k + 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 sth,ic ext) + | 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 +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 (*****************************************************************************) @@ -799,10 +798,11 @@ let make_args_list rl t = | [] -> let (_,t1,t2) = dest_rel0 t in [t1;t2] | _ -> rl -let make_term_list carrier rl = - List.fold_right - (fun x l -> lapp coq_cons [|carrier;x;l|]) rl - (lapp coq_nil [|carrier|]) +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 @@ -819,19 +819,24 @@ let ltac_ring_structure e = [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac] -let ring_lookup (f:glob_tactic_expr) lH rl t gl = - let env = pf_env gl in - let sigma = project gl in - let rl = make_args_list rl t in - let e = find_ring_structure env sigma rl in - let rl = carg (make_term_list e.ring_carrier rl) in - let lH = carg (make_hyp_list env lH) in - let ring = ltac_ring_structure e in - ltac_apply f (ring@[lH;rl]) gl +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] + [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t] END @@ -839,10 +844,10 @@ END (***********************************************************************) let new_field_path = - make_dirpath (List.map id_of_string ["Field_tac";plugin_dir;"Coq"]) + DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"]) let field_ltac s = - lazy(make_kn (MPfile new_field_path) (make_dirpath []) (mk_label s)) + lazy(make_kn (MPfile new_field_path) DirPath.empty (Label.make s)) let _ = add_map "field" @@ -851,9 +856,9 @@ let _ = add_map "field" 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", + my_reference "display_linear", (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot); - my_constant "display_pow_linear", + 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 *) @@ -865,16 +870,16 @@ let _ = add_map "field" 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_constant "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);; + my_reference "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);; let _ = add_map "field_cond" - (map_with_eq + (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_constant "PCond", (function -1|8|10|13->Eval|12->Rec|_->Prot)]);; -(* (function -1|8|10->Eval|9->Rec|_->Prot)]);;*) + 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" @@ -882,29 +887,29 @@ let _ = Redexpr.declare_reduction "simpl_field_expr" -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 +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 eq_constr f (Lazy.force afield_theory) -> - let rth = lapp af_ar + 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 eq_constr f (Lazy.force field_theory) -> + when is_global (Lazy.force field_theory) f -> let rth = - lapp f_r + 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 eq_constr f (Lazy.force sfield_theory) -> - let rth = lapp sf_sr + 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" @@ -922,13 +927,10 @@ type field_info = 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_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 field_for_relation rel = Cmap.find rel !field_from_relation let find_field_structure env sigma l = check_required_library (cdir@["Field_tac"]); @@ -948,35 +950,9 @@ let find_field_structure env sigma l = (str"cannot find a declared field structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false -(* 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) } 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) = @@ -987,10 +963,10 @@ let subst_th (subst,th) = 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'= subst_tactic subst th.field_cst_tac in - let pow_tac' = subst_tactic subst th.field_pow_tac in - let pretac'= subst_tactic subst th.field_pre_tac in - let posttac'= subst_tactic subst th.field_post_tac 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 && @@ -1019,17 +995,17 @@ 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 i=1 then cache_th o); + 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 r inv req = +let field_equality evd r inv req = match kind_of_term req with - | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) -> - mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|]) + | 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 ()) r req in + 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 @@ -1037,45 +1013,50 @@ let field_equality r inv req = 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) power sign odiv = +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 sigma = Evd.empty in + let evd = ref sigma 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 + 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 rth eqth morphth cst_tac (None,None) power sign odiv in - let (pow_tac, pspec) = interp_power env power in - let sspec = interp_sign env sign in - let dspec = interp_div env odiv in - let inv_m = field_equality r inv req 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 = - exec_tactic env 9 (field_ltac"field_lemmas") + 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 = constr_of params.(3) in - let lemma2 = constr_of params.(4) in - let lemma3 = constr_of params.(5) in - let lemma4 = constr_of params.(6) 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(constr_of params.(8),[|thm|]) - | None -> constr_of params.(7) 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 lemma4 = decl_constant (string_of_id name^"_field_lemma4") lemma4 in - let cond_lemma = decl_constant (string_of_id name^"_lemma5") cond_lemma in + | 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 -> Tacinterp.glob_tactic t + Some t -> Tacintern.glob_tactic t | _ -> TacId [] in let posttac = match post with - Some t -> Tacinterp.glob_tactic t + Some t -> Tacintern.glob_tactic t | _ -> TacId [] in let _ = Lib.add_leaf name @@ -1092,9 +1073,9 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi field_pre_tac = pretac; field_post_tac = posttac }) in () -type field_mod = - Ring_mod of ring_mod - | Inject of Topconstr.constr_expr +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 ] @@ -1112,23 +1093,31 @@ let process_field_mods l = let power = ref None in let div = ref None in List.iter(function - Ring_mod(Ring_kind k) -> set_once "field kind" kind k + 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 sth,ic ext) + | 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 i)) l; + | 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 +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 @@ -1146,18 +1135,23 @@ let ltac_field_structure e = [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 gl = - let env = pf_env gl in - let sigma = project gl in - let rl = make_args_list rl t in - let e = find_field_structure env sigma rl in - let rl = carg (make_term_list e.field_carrier rl) in - let lH = carg (make_hyp_list env lH) in - let field = ltac_field_structure e in - ltac_apply f (field@[lH;rl]) gl +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 ] + [ let (t,l) = List.sep_last lt in field_lookup f lH l t ] END |