diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /contrib/field/field.ml4 | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'contrib/field/field.ml4')
-rw-r--r-- | contrib/field/field.ml4 | 193 |
1 files changed, 0 insertions, 193 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 deleted file mode 100644 index dea79773..00000000 --- a/contrib/field/field.ml4 +++ /dev/null @@ -1,193 +0,0 @@ -(************************************************************************) -(* 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: field.ml4 10076 2007-08-16 11:16:43Z notin $ *) - -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; - Summary.survive_module = false; - Summary.survive_section = false } - -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') -let export_addfield x = Some x - -(* 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); - 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 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 = - match Hipattern.match_with_equation (pf_concl g) with - | Some (eq,t::args) when eq = (Coqlib.build_coq_eq_data()).Coqlib.eq -> t - | _ -> 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 |