summaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml33
-rw-r--r--pretyping/classops.ml6
-rw-r--r--pretyping/constr_matching.ml74
-rw-r--r--pretyping/detyping.ml11
-rw-r--r--pretyping/evarconv.ml26
-rw-r--r--pretyping/evarsolve.ml163
-rw-r--r--pretyping/evarutil.ml13
-rw-r--r--pretyping/evarutil.mli10
-rw-r--r--pretyping/evd.ml55
-rw-r--r--pretyping/evd.mli14
-rw-r--r--pretyping/find_subterm.ml1
-rw-r--r--pretyping/find_subterm.mli1
-rw-r--r--pretyping/glob_ops.mli3
-rw-r--r--pretyping/inductiveops.ml21
-rw-r--r--pretyping/inductiveops.mli10
-rw-r--r--pretyping/patternops.ml52
-rw-r--r--pretyping/patternops.mli3
-rw-r--r--pretyping/pretyping.ml10
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--pretyping/reductionops.ml52
-rw-r--r--pretyping/reductionops.mli7
-rw-r--r--pretyping/retyping.ml5
-rw-r--r--pretyping/tacred.ml14
-rw-r--r--pretyping/termops.ml1
-rw-r--r--pretyping/termops.mli1
-rw-r--r--pretyping/typeclasses.ml11
-rw-r--r--pretyping/typeclasses.mli2
-rw-r--r--pretyping/typeclasses_errors.ml1
-rw-r--r--pretyping/typeclasses_errors.mli1
-rw-r--r--pretyping/typing.mli1
-rw-r--r--pretyping/unification.ml13
-rw-r--r--pretyping/vnorm.ml17
32 files changed, 355 insertions, 279 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fdb19d37..fcbe90b6 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -285,11 +285,13 @@ let inductive_template evdref env tmloc ind =
applist (mkIndU indu,List.rev evarl)
let try_find_ind env sigma typ realnames =
- let (IndType(_,realargs) as ind) = find_rectype env sigma typ in
+ let (IndType(indf,realargs) as ind) = find_rectype env sigma typ in
let names =
match realnames with
| Some names -> names
- | None -> List.make (List.length realargs) Anonymous in
+ | None ->
+ let ind = fst (fst (dest_ind_family indf)) in
+ List.make (inductive_nrealdecls ind) Anonymous in
IsInd (typ,ind,names)
let inh_coerce_to_ind evdref env loc ty tyi =
@@ -730,7 +732,17 @@ let set_declaration_name x (_,c,t) = (x,c,t)
let recover_initial_subpattern_names = List.map2 set_declaration_name
-let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t))
+let recover_and_adjust_alias_names names sign =
+ let rec aux = function
+ | [],[] ->
+ []
+ | x::names, (_,None,t)::sign ->
+ (x,(alias_of_pat x,None,t)) :: aux (names,sign)
+ | names, (na,(Some _ as c),t)::sign ->
+ (PatVar (Loc.ghost,na),(na,c,t)) :: aux (names,sign)
+ | _ -> assert false
+ in
+ List.split (aux (names,sign))
let push_rels_eqn sign eqn =
{eqn with
@@ -1644,7 +1656,7 @@ let abstract_tycon loc env evdref subst tycon extenv t =
in
aux (0,extenv,subst0) t0
-let build_tycon loc env tycon_env subst tycon extenv evdref t =
+let build_tycon loc env tycon_env s subst tycon extenv evdref t =
let t,tt = match t with
| None ->
(* This is the situation we are building a return predicate and
@@ -1659,6 +1671,8 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t =
let evd,tt = Typing.e_type_of extenv !evdref t in
evdref := evd;
(t,tt) in
+ let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
+ if not b then anomaly (Pp.str "Build_tycon: should be a type");
{ uj_val = t; uj_type = tt }
(* For a multiple pattern-matching problem Xi on t1..tn with return
@@ -1693,11 +1707,12 @@ let build_inversion_problem loc env sigma tms t =
let pat,acc = make_patvar t acc in
let indf' = lift_inductive_family n indf in
let sign = make_arity_signature env true indf' in
- let sign = recover_alias_names alias_of_pat (pat :: List.rev patl) sign in
- let p = List.length realargs in
+ let patl = pat :: List.rev patl in
+ let patl,sign = recover_and_adjust_alias_names patl sign in
+ let p = List.length patl in
let env' = push_rel_context sign env in
- let patl',acc_sign,acc = aux (n+p+1) env' (sign@acc_sign) tms acc in
- patl@pat::patl',acc_sign,acc
+ let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in
+ List.rev_append patl patl',acc_sign,acc
| (t, NotInd (bo,typ)) :: tms ->
let pat,acc = make_patvar t acc in
let d = (alias_of_pat pat,None,typ) in
@@ -1780,7 +1795,7 @@ let build_inversion_problem loc env sigma tms t =
mat = [eqn1;eqn2];
caseloc = loc;
casestyle = RegularStyle;
- typing_function = build_tycon loc env pb_env subst} in
+ typing_function = build_tycon loc env pb_env s subst} in
let pred = (compile pb).uj_val in
(!evdref,pred)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 559f5fe6..055996de 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -60,9 +60,9 @@ let coe_info_typ_equal c1 c2 =
let cl_typ_ord t1 t2 = match t1, t2 with
| CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
- | CL_CONST c1, CL_CONST c2 -> con_user_ord c1 c2
- | CL_PROJ c1, CL_PROJ c2 -> con_user_ord c1 c2
- | CL_IND i1, CL_IND i2 -> ind_user_ord i1 i2
+ | CL_CONST c1, CL_CONST c2 -> con_ord c1 c2
+ | CL_PROJ c1, CL_PROJ c2 -> con_ord c1 c2
+ | CL_IND i1, CL_IND i2 -> ind_ord i1 i2
| _ -> Pervasives.compare t1 t2 (** OK *)
module ClTyp = struct
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index a6e2bc19..161cffa8 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -351,34 +351,45 @@ let authorized_occ env sigma partial_app closed pat c mk_ctx next =
else mkresult subst (mk_ctx (mkMeta special_meta)) next
with PatternMatchingFailure -> next ()
+let subargs env v = Array.map_to_list (fun c -> (env, c)) v
+
(* Tries to match a subterm of [c] with [pat] *)
let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
let rec aux env c mk_ctx next =
match kind_of_term c with
| Cast (c1,k,c2) ->
- let next_mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in
- let next () = try_aux [env] [c1] next_mk_ctx next in
+ let next_mk_ctx = function
+ | [c1] -> mk_ctx (mkCast (c1, k, c2))
+ | _ -> assert false
+ in
+ let next () = try_aux [env, c1] next_mk_ctx next in
authorized_occ env sigma partial_app closed pat c mk_ctx next
| Lambda (x,c1,c2) ->
- let next_mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in
+ let next_mk_ctx = function
+ | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2))
+ | _ -> assert false
+ in
let next () =
let env' = Environ.push_rel (x,None,c1) env in
- try_aux [env;env'] [c1; c2] next_mk_ctx next in
+ try_aux [(env, c1); (env', c2)] next_mk_ctx next in
authorized_occ env sigma partial_app closed pat c mk_ctx next
| Prod (x,c1,c2) ->
- let next_mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in
+ let next_mk_ctx = function
+ | [c1; c2] -> mk_ctx (mkProd (x, c1, c2))
+ | _ -> assert false
+ in
let next () =
let env' = Environ.push_rel (x,None,c1) env in
- try_aux [env;env'] [c1;c2] next_mk_ctx next in
+ try_aux [(env, c1); (env', c2)] next_mk_ctx next in
authorized_occ env sigma partial_app closed pat c mk_ctx next
| LetIn (x,c1,t,c2) ->
let next_mk_ctx = function
- | [c1;c2] -> mkLetIn (x,c1,t,c2)
+ | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2))
| _ -> assert false
in
let next () =
let env' = Environ.push_rel (x,Some c1,t) env in
- try_aux [env;env'] [c1;c2] next_mk_ctx next in
+ try_aux [(env, c1); (env', c2)] next_mk_ctx next in
authorized_occ env sigma partial_app closed pat c mk_ctx next
| App (c1,lc) ->
let next () =
@@ -390,14 +401,15 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
let mk_ctx = function
| [app';c] -> mk_ctx (mkApp (app',[|c|]))
| _ -> assert false in
- try_aux [env] [app;Array.last lc] mk_ctx next
+ try_aux [(env, app); (env, Array.last lc)] mk_ctx next
else
let rec aux2 app args next =
match args with
| [] ->
let mk_ctx le =
mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
- try_aux [env] (c1::Array.to_list lc) mk_ctx next
+ let sub = (env, c1) :: subargs env lc in
+ try_aux sub mk_ctx next
| arg :: args ->
let app = mkApp (app,[|arg|]) in
let next () = aux2 app args next in
@@ -407,7 +419,8 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
else
let mk_ctx le =
mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
- try_aux [env] (c1::Array.to_list lc) mk_ctx next
+ let sub = (env, c1) :: subargs env lc in
+ try_aux sub mk_ctx next
in
authorized_occ env sigma partial_app closed pat c mk_ctx next
| Case (ci,hd,c1,lc) ->
@@ -415,24 +428,24 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
| [] -> assert false
| c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
in
- let next () = try_aux [env] (c1 :: Array.to_list lc) next_mk_ctx next in
+ let sub = (env, c1) :: subargs env lc in
+ let next () = try_aux sub next_mk_ctx next in
authorized_occ env sigma partial_app closed pat c mk_ctx next
| Fix (indx,(names,types,bodies)) ->
let nb_fix = Array.length types in
let next_mk_ctx le =
let (ntypes,nbodies) = CList.chop nb_fix le in
mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in
- let next () =
- try_aux
- [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in
+ let sub = subargs env types @ subargs env bodies in
+ let next () = try_aux sub next_mk_ctx next in
authorized_occ env sigma partial_app closed pat c mk_ctx next
| CoFix (i,(names,types,bodies)) ->
let nb_fix = Array.length types in
let next_mk_ctx le =
let (ntypes,nbodies) = CList.chop nb_fix le in
mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in
- let next () =
- try_aux [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in
+ let sub = subargs env types @ subargs env bodies in
+ let next () = try_aux sub next_mk_ctx next in
authorized_occ env sigma partial_app closed pat c mk_ctx next
| Proj (p,c') ->
let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
@@ -441,27 +454,24 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
try
let term = Retyping.expand_projection env sigma p c' [] in
aux env term mk_ctx next
- with Retyping.RetypeError _ -> raise PatternMatchingFailure
+ with Retyping.RetypeError _ -> next ()
else
- try_aux [env] [c'] next_mk_ctx next in
+ try_aux [env, c'] next_mk_ctx next in
authorized_occ env sigma partial_app closed pat c mk_ctx next
| Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
authorized_occ env sigma partial_app closed pat c mk_ctx next
(* Tries [sub_match] for all terms in the list *)
- and try_aux lenv lc mk_ctx next =
- let rec try_sub_match_rec lacc lenv lc =
- match lenv, lc with
- | _, [] -> next ()
- | env :: tlenv, c::tl ->
- let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in
- let next () =
- let env' = match tlenv with [] -> lenv | _ -> tlenv in
- try_sub_match_rec (c::lacc) env' tl
- in
- aux env c mk_ctx next
- | _ -> assert false in
- try_sub_match_rec [] lenv lc in
+ and try_aux lc mk_ctx next =
+ let rec try_sub_match_rec lacc lc =
+ match lc with
+ | [] -> next ()
+ | (env, c) :: tl ->
+ let mk_ctx ce = mk_ctx (List.rev_append lacc (ce :: List.map snd tl)) in
+ let next () = try_sub_match_rec (c :: lacc) tl in
+ aux env c mk_ctx next
+ in
+ try_sub_match_rec [] lc in
let lempty () = IStream.Nil in
let result () = aux env c (fun x -> x) lempty in
IStream.thunk result
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 046ee0da..28fb8cbe 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -498,16 +498,17 @@ let rec detype flags avoid env sigma t =
else noparams ()
| Evar (evk,cl) ->
- let bound_to_itself id c =
+ let bound_to_itself_or_letin (id,b,_) c =
+ b != None ||
try let n = List.index Name.equal (Name id) (fst env) in
- isRelN n c
+ isRelN n c
with Not_found -> isVarId id c in
let id,l =
try
let id = Evd.evar_ident evk sigma in
- let l = Evd.evar_instance_array bound_to_itself (Evd.find sigma evk) cl in
- let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> (Id.Set.union fvs (collect_vars c), Int.Set.union rels (free_rels c))) (Id.Set.empty,Int.Set.empty) l in
- let l = Evd.evar_instance_array (fun id c -> not !print_evar_arguments && (bound_to_itself id c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
+ let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
+ let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
+ let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
id,l
with Not_found ->
Id.of_string ("X" ^ string_of_int (Evar.repr evk)),
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a95af253..f388f900 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -324,18 +324,25 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
Note: incomplete heuristic... *)
let ground_test =
if is_ground_term evd term1 && is_ground_term evd term2 then (
- let evd, b =
- try infer_conv ~pb:pbty ~ts:(fst ts) env evd term1 term2
- with Univ.UniverseInconsistency _ -> evd, false
+ let evd, e =
+ try
+ let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts)
+ env evd term1 term2
+ in
+ if b then evd, None
+ else evd, Some (ConversionFailed (env,term1,term2))
+ with Univ.UniverseInconsistency e -> evd, Some (UnifUnivInconsistency e)
in
- if b then Some (evd, true)
- else if is_ground_env evd env then Some (evd, false)
- else None)
+ match e with
+ | None -> Some (evd, e)
+ | Some e ->
+ if is_ground_env evd env then Some (evd, Some e)
+ else None)
else None
in
match ground_test with
- | Some (evd, true) -> Success evd
- | Some (evd, false) -> UnifFailure (evd,ConversionFailed (env,term1,term2))
+ | Some (evd, None) -> Success evd
+ | Some (evd, Some e) -> UnifFailure (evd,e)
| None ->
(* Until pattern-unification is used consistently, use nohdbeta to not
destroy beta-redexes that can be used for 1st-order unification *)
@@ -555,8 +562,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
| LetIn (na,b1,t1,c'1), LetIn (_,b2,t2,c'2) ->
let f1 i =
ise_and i
- [(fun i -> evar_conv_x ts env i CONV t1 t2);
- (fun i -> evar_conv_x ts env i CONV b1 b2);
+ [(fun i -> evar_conv_x ts env i CONV b1 b2);
(fun i ->
let b = nf_evar i b1 in
let t = nf_evar i t1 in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 5aa72c90..bfd19c6c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -64,30 +64,33 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
in
modified := true; evdref := evd; mkSort s'
| Prod (na,u,v) ->
- mkProd (na,u,refresh dir v)
+ mkProd (na,u,refresh dir v)
| _ -> t
(** Refresh the types of evars under template polymorphic references *)
- and refresh_term_evars onevars t =
+ and refresh_term_evars onevars top t =
match kind_of_term t with
| App (f, args) when is_template_polymorphic env f ->
let pos = get_polymorphic_positions f in
refresh_polymorphic_positions args pos
+ | App (f, args) when top && isEvar f ->
+ refresh_term_evars true false f;
+ Array.iter (refresh_term_evars onevars false) args
| Evar (ev, a) when onevars ->
let evi = Evd.find !evdref ev in
let ty' = refresh true evi.evar_concl in
if !modified then
evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
else ()
- | _ -> iter_constr (refresh_term_evars onevars) t
+ | _ -> iter_constr (refresh_term_evars onevars false) t
and refresh_polymorphic_positions args pos =
let rec aux i = function
| Some l :: ls ->
if i < Array.length args then
- ignore(refresh_term_evars true args.(i));
+ ignore(refresh_term_evars true false args.(i));
aux (succ i) ls
| None :: ls ->
if i < Array.length args then
- ignore(refresh_term_evars false args.(i));
+ ignore(refresh_term_evars false false args.(i));
aux (succ i) ls
| [] -> ()
in aux 0 pos
@@ -97,7 +100,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
(match pbty with
| None -> t
| Some dir -> refresh dir t)
- else (refresh_term_evars false t; t)
+ else (refresh_term_evars false true t; t)
in
if !modified then !evdref, t' else !evdref, t
@@ -118,11 +121,11 @@ let is_success = function Success _ -> true | UnifFailure _ -> false
let test_success conv_algo env evd c c' rhs =
is_success (conv_algo env evd c c' rhs)
-let add_conv_oriented_pb (pbty,env,t1,t2) evd =
+let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
match pbty with
- | Some true -> add_conv_pb (Reduction.CUMUL,env,t1,t2) evd
- | Some false -> add_conv_pb (Reduction.CUMUL,env,t2,t1) evd
- | None -> add_conv_pb (Reduction.CONV,env,t1,t2) evd
+ | Some true -> add_conv_pb ~tail (Reduction.CUMUL,env,t1,t2) evd
+ | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd
+ | None -> add_conv_pb ~tail (Reduction.CONV,env,t1,t2) evd
(*------------------------------------*
* Restricting existing evars *
@@ -175,20 +178,31 @@ let restrict_instance evd evk filter argsv =
Filter.filter_array (Filter.compose (evar_filter evi) filter) argsv
let noccur_evar env evd evk c =
- let rec occur_rec k c = match kind_of_term c with
+ let cache = ref Int.Set.empty (* cache for let-ins *) in
+ let rec occur_rec (k, env as acc) c =
+ match kind_of_term c with
| Evar (evk',args' as ev') ->
(match safe_evar_value evd ev' with
- | Some c -> occur_rec k c
+ | Some c -> occur_rec acc c
| None ->
if Evar.equal evk evk' then raise Occur
- else Array.iter (occur_rec k) args')
+ else Array.iter (occur_rec acc) args')
| Rel i when i > k ->
- (match pi2 (Environ.lookup_rel (i-k) env) with
+ if not (Int.Set.mem (i-k) !cache) then
+ (match pi2 (Environ.lookup_rel i env) with
| None -> ()
- | Some b -> occur_rec k (lift i b))
- | _ -> iter_constr_with_binders succ occur_rec k c
+ | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b))
+ | Proj (p,c) ->
+ let c =
+ try Retyping.expand_projection env evd p c []
+ with Retyping.RetypeError _ ->
+ (* Can happen when called from w_unify which doesn't assign evars/metas
+ eagerly enough *) c
+ in occur_rec acc c
+ | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env))
+ occur_rec acc c
in
- try occur_rec 0 c; true with Occur -> false
+ try occur_rec (0,env) c; true with Occur -> false
(***************************************)
(* Managing chains of local definitons *)
@@ -213,7 +227,7 @@ let compute_var_aliases sign =
sign Id.Map.empty
let compute_rel_aliases var_aliases rels =
- snd (List.fold_right (fun (_,b,t) (n,aliases) ->
+ snd (List.fold_right (fun (_,b,u) (n,aliases) ->
(n-1,
match b with
| Some t ->
@@ -227,7 +241,7 @@ let compute_rel_aliases var_aliases rels =
try Int.Map.find (p+n) aliases with Not_found -> [] in
Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases
| _ ->
- Int.Map.add n [lift n t] aliases)
+ Int.Map.add n [lift n (mkCast(t,DEFAULTcast,u))] aliases)
| None -> aliases))
rels (List.length rels,Int.Map.empty))
@@ -311,6 +325,7 @@ let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
let free_vars_and_rels_up_alias_expansion aliases c =
let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
+ let acc3 = ref Int.Set.empty and acc4 = ref Id.Set.empty in
let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
let is_in_cache depth = function
| Rel n -> Int.Set.mem (n-depth) !cache_rel
@@ -325,8 +340,13 @@ let free_vars_and_rels_up_alias_expansion aliases c =
| Rel _ | Var _ as ck ->
if is_in_cache depth ck then () else begin
put_in_cache depth ck;
- let c = expansion_of_var aliases c in
+ let c' = expansion_of_var aliases c in
+ (if c != c' then (* expansion, hence a let-in *)
match kind_of_term c with
+ | Var id -> acc4 := Id.Set.add id !acc4
+ | Rel n -> if n >= depth+1 then acc3 := Int.Set.add (n-depth) !acc3
+ | _ -> ());
+ match kind_of_term c' with
| Var id -> acc2 := Id.Set.add id !acc2
| Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
| _ -> frec (aliases,depth) c end
@@ -338,7 +358,7 @@ let free_vars_and_rels_up_alias_expansion aliases c =
frec (aliases,depth) c
in
frec (aliases,0) c;
- (!acc1,!acc2)
+ (!acc1,!acc2,!acc3,!acc4)
(********************************)
(* Managing pattern-unification *)
@@ -374,7 +394,7 @@ let get_actual_deps aliases l t =
l
else
(* Probably strong restrictions coming from t being evar-closed *)
- let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
+ let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion aliases t in
List.filter (fun c ->
match kind_of_term c with
| Var id -> Id.Set.mem id fv_ids
@@ -1013,52 +1033,52 @@ exception CannotProject of evar_map * existential
of subterms to eventually discard so as to be allowed to keep ti.
*)
-let rec is_constrainable_in top k (ev,(fv_rels,fv_ids) as g) t =
- let f,args = decompose_app_vect t in
+let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t =
+ let f,args2 = decompose_app_vect t in
+ let f,args1 = decompose_app_vect (whd_evar evd f) in
+ let args = Array.append args1 args2 in
match kind_of_term f with
| Construct ((ind,_),u) ->
let n = Inductiveops.inductive_nparams ind in
if n > Array.length args then true (* We don't try to be more clever *)
else
let params = fst (Array.chop n args) in
- Array.for_all (is_constrainable_in false k g) params
- | Ind _ -> Array.for_all (is_constrainable_in false k g) args
- | Prod (_,t1,t2) -> is_constrainable_in false k g t1 && is_constrainable_in false k g t2
+ Array.for_all (is_constrainable_in false evd k g) params
+ | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args
+ | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2
| Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
| Var id -> Id.Set.mem id fv_ids
| Rel n -> n <= k || Int.Set.mem n fv_rels
| Sort _ -> true
| _ -> (* We don't try to be more clever *) true
-let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
- let t = expansion_of_var aliases t in
- match kind_of_term t with
- | Var id -> Id.Set.mem id fv_ids
- | Rel n -> n <= k || Int.Set.mem n fv_rels
- | _ -> is_constrainable_in true k (ev,fvs) t
-
-let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
- let filter1 =
- restrict_upon_filter evd evk1 (noccur_evar env evd evk2) argsv1
- in
- let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
- let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in
- let filter2 =
- restrict_upon_filter evd evk2 (noccur_evar env evd evk1) argsv2
- in
- let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in
- let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in
- evd,ev1,ev2
+let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_rels,let_ids) t =
+ let t' = expansion_of_var aliases t in
+ if t' != t then
+ (* t is a local definition, we keep it only if appears in the list *)
+ (* of let-in variables effectively occurring on the right-hand side, *)
+ (* which is the only reason to keep it when inverting arguments *)
+ match kind_of_term t with
+ | Var id -> Id.Set.mem id let_ids
+ | Rel n -> Int.Set.mem n let_rels
+ | _ -> assert false
+ else
+ (* t is an instance for a proper variable; we filter it along *)
+ (* the free variables allowed to occur *)
+ match kind_of_term t with
+ | Var id -> Id.Set.mem id fv_ids
+ | Rel n -> n <= k || Int.Set.mem n fv_rels
+ | _ -> (not force || noccur_evar env evd ev t) && is_constrainable_in true evd k (ev,(fv_rels,fv_ids)) t
exception EvarSolvedOnTheFly of evar_map * constr
(* Try to project evk1[argsv1] on evk2[argsv2], if [ev1] is a pattern on
the common domain of definition *)
-let project_evar_on_evar g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
+let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
(* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in
let filter1 = restrict_upon_filter evd evk1
- (has_constrainable_free_vars evd aliases k2 evk2 fvs2)
+ (has_constrainable_free_vars env evd aliases force k2 evk2 fvs2)
argsv1 in
let candidates1 =
try restrict_candidates g env evd filter1 ev1 ev2
@@ -1094,9 +1114,9 @@ let check_evar_instance evd evk1 body conv_algo =
| Success evd -> evd
| UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
-let solve_evar_evar_l2r f g env evd aliases pbty ev1 (evk2,_ as ev2) =
+let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
try
- let evd,body = project_evar_on_evar g env evd aliases 0 pbty ev1 ev2 in
+ let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in
let evd' = Evd.define evk2 body evd in
check_evar_instance evd' evk2 body g
with EvarSolvedOnTheFly (evd,c) ->
@@ -1113,27 +1133,23 @@ let preferred_orientation evd evk1 evk2 =
| _,Evar_kinds.QuestionMark _ -> false
| _ -> true
-let solve_evar_evar_aux f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
+let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
let aliases = make_alias_map env in
if preferred_orientation evd evk1 evk2 then
- try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1
+ try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
with CannotProject (evd,ev2) ->
- try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2
+ try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
with CannotProject (evd,ev1) ->
- add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
+ add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
else
- try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2
+ try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
with CannotProject (evd,ev1) ->
- try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1
+ try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
with CannotProject (evd,ev2) ->
- add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
-
-let solve_evar_evar ?(force=false) f g env evd pbty ev1 ev2 =
- let (evd,(evk1,args1 as ev1),(evk2,args2 as ev2)),pbty =
- (* If an evar occurs in the instance of the other evar and the
- use of an heuristic is forced, we restrict *)
- if force then ensure_evar_independent g env evd ev1 ev2, None
- else (evd,ev1,ev2),pbty in
+ add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
+
+let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
+ let pbty = if force then None else pbty in
let evi = Evd.find evd evk1 in
let evd =
try
@@ -1162,7 +1178,7 @@ let solve_evar_evar ?(force=false) f g env evd pbty ev1 ev2 =
downcast evk2 t2 (downcast evk1 t1 evd)
with Reduction.NotArity ->
evd in
- solve_evar_evar_aux f g env evd pbty ev1 ev2
+ solve_evar_evar_aux force f g env evd pbty ev1 ev2
type conv_fun =
env -> evar_map -> conv_pb -> constr -> constr -> unification_result
@@ -1321,7 +1337,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
let aliases = lift_aliases k aliases in
(try
let ev = (evk,Array.map (lift k) argsv) in
- let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k None ev' ev in
+ let evd,body = project_evar_on_evar false conv_algo env' !evdref aliases k None ev' ev in
evdref := evd;
body
with
@@ -1338,7 +1354,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
let evd =
(* Try to project (a restriction of) the left evar ... *)
try
- let evd,body = project_evar_on_evar conv_algo env' evd aliases 0 None ev'' ev' in
+ let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in
let evd = Evd.define evk' body evd in
check_evar_instance evd evk' body conv_algo
with
@@ -1384,19 +1400,6 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
imitate envk t in
- let _fast rhs =
- let filter_ctxt = evar_filtered_context evi in
- let names = ref Idset.empty in
- let rec is_id_subst ctxt s =
- match ctxt, s with
- | ((id, _, _) :: ctxt'), (c :: s') ->
- names := Idset.add id !names;
- isVarId id c && is_id_subst ctxt' s'
- | [], [] -> true
- | _ -> false in
- is_id_subst filter_ctxt (Array.to_list argsv) &&
- closed0 rhs &&
- Idset.subset (collect_vars rhs) !names in
let rhs = whd_beta evd rhs (* heuristic *) in
let fast rhs =
let filter_ctxt = evar_filtered_context evi in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d286b98e..201a16eb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -212,9 +212,11 @@ let whd_head_evar sigma c =
(* Creating new metas *)
(**********************)
+let meta_counter_summary_name = "meta counter"
+
(* Generator of metavariables *)
let new_meta =
- let meta_ctr = Summary.ref 0 ~name:"meta counter" in
+ let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
fun () -> incr meta_ctr; !meta_ctr
let mk_new_meta () = mkMeta(new_meta())
@@ -241,9 +243,11 @@ let make_pure_subst evi args =
(* Creating new evars *)
(**********************)
+let evar_counter_summary_name = "evar counter"
+
(* Generator of existential names *)
let new_untyped_evar =
- let evar_ctr = Summary.ref 0 ~name:"evar counter" in
+ let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
(*------------------------------------*
@@ -838,3 +842,8 @@ let subterm_source evk (loc,k) =
| Evar_kinds.SubEvar (evk) -> evk
| _ -> evk in
(loc,Evar_kinds.SubEvar evk)
+
+
+(** Term exploration up to isntantiation. *)
+let kind_of_term_upto sigma t =
+ Constr.kind (Reductionops.whd_evar sigma t)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index f89266a6..49036798 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -199,6 +199,13 @@ val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
exception Uninstantiated_evar of existential_key
val flush_and_check_evars : evar_map -> constr -> constr
+(** {6 Term manipulation up to instantiation} *)
+
+(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t]
+ as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the
+ value of [e] in [sigma] is (recursively) used. *)
+val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
+
(** {6 debug pretty-printer:} *)
val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
@@ -236,3 +243,6 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b ->
val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
Evar_kinds.t Loc.located
+
+val meta_counter_summary_name : string
+val evar_counter_summary_name : string
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ee72d314..bf519fb7 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -230,20 +230,20 @@ let evar_instance_array test_id info args =
else instance_mismatch ()
| false :: filter, _ :: ctxt ->
instrec filter ctxt i
- | true :: filter, (id, _, _) :: ctxt ->
+ | true :: filter, (id,_,_ as d) :: ctxt ->
if i < len then
let c = Array.unsafe_get args i in
- if test_id id c then instrec filter ctxt (succ i)
+ if test_id d c then instrec filter ctxt (succ i)
else (id, c) :: instrec filter ctxt (succ i)
else instance_mismatch ()
| _ -> instance_mismatch ()
in
match Filter.repr (evar_filter info) with
| None ->
- let map i (id, _, _) =
+ let map i (id,_,_ as d) =
if (i < len) then
let c = Array.unsafe_get args i in
- if test_id id c then None else Some (id,c)
+ if test_id d c then None else Some (id,c)
else instance_mismatch ()
in
List.map_filter_i map (evar_context info)
@@ -251,7 +251,7 @@ let evar_instance_array test_id info args =
instrec filter (evar_context info) 0
let make_evar_instance_array info args =
- evar_instance_array isVarId info args
+ evar_instance_array (fun (id,_,_) -> isVarId id) info args
let instantiate_evar_array info c args =
let inst = make_evar_instance_array info args in
@@ -568,14 +568,6 @@ type evar_map = {
(*** Lifting primitive from Evar.Map. ***)
-(* HH: The progress tactical now uses this function. *)
-let progress_evar_map d1 d2 =
- let is_new k v =
- assert (v.evar_body == Evar_empty);
- EvMap.mem k d2.defn_evars
- in
- not (d1 == d2) && EvMap.exists is_new d1.undf_evars
-
let add_name_newly_undefined naming evk evi (evtoid,idtoev) =
let id = match naming with
| Misctypes.IntroAnonymous ->
@@ -779,7 +771,9 @@ let merge_universe_context evd uctx' =
let set_universe_context evd uctx' =
{ evd with universes = uctx' }
-let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
+let add_conv_pb ?(tail=false) pb d =
+ if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
+ else {d with conv_pbs = pb::d.conv_pbs}
let evar_source evk d = (find d evk).evar_source
@@ -1195,6 +1189,18 @@ let abstract_undefined_variables uctx =
in { uctx with uctx_local = Univ.ContextSet.empty;
uctx_univ_algebraic = vars' }
+let fix_undefined_variables ({ universes = uctx } as evm) =
+ let algs', vars' =
+ Univ.LMap.fold (fun u v (algs, vars as acc) ->
+ if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars)
+ else acc)
+ uctx.uctx_univ_variables
+ (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables)
+ in
+ {evm with universes =
+ { uctx with uctx_univ_variables = vars';
+ uctx_univ_algebraic = algs' } }
+
let refresh_undefined_univ_variables uctx =
let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
@@ -1301,27 +1307,6 @@ let e_eq_constr_univs evdref t u =
let eq_constr_univs_test evd t u =
snd (eq_constr_univs evd t u)
-let eq_named_context_val d ctx1 ctx2 =
- ctx1 == ctx2 ||
- let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
- let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
- Id.equal i1 i2 && Option.equal (eq_constr_univs_test d) c1 c2
- && (eq_constr_univs_test d) t1 t2
- in List.equal eq_named_declaration c1 c2
-
-let eq_evar_body d b1 b2 = match b1, b2 with
-| Evar_empty, Evar_empty -> true
-| Evar_defined t1, Evar_defined t2 -> eq_constr_univs_test d t1 t2
-| _ -> false
-
-let eq_evar_info d ei1 ei2 =
- ei1 == ei2 ||
- eq_constr_univs_test d ei1.evar_concl ei2.evar_concl &&
- eq_named_context_val d (ei1.evar_hyps) (ei2.evar_hyps) &&
- eq_evar_body d ei1.evar_body ei2.evar_body
- (** ppedrot: [eq_constr] may be a bit too permissive here *)
-
-
(**********************************************************)
(* Accessing metas *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 53f8b0db..fe785a83 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -12,7 +12,6 @@ open Names
open Term
open Context
open Environ
-open Mod_subst
(** {5 Existential variables and unification states}
@@ -127,10 +126,6 @@ type evar_map
(** Type of unification state. Essentially a bunch of state-passing data needed
to handle incremental term construction. *)
-val progress_evar_map : evar_map -> evar_map -> bool
-(** Assuming that the second map extends the first one, this says if
- some existing evar has been refined *)
-
val empty : evar_map
(** The empty evar map. *)
@@ -205,9 +200,6 @@ val add_constraints : evar_map -> Univ.constraints -> evar_map
val undefined_map : evar_map -> evar_info Evar.Map.t
(** Access the undefined evar mapping directly. *)
-val eq_evar_info : evar_map -> evar_info -> evar_info -> bool
-(** Compare the evar_info's up to the universe constraints of the evar map. *)
-
val drop_all_defined : evar_map -> evar_map
(** {6 Instantiating partial terms} *)
@@ -224,7 +216,7 @@ val existential_opt_value : evar_map -> existential -> constr option
(** Same as {!existential_value} but returns an option instead of raising an
exception. *)
-val evar_instance_array : (Id.t -> 'a -> bool) -> evar_info ->
+val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info ->
'a array -> (Id.t * 'a) list
val instantiate_evar_array : evar_info -> constr -> constr array -> constr
@@ -398,7 +390,7 @@ type clbinding =
(** Unification constraints *)
type conv_pb = Reduction.conv_pb
type evar_constraint = conv_pb * env * constr * constr
-val add_conv_pb : evar_constraint -> evar_map -> evar_map
+val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map
val extract_changed_conv_pbs : evar_map ->
(Evar.Set.t -> evar_constraint -> bool) ->
@@ -538,6 +530,8 @@ val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> e
val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
val abstract_undefined_variables : evar_universe_context -> evar_universe_context
+val fix_undefined_variables : evar_map -> evar_map
+
val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst
val nf_constraints : evar_map -> evar_map
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 7f7f4d76..95a6ba79 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -11,7 +11,6 @@ open Util
open Errors
open Names
open Locus
-open Context
open Term
open Nameops
open Termops
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 82330b84..47d9654e 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Names
open Locus
open Context
open Term
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 67f3cb41..e514fd52 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -13,6 +13,9 @@ open Glob_term
val cases_pattern_eq : cases_pattern -> cases_pattern -> bool
+val cast_type_eq : ('a -> 'a -> bool) ->
+ 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
+
val glob_constr_eq : glob_constr -> glob_constr -> bool
(** Operations on [glob_constr] *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 654f914b..dfdc24d4 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -18,7 +18,6 @@ open Declarations
open Declareops
open Environ
open Reductionops
-open Inductive
(* The following three functions are similar to the ones defined in
Inductive, but they expect an env *)
@@ -274,7 +273,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
let make_case_info env ind style =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let ind_tags =
- rel_context_tags (List.firstn mip.mind_nrealargs mip.mind_arity_ctxt) in
+ rel_context_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in
let cstr_tags =
Array.map2 (fun c n ->
let d,_ = decompose_prod_assum c in
@@ -366,14 +365,16 @@ let get_arity env ((ind,u),params) =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let parsign =
(* Dynamically detect if called with an instance of recursively
- uniform parameter only or also of non recursively uniform
+ uniform parameter only or also of recursively non-uniform
parameters *)
- let parsign = mib.mind_params_ctxt in
- let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in
- if Int.equal (List.length params) (rel_context_nhyps parsign - nnonrecparams) then
- snd (List.chop nnonrecparams mib.mind_params_ctxt)
- else
- parsign in
+ let nparams = List.length params in
+ if Int.equal nparams mib.mind_nparams then
+ mib.mind_params_ctxt
+ else begin
+ assert (Int.equal nparams mib.mind_nparams_rec);
+ let nnonrecparamdecls = List.length mib.mind_params_ctxt - mib.mind_nparams_rec in
+ snd (List.chop nnonrecparamdecls mib.mind_params_ctxt)
+ end in
let parsign = Vars.subst_instance_context u parsign in
let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in
@@ -527,7 +528,7 @@ let type_case_branches_with_names env indspec p c =
let (params,realargs) = List.chop nparams args in
let lbrty = Inductive.build_branches_type ind specif params p in
(* Build case type *)
- let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in
+ let conclty = Reduction.betazeta_appvect (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
(* Adjust names *)
if is_elim_predicate_explicitly_dependent env p (ind,params) then
(set_pattern_names env (fst ind) lbrty, conclty)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index af1783b7..7959759a 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -25,7 +25,9 @@ val type_of_constructors : env -> pinductive -> types array
(** Return constructor types in normal form *)
val arities_of_constructors : env -> pinductive -> types array
-(** An inductive type with its parameters *)
+(** An inductive type with its parameters (transparently supports
+ reasoning either with only recursively uniform parameters or with all
+ parameters including the recursively non-uniform ones *)
type inductive_family
val make_ind_family : inductive puniverses * constr list -> inductive_family
val dest_ind_family : inductive_family -> inductive puniverses * constr list
@@ -138,10 +140,14 @@ val lift_constructor : int -> constructor_summary -> constructor_summary
val get_constructor :
pinductive * mutual_inductive_body * one_inductive_body * constr list ->
int -> constructor_summary
-val get_arity : env -> inductive_family -> rel_context * sorts_family
val get_constructors : env -> inductive_family -> constructor_summary array
val get_projections : env -> inductive_family -> constant array option
+(** [get_arity] returns the arity of the inductive family instantiated
+ with the parameters; if recursively non-uniform parameters are not
+ part of the inductive family, they appears in the arity *)
+val get_arity : env -> inductive_family -> rel_context * sorts_family
+
val build_dependent_constructor : constructor_summary -> constr
val build_dependent_inductive : env -> inductive_family -> constr
val make_arity_signature : env -> bool -> inductive_family -> rel_context
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index c49bec9a..705e594a 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -123,6 +123,8 @@ let head_of_constr_reference c = match kind_of_term c with
let pattern_of_constr env sigma t =
let ctx = ref [] in
+ let keep = ref Evar.Set.empty in
+ let remove = ref Evar.Set.empty in
let rec pattern_of_constr env t =
match kind_of_term t with
| Rel n -> PRel n
@@ -141,28 +143,38 @@ let pattern_of_constr env sigma t =
| App (f,a) ->
(match
match kind_of_term f with
- Evar (evk,args as ev) ->
- (match snd (Evd.evar_source evk sigma) with
- Evar_kinds.MatchingVar (true,id) ->
- ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx;
- Some id
- | _ -> None)
- | _ -> None
- with
- | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
- | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
+ | Evar (evk,args as ev) ->
+ (match snd (Evd.evar_source evk sigma) with
+ Evar_kinds.MatchingVar (true,id) ->
+ let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+ ctx := (id,None,ty)::!ctx;
+ keep := Evar.Set.union (evars_of_term ty) !keep;
+ remove := Evar.Set.add evk !remove;
+ Some id
+ | _ -> None)
+ | _ -> None
+ with
+ | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
+ | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
| Const (sp,u) -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
| Ind (sp,u) -> PRef (canonical_gr (IndRef sp))
| Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
| Proj (p, c) ->
pattern_of_constr env (Retyping.expand_projection env sigma p c [])
| Evar (evk,ctxt as ev) ->
- (match snd (Evd.evar_source evk sigma) with
- | Evar_kinds.MatchingVar (b,id) ->
- ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx;
- assert (not b); PMeta (Some id)
- | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt)
- | _ -> PMeta None)
+ remove := Evar.Set.add evk !remove;
+ (match snd (Evd.evar_source evk sigma) with
+ | Evar_kinds.MatchingVar (b,id) ->
+ let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+ ctx := (id,None,ty)::!ctx;
+ let () = ignore (pattern_of_constr env ty) in
+ assert (not b); PMeta (Some id)
+ | Evar_kinds.GoalEvar ->
+ PEvar (evk,Array.map (pattern_of_constr env) ctxt)
+ | _ ->
+ let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+ let () = ignore (pattern_of_constr env ty) in
+ PMeta None)
| Case (ci,p,a,br) ->
let cip =
{ cip_style = ci.ci_pp_info.style;
@@ -178,9 +190,11 @@ let pattern_of_constr env sigma t =
| Fix f -> PFix f
| CoFix f -> PCoFix f in
let p = pattern_of_constr env t in
+ let remove = Evar.Set.diff !remove !keep in
+ let sigma = Evar.Set.fold (fun ev acc -> Evd.remove acc ev) remove sigma in
(* side-effect *)
(* Warning: the order of dependencies in ctx is not ensured *)
- (!ctx,p)
+ (sigma,!ctx,p)
(* To process patterns, we need a translation without typing at all. *)
@@ -220,7 +234,7 @@ let instantiate_pattern env sigma lvar c =
ctx
in
let c = substl inst c in
- snd (pattern_of_constr env sigma c)
+ pi3 (pattern_of_constr env sigma c)
with Not_found (* List.index failed *) ->
let vars =
List.map_filter (function Name id -> Some id | _ -> None) vars in
@@ -245,7 +259,7 @@ let rec subst_pattern subst pat =
| PRef ref ->
let ref',t = subst_global subst ref in
if ref' == ref then pat else
- snd (pattern_of_constr (Global.env()) Evd.empty t)
+ pi3 (pattern_of_constr (Global.env()) Evd.empty t)
| PVar _
| PEvar _
| PRel _ -> pat
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index cf02421c..9e72280f 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -39,7 +39,8 @@ val head_of_constr_reference : Term.constr -> global_reference
a pattern; currently, no destructor (Cases, Fix, Cofix) and no
existential variable are allowed in [c] *)
-val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> named_context * constr_pattern
+val pattern_of_constr : Environ.env -> Evd.evar_map -> constr ->
+ Evd.evar_map * named_context * constr_pattern
(** [pattern_of_glob_constr l c] translates a term [c] with metavariables into
a pattern; variables bound in [l] are replaced by the pattern to which they
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 040792ef..0cadffa4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -82,7 +82,7 @@ let search_guard loc env possible_indexes fixdefs =
iraise (e, info));
indexes
else
- (* we now search recursively amoungst all combinations *)
+ (* we now search recursively among all combinations *)
(try
List.iter
(fun l ->
@@ -220,7 +220,7 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
let c = if flags.expand_evars then nf_evar sigma c else c in
sigma,c
-(* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
let allow_anonymous_refs = ref false
(* Utilisé pour inférer le prédicat des Cases *)
@@ -324,12 +324,6 @@ let pretype_id pretype loc env evdref lvar id =
(* Check if [id] is a section or goal variable *)
try
let (_,_,typ) = lookup_named id env in
- (* let _ = *)
- (* try *)
- (* let ctx = Decls.variable_context id in *)
- (* evdref := Evd.merge_context_set univ_rigid !evdref ctx; *)
- (* with Not_found -> () *)
- (* in *)
{ uj_val = mkVar id; uj_type = typ }
with Not_found ->
(* [id] not found, standard error message *)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7d1e0c9b..142b5451 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -63,7 +63,7 @@ val all_no_fail_flags : inference_flags
val all_and_fail_flags : inference_flags
-(** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+(** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
val allow_anonymous_refs : bool ref
(** Generic call to the interpreter from glob_constr to open_constr, leaving
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a23963ab..dd671f11 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -60,13 +60,20 @@ module ReductionBehaviour = struct
let discharge = function
| _,(ReqGlobal (ConstRef c, req), (_, b)) ->
- let c' = pop_con c in
- let vars, _subst, _ctx = Lib.section_segment_of_constant c in
- let extra = List.length vars in
- let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in
- let recargs' = List.map ((+) extra) b.b_recargs in
- let b' = { b with b_nargs = nargs'; b_recargs = recargs' } in
- Some (ReqGlobal (ConstRef c', req), (ConstRef c', b'))
+ let b =
+ if Lib.is_in_section (ConstRef c) then
+ let vars, _, _ = Lib.section_segment_of_constant c in
+ let extra = List.length vars in
+ let nargs' =
+ if b.b_nargs = max_int then max_int
+ else if b.b_nargs < 0 then b.b_nargs
+ else b.b_nargs + extra in
+ let recargs' = List.map ((+) extra) b.b_recargs in
+ { b with b_nargs = nargs'; b_recargs = recargs' }
+ else b
+ in
+ let c = Lib.discharge_con c in
+ Some (ReqGlobal (ConstRef c, req), (ConstRef c, b))
| _ -> None
let rebuild = function
@@ -842,7 +849,14 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
let (tm',sk'),cst_l' =
whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
in
- if equal_stacks (x, app_sk) (tm', sk') || Stack.will_expose_iota sk'
+ let rec is_case x = match kind_of_term x with
+ | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
+ | App (hd, _) -> is_case hd
+ | Case _ -> true
+ | _ -> false in
+ if equal_stacks (x, app_sk) (tm', sk')
+ || Stack.will_expose_iota sk'
+ || is_case tm'
then fold ()
else whrec cst_l' (tm', sk' @ sk)
else match recargs with
@@ -980,7 +994,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
| CoFix cofix ->
if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
match Stack.strip_app stack with
- |args, (Stack.Case(ci, _, lf,_)::s') ->
+ |args, ((Stack.Case _ |Stack.Proj _)::s') ->
reduce_and_refold_cofix whrec env cst_l cofix stack
|_ -> fold ()
else fold ()
@@ -1059,7 +1073,7 @@ let local_whd_state_gen flags sigma =
| CoFix cofix ->
if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
match Stack.strip_app stack with
- |args, (Stack.Case(ci, _, lf,_)::s') ->
+ |args, ((Stack.Case _ | Stack.Proj _)::s') ->
whrec (contract_cofix cofix, stack)
|_ -> s
else s
@@ -1279,7 +1293,8 @@ let sigma_univ_state =
{ Reduction.compare = sigma_compare_sorts;
Reduction.compare_instances = sigma_compare_instances }
-let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y =
+let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state)
+ env sigma x y =
try
let b, sigma =
let b, cstrs =
@@ -1301,7 +1316,7 @@ let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y
sigma', true
with
| Reduction.NotConvertible -> sigma, false
- | Univ.UniverseInconsistency _ -> sigma, false
+ | Univ.UniverseInconsistency _ when catch_incon -> sigma, false
| e when is_anomaly e -> error "Conversion test raised an anomaly"
(********************************************************************)
@@ -1617,3 +1632,16 @@ let head_unfold_under_prod ts env _ c =
| Const cst -> beta_applist (unfold cst,l)
| _ -> c in
aux c
+
+let betazetaevar_applist sigma n c l =
+ let rec stacklam n env t stack =
+ if Int.equal n 0 then applist (substl env t, stack) else
+ match kind_of_term t, stack with
+ | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
+ | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
+ | Evar ev, _ ->
+ (match safe_evar_value sigma ev with
+ | Some body -> stacklam n env body stack
+ | None -> applist (substl env t, stack))
+ | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+ stacklam n [] c l
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 7c61d4e1..1df2a73b 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -268,9 +268,11 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con
(** [infer_fconv] Adds necessary universe constraints to the evar map.
pb defaults to CUMUL and ts to a full transparent state.
+ @raises UniverseInconsistency iff catch_incon is set to false,
+ otherwise returns false in that case.
*)
-val infer_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr ->
- evar_map * bool
+val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state ->
+ env -> evar_map -> constr -> constr -> evar_map * bool
(** {6 Special-Purpose Reduction Functions } *)
@@ -278,6 +280,7 @@ val whd_meta : evar_map -> constr -> constr
val plain_instance : constr Metamap.t -> constr -> constr
val instance : evar_map -> constr Metamap.t -> constr -> constr
val head_unfold_under_prod : transparent_state -> reduction_function
+val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
(** {6 Heuristic for Conversion with Evar } *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index cd52ba44..a56861c6 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -100,7 +100,7 @@ let retype ?(polyprop=true) sigma =
| Ind ind -> rename_type_of_inductive env ind
| Construct cstr -> rename_type_of_constructor env cstr
| Case (_,p,c,lf) ->
- let Inductiveops.IndType(_,realargs) =
+ let Inductiveops.IndType(indf,realargs) =
let t = type_of env c in
try Inductiveops.find_rectype env sigma t
with Not_found ->
@@ -109,7 +109,8 @@ let retype ?(polyprop=true) sigma =
Inductiveops.find_rectype env sigma t
with Not_found -> retype_error BadRecursiveType
in
- let t = whd_beta sigma (applist (p, realargs)) in
+ let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in
+ let t = betazetaevar_applist sigma n p realargs in
(match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
| Prod _ -> whd_beta sigma (applist (t, [c]))
| _ -> t)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b4e0459c..372b26aa 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -23,7 +23,6 @@ open Reductionops
open Cbv
open Patternops
open Locus
-open Pretype_errors
(* Errors *)
@@ -190,6 +189,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
if
Array.for_all (noccurn k) tys
&& Array.for_all (noccurn (k+nbfix)) bds
+ && k <= n
then
(k, List.nth labs (k-1))
else
@@ -597,13 +597,6 @@ let reduce_proj env sigma whfun whfun' c =
| _ -> raise Redelimination
in redrec c
-
-let dont_expose_case = function
- | EvalVar _ | EvalRel _ | EvalEvar _ -> false
- | EvalConst c ->
- Option.cata (fun (_,_,z) -> List.mem `ReductionDontExposeCase z)
- false (ReductionBehaviour.get (ConstRef c))
-
let whd_nothing_for_iota env sigma s =
let rec whrec (x, stack as s) =
match kind_of_term x with
@@ -1212,9 +1205,10 @@ let one_step_reduce env sigma c =
(ci,p,c,lf), stack)
with Redelimination -> raise NotStepReducible)
| Fix fix ->
- (match reduce_fix (whd_construct_stack env) sigma fix stack with
+ (try match reduce_fix (whd_construct_stack env) sigma fix stack with
| Reduced s' -> s'
- | NotReducible -> raise NotStepReducible)
+ | NotReducible -> raise NotStepReducible
+ with Redelimination -> raise NotStepReducible)
| _ when isEvalRef env x ->
let ref,u = destEvalRefU x in
(try
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 5862a852..9f04faa8 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -15,7 +15,6 @@ open Term
open Vars
open Context
open Environ
-open Locus
(* Sorts and sort family *)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 9f3efd72..2552c67e 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -11,7 +11,6 @@ open Names
open Term
open Context
open Environ
-open Locus
(** printers *)
val print_sort : sorts -> std_ppcmds
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 817d6878..18e83056 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -14,7 +14,6 @@ open Term
open Vars
open Context
open Evd
-open Environ
open Util
open Typeclasses_errors
open Libobject
@@ -427,7 +426,6 @@ let add_class cl =
cl.cl_projs
-open Declarations
(*
* interface functions
@@ -485,15 +483,6 @@ let is_instance = function
is_class (IndRef ind)
| _ -> false
-let is_implicit_arg = function
-| Evar_kinds.GoalEvar -> false
-| _ -> true
- (* match k with *)
- (* ImplicitArg (ref, (n, id), b) -> true *)
- (* | InternalHole -> true *)
- (* | _ -> false *)
-
-
(* To embed a boolean for resolvability status.
This is essentially a hack to mark which evars correspond to
goals and do not need to be resolved when we have nested [resolve_all_evars]
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 1a0b6696..b3170b97 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -77,8 +77,6 @@ val instance_priority : instance -> int option
val is_class : global_reference -> bool
val is_instance : global_reference -> bool
-val is_implicit_arg : Evar_kinds.t -> bool
-
(** Returns the term and type for the given instance of the parameters and fields
of the type class. *)
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 4f88dd86..585f066d 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -10,7 +10,6 @@
open Names
open Term
open Context
-open Evd
open Environ
open Constrexpr
open Globnames
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index dd808771..7982fc85 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -10,7 +10,6 @@ open Loc
open Names
open Term
open Context
-open Evd
open Environ
open Constrexpr
open Globnames
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index c933106d..1f822f1a 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Names
open Term
open Environ
open Evd
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 203b1ec8..01e1154e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -673,6 +673,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
(sigma,(k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst,
evarsubst)
else error_cannot_unify_local curenv sigma (m,n,cM)
+ | Evar (evk,_ as ev), Evar (evk',_)
+ when not (Evar.Set.mem evk flags.frozen_evars)
+ && Evar.equal evk evk' ->
+ sigma,metasubst,((curenv,ev,cN)::evarsubst)
| Evar (evk,_ as ev), _
when not (Evar.Set.mem evk flags.frozen_evars)
&& not (occur_evar evk cN) ->
@@ -1673,11 +1677,13 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
matchrec t
with ex when precatchable_exception ex ->
matchrec c)
+
| Lambda (_,t,c) ->
(try
matchrec t
with ex when precatchable_exception ex ->
matchrec c)
+
| _ -> error "Match_subterm"))
in
try matchrec cl
@@ -1774,7 +1780,12 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
try
(* This is up to delta for subterms w/o metas ... *)
w_unify_to_subterm env evd ~flags (strip_outer_cast op,t)
- with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op)
+ with PretypeError (env,_,NoOccurrenceFound _) when
+ allow_K ||
+ (* w_unify_to_subterm does not go through evars, so
+ the next step, which was already in <= 8.4, is
+ needed at least for compatibility of rewrite *)
+ dependent op t -> (evd,op)
in
if not allow_K &&
(* ensure we found a different instance *)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 19613c4e..8198db1b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -166,8 +166,15 @@ and nf_whd env whd typ =
mkApp(cfd,args)
| Vconstr_const n -> construct_of_constr_const env n typ
| Vconstr_block b ->
- let capp,ctyp = construct_of_constr_block env (btag b) typ in
- let args = nf_bargs env b ctyp in
+ let tag = btag b in
+ let (tag,ofs) =
+ if tag = Cbytecodes.last_variant_tag then
+ match whd_val (bfield b 0) with
+ | Vconstr_const tag -> (tag+Cbytecodes.last_variant_tag, 1)
+ | _ -> assert false
+ else (tag, 0) in
+ let capp,ctyp = construct_of_constr_block env tag typ in
+ let args = nf_bargs env b ofs ctyp in
mkApp(capp,args)
| Vatom_stk(Aid idkey, stk) ->
let c,typ = constr_type_of_idkey env idkey in
@@ -242,14 +249,14 @@ and nf_args env vargs t =
t := subst1 c codom; c) in
!t,args
-and nf_bargs env b t =
+and nf_bargs env b ofs t =
let t = ref t in
- let len = bsize b in
+ let len = bsize b - ofs in
let args =
Array.init len
(fun i ->
let _,dom,codom = decompose_prod env !t in
- let c = nf_val env (bfield b i) dom in
+ let c = nf_val env (bfield b (i+ofs)) dom in
t := subst1 c codom; c) in
args