diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-08-06 16:15:08 -0400 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-08-06 16:17:55 -0400 |
| commit | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch) | |
| tree | c413c5bb42d20daf5307634ae6402526bb994fd6 /plugins | |
| parent | b9f47391f7f259c24119d1de0a87839e2cc5e80c (diff) | |
Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg
Diffstat (limited to 'plugins')
116 files changed, 658 insertions, 1035 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index c2f19c4f..4171aceb 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ccalgo.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* This file implements the basic congruence-closure algorithm by *) (* Downey,Sethi and Tarjan. *) diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 02e03a97..2825be1a 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ccalgo.mli 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Term diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index cb1f4725..5ee17b6e 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ccproof.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* This file uses the (non-compressed) union-find structure to generate *) (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index 141d2e13..4c75f9b0 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ccproof.mli 13323 2010-07-24 15:57:30Z herbelin $ *) open Ccalgo open Names diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 2f8a4527..b7358121 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: cctac.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* This file is the interface between the c-c algorithm and Coq *) diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index 05200a33..1c07cabf 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: cctac.mli 13323 2010-07-24 15:57:30Z herbelin $ *) open Term open Proof_type diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 722e7fa4..bed77a7b 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: g_congruence.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Cctac open Tactics diff --git a/plugins/dp/Dp.v b/plugins/dp/Dp.v index bc7d73f6..5ddc4452 100644 --- a/plugins/dp/Dp.v +++ b/plugins/dp/Dp.v @@ -6,7 +6,7 @@ Require Export Classical. (* Zenon *) (* Copyright 2004 INRIA *) -(* $Id$ *) +(* $Id: Dp.v 12337 2009-09-17 15:58:14Z glondu $ *) Lemma zenon_nottrue : (~True -> False). diff --git a/plugins/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4 index d28873a0..9c61aad5 100644 --- a/plugins/dp/g_dp.ml4 +++ b/plugins/dp/g_dp.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: g_dp.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Dp diff --git a/plugins/dp/zenon.v b/plugins/dp/zenon.v index 502465c6..f2400a7f 100644 --- a/plugins/dp/zenon.v +++ b/plugins/dp/zenon.v @@ -1,5 +1,5 @@ (* Copyright 2004 INRIA *) -(* $Id$ *) +(* $Id: zenon.v 11996 2009-03-20 01:22:58Z letouzey $ *) Require Export Classical. diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v index c9556972..882bcae9 100644 --- a/plugins/extraction/ExtrOcamlBasic.v +++ b/plugins/extraction/ExtrOcamlBasic.v @@ -8,6 +8,8 @@ (** Extraction to Ocaml : use of basic Ocaml types *) +Scheme Equality for nat. + Extract Inductive bool => bool [ true false ]. Extract Inductive option => option [ Some None ]. Extract Inductive unit => unit [ "()" ]. diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 72429055..ca72f873 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: common.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) open Pp open Util diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 0d2258a8..619cddfb 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: common.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Names open Libnames diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 36df8d16..58d8fcb1 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: extract_env.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) open Term open Declarations diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 7520e6c8..b4516898 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: extract_env.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*s This module declares the extraction commands. *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index f031094a..057057d1 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: extraction.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Util diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 394e5ab7..0574b009 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: extraction.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*s Extraction from Coq terms to Miniml. *) diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index dd1e7149..57b7c365 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: haskell.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) (*s Production of Haskell syntax. *) diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli index 915b8a95..0b68e73b 100644 --- a/plugins/extraction/haskell.mli +++ b/plugins/extraction/haskell.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: haskell.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) val haskell_descr : Miniml.language_descr diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index d768ec96..7ff11b90 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: miniml.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*s Target language for extraction: a core ML called MiniML. *) diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 2c63e588..745a78fe 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: mlutil.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Pp diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index a692e6d5..d6b85f12 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: mlutil.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Util open Names diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 8369ba91..15145344 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: modutil.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) open Names open Declarations diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index 5a159dc7..bb405d60 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: modutil.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Names open Declarations diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index ae8ec249..36ca3713 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ocaml.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) (*s Production of Ocaml syntax. *) diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli index 646b1c8b..477b4351 100644 --- a/plugins/extraction/ocaml.mli +++ b/plugins/extraction/ocaml.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ocaml.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) val ocaml_descr : Miniml.language_descr diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 82fac0b6..fa293ba1 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: scheme.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) (*s Production of Scheme syntax. *) diff --git a/plugins/extraction/scheme.mli b/plugins/extraction/scheme.mli index 7bb97cf9..e413d31e 100644 --- a/plugins/extraction/scheme.mli +++ b/plugins/extraction/scheme.mli @@ -6,6 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: scheme.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) val scheme_descr : Miniml.language_descr diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index e33e1e06..fd640388 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: table.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) open Names open Term diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 96592f19..a3199b50 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: table.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Names open Libnames diff --git a/plugins/field/LegacyField.v b/plugins/field/LegacyField.v index b0e1bc97..6c825353 100644 --- a/plugins/field/LegacyField.v +++ b/plugins/field/LegacyField.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: LegacyField.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export LegacyField_Compl. Require Export LegacyField_Theory. diff --git a/plugins/field/LegacyField_Compl.v b/plugins/field/LegacyField_Compl.v index 6d4e49ab..a3b46900 100644 --- a/plugins/field/LegacyField_Compl.v +++ b/plugins/field/LegacyField_Compl.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: LegacyField_Compl.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import List. diff --git a/plugins/field/LegacyField_Tactic.v b/plugins/field/LegacyField_Tactic.v index 1b04c11a..9c92e38a 100644 --- a/plugins/field/LegacyField_Tactic.v +++ b/plugins/field/LegacyField_Tactic.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: LegacyField_Tactic.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import List. Require Import LegacyRing. diff --git a/plugins/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v index c7eed29a..2407026f 100644 --- a/plugins/field/LegacyField_Theory.v +++ b/plugins/field/LegacyField_Theory.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: LegacyField_Theory.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import List. Require Import Peano_dec. diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 6d3cb25c..47f52370 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: field.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Names open Pp diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 93c4504c..d039a930 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: formula.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Hipattern open Names diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 558eb876..fbb103c0 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: formula.mli 13323 2010-07-24 15:57:30Z herbelin $ *) open Term open Names diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 7451bcd2..19b63407 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: g_ground.ml4 13344 2010-07-28 15:04:36Z msozeau $ *) open Formula open Sequent @@ -54,7 +54,21 @@ let _= in declare_int_option gdopt -let default_solver=(Tacinterp.interp <:tactic<auto with *>>) +let (set_default_solver, default_solver, print_default_solver) = + Tactic_option.declare_tactic_option ~default:(<:tactic<auto with *>>) "Firstorder default solver" + +VERNAC COMMAND EXTEND Firstorder_Set_Solver +| [ "Set" "Firstorder" "Solver" tactic(t) ] -> [ + set_default_solver + (Vernacexpr.use_section_locality ()) + (Tacinterp.glob_tactic t) ] +END + +VERNAC COMMAND EXTEND Firstorder_Print_Solver +| [ "Print" "Firstorder" "Solver" ] -> [ + Pp.msgnl + (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ] +END let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") @@ -65,7 +79,7 @@ let gen_ground_tac flag taco ids bases gl= let solver= match taco with Some tac-> tac - | None-> default_solver in + | None-> snd (default_solver ()) in let startseq gl= let seq=empty_seq !ground_depth in extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in @@ -137,7 +151,7 @@ let default_declarative_automation gls = (Cctac.congruence_tac !congruence_depth [])) (gen_ground_tac true (Some (tclTHEN - default_solver + (snd (default_solver ())) (Cctac.congruence_tac !congruence_depth []))) [] []) gls diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 766fa0d3..354bcda2 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ground.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Formula open Sequent diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli index 3daf66d6..ba8051da 100644 --- a/plugins/firstorder/ground.mli +++ b/plugins/firstorder/ground.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ground.mli 13323 2010-07-24 15:57:30Z herbelin $ *) val ground_tac: Tacmach.tactic -> (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 7da65f08..714604ae 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: instances.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) open Formula open Sequent diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index 49716cc6..8b913719 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: instances.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Term open Tacmach diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index a35173cd..9cff67dc 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: rules.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Names diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index 070c1dbe..ec6d2bd0 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: rules.mli 13323 2010-07-24 15:57:30Z herbelin $ *) open Term open Tacmach diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 43be5714..1d439693 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: sequent.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Term open Util diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index c310aaff..1232f1e8 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: sequent.mli 13323 2010-07-24 15:57:30Z herbelin $ *) open Term open Util diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 27eca654..835b0409 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: unify.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) open Util open Formula diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli index 1412a23e..af2ce01d 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: unify.mli 13323 2010-07-24 15:57:30Z herbelin $ *) open Term diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v index 2304ddbe..05e85cde 100644 --- a/plugins/fourier/Fourier.v +++ b/plugins/fourier/Fourier.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Fourier.v 13323 2010-07-24 15:57:30Z herbelin $ *) (* "Fourier's method to solve linear inequations/equations systems.".*) diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v index 152bbc04..3cd26cb8 100644 --- a/plugins/fourier/Fourier_util.v +++ b/plugins/fourier/Fourier_util.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Fourier_util.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export Rbase. Comments "Lemmas used by the tactic Fourier". diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml index 081246da..16123fd7 100644 --- a/plugins/fourier/fourier.ml +++ b/plugins/fourier/fourier.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: fourier.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* Méthode d'élimination de Fourier *) (* Référence: diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 0af2849e..e9392e78 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: fourierR.ml 13323 2010-07-24 15:57:30Z herbelin $ *) diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 index c6976ff7..d3b8228d 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: g_fourier.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open FourierR diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index e2cad944..3590e698 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1345,7 +1345,6 @@ and acc_inv_id = Recdef.acc_inv_id and ltof_ref = Recdef.ltof_ref and acc_rel = Recdef.acc_rel and well_founded = Recdef.well_founded -and delayed_force = Recdef.delayed_force and h_intros = Recdef.h_intros and list_rewrite = Recdef.list_rewrite and evaluable_of_global_reference = Recdef.evaluable_of_global_reference diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 38f42844..f5a5fbd4 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -169,9 +169,8 @@ let build_newrecursive let arityc = Topconstr.prod_constr_expr arityc bl in let arity = Constrintern.interp_type sigma env0 arityc in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in - (Environ.push_named (recname,None,arity) env, (recname,impl) :: impls)) + (Environ.push_named (recname,None,arity) env, (recname, impl) :: impls)) (env0,[]) lnameargsardef in - let rec_impls = Constrintern.set_internalization_env_params rec_impls [] in let recdef = (* Declare local notations *) let fs = States.freeze() in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 7b592c2a..9c4cc78a 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: recdef.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Term open Termops @@ -281,8 +281,6 @@ let find_reference sl s = (List.map id_of_string (List.rev sl))) (id_of_string s)));; -let delayed_force f = f () - let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") let le_lt_n_Sm = function () -> (coq_base_constant "le_lt_n_Sm") diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 2296c6e2..3b667bf6 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -14,7 +14,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: g_micromega.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Quote open Ring diff --git a/plugins/nsatz/Nsatz_domain.v b/plugins/nsatz/Nsatz.v index 5e0ae4ef..aa32b386 100644 --- a/plugins/nsatz/Nsatz_domain.v +++ b/plugins/nsatz/Nsatz.v @@ -7,13 +7,14 @@ (************************************************************************) (* - Tactic nsatz: proofs of polynomials equalities with variables in R. - Uses Hilbert Nullstellensatz and Buchberger algorithm. - Thanks to B.Gregoire for the verification of the certicate - and L.Thery for help on ring tactic, - and to B.Barras for modularization of the ocaml code. - Example: see test-suite/success/Nsatz.v - L.Pottier, june 2010 + Tactic nsatz: proofs of polynomials equalities in a domain (ring without zero divisor). + Reification is done by type classes, following a technique shown by Mathieu +Sozeau. Verification of certificate is done by a code written by Benjamin +Gregoire, following an idea of Laurent Théry. + +Examples: see test-suite/success/Nsatz.v + +Loïc Pottier, july 2010 *) Require Import List. @@ -22,10 +23,10 @@ Require Import BinPos. Require Import BinList. Require Import Znumtheory. Require Import Ring_polynom Ring_tac InitialRing. +Require Export Morphisms Setoid Bool. Declare ML Module "nsatz_plugin". - Class Zero (A : Type) := {zero : A}. Notation "0" := zero. Class One (A : Type) := {one : A}. @@ -40,25 +41,37 @@ Class Opposite (A : Type) := {opposite : A -> A}. Notation "- x" := (opposite x). Class Ring (R:Type) := { - ring0: R; ring1: R; - ring_plus: R->R->R; ring_mult: R->R->R; - ring_sub: R->R->R; ring_opp: R->R; - ring_ring: - ring_theory ring0 ring1 ring_plus ring_mult ring_sub - ring_opp (@eq R)}. + ring0: R; ring1: R; + ring_plus: R->R->R; ring_mult: R->R->R; + ring_sub: R->R->R; ring_opp: R->R; + ring_eq : R -> R -> Prop; + ring_ring: + ring_theory ring0 ring1 ring_plus ring_mult ring_sub + ring_opp ring_eq; + ring_setoid: Equivalence ring_eq; + ring_plus_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_plus; + ring_mult_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_mult; + ring_sub_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_sub; + ring_opp_comp: Proper (ring_eq==>ring_eq) ring_opp +}. Class Domain (R : Type) := { domain_ring:> Ring R; domain_axiom_product: - forall x y, ring_mult x y = ring0 -> x = ring0 \/ y = ring0; - domain_axiom_one_zero: ring1 <> ring0}. - -Ltac ring2 := simpl; ring. + forall x y, ring_eq (ring_mult x y) ring0 -> (ring_eq x ring0) \/ (ring_eq y ring0); + domain_axiom_one_zero: not (ring_eq ring1 ring0)}. Section domain. Variable R: Type. Variable Rd: Domain R. + +Existing Instance ring_setoid. +Existing Instance ring_plus_comp. +Existing Instance ring_mult_comp. +Existing Instance ring_sub_comp. +Existing Instance ring_opp_comp. + Add Ring Rr: (@ring_ring R (@domain_ring R Rd)). Instance zero_ring : Zero R := {zero := ring0}. @@ -68,24 +81,27 @@ Instance multiplication_ring : Multiplication R := {multiplication x y := ring_m Instance subtraction_ring : Subtraction R := {subtraction x y := ring_sub x y}. Instance opposite_ring : Opposite R := {opposite x := ring_opp x}. -Lemma psos_r1b: forall x y:R, x - y = 0 -> x = y. -intros x y H; replace x with ((x - y) + y); - [rewrite H | idtac]; ring2. -Qed. +Infix "==" := ring_eq (at level 70, no associativity). -Lemma psos_r1: forall x y, x = y -> x - y = 0. -intros x y H; rewrite H; ring2. +Lemma psos_r1b: forall x y:R, x - y == 0 -> x == y. +intros x y H; setoid_replace x with ((x - y) + y); simpl; + [setoid_rewrite H | idtac]; simpl; ring. Qed. +Lemma psos_r1: forall x y, x == y -> x - y == 0. +intros x y H; simpl; setoid_rewrite H; simpl; ring. +Qed. -Lemma nsatzR_diff: forall x y:R, x<>y -> x - y<>0. +Lemma nsatzR_diff: forall x y:R, not (x == y) -> not (x - y == 0). intros. intro; apply H. -replace x with ((x - y) + y) by ring2. -rewrite H0; ring2. +simpl; setoid_replace x with ((x - y) + y). simpl. +setoid_rewrite H0. +simpl; ring. +simpl. simpl; ring. Qed. -(* code de Benjamin *) +(* adpatation du code de Benjamin aux setoides *) Require Import ZArith. Definition PolZ := Pol Z. @@ -129,42 +145,43 @@ Definition PhiR : list R -> PolZ -> R := Definition pow (r : R) (n : nat) := pow_N 1 ring_mult r (Nnat.N_of_nat n). Definition PEevalR : list R -> PEZ -> R := - PEeval 0 ring_plus ring_mult ring_sub ring_opp + PEeval 0 ring_plus ring_mult ring_sub ring_opp (gen_phiZ 0 1 ring_plus ring_mult ring_opp) Nnat.nat_of_N pow. Lemma P0Z_correct : forall l, PhiR l P0Z = 0. Proof. trivial. Qed. -Lemma Rext: ring_eq_ext ring_plus ring_mult ring_opp eq. -apply mk_reqe. intros. rewrite H; rewrite H0; trivial. - intros. rewrite H; rewrite H0; trivial. -intros. rewrite H; trivial. Qed. - -Lemma Rset : Setoid_Theory R eq. -apply Eqsth. +Lemma Rext: ring_eq_ext ring_plus ring_mult ring_opp ring_eq. +apply mk_reqe. intros. setoid_rewrite H; rewrite H0; ring. + intros. setoid_rewrite H; setoid_rewrite H0; ring. +intros. setoid_rewrite H; ring. Qed. + +Lemma Rset : Setoid_Theory R ring_eq. +apply ring_setoid. Qed. Lemma PolZadd_correct : forall P' P l, - PhiR l (PolZadd P P') = ((PhiR l P) + (PhiR l P')). + PhiR l (PolZadd P P') == ((PhiR l P) + (PhiR l P')). Proof. +simpl. refine (Padd_ok Rset Rext (Rth_ARth Rset Rext (@ring_ring _ (@domain_ring _ Rd))) (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd)))). Qed. Lemma PolZmul_correct : forall P P' l, - PhiR l (PolZmul P P') = ((PhiR l P) * (PhiR l P')). + PhiR l (PolZmul P P') == ((PhiR l P) * (PhiR l P')). Proof. refine (Pmul_ok Rset Rext (Rth_ARth Rset Rext (@ring_ring _ (@domain_ring _ Rd))) (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd)))). Qed. Lemma R_power_theory - : power_theory 1 ring_mult eq Nnat.nat_of_N pow. -apply mkpow_th. unfold pow. intros. rewrite Nnat.N_of_nat_of_N. trivial. Qed. + : power_theory 1 ring_mult ring_eq Nnat.nat_of_N pow. +apply mkpow_th. unfold pow. intros. rewrite Nnat.N_of_nat_of_N. ring. Qed. Lemma norm_correct : - forall (l : list R) (pe : PEZ), PEevalR l pe = PhiR l (norm pe). + forall (l : list R) (pe : PEZ), PEevalR l pe == PhiR l (norm pe). Proof. intros;apply (norm_aux_spec Rset Rext (Rth_ARth Rset Rext (@ring_ring _ (@domain_ring _ Rd))) (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd))) R_power_theory) @@ -174,7 +191,7 @@ Qed. Lemma PolZeq_correct : forall P P' l, PolZeq P P' = true -> - PhiR l P = PhiR l P'. + PhiR l P == PhiR l P'. Proof. intros;apply (Peq_ok Rset Rext (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd))));trivial. @@ -183,17 +200,19 @@ Qed. Fixpoint Cond0 (A:Type) (Interp:A->R) (l:list A) : Prop := match l with | List.nil => True - | a::l => Interp a = 0 /\ Cond0 A Interp l + | a::l => Interp a == 0 /\ Cond0 A Interp l end. Lemma mult_l_correct : forall l la lp, Cond0 PolZ (PhiR l) lp -> - PhiR l (mult_l la lp) = 0. + PhiR l (mult_l la lp) == 0. Proof. - induction la;simpl;intros;trivial. - destruct lp;trivial. + induction la;simpl;intros. ring. + destruct lp;trivial. simpl. ring. simpl in H;destruct H. - rewrite PolZadd_correct, PolZmul_correct, H, IHla;[ring2 | trivial]. + setoid_rewrite PolZadd_correct. + simpl. setoid_rewrite PolZmul_correct. simpl. setoid_rewrite H. + setoid_rewrite IHla. unfold zero. simpl. ring. trivial. Qed. Lemma compute_list_correct : forall l lla lp, @@ -209,7 +228,7 @@ Lemma check_correct : forall l lpe qe certif, check lpe qe certif = true -> Cond0 PEZ (PEevalR l) lpe -> - PEevalR l qe = 0. + PEevalR l qe == 0. Proof. unfold check;intros l lpe qe (lla, lq) H2 H1. apply PolZeq_correct with (l:=l) in H2. @@ -221,53 +240,53 @@ Proof. rewrite <- norm_correct;auto. Qed. -(* fin du code de Benjamin *) +(* fin *) -Lemma pow_not_zero: forall p n, pow p n = 0 -> p = 0. -induction n. unfold pow; simpl. intros. absurd (1 = 0). +Lemma pow_not_zero: forall p n, pow p n == 0 -> p == 0. +induction n. unfold pow; simpl. intros. absurd (1 == 0). simpl. apply domain_axiom_one_zero. - trivial. replace (pow p (S n)) with (p * (pow p n)). intros. -case (@domain_axiom_product _ _ _ _ H). trivial. trivial. -unfold pow; simpl. -clear IHn. induction n; try ring2. simpl. - rewrite pow_pos_Psucc. trivial. exact Rset. - intros. rewrite H; rewrite H0; trivial. - intros. ring2. intros. ring2. Qed. + trivial. setoid_replace (pow p (S n)) with (p * (pow p n)). intros. +case (@domain_axiom_product _ _ _ _ H). trivial. trivial. +unfold pow; simpl. +clear IHn. induction n; simpl; try ring. + rewrite pow_pos_Psucc. ring. exact Rset. + intros. setoid_rewrite H; setoid_rewrite H0; ring. + intros. simpl; ring. intros. simpl; ring. Qed. -Lemma Rdomain_pow: forall c p r, ~c= 0 -> c * (pow p r)= 0 -> p = ring0. -intros. case (@domain_axiom_product _ _ _ _ H0). intros; absurd (c = 0); auto. -intros. apply pow_not_zero with r. trivial. Qed. +Lemma Rdomain_pow: forall c p r, ~c == ring0 -> ring_mult c (pow p r) == ring0 -> p == ring0. +intros. case (@domain_axiom_product _ _ _ _ H0). intros; absurd (c == ring0); auto. +intros. apply pow_not_zero with r. trivial. Qed. -Definition R2:= 1 + 1. +Definition R2:= ring_plus ring1 ring1. Fixpoint IPR p {struct p}: R := match p with - xH => 1 - | xO xH => 1 + 1 - | xO p1 => R2 + (IPR p1) - | xI xH => 1 + (1 + 1) - | xI p1 => 1 + (R2 * (IPR p1)) + xH => ring1 + | xO xH => ring_plus ring1 ring1 + | xO p1 => ring_mult R2 (IPR p1) + | xI xH => ring_plus ring1 (ring_plus ring1 ring1) + | xI p1 => ring_plus ring1 (ring_mult R2 (IPR p1)) end. Definition IZR1 z := - match z with Z0 => 0 + match z with Z0 => ring0 | Zpos p => IPR p - | Zneg p => -(IPR p) + | Zneg p => ring_opp(IPR p) end. Fixpoint interpret3 t fv {struct t}: R := match t with | (PEadd t1 t2) => let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 + v2) + let v2 := interpret3 t2 fv in (ring_plus v1 v2) | (PEmul t1 t2) => let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 * v2) + let v2 := interpret3 t2 fv in (ring_mult v1 v2) | (PEsub t1 t2) => let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 - v2) + let v2 := interpret3 t2 fv in (ring_sub v1 v2) | (PEopp t1) => - let v1 := interpret3 t1 fv in (- v1) + let v1 := interpret3 t1 fv in (ring_opp v1) | (PEpow t1 t2) => let v1 := interpret3 t1 fv in pow v1 (Nnat.nat_of_N t2) | (PEc t1) => (IZR1 t1) @@ -279,14 +298,11 @@ End domain. Ltac equalities_to_goal := lazymatch goal with - | H: (@eq _ ?x 0) |- _ => try revert H - | H: (@eq _ 0 ?x) |- _ => - try generalize (sym_equal H); clear H - | H: (@eq _ ?x ?y) |- _ => + | H: (@ring_eq _ _ ?x ?y) |- _ => try generalize (@psos_r1 _ _ _ _ H); clear H end. -Ltac nsatz_domain_begin tacsimpl:= +Ltac nsatz_domain_begin tacsimpl := intros; try apply (@psos_r1b _ _); repeat equalities_to_goal; @@ -295,7 +311,7 @@ Ltac nsatz_domain_begin tacsimpl:= Ltac generalise_eq_hyps:= repeat (match goal with - |h : (?p = ?q)|- _ => revert h + |h : (@ring_eq _ _ ?p ?q)|- _ => revert h end). Ltac lpol_goal t := @@ -328,9 +344,13 @@ Ltac rev l := | (cons ?x ?l) => let l' := rev l in append1 x l' end. -Ltac nsatz_call_n info nparam p rr lp kont := + + +Ltac nsatz_call_n info nparam p rr lp kont := + (*idtac "Trying power: " rr;*) let ll := constr:(PEc info :: PEc nparam :: PEpow p rr :: lp) in - nsatz_compute ll; + nsatz_compute ll; + (*idtac "done";*) match goal with | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ => intros _; @@ -344,7 +364,6 @@ Ltac nsatz_call radicalmax info nparam p lp kont := lazymatch n with | 0%N => fail | _ => -(* idtac "Trying power: " n;*) (let r := eval compute in (Nminus radicalmax (Npred n)) in nsatz_call_n info nparam p r lp kont) || let n' := eval compute in (Npred n) in try_n n' @@ -368,7 +387,7 @@ Definition li_find_at (R:Type) (b:R) l i `{Cfind_at R b l i} {H:Cclosed_seq (T:= Class Creify (R:Type) (e:PExpr Z) (l:list R) (b:R) := {}. Instance Ireify_zero (R:Type) (Rd:Domain R) l : Creify (PEc 0%Z) l ring0. Instance Ireify_one (R:Type) (Rd:Domain R) l : Creify (PEc 1%Z) l ring1. -Instance Ireify_plus (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2} +Instance Ireify_plus (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2} : Creify (PEadd e1 e2) l (ring_plus b1 b2). Instance Ireify_mult (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2} : Creify (PEmul e1 e2) l (ring_mult b1 b2). @@ -382,7 +401,7 @@ Instance Ireify_var (R:Type) b l i `{Cfind_at R b l i} Class Creifylist (R:Type) (le:list (PExpr Z)) (l:list R) (lb:list R) := {}. Instance Creify_nil (R:Type) l : Creifylist nil l (@nil R). -Instance Creify_cons (R:Type) e1 l b1 le2 lb2 `{Creify R e1 l b1} `{Creifylist R le2 l lb2} +Instance Creify_cons (R:Type) e1 l b1 le2 lb2 `{Creify R e1 l b1} `{Creifylist R le2 l lb2} : Creifylist (e1::le2) l (b1::lb2). Definition li_reifyl (R:Type) le l lb `{Creifylist R le l lb} @@ -392,29 +411,29 @@ Unset Implicit Arguments. Ltac lterm_goal g := match g with - ?b1 = ?b2 => constr:(b1::b2::nil) - | ?b1 = ?b2 -> ?g => let l := lterm_goal g in constr:(b1::b2::l) + ring_eq ?b1 ?b2 => constr:(b1::b2::nil) + | ring_eq ?b1 ?b2 -> ?g => let l := lterm_goal g in constr:(b1::b2::l) end. -Ltac reify_goal l le lb:= +Ltac reify_goal l le lb Rd:= match le with nil => idtac - | ?e::?le1 => + | ?e::?le1 => match lb with - ?b::?lb1 => + ?b::?lb1 => (* idtac "b="; idtac b;*) let x := fresh "B" in set (x:= b) at 1; - change x with (@interpret3 _ _ e l); - clear x; - reify_goal l le1 lb1 + change x with (@interpret3 _ Rd e l); + clear x; + reify_goal l le1 lb1 Rd end end. Ltac get_lpol g := match g with - (interpret3 _ _ ?p _) = _ => constr:(p::nil) - | (interpret3 _ _ ?p _) = _ -> ?g => - let l := get_lpol g in constr:(p::l) + ring_eq (interpret3 _ _ ?p _) _ => constr:(p::nil) + | ring_eq (interpret3 _ _ ?p _) _ -> ?g => + let l := get_lpol g in constr:(p::l) end. Ltac nsatz_domain_generic radicalmax info lparam lvar tacsimpl Rd := @@ -422,7 +441,7 @@ Ltac nsatz_domain_generic radicalmax info lparam lvar tacsimpl Rd := |- ?g => let lb := lterm_goal g in (*idtac "lb"; idtac lb;*) match eval red in (li_reifyl (lb:=lb)) with - | (?fv, ?le) => + | (?fv, ?le) => let fv := match lvar with (@nil _) => fv | _ => lvar @@ -431,64 +450,111 @@ Ltac nsatz_domain_generic radicalmax info lparam lvar tacsimpl Rd := let nparam := eval compute in (Z_of_nat (List.length lparam)) in let fv := parametres_en_tete fv lparam in (*idtac "variables:"; idtac fv; - idtac "nparam:"; idtac nparam;*) + idtac "nparam:"; idtac nparam; *) match eval red in (li_reifyl (l:=fv) (lb:=lb)) with - | (?fv, ?le) => - idtac "variables:";idtac fv; - reify_goal fv le lb; - match goal with - |- ?g => - let lp := get_lpol g in + | (?fv, ?le) => + (*idtac "variables:";idtac fv; idtac le; idtac lb;*) + reify_goal fv le lb Rd; + match goal with + |- ?g => + let lp := get_lpol g in let lpol := eval compute in (List.rev lp) in (*idtac "polynomes:"; idtac lpol;*) tacsimpl; intros; - + let SplitPolyList kont := match lpol with | ?p2::?lp2 => kont p2 lp2 | _ => idtac "polynomial not in the ideal" - end in - tacsimpl; + end in + tacsimpl; SplitPolyList ltac:(fun p lp => set (p21:=p) ; set (lp21:=lp); (*idtac "lp:"; idtac lp; *) - nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => - set (q := PEmul c (PEpow p21 r)); - let Hg := fresh "Hg" in - assert (Hg:check lp21 q (lci,lq) = true); + nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => + set (q := PEmul c (PEpow p21 r)); + let Hg := fresh "Hg" in + assert (Hg:check lp21 q (lci,lq) = true); [ (vm_compute;reflexivity) || idtac "invalid nsatz certificate" - | let Hg2 := fresh "Hg" in - assert (Hg2: interpret3 _ _ q fv = ring0); - [ tacsimpl; + | let Hg2 := fresh "Hg" in + assert (Hg2: ring_eq (interpret3 _ Rd q fv) ring0); + [ tacsimpl; apply (@check_correct _ Rd fv lp21 q (lci,lq) Hg); tacsimpl; repeat (split;[assumption|idtac]); exact I - | simpl in Hg2; tacsimpl; - apply Rdomain_pow with (interpret3 _ _ c fv) (Nnat.nat_of_N r); tacsimpl; - [ apply domain_axiom_one_zero || idtac "could not prove discrimination result" - | exact Hg2] + | simpl in Hg2; tacsimpl; + apply Rdomain_pow with (interpret3 _ Rd c fv) (Nnat.nat_of_N r); auto with domain; + tacsimpl; apply domain_axiom_one_zero + || (simpl) || idtac "could not prove discrimination result" ] ] -) +) ) end end end end . -Ltac nsatz_domainpv radicalmax info lparam lvar tacsimpl rd:= - nsatz_domain_begin tacsimpl; +Ltac nsatz_domainpv pretac radicalmax info lparam lvar tacsimpl rd := + pretac; + nsatz_domain_begin tacsimpl; auto with domain; nsatz_domain_generic radicalmax info lparam lvar tacsimpl rd. -Ltac nsatz_domain:= +Ltac nsatz_domain:= intros; match goal with - |- (@eq ?r _ _ ) => - let a := constr:(@Ireify_zero _ _ (@nil r)) in - match a with - (@Ireify_zero _ ?rd _) => - nsatz_domainpv 6%N 1%Z (@nil r) (@nil r) ltac:(simpl) rd - end + |- (@ring_eq _ (@domain_ring ?r ?rd) _ _ ) => + nsatz_domainpv ltac:idtac 6%N 1%Z (@nil r) (@nil r) ltac:(simpl) rd end. +(* Dans R *) +Require Import Reals. +Require Import RealField. + +Instance Rri : Ring R := { + ring0 := 0%R; + ring1 := 1%R; + ring_plus := Rplus; + ring_mult := Rmult; + ring_sub := Rminus; + ring_opp := Ropp; + ring_eq := @eq R; + ring_ring := RTheory}. + +Lemma Raxiom_one_zero: 1%R <> 0%R. +discrR. +Qed. + +Instance Rdi : Domain R := { + domain_ring := Rri; + domain_axiom_product := Rmult_integral; + domain_axiom_one_zero := Raxiom_one_zero}. + +Hint Resolve ring_setoid ring_plus_comp ring_mult_comp ring_sub_comp ring_opp_comp: domain. + +Ltac replaceR:= +replace 0%R with (@ring0 _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; +replace 1%R with (@ring1 _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; +replace Rplus with (@ring_plus _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; +replace Rmult with (@ring_mult _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; +replace Rminus with (@ring_sub _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; +replace Ropp with (@ring_opp _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; +replace (@eq R) with (@ring_eq _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]. + +Ltac simplR:= + simpl; replaceR. + +Ltac pretacR:= + replaceR; + replace Rri with (@domain_ring _ Rdi) in *; [idtac | reflexivity]. + +Ltac nsatz_domainR:= + nsatz_domainpv ltac:pretacR 6%N 1%Z (@Datatypes.nil R) (@Datatypes.nil R) + ltac:simplR Rdi; + discrR. + + +Goal forall x y:R, x = y -> (x*x-x+1)%R = ((y*y-y)+1+0)%R. +nsatz_domainR. +Qed. (* Dans Z *) @@ -498,7 +564,8 @@ Instance Zri : Ring Z := { ring_plus := Zplus; ring_mult := Zmult; ring_sub := Zminus; - ring_opp := Zopp; + ring_opp := Zopp; + ring_eq := (@eq Z); ring_ring := Zth}. Lemma Zaxiom_one_zero: 1%Z <> 0%Z. @@ -510,49 +577,87 @@ Instance Zdi : Domain Z := { domain_axiom_product := Zmult_integral; domain_axiom_one_zero := Zaxiom_one_zero}. +Ltac replaceZ := +replace 0%Z with (@ring0 _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; +replace 1%Z with (@ring1 _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; +replace Zplus with (@ring_plus _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; +replace Zmult with (@ring_mult _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; +replace Zminus with (@ring_sub _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; +replace Zopp with (@ring_opp _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; +replace (@eq Z) with (@ring_eq _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]. Ltac simplZ:= - simpl; -replace 0%Z with (@ring0 _ (@domain_ring _ Zdi));[idtac|reflexivity]; -replace 1%Z with (@ring1 _ (@domain_ring _ Zdi));[idtac|reflexivity]; -replace Zplus with (@ring_plus _ (@domain_ring _ Zdi));[idtac|reflexivity]; -replace Zmult with (@ring_mult _ (@domain_ring _ Zdi));[idtac|reflexivity]; -replace Zminus with (@ring_sub _ (@domain_ring _ Zdi));[idtac|reflexivity]; -replace Zopp with (@ring_opp _ (@domain_ring _ Zdi));[idtac|reflexivity]. + simpl; replaceZ. -Ltac nsatz_domainZ:= nsatz_domainpv 6%N 1%Z (@nil Z) (@nil Z) ltac:simplZ Zdi. +Ltac pretacZ := +replaceZ; +replace Zri with (@domain_ring _ Zdi) in *; [idtac | reflexivity]. +Ltac nsatz_domainZ:= +nsatz_domainpv ltac:pretacZ 6%N 1%Z (@Datatypes.nil Z) (@Datatypes.nil Z) ltac:simplZ Zdi. -(* Dans R *) -Require Import Reals. -Require Import RealField. -Instance Rri : Ring R := { - ring0 := 0%R; - ring1 := 1%R; - ring_plus := Rplus; - ring_mult := Rmult; - ring_sub := Rminus; - ring_opp := Ropp; - ring_ring := RTheory}. +(* Dans Q *) +Require Import QArith. -Lemma Raxiom_one_zero: 1%R <> 0%R. -discrR. +Instance Qri : Ring Q := { + ring0 := 0%Q; + ring1 := 1%Q; + ring_plus := Qplus; + ring_mult := Qmult; + ring_sub := Qminus; + ring_opp := Qopp; + ring_eq := Qeq; + ring_ring := Qsrt}. + +Lemma Qaxiom_one_zero: not (Qeq 1%Q 0%Q). +discriminate. Qed. -Instance Rdi : Domain R := { - domain_ring := Rri; - domain_axiom_product := Rmult_integral; - domain_axiom_one_zero := Raxiom_one_zero}. +Instance Qdi : Domain Q := { + domain_ring := Qri; + domain_axiom_product := Qmult_integral; + domain_axiom_one_zero := Qaxiom_one_zero}. +Ltac replaceQ := +replace 0%Q with (@ring0 _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; +replace 1%Q with (@ring1 _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; +replace Qplus with (@ring_plus _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; +replace Qmult with (@ring_mult _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; +replace Qminus with (@ring_sub _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; +replace Qopp with (@ring_opp _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; +replace Qeq with (@ring_eq _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]. -Ltac simplR:= - simpl; -replace 0%R with (@ring0 _ (@domain_ring _ Rdi));[idtac|reflexivity]; -replace 1%R with (@ring1 _ (@domain_ring _ Rdi));[idtac|reflexivity]; -replace Rplus with (@ring_plus _ (@domain_ring _ Rdi));[idtac|reflexivity]; -replace Rmult with (@ring_mult _ (@domain_ring _ Rdi));[idtac|reflexivity]; -replace Rminus with (@ring_sub _ (@domain_ring _ Rdi));[idtac|reflexivity]; -replace Ropp with (@ring_opp _ (@domain_ring _ Rdi));[idtac|reflexivity]. - -Ltac nsatz_domainR:= nsatz_domainpv 6%N 1%Z (@List.nil R) (@List.nil R) ltac:simplR Rdi. +Ltac simplQ:= + simpl; replaceQ. + +Ltac pretacQ := +replaceQ; +replace Qri with (@domain_ring _ Qdi) in *; [idtac | reflexivity]. + +Ltac nsatz_domainQ:= +nsatz_domainpv ltac:pretacQ 6%N 1%Z (@Datatypes.nil Q) (@Datatypes.nil Q) ltac:simplQ Qdi. + +(* tactique générique *) + +Ltac nsatz := + intros; + match goal with + | |- (@eq R _ _) => nsatz_domainR + | |- (@eq Z _ _) => nsatz_domainZ + | |- (@Qeq _ _) => nsatz_domainQ + | |- _ => nsatz_domain + end. +(* +Goal forall x y:Q, Qeq x y -> Qeq (x*x-x+1)%Q ((y*y-y)+1+0)%Q. +nsatz. +Qed. + +Goal forall x y:Z, x = y -> (x*x-x+1)%Z = ((y*y-y)+1+0)%Z. +nsatz. +Qed. + +Goal forall x y:R, x = y -> (x*x-x+1)%R = ((y*y-y)+1+0)%R. +nsatz. +Qed. +*) diff --git a/plugins/nsatz/NsatzR.v b/plugins/nsatz/NsatzR.v deleted file mode 100644 index 41e02c76..00000000 --- a/plugins/nsatz/NsatzR.v +++ /dev/null @@ -1,407 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* - Tactic nsatz: proofs of polynomials equalities with variables in R. - Uses Hilbert Nullstellensatz and Buchberger algorithm. - Thanks to B.Gregoire and L.Thery for help on ring tactic, - and to B.Barras for modularization of the ocaml code. - Example: see test-suite/success/Nsatz.v - L.Pottier, june 2010 -*) - -Require Import List. -Require Import Setoid. -Require Import BinPos. -Require Import BinList. -Require Import Znumtheory. -Require Import RealField Rdefinitions Rfunctions RIneq DiscrR. -Require Import Ring_polynom Ring_tac InitialRing. - -Declare ML Module "nsatz_plugin". - -Local Open Scope R_scope. - -Lemma psos_r1b: forall x y, x - y = 0 -> x = y. -intros x y H; replace x with ((x - y) + y); - [rewrite H | idtac]; ring. -Qed. - -Lemma psos_r1: forall x y, x = y -> x - y = 0. -intros x y H; rewrite H; ring. -Qed. - -Lemma nsatzR_not1: forall x y:R, x<>y -> exists z:R, z*(x-y)-1=0. -intros. -exists (1/(x-y)). -field. -unfold not. -unfold not in H. -intros. -apply H. -replace x with ((x-y)+y). -rewrite H0. -ring. -ring. -Qed. - -Lemma nsatzR_not1_0: forall x:R, x<>0 -> exists z:R, z*x-1=0. -intros. -exists (1/(x)). -field. -auto. -Qed. - - -Ltac equalities_to_goal := - lazymatch goal with - | H: (@eq R ?x 0) |- _ => try revert H - | H: (@eq R 0 ?x) |- _ => - try generalize (sym_equal H); clear H - | H: (@eq R ?x ?y) |- _ => - try generalize (psos_r1 _ _ H); clear H - end. - -Lemma nsatzR_not2: 1<>0. -auto with *. -Qed. - -Lemma nsatzR_diff: forall x y:R, x<>y -> x-y<>0. -intros. -intro; apply H. -replace x with (x-y+y) by ring. -rewrite H0; ring. -Qed. - -(* Removes x<>0 from hypothesis *) -Ltac nsatzR_not_hyp:= - match goal with - | H: ?x<>?y |- _ => - match y with - |0 => - let H1:=fresh "Hnsatz" in - let y:=fresh "x" in - destruct (@nsatzR_not1_0 _ H) as (y,H1); clear H - |_ => generalize (@nsatzR_diff _ _ H); clear H; intro - end - end. - -Ltac nsatzR_not_goal := - match goal with - | |- ?x<>?y :> R => red; intro; apply nsatzR_not2 - | |- False => apply nsatzR_not2 - end. - -Ltac nsatzR_begin := - intros; - repeat nsatzR_not_hyp; - try nsatzR_not_goal; - try apply psos_r1b; - repeat equalities_to_goal. - -(* code de Benjamin *) - -Definition PolZ := Pol Z. -Definition PEZ := PExpr Z. - -Definition P0Z : PolZ := @P0 Z 0%Z. - -Definition PolZadd : PolZ -> PolZ -> PolZ := - @Padd Z 0%Z Zplus Zeq_bool. - -Definition PolZmul : PolZ -> PolZ -> PolZ := - @Pmul Z 0%Z 1%Z Zplus Zmult Zeq_bool. - -Definition PolZeq := @Peq Z Zeq_bool. - -Definition norm := - @norm_aux Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool. - -Fixpoint mult_l (la : list PEZ) (lp: list PolZ) : PolZ := - match la, lp with - | a::la, p::lp => PolZadd (PolZmul (norm a) p) (mult_l la lp) - | _, _ => P0Z - end. - -Fixpoint compute_list (lla: list (list PEZ)) (lp:list PolZ) := - match lla with - | List.nil => lp - | la::lla => compute_list lla ((mult_l la lp)::lp) - end. - -Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) := - let (lla, lq) := certif in - let lp := List.map norm lpe in - PolZeq (norm qe) (mult_l lq (compute_list lla lp)). - - -(* Correction *) -Definition PhiR : list R -> PolZ -> R := - (Pphi 0 Rplus Rmult (gen_phiZ 0 1 Rplus Rmult Ropp)). - -Definition PEevalR : list R -> PEZ -> R := - PEeval 0 Rplus Rmult Rminus Ropp (gen_phiZ 0 1 Rplus Rmult Ropp) - Nnat.nat_of_N pow. - -Lemma P0Z_correct : forall l, PhiR l P0Z = 0. -Proof. trivial. Qed. - - -Lemma PolZadd_correct : forall P' P l, - PhiR l (PolZadd P P') = (PhiR l P + PhiR l P'). -Proof. - refine (Padd_ok Rset Rext (Rth_ARth Rset Rext (F_R Rfield)) - (gen_phiZ_morph Rset Rext (F_R Rfield))). -Qed. - -Lemma PolZmul_correct : forall P P' l, - PhiR l (PolZmul P P') = (PhiR l P * PhiR l P'). -Proof. - refine (Pmul_ok Rset Rext (Rth_ARth Rset Rext (F_R Rfield)) - (gen_phiZ_morph Rset Rext (F_R Rfield))). -Qed. - -Lemma norm_correct : - forall (l : list R) (pe : PEZ), PEevalR l pe = PhiR l (norm pe). -Proof. - intros;apply (norm_aux_spec Rset Rext (Rth_ARth Rset Rext (F_R Rfield)) - (gen_phiZ_morph Rset Rext (F_R Rfield)) R_power_theory) with (lmp:= List.nil). - compute;trivial. -Qed. - -Lemma PolZeq_correct : forall P P' l, - PolZeq P P' = true -> - PhiR l P = PhiR l P'. -Proof. - intros;apply - (Peq_ok Rset Rext (gen_phiZ_morph Rset Rext (F_R Rfield)));trivial. -Qed. - -Fixpoint Cond0 (A:Type) (Interp:A->R) (l:list A) : Prop := - match l with - | List.nil => True - | a::l => Interp a = 0 /\ Cond0 A Interp l - end. - -Lemma mult_l_correct : forall l la lp, - Cond0 PolZ (PhiR l) lp -> - PhiR l (mult_l la lp) = 0. -Proof. - induction la;simpl;intros;trivial. - destruct lp;trivial. - simpl in H;destruct H. - rewrite PolZadd_correct, PolZmul_correct, H, IHla;[ring | trivial]. -Qed. - -Lemma compute_list_correct : forall l lla lp, - Cond0 PolZ (PhiR l) lp -> - Cond0 PolZ (PhiR l) (compute_list lla lp). -Proof. - induction lla;simpl;intros;trivial. - apply IHlla;simpl;split;trivial. - apply mult_l_correct;trivial. -Qed. - -Lemma check_correct : - forall l lpe qe certif, - check lpe qe certif = true -> - Cond0 PEZ (PEevalR l) lpe -> - PEevalR l qe = 0. -Proof. - unfold check;intros l lpe qe (lla, lq) H2 H1. - apply PolZeq_correct with (l:=l) in H2. - rewrite norm_correct, H2. - apply mult_l_correct. - apply compute_list_correct. - clear H2 lq lla qe;induction lpe;simpl;trivial. - simpl in H1;destruct H1. - rewrite <- norm_correct;auto. -Qed. - -(* fin du code de Benjamin *) - -Lemma nsatzR_l3:forall c p r, ~c=0 -> c*p^r=0 -> p=0. -intros. -elim (Rmult_integral _ _ H0);intros. - absurd (c=0);auto. - - clear H0; induction r; simpl in *. - contradict H1; discrR. - - elim (Rmult_integral _ _ H1); auto. -Qed. - - -Ltac generalise_eq_hyps:= - repeat - (match goal with - |h : (?p = ?q)|- _ => revert h - end). - -Ltac lpol_goal t := - match t with - | ?a = 0 -> ?b => - let r:= lpol_goal b in - constr:(a::r) - | ?a = 0 => constr:(a::nil) - end. - -Fixpoint IPR p {struct p}: R := - match p with - xH => 1 - | xO xH => 1 + 1 - | xO p1 => 2 * (IPR p1) - | xI xH => 1 + (1 + 1) - | xI p1 => 1 + 2 * (IPR p1) - end. - -Definition IZR1 z := - match z with Z0 => 0 - | Zpos p => IPR p - | Zneg p => -(IPR p) - end. - -Fixpoint interpret3 t fv {struct t}: R := - match t with - | (PEadd t1 t2) => - let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 + v2) - | (PEmul t1 t2) => - let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 * v2) - | (PEsub t1 t2) => - let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 - v2) - | (PEopp t1) => - let v1 := interpret3 t1 fv in (-v1) - | (PEpow t1 t2) => - let v1 := interpret3 t1 fv in v1 ^(Nnat.nat_of_N t2) - | (PEc t1) => (IZR1 t1) - | (PEX n) => List.nth (pred (nat_of_P n)) fv 0 - end. - -(* lp est incluse dans fv. La met en tete. *) - -Ltac parametres_en_tete fv lp := - match fv with - | (@nil _) => lp - | (@cons _ ?x ?fv1) => - let res := AddFvTail x lp in - parametres_en_tete fv1 res - end. - -Ltac append1 a l := - match l with - | (@nil _) => constr:(cons a l) - | (cons ?x ?l) => let l' := append1 a l in constr:(cons x l') - end. - -Ltac rev l := - match l with - |(@nil _) => l - | (cons ?x ?l) => let l' := rev l in append1 x l' - end. - - -Ltac nsatz_call_n info nparam p rr lp kont := - nsatz_compute (PEc info :: PEc nparam :: PEpow p rr :: lp); - match goal with - | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ => - intros _; - set (lci:=lci0); - set (lq:=lq0); - kont c rr lq lci - end. - -Ltac nsatz_call radicalmax info nparam p lp kont := - let rec try_n n := - lazymatch n with - | 0%N => fail - | _ => -(* idtac "Trying power: " n;*) - (let r := eval compute in (Nminus radicalmax (Npred n)) in - nsatz_call_n info nparam p r lp kont) || - let n' := eval compute in (Npred n) in try_n n' - end in - try_n radicalmax. - - -Ltac nsatzR_gen radicalmax info lparam lvar n RNG lH _rl := - get_Pre RNG (); - let mkFV := Ring_tac.get_RingFV RNG in - let mkPol := Ring_tac.get_RingMeta RNG in - generalise_eq_hyps; - let t := Get_goal in - let lpol := lpol_goal t in - intros; - let fv := - match lvar with - | nil => - let fv1 := FV_hypo_tac mkFV ltac:(get_Eq RNG) lH in - let fv1 := list_fold_right mkFV fv1 lpol in - rev fv1 - (* heuristique: les dernieres variables auront le poid le plus fort *) - | _ => lvar - end in - check_fv fv; - (*idtac "variables:";idtac fv;*) - let nparam := eval compute in (Z_of_nat (List.length lparam)) in - let fv := parametres_en_tete fv lparam in - idtac "variables:"; idtac fv; - (* idtac "nparam:"; idtac nparam;*) - let lpol := list_fold_right - ltac:(fun p l => let p' := mkPol p fv in constr:(p'::l)) - (@nil (PExpr Z)) - lpol in - let lpol := eval compute in (List.rev lpol) in - (*idtac lpol;*) - let SplitPolyList kont := - match lpol with - | ?p2::?lp2 => kont p2 lp2 - | _ => idtac "polynomial not in the ideal" - end in - SplitPolyList ltac:(fun p lp => - set (p21:=p) ; - set (lp21:=lp); - nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => - set (q := PEmul c (PEpow p21 r)); - let Hg := fresh "Hg" in - assert (Hg:check lp21 q (lci,lq) = true); - [ (vm_compute;reflexivity) || idtac "invalid nsatz certificate" - | let Hg2 := fresh "Hg" in - assert (Hg2: interpret3 q fv = 0); - [ simpl; apply (@check_correct fv lp21 q (lci,lq) Hg); simpl; - repeat (split;[assumption|idtac]); exact I - | simpl in Hg2; simpl; - apply nsatzR_l3 with (interpret3 c fv) (Nnat.nat_of_N r);simpl; - [ discrR || idtac "could not prove discrimination result" - | exact Hg2] - ] - ])). - -Ltac nsatzRpv radicalmax info lparam lvar:= - nsatzR_begin; - intros; - let G := Get_goal in - ring_lookup - (PackRing ltac:(nsatzR_gen radicalmax info lparam lvar ring_subst_niter)) - [] G. - -Ltac nsatzR := nsatzRpv 6%N 1%Z (@nil R) (@nil R). -Ltac nsatzRradical radicalmax := nsatzRpv radicalmax 1%Z (@nil R) (@nil R). -Ltac nsatzRparameters lparam := nsatzRpv 6%N 1%Z lparam (@nil R). - -Tactic Notation "nsatz" := nsatzR. -Tactic Notation "nsatz" "with" "lexico" := - nsatzRpv 6%N 2%Z (@nil R) (@nil R). -Tactic Notation "nsatz" "with" "lexico" "sugar":= - nsatzRpv 6%N 3%Z (@nil R) (@nil R). -Tactic Notation "nsatz" "without" "sugar":= - nsatzRpv 6%N 0%Z (@nil R) (@nil R). - - diff --git a/plugins/nsatz/NsatzZ.v b/plugins/nsatz/NsatzZ.v deleted file mode 100644 index b57aa0ed..00000000 --- a/plugins/nsatz/NsatzZ.v +++ /dev/null @@ -1,73 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import Reals ZArith. -Require Export NsatzR. - -Open Scope Z_scope. - -Lemma nsatzZhypR: forall x y:Z, x=y -> IZR x = IZR y. -Proof IZR_eq. (* or f_equal ... *) - -Lemma nsatzZconclR: forall x y:Z, IZR x = IZR y -> x = y. -Proof eq_IZR. - -Lemma nsatzZhypnotR: forall x y:Z, x<>y -> IZR x <> IZR y. -Proof IZR_neq. - -Lemma nsatzZconclnotR: forall x y:Z, IZR x <> IZR y -> x <> y. -Proof. -intros x y H. contradict H. f_equal. assumption. -Qed. - -Ltac nsatzZtoR1 := - repeat - (match goal with - | H:(@eq Z ?x ?y) |- _ => - generalize (@nsatzZhypR _ _ H); clear H; intro H - | |- (@eq Z ?x ?y) => apply nsatzZconclR - | H:not (@eq Z ?x ?y) |- _ => - generalize (@nsatzZhypnotR _ _ H); clear H; intro H - | |- not (@eq Z ?x ?y) => apply nsatzZconclnotR - end). - -Lemma nsatzZR1: forall x y:Z, IZR(x+y) = (IZR x + IZR y)%R. -Proof plus_IZR. - -Lemma nsatzZR2: forall x y:Z, IZR(x*y) = (IZR x * IZR y)%R. -Proof mult_IZR. - -Lemma nsatzZR3: forall x y:Z, IZR(x-y) = (IZR x - IZR y)%R. -Proof. -intros; symmetry. apply Z_R_minus. -Qed. - -Lemma nsatzZR4: forall (x:Z) p, IZR(x ^ Zpos p) = (IZR x ^ nat_of_P p)%R. -Proof. -intros. rewrite pow_IZR. -do 2 f_equal. -apply Zpos_eq_Z_of_nat_o_nat_of_P. -Qed. - -Ltac nsatzZtoR2:= - repeat - (rewrite nsatzZR1 in * || - rewrite nsatzZR2 in * || - rewrite nsatzZR3 in * || - rewrite nsatzZR4 in *). - -Ltac nsatzZ_begin := - intros; - nsatzZtoR1; - nsatzZtoR2; - simpl in *. - (*cbv beta iota zeta delta [nat_of_P Pmult_nat plus mult] in *.*) - -Ltac nsatzZ := - nsatzZ_begin; (*idtac "nsatzZ_begin;";*) - nsatzR. diff --git a/plugins/nsatz/vo.itarget b/plugins/nsatz/vo.itarget index 4af4786d..06fc8834 100644 --- a/plugins/nsatz/vo.itarget +++ b/plugins/nsatz/vo.itarget @@ -1,3 +1 @@ -NsatzR.vo -Nsatz_domain.vo -NsatzZ.vo +Nsatz.vo diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v index 65b780dd..fadecf5d 100644 --- a/plugins/omega/Omega.v +++ b/plugins/omega/Omega.v @@ -13,7 +13,7 @@ (* *) (**************************************************************************) -(* $Id$ *) +(* $Id: Omega.v 13323 2010-07-24 15:57:30Z herbelin $ *) (* We do not require [ZArith] anymore, but only what's necessary for Omega *) Require Export ZArith_base. diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v index 56a854d6..ec9faedd 100644 --- a/plugins/omega/OmegaLemmas.v +++ b/plugins/omega/OmegaLemmas.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id$ i*) +(*i $Id: OmegaLemmas.v 12337 2009-09-17 15:58:14Z glondu $ i*) Require Import ZArith_base. Open Local Scope Z_scope. diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v index c0b0eb47..ee942db0 100644 --- a/plugins/omega/OmegaPlugin.v +++ b/plugins/omega/OmegaPlugin.v @@ -6,6 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: OmegaPlugin.v 13323 2010-07-24 15:57:30Z herbelin $ *) Declare ML Module "omega_plugin". diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 471fb5da..e3f9a309 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -13,7 +13,7 @@ (* *) (**************************************************************************) -(* $Id$ *) +(* $Id: coq_omega.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Pp diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 4be7f2e5..eefa67ec 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -15,7 +15,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: g_omega.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Coq_omega open Refiner diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v index ea8f5bf9..b7cc13ae 100644 --- a/plugins/quote/Quote.v +++ b/plugins/quote/Quote.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Quote.v 13323 2010-07-24 15:57:30Z herbelin $ *) Declare ML Module "quote_plugin". diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index ef87a596..83bfb6ed 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: g_quote.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Tacexpr diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 760f93b8..b6ca770e 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: quote.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* The `Quote' tactic *) diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v index 27349683..3e30b90f 100644 --- a/plugins/ring/LegacyArithRing.v +++ b/plugins/ring/LegacyArithRing.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: LegacyArithRing.v 13323 2010-07-24 15:57:30Z herbelin $ *) (* Instantiation of the Ring tactic for the naturals of Arith $*) diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v index 7a2f4abc..337c3085 100644 --- a/plugins/ring/LegacyNArithRing.v +++ b/plugins/ring/LegacyNArithRing.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: LegacyNArithRing.v 13323 2010-07-24 15:57:30Z herbelin $ *) (* Instantiation of the Ring tactic for the binary natural numbers *) diff --git a/plugins/ring/LegacyRing.v b/plugins/ring/LegacyRing.v index 5ab90555..6b655134 100644 --- a/plugins/ring/LegacyRing.v +++ b/plugins/ring/LegacyRing.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: LegacyRing.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export Bool. Require Export LegacyRing_theory. diff --git a/plugins/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v index 74d8f186..fb4c87fb 100644 --- a/plugins/ring/LegacyRing_theory.v +++ b/plugins/ring/LegacyRing_theory.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: LegacyRing_theory.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export Bool. diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v index 293ac12e..22fa87c8 100644 --- a/plugins/ring/LegacyZArithRing.v +++ b/plugins/ring/LegacyZArithRing.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: LegacyZArithRing.v 13323 2010-07-24 15:57:30Z herbelin $ *) (* Instantiation of the Ring tactic for the binary integers of ZArith *) diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v index 96764e51..e65e1ce8 100644 --- a/plugins/ring/Ring_abstract.v +++ b/plugins/ring/Ring_abstract.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Ring_abstract.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import LegacyRing_theory. Require Import Quote. diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v index 320e1ab2..d68fef4f 100644 --- a/plugins/ring/Ring_normalize.v +++ b/plugins/ring/Ring_normalize.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Ring_normalize.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import LegacyRing_theory. Require Import Quote. diff --git a/plugins/ring/Setoid_ring.v b/plugins/ring/Setoid_ring.v index 15495071..3a3dfe84 100644 --- a/plugins/ring/Setoid_ring.v +++ b/plugins/ring/Setoid_ring.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Setoid_ring.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export Setoid_ring_theory. Require Export Quote. diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v index 6bd5b419..6a53b519 100644 --- a/plugins/ring/Setoid_ring_normalize.v +++ b/plugins/ring/Setoid_ring_normalize.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Setoid_ring_normalize.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import Setoid_ring_theory. Require Import Quote. diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v index 96910db6..d55f25fc 100644 --- a/plugins/ring/Setoid_ring_theory.v +++ b/plugins/ring/Setoid_ring_theory.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Setoid_ring_theory.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export Bool. Require Export Setoid. diff --git a/plugins/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4 index dc34fdbc..7fda4920 100644 --- a/plugins/ring/g_ring.ml4 +++ b/plugins/ring/g_ring.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: g_ring.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Quote open Ring diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index fc2a04b3..3cdf0117 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ring.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* ML part of the Ring tactic *) diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 8e7cf569..a62a0780 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Bintree.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export List. Require Export BinPos. diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index a61a2605..ffa619d0 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Rtauto.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export List. diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index 73311f63..22f8ca2a 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$*) +(* $Id: g_rtauto.ml4 13323 2010-07-24 15:57:30Z herbelin $*) (*i camlp4deps: "parsing/grammar.cma" i*) diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index cf9e7fd3..23530ef8 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: proof_search.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Term open Util diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli index 5ccc59a5..685a3059 100644 --- a/plugins/rtauto/proof_search.mli +++ b/plugins/rtauto/proof_search.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: proof_search.mli 13323 2010-07-24 15:57:30Z herbelin $ *) type form= Atom of int diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 77ef5a9c..e079a83c 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: refl_tauto.ml 13323 2010-07-24 15:57:30Z herbelin $ *) module Search = Explore.Make(Proof_search) diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index e8264c83..2ff45f57 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: refl_tauto.mli 13323 2010-07-24 15:57:30Z herbelin $ *) (* raises Not_found if no proof is found *) diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index a5187224..8940e565 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id$ i*) +(*i $Id: newring.ml4 13332 2010-07-26 22:12:43Z msozeau $ i*) open Pp open Util @@ -531,7 +531,7 @@ let ring_equality (r,add,mul,opp,req) = (setoid,op_morph) | _ -> let setoid = setoid_of_relation (Global.env ()) r req in - let signature = [Some (r,req);Some (r,req)],Some(r,req) in + let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in let add_m, add_m_lem = try Rewrite.default_morphism signature add with Not_found -> @@ -544,7 +544,7 @@ let ring_equality (r,add,mul,opp,req) = match opp with | Some opp -> (let opp_m,opp_m_lem = - try Rewrite.default_morphism ([Some(r,req)],Some(r,req)) opp + try Rewrite.default_morphism ([Some(r,Some req)],Some(r,Some req)) opp with Not_found -> error "ring opposite should be declared as a morphism" in let op_morph = @@ -1031,7 +1031,7 @@ let field_equality r inv req = mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|]) | _ -> let _setoid = setoid_of_relation (Global.env ()) r req in - let signature = [Some (r,req)],Some(r,req) in + let signature = [Some (r,Some req)],Some(r,Some req) in let inv_m, inv_m_lem = try Rewrite.default_morphism signature inv with Not_found -> diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml index 4b95df19..f1bdd640 100644 --- a/plugins/subtac/eterm.ml +++ b/plugins/subtac/eterm.ml @@ -141,16 +141,28 @@ let evar_dependencies evm ev = if Intset.equal deps deps' then deps else aux deps' in aux (Intset.singleton ev) - -let sort_dependencies evl = - List.stable_sort - (fun (id, ev, deps) (id', ev', deps') -> - if id = id' then 0 - else if Intset.mem id deps' then -1 - else if Intset.mem id' deps then 1 - else Pervasives.compare id id') - evl +let move_after (id, ev, deps as obl) l = + let rec aux restdeps = function + | (id', _, _) as obl' :: tl -> + let restdeps' = Intset.remove id' restdeps in + if Intset.is_empty restdeps' then + obl' :: obl :: tl + else obl' :: aux restdeps' tl + | [] -> [obl] + in aux (Intset.remove id deps) l + +let sort_dependencies evl = + let rec aux l found list = + match l with + | (id, ev, deps) as obl :: tl -> + let found' = Intset.union found (Intset.singleton id) in + if Intset.subset deps found' then + aux tl found' (obl :: list) + else aux (move_after obl tl) found list + | [] -> List.rev list + in aux evl Intset.empty [] + let map_evar_body f = function | Evar_empty -> Evar_empty | Evar_defined c -> Evar_defined (f c) diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli index d727c19c..262889c8 100644 --- a/plugins/subtac/eterm.mli +++ b/plugins/subtac/eterm.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: eterm.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Environ open Tacmach open Term diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index 87fd0479..cd8708d5 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -14,7 +14,7 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) -(* $Id$ *) +(* $Id: g_subtac.ml4 13332 2010-07-26 22:12:43Z msozeau $ *) open Flags @@ -53,7 +53,7 @@ open Constr let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) GEXTEND Gram - GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder subtac_withtac; + GLOBAL: subtac_gallina_loc typeclass_constraint subtac_withtac; subtac_gallina_loc: [ [ g = Vernac.gallina -> loc, g @@ -65,21 +65,12 @@ GEXTEND Gram | -> None ] ] ; - Constr.binder_let: + Constr.closed_binder: [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in [LocalRawAssum ([id], default_binder_kind, typ)] ] ]; - Constr.binder: - [ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" -> - ([id],default_binder_kind, mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, c, p)])) - | "("; id=Prim.name; ":"; c=Constr.lconstr; ")" -> - ([id],default_binder_kind, c) - | "("; id=Prim.name; lid=LIST1 Prim.name; ":"; c=Constr.lconstr; ")" -> - (id::lid,default_binder_kind, c) - ] ]; - END @@ -161,9 +152,11 @@ VERNAC COMMAND EXTEND Subtac_Set_Solver (Tacinterp.glob_tactic t) ] END +open Pp + VERNAC COMMAND EXTEND Subtac_Show_Solver | [ "Show" "Obligation" "Tactic" ] -> [ - Pp.msgnl (Pptactic.pr_glob_tactic (Global.env ()) (Subtac_obligations.default_tactic_expr ())) ] + msgnl (str"Program obligation tactic is " ++ Subtac_obligations.print_default_tactic ()) ] END VERNAC COMMAND EXTEND Subtac_Show_Obligations diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index c859c690..885f7fb6 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: subtac.ml 13344 2010-07-28 15:04:36Z msozeau $ *) open Global open Pp @@ -76,7 +76,7 @@ let start_proof_com env isevars sopt kind (bl,t) hook = (Pfedit.get_all_proof_names ()) in let evm, c, typ, imps = - Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr t bl) None + Subtac_pretyping.subtac_process ~is_type:true env isevars id [] (Topconstr.prod_constr_expr t bl) None in let c = solve_tccs_in_type env id isevars evm c typ in Lemmas.start_proof id kind c (fun loc gr -> @@ -138,9 +138,6 @@ let subtac (loc, command) = Dumpglob.dump_definition lid false "def"; (match expr with | ProveBody (bl, t) -> - if Lib.is_modtype () then - errorlabstrm "Subtac_command.StartProof" - (str "Proof editing mode not supported in module types"); start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) (fun _ _ -> ()) | DefineBody (bl, _, c, tycon) -> @@ -218,33 +215,10 @@ let subtac (loc, command) = ++ x ++ spc () ++ str "and" ++ spc () ++ y in msg_warning cmds - | Cases.PatternMatchingError (env, exn) as e -> - debug 2 (Himsg.explain_pattern_matching_error env exn); - raise e + | Cases.PatternMatchingError (env, exn) as e -> raise e - | Type_errors.TypeError (env, exn) as e -> - debug 2 (Himsg.explain_type_error env exn); - raise e + | Type_errors.TypeError (env, exn) as e -> raise e - | Pretype_errors.PretypeError (env, exn) as e -> - debug 2 (Himsg.explain_pretype_error env exn); - raise e + | Pretype_errors.PretypeError (env, exn) as e -> raise e - | (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) | - Stdpp.Exc_located (loc, e') as e) -> - debug 2 (str "Parsing exception: "); - (match e' with - | Type_errors.TypeError (env, exn) -> - debug 2 (Himsg.explain_type_error env exn); - raise e - - | Pretype_errors.PretypeError (env, exn) -> - debug 2 (Himsg.explain_pretype_error env exn); - raise e - - | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e''); - raise e) - - | e -> - msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e); - raise e + | e -> raise e diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 28cedc8a..f6f8695b 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: subtac_cases.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Cases open Util @@ -23,13 +23,11 @@ open Sign open Reductionops open Typeops open Type_errors - open Rawterm open Retyping open Pretype_errors open Evarutil open Evarconv - open Subtac_utils (************************************************************************) @@ -125,7 +123,7 @@ type tomatch_stack = tomatch_status list originating from a subterm in which case real args are not dependent; it accounts for n+1 binders if dep or n binders if not dep - [PrProd] types abstracted term ([Abstract]); it accounts for one binder - - [PrCcl] types the right-hand-side + - [PrCcl] types the right-hand side - Aliases [Alias] have no trace in [predicate_signature] *) @@ -1152,7 +1150,7 @@ let rec generalize_problem pb = function tomatch = Abstract d :: tomatch; pred = Option.map (generalize_predicate i d) pb'.pred } -(* No more patterns: typing the right-hand-side of equations *) +(* No more patterns: typing the right-hand side of equations *) let build_leaf pb = let rhs = extract_rhs pb in let tycon = match pb.pred with @@ -1514,11 +1512,11 @@ let eq_id avoid id = let hid' = next_ident_away hid avoid in hid' -let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |]) -let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |]) +let mk_eq typ x y = mkApp (delayed_force eq_ind, [| typ; x ; y |]) +let mk_eq_refl typ x = mkApp (delayed_force eq_refl, [| typ; x |]) let mk_JMeq typ x typ' y = - mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |]) -let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |]) + mkApp (delayed_force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |]) +let mk_JMeq_refl typ x = mkApp (delayed_force Subtac_utils.jmeq_refl, [| typ; x |]) let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true)) @@ -1610,7 +1608,7 @@ let vars_of_ctx ctx = | Some t' when kind_of_term t' = Rel 0 -> prev, (RApp (dummy_loc, - (RRef (dummy_loc, Lazy.force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars + (RRef (dummy_loc, delayed_force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars | _ -> match na with Anonymous -> raise (Invalid_argument "vars_of_ctx") @@ -1651,7 +1649,7 @@ let build_ineqs prevpatterns pats liftsign = lift_rel_context len ppat_sign @ sign, len', succ n, (* nth pattern *) - mkApp (Lazy.force eq_ind, + mkApp (delayed_force eq_ind, [| lift (len' + liftsign) curpat_ty; liftn (len + liftsign) (succ lens) ppat_c ; lift len' curpat_c |]) :: @@ -1929,7 +1927,7 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra let typing_fun tycon env = typing_fun tycon env isevars in - (* We build the matrix of patterns and right-hand-side *) + (* We build the matrix of patterns and right-hand side *) let matx = matx_of_eqns env eqns in (* We build the vector of terms to match consistently with the *) diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli index 823e9912..a4df1257 100644 --- a/plugins/subtac/subtac_cases.mli +++ b/plugins/subtac/subtac_cases.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: subtac_cases.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Util diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index f0ff9ba3..b2bf9912 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: subtac_classes.ml 13328 2010-07-26 11:05:30Z herbelin $ i*) open Pretyping open Evd @@ -30,11 +30,11 @@ open Util module SPretyping = Subtac_pretyping.Pretyping -let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c = +let interp_constr_evars_gen evdref env ?(impls=[]) kind c = SPretyping.understand_tcc_evars evdref env kind (intern_gen (kind=IsType) ~impls ( !evdref) env c) -let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ = +let interp_casted_constr_evars evdref env ?(impls=[]) c typ = interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c let interp_context_evars evdref env params = diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli index 1c6c473a..57c7aa5b 100644 --- a/plugins/subtac/subtac_classes.mli +++ b/plugins/subtac/subtac_classes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: subtac_classes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Names diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index 3f2a5dba..17c7284c 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -6,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: subtac_coercion.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Util open Names @@ -39,7 +39,7 @@ let rec disc_subset x = (match kind_of_term c with Ind i -> let len = Array.length l in - let sig_ = Lazy.force sig_ in + let sig_ = delayed_force sig_ in if len = 2 && i = Term.destInd sig_.typ then let (a, b) = pair_of_array l in @@ -53,7 +53,7 @@ and disc_exist env x = | App (c, l) -> (match kind_of_term c with Construct c -> - if c = Term.destConstruct (Lazy.force sig_).intro + if c = Term.destConstruct (delayed_force sig_).intro then Some (l.(0), l.(1), l.(2), l.(3)) else None | _ -> None) @@ -66,7 +66,7 @@ module Coercion = struct let disc_proj_exist env x = match kind_of_term x with | App (c, l) -> - (if Term.eq_constr c (Lazy.force sig_).proj1 + (if Term.eq_constr c (delayed_force sig_).proj1 && Array.length l = 3 then disc_exist env l.(2) else None) @@ -100,7 +100,7 @@ module Coercion = struct Some (u, p) -> let f, ct = aux u in (Some (fun x -> - app_opt f (mkApp ((Lazy.force sig_).proj1, + app_opt f (mkApp ((delayed_force sig_).proj1, [| u; p; x |]))), ct) | None -> (None, v) @@ -146,9 +146,9 @@ module Coercion = struct in let args = List.rev (restargs @ mkRel 1 :: lift_args 1 tele) in let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in - let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in + let eq = mkApp (delayed_force eq_ind, [| eqT; hdx; hdy |]) in let evar = make_existential loc env isevars eq in - let eq_app x = mkApp (Lazy.force eq_rect, + let eq_app x = mkApp (delayed_force eq_rect, [| eqT; hdx; pred; x; hdy; evar|]) in aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) else Some co @@ -187,8 +187,8 @@ module Coercion = struct (match kind_of_term c, kind_of_term c' with Ind i, Ind i' -> (* Inductive types *) let len = Array.length l in - let existS = Lazy.force existS in - let prod = Lazy.force prod in + let existS = delayed_force existS in + let prod = delayed_force prod in (* Sigma types *) if len = Array.length l' && len = 2 && i = i' && (i = Term.destInd existS.typ || i = Term.destInd prod.typ) @@ -279,7 +279,7 @@ module Coercion = struct Some (u, p) -> let c = coerce_unify env u y in let f x = - app_opt c (mkApp ((Lazy.force sig_).proj1, + app_opt c (mkApp ((delayed_force sig_).proj1, [| u; p; x |])) in Some f | None -> @@ -292,7 +292,7 @@ module Coercion = struct let evar = make_existential loc env isevars (mkApp (p, [| cx |])) in (mkApp - ((Lazy.force sig_).intro, + ((delayed_force sig_).intro, [| u; p; cx; evar |]))) | None -> raise NoSubtacCoercion @@ -496,8 +496,7 @@ module Coercion = struct with NoCoercion -> coerce_itf loc env' isevars None t t') with NoSubtacCoercion -> - let sigma = isevars in - error_cannot_coerce env' sigma (t, t')) + error_cannot_coerce env' isevars (t, t')) else isevars with _ -> isevars end diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index f2747225..e7dd7ef1 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -53,7 +53,7 @@ let evar_nf isevars c = Evarutil.nf_evar !isevars c let interp_gen kind isevars env - ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) + ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in let c' = SPretyping.understand_tcc_evars isevars env kind c' in @@ -62,13 +62,13 @@ let interp_gen kind isevars env let interp_constr isevars env c = interp_gen (OfType None) isevars env c -let interp_type_evars isevars env ?(impls=([],[])) c = +let interp_type_evars isevars env ?(impls=[]) c = interp_gen IsType isevars env ~impls c -let interp_casted_constr isevars env ?(impls=([],[])) c typ = +let interp_casted_constr isevars env ?(impls=[]) c typ = interp_gen (OfType (Some typ)) isevars env ~impls c -let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ = +let interp_casted_constr_evars isevars env ?(impls=[]) c typ = interp_gen (OfType (Some typ)) isevars env ~impls c let interp_open_constr isevars env c = @@ -237,14 +237,18 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = let rel = interp_constr isevars env r in let relty = type_of env !isevars rel in let relargty = - let ctx, ar = Reductionops.splay_prod_n env !isevars 2 relty in - match ctx, kind_of_term ar with - | [(_, None, t); (_, None, u)], Sort (Prop Null) - when Reductionops.is_conv env !isevars t u -> t - | _, _ -> - user_err_loc (constr_loc r, - "Subtac_command.build_wellfounded", - my_print_constr env rel ++ str " is not an homogeneous binary relation.") + let error () = + user_err_loc (constr_loc r, + "Subtac_command.build_wellfounded", + my_print_constr env rel ++ str " is not an homogeneous binary relation.") + in + try + let ctx, ar = Reductionops.splay_prod_n env !isevars 2 relty in + match ctx, kind_of_term ar with + | [(_, None, t); (_, None, u)], Sort (Prop Null) + when Reductionops.is_conv env !isevars t u -> t + | _, _ -> error () + with _ -> error () in let measure = interp_casted_constr isevars binders_env measure relargty in let wf_rel, wf_rel_fun, measure_fn = @@ -252,14 +256,14 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = it_mkLambda_or_LetIn measure letbinders, it_mkLambda_or_LetIn measure binders in - let comb = constr_of_global (Lazy.force measure_on_R_ref) in + let comb = constr_of_global (delayed_force measure_on_R_ref) in let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in let wf_rel_fun x y = mkApp (rel, [| subst1 x measure_body; subst1 y measure_body |]) in wf_rel, wf_rel_fun, measure in - let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |]) in + let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in let argid' = id_of_string (string_of_id argname ^ "'") in let wfarg len = (Name argid', None, mkSubset (Name argid') argtyp @@ -267,7 +271,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = in let intern_bl = wfarg 1 :: [arg] in let _intern_env = push_rel_context intern_bl env in - let proj = (Lazy.force sig_).Coqlib.proj1 in + let proj = (delayed_force sig_).Coqlib.proj1 in let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in let projection = (* in wfarg :: arg :: before *) mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |]) @@ -280,7 +284,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in let curry_fun = let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in - let arg = mkApp ((Lazy.force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in + let arg = mkApp ((delayed_force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in let rcurry = mkApp (rel, [| measure; lift len measure |]) in let lam = (Name (id_of_string "recproof"), None, rcurry) in @@ -292,21 +296,20 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = let lift_lets = Termops.lift_rel_context 1 letbinders in let intern_body = let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in - let (r, l, impls, scopes) = + let (r, l, impls, scopes) = Constrintern.compute_internalization_data env Constrintern.Recursive full_arity impls in let newimpls = [(recname, (r, l, impls @ [Some (id_of_string "recproof", Impargs.Manual, (true, false))], scopes @ [None]))] in - let newimpls = Constrintern.set_internalization_env_params newimpls [] in interp_casted_constr isevars ~impls:newimpls (push_rel_context ctx env) body (lift 1 top_arity) in let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in let prop = mkLambda (Name argname, argtyp, top_arity_let) in let def = - mkApp (constr_of_global (Lazy.force fix_sub_ref), + mkApp (constr_of_global (delayed_force fix_sub_ref), [| argtyp ; wf_rel ; make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ; prop ; intern_body_lam |]) @@ -429,7 +432,7 @@ let interp_recursive fixkind l boxed = List.fold_left2 (fun env' id t -> let sort = Retyping.get_type_of env !evdref t in let fixprot = - try mkApp (Lazy.force Subtac_utils.fix_proto, [|sort; t|]) + try mkApp (delayed_force Subtac_utils.fix_proto, [|sort; t|]) with e -> t in (id,None,fixprot) :: env') @@ -438,8 +441,8 @@ let interp_recursive fixkind l boxed = let env_rec = push_named_context rec_sign env in (* Get interpretation metadatas *) - let impls = Constrintern.compute_full_internalization_env env - Constrintern.Recursive [] fixnames fixtypes fiximps + let impls = Constrintern.compute_internalization_env env + Constrintern.Recursive fixnames fixtypes fiximps in let notations = List.flatten ntnl in @@ -453,7 +456,7 @@ let interp_recursive fixkind l boxed = let fixdefs = List.map out_def fixdefs in (* Instantiate evars and check all are resolved *) - let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in + let evd = Evarconv.consider_remaining_unif_problems env_rec !evdref in let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:false env_rec evd in @@ -518,8 +521,8 @@ let build_recursive l b = m ntn false) | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g -> - let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) -> - ({Command.fix_name = id; Command.fix_binders = bl; + let fixl = List.map (fun (((_,id),(n,ro),bl,typ,def),ntn) -> + ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = n; Command.fix_body = def; Command.fix_type = typ},ntn)) l in interp_recursive (IsFixpoint g) fixl b | _, _ -> @@ -528,7 +531,7 @@ let build_recursive l b = let build_corecursive l b = let fixl = List.map (fun (((_,id),bl,typ,def),ntn) -> - ({Command.fix_name = id; Command.fix_binders = bl; + ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = None; Command.fix_body = def; Command.fix_type = typ},ntn)) l in interp_recursive IsCoFixpoint fixl b diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli index 304aa139..0f24915e 100644 --- a/plugins/subtac/subtac_command.mli +++ b/plugins/subtac/subtac_command.mli @@ -13,7 +13,7 @@ val interp_gen : typing_constraint -> evar_map ref -> env -> - ?impls:full_internalization_env -> + ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr @@ -23,12 +23,12 @@ val interp_constr : val interp_type_evars : evar_map ref -> env -> - ?impls:full_internalization_env -> + ?impls:internalization_env -> constr_expr -> constr val interp_casted_constr_evars : evar_map ref -> env -> - ?impls:full_internalization_env -> + ?impls:internalization_env -> constr_expr -> types -> constr val interp_open_constr : evar_map ref -> env -> constr_expr -> constr diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 2836bc73..1424618f 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -21,8 +21,8 @@ let ppwarn cmd = Pp.warn (str"Program:" ++ cmd) let pperror cmd = Util.errorlabstrm "Program" cmd let error s = pperror (str s) -let reduce = - Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty +let reduce c = + Reductionops.clos_norm_flags Closure.betaiota (Global.env ()) Evd.empty c exception NoObligations of identifier option @@ -61,16 +61,15 @@ type program_info = { prg_implicits : (Topconstr.explicitation * (bool * bool * bool)) list; prg_notations : notations ; prg_kind : definition_kind; + prg_reduce : constr -> constr; prg_hook : Tacexpr.declaration_hook; } let assumption_message id = Flags.if_verbose message ((string_of_id id) ^ " is assumed") -let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC -let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Tacexpr.TacId []) - -let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t +let (set_default_tactic, get_default_tactic, print_default_tactic) = + Tactic_option.declare_tactic_option "Program tactic" (* true = All transparent, false = Opaque if possible *) let proofs_transparency = ref true @@ -136,10 +135,9 @@ let map_first m = let from_prg : program_info ProgMap.t ref = ref ProgMap.empty -let freeze () = !from_prg, !default_tactic_expr -let unfreeze (v, t) = from_prg := v; set_default_tactic t -let init () = - from_prg := ProgMap.empty; set_default_tactic (Tacexpr.TacId []) +let freeze () = !from_prg +let unfreeze v = from_prg := v +let init () = from_prg := ProgMap.empty (** Beware: if this code is dynamically loaded via dynlink after the start of Coq, then this [init] function will not be run by [Lib.init ()]. @@ -155,35 +153,16 @@ let _ = let progmap_union = ProgMap.fold ProgMap.add -let cache (_, (local, tac)) = - set_default_tactic tac - -let load (_, (local, tac)) = - if not local then set_default_tactic tac - -let subst (s, (local, tac)) = - (local, Tacinterp.subst_tactic s tac) - let (input,output) = declare_object { (default_object "Program state") with - cache_function = cache; - load_function = (fun _ -> load); - open_function = (fun _ -> load); - classify_function = (fun (local, tac) -> + classify_function = (fun () -> if not (ProgMap.is_empty !from_prg) then errorlabstrm "Program" (str "Unsolved obligations when closing module:" ++ spc () ++ prlist_with_sep spc (fun x -> Nameops.pr_id x) (map_keys !from_prg)); - if local then Dispose else Substitute (local, tac)); - subst_function = subst} + Dispose) } -let update_state local = - Lib.add_anonymous_leaf (input (local, !default_tactic_expr)) - -let set_default_tactic local t = - set_default_tactic t; update_state local - open Evd let progmap_remove prg = @@ -270,7 +249,7 @@ let declare_mutual_definition l = let subs, typ = (subst_body true x) in let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in - reduce term, reduce typ, x.prg_implicits) l) + x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l) in (* let fixdefs = List.map reduce_fix fixdefs in *) let fixkind = Option.get first.prg_fixkind in @@ -300,8 +279,8 @@ let declare_mutual_definition l = List.iter progmap_remove l; kn let declare_obligation prg obl body = - let body = reduce body in - let ty = reduce obl.obl_type in + let body = prg.prg_reduce body in + let ty = prg.prg_reduce obl.obl_type in match obl.obl_status with | Expand -> { obl with obl_body = Some body } | Define opaque -> @@ -321,9 +300,7 @@ let declare_obligation prg obl body = print_message (Subtac_utils.definition_message obl.obl_name); { obl with obl_body = Some (mkConst constant) } -let red = Reductionops.nf_betaiota Evd.empty - -let init_prog_info n b t deps fixkind notations obls impls kind hook = +let init_prog_info n b t deps fixkind notations obls impls kind reduce hook = let obls', b = match b with | None -> @@ -337,13 +314,13 @@ let init_prog_info n b t deps fixkind notations obls impls kind hook = Array.mapi (fun i (n, t, l, o, d, tac) -> { obl_name = n ; obl_body = None; - obl_location = l; obl_type = red t; obl_status = o; + obl_location = l; obl_type = reduce t; obl_status = o; obl_deps = d; obl_tac = tac }) obls, b in - { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls'); + { prg_name = n ; prg_body = b; prg_type = reduce t; prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; - prg_implicits = impls; prg_kind = kind; prg_hook = hook; } + prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; prg_hook = hook; } let get_prog name = let prg_infos = !from_prg in @@ -469,7 +446,7 @@ let rec solve_obligation prg num tac = | _ -> ()); trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ Subtac_utils.my_print_constr (Global.env ()) obl.obl_type); - Pfedit.by !default_tactic; + Pfedit.by (snd (get_default_tactic ())); Option.iter (fun tac -> Pfedit.set_end_tac (Tacinterp.interp tac)) tac; Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " @@ -501,7 +478,7 @@ and solve_obligation_by_tac prg obls i tac = | None -> match obl.obl_tac with | Some t -> t - | None -> !default_tactic + | None -> snd (get_default_tactic ()) in let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in obls.(i) <- declare_obligation prg obl t; @@ -579,9 +556,10 @@ let show_term n = my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ my_print_constr (Global.env ()) prg.prg_body) -let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun _ _ -> ()) obls = +let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic + ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls = Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); - let prg = init_prog_info n term t [] None [] obls implicits kind hook in + let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in let obls,_ = prg.prg_obligations in if Array.length obls = 0 then ( Flags.if_verbose ppnl (str "."); @@ -596,12 +574,14 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?ta | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res | _ -> res) -let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun _ _ -> ()) notations fixkind = +let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) + ?(hook=fun _ _ -> ()) notations fixkind = let deps = List.map (fun (n, b, t, imps, obls) -> n) l in let upd = List.fold_left (fun acc (n, b, t, imps, obls) -> - let prg = init_prog_info n (Some b) t deps (Some fixkind) notations obls imps kind hook in - ProgMap.add n prg acc) + let prg = init_prog_info n (Some b) t deps (Some fixkind) + notations obls imps kind reduce hook + in ProgMap.add n prg acc) !from_prg l in from_prg := upd; @@ -647,6 +627,3 @@ let next_obligation n tac = try array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls with Not_found -> anomaly "Could not find a solvable obligation." in solve_obligation prg i tac - -let default_tactic () = !default_tactic -let default_tactic_expr () = !default_tactic_expr diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli index 1608c134..bc5fc3e1 100644 --- a/plugins/subtac/subtac_obligations.mli +++ b/plugins/subtac/subtac_obligations.mli @@ -3,6 +3,7 @@ open Util open Libnames open Evd open Proof_type +open Vernacexpr type obligation_info = (identifier * Term.types * loc * @@ -16,8 +17,8 @@ type progress = (* Resolution status of a program *) | Defined of global_reference (* Defined as id *) val set_default_tactic : bool -> Tacexpr.glob_tactic_expr -> unit -val default_tactic : unit -> Proof_type.tactic -val default_tactic_expr : unit -> Tacexpr.glob_tactic_expr +val get_default_tactic : unit -> locality_flag * Proof_type.tactic +val print_default_tactic : unit -> Pp.std_ppcmds val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *) val get_proofs_transparency : unit -> bool @@ -26,6 +27,7 @@ val add_definition : Names.identifier -> ?term:Term.constr -> Term.types -> ?implicits:(Topconstr.explicitation * (bool * bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> ?tactic:Proof_type.tactic -> + ?reduce:(Term.constr -> Term.constr) -> ?hook:(Tacexpr.declaration_hook) -> obligation_info -> progress type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list @@ -39,6 +41,7 @@ val add_mutual_definitions : (Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list -> ?tactic:Proof_type.tactic -> ?kind:Decl_kinds.definition_kind -> + ?reduce:(Term.constr -> Term.constr) -> ?hook:Tacexpr.declaration_hook -> notations -> fixpoint_kind -> unit diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index 030bb3c5..23323ab3 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: subtac_pretyping.ml 13344 2010-07-28 15:04:36Z msozeau $ *) open Global open Pp @@ -70,7 +70,7 @@ let merge_evms x y = let interp env isevars c tycon = let j = pretype tycon env isevars ([],[]) c in let _ = isevars := Evarutil.nf_evar_map !isevars in - let evd,_ = consider_remaining_unif_problems env !isevars in + let evd = consider_remaining_unif_problems env !isevars in (* let unevd = undefined_evars evd in *) let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:false env unevd' in @@ -86,8 +86,10 @@ let find_with_index x l = open Vernacexpr -let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr ( evd) env -let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type ( evd) env +let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = + Constrintern.intern_constr evd env +let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = + Constrintern.intern_type evd env let env_with_binders env isevars l = let rec aux ((env, rels) as acc) = function @@ -109,21 +111,25 @@ let env_with_binders env isevars l = | [] -> acc in aux (env, []) l -let subtac_process env isevars id bl c tycon = +let subtac_process ?(is_type=false) env isevars id bl c tycon = let c = Topconstr.abstract_constr_expr c bl in - let tycon = + let tycon, imps = match tycon with - None -> empty_tycon + None -> empty_tycon, None | Some t -> let t = Topconstr.prod_constr_expr t bl in let t = coqintern_type !isevars env t in + let imps = Implicit_quantifiers.implicits_of_rawterm t in let coqt, ttyp = interp env isevars t empty_tycon in - mk_tycon coqt + mk_tycon coqt, Some imps in let c = coqintern_constr !isevars env c in - let imps = Implicit_quantifiers.implicits_of_rawterm c in + let imps = match imps with + | Some i -> i + | None -> Implicit_quantifiers.implicits_of_rawterm ~with_products:is_type c + in let coqc, ctyp = interp env isevars c tycon in - let evm = non_instanciated_map env isevars ( !isevars) in + let evm = non_instanciated_map env isevars !isevars in let ty = nf_evar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in evm, coqc, ty, imps diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli index 055c6df2..48906b23 100644 --- a/plugins/subtac/subtac_pretyping.mli +++ b/plugins/subtac/subtac_pretyping.mli @@ -16,7 +16,7 @@ val interp : Rawterm.rawconstr -> Evarutil.type_constraint -> Term.constr * Term.constr -val subtac_process : env -> evar_map ref -> identifier -> local_binder list -> +val subtac_process : ?is_type:bool -> env -> evar_map ref -> identifier -> local_binder list -> constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list val subtac_proof : Decl_kinds.definition_kind -> Tacexpr.declaration_hook -> env -> evar_map ref -> identifier -> local_binder list -> diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 16f2031b..7fcd4267 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: subtac_pretyping_F.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Pp open Util @@ -166,6 +166,28 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | RProp c -> judge_of_prop_contents c | RType _ -> judge_of_new_Type () + let split_tycon_lam loc env evd tycon = + let rec real_split evd c = + let t = whd_betadeltaiota env evd c in + match kind_of_term t with + | Prod (na,dom,rng) -> evd, (na, dom, rng) + | Evar ev when not (Evd.is_defined_evar evd ev) -> + let (evd',prod) = define_evar_as_product evd ev in + let (_,dom,rng) = destProd prod in + evd',(Anonymous, dom, rng) + | _ -> error_not_product_loc loc env evd c + in + match tycon with + | None -> evd,(Anonymous,None,None) + | Some (abs, c) -> + (match abs with + | None -> + let evd', (n, dom, rng) = real_split evd c in + evd', (n, mk_tycon dom, mk_tycon rng) + | Some (init, cur) -> + evd, (Anonymous, None, Some (Some (init, succ cur), c))) + + (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [( evdref)] and *) (* the type constraint tycon *) @@ -233,7 +255,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let newenv = let marked_ftys = Array.map (fun ty -> let sort = Retyping.get_type_of env !evdref ty in - mkApp (Lazy.force Subtac_utils.fix_proto, [| sort; ty |])) + mkApp (delayed_force Subtac_utils.fix_proto, [| sort; ty |])) ftys in push_rec_types (names,marked_ftys,[||]) env @@ -355,7 +377,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct evd, Some ty') evdref tycon in - let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon' in + let (name',dom,rng) = evd_comb1 (split_tycon_lam loc env) evdref tycon' in let dom_valcon = valcon_of_tycon dom in let j = pretype_type dom_valcon env evdref lvar c1 in let var = (name,None,j.utj_val) in @@ -586,11 +608,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (pretype tycon env evdref lvar c).uj_val | IsType -> (pretype_type empty_valcon env evdref lvar c).utj_val in - evdref := fst (consider_remaining_unif_problems env !evdref); + evdref := consider_remaining_unif_problems env !evdref; if resolve_classes then - evdref := - Typeclasses.resolve_typeclasses ~onlyargs:false + (evdref := Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:fail_evar env !evdref; + evdref := consider_remaining_unif_problems env !evdref); let c = if expand_evar then nf_evar !evdref c' else c' in if fail_evar then check_evars env Evd.empty !evdref c; c @@ -603,7 +625,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let understand_judgment sigma env c = let evdref = ref (create_evar_defs sigma) in let j = pretype empty_tycon env evdref ([],[]) c in - let evd,_ = consider_remaining_unif_problems env !evdref in + let evd = consider_remaining_unif_problems env !evdref in let j = j_nf_evar evd j in check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 06a80f68..689b110f 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -1,3 +1,5 @@ +(** -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *) + open Evd open Libnames open Coqlib @@ -18,14 +20,14 @@ let utils_module = "Utils" let fixsub_module = subtac_dir @ [fix_sub_module] let utils_module = subtac_dir @ [utils_module] let tactics_module = subtac_dir @ ["Tactics"] -let init_constant dir s = gen_constant contrib_name dir s -let init_reference dir s = gen_reference contrib_name dir s +let init_constant dir s () = gen_constant contrib_name dir s +let init_reference dir s () = gen_reference contrib_name dir s -let fixsub = lazy (init_constant fixsub_module "Fix_sub") -let ex_pi1 = lazy (init_constant utils_module "ex_pi1") -let ex_pi2 = lazy (init_constant utils_module "ex_pi2") +let fixsub = init_constant fixsub_module "Fix_sub" +let ex_pi1 = init_constant utils_module "ex_pi1" +let ex_pi2 = init_constant utils_module "ex_pi2" -let make_ref l s = lazy (init_reference l s) +let make_ref l s = init_reference l s let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded" let acc_ref = make_ref ["Init";"Wf"] "Acc" let acc_inv_ref = make_ref ["Init";"Wf"] "Acc_inv" @@ -41,68 +43,67 @@ let proj1_sig_ref = make_ref "Init.Specif.proj1_sig" let proj2_sig_ref = make_ref "Init.Specif.proj2_sig" let build_sig () = - { proj1 = init_constant ["Init"; "Specif"] "proj1_sig"; - proj2 = init_constant ["Init"; "Specif"] "proj2_sig"; - elim = init_constant ["Init"; "Specif"] "sig_rec"; - intro = init_constant ["Init"; "Specif"] "exist"; - typ = init_constant ["Init"; "Specif"] "sig" } + { proj1 = init_constant ["Init"; "Specif"] "proj1_sig" (); + proj2 = init_constant ["Init"; "Specif"] "proj2_sig" (); + elim = init_constant ["Init"; "Specif"] "sig_rec" (); + intro = init_constant ["Init"; "Specif"] "exist" (); + typ = init_constant ["Init"; "Specif"] "sig" () } -let sig_ = lazy (build_sig ()) +let sig_ = build_sig -let fix_proto = lazy (init_constant tactics_module "fix_proto") +let fix_proto = init_constant tactics_module "fix_proto" let fix_proto_ref () = match Nametab.global (make_ref "Program.Tactics.fix_proto") with | ConstRef c -> c | _ -> assert false -let eq_ind = lazy (init_constant ["Init"; "Logic"] "eq") -let eq_rec = lazy (init_constant ["Init"; "Logic"] "eq_rec") -let eq_rect = lazy (init_constant ["Init"; "Logic"] "eq_rect") -let eq_refl = lazy (init_constant ["Init"; "Logic"] "refl_equal") -let eq_ind_ref = lazy (init_reference ["Init"; "Logic"] "eq") -let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal") +let eq_ind = init_constant ["Init"; "Logic"] "eq" +let eq_rec = init_constant ["Init"; "Logic"] "eq_rec" +let eq_rect = init_constant ["Init"; "Logic"] "eq_rect" +let eq_refl = init_constant ["Init"; "Logic"] "refl_equal" +let eq_ind_ref = init_reference ["Init"; "Logic"] "eq" +let refl_equal_ref = init_reference ["Init"; "Logic"] "refl_equal" -let not_ref = lazy (init_constant ["Init"; "Logic"] "not") +let not_ref = init_constant ["Init"; "Logic"] "not" -let and_typ = lazy (Coqlib.build_coq_and ()) +let and_typ = Coqlib.build_coq_and -let eqdep_ind = lazy (init_constant [ "Logic";"Eqdep"] "eq_dep") -let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec") -let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep") -let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro") +let eqdep_ind = init_constant [ "Logic";"Eqdep"] "eq_dep" +let eqdep_rec = init_constant ["Logic";"Eqdep"] "eq_dep_rec" +let eqdep_ind_ref = init_reference [ "Logic";"Eqdep"] "eq_dep" +let eqdep_intro_ref = init_reference [ "Logic";"Eqdep"] "eq_dep_intro" let jmeq_ind = - lazy (check_required_library ["Coq";"Logic";"JMeq"]; - init_constant ["Logic";"JMeq"] "JMeq") + init_constant ["Logic";"JMeq"] "JMeq" + let jmeq_rec = - lazy (check_required_library ["Coq";"Logic";"JMeq"]; - init_constant ["Logic";"JMeq"] "JMeq_rec") + init_constant ["Logic";"JMeq"] "JMeq_rec" + let jmeq_refl = - lazy (check_required_library ["Coq";"Logic";"JMeq"]; - init_constant ["Logic";"JMeq"] "JMeq_refl") + init_constant ["Logic";"JMeq"] "JMeq_refl" -let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex") -let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro") +let ex_ind = init_constant ["Init"; "Logic"] "ex" +let ex_intro = init_reference ["Init"; "Logic"] "ex_intro" -let proj1 = lazy (init_constant ["Init"; "Logic"] "proj1") -let proj2 = lazy (init_constant ["Init"; "Logic"] "proj2") +let proj1 = init_constant ["Init"; "Logic"] "proj1" +let proj2 = init_constant ["Init"; "Logic"] "proj2" -let boolind = lazy (init_constant ["Init"; "Datatypes"] "bool") -let sumboolind = lazy (init_constant ["Init"; "Specif"] "sumbool") -let natind = lazy (init_constant ["Init"; "Datatypes"] "nat") -let intind = lazy (init_constant ["ZArith"; "binint"] "Z") -let existSind = lazy (init_constant ["Init"; "Specif"] "sigS") +let boolind = init_constant ["Init"; "Datatypes"] "bool" +let sumboolind = init_constant ["Init"; "Specif"] "sumbool" +let natind = init_constant ["Init"; "Datatypes"] "nat" +let intind = init_constant ["ZArith"; "binint"] "Z" +let existSind = init_constant ["Init"; "Specif"] "sigS" -let existS = lazy (build_sigma_type ()) +let existS = build_sigma_type -let prod = lazy (build_prod ()) +let prod = build_prod (* orders *) -let well_founded = lazy (init_constant ["Init"; "Wf"] "well_founded") -let fix = lazy (init_constant ["Init"; "Wf"] "Fix") -let acc = lazy (init_constant ["Init"; "Wf"] "Acc") -let acc_inv = lazy (init_constant ["Init"; "Wf"] "Acc_inv") +let well_founded = init_constant ["Init"; "Wf"] "well_founded" +let fix = init_constant ["Init"; "Wf"] "Fix" +let acc = init_constant ["Init"; "Wf"] "Acc" +let acc_inv = init_constant ["Init"; "Wf"] "Acc_inv" let extconstr = Constrextern.extern_constr true (Global.env ()) let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s) @@ -151,8 +152,8 @@ let wf_relations = Hashtbl.create 10 let std_relations () = let add k v = Hashtbl.add wf_relations k v in - add (init_constant ["Init"; "Peano"] "lt") - (lazy (init_constant ["Arith"; "Wf_nat"] "lt_wf")) + add (init_constant ["Init"; "Peano"] "lt" ()) + (init_constant ["Arith"; "Wf_nat"] "lt_wf") let std_relations = Lazy.lazy_from_fun std_relations @@ -226,7 +227,6 @@ let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixp open Tactics open Tacticals -let id x = x let filter_map f l = let rec aux acc = function hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl @@ -257,51 +257,51 @@ let build_dependent_sum l = (fun typ -> let tex = mkLambda (Name n, t, typ) in conttype - (mkApp (Lazy.force ex_ind, [| t; tex |]))) + (mkApp (ex_ind (), [| t; tex |]))) in aux (mkVar n :: names) conttac conttype tl | (n, t) :: [] -> (conttac intros, conttype t) | [] -> raise (Invalid_argument "build_dependent_sum") - in aux [] id id (List.rev l) + in aux [] identity identity (List.rev l) open Proof_type open Tacexpr let mkProj1 a b c = - mkApp (Lazy.force proj1, [| a; b; c |]) + mkApp (delayed_force proj1, [| a; b; c |]) let mkProj2 a b c = - mkApp (Lazy.force proj2, [| a; b; c |]) + mkApp (delayed_force proj2, [| a; b; c |]) let mk_ex_pi1 a b c = - mkApp (Lazy.force ex_pi1, [| a; b; c |]) + mkApp (delayed_force ex_pi1, [| a; b; c |]) let mk_ex_pi2 a b c = - mkApp (Lazy.force ex_pi2, [| a; b; c |]) + mkApp (delayed_force ex_pi2, [| a; b; c |]) let mkSubset name typ prop = - mkApp ((Lazy.force sig_).typ, + mkApp ((delayed_force sig_).typ, [| typ; mkLambda (name, typ, prop) |]) -let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |]) -let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |]) -let mk_JMeq typ x typ' y = mkApp (Lazy.force jmeq_ind, [| typ; x ; typ'; y |]) -let mk_JMeq_refl typ x = mkApp (Lazy.force jmeq_refl, [| typ; x |]) +let mk_eq typ x y = mkApp (delayed_force eq_ind, [| typ; x ; y |]) +let mk_eq_refl typ x = mkApp (delayed_force eq_refl, [| typ; x |]) +let mk_JMeq typ x typ' y = mkApp (delayed_force jmeq_ind, [| typ; x ; typ'; y |]) +let mk_JMeq_refl typ x = mkApp (delayed_force jmeq_refl, [| typ; x |]) let unsafe_fold_right f = function hd :: tl -> List.fold_right f tl hd | [] -> raise (Invalid_argument "unsafe_fold_right") let mk_conj l = - let conj_typ = Lazy.force and_typ in + let conj_typ = delayed_force and_typ in unsafe_fold_right (fun c conj -> mkApp (conj_typ, [| c ; conj |])) l let mk_not c = - let notc = Lazy.force not_ref in + let notc = delayed_force not_ref in mkApp (notc, [| c |]) let and_tac l hook = @@ -336,7 +336,7 @@ let destruct_ex ext ex = match kind_of_term c with App (f, args) -> (match kind_of_term f with - Ind i when i = Term.destInd (Lazy.force ex_ind) && Array.length args = 2 -> + Ind i when i = Term.destInd (delayed_force ex_ind) && Array.length args = 2 -> let (dom, rng) = try (args.(0), args.(1)) with _ -> assert(false) @@ -477,6 +477,7 @@ let pr_evar_map evd = let contrib_tactics_path = make_dirpath (List.map id_of_string ["Tactics";contrib_name;"Coq"]) + let tactics_tac s = lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s)) diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli index d0ad334d..f56c2932 100644 --- a/plugins/subtac/subtac_utils.mli +++ b/plugins/subtac/subtac_utils.mli @@ -17,53 +17,53 @@ val contrib_name : string val subtac_dir : string list val fix_sub_module : string val fixsub_module : string list -val init_constant : string list -> string -> constr -val init_reference : string list -> string -> global_reference -val fixsub : constr lazy_t -val well_founded_ref : global_reference lazy_t -val acc_ref : global_reference lazy_t -val acc_inv_ref : global_reference lazy_t -val fix_sub_ref : global_reference lazy_t -val measure_on_R_ref : global_reference lazy_t -val fix_measure_sub_ref : global_reference lazy_t -val refl_ref : global_reference lazy_t +val init_constant : string list -> string -> constr delayed +val init_reference : string list -> string -> global_reference delayed +val fixsub : constr delayed +val well_founded_ref : global_reference delayed +val acc_ref : global_reference delayed +val acc_inv_ref : global_reference delayed +val fix_sub_ref : global_reference delayed +val measure_on_R_ref : global_reference delayed +val fix_measure_sub_ref : global_reference delayed +val refl_ref : global_reference delayed val lt_ref : reference val sig_ref : reference val proj1_sig_ref : reference val proj2_sig_ref : reference val build_sig : unit -> coq_sigma_data -val sig_ : coq_sigma_data lazy_t +val sig_ : coq_sigma_data delayed -val fix_proto : constr lazy_t +val fix_proto : constr delayed val fix_proto_ref : unit -> constant -val eq_ind : constr lazy_t -val eq_rec : constr lazy_t -val eq_rect : constr lazy_t -val eq_refl : constr lazy_t - -val not_ref : constr lazy_t -val and_typ : constr lazy_t - -val eqdep_ind : constr lazy_t -val eqdep_rec : constr lazy_t - -val jmeq_ind : constr lazy_t -val jmeq_rec : constr lazy_t -val jmeq_refl : constr lazy_t - -val boolind : constr lazy_t -val sumboolind : constr lazy_t -val natind : constr lazy_t -val intind : constr lazy_t -val existSind : constr lazy_t -val existS : coq_sigma_data lazy_t -val prod : coq_sigma_data lazy_t - -val well_founded : constr lazy_t -val fix : constr lazy_t -val acc : constr lazy_t -val acc_inv : constr lazy_t +val eq_ind : constr delayed +val eq_rec : constr delayed +val eq_rect : constr delayed +val eq_refl : constr delayed + +val not_ref : constr delayed +val and_typ : constr delayed + +val eqdep_ind : constr delayed +val eqdep_rec : constr delayed + +val jmeq_ind : constr delayed +val jmeq_rec : constr delayed +val jmeq_refl : constr delayed + +val boolind : constr delayed +val sumboolind : constr delayed +val natind : constr delayed +val intind : constr delayed +val existSind : constr delayed +val existS : coq_sigma_data delayed +val prod : coq_sigma_data delayed + +val well_founded : constr delayed +val fix : constr delayed +val acc : constr delayed +val acc_inv : constr delayed val extconstr : constr -> constr_expr val extsort : sorts -> constr_expr @@ -81,7 +81,7 @@ val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds val debug : int -> std_ppcmds -> unit val debug_msg : int -> std_ppcmds -> std_ppcmds val trace : std_ppcmds -> unit -val wf_relations : (constr, constr lazy_t) Hashtbl.t +val wf_relations : (constr, constr delayed) Hashtbl.t type binders = local_binder list val app_opt : ('a -> 'a) option -> 'a -> 'a diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 19473dfa..ae3afff4 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id$ i*) +(*i $Id: ascii_syntax.ml 12406 2009-10-21 15:12:52Z soubiran $ i*) open Pp open Util diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 89419d5e..1e9a055f 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: nat_syntax.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* This file defines the printer for natural numbers in [nat] *) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index 162588ac..787577b2 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: numbers_syntax.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) (* digit-based syntax for int31, bigN bigZ and bigQ *) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index f8e8e210..af1477f1 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: r_syntax.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) open Pp open Util diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index bc02357a..534605c8 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id$ i*) +(*i $Id: string_syntax.ml 12337 2009-09-17 15:58:14Z glondu $ i*) open Pp open Util diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 931bd77d..87f14a64 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: z_syntax.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pcoq open Pp diff --git a/plugins/xml/xml.mli b/plugins/xml/xml.mli index cfa050d7..2a9d1de4 100644 --- a/plugins/xml/xml.mli +++ b/plugins/xml/xml.mli @@ -12,7 +12,7 @@ (* http://helm.cs.unibo.it *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: xml.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (* Tokens for XML cdata, empty elements and not-empty elements *) (* Usage: *) diff --git a/plugins/xml/xmlcommand.mli b/plugins/xml/xmlcommand.mli index fc9fbf32..476ad630 100644 --- a/plugins/xml/xmlcommand.mli +++ b/plugins/xml/xmlcommand.mli @@ -12,7 +12,7 @@ (* http://helm.cs.unibo.it *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: xmlcommand.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (* print_global qid fn *) (* where qid is a long name denoting a definition/theorem or *) diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4 index a6d815da..bf6c7388 100644 --- a/plugins/xml/xmlentries.ml4 +++ b/plugins/xml/xmlentries.ml4 @@ -14,7 +14,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: xmlentries.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Util;; open Vernacinterp;; |