aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml6
-rw-r--r--pretyping/coercion.ml33
-rw-r--r--pretyping/evarutil.ml40
-rw-r--r--pretyping/evarutil.mli2
-rw-r--r--pretyping/pretyping.ml33
5 files changed, 58 insertions, 56 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ec1246b745..4ad85af9a8 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -352,7 +352,7 @@ let find_tomatch_tycon isevars env loc = function
| Some (_,ind,_),_
(* Otherwise try to get constraints from (the 1st) constructor in clauses *)
| None, Some (_,(ind,_)) ->
- Some (0, inductive_template isevars env loc ind)
+ mk_tycon (inductive_template isevars env loc ind)
| None, None ->
empty_tycon
@@ -412,7 +412,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) (0, indt)).uj_val in
+ pb.isevars (make_judge current typ) (mk_tycon_type indt)).uj_val in
let sigma = Evd.evars_of !(pb.isevars) in
let typ = IsInd (indt,find_rectype pb.env sigma indt) in
((current,typ),deps))
@@ -1663,7 +1663,7 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
(* No type annotation *)
| None ->
(match tycon with
- | Some (0, t) ->
+ | Some (None, t) ->
let names,pred =
prepare_predicate_from_tycon loc false env isevars tomatchs t
in Some (build_initial_predicate false names pred)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 841e6b0347..b1b02ffd01 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -160,13 +160,6 @@ module Default = struct
with Reduction.NotConvertible -> raise NoCoercion
open Pp
let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
-(* (try *)
-(* msgnl (str "inh_conv_coerces_to_fail called for " ++ *)
-(* Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
-(* Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++ *)
-(* Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
-(* Termops.print_env env); *)
-(* with _ -> ()); *)
try (the_conv_x_leq env t c1 isevars, v, t)
with Reduction.NotConvertible ->
(try
@@ -225,18 +218,20 @@ module Default = struct
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
let inh_conv_coerce_to loc env isevars cj (n, t) =
- if n = 0 then
- let (evd', val', type') =
- try
- inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
- with NoCoercion ->
- let sigma = evars_of isevars in
- error_actual_type_loc loc env sigma cj t
- in
- let val' = match val' with Some v -> v | None -> assert(false) in
- (evd',{ uj_val = val'; uj_type = t })
- else
- (isevars, cj)
+ match n with
+ None ->
+ let (evd', val', type') =
+ try
+ inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
+ with NoCoercion ->
+ let sigma = evars_of isevars in
+ error_actual_type_loc loc env sigma 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) -> (isevars, cj)
+
+
open Pp
let inh_conv_coerces_to loc env isevars t (abs, t') = isevars
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index e9f605ecb5..79e25a5afc 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -556,7 +556,7 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
(* Operations on value/type constraints *)
-type type_constraint_type = int * constr
+type type_constraint_type = (int * int) option * constr
type type_constraint = type_constraint_type option
type val_constraint = constr option
@@ -578,8 +578,9 @@ type val_constraint = constr option
(* The empty type constraint *)
let empty_tycon = None
-let mk_tycon_type c = (0, c)
-let mk_abstr_tycon_type n c = (n, c)
+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)
@@ -651,28 +652,35 @@ let split_tycon loc env isevars tycon =
match tycon with
| None -> isevars,(Anonymous,None,None)
| Some (abs, c) ->
- if abs = 0 then real_split c
- else if abs = 1 then
- isevars, (Anonymous, None, mk_tycon c)
- else
- isevars, (Anonymous, None, Some (pred abs, c))
+ (match abs with
+ None -> real_split c
+ | Some (init, cur) ->
+ if cur = 1 then isevars, (Anonymous, None,
+ Some (Some (init, 0), c))
+ else
+ isevars, (Anonymous, None, Some (Some (init, pred cur), c)))
let valcon_of_tycon x =
match x with
- | Some (0, t) -> Some t
+ | Some (None, t) -> Some t
| _ -> None
-let lift_tycon_type n (abs, c) =
- let abs' = abs + n in
- if abs' < 0 then raise (Invalid_argument "lift_tycon_type")
- else (abs', c)
+let lift_tycon_type n (abs, t) =
+ abs, lift n t
+(* match abs with
+ None -> (abs, lift n t)
+ | Some (init, abs) ->
+ let abs' = abs + n in
+ if abs' < 0 then raise (Invalid_argument "lift_tycon_type")
+ else (Some (init, abs'), lift n t)*)
let lift_tycon n = option_app (lift_tycon_type n)
let pr_tycon_type env (abs, t) =
- if abs = 0 then Termops.print_constr_env env t
- else str "Abstract " ++ int abs ++ str " " ++ Termops.print_constr_env env 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 pr_tycon env = function
None -> str "None"
| Some t -> pr_tycon_type env t
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 7260b5ad35..8c5fe9c99b 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -87,7 +87,7 @@ val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
val judge_of_new_Type : unit -> unsafe_judgment
-type type_constraint_type = int * constr
+type type_constraint_type = (int * int) option * constr
type type_constraint = type_constraint_type option
type val_constraint = constr option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 217a9714be..b3590492ab 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -259,14 +259,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
(* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
(* in environment [env], with existential variables [(evars_of isevars)] and *)
(* the type constraint tycon *)
- let rec pretype (tycon : type_constraint) env isevars lvar c =
-(* (try
- msgnl (str "pretype with tycon: " ++
- Evarutil.pr_tycon env tycon ++ str " with evars: " ++ spc () ++
- Evd.pr_evar_defs !isevars ++ str " in env: " ++ spc () ++
- Termops.print_env env);
- with _ -> ());*)
- match c with
+ let rec pretype (tycon : type_constraint) env isevars lvar = function
| RRef (loc,ref) ->
inh_conv_coerce_to_tycon loc env isevars
(pretype_ref isevars env ref)
@@ -294,7 +287,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
| RHole (loc,k) ->
let ty =
match tycon with
- | Some (n, ty) when n = 0 -> ty
+ | Some (None, ty) -> ty
| None | Some _ ->
e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in
{ uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }
@@ -357,9 +350,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let ftycon =
match tycon with
None -> None
- | Some (n, ty) ->
- if n = 0 then mk_abstr_tycon length ty
- else Some (n + length, ty)
+ | Some (None, ty) -> mk_abstr_tycon length ty
+ | Some (Some (init, cur), ty) ->
+ Some (Some (length + init, cur), ty)
in
let fj = pretype ftycon env isevars lvar f in
let floc = loc_of_rawconstr f in
@@ -375,11 +368,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
let typ' = nf_isevar !isevars typ in
let tycon =
- match tycon with
+ match tycon with
Some (abs, ty) ->
- isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
- (abs, ty);
- Some (pred abs, nf_isevar !isevars ty)
+ (match abs with
+ None ->
+ isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
+ (abs, ty);
+ Some (None, nf_isevar !isevars ty)
+ | Some (init, cur) ->
+ isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
+ (abs, ty);
+ Some (Some (init, pred cur), nf_isevar !isevars ty))
| None -> None
in
apply_rec env (n+1)
@@ -532,7 +531,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
jtyp.uj_val, jtyp.uj_type
| None ->
let p = match tycon with
- | Some (n, ty) when n = 0 -> ty
+ | Some (None, ty) -> ty
| None | Some _ ->
e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-13 05:45:04 +0000