summaryrefslogtreecommitdiff
path: root/contrib/field
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/field')
-rw-r--r--contrib/field/Field.v2
-rw-r--r--contrib/field/Field_Compl.v2
-rw-r--r--contrib/field/Field_Tactic.v154
-rw-r--r--contrib/field/Field_Theory.v2
-rw-r--r--contrib/field/field.ml420
5 files changed, 90 insertions, 90 deletions
diff --git a/contrib/field/Field.v b/contrib/field/Field.v
index 7b48e275..3cc097fc 100644
--- a/contrib/field/Field.v
+++ b/contrib/field/Field.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Field.v,v 1.6.2.1 2004/07/16 19:30:09 herbelin Exp $ *)
+(* $Id: Field.v 5920 2004-07-16 20:01:26Z herbelin $ *)
Require Export Field_Compl.
Require Export Field_Theory.
diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v
index cba921f7..774b3084 100644
--- a/contrib/field/Field_Compl.v
+++ b/contrib/field/Field_Compl.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Field_Compl.v,v 1.8.2.1 2004/07/16 19:30:09 herbelin Exp $ *)
+(* $Id: Field_Compl.v 5920 2004-07-16 20:01:26Z herbelin $ *)
Inductive listT (A:Type) : Type :=
| nilT : listT A
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index c5c06547..afa0a814 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Field_Tactic.v,v 1.20.2.1 2004/07/16 19:30:09 herbelin Exp $ *)
+(* $Id: Field_Tactic.v 8134 2006-03-05 16:39:17Z herbelin $ *)
Require Import Ring.
Require Export Field_Compl.
@@ -14,6 +14,10 @@ Require Export Field_Theory.
(**** Interpretation A --> ExprA ****)
+Ltac get_component a s := eval cbv beta iota delta [a] in (a s).
+
+Ltac body_of s := eval cbv beta iota delta [s] in s.
+
Ltac mem_assoc var lvar :=
match constr:lvar with
| (nilT _) => constr:false
@@ -24,49 +28,46 @@ Ltac mem_assoc var lvar :=
end
end.
-Ltac seek_var_aux FT lvar trm :=
- let AT := eval cbv beta iota delta [A] in (A FT)
- with AzeroT := eval cbv beta iota delta [Azero] in (Azero FT)
- with AoneT := eval cbv beta iota delta [Aone] in (Aone FT)
- with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
- with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
- with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
- with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in
- match constr:trm with
- | AzeroT => lvar
- | AoneT => lvar
- | (AplusT ?X1 ?X2) =>
- let l1 := seek_var_aux FT lvar X1 in
- seek_var_aux FT l1 X2
- | (AmultT ?X1 ?X2) =>
- let l1 := seek_var_aux FT lvar X1 in
- seek_var_aux FT l1 X2
- | (AoppT ?X1) => seek_var_aux FT lvar X1
- | (AinvT ?X1) => seek_var_aux FT lvar X1
- | ?X1 =>
- let res := mem_assoc X1 lvar in
- match constr:res with
- | true => lvar
- | false => constr:(consT AT X1 lvar)
- end
- end.
-
-Ltac seek_var FT trm :=
- let AT := eval cbv beta iota delta [A] in (A FT) in
- seek_var_aux FT (nilT AT) trm.
-
-Ltac number_aux lvar cpt :=
- match constr:lvar with
- | (nilT ?X1) => constr:(nilT (prodT X1 nat))
- | (consT ?X1 ?X2 ?X3) =>
- let l2 := number_aux X3 (S cpt) in
- constr:(consT (prodT X1 nat) (pairT X1 nat X2 cpt) l2)
- end.
-
-Ltac number lvar := number_aux lvar 0.
-
-Ltac build_varlist FT trm := let lvar := seek_var FT trm in
- number lvar.
+Ltac number lvar :=
+ let rec number_aux lvar cpt :=
+ match constr:lvar with
+ | (nilT ?X1) => constr:(nilT (prodT X1 nat))
+ | (consT ?X1 ?X2 ?X3) =>
+ let l2 := number_aux X3 (S cpt) in
+ constr:(consT (prodT X1 nat) (pairT X1 nat X2 cpt) l2)
+ end
+ in number_aux lvar 0.
+
+Ltac build_varlist FT trm :=
+ let rec seek_var lvar trm :=
+ let AT := get_component A FT
+ with AzeroT := get_component Azero FT
+ with AoneT := get_component Aone FT
+ with AplusT := get_component Aplus FT
+ with AmultT := get_component Amult FT
+ with AoppT := get_component Aopp FT
+ with AinvT := get_component Ainv FT in
+ match constr:trm with
+ | AzeroT => lvar
+ | AoneT => lvar
+ | (AplusT ?X1 ?X2) =>
+ let l1 := seek_var lvar X1 in
+ seek_var l1 X2
+ | (AmultT ?X1 ?X2) =>
+ let l1 := seek_var lvar X1 in
+ seek_var l1 X2
+ | (AoppT ?X1) => seek_var lvar X1
+ | (AinvT ?X1) => seek_var lvar X1
+ | ?X1 =>
+ let res := mem_assoc X1 lvar in
+ match constr:res with
+ | true => lvar
+ | false => constr:(consT AT X1 lvar)
+ end
+ end in
+ let AT := get_component A FT in
+ let lvar := seek_var (nilT AT) trm in
+ number lvar.
Ltac assoc elt lst :=
match constr:lst with
@@ -79,13 +80,13 @@ Ltac assoc elt lst :=
end.
Ltac interp_A FT lvar trm :=
- let AT := eval cbv beta iota delta [A] in (A FT)
- with AzeroT := eval cbv beta iota delta [Azero] in (Azero FT)
- with AoneT := eval cbv beta iota delta [Aone] in (Aone FT)
- with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
- with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
- with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
- with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in
+ let AT := get_component A FT
+ with AzeroT := get_component Azero FT
+ with AoneT := get_component Aone FT
+ with AplusT := get_component Aplus FT
+ with AmultT := get_component Amult FT
+ with AoppT := get_component Aopp FT
+ with AinvT := get_component Ainv FT in
match constr:trm with
| AzeroT => constr:EAzero
| AoneT => constr:EAone
@@ -181,18 +182,17 @@ Ltac weak_reduce :=
Ltac multiply mul :=
match goal with
- | |- (interp_ExprA ?X1 ?X2 ?X3 = interp_ExprA ?X1 ?X2 ?X4) =>
- let AzeroT := eval cbv beta iota delta [Azero X1] in (Azero X1) in
- (cut (interp_ExprA X1 X2 mul <> AzeroT);
- [ intro; let id := grep_mult in
- apply (mult_eq X1 X3 X4 mul X2 id)
+ | |- (interp_ExprA ?FT ?X2 ?X3 = interp_ExprA ?FT ?X2 ?X4) =>
+ let AzeroT := get_component Azero FT in
+ (cut (interp_ExprA FT X2 mul <> AzeroT);
+ [ intro; let id := grep_mult in apply (mult_eq FT X3 X4 mul X2 id)
| weak_reduce;
- let AoneT := eval cbv beta iota delta [Aone X1] in (Aone X1)
- with AmultT := eval cbv beta iota delta [Amult X1] in (Amult X1) in
+ let AoneT := get_component Aone ltac:(body_of FT)
+ with AmultT := get_component Amult ltac:(body_of FT) in
(try
match goal with
- | |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r X1)
- end; clear X1 X2) ])
+ | |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r FT)
+ end; clear FT X2) ])
end.
Ltac apply_multiply FT lvar trm :=
@@ -219,10 +219,10 @@ Ltac apply_inverse mul FT lvar trm :=
Ltac strong_fail tac := first [ tac | fail 2 ].
Ltac inverse_test_aux FT trm :=
- let AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
- with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
- with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
- with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in
+ let AplusT := get_component Aplus FT
+ with AmultT := get_component Amult FT
+ with AoppT := get_component Aopp FT
+ with AinvT := get_component Ainv FT in
match constr:trm with
| (AinvT _) => fail 1
| (AoppT ?X1) =>
@@ -235,7 +235,7 @@ Ltac inverse_test_aux FT trm :=
end.
Ltac inverse_test FT :=
- let AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT) in
+ let AplusT := get_component Aplus FT in
match goal with
| |- (?X1 = ?X2) => inverse_test_aux FT (AplusT X1 X2)
end.
@@ -253,27 +253,27 @@ Ltac apply_simplif sfun :=
end.
Ltac unfolds FT :=
- match eval cbv beta iota delta [Aminus] in (Aminus FT) with
+ match get_component Aminus FT with
| (Field_Some _ ?X1) => unfold X1 in |- *
| _ => idtac
end;
- match eval cbv beta iota delta [Adiv] in (Adiv FT) with
+ match get_component Adiv FT with
| (Field_Some _ ?X1) => unfold X1 in |- *
| _ => idtac
end.
Ltac reduce FT :=
- let AzeroT := eval cbv beta iota delta [Azero] in (Azero FT)
- with AoneT := eval cbv beta iota delta [Aone] in (Aone FT)
- with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
- with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
- with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
- with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in
+ let AzeroT := get_component Azero FT
+ with AoneT := get_component Aone FT
+ with AplusT := get_component Aplus FT
+ with AmultT := get_component Amult FT
+ with AoppT := get_component Aopp FT
+ with AinvT := get_component Ainv FT in
(cbv beta iota zeta delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] in |- * ||
compute in |- *).
Ltac field_gen_aux FT :=
- let AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT) in
+ let AplusT := get_component Aplus FT in
match goal with
| |- (?X1 = ?X2) =>
let lvar := build_varlist FT (AplusT X1 X2) in
@@ -303,11 +303,11 @@ Ltac field_gen FT := unfolds FT; (inverse_test FT; ring) || field_gen_aux FT.
Ltac init_exp FT trm :=
let e :=
- (match eval cbv beta iota delta [Aminus] in (Aminus FT) with
+ (match get_component Aminus FT with
| (Field_Some _ ?X1) => eval cbv beta delta [X1] in trm
| _ => trm
end) in
- match eval cbv beta iota delta [Adiv] in (Adiv FT) with
+ match get_component Adiv FT with
| (Field_Some _ ?X1) => eval cbv beta delta [X1] in e
| _ => e
end.
@@ -429,4 +429,4 @@ Ltac field_term FT exp :=
simpl_all_monomials
ltac:(assoc_distrib ltac:(simpl_all_monomials ltac:(simpl_inv tma))) in
let trep := eval_weak_reduce (interp_ExprA FT lvar tsmp) in
- (replace exp with trep; [ ring trep | field_gen FT ]). \ No newline at end of file
+ (replace exp with trep; [ ring trep | field_gen FT ]).
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index 8737fd79..2c954652 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Field_Theory.v,v 1.12.2.1 2004/07/16 19:30:09 herbelin Exp $ *)
+(* $Id: Field_Theory.v 5920 2004-07-16 20:01:26Z herbelin $ *)
Require Import Peano_dec.
Require Import Ring.
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 32adec66..35591f23 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: field.ml4,v 1.33.2.1 2004/07/16 19:30:09 herbelin Exp $ *)
+(* $Id: field.ml4 7837 2006-01-11 09:47:32Z herbelin $ *)
open Names
open Pp
@@ -21,6 +21,7 @@ open Util
open Vernacinterp
open Vernacexpr
open Tacexpr
+open Mod_subst
(* Interpretation of constr's *)
let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
@@ -43,7 +44,7 @@ let lookup env typ =
with Not_found ->
errorlabstrm "field"
(str "No field is declared for type" ++ spc() ++
- Printer.prterm_env env typ)
+ Printer.pr_lconstr_env env typ)
let _ =
let init () = th_tab := Gmap.empty in
@@ -113,8 +114,8 @@ END
*)
(* For the translator, otherwise the code above is OK *)
-open Ppconstrnew
-let pp_minus_div_arg _prc _prt (omin,odiv) =
+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 ++
@@ -149,8 +150,7 @@ END
(* Guesses the type and calls field_gen with the right theory *)
let field g =
- Library.check_required_library ["Coq";"field";"Field"];
- let ist = { lfun=[]; debug=get_debug () } in
+ Coqlib.check_required_library ["Coq";"field";"Field"];
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
@@ -172,7 +172,7 @@ let guess_theory env evc = function
(* Guesses the type and calls Field_Term with the right theory *)
let field_term l g =
- Library.check_required_library ["Coq";"field";"Field"];
+ Coqlib.check_required_library ["Coq";"field";"Field"];
let env = (pf_env g)
and evc = (project g) in
let th = valueIn (VConstr (guess_theory env evc l))
@@ -184,7 +184,7 @@ let field_term l g =
(* Declaration of Field *)
-TACTIC EXTEND Field
-| [ "Field" ] -> [ field ]
-| [ "Field" ne_constr_list(l) ] -> [ field_term l ]
+TACTIC EXTEND field
+| [ "field" ] -> [ field ]
+| [ "field" ne_constr_list(l) ] -> [ field_term l ]
END
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 11:28:09 +0000