diff options
Diffstat (limited to 'pretyping')
69 files changed, 297 insertions, 231 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 3b3de33d8e..47916ffb79 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index 6d1b6eefd4..f1c84cb63b 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index d7a6c4c832..20dec96ef4 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -824,7 +824,7 @@ let push_alias_eqn sigma alias eqn = (**********************************************************************) (* Functions to deal with elimination predicate *) -(* Infering the predicate *) +(* Inferring the predicate *) (* The problem to solve is the following: @@ -1455,7 +1455,7 @@ let compile ~program_mode sigma pb = (* Building the sub-problem when all patterns are variables. Case - where [current] is an intially pushed term. *) + where [current] is an initially pushed term. *) and shift_problem ((current,t),_,na) sigma pb = let ty = type_of_tomatch t in let tomatch = lift_tomatch_stack 1 pb.tomatch in @@ -1542,7 +1542,7 @@ let compile ~program_mode sigma pb = mat = List.map drop_alias_eqn pb.mat } in compile sigma pb in - (* If the "match" was orginally over a variable, as in "match x with + (* If the "match" was originally over a variable, as in "match x with O => true | n => n end", we give preference to non-expansion in the default clause (i.e. "match x with O => true | n => n end" rather than "match x with O => true | S p => S p end"; @@ -2067,7 +2067,7 @@ let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign ty let p2 = prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs arsign t in (* Third strategy: we take the type constraint as it is; of course we could *) - (* need something inbetween, abstracting some but not all of the dependencies *) + (* need something in between, abstracting some but not all of the dependencies *) (* the "inversion" strategy deals with that but unification may not be *) (* powerful enough so strategy 2 and 3 helps; moreover, inverting does not *) (* work (yet) when a constructor has a type not precise enough for the inversion *) diff --git a/pretyping/cases.mli b/pretyping/cases.mli index b0349a3d05..59cb1ca4ab 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 5ea9b79336..43b94aed3d 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -477,7 +477,7 @@ and cbv_stack_value info env = function cbv_stack_value info env (CONSTR(c, [||]), stack_app args stk) | Some v -> cbv_stack_value info env (v,stk) | None -> mkSTACK(PRIMITIVE(op,c,args), stk) - else (* partical application *) + else (* partial application *) (assert (stk = TOP); PRIMITIVE(op,c,appl)) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index d6c2ad146e..16c4364f17 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 90ce1cc594..f5fffc4c1c 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -441,7 +441,7 @@ let coercion_of_reference r = module CoercionPrinting = struct type t = coe_typ - let compare = GlobRef.Ordered.compare + module Set = GlobRef.Set let encode _env = coercion_of_reference let subst = subst_coe_typ let printer x = Nametab.pr_global_env Id.Set.empty x diff --git a/pretyping/classops.mli b/pretyping/classops.mli index c04182930e..9c5274286e 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 8c9b6550f3..3c71871968 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 43d4059785..0dc8208786 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 6bfbb9a9c0..415b9ec6df 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index d19789ef42..88001bba6e 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 82726eccf0..0daf1ab531 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -182,7 +182,7 @@ module PrintingInductiveMake = end) -> struct type t = inductive - let compare = ind_ord + module Set = Indset let encode = Test.encode let subst subst obj = subst_ind subst obj let printer ind = Nametab.pr_global_env Id.Set.empty (IndRef ind) @@ -688,20 +688,21 @@ let hack_qualid_of_univ_level sigma l = let detype_universe sigma u = let fn (l, n) = - let qid = hack_qualid_of_univ_level sigma l in - Some (qid, n) - in + let s = + if Univ.Level.is_prop l then GProp else + if Univ.Level.is_set l then GSet else + GType (hack_qualid_of_univ_level sigma l) in + (s, n) in Univ.Universe.map fn u let detype_sort sigma = function - | SProp -> GSProp - | Prop -> GProp - | Set -> GSet + | SProp -> UNamed [GSProp,0] + | Prop -> UNamed [GProp,0] + | Set -> UNamed [GSet,0] | Type u -> - GType (if !print_universes - then detype_universe sigma u - else []) + then UNamed (detype_universe sigma u) + else UAnonymous {rigid=true}) type binder_kind = BProd | BLambda | BLetIn @@ -710,7 +711,7 @@ type binder_kind = BProd | BLambda | BLetIn let detype_level sigma l = let l = hack_qualid_of_univ_level sigma l in - GType (UNamed l) + UNamed (GType l) let detype_instance sigma l = let l = EInstance.kind sigma l in diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 00b0578a52..cc9f520583 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -91,7 +91,7 @@ module PrintingInductiveMake : end) -> sig type t = Names.inductive - val compare : t -> t -> int + module Set = Indset val encode : Environ.env -> Libnames.qualid -> Names.inductive val subst : substitution -> t -> t val printer : t -> Pp.t diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6b149a8b41..edc948eb65 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index eae961714d..e1dd0a0cdc 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -34,7 +34,7 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error ([unify_delay]) and another that tries to solve such remaining constraints using heuristics ([unify]). *) -(** Theses functions allow to pass arbitrary flags to the unifier and can delay constraints. +(** These functions allow to pass arbitrary flags to the unifier and can delay constraints. In case the flags are not specified, they default to [default_flags_of TransparentState.full] currently. diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index a51cb22c20..705ab56703 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index 8ff113196b..3dc3e45068 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4a941a68b1..769079dea7 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -284,9 +284,9 @@ let noccur_evar env evd evk c = in try occur_rec false (0,env) c; true with Occur -> false -(***************************************) -(* Managing chains of local definitons *) -(***************************************) +(****************************************) +(* Managing chains of local definitions *) +(****************************************) type alias = | RelAlias of int @@ -629,7 +629,7 @@ let solve_pattern_eqn env sigma l c = * If a variable and an alias of it are bound to the same instance, we skip * the alias (we just use eq_constr -- instead of conv --, since anyway, * only instances that are variables -- or evars -- are later considered; - * morever, we can bet that similar instances came at some time from + * moreover, we can bet that similar instances came at some time from * the very same substitution. The removal of aliased duplicates is * useful to ensure the uniqueness of a projection. *) @@ -1738,7 +1738,7 @@ let reconsider_unif_constraints unify flags evd = * Returns an optional list of evars that were instantiated, or None * if the problem couldn't be solved. *) -(* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) +(* Rq: incomplete algorithm if pbty = CONV_X_LEQ ! *) let solve_simple_eqn unify flags ?(choose=false) ?(imitate_defs=true) env evd (pbty,(evk1,args1 as ev1),t2) = try diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index ebf8230bbd..9d5d75d9ba 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 7019cdf046..9db37bfa9b 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index 9ba63b4f52..3ad69e6e50 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/geninterp.ml b/pretyping/geninterp.ml index 32152ad0e4..b9128aa107 100644 --- a/pretyping/geninterp.ml +++ b/pretyping/geninterp.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli index 49d874289d..088f97271b 100644 --- a/pretyping/geninterp.mli +++ b/pretyping/geninterp.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index e76eb2a7de..d49a39b547 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index cdd36bbba6..a49ac80f47 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -40,7 +40,7 @@ type t val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t -(** Export the underlying environement *) +(** Export the underlying environment *) val env : t -> env diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 85b9faac77..ea94305dd8 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -45,20 +45,27 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) = let comp2 = f ty in (na,k,comp1,comp2) +let glob_sort_name_eq g1 g2 = match g1, g2 with + | GSProp, GSProp + | GProp, GProp + | GSet, GSet -> true + | GType u1, GType u2 -> Libnames.qualid_eq u1 u2 + | (GSProp|GProp|GSet|GType _), _ -> false -let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with -| GSProp, GSProp -| GProp, GProp -| GSet, GSet -> true -| GType l1, GType l2 -> - List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n)) l1 l2 -| (GSProp|GProp|GSet|GType _), _ -> false +exception ComplexSort let glob_sort_family = let open Sorts in function -| GSProp -> InSProp -| GProp -> InProp -| GSet -> InSet -| GType _ -> InType + | UAnonymous {rigid=true} -> InType + | UNamed [GSProp,0] -> InProp + | UNamed [GProp,0] -> InProp + | UNamed [GSet,0] -> InSet + | _ -> raise ComplexSort + +let glob_sort_eq u1 u2 = match u1, u2 with + | UAnonymous {rigid=r1}, UAnonymous {rigid=r2} -> r1 = r2 + | UNamed l1, UNamed l2 -> + List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n) l1 l2 + | (UNamed _ | UAnonymous _), _ -> false let binding_kind_eq bk1 bk2 = match bk1, bk2 with | Decl_kinds.Explicit, Decl_kinds.Explicit -> true diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index df902a8fa7..467b72e520 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -15,10 +15,13 @@ open Glob_term val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool -val glob_sort_family : 'a glob_sort_gen -> Sorts.family - val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool +(** Expect a Prop/SProp/Set/Type universe; raise [ComplexSort] if + contains a max, an increment, or a flexible universe *) +exception ComplexSort +val glob_sort_family : glob_sort -> Sorts.family + val alias_of_pat : 'a cases_pattern_g -> Name.t val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 02cb294f6d..7c859a5332 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -23,23 +23,23 @@ type existential_name = Id.t (** Sorts *) -type 'a glob_sort_gen = +type glob_sort_name = | GSProp (** representation of [SProp] literal *) - | GProp (** representation of [Prop] literal *) - | GSet (** representation of [Set] literal *) - | GType of 'a (** representation of [Type] literal *) + | GProp (** representation of [Prop] level *) + | GSet (** representation of [Set] level *) + | GType of Libnames.qualid (** representation of a [Type] level *) -type 'a universe_kind = - | UAnonymous - | UUnknown +type 'a glob_sort_expr = + | UAnonymous of { rigid : bool } (** not rigid = unifiable by minimization *) | UNamed of 'a -type level_info = Libnames.qualid universe_kind -type glob_level = level_info glob_sort_gen -type glob_constraint = glob_level * Univ.constraint_type * glob_level +(** levels, occurring in universe instances *) +type glob_level = glob_sort_name glob_sort_expr -type sort_info = (Libnames.qualid * int) option list -type glob_sort = sort_info glob_sort_gen +(** sort expressions *) +type glob_sort = (glob_sort_name * int) list glob_sort_expr + +type glob_constraint = glob_sort_name * Univ.constraint_type * glob_sort_name type glob_recarg = int option diff --git a/pretyping/heads.ml b/pretyping/heads.ml index ef27ca9b4e..d65faecd19 100644 --- a/pretyping/heads.ml +++ b/pretyping/heads.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/heads.mli b/pretyping/heads.mli index e5f9967590..bb096a846e 100644 --- a/pretyping/heads.mli +++ b/pretyping/heads.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 7615a17514..e25ebad380 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -84,7 +84,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let () = if Option.is_empty projs then check_privacy_block mib in let () = - if not (Sorts.List.mem kind (elim_sorts specif)) then + if not (Sorts.family_leq kind (elim_sort specif)) then raise (RecursionSchemeError (env, NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family kind), pind))) @@ -557,8 +557,8 @@ let weaken_sort_scheme env evd set sort npars term ty = let check_arities env listdepkind = let _ = List.fold_left (fun ln (((_,ni as mind),u),mibi,mipi,dep,kind) -> - let kelim = elim_sorts (mibi,mipi) in - if not (Sorts.List.mem kind kelim) then raise + let kelim = elim_sort (mibi,mipi) in + if not (Sorts.family_leq kind kelim) then raise (RecursionSchemeError (env, NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family kind),(mind,u)))) else if Int.List.mem ni ln then raise diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 8eb571a8be..ae23fc4ee6 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index b1c98da2c7..36b405e981 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -255,10 +255,13 @@ let inductive_has_local_defs env ind = let l2 = mib.mind_nparams + mip.mind_nrealargs in not (Int.equal l1 l2) -let allowed_sorts env (kn,i as ind) = +let top_allowed_sort env (kn,i as ind) = let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_kelim +let sorts_below top = + List.filter (fun s -> Sorts.family_leq s top) Sorts.[InSProp;InProp;InSet;InType] + let has_dependent_elim mib = match mib.mind_record with | PrimRecord _ -> mib.mind_finite == BiFinite diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index cfc650938e..55eb74cacf 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -141,7 +141,9 @@ val constructor_nrealdecls_env : env -> constructor -> int val constructor_has_local_defs : env -> constructor -> bool val inductive_has_local_defs : env -> inductive -> bool -val allowed_sorts : env -> inductive -> Sorts.family list +val sorts_below : Sorts.family -> Sorts.family list + +val top_allowed_sort : env -> inductive -> Sorts.family (** (Co)Inductive records with primitive projections do not have eta-conversion, hence no dependent elimination. *) diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index 9f2397ec38..ed069eace0 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli index 6e5bf30f6b..a234e334d1 100644 --- a/pretyping/inferCumulativity.mli +++ b/pretyping/inferCumulativity.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/locus.ml b/pretyping/locus.ml index 087a6b9174..afb4cc708a 100644 --- a/pretyping/locus.ml +++ b/pretyping/locus.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index aaa4ce684d..02c8f6a2a8 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index ac15fe1018..195dbec935 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 0fcd6a9e9d..0c639b4328 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index 4997d0bf0d..02de034fcb 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index d1c0a4ea2a..e0beb383b5 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index c788efda48..3600f1761b 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -410,7 +410,9 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function PLetIn (na, pat_of_raw metas vars c1, Option.map (pat_of_raw metas vars) t, pat_of_raw metas (na::vars) c2) - | GSort gs -> PSort (Glob_ops.glob_sort_family gs) + | GSort gs -> + (try PSort (Glob_ops.glob_sort_family gs) + with Glob_ops.ComplexSort -> user_err ?loc (str "Unexpected universe in pattern.")) | GHole _ -> PMeta None | GCast (c,_) -> diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 3821fbf1a0..304e06818e 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 35a7036af4..c1b05014c0 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index a9e2b0ea8f..af2d75a19d 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -107,7 +107,7 @@ val error_ill_typed_rec_body : val error_elim_arity : ?loc:Loc.t -> env -> Evd.evar_map -> pinductive -> constr -> - unsafe_judgment -> (Sorts.family list * Sorts.family * Sorts.family * arity_error) option -> 'b + unsafe_judgment -> (Sorts.family * Sorts.family * Sorts.family * arity_error) option -> 'b val error_not_a_type : ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f2b8671a48..280b6f9dae 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -52,6 +52,18 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint let (!!) env = GlobEnv.env env +let bidi_hints = + Summary.ref (GlobRef.Map.empty : int GlobRef.Map.t) ~name:"bidirectionalityhints" + +let add_bidirectionality_hint gr n = + bidi_hints := GlobRef.Map.add gr n !bidi_hints + +let get_bidirectionality_hint gr = + GlobRef.Map.find_opt gr !bidi_hints + +let clear_bidirectionality_hint gr = + bidi_hints := GlobRef.Map.remove gr !bidi_hints + (************************************************************************) (* This concerns Cases *) open Inductive @@ -120,7 +132,7 @@ let is_strict_universe_declarations = (** Miscellaneous interpretation functions *) -let interp_known_universe_level evd qid = +let interp_known_universe_level_name evd qid = try let open Libnames in if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid @@ -130,7 +142,7 @@ let interp_known_universe_level evd qid = Univ.Level.make qid let interp_universe_level_name ~anon_rigidity evd qid = - try evd, interp_known_universe_level evd qid + try evd, interp_known_universe_level_name evd qid with Not_found -> if Libnames.qualid_is_ident qid then (* Undeclared *) let id = Libnames.qualid_basename qid in @@ -152,44 +164,31 @@ let interp_universe_level_name ~anon_rigidity evd qid = with UGraph.AlreadyDeclared -> evd in evd, level -let interp_universe ?loc evd = function - | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in - evd, Univ.Universe.make l - | l -> - List.fold_left (fun (evd, u) l -> - let evd', u' = - match l with - | Some (l,n) -> - (* [univ_flexible_alg] can produce algebraic universes in terms *) - let anon_rigidity = univ_flexible in - let evd', l = interp_universe_level_name ~anon_rigidity evd l in - let u' = Univ.Universe.make l in - (match n with - | 0 -> evd', u' - | 1 -> evd', Univ.Universe.super u' - | _ -> - user_err ?loc ~hdr:"interp_universe" - (Pp.(str "Cannot interpret universe increment +" ++ int n))) - | None -> - let evd, l = new_univ_level_variable ?loc univ_flexible evd in - evd, Univ.Universe.make l +let interp_universe_name ?loc evd l = + (* [univ_flexible_alg] can produce algebraic universes in terms *) + let anon_rigidity = univ_flexible in + let evd', l = interp_universe_level_name ~anon_rigidity evd l in + evd', l + +let interp_sort_name ?loc sigma = function + | GSProp -> sigma, Univ.Level.sprop + | GProp -> sigma, Univ.Level.prop + | GSet -> sigma, Univ.Level.set + | GType l -> interp_universe_name ?loc sigma l + +let interp_sort_info ?loc evd l = + List.fold_left (fun (evd, u) (l,n) -> + let evd', u' = interp_sort_name ?loc evd l in + let u' = Univ.Universe.make u' in + let u' = match n with + | 0 -> u' + | 1 -> Univ.Universe.super u' + | n -> + user_err ?loc ~hdr:"interp_universe" + (Pp.(str "Cannot interpret universe increment +" ++ int n)) in (evd', Univ.sup u u')) (evd, Univ.Universe.type0m) l -let interp_known_level_info ?loc evd = function - | UUnknown | UAnonymous -> - user_err ?loc ~hdr:"interp_known_level_info" - (str "Anonymous universes not allowed here.") - | UNamed qid -> - try interp_known_universe_level evd qid - with Not_found -> - user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid) - -let interp_level_info ?loc evd : level_info -> _ = function - | UUnknown -> new_univ_level_variable ?loc univ_rigid evd - | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd - | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s - type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr type inference_flags = { @@ -403,13 +402,14 @@ let interp_known_glob_level ?loc evd = function | GSProp -> Univ.Level.sprop | GProp -> Univ.Level.prop | GSet -> Univ.Level.set - | GType s -> interp_known_level_info ?loc evd s + | GType qid -> + try interp_known_universe_level_name evd qid + with Not_found -> + user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid) let interp_glob_level ?loc evd : glob_level -> _ = function - | GSProp -> evd, Univ.Level.sprop - | GProp -> evd, Univ.Level.prop - | GSet -> evd, Univ.Level.set - | GType s -> interp_level_info ?loc evd s + | UAnonymous {rigid} -> new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd + | UNamed s -> interp_sort_name ?loc evd s let interp_instance ?loc evd l = let evd, l' = @@ -448,18 +448,26 @@ let pretype_ref ?loc sigma env ref us = let ty = unsafe_type_of !!env sigma c in sigma, make_judge c ty -let judge_of_Type ?loc evd s = - let evd, s = interp_universe ?loc evd s in +let interp_sort ?loc evd : glob_sort -> _ = function + | UAnonymous {rigid} -> + let evd, l = new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd in + evd, Univ.Universe.make l + | UNamed l -> interp_sort_info ?loc evd l + +let judge_of_sort ?loc evd s = let judge = { uj_val = mkType s; uj_type = mkType (Univ.super s) } in evd, judge -let pretype_sort ?loc sigma = function - | GSProp -> sigma, judge_of_sprop - | GProp -> sigma, judge_of_prop - | GSet -> sigma, judge_of_set - | GType s -> judge_of_Type ?loc sigma s +let pretype_sort ?loc sigma s = + match s with + | UNamed [GSProp,0] -> sigma, judge_of_sprop + | UNamed [GProp,0] -> sigma, judge_of_prop + | UNamed [GSet,0] -> sigma, judge_of_set + | _ -> + let sigma, s = interp_sort ?loc sigma s in + judge_of_sort ?loc sigma s let new_type_evar env sigma loc = new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole) @@ -635,24 +643,36 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : let sigma, fj = pretype empty_tycon env sigma f in let floc = loc_of_glob_constr f in let length = List.length args in + let nargs_before_bidi = + (* if `f` is a global, we retrieve bidirectionality hints *) + try + let (gr,_) = destRef sigma fj.uj_val in + Option.default length @@ GlobRef.Map.find_opt gr !bidi_hints + with DestKO -> + length + in let candargs = - (* Bidirectional typechecking hint: - parameters of a constructor are completely determined - by a typing constraint *) + (* Bidirectional typechecking hint: + parameters of a constructor are completely determined + by a typing constraint *) + (* This bidirectionality machinery is the one of `Program` for + constructors and is orthogonal to bidirectionality hints. However, we + could probably factorize both by providing default bidirectionality hints + for constructors corresponding to their number of parameters. *) if program_mode && length > 0 && isConstruct sigma fj.uj_val then - match tycon with - | None -> [] - | Some ty -> + match tycon with + | None -> [] + | Some ty -> let ((ind, i), u) = destConstruct sigma fj.uj_val in let npars = inductive_nparams !!env ind in - if Int.equal npars 0 then [] - else - try - let IndType (indf, args) = find_rectype !!env sigma ty in - let ((ind',u'),pars) = dest_ind_family indf in - if eq_ind ind ind' then List.map EConstr.of_constr pars - else (* Let the usual code throw an error *) [] - with Not_found -> [] + if Int.equal npars 0 then [] + else + try + let IndType (indf, args) = find_rectype !!env sigma ty in + let ((ind',u'),pars) = dest_ind_family indf in + if eq_ind ind ind' then List.map EConstr.of_constr pars + else (* Let the usual code throw an error *) [] + with Not_found -> [] else [] in let app_f = @@ -662,20 +682,29 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : let p = Projection.make p false in let npars = Projection.npars p in fun n -> - if n == npars + 1 then fun _ v -> mkProj (p, v) + if Int.equal n npars then fun _ v -> mkProj (p, v) else fun f v -> applist (f, [v]) | _ -> fun _ f v -> applist (f, [v]) in - let rec apply_rec env sigma n resj candargs = function - | [] -> sigma, resj + let rec apply_rec env sigma n resj candargs bidiargs = function + | [] -> sigma, resj, List.rev bidiargs | c::rest -> + let bidi = n >= nargs_before_bidi in let argloc = loc_of_glob_constr c in let sigma, resj = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in let resty = whd_all !!env sigma resj.uj_type in match EConstr.kind sigma resty with | Prod (na,c1,c2) -> let tycon = Some c1 in - let sigma, hj = pretype tycon env sigma c in + let (sigma, hj), bidiargs = + if bidi && Option.has_some tycon then + (* We want to get some typing information from the context before + typing the argument, so we replace it by an existential + variable *) + let sigma, c_hole = new_evar env sigma ~src:(loc,Evar_kinds.InternalHole) c1 in + (sigma, make_judge c_hole c1), (c_hole, c) :: bidiargs + else pretype tycon env sigma c, bidiargs + in let sigma, candargs, ujval = match candargs with | [] -> sigma, [], j_val hj @@ -687,30 +716,45 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : sigma, args, nf_evar sigma (j_val hj) end in - let sigma, ujval = adjust_evar_source sigma na.binder_name ujval in - let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in - let j = { uj_val = value; uj_type = typ } in - apply_rec env sigma (n+1) j candargs rest - | _ -> - let sigma, hj = pretype empty_tycon env sigma c in - error_cant_apply_not_functional - ?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|] + let sigma, ujval = adjust_evar_source sigma na.binder_name ujval in + let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in + let j = { uj_val = value; uj_type = typ } in + apply_rec env sigma (n+1) j candargs bidiargs rest + | _ -> + let sigma, hj = pretype empty_tycon env sigma c in + error_cant_apply_not_functional + ?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|] in - let sigma, resj = apply_rec env sigma 1 fj candargs args in + let sigma, resj, bidiargs = apply_rec env sigma 0 fj candargs [] args in let sigma, resj = match EConstr.kind sigma resj.uj_val with | App (f,args) -> - if Termops.is_template_polymorphic_ind !!env sigma f then - (* Special case for inductive type applications that must be - refreshed right away. *) - let c = mkApp (f, args) in - let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in - let t = Retyping.get_type_of !!env sigma c in - sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t - else sigma, resj + if Termops.is_template_polymorphic_ind !!env sigma f then + (* Special case for inductive type applications that must be + refreshed right away. *) + let c = mkApp (f, args) in + let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in + let t = Retyping.get_type_of !!env sigma c in + sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t + else sigma, resj | _ -> sigma, resj in - inh_conv_coerce_to_tycon ?loc env sigma resj tycon + let sigma, t = inh_conv_coerce_to_tycon ?loc env sigma resj tycon in + let refine_arg sigma (newarg,origarg) = + (* Refine an argument (originally `origarg`) represented by an evar + (`newarg`) to use typing information from the context *) + (* Recover the expected type of the argument *) + let ty = Retyping.get_type_of !!env sigma newarg in + (* Type the argument using this expected type *) + let sigma, j = pretype (Some ty) env sigma origarg in + (* Unify the (possibly refined) existential variable with the + (typechecked) original value *) + Evarconv.unify_delay !!env sigma newarg (j_val j) + in + (* We now refine any arguments whose typing was delayed for + bidirectionality *) + let sigma = List.fold_left refine_arg sigma bidiargs in + (sigma, t) | GLambda(name,bk,c1,c2) -> let sigma, tycon' = diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 1037cf6cc5..f9da568c75 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -14,14 +14,24 @@ into elementary ones, insertion of coercions and resolution of implicit arguments. *) +open Names open Environ open Evd open EConstr open Glob_term open Ltac_pretype +val add_bidirectionality_hint : GlobRef.t -> int -> unit +(** A bidirectionality hint `n` for a global `g` tells the pretyper to use + typing information from the context after typing the `n` for arguments of an + application of `g`. *) + +val get_bidirectionality_hint : GlobRef.t -> int option + +val clear_bidirectionality_hint : GlobRef.t -> unit + val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> - glob_level -> Univ.Level.t + glob_sort_name -> Univ.Level.t (** An auxiliary function for searching for fixpoint guard indexes *) diff --git a/pretyping/program.ml b/pretyping/program.ml index 7e38c09189..a15e66f329 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/program.mli b/pretyping/program.mli index a8f5115788..6604b3a854 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -11,7 +11,7 @@ open Names open EConstr -(** A bunch of Coq constants used by Progam *) +(** A bunch of Coq constants used by Program *) val sig_typ : unit -> GlobRef.t val sig_intro : unit -> GlobRef.t diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index a23c58c062..1b70119f20 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 25b6cd0751..3f64c06a2d 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 85e6f51387..d8f01c6bb5 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -886,7 +886,7 @@ module CredNative = RedNative(CNativeEntries) (** Generic reduction function with environment Here is where unfolded constant are stored in order to be - eventualy refolded. + eventually refolded. If tactic_mode is true, it uses ReductionBehaviour, prefers refold constant instead of value and tries to infer constants @@ -1315,7 +1315,7 @@ let whd_allnolet_stack env = let whd_allnolet env = red_of_state_red (whd_allnolet_state env) -(* 4. Ad-hoc eta reduction, does not subsitute evars *) +(* 4. Ad-hoc eta reduction, does not substitute evars *) let shrink_eta c = Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty)) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index aa39921ea2..e72f5f2793 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 38e254a5b4..cc341afac3 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 252bfb1a84..68a88df194 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 231219c9de..6646dfb80c 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 0887d0efd3..c05a6cde18 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index ee27aea93f..1d3e77452f 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -62,7 +62,7 @@ type typeclass = { (* Context of definitions and properties on defs, will not be shared *) cl_props : Constr.rel_context; - (* The method implementaions as projections. *) + (* The method implementations as projections. *) cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index e42b82c51f..787c722938 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index af5b3016c9..a335ba8b0b 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -8,13 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(*i*) open Names open EConstr open Environ -(*i*) - -type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index fd75781ed5..3b58b4a16e 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -12,8 +12,6 @@ open Names open EConstr open Environ -type contexts = Parameters | Properties - type typeclass_error = | NotAClass of constr | UnboundMethod of GlobRef.t * lident (** Class name, method *) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index be71f44a5e..2db5512ff4 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -117,12 +117,12 @@ let check_branch_types env sigma (ind,u) cj (lfj,explft) = sigma lfj explft let max_sort l = - if Sorts.List.mem InType l then InType else - if Sorts.List.mem InSet l then InSet else InProp + if List.mem_f Sorts.family_equal InType l then InType else + if List.mem_f Sorts.family_equal InSet l then InSet else InProp let is_correct_arity env sigma c pj ind specif params = let arsign = make_arity_signature env sigma true (make_ind_family (ind,params)) in - let allowed_sorts = elim_sorts specif in + let allowed_sorts = sorts_below (elim_sort specif) in let error () = Pretype_errors.error_elim_arity env sigma ind c pj None in let rec srec env sigma pt ar = let pt' = whd_all env sigma pt in @@ -135,7 +135,7 @@ let is_correct_arity env sigma c pj ind specif params = end | Sort s, [] -> let s = ESorts.kind sigma s in - if not (Sorts.List.mem (Sorts.family s) allowed_sorts) + if not (List.mem_f Sorts.family_equal (Sorts.family s) allowed_sorts) then error () else sigma, s | Evar (ev,_), [] -> @@ -199,13 +199,13 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj = (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let specif = lookup_mind_specif env (fst ind) in - let sorts = elim_sorts specif in + let sorts = elim_sort specif in let pj = Retyping.get_judgment_of env sigma p in let _, s = splay_prod env sigma pj.uj_type in let ksort = match EConstr.kind sigma s with | Sort s -> Sorts.family (ESorts.kind sigma s) | _ -> error_elim_arity env sigma ind c pj None in - if not (List.exists ((==) ksort) sorts) then + if not (Sorts.family_leq ksort sorts) then let s = inductive_sort_family (snd specif) in error_elim_arity env sigma ind c pj (Some(sorts,ksort,s,Type_errors.error_elim_explain ksort s)) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index f68820429b..63fb0679f1 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index d134c7319f..00831b5962 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -1219,12 +1219,12 @@ let merge_instances env sigma flags st1 st2 c1 c2 = * bindings. This may or may not close off all RHSs of * the EVARs. For each EVAR whose RHS is closed off, * we can just apply it, and go on. For each which - * is not closed off, we need to do a mimick step - + * is not closed off, we need to do a mimic step - * in general, we have something like: * * ?X == (c e1 e2 ... ei[Meta(k)] ... en) * - * so we need to do a mimick step, converting ?X + * so we need to do a mimic step, converting ?X * into * * ?X -> (c ?z1 ... ?zn) @@ -1247,7 +1247,7 @@ let merge_instances env sigma flags st1 st2 c1 c2 = * we can reverse the equation, put it into our metavar * substitution, and keep going. * - * The most efficient mimick possible is, for each + * The most efficient mimic possible is, for each * Meta-var remaining in the term, to declare a * new EVAR of the same type. This is supposedly * determinable from the clausale form context - diff --git a/pretyping/unification.mli b/pretyping/unification.mli index a45b8f1dd8..0ee71246d8 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 1fe6545ce4..da0a92f284 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli index 3e0eabb013..07f1696032 100644 --- a/pretyping/vnorm.mli +++ b/pretyping/vnorm.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) |