summaryrefslogtreecommitdiff
path: root/plugins/field/field.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/field/field.ml4')
-rw-r--r--plugins/field/field.ml4191
1 files changed, 191 insertions, 0 deletions
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
new file mode 100644
index 00000000..238b4c1e
--- /dev/null
+++ b/plugins/field/field.ml4
@@ -0,0 +1,191 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Names
+open Pp
+open Proof_type
+open Tacinterp
+open Tacmach
+open Term
+open Typing
+open Util
+open Vernacinterp
+open Vernacexpr
+open Tacexpr
+open Mod_subst
+open Coqlib
+
+(* Interpretation of constr's *)
+let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
+
+(* Construction of constants *)
+let constant dir s = gen_constant "Field" ("field"::dir) s
+let init_constant s = gen_constant_in_modules "Field" init_modules s
+
+(* To deal with the optional arguments *)
+let constr_of_opt a opt =
+ let ac = constr_of a in
+ let ac3 = mkArrow ac (mkArrow ac ac) in
+ match opt with
+ | None -> mkApp (init_constant "None",[|ac3|])
+ | Some f -> mkApp (init_constant "Some",[|ac3;constr_of f|])
+
+(* Table of theories *)
+let th_tab = ref (Gmap.empty : (constr,constr) Gmap.t)
+
+let lookup env typ =
+ try Gmap.find typ !th_tab
+ with Not_found ->
+ errorlabstrm "field"
+ (str "No field is declared for type" ++ spc() ++
+ Printer.pr_lconstr_env env typ)
+
+let _ =
+ let init () = th_tab := Gmap.empty in
+ let freeze () = !th_tab in
+ let unfreeze fs = th_tab := fs in
+ Summary.declare_summary "field"
+ { Summary.freeze_function = freeze;
+ Summary.unfreeze_function = unfreeze;
+ Summary.init_function = init }
+
+let load_addfield _ = ()
+let cache_addfield (_,(typ,th)) = th_tab := Gmap.add typ th !th_tab
+let subst_addfield (subst,(typ,th as obj)) =
+ let typ' = subst_mps subst typ in
+ let th' = subst_mps subst th in
+ if typ' == typ && th' == th then obj else
+ (typ',th')
+
+(* Declaration of the Add Field library object *)
+let (in_addfield,out_addfield)=
+ Libobject.declare_object {(Libobject.default_object "ADD_FIELD") with
+ Libobject.open_function = (fun i o -> if i=1 then cache_addfield o);
+ Libobject.cache_function = cache_addfield;
+ Libobject.subst_function = subst_addfield;
+ Libobject.classify_function = (fun a -> Libobject.Substitute a)}
+
+(* Adds a theory to the table *)
+let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
+ ainv_l =
+ begin
+ (try
+ Ring.add_theory true true false a None None None aplus amult aone azero
+ (Some aopp) aeq rth Quote.ConstrSet.empty
+ with | UserError("Add Semi Ring",_) -> ());
+ let th = mkApp ((constant ["LegacyField_Theory"] "Build_Field_Theory"),
+ [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in
+ begin
+ let _ = type_of (Global.env ()) Evd.empty th in ();
+ Lib.add_anonymous_leaf (in_addfield (a,th))
+ end
+ end
+
+(* Vernac command declaration *)
+open Extend
+open Pcoq
+open Genarg
+
+VERNAC ARGUMENT EXTEND divarg
+| [ "div" ":=" constr(adiv) ] -> [ adiv ]
+END
+
+VERNAC ARGUMENT EXTEND minusarg
+| [ "minus" ":=" constr(aminus) ] -> [ aminus ]
+END
+
+(*
+(* The v7->v8 translator needs printers, then temporary use ARGUMENT EXTEND...*)
+VERNAC ARGUMENT EXTEND minus_div_arg
+| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
+| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
+| [ ] -> [ None, None ]
+END
+*)
+
+(* For the translator, otherwise the code above is OK *)
+open Ppconstr
+let pp_minus_div_arg _prc _prlc _prt (omin,odiv) =
+ if omin=None && odiv=None then mt() else
+ spc() ++ str "with" ++
+ pr_opt (fun c -> str "minus := " ++ _prc c) omin ++
+ pr_opt (fun c -> str "div := " ++ _prc c) odiv
+(*
+let () =
+ Pptactic.declare_extra_genarg_pprule true
+ (rawwit_minus_div_arg,pp_minus_div_arg)
+ (globwit_minus_div_arg,pp_minus_div_arg)
+ (wit_minus_div_arg,pp_minus_div_arg)
+*)
+ARGUMENT EXTEND minus_div_arg
+ TYPED AS constr_opt * constr_opt
+ PRINTED BY pp_minus_div_arg
+| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
+| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
+| [ ] -> [ None, None ]
+END
+
+VERNAC COMMAND EXTEND Field
+ [ "Add" "Legacy" "Field"
+ constr(a) constr(aplus) constr(amult) constr(aone)
+ constr(azero) constr(aopp) constr(aeq)
+ constr(ainv) constr(rth) constr(ainv_l) minus_div_arg(md) ]
+ -> [ let (aminus_o, adiv_o) = md in
+ add_field
+ (constr_of a) (constr_of aplus) (constr_of amult)
+ (constr_of aone) (constr_of azero) (constr_of aopp)
+ (constr_of aeq) (constr_of ainv) (constr_of_opt a aminus_o)
+ (constr_of_opt a adiv_o) (constr_of rth) (constr_of ainv_l) ]
+END
+
+(* Guesses the type and calls field_gen with the right theory *)
+let field g =
+ Coqlib.check_required_library ["Coq";"field";"LegacyField"];
+ let typ =
+ try match Hipattern.match_with_equation (pf_concl g) with
+ | _,_,Hipattern.PolymorphicLeibnizEq (t,_,_) -> t
+ | _ -> raise Exit
+ with Hipattern.NoEquationFound | Exit ->
+ error "The statement is not built from Leibniz' equality" in
+ let th = VConstr ([],lookup (pf_env g) typ) in
+ (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ())
+ <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g
+
+(* Verifies that all the terms have the same type and gives the right theory *)
+let guess_theory env evc = function
+ | c::tl ->
+ let t = type_of env evc c in
+ if List.exists (fun c1 ->
+ not (Reductionops.is_conv env evc t (type_of env evc c1))) tl then
+ errorlabstrm "Field:" (str" All the terms must have the same type")
+ else
+ lookup env t
+ | [] -> anomaly "Field: must have a non-empty constr list here"
+
+(* Guesses the type and calls Field_Term with the right theory *)
+let field_term l g =
+ Coqlib.check_required_library ["Coq";"field";"LegacyField"];
+ let env = (pf_env g)
+ and evc = (project g) in
+ let th = valueIn (VConstr ([],guess_theory env evc l))
+ and nl = List.map (fun x -> valueIn (VConstr ([],x))) (Quote.sort_subterm g l) in
+ (List.fold_right
+ (fun c a ->
+ let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in
+ Tacticals.tclTHENFIRSTn tac [|a|]) nl Tacticals.tclIDTAC) g
+
+(* Declaration of Field *)
+
+TACTIC EXTEND legacy_field
+| [ "legacy" "field" ] -> [ field ]
+| [ "legacy" "field" ne_constr_list(l) ] -> [ field_term l ]
+END
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-01 07:27:07 +0000