diff options
90 files changed, 975 insertions, 618 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b39e74ffee..8fd5eb3972 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -640,9 +640,6 @@ library:ci-fiat-crypto: - library:ci-coqprime - plugin:ci-rewriter -library:ci-fiat-crypto-legacy: - extends: .ci-template-flambda - library:ci-flocq: extends: .ci-template diff --git a/Makefile.ci b/Makefile.ci index 10c3b027c3..f14203fa4a 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -25,7 +25,6 @@ CI_TARGETS= \ ci-equations \ ci-fcsl-pcm \ ci-fiat-crypto \ - ci-fiat-crypto-legacy \ ci-fiat_parsers \ ci-flocq \ ci-geocoq \ diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 608cc127a0..60c266699c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -165,13 +165,6 @@ : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## -# fiat_crypto_legacy -######################################################################## -: "${fiat_crypto_legacy_CI_REF:=sp2019latest}" -: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" -: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}" - -######################################################################## # coq_dpdgraph ######################################################################## : "${coq_dpdgraph_CI_REF:=coq-master}" diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh deleted file mode 100755 index 9ce5da9f50..0000000000 --- a/dev/ci/ci-fiat-crypto-legacy.sh +++ /dev/null @@ -1,14 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -FORCE_GIT=1 -git_download fiat_crypto_legacy - -fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite-hardcoded old-pipeline-lite-hardcoded lite-display-hardcoded" -fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem-hardcoded old-pipeline-nobigmem-hardcoded nonautogenerated-specific nonautogenerated-specific-display" - -( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \ - ./etc/ci/remove_autogenerated.sh && \ - make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index f08a08531f..c8ea59f08a 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -91,7 +91,6 @@ let projects = { cross_crypto = callPackage ./cross_crypto.nix {}; Elpi = callPackage ./Elpi.nix {}; fiat_crypto = callPackage ./fiat_crypto.nix {}; - fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {}; flocq = callPackage ./flocq.nix {}; formal-topology = callPackage ./formal-topology.nix {}; GeoCoq = callPackage ./GeoCoq.nix {}; diff --git a/dev/ci/nix/fiat_crypto_legacy.nix b/dev/ci/nix/fiat_crypto_legacy.nix deleted file mode 100644 index 3248665579..0000000000 --- a/dev/ci/nix/fiat_crypto_legacy.nix +++ /dev/null @@ -1,6 +0,0 @@ -{}: - -{ - configure = "./etc/ci/remove_autogenerated.sh"; - make = "make print-old-pipeline-lite old-pipeline-lite lite-display"; -} diff --git a/dev/ci/user-overlays/11235-non-maximal-implicit.sh b/dev/ci/user-overlays/11235-non-maximal-implicit.sh new file mode 100644 index 0000000000..fd63980036 --- /dev/null +++ b/dev/ci/user-overlays/11235-non-maximal-implicit.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "11235" ] || [ "$CI_BRANCH" = "non-maximal-implicit" ]; then + + quickchick_CI_REF=non_maximal_implicit + quickchick_CI_GITURL=https://github.com/SimonBoulier/QuickChick + + elpi_CI_REF=non_maximal_implicit + elpi_CI_GITURL=https://github.com/SimonBoulier/coq-elpi + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 3bc92e6aee..cb6e695865 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -17,6 +17,11 @@ Printers: Constrextern.extern_constr which were taking a boolean argument for the goal style now take instead a label. +Implicit arguments: + +- The type `Impargs.implicit_kind` was removed in favor of + `Glob_term.binding_kind`. + ## Changes between Coq 8.10 and Coq 8.11 ### ML API diff --git a/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst b/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst new file mode 100644 index 0000000000..57bce7e4f6 --- /dev/null +++ b/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst @@ -0,0 +1,7 @@ +- **Changed:** + Warn when manual implicit arguments are used in unexpected positions + of a term (e.g. in `Check id (forall {x}, x)`) or when a implicit + argument name is shadowed (e.g. in `Check fun f : forall {x:nat} + {x}, nat => f`) + (`#10202 <https://github.com/coq/coq/pull/10202>`_, + by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst new file mode 100644 index 0000000000..d8ff1fec31 --- /dev/null +++ b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst @@ -0,0 +1,6 @@ +- **Added:** + Syntax for non maximal implicit arguments in definitions and terms using + square brackets. The syntax is ``[x : A]``, ``[x]``, ```[A]`` + to be consistent with the command :cmd:`Arguments (implicits)`. + (`#11235 <https://github.com/coq/coq/pull/11235>`_, + by SimonBoulier). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 510e271951..7b4b652a6a 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1570,11 +1570,26 @@ inserted. In the second case, the function is considered to be implicitly applied to the implicit arguments it is waiting for: one says that the implicit argument is maximally inserted. -Each implicit argument can be declared to have to be inserted maximally or non -maximally. This can be governed argument per argument by the command -:cmd:`Arguments (implicits)` or globally by the :flag:`Maximal Implicit Insertion` flag. +Each implicit argument can be declared to be inserted maximally or non +maximally. In Coq, maximally-inserted implicit arguments are written between curly braces +"{ }" and non-maximally-inserted implicit arguments are written in square brackets "[ ]". -.. seealso:: :ref:`displaying-implicit-args`. +.. seealso:: :flag:`Maximal Implicit Insertion` + +Trailing Implicit Arguments ++++++++++++++++++++++++++++ + +An implicit argument is considered trailing when all following arguments are declared +implicit. Trailing implicit arguments cannot be declared non maximally inserted, +otherwise they would never be inserted. + +.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. + + For instance: + + .. coqtop:: all fail + + Fail Definition double [n] := n + n. Casual use of implicit arguments @@ -1608,7 +1623,7 @@ Implicit Argument Binders In the first setting, one wants to explicitly give the implicit arguments of a declared object as part of its definition. To do this, one has to surround the bindings of implicit arguments by curly -braces: +braces or square braces: .. coqtop:: all @@ -1624,6 +1639,17 @@ absent in every situation but still be able to specify it if needed: Goal forall A, compose id id = id (A:=A). +For non maximally inserted implicit arguments, use square brackets: + +.. coqtop:: all + + Fixpoint map [A B : Type] (f : A -> B) (l : list A) : list B := + match l with + | nil => nil + | cons a t => cons (f a) (map f t) + end. + + Print Implicit map. The syntax is supported in all top-level definitions: :cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype @@ -1643,6 +1669,44 @@ For example: One can always specify the parameter if it is not uniform using the usual implicit arguments disambiguation syntax. +The syntax is also supported in internal binders. For instance, in the +following kinds of expressions, the type of each declaration present +in :token:`binders` can be bracketed to mark the declaration as +implicit: +:n:`fun (@ident:forall @binders, @type) => @term`, +:n:`forall (@ident:forall @binders, @type), @type`, +:n:`let @ident @binders := @term in @term`, +:n:`fix @ident @binders := @term in @term` and +:n:`cofix @ident @binders := @term in @term`. +Here is an example: + +.. coqtop:: all + + Axiom Ax : + forall (f:forall {A} (a:A), A * A), + let g {A} (x y:A) := (x,y) in + f 0 = g 0 0. + +.. warn:: Ignoring implicit binder declaration in unexpected position + + This is triggered when setting an argument implicit in an + expression which does not correspond to the type of an assumption + or to the body of a definition. Here is an example: + + .. coqtop:: all warn + + Definition f := forall {y}, y = 0. + +.. warn:: Making shadowed name of implicit argument accessible by position + + This is triggered when two variables of same name are set implicit + in the same block of binders, in which case the first occurrence is + considered to be unnamed. Here is an example: + + .. coqtop:: all warn + + Check let g {x:nat} (H:x=x) {x} (H:x=x) := x in 0. + Declaring Implicit Arguments ++++++++++++++++++++++++++++ @@ -1728,14 +1792,6 @@ Declaring Implicit Arguments To know which are the implicit arguments of an object, use the command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). -.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. - - For instance in - - .. coqtop:: all fail - - Arguments prod _ [_]. - Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1811,7 +1867,7 @@ appear strictly in the body of the type, they are implicit. Mode for automatic declaration of implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +++++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Implicit Arguments @@ -1823,7 +1879,7 @@ Mode for automatic declaration of implicit arguments .. _controlling-strict-implicit-args: Controlling strict implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++ .. flag:: Strict Implicit @@ -1842,7 +1898,7 @@ Controlling strict implicit arguments .. _controlling-contextual-implicit-args: Controlling contextual implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++++++ .. flag:: Contextual Implicit @@ -1853,7 +1909,7 @@ Controlling contextual implicit arguments .. _controlling-rev-pattern-implicit-args: Controlling reversible-pattern implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Reversible Pattern Implicit @@ -1864,7 +1920,7 @@ Controlling reversible-pattern implicit arguments .. _controlling-insertion-implicit-args: Controlling the insertion of implicit arguments not followed by explicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Maximal Implicit Insertion @@ -1873,6 +1929,28 @@ Controlling the insertion of implicit arguments not followed by explicit argumen function is partially applied and the next argument of the function is an implicit one. +Combining manual declaration and automatic declaration +++++++++++++++++++++++++++++++++++++++++++++++++++++++ + +When some arguments are manually specified implicit with binders in a definition +and the automatic declaration mode in on, the manual implicit arguments are added to the +automatically declared ones. + +In that case, and when the flag :flag:`Maximal Implicit Insertion` is set to off, +some trailing implicit arguments can be inferred to be non maximally inserted. In +this case, they are converted to maximally inserted ones. + +.. example:: + + .. coqtop:: all + + Set Implicit Arguments. + Axiom eq0_le0 : forall (n : nat) (x : n = 0), n <= 0. + Print Implicit eq0_le0. + Axiom eq0_le0' : forall (n : nat) {x : n = 0}, n <= 0. + Print Implicit eq0_le0'. + + .. _explicit-applications: Explicit applications @@ -2136,8 +2214,10 @@ Implicit generalization ~~~~~~~~~~~~~~~~~~~~~~~ .. index:: `{ } +.. index:: `[ ] .. index:: `( ) .. index:: `{! } +.. index:: `[! ] .. index:: `(! ) Implicit generalization is an automatic elaboration of a statement @@ -2145,11 +2225,12 @@ with free variables into a closed statement where these variables are quantified explicitly. It is activated for a binder by prefixing a \`, and for terms by -surrounding it with \`{ } or \`( ). +surrounding it with \`{ }, or \`[ ] or \`( ). Terms surrounded by \`{ } introduce their free variables as maximally -inserted implicit arguments, and terms surrounded by \`( ) introduce -them as explicit arguments. +inserted implicit arguments, terms surrounded by \`[ ] introduce them as +non maximally inserted implicit arguments and terms surrounded by \`( ) +introduce them as explicit arguments. Generalizing binders always introduce their free variables as maximally inserted implicit arguments. The binder itself introduces diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index d591718b17..09090ce89a 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -283,8 +283,10 @@ Binders | ( {+ @name } : @term ) | ( @name {? : @term } := @term ) | %{ {+ @name } {? : @term } %} + | [ {+ @name } {? : @term } ] | `( {+, @typeclass_constraint } ) | `%{ {+, @typeclass_constraint } %} + | `[ {+, @typeclass_constraint } ] | ' @pattern0 | ( @name : @term %| @term ) typeclass_constraint ::= {? ! } @term diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index ff0b90dcff..e1b9c6b7cb 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -831,8 +831,9 @@ let rec print_symbol : type s tr r. formatter -> (s, tr, r) ty_symbol -> unit = fprintf ppf "LIST1 %a SEP %a%s" print_symbol1 s print_symbol1 t (if osep then " OPT_SEP" else "") | Sopt s -> fprintf ppf "OPT %a" print_symbol1 s - | Stoken p when L.tok_pattern_strings p <> ("", None) -> + | Stoken p -> begin match L.tok_pattern_strings p with + | "", Some s -> print_str ppf s | con, Some prm -> fprintf ppf "%s@ %a" con print_str prm | con, None -> fprintf ppf "%s" con end | Snterml (e, l) -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f4ae5bf676..2ceea58297 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -257,7 +257,7 @@ type intern_env = { tmp_scope: Notation_term.tmp_scope_name option; scopes: Notation_term.scope_name list; impls: internalization_env; - impl_binder_index: int option; + binder_block_names: (abstraction_kind option (* None = unknown *) * Id.Set.t) option; } (**********************************************************************) @@ -330,15 +330,18 @@ let exists_name na l = | _ -> false let build_impls ?loc n bk na acc = - match bk with - | Implicit -> + let impl_status max = let na = - if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end - else na in + if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end + else na in let impl = match na with - | Name id -> Some (ExplByName id,Manual,(true,true)) - | Anonymous -> Some (ExplByPos (n,None),Manual,(true,true)) in - impl :: acc + | Name id -> Some (ExplByName id,Manual,(max,true)) + | Anonymous -> Some (ExplByPos (n,None),Manual,(max,true)) in + impl + in + match bk with + | NonMaxImplicit -> impl_status false :: acc + | MaxImplicit -> impl_status true :: acc | Explicit -> None :: acc let impls_binder_list = @@ -373,6 +376,49 @@ let rec check_capture ty = let open CAst in function | [] -> () +(** Status of the internalizer wrt "Arguments" of names *) + +let restart_no_binders env = + { env with binder_block_names = None} + (* Not in relation with the "Arguments" of a name *) + +let restart_prod_binders env = + { env with binder_block_names = Some (Some AbsPi, Id.Set.empty) } + (* In a position binding a type to a name *) + +let restart_lambda_binders env = + { env with binder_block_names = Some (Some AbsLambda, Id.Set.empty) } + (* In a position binding a body to a name *) + +let switch_prod_binders env = + match env.binder_block_names with + | Some (o,ids) when o <> Some AbsLambda -> restart_prod_binders env + | _ -> restart_no_binders env + (* In a position switching to a type *) + +let switch_lambda_binders env = + match env.binder_block_names with + | Some (o,ids) when o <> Some AbsPi -> restart_lambda_binders env + | _ -> restart_no_binders env + (* In a position switching to a term *) + +let slide_binders env = + match env.binder_block_names with + | Some (o,ids) when o <> Some AbsPi -> restart_prod_binders env + | _ -> restart_no_binders env + (* In a position of cast *) + +let binder_status_fun = { + no = (fun x -> x); + restart_prod = on_snd restart_prod_binders; + restart_lambda = on_snd restart_lambda_binders; + switch_prod = on_snd switch_prod_binders; + switch_lambda = on_snd switch_lambda_binders; + slide = on_snd slide_binders; +} + +(**) + let locate_if_hole ?loc na c = match DAst.get c with | GHole (_,naming,arg) -> (try match na with @@ -397,7 +443,11 @@ let check_hidden_implicit_parameters ?loc id impls = strbrk "the type of a constructor shall use a different name.") let pure_push_name_env (id,implargs) env = - {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} + {env with + ids = Id.Set.add id env.ids; + impls = Id.Map.add id implargs env.impls; + binder_block_names = Option.map (fun (b,ids) -> (b,Id.Set.add id ids)) env.binder_block_names; + } let push_name_env ntnvars implargs env = let open CAst in @@ -421,13 +471,15 @@ let remember_binders_impargs env bl = let restore_binders_impargs env l = List.fold_right pure_push_name_env l env -let warn_unexpected_implicit_binder_declaration = +let warn_ignoring_unexpected_implicit_binder_declaration = CWarnings.create ~name:"unexpected-implicit-declaration" ~category:"syntax" - Pp.(fun () -> str "Unexpected implicit binder declaration.") + Pp.(fun () -> str "Ignoring implicit binder declaration in unexpected position.") let check_implicit_meaningful ?loc k env = - if k = Implicit && env.impl_binder_index = None then - warn_unexpected_implicit_binder_declaration ?loc () + if k <> Explicit && env.binder_block_names = None then + (warn_ignoring_unexpected_implicit_binder_declaration ?loc (); Explicit) + else + k let intern_generalized_binder intern_type ntnvars env {loc;v=na} b' t ty = @@ -441,10 +493,10 @@ let intern_generalized_binder intern_type ntnvars let env' = List.fold_left (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x)) env fvs in - check_implicit_meaningful ?loc b' env; + let b' = check_implicit_meaningful ?loc b' env in let bl = List.map CAst.(map (fun id -> - (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) + (Name id, MaxImplicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) fvs in let na = match na with @@ -463,7 +515,7 @@ let intern_generalized_binder intern_type ntnvars (make ?loc (na,b',ty')) :: List.rev bl) let intern_assumption intern ntnvars env nal bk ty = - let intern_type env = intern (set_type_scope env) in + let intern_type env = intern (restart_prod_binders (set_type_scope env)) in match bk with | Default k -> let ty = intern_type env ty in @@ -471,7 +523,7 @@ let intern_assumption intern ntnvars env nal bk ty = let impls = impls_type_list 1 ty in List.fold_left (fun (env, bl) ({loc;v=na} as locna) -> - check_implicit_meaningful ?loc k env; + let k = check_implicit_meaningful ?loc k env in (push_name_env ntnvars impls env locna, (make ?loc (na,k,locate_if_hole ?loc na ty))::bl)) (env, []) nal @@ -492,8 +544,8 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd") let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) = - let term = intern env def in - let ty = Option.map (intern env) ty in + let term = intern (reset_tmp_scope (restart_lambda_binders env)) def in + let ty = Option.map (intern (set_type_scope (restart_prod_binders env))) ty in let impls = impls_term_list 1 term in (push_name_env ntnvars impls env locna, (na,Explicit,term,ty)) @@ -713,6 +765,19 @@ let flatten_binders bl = | a -> [a] in List.flatten (List.map dispatch bl) +let rec adjust_env env = function + (* We need to adjust scopes, binder blocks ... to the env expected + at the recursive occurrence; We do an underapproximation... *) + | NProd (_,_,c) -> adjust_env (switch_prod_binders env) c + | NLambda (_,_,c) -> adjust_env (switch_lambda_binders env) c + | NLetIn (_,_,_,c) -> adjust_env env c + | NVar id when Id.equal id ldots_var -> env + | NCast (c,_) -> adjust_env env c + | NApp _ -> restart_no_binders env + | NVar _ | NRef _ | NHole _ | NCases _ | NLetTuple _ | NIf _ + | NRec _ | NSort _ | NInt _ | NFloat _ + | NList _ | NBinderList _ -> env (* to be safe, but restart should be ok *) + let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let (terms,termlists,binders,binderlists) = subst in (* when called while defining a notation, avoid capturing the private binders @@ -725,7 +790,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let rec aux_letin env = function | [],terminator,_ -> aux (terms,None,None) (renaming,env) terminator | AddPreBinderIter (y,binder)::rest,terminator,iter -> - let env,binders = intern_local_binder_aux intern ntnvars (env,[]) binder in + let env,binders = intern_local_binder_aux intern ntnvars (adjust_env env iter,[]) binder in let binder,extra = flatten_generalized_binders_if_any y binders in aux (terms,Some (y,binder),Some (extra@rest,terminator,iter)) (renaming,env) iter | AddBinderIter (y,binder)::rest,terminator,iter -> @@ -733,7 +798,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = | AddTermIter nterms::rest,terminator,iter -> aux (nterms,None,Some (rest,terminator,iter)) (renaming,env) iter | AddLetIn (na,c,t)::rest,terminator,iter -> - let env,(na,_,c,t) = intern_letin_binder intern ntnvars env (na,c,t) in + let env,(na,_,c,t) = intern_letin_binder intern ntnvars (adjust_env env iter) (na,c,t) in DAst.make ?loc (GLetIn (na,c,t,aux_letin env (rest,terminator,iter))) in aux_letin env (Option.get iteropt) | NVar id -> subst_var subst' (renaming, env) id @@ -823,7 +888,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = DAst.make ?loc @@ GLambda (na,Explicit,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c')) | t -> glob_constr_of_notation_constr_with_binders ?loc - (traverse_binder intern_pat ntnvars subst avoid) (aux subst') subinfos t + (traverse_binder intern_pat ntnvars subst avoid) (aux subst') ~h:binder_status_fun subinfos t and subst_var (terms, binderopt, _terminopt) (renaming, env) id = (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) @@ -1144,7 +1209,7 @@ let interp_reference vars r = intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None) {ids = Id.Set.empty; unb = false ; tmp_scope = None; scopes = []; impls = empty_internalization_env; - impl_binder_index = None} + binder_block_names = None} Environ.empty_named_context_val (vars, Id.Map.empty) None [] r in r @@ -1892,6 +1957,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = with Not_found -> raise (InternalizationError (locid,UnboundFixName (false,iddef))) in + let env = restart_lambda_binders env in let idl_temp = Array.map (fun (id,recarg,bl,ty,_) -> let recarg = Option.map (function { CAst.v = v } -> match v with @@ -1934,6 +2000,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = with Not_found -> raise (InternalizationError (locid,UnboundFixName (true,iddef))) in + let env = restart_lambda_binders env in let idl_tmp = Array.map (fun ({ CAst.loc; v = id },bl,ty,_) -> let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in @@ -1957,18 +2024,18 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = Array.map (fun (_,_,bd) -> bd) idl) | CProdN ([],c2) -> anomaly (Pp.str "The AST is malformed, found prod without binders.") | CProdN (bl,c2) -> - let (env',bl) = List.fold_left intern_local_binder (env,[]) bl in + let (env',bl) = List.fold_left intern_local_binder (switch_prod_binders env,[]) bl in expand_binders ?loc mkGProd bl (intern_type env' c2) | CLambdaN ([],c2) -> anomaly (Pp.str "The AST is malformed, found lambda without binders.") | CLambdaN (bl,c2) -> - let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope env,[]) bl in + let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope (switch_lambda_binders env),[]) bl in expand_binders ?loc mkGLambda bl (intern env' c2) | CLetIn (na,c1,t,c2) -> - let inc1 = intern_restart_implicit (reset_tmp_scope env) c1 in - let int = Option.map (intern_type_restart_implicit env) t in + let inc1 = intern_restart_binders (reset_tmp_scope env) c1 in + let int = Option.map (intern_type_restart_binders env) t in DAst.make ?loc @@ GLetIn (na.CAst.v, inc1, int, - intern_restart_implicit (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2) + intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2) | CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a -> let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p))) @@ -2009,7 +2076,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in let x, impl, scopes, l = find_appl_head_data c in (x,impl,scopes,l), args - | _ -> assert (Option.is_empty isproj); (intern env f,[],[],[]), args in + | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in apply_impargs c env impargs args_scopes (merge_impargs l args) loc @@ -2053,7 +2120,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = tms ([],Id.Set.empty,Id.Map.empty,[]) in let env' = Id.Set.fold (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var)) - (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in + (Id.Set.union ex_ids as_in_vars) + (reset_hidden_inductive_implicit_test (restart_lambda_binders env)) in (* PatVars before a real pattern do not need to be matched *) let stripped_match_from_in = let rec aux = function @@ -2063,7 +2131,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = in aux match_from_in in let rtnpo = Option.map (replace_vars_constr_expr aliases) rtnpo in let rtnpo = match stripped_match_from_in with - | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *) + | [] -> Option.map (intern_type (slide_binders env')) rtnpo (* Only PatVar in "in" clauses *) | l -> (* Build a return predicate by expansion of the patterns of the "in" clause *) let thevars, thepats = List.split l in @@ -2071,7 +2139,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let sub_tms = List.map (fun id -> (DAst.make @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in let main_sub_eqn = CAst.make @@ ([],thepats, (* "|p1,..,pn" *) - Option.cata (intern_type env') + Option.cata (intern_type_no_implicit env') (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,IntroAnonymous,None)) rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in let catch_all_sub_eqn = @@ -2090,7 +2158,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let p' = Option.map (fun u -> let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env') (CAst.make na') in - intern_type env'' u) po in + intern_type (slide_binders env'') u) po in DAst.make ?loc @@ GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b', intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) @@ -2100,7 +2168,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let p' = Option.map (fun p -> let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env) (CAst.make na') in - intern_type env'' p) po in + intern_type (slide_binders env'') p) po in DAst.make ?loc @@ GIf (c', (na', p'), intern env b1, intern env b2) | CHole (k, naming, solve) -> @@ -2160,18 +2228,20 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = GSort s | CCast (c1, c2) -> DAst.make ?loc @@ - GCast (intern env c1, map_cast_type (intern_type env) c2) + GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2) ) and intern_type env = intern (set_type_scope env) - and intern_no_implicit env = intern {env with impl_binder_index = None} + and intern_type_no_implicit env = intern (restart_no_binders (set_type_scope env)) - and intern_restart_implicit env = intern {env with impl_binder_index = Some 0} + and intern_no_implicit env = intern (restart_no_binders env) - and intern_type_restart_implicit env = intern {(set_type_scope env) with impl_binder_index = Some 0} + and intern_restart_binders env = intern (restart_lambda_binders env) + + and intern_type_restart_binders env = intern (restart_prod_binders (set_type_scope env)) and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list = - intern_local_binder_aux intern_restart_implicit ntnvars env bind + intern_local_binder_aux intern ntnvars env bind (* Expands a multiple pattern into a disjunction of multiple patterns *) and intern_multiple_pattern env n pl = @@ -2198,7 +2268,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in List.map (fun (asubst,pl) -> let rhs = replace_vars_constr_expr asubst rhs in - let rhs' = intern {env with ids = env_ids} rhs in + let rhs' = intern_no_implicit {env with ids = env_ids} rhs in CAst.make ?loc (eqn_ids,pl,rhs')) pll and intern_case_item env forbidden_names_for_gen (tm,na,t) = @@ -2336,7 +2406,12 @@ let extract_ids env = let scope_of_type_kind sigma = function | IsType -> Notation.current_type_scope_name () | OfType typ -> compute_type_scope sigma typ - | WithoutTypeConstraint -> None + | WithoutTypeConstraint | UnknownIfTermOrType -> None + +let allowed_binder_kind_of_type_kind = function + | IsType -> Some AbsPi + | OfType _ | WithoutTypeConstraint -> Some AbsLambda + | UnknownIfTermOrType -> None let empty_ltac_sign = { ltac_vars = Id.Set.empty; @@ -2348,9 +2423,10 @@ let intern_gen kind env sigma ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) c = let tmp_scope = scope_of_type_kind sigma kind in + let k = allowed_binder_kind_of_type_kind kind in internalize env {ids = extract_ids env; unb = false; tmp_scope = tmp_scope; scopes = []; - impls; impl_binder_index = Some 0} + impls; binder_block_names = Some (k,Id.Map.domain impls)} pattern_mode (ltacvars, Id.Map.empty) c let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c @@ -2372,8 +2448,8 @@ let interp_gen kind env sigma ?(impls=empty_internalization_env) c = let c = intern_gen kind ~impls env sigma c in understand ~expected_type:kind env sigma c -let interp_constr env sigma ?(impls=empty_internalization_env) c = - interp_gen WithoutTypeConstraint env sigma c +let interp_constr ?(expected_type=WithoutTypeConstraint) env sigma ?(impls=empty_internalization_env) c = + interp_gen expected_type env sigma c let interp_type env sigma ?(impls=empty_internalization_env) c = interp_gen IsType env sigma ~impls c @@ -2383,8 +2459,8 @@ let interp_casted_constr env sigma ?(impls=empty_internalization_env) c typ = (* Not all evars expected to be resolved *) -let interp_open_constr env sigma c = - understand_tcc env sigma (intern_constr env sigma c) +let interp_open_constr ?(expected_type=WithoutTypeConstraint) env sigma c = + understand_tcc env sigma (intern_gen expected_type env sigma c) (* Not all evars expected to be resolved and computation of implicit args *) @@ -2432,8 +2508,10 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c = let tmp_scope = scope_of_type_kind sigma kind in let impls = empty_internalization_env in + let k = allowed_binder_kind_of_type_kind kind in internalize env - {ids; unb = false; tmp_scope; scopes = []; impls; impl_binder_index = Some 0} + {ids; unb = false; tmp_scope; scopes = []; impls; + binder_block_names = Some (k,Id.Set.empty)} pattern_mode (ltacvars, vl) c let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = @@ -2442,7 +2520,7 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in let c = internalize env - {ids; unb = false; tmp_scope = None; scopes = []; impls; impl_binder_index = None} + {ids; unb = false; tmp_scope = None; scopes = []; impls; binder_block_names = None} false (empty_ltac_sign, vl) a in (* Splits variables into those that are binding, bound, or both *) (* Translate and check that [c] has all its free variables bound in [vars] *) @@ -2473,13 +2551,17 @@ let my_intern_constr env lvar acc c = let intern_context env impl_env binders = try let lvar = (empty_ltac_sign, Id.Map.empty) in + let ids = + (* We assume all ids around are parts of the prefix of the current + context being interpreted *) + extract_ids env in let lenv, bl = List.fold_left (fun (lenv, bl) b -> let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in (env, bl)) - ({ids = extract_ids env; unb = false; + ({ids; unb = false; tmp_scope = None; scopes = []; impls = impl_env; - impl_binder_index = Some 0}, []) binders in + binder_block_names = Some (Some AbsPi,ids)}, []) binders in (lenv.impls, List.map glob_local_binder_of_extended bl) with InternalizationError (loc,e) -> user_err ?loc ~hdr:"internalize" (explain_internalization_error e) @@ -2500,8 +2582,10 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = let r = Retyping.relevance_of_type env sigma t in let d = LocalAssum (make_annot na r,t) in let impls = - if k == Implicit then CAst.make (Some (na,true)) :: impls - else CAst.make None :: impls + match k with + | NonMaxImplicit -> CAst.make (Some (na,false)) :: impls + | MaxImplicit -> CAst.make (Some (na,true)) :: impls + | Explicit -> CAst.make None :: impls in (push_rel d env, sigma, d::params, succ n, impls) | Some b -> diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 8cce7cd9af..670563f02f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -97,7 +97,7 @@ val intern_context : env -> internalization_env -> local_binder_expr list -> int (** Main interpretation functions, using type class inference, expecting evars and pending problems to be all resolved *) -val interp_constr : env -> evar_map -> ?impls:internalization_env -> +val interp_constr : ?expected_type:typing_constraint -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> constr Evd.in_evar_universe_context val interp_casted_constr : env -> evar_map -> ?impls:internalization_env -> @@ -109,7 +109,7 @@ val interp_type : env -> evar_map -> ?impls:internalization_env -> (** Main interpretation function expecting all postponed problems to be resolved, but possibly leaving evars. *) -val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr +val interp_open_constr : ?expected_type:typing_constraint -> env -> evar_map -> constr_expr -> evar_map * constr (** Accepting unresolved evars *) diff --git a/interp/impargs.ml b/interp/impargs.ml index e2c732809a..9b50d9ca71 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -14,6 +14,7 @@ open Util open Names open Constr open Globnames +open Glob_term open Declarations open Lib open Libobject @@ -80,10 +81,24 @@ let with_implicit_protection f x = let () = implicit_args := oflags in iraise reraise -let set_maximality imps b = +type on_trailing_implicit = Error | Info | Silent + +let msg_trailing_implicit (fail : on_trailing_implicit) id = + let str1 = "Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, " in + match fail with + | Error -> + user_err (strbrk (str1 ^ "so it can't be declared non maximal. Please use { } instead of [ ].")) + | Info -> + Flags.if_verbose Feedback.msg_info (strbrk (str1 ^ "so it has been declared maximally inserted.")) + | Silent -> () + +let set_maximality fail id imps b = (* Force maximal insertion on ending implicits (compatibility) *) - let is_set x = match x with None -> false | _ -> true in - b || List.for_all is_set imps + b || ( + let is_set x = match x with None -> false | _ -> true in + let b' = List.for_all is_set imps in + if b' then msg_trailing_implicit fail id; + b') (*s Computation of implicit arguments *) @@ -302,6 +317,11 @@ let is_status_implicit = function let name_of_pos k = Id.of_string ("arg_" ^ string_of_int k) +let binding_kind_of_status = function + | Some (_, _, (false, _)) -> NonMaxImplicit + | Some (_, _, (true, _)) -> MaxImplicit + | None -> Explicit + let name_of_implicit = function | None -> anomaly (Pp.str "Not an implicit argument.") | Some (ExplByName id,_,_) -> id @@ -340,19 +360,19 @@ let rec prepare_implicits f = function | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.") | (Name id, Some imp)::imps -> let imps' = prepare_implicits f imps in - Some (ExplByName id,imp,(set_maximality imps' f.maximal,true)) :: imps' + Some (ExplByName id,imp,(set_maximality Silent id imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits f imps -let set_manual_implicits flags enriching autoimps l = +let set_manual_implicits silent flags enriching autoimps l = (* Compare with automatic implicits to recover printing data and names *) 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.CAst.v with | (Name id,_), Some (_,max) -> - Some (ExplByName id, Manual, (set_maximality imps' max, true)) + Some (ExplByName id, Manual, (set_maximality (if silent then Silent else Error) id imps' max, true)) | (Name id,Some exp), None when enriching -> - Some (ExplByName id, exp, (set_maximality imps' flags.maximal, true)) + Some (ExplByName id, exp, (set_maximality (if silent then Silent else Info) id imps' flags.maximal, true)) | (Name _,_), None -> None | (Anonymous,_), Some (Name id,max) -> Some (ExplByName id,Manual,(max,true)) @@ -497,8 +517,9 @@ let impls_of_context ctx = let map decl = let id = NamedDecl.get_id decl in match Id.Map.get id !sec_implicits with - | Glob_term.Implicit -> Some (ExplByName id, Manual, (true, true)) - | Glob_term.Explicit -> None + | NonMaxImplicit -> Some (ExplByName id, Manual, (false, true)) + | MaxImplicit -> Some (ExplByName id, Manual, (true, true)) + | Explicit -> None in List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx) @@ -608,7 +629,7 @@ type manual_implicits = (Name.t * bool) option CAst.t 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 !implicit_args enriching autoimpls l + set_manual_implicits true !implicit_args enriching autoimpls l let check_inclusion l = (* Check strict inclusion *) @@ -636,7 +657,7 @@ let declare_manual_implicits local ref ?enriching l = let t = of_constr t in let enriching = Option.default flags.auto enriching in let autoimpls = compute_auto_implicits env sigma flags enriching t in - let l = [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] in + let l = [DefaultImpArgs, set_manual_implicits false flags enriching autoimpls l] in let req = if is_local local ref then ImplLocal else ImplInteractive(flags,ImplManual (List.length autoimpls)) @@ -647,22 +668,16 @@ let maybe_declare_manual_implicits local ref ?enriching l = declare_manual_implicits local ref ?enriching l -let msg_trailing_implicit id = - user_err (strbrk ("Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ].")) - -type implicit_kind = Implicit | MaximallyImplicit | NotImplicit - let compute_implicit_statuses autoimps l = let rec aux i = function - | _ :: autoimps, NotImplicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps) - | Name id :: autoimps, MaximallyImplicit :: manualimps -> + | _ :: autoimps, Explicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps) + | Name id :: autoimps, MaxImplicit :: manualimps -> Some (ExplByName id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps) - | Name id :: autoimps, Implicit :: manualimps -> + | Name id :: autoimps, NonMaxImplicit :: manualimps -> let imps' = aux (i+1) (autoimps, manualimps) in - let max = set_maximality imps' false in - if max then msg_trailing_implicit id; + let max = set_maximality Error id imps' false in Some (ExplByName id, Manual, (max, true)) :: imps' - | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ -> + | Anonymous :: _, (NonMaxImplicit | MaxImplicit) :: _ -> user_err ~hdr:"set_implicits" (strbrk ("Argument number " ^ string_of_int i ^ " (anonymous in original definition) cannot be declared implicit.")) | autoimps, [] -> List.map (fun _ -> None) autoimps @@ -684,7 +699,7 @@ let set_implicits local ref l = check_rigidity (is_rigid env sigma t); (* Sort by number of implicits, decreasing *) let is_implicit = function - | NotImplicit -> false + | Explicit -> false | _ -> true in let l = List.map (fun imps -> (imps,List.count is_implicit imps)) l in let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in diff --git a/interp/impargs.mli b/interp/impargs.mli index ef3c2496f4..65e7fd8aaf 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -77,6 +77,7 @@ type implicit_side_condition type implicits_list = implicit_side_condition * implicit_status list val is_status_implicit : implicit_status -> bool +val binding_kind_of_status : implicit_status -> Glob_term.binding_kind val is_inferable_implicit : bool -> int -> implicit_status -> bool val name_of_implicit : implicit_status -> Id.t val maximal_insertion_of : implicit_status -> bool @@ -113,12 +114,10 @@ val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> manual_implicits -> unit -type implicit_kind = Implicit | MaximallyImplicit | NotImplicit - (** [set_implicits local ref l] Manual declaration of implicit arguments. `l` is a list of possible sequences of implicit statuses. *) -val set_implicits : bool -> GlobRef.t -> implicit_kind list list -> unit +val set_implicits : bool -> GlobRef.t -> Glob_term.binding_kind list list -> unit val implicits_of_global : GlobRef.t -> implicits_list list diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 8b457ab37b..ffbb982ab7 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -203,8 +203,9 @@ let warn_ignoring_implicit_status = let implicits_of_glob_constr ?(with_products=true) l = let add_impl ?loc na bk l = match bk with - | Implicit -> CAst.make ?loc (Some (na,true)) :: l - | _ -> CAst.make ?loc None :: l + | NonMaxImplicit -> CAst.make ?loc (Some (na,false)) :: l + | MaxImplicit -> CAst.make ?loc (Some (na,true)) :: l + | Explicit -> CAst.make ?loc None :: l in let rec aux c = match DAst.get c with @@ -212,8 +213,9 @@ let implicits_of_glob_constr ?(with_products=true) l = if with_products then add_impl na bk (aux b) else let () = match bk with - | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc - | _ -> () + | NonMaxImplicit + | MaxImplicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc + | Explicit -> () in [] | GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b) | GLetIn (na, b, t, c) -> aux c diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 265ca58ed9..d1eb50d370 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -151,6 +151,24 @@ let rec subst_glob_vars l gc = DAst.map (function let ldots_var = Id.of_string ".." +type 'a binder_status_fun = { + no : 'a -> 'a; + restart_prod : 'a -> 'a; + restart_lambda : 'a -> 'a; + switch_prod : 'a -> 'a; + switch_lambda : 'a -> 'a; + slide : 'a -> 'a; +} + +let default_binder_status_fun = { + no = (fun x -> x); + restart_prod = (fun x -> x); + restart_lambda = (fun x -> x); + switch_prod = (fun x -> x); + switch_lambda = (fun x -> x); + slide = (fun x -> x); +} + let protect g e na = let e',disjpat,na = g e na in if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern."); @@ -163,10 +181,10 @@ let apply_cases_pattern_term ?loc (ids,disjpat) tm c = let apply_cases_pattern ?loc (ids_disjpat,id) c = apply_cases_pattern_term ?loc ids_disjpat (DAst.make ?loc (GVar id)) c -let glob_constr_of_notation_constr_with_binders ?loc g f e nc = +let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_status_fun) e nc = let lt x = DAst.make ?loc x in lt @@ match nc with | NVar id -> GVar id - | NApp (a,args) -> GApp (f e a, List.map (f e) args) + | NApp (a,args) -> let e = h.no e in GApp (f e a, List.map (f e) args) | NList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in @@ -180,15 +198,18 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in DAst.get (subst_glob_vars outerl it) | NLambda (na,ty,c) -> - let e',disjpat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) + let e = h.switch_lambda e in + let e',disjpat,na = g e na in GLambda (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) | NProd (na,ty,c) -> - let e',disjpat,na = g e na in GProd (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) + let e = h.switch_prod e in + let e',disjpat,na = g e na in GProd (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) | NLetIn (na,b,t,c) -> let e',disjpat,na = g e na in (match disjpat with - | None -> GLetIn (na,f e b,Option.map (f e) t,f e' c) + | None -> GLetIn (na,f (h.restart_lambda e) b,Option.map (f (h.restart_prod e)) t,f e' c) | Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c))) | NCases (sty,rtntypopt,tml,eqnl) -> + let e = h.no e in let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with | None -> e',None @@ -207,19 +228,22 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = List.map (fun patl -> CAst.make (idl,patl,f e rhs)) disjpatl) eqnl in GCases (sty,Option.map (f e') rtntypopt,tml',List.flatten eqnl') | NLetTuple (nal,(na,po),b,c) -> + let e = h.no e in let e',nal = List.fold_left_map (protect g) e nal in let e'',na = protect g e na in GLetTuple (nal,(na,Option.map (f e'') po),f e b,f e' c) | NIf (c,(na,po),b1,b2) -> + let e = h.no e in let e',na = protect g e na in GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2) | NRec (fk,idl,dll,tl,bl) -> + let e = h.no e in let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) -> let e,na = protect g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = Array.fold_left_map (to_id (protect g)) e idl in GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) - | NCast (c,k) -> GCast (f e c,map_cast_type (f e) k) + | NCast (c,k) -> GCast (f e c,map_cast_type (f (h.slide e)) k) | NSort x -> GSort x | NHole (x, naming, arg) -> GHole (x, naming, arg) | NRef x -> GRef (x,None) diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index f9de6b7d6b..c62dac013b 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -35,12 +35,21 @@ val notation_constr_of_glob_constr : notation_interp_env -> (** Re-interpret a notation as a [glob_constr], taking care of binders *) +type 'a binder_status_fun = { + no : 'a -> 'a; + restart_prod : 'a -> 'a; + restart_lambda : 'a -> 'a; + switch_prod : 'a -> 'a; + switch_lambda : 'a -> 'a; + slide : 'a -> 'a; +} + val apply_cases_pattern : ?loc:Loc.t -> (Id.t list * cases_pattern_disjunction) * Id.t -> glob_constr -> glob_constr val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t -> ('a -> Name.t -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t) -> - ('a -> notation_constr -> glob_constr) -> + ('a -> notation_constr -> glob_constr) -> ?h:'a binder_status_fun -> 'a -> notation_constr -> glob_constr val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_constr diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index af1e973261..dcc3a87b11 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -205,7 +205,7 @@ GRAMMAR EXTEND Gram | "{"; c = binder_constr ; "}" -> { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } | "`{"; c = operconstr LEVEL "200"; "}" -> - { CAst.make ~loc @@ CGeneralization (Implicit, None, c) } + { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) } | "`("; c = operconstr LEVEL "200"; ")" -> { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } ] ] ; @@ -431,17 +431,27 @@ GRAMMAR EXTEND Gram | "("; id = name; ":"; t = lconstr; ":="; c = lconstr; ")" -> { [CLocalDef (id,c,Some t)] } | "{"; id = name; "}" -> - { [CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } + { [CLocalAssum ([id],Default MaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } | "{"; id = name; idl = LIST1 name; ":"; c = lconstr; "}" -> - { [CLocalAssum (id::idl,Default Implicit,c)] } + { [CLocalAssum (id::idl,Default MaxImplicit,c)] } | "{"; id = name; ":"; c = lconstr; "}" -> - { [CLocalAssum ([id],Default Implicit,c)] } + { [CLocalAssum ([id],Default MaxImplicit,c)] } | "{"; id = name; idl = LIST1 name; "}" -> - { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } + { List.map (fun id -> CLocalAssum ([id],Default MaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } + | "["; id = name; "]" -> + { [CLocalAssum ([id],Default NonMaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } + | "["; id = name; idl = LIST1 name; ":"; c = lconstr; "]" -> + { [CLocalAssum (id::idl,Default NonMaxImplicit,c)] } + | "["; id = name; ":"; c = lconstr; "]" -> + { [CLocalAssum ([id],Default NonMaxImplicit,c)] } + | "["; id = name; idl = LIST1 name; "]" -> + { List.map (fun id -> CLocalAssum ([id],Default NonMaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Explicit, b), t)) tc } | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> - { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, b), t)) tc } + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (MaxImplicit, b), t)) tc } + | "`["; tc = LIST1 typeclass_constraint SEP "," ; "]" -> + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (NonMaxImplicit, b), t)) tc } | "'"; p = pattern LEVEL "0" -> { let (p, ty) = match p.CAst.v with diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 500f464ea7..fdc70ccaa8 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -492,7 +492,7 @@ let rec add_term state t= Not_found -> let b=next uf in let trm = constr_of_term t in - let typ = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr trm) in + let typ = Retyping.get_type_of state.env state.sigma (EConstr.of_constr trm) in let typ = canonize_name state.sigma typ in let new_node= match t with @@ -809,23 +809,23 @@ let new_state_var typ state = let complete_one_class state i= match (get_representative state.uf i).inductive_status with - Partial pac -> - let rec app t typ n = - if n<=0 then t else - let _,etyp,rest= destProd typ in - let id = new_state_var (EConstr.of_constr etyp) state in - app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in - let _c = Typing.unsafe_type_of state.env state.sigma - (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in - let _c = EConstr.Unsafe.to_constr _c in - let _args = - List.map (fun i -> constr_of_term (term state.uf i)) - pac.args in - let typ = Term.prod_applist _c (List.rev _args) in - let ct = app (term state.uf i) typ pac.arity in - state.uf.epsilons <- pac :: state.uf.epsilons; - ignore (add_term state ct) - | _ -> anomaly (Pp.str "wrong incomplete class.") + | Partial pac -> + let rec app t typ n = + if n<=0 then t else + let _,etyp,rest= destProd typ in + let id = new_state_var (EConstr.of_constr etyp) state in + app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in + let c = Retyping.get_type_of state.env state.sigma + (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in + let c = EConstr.Unsafe.to_constr c in + let args = + List.map (fun i -> constr_of_term (term state.uf i)) + pac.args in + let typ = Term.prod_applist c (List.rev args) in + let ct = app (term state.uf i) typ pac.arity in + state.uf.epsilons <- pac :: state.uf.epsilons; + ignore (add_term state ct) + | _ -> anomaly (Pp.str "wrong incomplete class.") let complete state = Int.Set.iter (complete_one_class state) state.pa_classes diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 556e6b48e6..8a650d9e7a 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -277,10 +277,12 @@ let refresh_type env evm ty = Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true (Some false) env evm ty -let refresh_universes ty k = +let type_and_refresh c k = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let evm = Tacmach.New.project gl in + (* XXX is get_type_of enough? *) + let evm, ty = Typing.type_of env evm c in let evm, ty = refresh_type env evm ty in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k ty) end @@ -289,7 +291,6 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c) let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> - let type_of t = Tacmach.New.pf_unsafe_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with Ax c -> exact_check (EConstr.of_constr c) @@ -297,17 +298,17 @@ let rec proof_tac p : unit Proofview.tactic = let c = EConstr.of_constr c in let l=constr_of_term p.p_lhs and r=constr_of_term p.p_rhs in - refresh_universes (type_of l) (fun typ -> + type_and_refresh l (fun typ -> app_global _sym_eq [|typ;r;l;c|] exact_check) | Refl t -> let lr = constr_of_term t in - refresh_universes (type_of lr) (fun typ -> + type_and_refresh lr (fun typ -> app_global _refl_equal [|typ;constr_of_term t|] exact_check) | Trans (p1,p2)-> let t1 = constr_of_term p1.p_lhs and t2 = constr_of_term p1.p_rhs and t3 = constr_of_term p2.p_rhs in - refresh_universes (type_of t2) (fun typ -> + type_and_refresh t2 (fun typ -> let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in Tacticals.New.tclTHENS prf [(proof_tac p1);(proof_tac p2)]) | Congr (p1,p2)-> @@ -315,9 +316,9 @@ let rec proof_tac p : unit Proofview.tactic = and tx1=constr_of_term p2.p_lhs and tf2=constr_of_term p1.p_rhs and tx2=constr_of_term p2.p_rhs in - refresh_universes (type_of tf1) (fun typf -> - refresh_universes (type_of tx1) (fun typx -> - refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx -> + type_and_refresh tf1 (fun typf -> + type_and_refresh tx1 (fun typx -> + type_and_refresh (mkApp (tf1,[|tx1|])) (fun typfx -> let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in let appx1 = mkLambda(make_annot (Name id) Sorts.Relevant,typf,mkApp(mkRel 1,[|tx1|])) in let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in @@ -341,8 +342,8 @@ let rec proof_tac p : unit Proofview.tactic = let tj=constr_of_term prf.p_rhs in let default=constr_of_term p.p_lhs in let special=mkRel (1+nargs-argind) in - refresh_universes (type_of ti) (fun intype -> - refresh_universes (type_of default) (fun outtype -> + type_and_refresh ti (fun intype -> + type_and_refresh default (fun outtype -> let sigma, proj = build_projection intype cstr special default gl in @@ -362,7 +363,7 @@ let refute_tac c t1 t2 p = let neweq= app_global _eq [|intype;tt1;tt2|] in Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] - in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k + in type_and_refresh tt1 k end let refine_exact_check c = @@ -382,7 +383,7 @@ let convert_to_goal_tac c t1 t2 p = let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) [proof_tac p; endt refine_exact_check] - in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k + in type_and_refresh tt2 k end let convert_to_hyp_tac c1 t1 c2 t2 p = @@ -401,7 +402,8 @@ let discriminate_tac cstru p = let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in let env = Proofview.Goal.env gl in let evm = Tacmach.New.project gl in - let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl lhs) in + let evm, intype = Typing.type_of env evm lhs in + let evm, intype = refresh_type env evm intype in let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in let neweq=app_global _eq [|intype;lhs;rhs|] in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 8946587a02..9d208e1c86 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -88,7 +88,7 @@ let gen_ground_tac flag taco ids bases = Proofview.Goal.enter begin fun gl -> let seq=empty_seq !ground_depth in let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in - let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in + let seq, sigma = extend_with_auto_hints (pf_env gl) sigma bases seq in tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq) end in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index e131cad7da..866b45e4df 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -100,25 +100,28 @@ let rec collect_quantified sigma seq= let dummy_bvid=Id.of_string "x" -let mk_open_instance env evmap id idc m t = - let var_id= - if id==dummy_id then dummy_bvid else - let typ=Typing.unsafe_type_of env evmap idc in +let mk_open_instance env sigma id idc m t = + let var_id = + (* XXX why physical equality? *) + if id == dummy_id then dummy_bvid else + let typ = Retyping.get_type_of env sigma idc in (* since we know we will get a product, reduction is not too expensive *) - let (nam,_,_)=destProd evmap (whd_all env evmap typ) in + let (nam,_,_) = destProd sigma (whd_all env sigma typ) in match nam.Context.binder_name with - Name id -> id - | Anonymous -> dummy_bvid in - let revt=substl (List.init m (fun i->mkRel (m-i))) t in - let rec aux n avoid env evmap decls = - if Int.equal n 0 then evmap, decls else - let nid=(fresh_id_in_env avoid var_id env) in - let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in + | Name id -> id + | Anonymous -> dummy_bvid + in + let revt = substl (List.init m (fun i->mkRel (m-i))) t in + let rec aux n avoid env sigma decls = + if Int.equal n 0 then sigma, decls else + let nid = fresh_id_in_env avoid var_id env in + let (sigma, (c, _)) = Evarutil.new_type_evar env sigma Evd.univ_flexible in let decl = LocalAssum (Context.make_annot (Name nid) Sorts.Relevant, c) in - aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in - let evmap, decls = aux m Id.Set.empty env evmap [] in - (evmap, decls, revt) + aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) sigma (decl::decls) + in + let sigma, decls = aux m Id.Set.empty env sigma [] in + (sigma, decls, revt) (* tactics *) diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 7d84ee6851..65af123d9c 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -204,28 +204,28 @@ let extend_with_ref_list env sigma l seq = open Hints let extend_with_auto_hints env sigma l seq = - let seqref=ref seq in - let f p_a_t = + let f (seq,sigma) p_a_t = match repr_hint p_a_t.code with - Res_pf (c,_) | Give_exact (c,_) - | Res_pf_THEN_trivial_fail (c,_) -> - let (c, _, _) = c in - (try - let (gr, _) = Termops.global_of_constr sigma c in - let typ=(Typing.unsafe_type_of env sigma c) in - seqref:=add_formula env sigma Hint gr typ !seqref - with Not_found->()) - | _-> () in - let g _ _ l = List.iter f l in - let h dbname= - let hdb= + | Res_pf (c,_) | Give_exact (c,_) + | Res_pf_THEN_trivial_fail (c,_) -> + let (c, _, _) = c in + (try + let (gr, _) = Termops.global_of_constr sigma c in + let sigma, typ = Typing.type_of env sigma c in + add_formula env sigma Hint gr typ seq, sigma + with Not_found -> seq, sigma) + | _ -> seq, sigma + in + let h acc dbname = + let hdb = try searchtable_map dbname with Not_found-> - user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database")) in - Hint_db.iter g hdb in - List.iter h l; - !seqref, sigma (*FIXME: forgetting about universes*) + user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database")) + in + Hint_db.fold (fun _ _ l acc -> List.fold_left f acc l) hdb acc + in + List.fold_left h (seq,sigma) l let print_cmap map= let print_entry c l s= diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 6db0a1119b..9749af1e66 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -475,7 +475,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = tclIDTAC in try - scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id] + scan_type [] (Typing.type_of_variable env hyp_id), [hyp_id] with TOREMOVE -> thin [hyp_id],[] @@ -525,7 +525,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = tclMAP (fun id -> Proofview.V82.of_tactic (introduction id)) dyn_infos.rec_hyps; observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) - let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in + let new_term_value_eq = pf_get_hyp_typ g' heq_id in (* compute the new value of the body *) let new_term_value = match EConstr.kind (project g') new_term_value_eq with @@ -536,22 +536,23 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = ); anomaly (Pp.str "cannot compute new term value.") in - let fun_body = - mkLambda(make_annot Anonymous Sorts.Relevant, - pf_unsafe_type_of g' term, - Termops.replace_term (project g') term (mkRel 1) dyn_infos.info - ) - in - let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in - let new_infos = - {dyn_infos with + let g', termtyp = tac_type_of g' term in + let fun_body = + mkLambda(make_annot Anonymous Sorts.Relevant, + termtyp, + Termops.replace_term (project g') term (mkRel 1) dyn_infos.info + ) + in + let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in + let new_infos = + {dyn_infos with info = new_body; eq_hyps = heq_id::dyn_infos.eq_hyps - } - in - clean_goal_with_heq ptes_infos continue_tac new_infos g' - )]) - ] + } + in + clean_goal_with_heq ptes_infos continue_tac new_infos g' + )]) + ] g @@ -633,7 +634,7 @@ let build_proof let dyn_infos = {dyn_info' with info = mkCase(ci,ct,t,cb)} in let g_nb_prod = nb_prod (project g) (pf_concl g) in - let type_of_term = pf_unsafe_type_of g t in + let g, type_of_term = tac_type_of g t in let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in @@ -849,7 +850,7 @@ let generalize_non_dep hyp g = (* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *) let hyps = [hyp] in let env = Global.env () in - let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in + let hyp_typ = pf_get_hyp_typ g hyp in let to_revert,_ = let open Context.Named.Declaration in Environ.fold_named_context_reverse (fun (clear,keep) decl -> @@ -1351,7 +1352,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = let rewrite = tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs ) in - let _,hrec_concl = decompose_prod (project gls) (pf_unsafe_type_of gls (mkVar hrec)) in + let _,hrec_concl = decompose_prod (project gls) (pf_get_hyp_typ gls hrec) in let f_app = Array.last (snd (destApp (project gls) hrec_concl)) in let f = (fst (destApp (project gls) f_app)) in let rec backtrack : tactic = @@ -1573,19 +1574,16 @@ let prove_principle_for_gen (List.rev_map (get_name %> Nameops.Name.get_id) (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) ); - (* observe_tac "" *) Proofview.V82.of_tactic (assert_by - (Name acc_rec_arg_id) - (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) - (Proofview.V82.tactic prove_rec_arg_acc) - ); -(* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); -(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) -(* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) - (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1))); -(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) + Proofview.V82.of_tactic + (assert_by + (Name acc_rec_arg_id) + (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) + (Proofview.V82.tactic prove_rec_arg_acc)); + (revert (List.rev (acc_rec_arg_id::args_ids))); + (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1))); h_intros (List.rev (acc_rec_arg_id::args_ids)); Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); - (* observe_tac "finish" *) (fun gl' -> + (fun gl' -> let body = let _,args = destApp (project gl') (pf_concl gl') in Array.last args diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 58efee1518..68661174ac 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -617,7 +617,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i let constructor_args g = List.fold_right (fun hid acc -> - let type_of_hid = pf_unsafe_type_of g (mkVar hid) in + let type_of_hid = pf_get_hyp_typ g hid in let sigma = project g in match EConstr.kind sigma type_of_hid with | Prod(_,_,t') -> @@ -953,7 +953,7 @@ let rec reflexivity_with_destruct_cases g = match sc with None -> tclIDTAC g | Some id -> - match EConstr.kind (project g) (pf_unsafe_type_of g (mkVar id)) with + match EConstr.kind (project g) (pf_get_hyp_typ g id) with | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 then Proofview.V82.of_tactic (Equality.discrHyp id) g @@ -993,7 +993,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti (* We get the constant and the principle corresponding to this lemma *) let f = funcs.(i) in let graph_principle = Reductionops.nf_zeta (pf_env g) (project g) (EConstr.of_constr schemes.(i)) in - let princ_type = pf_unsafe_type_of g graph_principle in + let g, princ_type = tac_type_of g graph_principle in let princ_infos = Tactics.compute_elim_sig (project g) princ_type in (* Then we get the number of argument of the function and compute a fresh name for each of them @@ -1210,7 +1210,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef in let _ = evd := sigma in let l_schemes = - List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma %> EConstr.Unsafe.to_constr) schemes + List.map (EConstr.of_constr %> Retyping.get_type_of env sigma %> EConstr.Unsafe.to_constr) schemes in let i = ref (-1) in let sorts = @@ -2051,7 +2051,7 @@ let build_case_scheme fa = let (sigma, scheme) = Indrec.build_case_analysis_scheme_default env sigma ind sf in - let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in + let scheme_type = EConstr.Unsafe.to_constr ((Retyping.get_type_of env sigma) (EConstr.of_constr scheme)) in let sorts = (fun (_,_,x) -> fst @@ UnivGen.fresh_sort_in_family x diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index e41b92d4dc..84f09c385f 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -514,8 +514,9 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret a pseudo value "v1 ... vn". The "value" of this branch is then simply [res] *) + (* XXX here and other [understand] calls drop the ctx *) let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in - let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in + let rt_typ = Retyping.get_type_of env (Evd.from_env env) rt_as_constr in let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in @@ -629,7 +630,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let v_res = build_entry_lc env sigma funnames avoid v in let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in - let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in + let v_type = Retyping.get_type_of env (Evd.from_env env) v_as_constr in let v_r = Sorts.Relevant in (* TODO relevance *) let new_env = match n with @@ -646,7 +647,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret build_entry_lc_from_case env sigma funnames make_discr el brl avoid | GIf(b,(na,e_option),lhs,rhs) -> let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in - let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in + let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> @@ -678,7 +679,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret nal in let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in - let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in + let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> @@ -723,7 +724,7 @@ and build_entry_lc_from_case env sigma funname make_discr let types = List.map (fun (case_arg,_) -> let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in - EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr) + EConstr.Unsafe.to_constr (Retyping.get_type_of env (Evd.from_env env) case_arg_as_constr) ) el in (****** The next works only if the match is not dependent ****) @@ -769,9 +770,7 @@ and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to let env_with_pat_ids = add_pat_variables sigma pat typ new_env in List.fold_right (fun id acc -> - let typ_of_id = - Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id) - in + let typ_of_id = Typing.type_of_variable env_with_pat_ids id in let raw_typ_of_id = Detyping.detype Detyping.Now false Id.Set.empty env_with_pat_ids (Evd.from_env env) typ_of_id @@ -832,7 +831,7 @@ and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to (fun id acc -> if Id.Set.mem id this_pat_ids then (Prod (Name id), - let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in + let typ_of_id = Typing.type_of_variable new_env id in let raw_typ_of_id = Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id in @@ -1166,7 +1165,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in let evd = Evd.from_ctx ctx in - let type_t' = Typing.unsafe_type_of env evd t' in + let type_t' = Retyping.get_type_of env evd t' in let t' = EConstr.Unsafe.to_constr t' in let type_t' = EConstr.Unsafe.to_constr type_t' in let new_env = Environ.push_rel (LocalDef (make_annot n Sorts.Relevant,t',type_t')) env in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a205c0744a..f28e98dcc2 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -64,12 +64,10 @@ let functional_induction with_clean c princl pat = | InSet -> finfo.rec_lemma | InType -> finfo.rect_lemma in - let princ = (* then we get the principle *) + let sigma, princ = (* then we get the principle *) match princ_option with | Some princ -> - let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ) in - Proofview.Unsafe.tclEVARS sigma >>= fun () -> - Proofview.tclUNIT princ + Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ) | None -> (*i If there is not default lemma defined then, we cross our finger and try to find a lemma named f_ind @@ -87,19 +85,18 @@ let functional_induction with_clean c princl pat = user_err (str "Cannot find induction principle for " ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') ) in - let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) princ_ref in - Proofview.Unsafe.tclEVARS sigma >>= fun () -> - Proofview.tclUNIT princ + Evd.fresh_global (pf_env gl) (project gl) princ_ref in - princ >>= fun princ -> - (* We need to refresh gl due to the updated evar_map in princ *) - Proofview.Goal.enter_one (fun gl -> - Proofview.tclUNIT (princ, Tactypes.NoBindings, pf_unsafe_type_of gl princ, args)) + let princt = Retyping.get_type_of (pf_env gl) sigma princ in + Proofview.Unsafe.tclEVARS sigma <*> + Proofview.tclUNIT (princ, Tactypes.NoBindings, princt, args) | _ -> CErrors.user_err (str "functional induction must be used with a function" ) end | Some ((princ,binding)) -> - Proofview.tclUNIT (princ, binding, pf_unsafe_type_of gl princ, args) + let sigma, princt = pf_type_of gl princ in + Proofview.Unsafe.tclEVARS sigma <*> + Proofview.tclUNIT (princ, binding, princt, args) ) >>= fun (princ, bindings, princ_type, args) -> Proofview.Goal.enter (fun gl -> let sigma = project gl in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index b55d8537d6..bce09d8fbd 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -526,3 +526,7 @@ let funind_purify f x = let e = CErrors.push e in Vernacstate.unfreeze_interp_state st; Exninfo.iraise e + +let tac_type_of g c = + let sigma, t = Tacmach.pf_type_of g c in + {g with Evd.sigma}, t diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 550f727951..bd8b34088b 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -119,3 +119,5 @@ type tcc_lemma_value = | Not_needed val funind_purify : ('a -> 'b) -> ('a -> 'b) + +val tac_type_of : Goal.goal Evd.sigma -> EConstr.constr -> Goal.goal Evd.sigma * EConstr.types diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d72319d078..332d058ce7 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -28,7 +28,7 @@ open Indfun_common *) let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl -> let sigma = project gl in - let typ = pf_unsafe_type_of gl (mkVar hid) in + let typ = pf_get_hyp_typ hid gl in match EConstr.kind sigma typ with | App(i,args) when isInd sigma i -> let ((kn',num) as ind'),u = destInd sigma i in @@ -77,7 +77,7 @@ let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl -> let functional_inversion kn hid fconst f_correct = Proofview.Goal.enter (fun gl -> let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps gl) Id.Set.empty in let sigma = project gl in - let type_of_h = pf_unsafe_type_of gl (mkVar hid) in + let type_of_h = pf_get_hyp_typ hid gl in match EConstr.kind sigma type_of_h with | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) -> let pre_tac,f_args,res = @@ -128,7 +128,7 @@ let invfun qhyp f = | None -> let tac_action hid gl = let sigma = project gl in - let hyp_typ = pf_unsafe_type_of gl (mkVar hid) in + let hyp_typ = pf_get_hyp_typ hid gl in match EConstr.kind sigma hyp_typ with | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) -> begin diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 66ed1961ba..f7f8004998 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -31,7 +31,6 @@ open Tactics open Nametab open Declare open Tacred -open Goal open Glob_term open Pretyping open Termops @@ -110,9 +109,10 @@ let pf_get_new_ids idl g = let next_ident_away_in_goal ids avoid = next_ident_away_in_goal ids (Id.Set.of_list avoid) -let compute_renamed_type gls c = +let compute_renamed_type gls id = rename_bound_vars_as_displayed (project gls) (*no avoid*) Id.Set.empty (*no rels*) [] - (pf_unsafe_type_of gls c) + (pf_get_hyp_typ gls id) + let h'_id = Id.of_string "h'" let teq_id = Id.of_string "teq" let ano_id = Id.of_string "anonymous" @@ -370,7 +370,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = Proofview.V82.of_tactic (clear to_intros); h_intros to_intros; (fun g' -> - let ty_teq = pf_unsafe_type_of g' (mkVar heq) in + let ty_teq = pf_get_hyp_typ g' heq in let teq_lhs,teq_rhs = let _,args = try destApp (project g') ty_teq with DestKO -> assert false in args.(1),args.(2) @@ -487,13 +487,13 @@ let rec prove_lt hyple g = in let h = List.find (fun id -> - match decompose_app sigma (pf_unsafe_type_of g (mkVar id)) with + match decompose_app sigma (pf_get_hyp_typ g id) with | _, t::_ -> EConstr.eq_constr sigma t varx | _ -> false ) hyple in let y = - List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (mkVar h))))) in + List.hd (List.tl (snd (decompose_app sigma (pf_get_hyp_typ g h)))) in observe_tclTHENLIST (fun _ _ -> str "prove_lt1")[ Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))); observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple) @@ -645,9 +645,7 @@ let pf_typel l tac = modified hypotheses are generalized in the process and should be introduced back later; the result is the pair of the tactic and the list of hypotheses that have been generalized and cleared. *) -let mkDestructEq : - Id.t list -> constr -> goal Evd.sigma -> tactic * Id.t list = - fun not_on_hyp expr g -> +let mkDestructEq not_on_hyp expr g = let hyps = pf_hyps g in let to_revert = Util.List.map_filter @@ -657,9 +655,9 @@ let mkDestructEq : if Id.List.mem id not_on_hyp || not (Termops.dependent (project g) expr (get_type decl)) then None else Some id) hyps in let to_revert_constr = List.rev_map mkVar to_revert in - let type_of_expr = pf_unsafe_type_of g expr in - let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|]):: - to_revert_constr in + let g, type_of_expr = tac_type_of g expr in + let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::to_revert_constr in + let tac = pf_typel new_hyps (fun _ -> observe_tclTHENLIST (fun _ _ -> str "mkDestructEq") [Proofview.V82.of_tactic (generalize new_hyps); @@ -668,7 +666,9 @@ let mkDestructEq : pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in Proofview.V82.of_tactic (change_in_concl ~check:true None changefun) g2); - Proofview.V82.of_tactic (simplest_case expr)]), to_revert + Proofview.V82.of_tactic (simplest_case expr)]) + in + g, tac, to_revert let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let sigma = project g in @@ -686,7 +686,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = info = mkCase(ci,t,a',l); is_main_branch = expr_info.is_main_branch; is_final = expr_info.is_final} in - let destruct_tac,rev_to_thin_intro = + let g,destruct_tac,rev_to_thin_intro = mkDestructEq [expr_info.rec_arg_id] a' g in let to_thin_intro = List.rev rev_to_thin_intro in observe_tac (fun _ _ -> str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a') @@ -842,7 +842,7 @@ let rec make_rewrite_list expr_info max = function (observe_tac (fun _ _ -> str "rewrite heq on " ++ Id.print p ) ( (fun g -> let sigma = project g in - let t_eq = compute_renamed_type g (mkVar hp) in + let t_eq = compute_renamed_type g hp in let k,def = let k_na,_,t = destProd sigma t_eq in let _,_,t = destProd sigma t in @@ -868,7 +868,7 @@ let make_rewrite expr_info l hp max = (observe_tac (fun _ _ -> str "make_rewrite") (tclTHENS (fun g -> let sigma = project g in - let t_eq = compute_renamed_type g (mkVar hp) in + let t_eq = compute_renamed_type g hp in let k,def = let k_na,_,t = destProd sigma t_eq in let _,_,t = destProd sigma t in diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 6c63a891e8..513f5ca77b 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -736,7 +736,7 @@ let refl_equal () = Coqlib.lib_ref "core.eq.type" call it before it is defined. *) let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> - let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in + let type_of_a = Tacmach.New.pf_get_type_of gl a in Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req -> Tacticals.New.tclTHENLIST [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))]; @@ -794,7 +794,7 @@ let destauto t = let destauto_in id = Proofview.Goal.enter begin fun gl -> - let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in + let ctype = Tacmach.New.pf_get_type_of gl (mkVar id) in (* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) (* Pp.msgnl (Printer.pr_lconstr (ctype)); *) destauto ctype diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 98d14f3d33..a0eefd1a39 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -483,7 +483,7 @@ let rec decompose_app_rel env evd t = | App (f, [||]) -> assert false | App (f, [|arg|]) -> let (f', argl, argr) = decompose_app_rel env evd arg in - let ty = Typing.unsafe_type_of env evd argl in + let ty = Retyping.get_type_of env evd argl in let r = Retyping.relevance_of_type env evd ty in let f'' = mkLambda (make_annot (Name default_dependent_ident) r, ty, mkLambda (make_annot (Name (Id.of_string "y")) r, lift 1 ty, @@ -789,7 +789,8 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev let morphargs, morphobjs = Array.chop first args in let morphargs', morphobjs' = Array.chop first args' in let appm = mkApp(m, morphargs) in - let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in + let evd, appmtype = Typing.type_of env (goalevars evars) appm in + let evars = evd, snd evars in let cstrs = List.map (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) (Array.to_list morphobjs') @@ -1906,7 +1907,7 @@ let declare_projection n instance_id r = let build_morphism_signature env sigma m = let m,ctx = Constrintern.interp_constr env sigma m in let sigma = Evd.from_ctx ctx in - let t = Typing.unsafe_type_of env sigma m in + let t = Retyping.get_type_of env sigma m in let cstrs = let rec aux t = match EConstr.kind sigma t with @@ -1936,7 +1937,7 @@ let build_morphism_signature env sigma m = let default_morphism sign m = let env = Global.env () in let sigma = Evd.from_env env in - let t = Typing.unsafe_type_of env sigma m in + let t = Retyping.get_type_of env sigma m in let evars, _, sign, cstrs = PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign) in @@ -2195,10 +2196,10 @@ let setoid_transitivity c = (transitivity_red true c) let setoid_symmetry_in id = - let open Tacmach.New in Proofview.Goal.enter begin fun gl -> - let sigma = project gl in - let ctype = pf_unsafe_type_of gl (mkVar id) in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let ctype = Retyping.get_type_of env sigma (mkVar id) in let binders,concl = decompose_prod_assum sigma ctype in let (equiv, args) = decompose_app sigma concl in let rec split_last_two = function diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index dcd85401d6..979e5bb8d8 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1713,7 +1713,6 @@ let onClearedName2 id tac = let destructure_hyps = Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_unsafe_type_of gl in let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let decidability = decidability env sigma in @@ -1759,7 +1758,7 @@ let destructure_hyps = | Kimp(t1,t2) -> (* t1 and t2 might be in Type rather than Prop. For t1, the decidability check will ensure being Prop. *) - if Termops.is_Prop sigma (type_of t2) + if Termops.is_Prop sigma (Retyping.get_type_of env sigma t2) then let d1 = decidability t1 in tclTHENLIST [ diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index d8dbf2f3dc..b212e7046a 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -151,7 +151,7 @@ let declare_one_prenex_implicit locality f = with _ -> errorstrm (pr_qualid f ++ str " is not declared") in let rec loop = function | a :: args' when Impargs.is_status_implicit a -> - Impargs.MaximallyImplicit :: loop args' + MaxImplicit :: loop args' | args' when List.exists Impargs.is_status_implicit args' -> errorstrm (str "Expected prenex implicits for " ++ pr_qualid f) | _ -> [] in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index cbd04a76ad..29d6726262 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2164,7 +2164,7 @@ let constr_of_pat env sigma arsign pat avoid = let IndType (indf, _) = try find_rectype env sigma (lift (-(List.length realargs)) ty) with Not_found -> error_case_not_inductive env sigma - {uj_val = ty; uj_type = Typing.unsafe_type_of env sigma ty} + {uj_val = ty; uj_type = Retyping.get_type_of env sigma ty} in let (ind,u), params = dest_ind_family indf in let params = List.map EConstr.of_constr params in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 02c2fc4a13..0969b3cc03 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -68,8 +68,9 @@ let glob_sort_eq u1 u2 = match u1, u2 with let binding_kind_eq bk1 bk2 = match bk1, bk2 with | Explicit, Explicit -> true - | Implicit, Implicit -> true - | (Explicit | Implicit), _ -> false + | NonMaxImplicit, NonMaxImplicit -> true + | MaxImplicit, MaxImplicit -> true + | (Explicit | NonMaxImplicit | MaxImplicit), _ -> false let case_style_eq s1 s2 = let open Constr in match s1, s2 with | LetStyle, LetStyle -> true diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 44323441b6..485a19421d 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -65,7 +65,7 @@ and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t type cases_pattern = [ `any ] cases_pattern_g -type binding_kind = Explicit | Implicit +type binding_kind = Explicit | MaxImplicit | NonMaxImplicit (** Representation of an internalized (or in other words globalized) term. *) type 'a glob_constr_r = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index bf61d44a10..2d98d48aa0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -47,7 +47,7 @@ open Evarconv module NamedDecl = Context.Named.Declaration -type typing_constraint = OfType of types | IsType | WithoutTypeConstraint +type typing_constraint = UnknownIfTermOrType | IsType | OfType of types | WithoutTypeConstraint let (!!) env = GlobEnv.env env @@ -446,7 +446,7 @@ let pretype_ref ?loc sigma env ref us = Pretype_errors.error_var_not_found ?loc !!env sigma id) | ref -> let sigma, c = pretype_global ?loc univ_flexible env sigma ref us in - let ty = unsafe_type_of !!env sigma c in + let sigma, ty = type_of !!env sigma c in sigma, make_judge c ty let interp_sort ?loc evd : glob_sort -> _ = function @@ -1290,7 +1290,7 @@ let ise_pretype_gen flags env sigma lvar kind c = in let env = GlobEnv.make ~hypnaming env sigma lvar in let sigma', c', c'_ty = match kind with - | WithoutTypeConstraint -> + | WithoutTypeConstraint | UnknownIfTermOrType -> let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses empty_tycon env sigma c in sigma, j.uj_val, j.uj_type | OfType exptyp -> diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 18e416596e..ee57f690a1 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -38,7 +38,11 @@ val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> val search_guard : ?loc:Loc.t -> env -> int list list -> Constr.rec_declaration -> int array -type typing_constraint = OfType of types | IsType | WithoutTypeConstraint +type typing_constraint = + | UnknownIfTermOrType (** E.g., unknown if manual implicit arguments allowed *) + | IsType (** Necessarily a type *) + | OfType of types (** A term of the expected type *) + | WithoutTypeConstraint (** A term of unknown expected type *) type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 4d4fe13983..d5beebe690 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -722,32 +722,31 @@ let magicaly_constant_of_fixbody env sigma reference bd = function | Name.Anonymous -> bd | Name.Name id -> let open UnivProblem in - try - let (cst_mod,_) = Constant.repr2 reference in - let cst = Constant.make2 cst_mod (Label.of_id id) in + let (cst_mod,_) = Constant.repr2 reference in + let cst = Constant.make2 cst_mod (Label.of_id id) in + if not (Environ.mem_constant cst env) then bd + else let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in match constant_opt_value_in env (cst,u) with | None -> bd | Some t -> let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in begin match csts with - | Some csts -> - let subst = Set.fold (fun cst acc -> - let l, r = match cst with - | ULub (u, v) | UWeak (u, v) -> u, v - | UEq (u, v) | ULe (u, v) -> - let get u = Option.get (Universe.level u) in - get u, get v - in - Univ.LMap.add l r acc) - csts Univ.LMap.empty - in - let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in - mkConstU (cst, EInstance.make inst) - | None -> bd + | Some csts -> + let subst = Set.fold (fun cst acc -> + let l, r = match cst with + | ULub (u, v) | UWeak (u, v) -> u, v + | UEq (u, v) | ULe (u, v) -> + let get u = Option.get (Universe.level u) in + get u, get v + in + Univ.LMap.add l r acc) + csts Univ.LMap.empty + in + let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in + mkConstU (cst, EInstance.make inst) + | None -> bd end - with - | Not_found -> bd let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) = let nbodies = Array.length bodies in diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 10e8cf7e0f..f87c50b5e4 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1197,7 +1197,7 @@ let abstract_scheme env sigma (locc,a) (c, sigma) = let pattern_occs loccs_trm = begin fun env sigma c -> let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in try - let _ = Typing.unsafe_type_of env sigma abstr_trm in + let sigma, _ = Typing.type_of env sigma abstr_trm in (sigma, applist(abstr_trm, List.map snd loccs_trm)) with Type_errors.TypeError (env',t) -> raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t)))) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index a15134f58d..4582844b71 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -253,6 +253,9 @@ let judge_of_type u = let judge_of_relative env v = Environ.on_judgment EConstr.of_constr (judge_of_relative env v) +let type_of_variable env id = + EConstr.of_constr (type_of_variable env id) + let judge_of_variable env id = Environ.on_judgment EConstr.of_constr (judge_of_variable env id) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1b07b2bb78..fd2dc7c2fc 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -30,6 +30,9 @@ val sort_of : env -> evar_map -> types -> evar_map * Sorts.t (** Typecheck a term has a given type (assuming the type is OK) *) val check : env -> evar_map -> constr -> types -> evar_map +(** Type of a variable. *) +val type_of_variable : env -> variable -> types + (** Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6486435ca2..2157c4ef6a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1274,12 +1274,14 @@ let applyHead env evd n c = else match EConstr.kind evd (whd_all env evd cty) with | Prod (_,c1,c2) -> - let (evd',evar) = - Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in - apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' + let (evd,evar) = + Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 + in + apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd | _ -> user_err Pp.(str "Apply_Head_Then") in - apprec n c (Typing.unsafe_type_of env evd c) evd + let evd, t = Typing.type_of env evd c in + apprec n c t evd let is_mimick_head sigma ts f = match EConstr.kind sigma f with diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index b55a41471a..2416819a6a 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -143,7 +143,8 @@ let tag_var = tag Tag.variable let pr_generalization bk ak c = let hd, tl = match bk with - | Implicit -> "{", "}" + | NonMaxImplicit -> "[", "]" + | MaxImplicit -> "{", "}" | Explicit -> "(", ")" in (* TODO: syntax Abstraction Kind *) str "`" ++ str hd ++ c ++ str tl @@ -324,12 +325,14 @@ let tag_var = tag Tag.variable let surround_impl k p = match k with | Explicit -> str"(" ++ p ++ str")" - | Implicit -> str"{" ++ p ++ str"}" + | NonMaxImplicit -> str"[" ++ p ++ str"]" + | MaxImplicit -> str"{" ++ p ++ str"}" let surround_implicit k p = match k with | Explicit -> p - | Implicit -> (str"{" ++ p ++ str"}") + | NonMaxImplicit -> str"[" ++ p ++ str"]" + | MaxImplicit -> (str"{" ++ p ++ str"}") let pr_binder many pr (nal,k,t) = match k with diff --git a/proofs/clenv.ml b/proofs/clenv.ml index e466992721..b0eb8dc646 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -128,8 +128,6 @@ let mk_clenv_from_n gls n (c,cty) = let mk_clenv_from gls = mk_clenv_from_n gls None -let mk_clenv_type_of gls t = mk_clenv_from gls (t,Tacmach.New.pf_unsafe_type_of gls t) - (******************************************************************) (* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 3fca967395..7213c9318c 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -46,7 +46,6 @@ val clenv_meta_type : clausenv -> metavariable -> types val mk_clenv_from : Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv val mk_clenv_from_n : Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv -val mk_clenv_type_of : Proofview.Goal.t -> EConstr.constr -> clausenv val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv (** Refresh the universes in a clenv *) diff --git a/proofs/logic.ml b/proofs/logic.ml index a361c4208e..bac13fcfc3 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -79,7 +79,7 @@ let check = ref false let with_check = Flags.with_option check let check_typability env sigma c = - if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in () + if !check then fst (type_of env sigma (EConstr.of_constr c)) else sigma (************************************************************************) (************************************************************************) @@ -363,7 +363,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = gl::goalacc, conclty, sigma, ev | Cast (t,k, ty) -> - check_typability env sigma ty; + let sigma = check_typability env sigma ty in let sigma = check_conv_leq_goal env sigma trm ty conclty in let res = mk_refgoals sigma goal goalacc ty t in (* we keep the casts (in particular VMcast and NATIVEcast) except @@ -430,13 +430,13 @@ and mk_hdgoals sigma goal goalacc trm = Goal.V82.mk_goal sigma hyps concl in match kind trm with | Cast (c,_, ty) when isMeta c -> - check_typability env sigma ty; + let sigma = check_typability env sigma ty in let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in let ev = EConstr.Unsafe.to_constr ev in gl::goalacc,ty,sigma,ev | Cast (t,_, ty) -> - check_typability env sigma ty; + let sigma = check_typability env sigma ty in mk_refgoals sigma goal goalacc ty t | App (f,l) -> diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index cd6f445503..1bbcca8827 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -238,7 +238,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = in try let others,(c1,c2) = split_last_two args in - let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in + let ty1, ty2 = Retyping.get_type_of env eqclause.evd c1, Retyping.get_type_of env eqclause.evd c2 in (* XXX: It looks like mk_clenv_from_env should be fixed instead? *) let open EConstr in let hyp_ty = Unsafe.to_constr ty in @@ -261,7 +261,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = | None -> None let find_applied_relation ?loc metas env sigma c left2right = - let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in + let ctype = Retyping.get_type_of env sigma (EConstr.of_constr c) in match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index f8cb8870ea..ccd88d2c35 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1202,10 +1202,9 @@ let autoapply c i = in let flags = auto_unif_flags (Hints.Hint_db.transparent_state hintdb) in - let cty = Tacmach.New.pf_unsafe_type_of gl c in + let cty = Tacmach.New.pf_get_type_of gl c in let ce = mk_clenv_from gl (c,cty) in - unify_e_resolve false flags gl - ((c,cty,Univ.ContextSet.empty),0,ce) <*> + unify_e_resolve false flags gl ((c,cty,Univ.ContextSet.empty),0,ce) <*> Proofview.tclEVARMAP >>= (fun sigma -> let sigma = Typeclasses.make_unresolvables (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 1f5a6380fd..c7b6998c8c 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -110,8 +110,7 @@ let contradiction_term (c,lbind as cl) = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let type_of = Tacmach.New.pf_unsafe_type_of gl in - let typ = type_of c in + let typ = Tacmach.New.pf_get_type_of gl c in let _, ccl = splay_prod env sigma typ in if is_empty_type env sigma ccl then Tacticals.New.tclTHEN diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 361215bf38..80ca124912 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -32,11 +32,13 @@ let eauto_unif_flags = auto_flags_of_state TransparentState.full let e_give_exact ?(flags=eauto_unif_flags) c = Proofview.Goal.enter begin fun gl -> - let t1 = Tacmach.New.pf_unsafe_type_of gl c in + let sigma, t1 = Tacmach.New.pf_type_of gl c in let t2 = Tacmach.New.pf_concl gl in - let sigma = Tacmach.New.project gl in if occur_existential sigma t1 || occur_existential sigma t2 then - Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) + Tacticals.New.tclTHENLIST + [Proofview.Unsafe.tclEVARS sigma; + Clenvtac.unify ~flags t1; + exact_no_check c] else exact_check c end diff --git a/tactics/elim.ml b/tactics/elim.ml index ea61b8e4df..379a8d5401 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -80,14 +80,11 @@ let up_to_delta = ref false (* true *) let general_decompose recognizer c = Proofview.Goal.enter begin fun gl -> - let type_of = pf_unsafe_type_of gl in - let env = pf_env gl in - let sigma = project gl in - let typc = type_of c in + let typc = pf_get_type_of gl c in tclTHENS (cut typc) [ tclTHEN (intro_using tmphyp_name) (onLastHypId - (ifOnHyp (recognizer env sigma) (general_decompose_aux (recognizer env sigma)) + (ifOnHyp recognizer (general_decompose_aux recognizer) (fun id -> clear [id]))); exact_no_check c ] end @@ -136,7 +133,7 @@ let induction_trailer abs_i abs_j bargs = (onLastHypId (fun id -> Proofview.Goal.enter begin fun gl -> - let idty = pf_unsafe_type_of gl (mkVar id) in + let idty = pf_get_type_of gl (mkVar id) in let fvty = global_vars (pf_env gl) (project gl) idty in let possible_bring_hyps = (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index bdfd200988..a82b26f428 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -195,13 +195,13 @@ let rec solveArg hyps eqonleft mk largs rargs = match largs, rargs with ] | a1 :: largs, a2 :: rargs -> Proofview.Goal.enter begin fun gl -> - let rectype = pf_unsafe_type_of gl a1 in + let sigma, rectype = pf_type_of gl a1 in let decide = mk rectype a1 a2 in let tac hyp = solveArg (hyp :: hyps) eqonleft mk largs rargs in let subtacs = if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto] else [diseqCase hyps eqonleft;eqCase tac;default_auto] in - (tclTHENS (elim_type decide) subtacs) + tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENS (elim_type decide) subtacs) end | _ -> invalid_arg "List.fold_right2" @@ -274,11 +274,12 @@ let compare c1 c2 = pf_constr_of_global (lib_ref "core.eq.type") >>= fun eqc -> pf_constr_of_global (lib_ref "core.not.type") >>= fun notc -> Proofview.Goal.enter begin fun gl -> - let rectype = pf_unsafe_type_of gl c1 in + let sigma, rectype = pf_type_of gl c1 in let ops = (opc,eqc,notc) in let decide = mkDecideEqGoal true ops rectype c1 c2 in - (tclTHENS (cut decide) - [(tclTHEN intro - (tclTHEN (onLastHyp simplest_case) clear_last)); - decideEquality rectype ops]) + tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (tclTHENS (cut decide) + [(tclTHEN intro + (tclTHEN (onLastHyp simplest_case) clear_last)); + decideEquality rectype ops]) end diff --git a/tactics/equality.ml b/tactics/equality.ml index 96b61b6994..9195746dc6 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1062,14 +1062,14 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let onEquality with_evars tac (c,lbindc) = Proofview.Goal.enter begin fun gl -> - let type_of = pf_unsafe_type_of gl in let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in - let t = type_of c in + let t = pf_get_type_of gl c in let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in let eqn = clenv_type eq_clause' in - let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in + (* FIXME evar leak *) + let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) (tac (eq,eqn,eq_args) eq_clause') @@ -1165,7 +1165,7 @@ let minimal_free_rels_rec env sigma = let rec minimalrec_free_rels_rec prev_rels (c,cty) = let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in let combined_rels = Int.Set.union prev_rels direct_rels in - let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i))) + let folder rels i = snd (minimalrec_free_rels_rec rels (c, get_type_of env sigma (mkRel i))) in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels))) in minimalrec_free_rels_rec Int.Set.empty @@ -1210,7 +1210,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let rec sigrec_clausal_form sigma siglen p_i = if Int.equal siglen 0 then (* is the default value typable with the expected type *) - let dflt_typ = unsafe_type_of env sigma dflt in + let sigma, dflt_typ = type_of env sigma dflt in try let sigma = Evarconv.unify_leq_delay env sigma dflt_typ p_i in let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in @@ -1224,29 +1224,21 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let sigma, ev = Evarutil.new_evar env sigma a in let rty = beta_applist sigma (p_i_minus_1,[ev]) in let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in - let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in - match evopt with - | Some w -> - let w_type = unsafe_type_of env sigma w in - begin match Evarconv.unify_leq_delay env sigma w_type a with - | sigma -> - let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in - sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) - | exception Evarconv.UnableToUnify _ -> - user_err Pp.(str "Cannot solve a unification problem.") - end - | None -> - (* This at least happens if what has been detected as a - dependency is not one; use an evasive error message; - even if the problem is upwards: unification should be - tried in the first place in make_iterated_tuple instead - of approximatively computing the free rels; then - unsolved evars would mean not binding rel *) - user_err Pp.(str "Cannot solve a unification problem.") + if EConstr.isEvar sigma ev then + (* This at least happens if what has been detected as a + dependency is not one; use an evasive error message; + even if the problem is upwards: unification should be + tried in the first place in make_iterated_tuple instead + of approximatively computing the free rels; then + unsolved evars would mean not binding rel *) + user_err Pp.(str "Cannot solve a unification problem.") + else + let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in + sigma, applist(exist_term,[a;p_i_minus_1;ev;tuple_tail]) in let sigma = Evd.clear_metas sigma in let sigma, scf = sigrec_clausal_form sigma siglen ty in - sigma, Evarutil.nf_evar sigma scf + sigma, Evarutil.nf_evar sigma scf (* The problem is to build a destructor (a generalization of the predecessor) which, when applied to a term made of constructors @@ -1319,7 +1311,7 @@ let make_iterated_tuple env sigma dflt (z,zty) = sigma, (tuple,tuplety,dfltval) let rec build_injrec env sigma dflt c = function - | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c) + | [] -> make_iterated_tuple env sigma dflt (c,get_type_of env sigma c) | ((sp,cnum),argnum)::l -> try let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in @@ -1341,7 +1333,7 @@ let inject_if_homogenous_dependent_pair ty = Proofview.Goal.enter begin fun gl -> try let sigma = Tacmach.New.project gl in - let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in + let eq,u,(t,t1,t2) = pf_apply find_this_eq_data_decompose gl ty in (* fetch the informations of the pair *) let sigTconstr = Coqlib.(lib_ref "core.sigT.type") in let existTconstr = Coqlib.lib_ref "core.sigT.intro" in @@ -1360,7 +1352,7 @@ let inject_if_homogenous_dependent_pair ty = if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind && pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit; check_required_library ["Coq";"Logic";"Eqdep_dec"]; - let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in + let new_eq_args = [|pf_get_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in let inj2 = lib_ref "core.eqdep_dec.inj_pair2" in let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in (* cut with the good equality and prove the requested goal *) @@ -1603,7 +1595,7 @@ let cutSubstInConcl l2r eqn = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in + let (lbeq,u,(t,e1,e2)) = pf_apply find_eq_data_decompose gl eqn in let typ = pf_concl gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in @@ -1620,7 +1612,7 @@ let cutSubstInHyp l2r eqn id = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in + let (lbeq,u,(t,e1,e2)) = pf_apply find_eq_data_decompose gl eqn in let typ = pf_get_hyp_typ id gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in @@ -1715,7 +1707,7 @@ let is_eq_x gl x d = | _ -> false in let c = pf_nf_evar gl (NamedDecl.get_type d) in - let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in + let (_,lhs,rhs) = pi3 (pf_apply find_eq_data_decompose gl c) in if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true)); if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false)) with Constr_matching.PatternMatchingFailure -> @@ -1812,7 +1804,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let find_equations gl = let env = Proofview.Goal.env gl in let sigma = project gl in - let find_eq_data_decompose = find_eq_data_decompose gl in + let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in let select_equation_name decl = try let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in @@ -1837,7 +1829,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = Proofview.Goal.enter begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in - let find_eq_data_decompose = find_eq_data_decompose gl in + let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in let c = pf_get_hyp hyp gl |> NamedDecl.get_type in let _,_,(_,x,y) = find_eq_data_decompose c in (* J.F.: added to prevent failure on goal containing x=x as an hyp *) @@ -1863,7 +1855,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let-ins *) Proofview.Goal.enter begin fun gl -> let sigma = project gl in - let find_eq_data_decompose = find_eq_data_decompose gl in + let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in let test (_,c) = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in @@ -1887,19 +1879,19 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let cond_eq_term_left c t gl = try - let (_,x,_) = pi3 (find_eq_data_decompose gl t) in + let (_,x,_) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then true else failwith "not convertible" with Constr_matching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term_right c t gl = try - let (_,_,x) = pi3 (find_eq_data_decompose gl t) in + let (_,_,x) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then false else failwith "not convertible" with Constr_matching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term c t gl = try - let (_,x,y) = pi3 (find_eq_data_decompose gl t) in + let (_,x,y) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then true else if pf_conv_x gl c y then false else failwith "not convertible" diff --git a/tactics/hints.ml b/tactics/hints.ml index 7b3797119a..73e8331bcb 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -26,7 +26,6 @@ open Libnames open Smartlocate open Termops open Inductiveops -open Typing open Typeclasses open Pattern open Patternops @@ -966,16 +965,17 @@ let make_mode ref m = let make_trivial env sigma poly ?(name=PathAny) r = let c,ctx = fresh_global_or_constr env sigma poly r in let sigma = Evd.merge_context_set univ_flexible sigma ctx in - let t = hnf_constr env sigma (unsafe_type_of env sigma c) in + let t = hnf_constr env sigma (Retyping.get_type_of env sigma c) in let hd = head_constr sigma t in let ce = mk_clenv_from_env env sigma None (c,t) in - (Some hd, { pri=1; - poly = poly; - pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce))); - name = name; - db = None; - secvars = secvars_of_constr env sigma c; - code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) + (Some hd, + { pri=1; + poly = poly; + pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce))); + name = name; + db = None; + secvars = secvars_of_constr env sigma c; + code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) diff --git a/tactics/hints.mli b/tactics/hints.mli index 2a9b71387e..9c9f0b7708 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -160,6 +160,8 @@ module Hint_db : val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit + val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a + val use_dn : t -> bool val transparent_state : t -> TransparentState.t val set_transparent_state : t -> TransparentState.t -> t diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 90a9a7acd9..c5ed02e043 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -19,7 +19,6 @@ open Inductiveops open Constr_matching open Coqlib open Declarations -open Tacmach.New open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -452,26 +451,26 @@ let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *) let hd,u = destInd sigma (fst (destApp sigma eqn)) in d,u,k -let extract_eq_args gl = function +let extract_eq_args env sigma = function | MonomorphicLeibnizEq (e1,e2) -> - let t = pf_unsafe_type_of gl e1 in (t,e1,e2) + let t = Retyping.get_type_of env sigma e1 in (t,e1,e2) | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2) | HeterogenousEq (t1,e1,t2,e2) -> - if pf_conv_x gl t1 t2 then (t1,e1,e2) + if Reductionops.is_conv env sigma t1 t2 then (t1,e1,e2) else raise PatternMatchingFailure -let find_eq_data_decompose gl eqn = - let (lbeq,u,eq_args) = find_eq_data (project gl) eqn in - (lbeq,u,extract_eq_args gl eq_args) +let find_eq_data_decompose env sigma eqn = + let (lbeq,u,eq_args) = find_eq_data sigma eqn in + (lbeq,u,extract_eq_args env sigma eq_args) -let find_this_eq_data_decompose gl eqn = +let find_this_eq_data_decompose env sigma eqn = let (lbeq,u,eq_args) = try (*first_match (match_eq eqn) inversible_equalities*) - find_eq_data (project gl) eqn + find_eq_data sigma eqn with PatternMatchingFailure -> user_err (str "No primitive equality found.") in let eq_args = - try extract_eq_args gl eq_args + try extract_eq_args env sigma eq_args with PatternMatchingFailure -> user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in (lbeq,u,eq_args) diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 803305a1ca..0000f81d3f 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -122,11 +122,11 @@ val match_with_equation: (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *) -val find_eq_data_decompose : Proofview.Goal.t -> constr -> +val find_eq_data_decompose : Environ.env -> evar_map -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** Idem but fails with an error message instead of PatternMatchingFailure *) -val find_this_eq_data_decompose : Proofview.Goal.t -> constr -> +val find_this_eq_data_decompose : Environ.env -> evar_map -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** A variant that returns more informative structure on the equality found *) diff --git a/tactics/inv.ml b/tactics/inv.ml index be0421d42d..2181eb25af 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -464,7 +464,7 @@ let raw_inversion inv_kind id status names = let concl = Proofview.Goal.concl gl in let c = mkVar id in let (ind, t) = - try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c) + try pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl c) with UserError _ -> let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in CErrors.user_err msg diff --git a/tactics/leminv.ml b/tactics/leminv.ml index cf58c9306c..def4af1ae8 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -259,7 +259,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac = let lemInv id c = Proofview.Goal.enter begin fun gls -> try - let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in + let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_get_type_of gls c) in let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false with diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index ed7ab9164a..58d2097dea 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -587,7 +587,7 @@ module New = struct let ifOnHyp pred tac1 tac2 id = Proofview.Goal.enter begin fun gl -> let typ = Tacmach.New.pf_get_hyp_typ id gl in - if pred (id,typ) then + if pf_apply pred gl (id,typ) then tac1 id else tac2 id @@ -633,7 +633,7 @@ module New = struct (Proofview.Goal.enter begin fun gl -> let indclause = mk_clenv_from gl (c, t) in (* applying elimination_scheme just a little modified *) - let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim) in + let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim) in let indmv = match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with | Meta mv -> mv @@ -741,7 +741,7 @@ module New = struct let elimination_then tac c = Proofview.Goal.enter begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in + let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with | NotRecord -> true,gl_make_elim diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 31d26834d6..4b93b81d1c 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -222,7 +222,7 @@ module New : sig val nLastDecls : Proofview.Goal.t -> int -> named_context - val ifOnHyp : (Id.t * types -> bool) -> + val ifOnHyp : (Environ.env -> evar_map -> Id.t * types -> bool) -> (Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) -> Id.t -> unit Proofview.tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f6f7c71dfd..609b752716 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -47,6 +47,9 @@ open Context.Named.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration +let tclEVARS = Proofview.Unsafe.tclEVARS +let tclEVARSTHEN sigma t = Proofview.tclTHEN (tclEVARS sigma) t + let inj_with_occurrences e = (AllOccurrences,e) let typ_of env sigma c = @@ -151,11 +154,12 @@ let convert_concl ~check ty k = Refine.refine ~typecheck:false begin fun sigma -> let sigma = if check then begin - ignore (Typing.unsafe_type_of env sigma ty); + let sigma, _ = Typing.type_of env sigma ty in match Reductionops.infer_conv env sigma ty conclty with | None -> error "Not convertible." | Some sigma -> sigma - end else sigma in + end else sigma + in let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ty in let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in (sigma, ans) @@ -849,12 +853,13 @@ let change_on_subterm ~check cv_pb deep t where env sigma c = change_and_check Reduction.CONV mayneedglobalcheck true (t subst) else fun env sigma _c -> t subst env sigma) env sigma c in - if !mayneedglobalcheck then + let sigma = if !mayneedglobalcheck then begin - try ignore (Typing.unsafe_type_of env sigma c) + try fst (Typing.type_of env sigma c) with e when catchable_exception e -> error "Replacement would lead to an ill-typed term." - end; + end else sigma + in (sigma, c) let change_in_concl ~check occl t = @@ -1308,30 +1313,23 @@ let cut c = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in - let relevance = - try - (* Backward compat: ensure that [c] is well-typed. Plus we - need to know the relevance *) - let typ = Typing.unsafe_type_of env sigma c in - let typ = whd_all env sigma typ in - match EConstr.kind sigma typ with - | Sort s -> Some (Sorts.relevance_of_sort (ESorts.kind sigma s)) - | _ -> None - with e when Pretype_errors.precatchable_exception e -> None - in - match relevance with - | Some r -> + (* Backward compat: ensure that [c] is well-typed. Plus we need to + know the relevance *) + match Typing.sort_of env sigma c with + | exception e when Pretype_errors.precatchable_exception e -> + Tacticals.New.tclZEROMSG (str "Not a proposition or a type.") + | sigma, s -> + let r = Sorts.relevance_of_sort s in let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in (* Backward compat: normalize [c]. *) let c = if normalize_cut then local_strong whd_betaiota sigma c else c in - Refine.refine ~typecheck:false begin fun h -> - let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in - let (h, x) = Evarutil.new_evar env h c in - let f = mkLetIn (make_annot (Name id) r, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in - (h, f) - end - | None -> - Tacticals.New.tclZEROMSG (str "Not a proposition or a type.") + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Refine.refine ~typecheck:false begin fun h -> + let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in + let (h, x) = Evarutil.new_evar env h c in + let f = mkLetIn (make_annot (Name id) r, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in + (h, f) + end) end let error_uninstantiated_metas t clenv = @@ -1533,16 +1531,19 @@ exception IsNonrec let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite -let find_ind_eliminator ind s gl = - let env = Proofview.Goal.env gl in +let find_ind_eliminator env sigma ind s = let gr = lookup_eliminator env ind s in - Tacmach.New.pf_apply Evd.fresh_global gl gr + Evd.fresh_global env sigma gr let find_eliminator c gl = - let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let sigma, t = Typing.type_of env sigma c in + let ((ind,u),t) = reduce_to_quantified_ind env sigma t in if is_nonrec ind then raise IsNonrec; - let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in - evd, { elimindex = None; elimbody = (c,NoBindings) } + let sigma, c = find_ind_eliminator env sigma ind (Retyping.get_sort_family_of env sigma concl) in + sigma, { elimindex = None; elimbody = (c,NoBindings) } let default_elim with_evars clear_flag (c,_ as cx) = Proofview.tclORELSE @@ -1928,18 +1929,20 @@ let apply_in_delayed_once ?(respect_opaque = false) with_delta let cut_and_apply c = Proofview.Goal.enter begin fun gl -> - let sigma = Tacmach.New.project gl in - match EConstr.kind sigma (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with - | Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 -> - let concl = Proofview.Goal.concl gl in - let env = Tacmach.New.pf_env gl in - Refine.refine ~typecheck:false begin fun sigma -> - let typ = mkProd (make_annot Anonymous Sorts.Relevant, c2, concl) in - let (sigma, f) = Evarutil.new_evar env sigma typ in - let (sigma, x) = Evarutil.new_evar env sigma c1 in - (sigma, mkApp (f, [|mkApp (c, [|x|])|])) - end - | _ -> error "lapply needs a non-dependent product." + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let sigma, t = Typing.type_of env sigma c in + match EConstr.kind sigma (hnf_constr env sigma t) with + | Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 -> + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Refine.refine ~typecheck:false begin fun sigma -> + let typ = mkProd (make_annot Anonymous Sorts.Relevant, c2, concl) in + let (sigma, f) = Evarutil.new_evar env sigma typ in + let (sigma, x) = Evarutil.new_evar env sigma c1 in + (sigma, mkApp (f, [|mkApp (c, [|x|])|])) + end) + | _ -> error "lapply needs a non-dependent product." end (********************************************************************) @@ -2285,8 +2288,8 @@ let intro_decomp_eq_function = ref (fun _ -> failwith "Not implemented") let declare_intro_decomp_eq f = intro_decomp_eq_function := f -let my_find_eq_data_decompose gl t = - try Some (find_eq_data_decompose gl t) +let my_find_eq_data_decompose env sigma t = + try Some (find_eq_data_decompose env sigma t) with e when is_anomaly e (* Hack in case equality is not yet defined... one day, maybe, known equalities will be dynamically registered *) @@ -2296,13 +2299,15 @@ let my_find_eq_data_decompose gl t = let intro_decomp_eq ?loc l thin tac id = Proofview.Goal.enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_unsafe_type_of gl c in - let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in - match my_find_eq_data_decompose gl t with + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, t = Typing.type_of env sigma c in + let _,t = reduce_to_quantified_ind env sigma t in + match my_find_eq_data_decompose env sigma t with | Some (eq,u,eq_args) -> !intro_decomp_eq_function - (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l) - (eq,t,eq_args) (c, t) + (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l) + (eq,t,eq_args) (c, t) | None -> Tacticals.New.tclZEROMSG (str "Not a primitive equality here.") end @@ -2310,16 +2315,19 @@ let intro_decomp_eq ?loc l thin tac id = let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id = Proofview.Goal.enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_unsafe_type_of gl c in - let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, t = Typing.type_of env sigma c in + let (ind,t) = reduce_to_quantified_ind env sigma t in let branchsigns = compute_constructor_signatures ~rec_flag:false ind in let nv_with_let = Array.map List.length branchsigns in let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in let ll = get_and_check_or_and_pattern ?loc ll branchsigns in - Tacticals.New.tclTHENLASTn - (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id])) - (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l) - nv_with_let ll) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tacticals.New.tclTHENLASTn + (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id])) + (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l) + nv_with_let ll)) end let rewrite_hyp_then assert_style with_evars thin l2r id tac = @@ -2333,9 +2341,8 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let type_of = Tacmach.New.pf_unsafe_type_of gl in - let whd_all = Tacmach.New.pf_apply whd_all gl in - let t = whd_all (type_of (mkVar id)) in + let sigma, t = Typing.type_of env sigma (mkVar id) in + let t = whd_all env sigma t in let eqtac, thin = match match_with_equality_type env sigma t with | Some (hdcncl,[_;lhs;rhs]) -> if l2r && isVar sigma lhs && not (occur_var env sigma (destVar sigma lhs) rhs) then @@ -2361,7 +2368,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]), thin in (* Skip the side conditions of the rewriting step *) - Tacticals.New.tclTHENFIRST eqtac (tac thin) + tclEVARSTHEN sigma (Tacticals.New.tclTHENFIRST eqtac (tac thin)) end let prepare_naming ?loc = function @@ -3392,8 +3399,9 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = let id = match EConstr.kind sigma c with | Var id -> id | _ -> - let type_of = Tacmach.New.pf_unsafe_type_of gl in - id_of_name_using_hdchar env sigma (type_of c) Anonymous in + let type_of = Tacmach.New.pf_get_type_of gl in + id_of_name_using_hdchar env sigma (type_of c) Anonymous + in let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN (letin_tac None (Name x) c None allHypsAndConcl) @@ -3794,15 +3802,15 @@ let is_defined_variable env id = env |> lookup_named id |> is_local_def let abstract_args gl generalize_vars dep id defined f args = - let open Tacmach.New in let open Context.Rel.Declaration in let sigma = ref (Tacmach.New.project gl) in let env = Tacmach.New.pf_env gl in let concl = Tacmach.New.pf_concl gl in + let hyps = Proofview.Goal.hyps gl in let dep = dep || local_occur_var !sigma id concl in let avoid = ref Id.Set.empty in let get_id name = - let id = new_fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in + let id = fresh_id_in_env !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") env in avoid := Id.Set.add id !avoid; id in (* Build application generalized w.r.t. the argument plus the necessary eqs. @@ -3811,14 +3819,14 @@ let abstract_args gl generalize_vars dep id defined f args = eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *) *) - let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg = + let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars) arg = let name, ty_relevance, ty, arity = let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in let decl = List.hd rel in RelDecl.get_name decl, RelDecl.get_relevance decl, RelDecl.get_type decl, c in - let argty = Tacmach.New.pf_unsafe_type_of gl arg in - let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in + let sigma', argty = Typing.type_of env !sigma arg in + let sigma', ty = Evarsolve.refresh_universes (Some true) env sigma' ty in let () = sigma := sigma' in let lenctx = List.length ctx in let liftargty = lift lenctx argty in @@ -3826,7 +3834,7 @@ let abstract_args gl generalize_vars dep id defined f args = match EConstr.kind !sigma arg with | Var id when not (is_defined_variable env id) && leq && not (Id.Set.mem id nongenvars) -> (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, - Id.Set.add id nongenvars, Id.Set.remove id vars, env) + Id.Set.add id nongenvars, Id.Set.remove id vars) | _ -> let name = get_id name in let decl = LocalAssum (make_annot (Name name) ty_relevance, ty) in @@ -3848,7 +3856,7 @@ let abstract_args gl generalize_vars dep id defined f args = let refls = refl :: refls in let argvars = ids_of_constr !sigma vars arg in (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, - nongenvars, Id.Set.union argvars vars, env) + nongenvars, Id.Set.union argvars vars) in let f', args' = decompose_indapp !sigma f args in let dogen, f', args' = @@ -3862,15 +3870,16 @@ let abstract_args gl generalize_vars dep id defined f args = true, mkApp (f', before), after in if dogen then - let tyf' = Tacmach.New.pf_unsafe_type_of gl f' in - let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = - Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' + let sigma', tyf' = Typing.type_of env !sigma f' in + sigma := sigma'; + let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars = + Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty) args' in let args, refls = List.rev args, List.rev refls in let vars = if generalize_vars then let nogen = Id.Set.add id nogen in - hyps_of_vars (pf_env gl) (project gl) (Proofview.Goal.hyps gl) nogen vars + hyps_of_vars env !sigma hyps nogen vars else [] in let body, c' = @@ -3878,7 +3887,7 @@ let abstract_args gl generalize_vars dep id defined f args = else None, c' in let typ = Tacmach.New.pf_get_hyp_typ id gl in - let tac = make_abstract_generalize (pf_env gl) id typ concl dep ctx body c' eqs args refls in + let tac = make_abstract_generalize env id typ concl dep ctx body c' eqs args refls in let tac = Proofview.Unsafe.tclEVARS !sigma <*> tac in Some (tac, dep, succ (List.length ctx), vars) else None @@ -4222,15 +4231,15 @@ let guess_elim isrec dep s hyp0 gl = let ind = EConstr.of_constr ind in (sigma, ind) in - let elimt = Typing.unsafe_type_of env sigma elimc in - sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u) + let sigma, elimt = Typing.type_of env sigma elimc in + sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u) let given_elim hyp0 (elimc,lbind as e) gl = let sigma = Tacmach.New.project gl in let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let ind_type_guess,_ = decompose_app sigma (snd (decompose_prod sigma tmptyp0)) in - let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in - Tacmach.New.project gl, (e, elimt), ind_type_guess + let sigma, elimt = Tacmach.New.pf_type_of gl elimc in + sigma, (e, elimt), ind_type_guess type scheme_signature = (Id.Set.t * (elim_arg_kind * bool * bool * Id.t) list) array @@ -4240,33 +4249,32 @@ type eliminator_source = | ElimOver of bool * Id.t let find_induction_type isrec elim hyp0 gl = - let sigma = Tacmach.New.project gl in - let scheme,elim = + let sigma, scheme,elim = match elim with | None -> let sort = Tacticals.New.elimination_sort_of_goal gl in - let _, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in + let sigma, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in let scheme = compute_elim_sig sigma ~elimc elimt in (* We drop the scheme waiting to know if it is dependent *) - scheme, ElimOver (isrec,hyp0) + sigma, scheme, ElimOver (isrec,hyp0) | Some e -> - let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in + let sigma, (elimc,elimt),ind_guess = given_elim hyp0 e gl in let scheme = compute_elim_sig sigma ~elimc elimt in if Option.is_empty scheme.indarg then error "Cannot find induction type"; - let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in + let indsign = compute_scheme_signature sigma scheme hyp0 ind_guess in let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in - scheme, ElimUsing (elim,indsign) + sigma, scheme, ElimUsing (elim,indsign) in match scheme.indref with | None -> error_ind_scheme "" - | Some ref -> ref, scheme.nparams, elim + | Some ref -> sigma, (ref, scheme.nparams, elim) let get_elim_signature elim hyp0 gl = compute_elim_signature (given_elim hyp0 elim gl) hyp0 let is_functional_induction elimc gl = let sigma = Tacmach.New.project gl in - let scheme = compute_elim_sig sigma ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in + let scheme = compute_elim_sig sigma ~elimc (Tacmach.New.pf_get_type_of gl (fst elimc)) in (* The test is not safe: with non-functional induction on non-standard induction scheme, this may fail *) Option.is_empty scheme.indarg @@ -4380,10 +4388,11 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps = Proofview.Goal.enter begin fun gl -> - let elim_info = find_induction_type isrec elim hyp0 gl in - atomize_param_of_ind_then elim_info hyp0 (fun indvars -> - apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names - (fun elim -> induction_tac with_evars [] [hyp0] elim)) + let sigma, elim_info = find_induction_type isrec elim hyp0 gl in + tclEVARSTHEN sigma + (atomize_param_of_ind_then elim_info hyp0 (fun indvars -> + apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names + (fun elim -> induction_tac with_evars [] [hyp0] elim))) end let msg_not_right_number_induction_arguments scheme = @@ -4658,18 +4667,16 @@ let induction_gen_l isrec with_evars elim names lc = | _ -> Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_unsafe_type_of gl in - let sigma = Tacmach.New.project gl in - Proofview.tclENV >>= fun env -> - let x = - id_of_name_using_hdchar env sigma (type_of c) Anonymous in - + let sigma, t = pf_apply Typing.type_of gl c in + let x = id_of_name_using_hdchar (Proofview.Goal.env gl) sigma t Anonymous in let id = new_fresh_id Id.Set.empty x gl in let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in let () = newlc:=id::!newlc in - Tacticals.New.tclTHEN - (letin_tac None (Name id) c None allHypsAndConcl) - (atomize_list newl') + Tacticals.New.tclTHENLIST [ + tclEVARS sigma; + letin_tac None (Name id) c None allHypsAndConcl; + atomize_list newl'; + ] end in Tacticals.New.tclTHENLIST [ @@ -4765,7 +4772,10 @@ let destruct ev clr c l e = let elim_scheme_type elim t = Proofview.Goal.enter begin fun gl -> - let clause = mk_clenv_type_of gl elim in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, elimt = Typing.type_of env sigma elim in + let clause = mk_clenv_from_env env sigma None (elim,elimt) in match EConstr.kind clause.evd (last_arg clause.evd clause.templval.rebus) with | Meta mv -> let clause' = @@ -4779,7 +4789,9 @@ let elim_scheme_type elim t = let elim_type t = Proofview.Goal.enter begin fun gl -> let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in - let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in + let evd, elimc = Tacmach.New.pf_apply find_ind_eliminator gl (fst ind) + (Tacticals.New.elimination_sort_of_goal gl) + in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t) end @@ -4857,7 +4869,8 @@ let prove_symmetry hdcncl eq_kind = Tacticals.New.onLastHyp simplest_case; one_constructor 1 NoBindings ]) -let match_with_equation sigma c = +let match_with_equation c = + Proofview.tclEVARMAP >>= fun sigma -> Proofview.tclENV >>= fun env -> try let res = match_with_equation env sigma c in @@ -4870,9 +4883,8 @@ let symmetry_red allowred = (* PL: usual symmetry don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) - let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - match_with_equation sigma concl >>= fun with_eqn -> + match_with_equation concl >>= fun with_eqn -> match with_eqn with | Some eq_data,_,_ -> Tacticals.New.tclTHEN @@ -4894,25 +4906,25 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = Proofview.Goal.enter begin fun gl -> - let sigma = Tacmach.New.project gl in - let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in - let sign,t = decompose_prod_assum sigma ctype in - Proofview.tclORELSE - begin - match_with_equation sigma t >>= fun (_,hdcncl,eq) -> - let symccl = - match eq with - | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |]) - | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |]) - | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in - Tacticals.New.tclTHENS (cut (EConstr.it_mkProd_or_LetIn symccl sign)) - [ intro_replacing id; - Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ] - end - begin function (e, info) -> match e with - | NoEquationFound -> Hook.get forward_setoid_symmetry_in id - | e -> Proofview.tclZERO ~info e - end + let sigma, ctype = Tacmach.New.pf_type_of gl (mkVar id) in + let sign,t = decompose_prod_assum sigma ctype in + tclEVARSTHEN sigma + (Proofview.tclORELSE + begin + match_with_equation t >>= fun (_,hdcncl,eq) -> + let symccl = + match eq with + | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |]) + | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |]) + | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in + Tacticals.New.tclTHENS (cut (EConstr.it_mkProd_or_LetIn symccl sign)) + [ intro_replacing id; + Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ] + end + begin function (e, info) -> match e with + | NoEquationFound -> Hook.get forward_setoid_symmetry_in id + | e -> Proofview.tclZERO ~info e + end) end let intros_symmetry = @@ -4939,25 +4951,26 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make () (* This is probably not very useful any longer *) let prove_transitivity hdcncl eq_kind t = Proofview.Goal.enter begin fun gl -> - let (eq1,eq2) = match eq_kind with - | MonomorphicLeibnizEq (c1,c2) -> - mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]) - | PolymorphicLeibnizEq (typ,c1,c2) -> - mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |]) - | HeterogenousEq (typ1,c1,typ2,c2) -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let type_of = Typing.unsafe_type_of env sigma in - let typt = type_of t in - (mkApp(hdcncl, [| typ1; c1; typt ;t |]), - mkApp(hdcncl, [| typt; t; typ2; c2 |])) - in - Tacticals.New.tclTHENFIRST (cut eq2) - (Tacticals.New.tclTHENFIRST (cut eq1) - (Tacticals.New.tclTHENLIST - [ Tacticals.New.tclDO 2 intro; - Tacticals.New.onLastHyp simplest_case; - assumption ])) + let sigma = Tacmach.New.project gl in + let sigma, eq1, eq2 = match eq_kind with + | MonomorphicLeibnizEq (c1,c2) -> + sigma, mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]) + | PolymorphicLeibnizEq (typ,c1,c2) -> + sigma, mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |]) + | HeterogenousEq (typ1,c1,typ2,c2) -> + let env = Proofview.Goal.env gl in + let sigma, typt = Typing.type_of env sigma t in + sigma, + mkApp(hdcncl, [| typ1; c1; typt ;t |]), + mkApp(hdcncl, [| typt; t; typ2; c2 |]) + in + tclEVARSTHEN sigma + (Tacticals.New.tclTHENFIRST (cut eq2) + (Tacticals.New.tclTHENFIRST (cut eq1) + (Tacticals.New.tclTHENLIST + [ Tacticals.New.tclDO 2 intro; + Tacticals.New.onLastHyp simplest_case; + assumption ]))) end let transitivity_red allowred t = @@ -4965,9 +4978,8 @@ let transitivity_red allowred t = (* PL: usual transitivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) - let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - match_with_equation sigma concl >>= fun with_eqn -> + match_with_equation concl >>= fun with_eqn -> match with_eqn with | Some eq_data,_,_ -> Tacticals.New.tclTHEN diff --git a/test-suite/bugs/closed/bug_11515.v b/test-suite/bugs/closed/bug_11515.v new file mode 100644 index 0000000000..fe4ba87447 --- /dev/null +++ b/test-suite/bugs/closed/bug_11515.v @@ -0,0 +1,7 @@ +Require Import Ltac2.Ltac2. + +Lemma foo : + True. +Proof. + Fail rewrite _. +Abort. diff --git a/test-suite/bugs/closed/bug_11553.v b/test-suite/bugs/closed/bug_11553.v new file mode 100644 index 0000000000..a4a4353cd6 --- /dev/null +++ b/test-suite/bugs/closed/bug_11553.v @@ -0,0 +1,34 @@ +Definition var := nat. +Module Import A. +Class Rename (term : Type) := rename : (var -> var) -> term -> term. +End A. + +Inductive tm : Type := + (* | tv : vl_ -> tm *) + with vl_ : Type := + | var_vl : var -> vl_. + +Definition vl := vl_. + +Fixpoint tm_rename (sb : var -> var) (t : tm) : tm := + let b := vl_rename : Rename vl in + match t with + end +with +vl_rename (sb : var -> var) v : vl := + let a := tm_rename : Rename tm in + let b := vl_rename : Rename vl in + match v with + | var_vl x => var_vl (sb x) + end. + +Instance rename_vl : Rename vl := vl_rename. + +Lemma foo ξ x: rename_vl ξ (var_vl x) = var_vl x. +(* Succeeds *) +cbn. Abort. + +Lemma foo ξ x: rename ξ (var_vl x) = var_vl x. +(* Fails *) +cbn. +Abort. diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index c142d28ebe..0a989646cf 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -61,3 +61,18 @@ H : a = 0 -> forall a : nat, a = 0 ============================ a = 0 +File "stdin", line 101, characters 47-48: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 105, characters 36-37: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 106, characters 34-35: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 112, characters 22-23: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 112, characters 30-31: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v index 7f3b332d7d..610fa48c0c 100644 --- a/test-suite/output/Naming.v +++ b/test-suite/output/Naming.v @@ -90,3 +90,25 @@ apply H with (a:=a). (* test compliance with printing *) Abort. End A. + +Module B. + +(* Check valid/invalid implicit arguments *) +Definition f1 {x} (y:forall {x}, x=0) := x+0. +Definition f2 := (((fun x => 0):forall {x:nat}, nat), 0). +Definition f3 := fun {x} (y:forall {x}, x=0) => x+0. + +Definition g1 {x} := match x with true => fun {x:bool} => x | false => fun x:bool => x end. +(* TODO: do not ignore the implicit here *) +Definition g2 '(x,y) {z} := x+y+z. + +Definition h1 := fun x:nat => (fun {x} => x) 0. +Definition h2 := let g := forall {y}, y=0 in g. + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope. + +Definition l1 := ∀ {x:nat} {y:nat}, x=0. + +End B. diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index aeebc0f98b..839df99ea7 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -219,8 +219,8 @@ Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0. Module G. Generalizable Variables A R. Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x. -Check exists_true `{Reflexive A R}, forall x, R x x. -Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z. +Check exists_true `(Reflexive A R), forall x, R x x. +Check exists_true x `(Reflexive A R) y, x+y=0 -> forall z, R z z. End G. (* Allows recursive patterns for binders to be associative on the left *) diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 43f88f42a5..f65696e464 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -4,11 +4,11 @@ Entry constr:myconstr is [ "6" RIGHTA [ ] | "5" RIGHTA - [ SELF; "+"; NEXT ] + [ SELF; "+"; NEXT ] | "4" RIGHTA - [ SELF; "*"; NEXT ] + [ SELF; "*"; NEXT ] | "3" RIGHTA - [ "<"; constr:operconstr LEVEL "10"; ">" ] ] + [ "<"; constr:operconstr LEVEL "10"; ">" ] ] [< b > + < b > * < 2 >] : nat diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v index de34e007d2..df729588f4 100644 --- a/test-suite/success/Generalization.v +++ b/test-suite/success/Generalization.v @@ -11,4 +11,10 @@ Admitted. Print a_eq_b. +Require Import Morphisms. +Class Equiv A := equiv : A -> A -> Prop. +Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv). + +Lemma vcons_proper A `[Equiv A] `[!Setoid A] (x : True) : True. +Admitted. diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index b16e4a1186..e68040e4d4 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -1,3 +1,15 @@ + +Axiom foo : forall (x y z t : nat), nat. + +Arguments foo {_} _ [z] t. +Check (foo 1). +Arguments foo {_} _ {z} {t}. +Fail Arguments foo {_} _ [z] {t}. +Check (foo 1). + +Definition foo1 [m] n := n + m. +Check (foo1 1). + Inductive vector {A : Type} : nat -> Type := | vnil : vector 0 | vcons : A -> forall {n'}, vector n' -> vector (S n'). @@ -33,3 +45,11 @@ Abort. Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A. Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P. + +Inductive A' {P:forall m [n], n=m -> Prop} := C' : P 0 eq_refl -> A'. +Inductive A'' [P:forall m {n}, n=m -> Prop] (b : bool):= C'' : P 0 eq_refl -> A'' b. +Inductive A''' (P:forall m [n], n=m -> Prop) (b : bool):= C''' : P 0 eq_refl -> A''' P b. + +Definition F (id: forall [A] [x : A], A) := id. +Definition G := let id := (fun [A] (x : A) => x) in id. +Fail Definition G' := let id := (fun {A} (x : A) => x) in id. diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index ecaaedca53..668d765d83 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -114,9 +114,13 @@ Check h 0. Inductive I {A} (a:A) : forall {n:nat}, Prop := | C : I a (n:=0). +Inductive I' [A] (a:A) : forall [n:nat], n =0 -> Prop := + | C' : I' a eq_refl. + Inductive I2 (x:=0) : Prop := - | C2 {p:nat} : p = 0 -> I2. -Check C2 eq_refl. + | C2 {p:nat} : p = 0 -> I2 + | C2' [p:nat] : p = 0 -> I2. +Check C2' eq_refl. Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop := | C3 : I3 a (n:=0). @@ -147,6 +151,7 @@ Set Warnings "syntax". (* Miscellaneous tests *) Check let f := fun {x:nat} y => y=true in f false. +Check let f := fun [x:nat] y => y=true in f false. (* Isn't the name "arg_1" a bit fragile, here? *) @@ -157,3 +162,10 @@ Check fun f : forall {_:nat}, nat => f (arg_1:=0). Set Warnings "+syntax". Check id (fun x => let f c {a} (b:a=a) := b in f true (eq_refl 0)). Set Warnings "syntax". + + +Axiom eq0le0 : forall (n : nat) (x : n = 0), n <= 0. +Variable eq0le0' : forall (n : nat) {x : n = 0}, n <= 0. +Axiom eq0le0'' : forall (n : nat) {x : n = 0}, n <= 0. +Definition eq0le0''' : forall (n : nat) {x : n = 0}, n <= 0. Admitted. +Fail Axiom eq0le0'''' : forall [n : nat] {x : n = 0}, n <= 0. diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml index 561bd9c0c5..8a14be9ca7 100644 --- a/user-contrib/Ltac2/tac2tactics.ml +++ b/user-contrib/Ltac2/tac2tactics.ml @@ -33,6 +33,7 @@ let delayed_of_tactic tac env sigma = let _, pv = Proofview.init sigma [] in let name, poly = Id.of_string "ltac2_delayed", false in let c, pv, _, _ = Proofview.apply ~name ~poly env tac pv in + let _, sigma = Proofview.proofview pv in (sigma, c) let delayed_of_thunk r tac env sigma = diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index f954915cf8..6bdb3159cf 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -395,7 +395,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = in Proofview.Goal.enter begin fun gl -> - let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in + let type_of_pq = Tacmach.New.pf_get_type_of gl p in let sigma = Tacmach.New.project gl in let env = Tacmach.New.pf_env gl in let u,v = destruct_ind env sigma type_of_pq @@ -458,11 +458,11 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = match (l1,l2) with | (t1::q1,t2::q2) -> Proofview.Goal.enter begin fun gl -> - let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in let sigma = Tacmach.New.project gl in let env = Tacmach.New.pf_env gl in if EConstr.eq_constr sigma t1 t2 then aux q1 q2 else ( + let tt1 = Tacmach.New.pf_get_type_of gl t1 in let u,v = try destruct_ind env sigma tt1 (* trick so that the good sequence is returned*) with e when CErrors.noncritical e -> indu,[||] diff --git a/vernac/classes.ml b/vernac/classes.ml index 77bc4e4f8a..b92c9e9b71 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -510,7 +510,7 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri let interp_instance_context ~program_mode env ctx ~generalize pl tclass = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in let tclass = - if generalize then CAst.make @@ CGeneralization (Glob_term.Implicit, Some AbsPi, tclass) + if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass) else tclass in let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index 15077298aa..9d43debb77 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -228,7 +228,7 @@ let vernac_arguments ~section_local reference args more_implicits flags = let implicits = List.map (List.map snd) implicits in let implicits_specified = match implicits with - | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l + | [l] -> List.exists (function Glob_term.Explicit -> false | _ -> true) l | _ -> true in if implicits_specified && clear_implicits_flag then diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli index 71effddf67..cbc5fc15e2 100644 --- a/vernac/comArguments.mli +++ b/vernac/comArguments.mli @@ -12,6 +12,6 @@ val vernac_arguments : section_local:bool -> Libnames.qualid Constrexpr.or_by_notation -> Vernacexpr.vernac_argument_status list - -> (Names.Name.t * Impargs.implicit_kind) list list + -> (Names.Name.t * Glob_term.binding_kind) list list -> Vernacexpr.arguments_modifier list -> unit diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 625ffb5a06..d97bf6724c 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -270,7 +270,7 @@ let context ~poly l = | Some (Name id',_) -> Id.equal name id' | _ -> false in - let impl = Glob_term.(if List.exists test impls then Implicit else Explicit) in + let impl = Glob_term.(if List.exists test impls then MaxImplicit else Explicit) in (* ??? *) name,b,t,impl) ctx in diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index 56ab6f289d..2c582da495 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -198,10 +198,9 @@ let build_id_coercion idf_opt source poly = lams in (* juste pour verification *) - let _ = - if not - (Reductionops.is_conv_leq env sigma - (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f)) (EConstr.of_constr typ_f)) + let sigma, val_t = Typing.type_of env sigma (EConstr.of_constr val_f) in + let () = + if not (Reductionops.is_conv_leq env sigma val_t (EConstr.of_constr typ_f)) then user_err (strbrk "Cannot be defined as coercion (maybe a bad number of arguments).") diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index d48e2139d1..84f8578ad4 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -127,7 +127,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let sigma, (rel, _) = interp_constr_evars_impls ~program_mode:true env sigma r in - let relty = Typing.unsafe_type_of env sigma rel in + let relty = Retyping.get_type_of env sigma rel in let relargty = let error () = user_err ?loc:(constr_loc r) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 3302231fd1..d0374bc4fa 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -16,7 +16,6 @@ open Util open Names open Glob_term open Vernacexpr -open Impargs open Constrexpr open Constrexpr_ops open Extend @@ -817,7 +816,7 @@ GRAMMAR EXTEND Gram { let name, recarg_like, notation_scope = item in [RealArg { name=name; recarg_like=recarg_like; notation_scope=notation_scope; - implicit_status = NotImplicit}] } + implicit_status = Explicit}] } | "/" -> { [VolatileArg] } | "&" -> { [BidiArg] } | "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter -> @@ -827,7 +826,7 @@ GRAMMAR EXTEND Gram List.map (fun (name,recarg_like,notation_scope) -> RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; - implicit_status = NotImplicit}) items } + implicit_status = Explicit}) items } | "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x @@ -835,7 +834,7 @@ GRAMMAR EXTEND Gram List.map (fun (name,recarg_like,notation_scope) -> RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; - implicit_status = Implicit}) items } + implicit_status = NonMaxImplicit}) items } | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x @@ -843,16 +842,16 @@ GRAMMAR EXTEND Gram List.map (fun (name,recarg_like,notation_scope) -> RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; - implicit_status = MaximallyImplicit}) items } + implicit_status = MaxImplicit}) items } ] ]; (* Same as [argument_spec_block], but with only implicit status and names *) more_implicits_block: [ - [ name = name -> { [(name.CAst.v, NotImplicit)] } + [ name = name -> { [(name.CAst.v, Explicit)] } | "["; items = LIST1 name; "]" -> - { List.map (fun name -> (name.CAst.v, Impargs.Implicit)) items } + { List.map (fun name -> (name.CAst.v, NonMaxImplicit)) items } | "{"; items = LIST1 name; "}" -> - { List.map (fun name -> (name.CAst.v, MaximallyImplicit)) items } + { List.map (fun name -> (name.CAst.v, MaxImplicit)) items } ] ]; strategy_level: diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index a1bd99c237..82132a1af6 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1076,14 +1076,14 @@ let string_of_definition_object_kind = let open Decls in function let pr_br imp force x = let left,right = match imp with - | Impargs.Implicit -> str "[", str "]" - | Impargs.MaximallyImplicit -> str "{", str "}" - | Impargs.NotImplicit -> if force then str"(",str")" else mt(),mt() + | Glob_term.NonMaxImplicit -> str "[", str "]" + | Glob_term.MaxImplicit -> str "{", str "}" + | Glob_term.Explicit -> if force then str"(",str")" else mt(),mt() in left ++ x ++ right in let get_arguments_like s imp tl = - if s = None && imp = Impargs.NotImplicit then [], tl + if s = None && imp = Glob_term.Explicit then [], tl else let rec fold extra = function | RealArg arg :: tl when diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index c9ce2d77fd..32c438c724 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -258,18 +258,18 @@ let implicit_name_of_pos = function | Constrexpr.ExplByPos (n,k) -> Anonymous let implicit_kind_of_status = function - | None -> Anonymous, NotImplicit - | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then MaximallyImplicit else Implicit + | None -> Anonymous, Glob_term.Explicit + | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit let dummy = { - Vernacexpr.implicit_status = NotImplicit; + Vernacexpr.implicit_status = Glob_term.Explicit; name = Anonymous; recarg_like = false; notation_scope = None; } let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} = - name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit + name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit let rec main_implicits i renames recargs scopes impls = if renames = [] && recargs = [] && scopes = [] && impls = [] then [] @@ -281,8 +281,8 @@ let rec main_implicits i renames recargs scopes impls = let (name, implicit_status) = match renames, impls with | _, (Some _ as i) :: _ -> implicit_kind_of_status i - | name::_, _ -> (name,NotImplicit) - | [], (None::_ | []) -> (Anonymous, NotImplicit) + | name::_, _ -> (name,Glob_term.Explicit) + | [], (None::_ | []) -> (Anonymous, Glob_term.Explicit) in let notation_scope = match scopes with | scope :: _ -> Option.map CAst.make scope diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 60771e6ecf..fd588f5b15 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1571,7 +1571,7 @@ let query_command_selector ?loc = function let vernac_check_may_eval ~pstate ~atts redexp glopt rc = let glopt = query_command_selector glopt in let sigma, env = get_current_context_of_args ~pstate glopt in - let sigma, c = interp_open_constr env sigma rc in + let sigma, c = interp_open_constr ~expected_type:Pretyping.UnknownIfTermOrType env sigma rc in let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in Evarconv.check_problems_are_solved env sigma; let sigma = Evd.minimize_universes sigma in diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 1daa244986..22a8de7f99 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -254,7 +254,7 @@ type vernac_one_argument_status = { name : Name.t; recarg_like : bool; notation_scope : string CAst.t option; - implicit_status : Impargs.implicit_kind; + implicit_status : Glob_term.binding_kind; } type vernac_argument_status = @@ -386,7 +386,7 @@ type nonrec vernac_expr = | VernacArguments of qualid or_by_notation * vernac_argument_status list (* Main arguments status list *) * - (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) * + (Name.t * Glob_term.binding_kind) list list (* Extra implicit status lists *) * arguments_modifier list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option |