aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-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
4 files changed, 55 insertions, 43 deletions
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 4b4a25e718..e0d779ca38 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 94f2d70ac4..1b92c69110 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 d620c8e9fa..6c165dada1 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 a53016484b..92a995c891 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 08:41:44 +0000