(k', e', ens', C.MutConstruct (_,_,j,_), []) ->
reduce (k, e, ens, (List.nth pl (j-1)), s)
| (k', e', ens', C.MutConstruct (_,_,j,_), s') ->
- let (arity, r) =
+ let r =
let o,_ =
CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind
in
match o with
- C.InductiveDefinition (s,ingredients,r,_) ->
- let (_,_,arity,_) = List.nth s i in
- (arity,r)
+ C.InductiveDefinition (_,_,r,_) -> r
| _ -> raise WrongUriToInductiveDefinition
in
let ts =
let are_convertible whd ?(subst=[]) ?(metasenv=[]) =
let heuristic = ref true in
let rec aux test_equality_only context t1 t2 ugraph =
- let aux2 test_equality_only t1 t2 ugraph =
+ let rec aux2 test_equality_only t1 t2 ugraph =
(* this trivial euristic cuts down the total time of about five times ;-) *)
(* this because most of the time t1 and t2 are "sintactically" the same *)
fl1 fl2 (true,ugraph)
else
false,ugraph
- | (C.Cast _, _) | (_, C.Cast _)
+ | C.Cast (bo,_),t -> aux2 test_equality_only bo t ugraph
+ | t,C.Cast (bo,_) -> aux2 test_equality_only t bo ugraph
| (C.Implicit _, _) | (_, C.Implicit _) -> assert false
| (_,_) -> false,ugraph
end
(* performs an head beta/cast reduction *)
-let rec head_beta_reduce =
+let rec head_beta_reduce ?(delta=false) =
function
(Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
let he'' = CicSubstitution.subst he' t in
Cic.Appl l -> Cic.Appl (l@tl')
| _ -> Cic.Appl (he''::tl')
in
- head_beta_reduce he'''
- | Cic.Cast (te,_) -> head_beta_reduce te
+ head_beta_reduce ~delta he'''
+ | Cic.Cast (te,_) -> head_beta_reduce ~delta te
+ | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true ->
+ let bo =
+ match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
+ Cic.Constant (_,bo,_,_,_) -> bo
+ | Cic.Variable _ -> raise ReferenceToVariable
+ | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
+ | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ in
+ (match bo with
+ None -> t
+ | Some bo ->
+ head_beta_reduce
+ ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl)))
+ | Cic.Const (uri,ens) as t when delta=true ->
+ let bo =
+ match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
+ Cic.Constant (_,bo,_,_,_) -> bo
+ | Cic.Variable _ -> raise ReferenceToVariable
+ | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
+ | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ in
+ (match bo with
+ None -> t
+ | Some bo ->
+ head_beta_reduce ~delta (CicSubstitution.subst_vars ens bo))
| t -> t
(*