diff options
author | 2001-04-19 05:00:21 +0000 | |
---|---|---|
committer | 2001-04-19 05:00:21 +0000 | |
commit | 8bd7161251dc0b8e27e4d117ad0e73edf60bbb67 (patch) | |
tree | f927af9513747fc16c3b709768eba4520f628d81 /contrib/field/field.ml4 | |
parent | 70eb06865e5f6a717b6bf746ef6cb61a75abb7a4 (diff) |
Ajout de Field
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1609 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/field/field.ml4')
-rw-r--r-- | contrib/field/field.ml4 | 113 |
1 files changed, 113 insertions, 0 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 new file mode 100644 index 000000000..60edfe07d --- /dev/null +++ b/contrib/field/field.ml4 @@ -0,0 +1,113 @@ +(* field.ml4 *) + +(*i camlp4deps: "parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo" i*) + +open Names +open Proof_type +open Tacinterp +open Tacmach +open Term +open Util +open Vernacinterp + +(* Interpretation of constr's *) +let constr_of com = Astterm.interp_constr Evd.empty (Global.env()) com + +(* Construction of constants *) +let constant dir s = + let dir = "Coq"::"field"::dir in + let id = id_of_string s in + try + Declare.global_reference_in_absolute_module dir id + with Not_found -> + anomaly ("Field: cannot find "^ + (Nametab.string_of_qualid (Nametab.make_qualid dir id))) + +(* To deal with the optional arguments *) +let constr_of_opt a opt = + let ac = constr_of a in + match opt with + | None -> mkApp ((constant ["Field_Compl"] "None"),[|ac|]) + | Some f -> mkApp ((constant ["Field_Compl"] "Some"),[|ac;constr_of f|]) + +(* Table of theories *) +let th_tab = ref ((Hashtbl.create 53) : (constr,constr) Hashtbl.t) + +let lookup typ = Hashtbl.find !th_tab typ + +let _ = + let init () = th_tab := (Hashtbl.create 53) 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; + Summary.survive_section = false } + +let load_addfield _ = () +let cache_addfield (_,(typ,th)) = Hashtbl.add !th_tab typ th +let export_addfield x = Some x + +(* Declaration of the Add Field library object *) +let (in_addfield,out_addfield)= + Libobject.declare_object + ("ADD_FIELD", + { Libobject.load_function = load_addfield; + Libobject.open_function = cache_addfield; + Libobject.cache_function = cache_addfield; + Libobject.export_function = export_addfield }) + +(* 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 a aplus amult aone azero aopp aeq rth + Quote.ConstrSet.empty + with | UserError("Add Semi Ring",_) -> ()); + let th = mkApp ((constant ["Field_Theory"] "Build_Field_Theory"), + [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in + Lib.add_anonymous_leaf (in_addfield (a,th)) + end + +(* Vernac command declaration *) +let _ = + let rec opt_arg (aminus_o,adiv_o) = function + | (VARG_STRING "minus")::(VARG_CONSTR aminus)::l -> + (match aminus_o with + | None -> opt_arg ((Some aminus),adiv_o) l + | _ -> anomaly "AddField") + | (VARG_STRING "div")::(VARG_CONSTR adiv)::l -> + (match adiv_o with + | None -> opt_arg (aminus_o,(Some adiv)) l + | _ -> anomaly "AddField") + | _ -> (aminus_o,adiv_o) in + vinterp_add "AddField" + (function + | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult) + ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp) + ::(VARG_CONSTR aeq)::(VARG_CONSTR ainv)::(VARG_CONSTR rth) + ::(VARG_CONSTR ainv_l)::l -> + (fun () -> + let (aminus_o,adiv_o) = opt_arg (None,None) l 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)) + | _ -> anomaly "AddField") + +(* Guesses the type and calls Field_Gen with the right theory *) +let field g = + let evc = project g + and env = pf_env g in + let typ = constr_of_Constr (interp_tacarg (evc,env,[],[],Some g,get_debug ()) + <:tactic< + Match Context With + | [|-(eq ?1 ? ?)] -> ?1 + | [|-(eqT ?1 ? ?)] -> ?1>>) in + let th = VArg (Constr (lookup typ)) in + (tac_interp [("FT",th)] [] (get_debug ()) <:tactic<Field_Gen FT>>) g + +(* Declaration of Field *) +let _ = hide_tactic "Field" (function _ -> field) |