aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/subtac/subtac_cases.ml2
-rw-r--r--plugins/subtac/subtac_coercion.ml60
-rw-r--r--plugins/subtac/subtac_pretyping.ml2
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml83
-rw-r--r--plugins/subtac/subtac_utils.ml2
-rw-r--r--plugins/subtac/subtac_utils.mli2
-rw-r--r--pretyping/cases.ml21
-rw-r--r--pretyping/coercion.ml84
-rw-r--r--pretyping/coercion.mli8
-rw-r--r--pretyping/evarutil.ml50
-rw-r--r--pretyping/evarutil.mli12
-rw-r--r--pretyping/pretyping.ml63
-rw-r--r--pretyping/unification.ml3
-rw-r--r--proofs/goal.ml3
-rw-r--r--theories/Vectors/Fin.v6
15 files changed, 169 insertions, 232 deletions
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 6893f1351..279e4d87a 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -413,7 +413,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) =
current
else
(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
- pb.isevars (make_judge current typ) (mk_tycon_type indt)).uj_val in
+ pb.isevars (make_judge current typ) indt).uj_val in
let sigma = !(pb.isevars) in
let typ = IsInd (indt,find_rectype pb.env sigma indt) in
((current,typ),deps))
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 3cbf9fcab..b55c43d82 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -409,9 +409,9 @@ module Coercion = struct
let inh_coerce_to_prod loc env isevars t =
let isevars = ref isevars in
- let typ = hnf env !isevars (snd t) in
+ let typ = hnf env !isevars t in
let _, typ' = mu env isevars typ in
- !isevars, (fst t, typ')
+ !isevars, typ'
let inh_coerce_to_fail env evd rigidonly v t c1 =
if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
@@ -462,50 +462,30 @@ module Coercion = struct
| _ -> raise NoCoercion
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
- let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) =
- match n with
- | None ->
- let cj = { cj with uj_type = hnf_nodelta env evd cj.uj_type }
- and t = hnf_nodelta env evd t in
- let (evd', val') =
- try
- inh_conv_coerce_to_fail loc env evd rigidonly
+ let inh_conv_coerce_to_gen rigidonly loc env evd cj t =
+ let cj = { cj with uj_type = hnf_nodelta env evd cj.uj_type }
+ and t = hnf_nodelta env evd t in
+ let (evd', val') =
+ try
+ inh_conv_coerce_to_fail loc env evd rigidonly
(Some cj.uj_val) cj.uj_type t
- with NoCoercion ->
+ with NoCoercion ->
(try
coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
with NoSubtacCoercion ->
error_actual_type_loc loc env evd cj t)
- in
- let val' = match val' with Some v -> v | None -> assert(false) in
- (evd',{ uj_val = val'; uj_type = t })
- | Some (init, cur) ->
- (evd, cj)
-
+ in
+ let val' = match val' with Some v -> v | None -> assert(false) in
+ (evd',{ uj_val = val'; uj_type = t })
+
let inh_conv_coerce_to = inh_conv_coerce_to_gen false
let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
- let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) =
- let nabsinit, nabs =
- match abs with
- None -> 0, 0
- | Some (init, cur) -> init, cur
- in
- try
- let rels, rng = Reductionops.splay_prod_n env ( isevars) nabs t in
- (* The final range free variables must have been replaced by evars, we accept only that evars
- in rng are applied to free vars. *)
- if noccur_with_meta 1 (succ nabs) rng then (
- let env', t, t' =
- let env' = push_rel_context rels env in
- env', rng, lift nabs t'
- in
- try
- fst (try inh_conv_coerce_to_fail loc env' isevars false None t t'
- with NoCoercion ->
- coerce_itf loc env' isevars None t t')
- with NoSubtacCoercion ->
- error_cannot_coerce env' isevars (t, t'))
- else isevars
- with _ -> isevars
+
+ let inh_conv_coerces_to loc env evd t t' =
+ try
+ fst (inh_conv_coerce_to_fail loc env evd true None t t')
+ with NoCoercion ->
+ evd (* Maybe not enough information to unify *)
+
end
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index c8acf7e0b..b83057ac8 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -126,7 +126,7 @@ let subtac_process ?(is_type=false) env isevars id bl c tycon =
in
let coqc, ctyp = interp env isevars c tycon in
let evm = non_instanciated_map env isevars !isevars in
- let ty = nf_evar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
+ let ty = nf_evar !isevars (match tycon with Some c -> c | _ -> ctyp) in
evm, coqc, ty, imps
open Subtac_obligations
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index fbeed381d..43182765d 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -177,13 +177,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
in
match tycon with
| None -> evd,(Anonymous,None,None)
- | Some (abs, c) ->
- (match abs with
- | None ->
- let evd', (n, dom, rng) = real_split evd c in
- evd', (n, mk_tycon dom, mk_tycon rng)
- | Some (init, cur) ->
- evd, (Anonymous, None, Some (Some (init, succ cur), c)))
+ | Some c ->
+ let evd', (n, dom, rng) = real_split evd c in
+ evd', (n, mk_tycon dom, mk_tycon rng)
(* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
@@ -222,8 +218,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| GHole (loc,k) ->
let ty =
match tycon with
- | Some (None, ty) -> ty
- | None | Some _ ->
+ | Some ty -> ty
+ | None ->
e_new_evar evdref env ~src:(loc, InternalHole) (Termops.new_Type ()) in
{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
@@ -312,43 +308,52 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
inh_conv_coerce_to_tycon loc env evdref s' tycon
| GApp (loc,f,args) ->
+ let fj = pretype empty_tycon env evdref lvar f in
+ let floc = loc_of_glob_constr f in
let length = List.length args in
- let ftycon =
- let ty =
- if length > 0 then
- match tycon with
- | None -> None
- | Some (None, ty) -> mk_abstr_tycon length ty
- | Some (Some (init, cur), ty) ->
- Some (Some (length + init, length + cur), ty)
- else tycon
- in
- match ty with
- | Some (_, t) ->
- if Subtac_coercion.disc_subset (whd_betadeltaiota env !evdref t) = None then ty
- else None
- | _ -> None
+ let candargs =
+ (* Bidirectional typechecking hint:
+ parameters of a constructor are completely determined
+ by a typing constraint *)
+ if length > 0 && isConstruct fj.uj_val then
+ match tycon with
+ | None -> []
+ | Some ty ->
+ let (ind, i) = destConstruct fj.uj_val in
+ let npars = inductive_nparams ind in
+ if npars = 0 then []
+ else
+ try
+ (* Does not treat partially applied constructors. *)
+ let IndType (indf, args) = find_rectype env !evdref ty in
+ let (ind',pars) = dest_ind_family indf in
+ if ind = ind' then pars
+ else (* Let the usual code throw an error *) []
+ with Not_found -> []
+ else []
in
- let fj = pretype ftycon env evdref lvar f in
- let floc = loc_of_glob_constr f in
- let rec apply_rec env n resj tycon = function
+ let rec apply_rec env n resj candargs = function
| [] -> resj
| c::rest ->
let argloc = loc_of_glob_constr c in
let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
let resty = whd_betadeltaiota env !evdref resj.uj_type in
match kind_of_term resty with
- | Prod (na,c1,c2) ->
- Option.iter (fun ty -> evdref :=
- Coercion.inh_conv_coerces_to loc env !evdref resty ty) tycon;
- let evd, (_, _, tycon) = split_tycon loc env !evdref tycon in
- evdref := evd;
- let hj = pretype (mk_tycon c1) env evdref lvar c in
- let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
- apply_rec env (n+1)
+ | Prod (na,c1,c2) ->
+ let hj = pretype (mk_tycon c1) env evdref lvar c in
+ let candargs, ujval =
+ match candargs with
+ | [] -> [], j_val hj
+ | arg :: args ->
+ if e_conv env evdref (j_val hj) arg then
+ args, nf_evar !evdref (j_val hj)
+ else [], j_val hj
+ in
+ let value, typ = applist (j_val resj, [ujval]), subst1 ujval c2 in
+ apply_rec env (n+1)
{ uj_val = value;
uj_type = typ }
- (Option.map (fun (abs, c) -> abs, c) tycon) rest
+ candargs rest
| _ ->
let hj = pretype empty_tycon env evdref lvar c in
@@ -356,7 +361,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(join_loc floc argloc) env !evdref
resj [hj]
in
- let resj = apply_rec env 1 fj ftycon args in
+ let resj = apply_rec env 1 fj candargs args in
let resj =
match kind_of_term (whd_evar !evdref resj.uj_val) with
| App (f,args) when isInd f or isConst f ->
@@ -503,8 +508,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
jtyp.uj_val, jtyp.uj_type
| None ->
let p = match tycon with
- | Some (None, ty) -> ty
- | None | Some _ ->
+ | Some ty -> ty
+ | None ->
e_new_evar evdref env ~src:(loc,InternalHole) (Termops.new_Type ())
in
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 0ed78a23b..cb1c9f8e1 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -114,7 +114,7 @@ let my_print_env = Termops.print_env
let my_print_glob_constr = Printer.pr_glob_constr_env
let my_print_evardefs = Evd.pr_evar_map None
-let my_print_tycon_type = Evarutil.pr_tycon_type
+let my_print_tycon = Evarutil.pr_tycon
let debug_level = 2
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index 70ad0bcc8..719b87952 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -70,7 +70,7 @@ val my_print_rel_context : env -> rel_context -> std_ppcmds
val my_print_named_context : env -> std_ppcmds
val my_print_env : env -> std_ppcmds
val my_print_glob_constr : env -> glob_constr -> std_ppcmds
-val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds
+val my_print_tycon : env -> type_constraint -> std_ppcmds
val debug : int -> std_ppcmds -> unit
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3ef14f7e1..2883df6d7 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -390,7 +390,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
current
else
(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
- pb.evdref (make_judge current typ) (mk_tycon_type indt)).uj_val in
+ pb.evdref (make_judge current typ) indt).uj_val in
let sigma = !(pb.evdref) in
(current,try_find_ind pb.env sigma indt names))
| _ -> (current,tmtyp)
@@ -1743,7 +1743,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
let preds =
match pred, tycon with
(* No type annotation *)
- | None, Some (None, t) when not (noccur_with_meta 0 max_int t) ->
+ | None, Some t when not (noccur_with_meta 0 max_int t) ->
(* If the tycon is not closed w.r.t real variables, we try *)
(* two different strategies *)
(* First strategy: we abstract the tycon wrt to the dependencies *)
@@ -1756,8 +1756,8 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
(* No dependent type constraint, or no constraints at all: *)
(* we use two strategies *)
let sigma,t = match tycon with
- | Some (None, t) -> sigma,t
- | _ -> new_type_evar sigma env ~src:(loc, CasesType) in
+ | Some t -> sigma,t
+ | None -> new_type_evar sigma env ~src:(loc, CasesType) in
(* First strategy: we build an "inversion" predicate *)
let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
(* Second strategy: we directly use the evar as a non dependent pred *)
@@ -1770,12 +1770,13 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
let sigma, newt = new_sort_variable sigma in
let evdref = ref sigma in
let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in
- let sigma = Option.cata (fun tycon ->
- let na = Name (id_of_string "x") in
- let tms = List.map (fun tm -> Pushed(tm,[],na)) tomatchs in
- let predinst = extract_predicate predcclj.uj_val tms in
- Coercion.inh_conv_coerces_to loc env !evdref predinst tycon)
- !evdref tycon in
+ let sigma = !evdref in
+ (* let sigma = Option.cata (fun tycon -> *)
+ (* let na = Name (id_of_string "x") in *)
+ (* let tms = List.map (fun tm -> Pushed(tm,[],na)) tomatchs in *)
+ (* let predinst = extract_predicate predcclj.uj_val tms in *)
+ (* Coercion.inh_conv_coerce_to loc env !evdref predinst tycon) *)
+ (* !evdref tycon in *)
let predccl = (j_nf_evar sigma predcclj).uj_val in
[sigma, predccl]
in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 0c340f9ed..eb014af46 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -54,22 +54,22 @@ module type S = sig
(* [inh_coerce_to_prod env evars t] coerces [t] to a product type *)
val inh_coerce_to_prod : loc ->
- env -> evar_map -> type_constraint_type -> evar_map * type_constraint_type
+ env -> evar_map -> types -> evar_map * types
(* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type
[t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
[j.uj_type] are convertible; it fails if no coercion is applicable *)
val inh_conv_coerce_to : loc ->
- env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
+ env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
val inh_conv_coerce_rigid_to : loc ->
- env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
+ env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
- (* [inh_conv_coerces_to loc env evd t t'] checks if an object of type [t]
+ (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
is coercible to an object of type [t'] adding evar constraints if needed;
it fails if no coercion exists *)
val inh_conv_coerces_to : loc ->
- env -> evar_map -> types -> type_constraint_type -> evar_map
+ env -> evar_map -> types -> types -> evar_map
(* [inh_pattern_coerce_to loc env evd pat ind1 ind2] coerces the Cases
pattern [pat] typed in [ind1] into a pattern typed in [ind2];
@@ -223,63 +223,27 @@ module Default = struct
| _ -> raise NoCoercion
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
- let inh_conv_coerce_to_gen rigidonly loc env evd cj (n, t) =
- match n with
- None ->
- let (evd', val') =
- try
- inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
- with NoCoercion ->
- let evd = saturate_evd env evd in
- try
- inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
- with NoCoercion ->
- error_actual_type_loc loc env evd cj t
- in
- let val' = match val' with Some v -> v | None -> assert(false) in
- (evd',{ uj_val = val'; uj_type = t })
- | Some (init, cur) -> (evd, cj)
+ let inh_conv_coerce_to_gen rigidonly loc env evd cj t =
+ let (evd', val') =
+ try
+ inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
+ with NoCoercion ->
+ let evd = saturate_evd env evd in
+ try
+ inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
+ with NoCoercion ->
+ error_actual_type_loc loc env evd cj t
+ in
+ let val' = match val' with Some v -> v | None -> assert(false) in
+ (evd',{ uj_val = val'; uj_type = t })
let inh_conv_coerce_to = inh_conv_coerce_to_gen false
let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
-
- let inh_conv_coerces_to loc env (evd : evar_map) t (abs, t') =
- if abs = None then
- try
- fst (inh_conv_coerce_to_fail loc env evd true None t t')
- with NoCoercion ->
- evd (* Maybe not enough information to unify *)
- else
- evd
- (* Still problematic, as it changes unification
- let nabsinit, nabs =
- match abs with
- None -> 0, 0
- | Some (init, cur) -> init, cur
- in
- try
- let (rels, rng) =
- (* a little more effort to get products is needed *)
- try decompose_prod_n nabs t
- with _ ->
- if !Flags.debug then
- msg_warning (str "decompose_prod_n failed");
- raise (Invalid_argument "Coercion.inh_conv_coerces_to")
- in
- (* The final range free variables must have been replaced by evars, we accept only that evars
- in rng are applied to free vars. *)
- if noccur_with_meta 0 (succ nabsinit) rng then (
- let env', t, t' =
- let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
- env', rng, lift nabs t'
- in
- try
- pi1 (inh_conv_coerce_to_fail loc env' evd None t t')
- with NoCoercion ->
- evd) (* Maybe not enough information to unify *)
- (*let sigma = evd in
- error_cannot_coerce env' sigma (t, t'))*)
- else evd
- with Invalid_argument _ -> evd *)
+ let inh_conv_coerces_to loc env evd t t' =
+ try
+ fst (inh_conv_coerce_to_fail loc env evd true None t t')
+ with NoCoercion ->
+ evd (* Maybe not enough information to unify *)
+
end
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index f312802a8..91cb693ab 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -39,22 +39,22 @@ module type S = sig
(** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
val inh_coerce_to_prod : loc ->
- env -> evar_map -> type_constraint_type -> evar_map * type_constraint_type
+ env -> evar_map -> types -> evar_map * types
(** [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type
[t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
[j.uj_type] are convertible; it fails if no coercion is applicable *)
val inh_conv_coerce_to : loc ->
- env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
+ env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
val inh_conv_coerce_rigid_to : loc ->
- env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
+ env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
(** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
is coercible to an object of type [t'] adding evar constraints if needed;
it fails if no coercion exists *)
val inh_conv_coerces_to : loc ->
- env -> evar_map -> types -> type_constraint_type -> evar_map
+ env -> evar_map -> types -> types -> evar_map
(** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
pattern [pat] typed in [ind1] into a pattern typed in [ind2];
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 5faa86cb0..8da127072 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1632,8 +1632,7 @@ open Glob_term
(* Operations on value/type constraints *)
-type type_constraint_type = (int * int) option * constr
-type type_constraint = type_constraint_type option
+type type_constraint = types option
type val_constraint = constr option
@@ -1654,14 +1653,8 @@ type val_constraint = constr option
(* The empty type constraint *)
let empty_tycon = None
-let mk_tycon_type c = (None, c)
-let mk_abstr_tycon_type n c = (Some (n, n), c) (* First component is initial abstraction, second
- is current abstraction *)
-
(* Builds a type constraint *)
-let mk_tycon ty = Some (mk_tycon_type ty)
-
-let mk_abstr_tycon n ty = Some (mk_abstr_tycon_type n ty)
+let mk_tycon ty = Some ty
(* Constrains the value of a type *)
let empty_valcon = None
@@ -1669,7 +1662,6 @@ let empty_valcon = None
(* Builds a value constraint *)
let mk_valcon c = Some c
-
let new_type_evar ?src ?filter evd env =
let evd', s = new_sort_variable evd in
new_evar evd' env ?src ?filter (mkSort s)
@@ -1765,10 +1757,6 @@ let judge_of_new_Type evd =
constraint on its domain and codomain. If the input constraint is
an evar instantiate it with the product of 2 new evars. *)
-let unlift_tycon init cur c =
- if cur = 1 then None, c
- else Some (init, pred cur), c
-
let split_tycon loc env evd tycon =
let rec real_split evd c =
let t = whd_betadeltaiota env evd c in
@@ -1785,35 +1773,13 @@ let split_tycon loc env evd tycon =
in
match tycon with
| None -> evd,(Anonymous,None,None)
- | Some (abs, c) ->
- (match abs with
- None ->
- let evd', (n, dom, rng) = real_split evd c in
- evd', (n, mk_tycon dom, mk_tycon rng)
- | Some (init, cur) ->
- evd, (Anonymous, None, Some (unlift_tycon init cur c)))
-
-let valcon_of_tycon x =
- match x with
- | Some (None, t) -> Some t
- | _ -> None
-
-let lift_abstr_tycon_type n (abs, t) =
- match abs with
- None -> raise (Invalid_argument "lift_abstr_tycon_type: not an abstraction")
- | Some (init, abs) ->
- let abs' = abs + n in
- if abs' < 0 then raise (Invalid_argument "lift_abstr_tycon_type")
- else (Some (init, abs'), t)
-
-let lift_tycon_type n (abs, t) = (abs, lift n t)
-let lift_tycon n = Option.map (lift_tycon_type n)
+ | Some c ->
+ let evd', (n, dom, rng) = real_split evd c in
+ evd', (n, mk_tycon dom, mk_tycon rng)
-let pr_tycon_type env (abs, t) =
- match abs with
- None -> Termops.print_constr_env env t
- | Some (init, cur) -> str "Abstract (" ++ int init ++ str "," ++ int cur ++ str ") " ++ Termops.print_constr_env env t
+let valcon_of_tycon x = x
+let lift_tycon n = Option.map (lift n)
let pr_tycon env = function
None -> str "None"
- | Some t -> pr_tycon_type env t
+ | Some t -> Termops.print_constr_env env t
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 82205c91f..fb0c481ef 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -146,16 +146,11 @@ val undefined_evars_of_evar_info : evar_map -> evar_info -> Intset.t
val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment
-type type_constraint_type = (int * int) option * constr
-type type_constraint = type_constraint_type option
-
+type type_constraint = types option
type val_constraint = constr option
val empty_tycon : type_constraint
-val mk_tycon_type : constr -> type_constraint_type
-val mk_abstr_tycon_type : int -> constr -> type_constraint_type
val mk_tycon : constr -> type_constraint
-val mk_abstr_tycon : int -> constr -> type_constraint
val empty_valcon : val_constraint
val mk_valcon : constr -> val_constraint
@@ -164,10 +159,6 @@ val split_tycon :
evar_map * (name * type_constraint * type_constraint)
val valcon_of_tycon : type_constraint -> val_constraint
-
-val lift_abstr_tycon_type : int -> type_constraint_type -> type_constraint_type
-
-val lift_tycon_type : int -> type_constraint_type -> type_constraint_type
val lift_tycon : int -> type_constraint -> type_constraint
(***********************************************************)
@@ -202,7 +193,6 @@ val expand_vars_in_term : env -> constr -> constr
(** {6 debug pretty-printer:} *)
-val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds
val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b1419c47b..4f286efe7 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -219,6 +219,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
(* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
let allow_anonymous_refs = ref false
+ let program_mode = ref false
+
let evd_comb0 f evdref =
let (evd',x) = f !evdref in
evdref := evd';
@@ -355,16 +357,16 @@ module Pretyping_F (Coercion : Coercion.S) = struct
| GPatVar (loc,(someta,n)) ->
let ty =
match tycon with
- | Some (None, ty) -> ty
- | None | Some _ -> new_type_evar evdref env loc in
+ | Some ty -> ty
+ | None -> new_type_evar evdref env loc in
let k = MatchingVar (someta,n) in
{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
| GHole (loc,k) ->
let ty =
match tycon with
- | Some (None, ty) -> ty
- | None | Some _ ->
+ | Some ty -> ty
+ | None ->
new_type_evar evdref env loc in
{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
@@ -438,27 +440,58 @@ module Pretyping_F (Coercion : Coercion.S) = struct
| GApp (loc,f,args) ->
let fj = pretype empty_tycon env evdref lvar f in
let floc = loc_of_glob_constr f in
- let rec apply_rec env n resj = function
+ let length = List.length args in
+ let candargs =
+ (* Bidirectional typechecking hint:
+ parameters of a constructor are completely determined
+ by a typing constraint *)
+ if !program_mode && length > 0 && isConstruct fj.uj_val then
+ match tycon with
+ | None -> []
+ | Some ty ->
+ let (ind, i) = destConstruct fj.uj_val in
+ let npars = inductive_nparams ind in
+ if npars = 0 then []
+ else
+ try
+ (* Does not treat partially applied constructors. *)
+ let IndType (indf, args) = find_rectype env !evdref ty in
+ let (ind',pars) = dest_ind_family indf in
+ if ind = ind' then pars
+ else (* Let the usual code throw an error *) []
+ with Not_found -> []
+ else []
+ in
+ let rec apply_rec env n resj candargs = function
| [] -> resj
| c::rest ->
let argloc = loc_of_glob_constr c in
let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
let resty = whd_betadeltaiota env !evdref resj.uj_type in
match kind_of_term resty with
- | Prod (na,c1,c2) ->
- let hj = pretype (mk_tycon c1) env evdref lvar c in
- let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
- apply_rec env (n+1)
- { uj_val = value;
- uj_type = typ }
- rest
+ | Prod (na,c1,c2) ->
+ let hj = pretype (mk_tycon c1) env evdref lvar c in
+ let candargs, ujval =
+ match candargs with
+ | [] -> [], j_val hj
+ | arg :: args ->
+ if e_conv env evdref (j_val hj) arg then
+ args, nf_evar !evdref (j_val hj)
+ else [], j_val hj
+ in
+ let value, typ = applist (j_val resj, [ujval]), subst1 ujval c2 in
+ apply_rec env (n+1)
+ { uj_val = value;
+ uj_type = typ }
+ candargs rest
+
| _ ->
let hj = pretype empty_tycon env evdref lvar c in
error_cant_apply_not_functional_loc
(join_loc floc argloc) env !evdref
resj [hj]
in
- let resj = apply_rec env 1 fj args in
+ let resj = apply_rec env 1 fj candargs args in
let resj =
match evar_kind_of_term !evdref resj.uj_val with
| App (f,args) ->
@@ -612,8 +645,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
pred, typ
| None ->
let p = match tycon with
- | Some (None, ty) -> ty
- | None | Some _ -> new_type_evar evdref env loc
+ | Some ty -> ty
+ | None -> new_type_evar evdref env loc
in
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
let pred = nf_evar !evdref pred in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 48a2c8c42..be6d90a26 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -795,8 +795,7 @@ let try_to_coerce env evd c cty tycon =
(evd',j'.uj_val)
let w_coerce_to_type env evd c cty mvty =
- let evd,mvty = pose_all_metas_as_evars env evd mvty in
- let tycon = mk_tycon_type mvty in
+ let evd,tycon = pose_all_metas_as_evars env evd mvty in
try try_to_coerce env evd c cty tycon
with e when precatchable_exception e ->
(* inh_conv_coerce_rigid_to should have reasoned modulo reduction
diff --git a/proofs/goal.ml b/proofs/goal.ml
index f0ab31c5b..4d65b636c 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -153,9 +153,8 @@ module Refinable = struct
and add the new evars to it. *)
let my_type = Retyping.get_type_of env !rdefs t in
let j = Environ.make_judge t my_type in
- let tycon = Evarutil.mk_tycon_type typ in
let (new_defs,j') =
- Coercion.Default.inh_conv_coerce_to (Pp.dummy_loc) env !rdefs j tycon
+ Coercion.Default.inh_conv_coerce_to (Pp.dummy_loc) env !rdefs j typ
in
rdefs := new_defs;
j'.Environ.uj_val
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index a5e37f34b..717139a0a 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -78,8 +78,8 @@ end.
(** [to_nat f] = p iff [f] is the p{^ th} element of [fin m]. *)
Fixpoint to_nat {m} (n : t m) : {i | i < m} :=
- match n in t k return {i | i< k} with
- |F1 j => exist (fun i => i< S j) 0 (Lt.lt_0_Sn j)
+ match n with
+ |F1 j => exist _ 0 (Lt.lt_0_Sn j)
|FS _ p => match to_nat p with |exist i P => exist _ (S i) (Lt.lt_n_S _ _ P) end
end.
@@ -87,7 +87,7 @@ Fixpoint to_nat {m} (n : t m) : {i | i < m} :=
p >= n else *)
Fixpoint of_nat (p n : nat) : (t n) + { exists m, p = n + m } :=
match n with
- |0 => inright _ (ex_intro (fun x => p = 0 + x) p (@eq_refl _ p))
+ |0 => inright _ (ex_intro _ p eq_refl)
|S n' => match p with
|0 => inleft _ (F1)
|S p' => match of_nat p' n' with
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 08:51:48 +0000