aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/subtac/subtac_coercion.ml44
-rw-r--r--contrib/subtac/subtac_command.ml52
-rw-r--r--contrib/subtac/subtac_utils.ml1
-rw-r--r--contrib/subtac/subtac_utils.mli1
-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
9 files changed, 113 insertions, 99 deletions
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 4b4a25e71..e0d779ca3 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -429,21 +429,22 @@ module Coercion = struct
Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
Termops.print_env env);
with _ -> ());
- 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
- try
- coerce_itf loc env isevars (Some cj.uj_val) cj.uj_type t
- with NoSubtacCoercion ->
- 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
+ try
+ coerce_itf loc env isevars (Some cj.uj_val) cj.uj_type t
+ with NoSubtacCoercion ->
+ 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)
let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) =
(try
@@ -453,20 +454,25 @@ module Coercion = struct
Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
Termops.print_env env);
with _ -> ());
+ let nabsinit, nabs =
+ match abs with
+ None -> 0, 0
+ | Some (init, cur) -> init, cur
+ in
let (rels, rng) =
(* a little more effort to get products is needed *)
- try decompose_prod_n abs t
+ try decompose_prod_n nabs t
with _ ->
trace (str "decompose_prod_n failed");
raise (Invalid_argument "Subtac_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 abs) rng then (
- trace (str "No occur between 0 and " ++ int (succ abs));
+ if noccur_with_meta 0 (succ (nabsinit - nabs)) rng then (
+ trace (str "No occur between 0 and " ++ int (succ (nabsinit - nabs)));
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 abs t'
+ env', rng, lift nabs t'
in
try
pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t'
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 94f2d70ac..1b92c6911 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -56,6 +56,7 @@ let interp_gen kind isevars env
c =
let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
let c' = Subtac_interp_fixpoint.rewrite_cases env c' in
+ msgnl (str "Pretyping " ++ my_print_constr_expr c);
let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
evar_nf isevars c'
@@ -69,9 +70,10 @@ let interp_casted_constr isevars env ?(impls=([],[])) c typ =
interp_gen (OfType (Some typ)) isevars env ~impls c
let interp_open_constr isevars env c =
- let c = SPretyping.pretype_gen isevars env ([], []) (OfType None)
- (Constrintern.intern_constr (Evd.evars_of !isevars) env c) in
- evar_nf isevars c
+ msgnl (str "Pretyping " ++ my_print_constr_expr c);
+ let c = Constrintern.intern_constr (Evd.evars_of !isevars) env c in
+ let c' = SPretyping.pretype_gen isevars env ([], []) (OfType None) c in
+ evar_nf isevars c'
let interp_constr_judgment isevars env c =
let j =
@@ -204,22 +206,22 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
Ppconstr.pr_constr_expr body)
in
let env', binders_rel = interp_context isevars env0 bl in
- let before, ((argname, _, argtyp) as arg), after = list_chop_hd n binders_rel in
+ let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in
let argid = match argname with Name n -> n | _ -> assert(false) in
let after' = List.map (fun (n, c, t) -> (n, option_app (lift 1) c, lift 1 t)) after in
let envwf = push_rel_context before env0 in
let wf_rel = interp_constr isevars envwf r in
let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in
- let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| wf_rel; mkRel 1 |])) in
+ let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| argtyp; wf_rel; mkRel 1 |])) in
let argid' = id_of_string (string_of_id argid ^ "'") in
let before_length, after_length = List.length before, List.length after in
let full_length = before_length + 1 + after_length in
- let wfarg = (Name argid, None,
- mkSubset (Name argid') argtyp
- (mkApp (wf_rel, [|mkRel 1; mkRel (full_length + 1)|])))
+ let wfarg len = (Name argid, None,
+ mkSubset (Name argid') argtyp
+ (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
in
- let new_bl = before @ (arg :: accarg :: after')
- and intern_bl = before @ (wfarg :: after)
+ let new_bl = after' @ (accarg :: arg :: before)
+ and intern_bl = after @ (wfarg (before_length + 1) :: before)
in
let intern_env = push_rel_context intern_bl env0 in
let env' = push_rel_context new_bl env0 in
@@ -227,7 +229,15 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
let intern_arity = it_mkProd_or_LetIn arity intern_bl in
let arity' = interp_type isevars env' arityc in
let arity' = it_mkProd_or_LetIn arity' new_bl in
- let fun_bl = before @ (arg :: (Name recname, None, arity) :: after') in
+ let fun_bl = after @ ((Name recname, None, intern_arity) :: arg :: before) in
+ let _ =
+ let pr c = my_print_constr env c in
+ let prr = Printer.pr_rel_context env in
+ trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++
+ str "Intern bl" ++ prr intern_bl ++ spc () ++
+ str "Extern bl" ++ prr new_bl ++ spc () ++
+ str "Intern arity: " ++ pr intern_arity)
+ in
let impl =
if Impargs.is_implicit_args()
then Impargs.compute_implicits intern_env arity'
@@ -256,11 +266,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
let def = abstract_constr_expr def bl in
isevars, info, interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
def arity
- | Some (n, artyp, wfrel, bl, intern_bl, intern_arity) ->
- let rec_sign = push_rel_context bl rec_sign in
+ | Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) ->
+ let rec_sign = push_rel_context fun_bl rec_sign in
let cstr = interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
def intern_arity
- in isevars, info, cstr)
+ in isevars, info, it_mkLambda_or_LetIn cstr fun_bl)
lnameargsardef arityl
with e ->
States.unfreeze fs; raise e in
@@ -328,19 +338,13 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
let evm = Evd.evars_of isevars in
let _, _, typ = arrec.(i) in
let id = namerec.(i) in
- let def =
- match info with
- Some (n, artyp, wfrel, funbl, bl, arity) ->
- def (* mkApp (def, *)
-
- | None -> def
- in
- (* Generalize by the recursive prototypes *)
+ let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in
+ (* Generalize by the recursive prototypes *)
let def =
Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign)
and typ =
- Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) in
- let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in
+ Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign)
+ in
(*let evars_typ = match evars_typ with Some t -> t | None -> assert(false) in*)
(*let fi = id_of_string (string_of_id id ^ "_evars") in*)
(*let ce =
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index d620c8e9f..6c165dada 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -74,6 +74,7 @@ let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)
open Pp
let my_print_constr = Termops.print_constr_env
+let my_print_constr_expr = Ppconstr.pr_constr_expr
let my_print_context = Termops.print_rel_context
let my_print_env = Termops.print_env
let my_print_rawconstr = Printer.pr_rawconstr_env
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index a53016484..92a995c89 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -47,6 +47,7 @@ val acc_inv : constr lazy_t
val extconstr : constr -> constr_expr
val extsort : sorts -> constr_expr
val my_print_constr : env -> constr -> std_ppcmds
+val my_print_constr_expr : constr_expr -> std_ppcmds
val my_print_evardefs : evar_defs -> std_ppcmds
val my_print_context : env -> std_ppcmds
val my_print_env : env -> std_ppcmds
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ec1246b74..4ad85af9a 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 841e6b034..b1b02ffd0 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 e9f605ecb..79e25a5af 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 7260b5ad3..8c5fe9c99 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 217a9714b..b3590492a 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.39.1) at 2024-07-05 22:51:52 +0000