diff options
author | 2002-03-17 04:57:32 +0000 | |
---|---|---|
committer | 2002-03-17 04:57:32 +0000 | |
commit | 1a750105e7d9630acf44dd0833cdc34578a0aea5 (patch) | |
tree | 5165a4abf83dec76bca5fc37fdc1403e23c0bb58 /contrib/field/field.ml4 | |
parent | 6e616fea2b9e153b04232537b7ee2539409521ac (diff) |
Meilleure gestion de la reduction dans Field
Field term (nouveau)
Injections dans l'interpreteur de tactiques
Exportation de quelques entrees de grammaires
Exportation de quelques fonctionnalites des definitions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2538 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/field/field.ml4')
-rw-r--r-- | contrib/field/field.ml4 | 40 |
1 files changed, 38 insertions, 2 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 10e22b86c..1edf302e0 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -11,10 +11,12 @@ (* $Id$ *) open Names +open Pp open Proof_type open Tacinterp open Tacmach open Term +open Typing open Util open Vernacinterp @@ -77,7 +79,10 @@ let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth 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)) + begin + let _ = type_of (Global.env ()) Evd.empty th in (); + Lib.add_anonymous_leaf (in_addfield (a,th)) + end end (* Vernac command declaration *) @@ -128,5 +133,36 @@ let field g = | [id:t |- ?] -> Rewrite id;Reflexivity)|Field_Gen FT] | [|- (eqT ? ? ?)] -> Field_Gen FT>>) 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 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 = + let env = (pf_env g) + and evc = (project g) in + let th = constrIn (guess_theory env evc l) + and nl = List.map constrIn (Quote.sort_subterm g l) in + (List.fold_right + (fun c a -> + let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in + tclTHENSI tac [a]) nl tclIDTAC) g + +(* Gives the constr list from the tactic_arg list *) +let targ_constr = + List.map + (fun e -> + match e with + | Constr c -> c + | _ -> anomaly "Field: must be a constr") + (* Declaration of Field *) -let _ = hide_tactic "Field" (function _ -> field) +let _ = hide_tactic "Field" + (fun l -> if l = [] then field else field_term (targ_constr l)) |