diff options
| -rw-r--r-- | Makefile.doc | 3 | ||||
| -rwxr-xr-x | dev/build/windows/MakeCoq_88git_installer.bat | 27 | ||||
| -rw-r--r-- | dev/build/windows/MakeCoq_MinGW.bat | 3 | ||||
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 12 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh | 12 | ||||
| -rw-r--r-- | doc/refman/Misc.tex | 63 | ||||
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 1 | ||||
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 67 | ||||
| -rw-r--r-- | doc/sphinx/index.rst | 1 | ||||
| -rwxr-xr-x | ide/MacOS/relatify_with-respect-to_.sh | 15 | ||||
| -rw-r--r-- | interp/impargs.ml | 294 | ||||
| -rw-r--r-- | intf/misctypes.ml | 13 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/pltac.mli | 2 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.mli | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacarg.mli | 6 | ||||
| -rw-r--r-- | plugins/ltac/tacexpr.ml | 18 | ||||
| -rw-r--r-- | plugins/ltac/tacexpr.mli | 18 | ||||
| -rw-r--r-- | tactics/equality.mli | 10 | ||||
| -rw-r--r-- | tactics/inv.ml | 5 | ||||
| -rw-r--r-- | tactics/inv.mli | 5 | ||||
| -rw-r--r-- | tactics/tactics.ml | 7 | ||||
| -rw-r--r-- | tactics/tactics.mli | 8 |
23 files changed, 331 insertions, 263 deletions
diff --git a/Makefile.doc b/Makefile.doc index 0b45b9cec..fc791ce1c 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -60,8 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex \ - Universes.v.tex \ - Misc.v.tex) + Universes.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ diff --git a/dev/build/windows/MakeCoq_88git_installer.bat b/dev/build/windows/MakeCoq_88git_installer.bat new file mode 100755 index 000000000..b016fb389 --- /dev/null +++ b/dev/build/windows/MakeCoq_88git_installer.bat @@ -0,0 +1,27 @@ +@ECHO OFF
+
+REM ========== COPYRIGHT/COPYLEFT ==========
+
+REM (C) 2016 Intel Deutschland GmbH
+REM Author: Michael Soegtrop
+
+REM Released to the public by Intel under the
+REM GNU Lesser General Public License Version 2.1 or later
+REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
+
+REM ========== BUILD COQ ==========
+
+call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -installer=Y ^
+ -coqver=git-v8.8 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_88_inst ^
+ -destcoq=%ROOTPATH%\coq64_88_inst ^
+ -addon=bignums
+
+IF %ERRORLEVEL% NEQ 0 (
+ ECHO MakeCoq_88git_installer.bat failed with error code %ERRORLEVEL%
+ EXIT /b %ERRORLEVEL%
+)
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index ccf22cc86..f960ff008 100644 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -34,7 +34,7 @@ REM see -ocaml in ReadMe.txt SET INSTALLOCAML=N REM see -make in ReadMe.txt -SET INSTALLMAKE=Y +SET INSTALLMAKE=N REM see -destcyg in ReadMe.txt SET DESTCYG=C:\bin\cygwin_coq @@ -267,7 +267,6 @@ IF "%INSTALLMODE%" == "mingwincygwin" ( IF "%MAKEINSTALLER%" == "Y" ( SET INSTALLMODE=relocatable SET INSTALLOCAML=Y - SET INSTALLMAKE=Y ) REM ========== CONFIRM PARAMETERS ========== diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 8e0d2341d..918900ccb 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -142,18 +142,22 @@ LOGS=`pwd`/buildlogs # The current log target (first part of the log file name) LOGTARGET=other +# Log command output - take log target name from command name (like log1 make => log target is "<module>-make") log1() { "$@" > $LOGS/$LOGTARGET-$1.log 2> $LOGS/$LOGTARGET-$1.err } +# Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install") log2() { "$@" > $LOGS/$LOGTARGET-$1-$2.log 2> $LOGS/$LOGTARGET-$1-$2.err } +# Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure") log_1_3() { "$@" > $LOGS/$LOGTARGET-$1-$3.log 2> $LOGS/$LOGTARGET-$1-$3.err } +# Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar") logn() { LOGTARGETEX=$1 shift @@ -1281,7 +1285,6 @@ function get_cygwin_mingw_sources { function make_coq_installer { make_coq - make_mingw_make get_cygwin_mingw_sources # Prepare the file lists for the installer. We created to file list dumps of the target folder during the build: @@ -1334,12 +1337,13 @@ function make_coq_installer { } ###################### ADDONS ##################### + function make_addon_bignums { - if build_prep https://github.com/coq/bignums/archive/ V8.8+beta1 zip 1; then + if build_prep https://github.com/coq/bignums/archive/ V8.8+beta1 zip 1 bignums-8.8+beta1; then # To make command lines shorter :-( echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local - logn make make all - logn make-install make install + log1 make all + log2 make install build_post fi } diff --git a/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh b/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh new file mode 100644 index 000000000..cf2af9ae9 --- /dev/null +++ b/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "6960" ] || [ "$CI_BRANCH" = "ltac+tacdepr" ]; then + + # Equations_CI_BRANCH=ssr+correct_packing + # Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + ltac2_CI_BRANCH=ltac+tacdepr + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + # Elpi_CI_BRANCH=ssr+correct_packing + # Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git + +fi diff --git a/doc/refman/Misc.tex b/doc/refman/Misc.tex deleted file mode 100644 index ab00fbfe3..000000000 --- a/doc/refman/Misc.tex +++ /dev/null @@ -1,63 +0,0 @@ -\achapter{\protect{Miscellaneous extensions}} -%HEVEA\cutname{miscellaneous.html} - -\asection{Program derivation} - -Coq comes with an extension called {\tt Derive}, which supports -program derivation. Typically in the style of Bird and Meertens or -derivations of program refinements. To use the {\tt Derive} extension -it must first be required with {\tt Require Coq.Derive.Derive}. When -the extension is loaded, it provides the following command. - -\subsection[\tt Derive \ident$_1$ SuchThat \term{} As \ident$_2$] - {\tt Derive \ident$_1$ SuchThat \term{} As \ident$_2$\comindex{Derive}} - -The name $\ident_1$ can appear in \term. This command opens a new -proof presenting the user with a goal for \term{} in which the name -$\ident_1$ is bound to a existential variables {\tt ?x} (formally, -there are other goals standing for the existential variables but they -are shelved, as described in Section~\ref{shelve}). - -When the proof ends two constants are defined: -\begin{itemize} -\item The first one is name $\ident_1$ and is defined as the proof of - the shelved goal (which is also the value of {\tt ?x}). It is -always transparent. -\item The second one is name $\ident_2$. It has type {\tt \term}, and - its body is the proof of the initially visible goal. It is opaque if - the proof ends with {\tt Qed}, and transparent if the proof ends - with {\tt Defined}. -\end{itemize} - -\Example -\begin{coq_example*} -Require Coq.derive.Derive. -Require Import Coq.Numbers.Natural.Peano.NPeano. - -Section P. - -Variables (n m k:nat). - -\end{coq_example*} -\begin{coq_example} -Derive p SuchThat ((k*n)+(k*m) = p) As h. -Proof. -rewrite <- Nat.mul_add_distr_l. -subst p. -reflexivity. -\end{coq_example} -\begin{coq_example*} -Qed. - -End P. - -\end{coq_example*} -\begin{coq_example} -Print p. -Check h. -\end{coq_example} - -Any property can be used as \term, not only an equation. In -particular, it could be an order relation specifying some form of -program refinement or a non-executable property from which deriving a -program is convenient. diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 7e68dd752..e51116007 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -118,7 +118,6 @@ Options A and B of the licence are {\em not} elected.} \part{Addendum to the Reference Manual} \include{AddRefMan-pre}% \include{Universes.v}% Universe polymorphes -\include{Misc.v} %BEGIN LATEX \RefManCutCommand{ENDADDENDUM=\thepage} %END LATEX diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst new file mode 100644 index 000000000..b0343a8f0 --- /dev/null +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -0,0 +1,67 @@ +.. include:: ../replaces.rst + +.. _miscellaneousextensions: + +Miscellaneous extensions +======================= + +:Source: https://coq.inria.fr/distrib/current/refman/miscellaneous.html +:Converted by: Paul Steckler + +.. contents:: + :local: + :depth: 1 +---- + +Program derivation +----------------- + +|Coq| comes with an extension called ``Derive``, which supports program +derivation. Typically in the style of Bird and Meertens or derivations +of program refinements. To use the Derive extension it must first be +required with ``Require Coq.Derive.Derive``. When the extension is loaded, +it provides the following command: + +.. cmd:: Derive @ident SuchThat @term As @ident + +The first `ident` can appear in `term`. This command opens a new proof +presenting the user with a goal for term in which the name `ident` is +bound to an existential variable `?x` (formally, there are other goals +standing for the existential variables but they are shelved, as +described in Section :ref:`TODO-8.17.4`). + +When the proof ends two constants are defined: + ++ The first one is named using the first `ident` and is defined as the proof of the + shelved goal (which is also the value of `?x`). It is always + transparent. ++ The second one is named using the second `ident`. It has type `term`, and its body is + the proof of the initially visible goal. It is opaque if the proof + ends with ``Qed``, and transparent if the proof ends with ``Defined``. + +.. example:: + .. coqtop:: all + + Require Coq.derive.Derive. + Require Import Coq.Numbers.Natural.Peano.NPeano. + + Section P. + + Variables (n m k:nat). + + Derive p SuchThat ((k*n)+(k*m) = p) As h. + Proof. + rewrite <- Nat.mul_add_distr_l. + subst p. + reflexivity. + Qed. + + End P. + + Print p. + Check h. + +Any property can be used as `term`, not only an equation. In particular, +it could be an order relation specifying some form of program +refinement or a non-executable property from which deriving a program +is convenient. diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index 3dd4f8020..db03693ff 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -55,6 +55,7 @@ Table of contents addendum/nsatz addendum/generalized-rewriting addendum/parallel-proof-processing + addendum/miscellaneous-extensions .. toctree:: :caption: Reference diff --git a/ide/MacOS/relatify_with-respect-to_.sh b/ide/MacOS/relatify_with-respect-to_.sh deleted file mode 100755 index a24af9395..000000000 --- a/ide/MacOS/relatify_with-respect-to_.sh +++ /dev/null @@ -1,15 +0,0 @@ -#!/bin/sh - -set -e - -for i in "$3/"*.dylib -do install_name_tool -change "$2"/$(basename $i) @executable_path/../Resources/lib/$(basename $i) "$1" -done -case "$1" in - *.dylib) - install_name_tool -id @executable_path/../Resources/lib/$(basename $1) $1 - for i in "$3"/*.dylib - do install_name_tool -change "$2/"$(basename $1) @executable_path/../Resources/lib/$(basename $1) $i - done;; - *) -esac diff --git a/interp/impargs.ml b/interp/impargs.ml index 9ad62c0de..b424f73de 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -139,7 +139,7 @@ let argument_less = function | Hyp _, Conclusion -> true | Conclusion, _ -> false -let update pos rig (na,st) = +let update pos rig st = let e = if rig then match st with @@ -163,7 +163,7 @@ let update pos rig (na,st) = | Some (DepFlex fpos as x) -> if argument_less (pos,fpos) then DepFlex pos else x | Some Manual -> assert false - in na, Some e + in Some e (* modified is_rigid_reference with a truncated env *) let is_flexible_reference env sigma bound depth f = @@ -214,6 +214,8 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in acc +(* compute the list of implicit arguments *) + let rec is_rigid_head sigma t = match kind sigma t with | Rel _ | Evar _ -> false | Ind _ | Const _ | Var _ | Sort _ -> true @@ -226,7 +228,14 @@ let rec is_rigid_head sigma t = match kind sigma t with | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _ | Prod _ | Meta _ | Cast _ -> assert false -(* calcule la liste des arguments implicites *) +let is_rigid env sigma t = + let open Context.Rel.Declaration in + let t = whd_all env sigma t in + match kind sigma t with + | Prod (na,a,b) -> + let (_,t) = splay_prod (push_rel (LocalAssum (na,a)) env) sigma b in + is_rigid_head sigma t + | _ -> true let find_displayed_name_in all avoid na (env, b) = let envnames_b = (env, b) in @@ -234,43 +243,54 @@ let find_displayed_name_in all avoid na (env, b) = if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b else compute_displayed_name_in Evd.empty flag avoid na b -let compute_implicits_gen strict strongly_strict revpat contextual all env sigma (t : EConstr.t) = - let rigid = ref true in +let compute_implicits_names_gen all env sigma t = + let open Context.Rel.Declaration in + let rec aux env avoid names t = + let t = whd_all env sigma t in + match kind sigma t with + | Prod (na,a,b) -> + let na',avoid' = find_displayed_name_in all avoid na (names,b) in + aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b + | _ -> List.rev names + in aux env Id.Set.empty [] t + +let compute_implicits_names = compute_implicits_names_gen true + +let compute_implicits_explanation_gen strict strongly_strict revpat contextual env sigma t = let open Context.Rel.Declaration in - let rec aux env avoid n names (t : EConstr.t) = + let rec aux env n t = let t = whd_all env sigma t in match kind sigma t with - | Prod (na,a,b) -> - let na',avoid' = find_displayed_name_in all avoid na (names,b) in - add_free_rels_until strict strongly_strict revpat n env sigma a (Hyp (n+1)) - (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b) - | _ -> - rigid := is_rigid_head sigma t; - let names = List.rev names in - let v = Array.map (fun na -> na,None) (Array.of_list names) in - if contextual then - add_free_rels_until strict strongly_strict revpat n env sigma t Conclusion v - else v + | Prod (na,a,b) -> + add_free_rels_until strict strongly_strict revpat n env sigma a (Hyp (n+1)) + (aux (push_rel (LocalAssum (na,a)) env) (n+1) b) + | _ -> + let v = Array.make n None in + if contextual then + add_free_rels_until strict strongly_strict revpat n env sigma t Conclusion v + else v in match kind sigma (whd_all env sigma t) with - | Prod (na,a,b) -> - let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in - let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in - !rigid, Array.to_list v - | _ -> true, [] + | Prod (na,a,b) -> + let v = aux (push_rel (LocalAssum (na,a)) env) 1 b in + Array.to_list v + | _ -> [] -let compute_implicits_flags env sigma f all t = - compute_implicits_gen +let compute_implicits_explanation_flags env sigma f t = + compute_implicits_explanation_gen (f.strict || f.strongly_strict) f.strongly_strict - f.reversible_pattern f.contextual all env sigma t + f.reversible_pattern f.contextual env sigma t -let compute_auto_implicits env sigma flags enriching t = - if enriching then compute_implicits_flags env sigma flags true t - else compute_implicits_gen false false false true true env sigma t +let compute_implicits_flags env sigma f all t = + List.combine + (compute_implicits_names_gen all env sigma t) + (compute_implicits_explanation_flags env sigma f t) -let compute_implicits_names env sigma t = - let _, impls = compute_implicits_gen false false false false true env sigma t in - List.map fst impls +let compute_auto_implicits env sigma flags enriching t = + List.combine + (compute_implicits_names env sigma t) + (if enriching then compute_implicits_explanation_flags env sigma flags t + else compute_implicits_explanation_gen false false false true env sigma t) (* Extra information about implicit arguments *) @@ -329,13 +349,16 @@ let rec prepare_implicits f = function Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits f imps -let set_implicit id imp insmax = - (id,(match imp with None -> Manual | Some imp -> imp),insmax) - -let rec assoc_by_pos k = function - (ExplByPos (k', x), b) :: tl when Int.equal k k' -> (x,b), tl - | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl - | [] -> raise Not_found +(* +If found, returns Some (x,(b,fi,fo)) and l with the entry removed, +otherwise returns None and l unchanged. + *) +let assoc_by_pos k l = + let rec aux = function + (ExplByPos (k', x), b) :: tl when Int.equal k k' -> Some (x,b), tl + | hd :: tl -> let (x, tl) = aux tl in x, hd :: tl + | [] -> raise Not_found + in try aux l with Not_found -> None, l let check_correct_manual_implicits autoimps l = List.iter (function @@ -352,70 +375,65 @@ let check_correct_manual_implicits autoimps l = (str "Cannot set implicit argument number " ++ int i ++ str ": it has no name.")) l -let set_manual_implicits env flags enriching autoimps l = - let try_forced k l = - try - let (id, (b, fi, fo)), l' = assoc_by_pos k l in - if fo then - let id = match id with Some id -> id | None -> Id.of_string ("arg_" ^ string_of_int k) in - l', Some (id,Manual,(b,fi)) - else l, None - with Not_found -> l, None - in +(* Take a list l of explicitations, and map them to positions. *) +let flatten_explicitations l autoimps = + let rec aux k l = function + | (Name id,_)::imps -> + let value, l' = + try + let eq = explicitation_eq in + let flags = List.assoc_f eq (ExplByName id) l in + Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l + with Not_found -> assoc_by_pos k l + in value :: aux (k+1) l' imps + | (Anonymous,_)::imps -> + let value, l' = assoc_by_pos k l + in value :: aux (k+1) l' imps + | [] when List.is_empty l -> [] + | [] -> + check_correct_manual_implicits autoimps l; + [] + in aux 1 l autoimps + +let set_manual_implicits flags enriching autoimps l = if not (List.distinct l) then user_err Pp.(str "Some parameters are referred more than once."); (* Compare with automatic implicits to recover printing data and names *) - let rec merge k l = function - | (Name id,imp)::imps -> - let l',imp,m = - try - let eq = explicitation_eq in - let (b, fi, fo) = List.assoc_f eq (ExplByName id) l in - List.remove_assoc_f eq (ExplByName id) l, (Some Manual), (Some (b, fi)) - with Not_found -> - try - let (id, (b, fi, fo)), l' = assoc_by_pos k l in - l', (Some Manual), (Some (b,fi)) - with Not_found -> - let m = match enriching, imp with - | true, Some _ -> Some (flags.maximal, true) - | _ -> None - in - l, imp, m - in - let imps' = merge (k+1) l' imps in - let m = Option.map (fun (b,f) -> - (* match imp with Some Manual -> (b,f) *) - (* | _ -> *)set_maximality imps' b, f) m in - Option.map (set_implicit id imp) m :: imps' - | (Anonymous,imp)::imps -> - let l', forced = try_forced k l in - forced :: merge (k+1) l' imps - | [] when begin match l with [] -> true | _ -> false end -> [] - | [] -> - check_correct_manual_implicits autoimps l; - [] - in - merge 1 l autoimps - -let compute_semi_auto_implicits env sigma f manual t = - match manual with - | [] -> - if not f.auto then [DefaultImpArgs, []] - else let _,l = compute_implicits_flags env sigma f false t in - [DefaultImpArgs, prepare_implicits f l] - | _ -> - let _,autoimpls = compute_auto_implicits env sigma f f.auto t in - [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual] + let rec merge k autoimps explimps = match autoimps, explimps with + | autoimp::autoimps, explimp::explimps -> + let imps' = merge (k+1) autoimps explimps in + begin match autoimp, explimp with + | (Name id,_), Some (_, (b, fi, _)) -> + Some (id, Manual, (set_maximality imps' b, fi)) + | (Name id,Some exp), None when enriching -> + Some (id, exp, (set_maximality imps' flags.maximal, true)) + | (Name _,_), None -> None + | (Anonymous,_), Some (Some id, (b, fi, true)) -> + Some (id,Manual,(b,fi)) + | (Anonymous,_), Some (None, (b, fi, true)) -> + let id = Id.of_string ("arg_" ^ string_of_int k) in + Some (id,Manual,(b,fi)) + | (Anonymous,_), Some (_, (_, _, false)) -> None + | (Anonymous,_), None -> None + end :: imps' + | [], [] -> [] + (* flatten_explicitations returns a list of the same length as autoimps *) + | _ -> assert false + in merge 1 autoimps (flatten_explicitations l autoimps) + +let compute_semi_auto_implicits env sigma f t = + if not f.auto then [DefaultImpArgs, []] + else let l = compute_implicits_flags env sigma f false t in + [DefaultImpArgs, prepare_implicits f l] (*s Constants. *) -let compute_constant_implicits flags manual cst = +let compute_constant_implicits flags cst = let env = Global.env () in let sigma = Evd.from_env env in let cb = Environ.lookup_constant cst env in let ty = of_constr cb.const_type in - let impls = compute_semi_auto_implicits env sigma flags manual ty in + let impls = compute_semi_auto_implicits env sigma flags ty in impls (*s Inductives and constructors. Their implicit arguments are stored @@ -423,7 +441,7 @@ let compute_constant_implicits flags manual cst = $i$ are the implicit arguments of the inductive and $v$ the array of implicit arguments of the constructors. *) -let compute_mib_implicits flags manual kn = +let compute_mib_implicits flags kn = let env = Global.env () in let sigma = Evd.from_env env in let mib = Environ.lookup_mind kn env in @@ -439,34 +457,34 @@ let compute_mib_implicits flags manual kn = let imps_one_inductive i mip = let ind = (kn,i) in let ar, _ = Global.type_of_global_in_context env (IndRef ind) in - ((IndRef ind,compute_semi_auto_implicits env sigma flags manual (of_constr ar)), + ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)), Array.mapi (fun j c -> - (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags manual c)) + (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c)) (Array.map of_constr mip.mind_nf_lc)) in Array.mapi imps_one_inductive mib.mind_packets -let compute_all_mib_implicits flags manual kn = - let imps = compute_mib_implicits flags manual kn in +let compute_all_mib_implicits flags kn = + let imps = compute_mib_implicits flags kn in List.flatten (Array.map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps) (*s Variables. *) -let compute_var_implicits flags manual id = +let compute_var_implicits flags id = let env = Global.env () in let sigma = Evd.from_env env in - compute_semi_auto_implicits env sigma flags manual (NamedDecl.get_type (lookup_named id env)) + compute_semi_auto_implicits env sigma flags (NamedDecl.get_type (lookup_named id env)) (* Implicits of a global reference. *) -let compute_global_implicits flags manual = function - | VarRef id -> compute_var_implicits flags manual id - | ConstRef kn -> compute_constant_implicits flags manual kn +let compute_global_implicits flags = function + | VarRef id -> compute_var_implicits flags id + | ConstRef kn -> compute_constant_implicits flags kn | IndRef (kn,i) -> - let ((_,imps),_) = (compute_mib_implicits flags manual kn).(i) in imps + let ((_,imps),_) = (compute_mib_implicits flags kn).(i) in imps | ConstructRef ((kn,i),j) -> - let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1) + let (_,cimps) = (compute_mib_implicits flags kn).(i) in snd cimps.(j-1) (* Merge a manual explicitation with an implicit_status list *) @@ -573,34 +591,34 @@ let rebuild_implicits (req,l) = | ImplLocal -> assert false | ImplConstant (con,flags) -> let oldimpls = snd (List.hd l) in - let newimpls = compute_constant_implicits flags [] con in + let newimpls = compute_constant_implicits flags con in req, [ConstRef con, List.map2 merge_impls oldimpls newimpls] | ImplMutualInductive (kn,flags) -> - let newimpls = compute_all_mib_implicits flags [] kn in + let newimpls = compute_all_mib_implicits flags kn in let rec aux olds news = - match olds, news with - | (_, oldimpls) :: old, (gr, newimpls) :: tl -> - (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl - | [], [] -> [] - | _, _ -> assert false + match olds, news with + | (_, oldimpls) :: old, (gr, newimpls) :: tl -> + (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl + | [], [] -> [] + | _, _ -> assert false in req, aux l newimpls | ImplInteractive (ref,flags,o) -> (if isVarRef ref && is_in_section ref then ImplLocal else req), match o with | ImplAuto -> - let oldimpls = snd (List.hd l) in - let newimpls = compute_global_implicits flags [] ref in - [ref,List.map2 merge_impls oldimpls newimpls] + let oldimpls = snd (List.hd l) in + let newimpls = compute_global_implicits flags ref in + [ref,List.map2 merge_impls oldimpls newimpls] | ImplManual userimplsize -> - let oldimpls = snd (List.hd l) in - if flags.auto then - let newimpls = List.hd (compute_global_implicits flags [] ref) in - let p = List.length (snd newimpls) - userimplsize in - let newimpls = on_snd (List.firstn p) newimpls in - [ref,List.map (fun o -> merge_impls o newimpls) oldimpls] - else - [ref,oldimpls] + let oldimpls = snd (List.hd l) in + if flags.auto then + let newimpls = List.hd (compute_global_implicits flags ref) in + let p = List.length (snd newimpls) - userimplsize in + let newimpls = on_snd (List.firstn p) newimpls in + [ref,List.map (fun o -> merge_impls o newimpls) oldimpls] + else + [ref,oldimpls] let classify_implicits (req,_ as obj) = match req with | ImplLocal -> Dispose @@ -622,7 +640,7 @@ let inImplicits : implicits_obj -> obj = let is_local local ref = local || isVarRef ref && is_in_section ref let declare_implicits_gen req flags ref = - let imps = compute_global_implicits flags [] ref in + let imps = compute_global_implicits flags ref in add_anonymous_leaf (inImplicits (req,[ref,imps])) let declare_implicits local ref = @@ -643,7 +661,7 @@ let declare_mib_implicits kn = let flags = !implicit_args in let imps = Array.map_to_list (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) - (compute_mib_implicits flags [] kn) in + (compute_mib_implicits flags kn) in add_anonymous_leaf (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps)) @@ -653,8 +671,8 @@ type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool) type manual_implicits = manual_explicitation list let compute_implicits_with_manual env sigma typ enriching l = - let _,autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in - set_manual_implicits env !implicit_args enriching autoimpls l + let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in + set_manual_implicits !implicit_args enriching autoimpls l let check_inclusion l = (* Check strict inclusion *) @@ -679,26 +697,26 @@ let declare_manual_implicits local ref ?enriching l = let env = Global.env () in let sigma = Evd.from_env env in let t, _ = Global.type_of_global_in_context env ref in + let t = of_constr t in let enriching = Option.default flags.auto enriching in - let isrigid,autoimpls = compute_auto_implicits env sigma flags enriching (of_constr t) in + let autoimpls = compute_auto_implicits env sigma flags enriching t in let l' = match l with | [] -> assert false | [l] -> - [DefaultImpArgs, set_manual_implicits env flags enriching autoimpls l] + [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] | _ -> - check_rigidity isrigid; - let l = List.map (fun imps -> (imps,List.length imps)) l in - let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in - check_inclusion l; - let nargs = List.length autoimpls in - List.map (fun (imps,n) -> - (LessArgsThan (nargs-n), - set_manual_implicits env flags enriching autoimpls imps)) l in + check_rigidity (is_rigid env sigma t); + let l = List.map (fun imps -> (imps,List.length imps)) l in + let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in + check_inclusion l; + let nargs = List.length autoimpls in + List.map (fun (imps,n) -> + (LessArgsThan (nargs-n), + set_manual_implicits flags enriching autoimpls imps)) l in let req = if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) - in - add_anonymous_leaf (inImplicits (req,[ref,l'])) + in add_anonymous_leaf (inImplicits (req,[ref,l'])) let maybe_declare_manual_implicits local ref ?enriching l = match l with diff --git a/intf/misctypes.ml b/intf/misctypes.ml index 9eb6f62cc..72db3b31c 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -142,19 +142,6 @@ type multi = | RepeatStar | RepeatPlus -type 'a core_destruction_arg = - | ElimOnConstr of 'a - | ElimOnIdent of lident - | ElimOnAnonHyp of int - -type 'a destruction_arg = - clear_flag * 'a core_destruction_arg - -type inversion_kind = - | SimpleInversion - | FullInversion - | FullInversionClear - type ('a, 'b) gen_universe_decl = { univdecl_instance : 'a; (* Declared universes *) univdecl_extensible_instance : bool; (* Can new universes be added *) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 2743a8a2f..ae84eaa93 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -969,7 +969,7 @@ let functional_inversion kn hid fconst f_correct : Tacmach.tactic = Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]); thin [hid]; Proofview.V82.of_tactic (Simple.intro hid); - Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid)); + Proofview.V82.of_tactic (Inv.inv Inv.FullInversion None (NamedHyp hid)); (fun g -> let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in tclMAP (revert_graph kn pre_tac) (hid::new_ids) g diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 6637de745..434feba95 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -25,7 +25,7 @@ val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eva val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry val uconstr : constr_expr Gram.entry val quantified_hypothesis : quantified_hypothesis Gram.entry -val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry +val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry val int_or_var : int or_var Gram.entry val simple_tactic : raw_tactic_expr Gram.entry val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5951f2b11..aea00c240 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -84,7 +84,7 @@ type pp_tactic = { pptac_prods : grammar_terminals; } -val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t +val pr_goal_selector : toplevel:bool -> Vernacexpr.goal_selector -> Pp.t val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index 5347eda7d..59473a5e5 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -23,7 +23,7 @@ val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_typ val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type val wit_destruction_arg : - (constr_expr with_bindings Tacexpr.destruction_arg, - glob_constr_and_expr with_bindings Tacexpr.destruction_arg, - delayed_open_constr_with_bindings Tacexpr.destruction_arg) genarg_type + (constr_expr with_bindings Tactics.destruction_arg, + glob_constr_and_expr with_bindings Tactics.destruction_arg, + delayed_open_constr_with_bindings Tactics.destruction_arg) genarg_type diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 8b0c44041..3baa475ab 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -40,25 +40,29 @@ type goal_selector = Vernacexpr.goal_selector = | SelectList of (int * int) list | SelectId of Id.t | SelectAll +[@@ocaml.deprecated "Use Vernacexpr.goal_selector"] -type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg = +type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of lident | ElimOnAnonHyp of int +[@@ocaml.deprecated "Use Tactics.core_destruction_arg"] type 'a destruction_arg = - clear_flag * 'a core_destruction_arg + clear_flag * 'a Tactics.core_destruction_arg +[@@ocaml.deprecated "Use Tactics.destruction_arg"] -type inversion_kind = Misctypes.inversion_kind = +type inversion_kind = Inv.inversion_kind = | SimpleInversion | FullInversion | FullInversionClear +[@@ocaml.deprecated "Use Tactics.inversion_kind"] type ('c,'d,'id) inversion_strength = | NonDepInversion of - inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option | DepInversion of - inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option | InversionUsing of 'c * 'id list type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b @@ -69,7 +73,7 @@ type 'id message_token = | MsgIdent of 'id type ('dconstr,'id) induction_clause = - 'dconstr with_bindings destruction_arg * + 'dconstr with_bindings Tactics.destruction_arg * (intro_pattern_naming_expr CAst.t option (* eqn:... *) * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *) * 'id clause_expr option (* in ... *) @@ -265,7 +269,7 @@ and 'a gen_tactic_expr = ('p,'a gen_tactic_expr) match_rule list | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located - | TacSelect of goal_selector * 'a gen_tactic_expr + | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr (* For ML extensions *) | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located (* For syntax extensions *) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 8b0c44041..3baa475ab 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -40,25 +40,29 @@ type goal_selector = Vernacexpr.goal_selector = | SelectList of (int * int) list | SelectId of Id.t | SelectAll +[@@ocaml.deprecated "Use Vernacexpr.goal_selector"] -type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg = +type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of lident | ElimOnAnonHyp of int +[@@ocaml.deprecated "Use Tactics.core_destruction_arg"] type 'a destruction_arg = - clear_flag * 'a core_destruction_arg + clear_flag * 'a Tactics.core_destruction_arg +[@@ocaml.deprecated "Use Tactics.destruction_arg"] -type inversion_kind = Misctypes.inversion_kind = +type inversion_kind = Inv.inversion_kind = | SimpleInversion | FullInversion | FullInversionClear +[@@ocaml.deprecated "Use Tactics.inversion_kind"] type ('c,'d,'id) inversion_strength = | NonDepInversion of - inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option | DepInversion of - inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option | InversionUsing of 'c * 'id list type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b @@ -69,7 +73,7 @@ type 'id message_token = | MsgIdent of 'id type ('dconstr,'id) induction_clause = - 'dconstr with_bindings destruction_arg * + 'dconstr with_bindings Tactics.destruction_arg * (intro_pattern_naming_expr CAst.t option (* eqn:... *) * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *) * 'id clause_expr option (* in ... *) @@ -265,7 +269,7 @@ and 'a gen_tactic_expr = ('p,'a gen_tactic_expr) match_rule list | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located - | TacSelect of goal_selector * 'a gen_tactic_expr + | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr (* For ML extensions *) | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located (* For syntax extensions *) diff --git a/tactics/equality.mli b/tactics/equality.mli index c0be917a0..ccf454c3e 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -80,20 +80,20 @@ val discrConcl : unit Proofview.tactic val discrHyp : Id.t -> unit Proofview.tactic val discrEverywhere : evars_flag -> unit Proofview.tactic val discr_tac : evars_flag -> - constr with_bindings destruction_arg option -> unit Proofview.tactic + constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic (* Below, if flag is [None], it takes the value from the dynamic value of the option *) val inj : inj_flags option -> intro_patterns option -> evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic val injClause : inj_flags option -> intro_patterns option -> evars_flag -> - constr with_bindings destruction_arg option -> unit Proofview.tactic + constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic val injHyp : inj_flags option -> clear_flag -> Id.t -> unit Proofview.tactic val injConcl : inj_flags option -> unit Proofview.tactic val simpleInjClause : inj_flags option -> evars_flag -> - constr with_bindings destruction_arg option -> unit Proofview.tactic + constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic -val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic +val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic +val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr) diff --git a/tactics/inv.ml b/tactics/inv.ml index 067fc8941..d76c9a697 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -64,6 +64,11 @@ let var_occurs_in_pf gl id = type inversion_status = Dep of constr option | NoDep +type inversion_kind = + | SimpleInversion + | FullInversion + | FullInversionClear + let compute_eqn env sigma n i ai = (mkRel (n-i),get_type_of env sigma (mkRel (n-i))) diff --git a/tactics/inv.mli b/tactics/inv.mli index c63d57af5..9d4ffdd7b 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -15,6 +15,11 @@ open Tactypes type inversion_status = Dep of constr option | NoDep +type inversion_kind = + | SimpleInversion + | FullInversion + | FullInversionClear + val inv_clause : inversion_kind -> or_and_intro_pattern option -> Id.t list -> quantified_hypothesis -> unit Proofview.tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0d9f3d821..d0ec3358a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1159,6 +1159,13 @@ let tactic_infer_flags with_evar = { Pretyping.fail_evar = not with_evar; Pretyping.expand_evars = true } +type 'a core_destruction_arg = + | ElimOnConstr of 'a + | ElimOnIdent of lident + | ElimOnAnonHyp of int + +type 'a destruction_arg = + clear_flag * 'a core_destruction_arg let onOpenInductionArg env sigma tac = function | clear_flag,ElimOnConstr f -> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 079baa3ef..7809dbf48 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -95,6 +95,14 @@ val try_intros_until : (** Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) +type 'a core_destruction_arg = + | ElimOnConstr of 'a + | ElimOnIdent of lident + | ElimOnAnonHyp of int + +type 'a destruction_arg = + clear_flag * 'a core_destruction_arg + val onInductionArg : (clear_flag -> constr with_bindings -> unit Proofview.tactic) -> constr with_bindings destruction_arg -> unit Proofview.tactic |