let leng = List.length fl in
let new_env =
let counter = ref 0 in
- let rec build_env e =
- if !counter = leng then e
+ let rec build_env e' =
+ if !counter = leng then e'
else
(incr counter ;
build_env
- ((RS.to_env (k,e,ens,C.Fix (!counter -1, fl),[]))::e))
+ ((RS.to_env (k,e,ens,C.Fix (!counter -1, fl),[]))::e'))
in
build_env e
in
with CicUtil.Subst_not_found _ -> false,ugraph)
(* TASSI: CONSTRAINTS *)
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
- true,(CicUniv.add_eq t2 t1 ugraph)
+ (try
+ true,(CicUniv.add_eq t2 t1 ugraph)
+ with CicUniv.UniverseInconsistency _ -> false,ugraph)
(* TASSI: CONSTRAINTS *)
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- true,(CicUniv.add_ge t2 t1 ugraph)
+ (try
+ true,(CicUniv.add_ge t2 t1 ugraph)
+ with CicUniv.UniverseInconsistency _ -> false,ugraph)
(* TASSI: CONSTRAINTS *)
| (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
(* TASSI: CONSTRAINTS *)
else
false,ugraph
| (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
- let tys =
- List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl1
in
if i1 = i2 then
List.fold_right2
else
false,ugraph
| (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
- let tys =
- List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
- in
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl1
+ in
if i1 = i2 then
List.fold_right2
(fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
(* performs an head beta/cast reduction *)
-let rec head_beta_reduce =
- function
- (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
- let he'' = CicSubstitution.subst he' t in
- if tl' = [] then
- he''
- else
- let he''' =
- match he'' with
- Cic.Appl l -> Cic.Appl (l@tl')
- | _ -> Cic.Appl (he''::tl')
+let rec head_beta_reduce ?(delta=false) ?(upto=(-1)) t =
+ match upto with
+ 0 -> t
+ | n ->
+ match t with
+ (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
+ let he'' = CicSubstitution.subst he' t in
+ if tl' = [] then
+ he''
+ else
+ let he''' =
+ match he'' with
+ Cic.Appl l -> Cic.Appl (l@tl')
+ | _ -> Cic.Appl (he''::tl')
+ in
+ head_beta_reduce ~delta ~upto:(upto - 1) he'''
+ | Cic.Cast (te,_) -> head_beta_reduce ~delta ~upto 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 ~upto
+ ~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
- head_beta_reduce he'''
- | Cic.Cast (te,_) -> head_beta_reduce te
- | t -> t
+ (match bo with
+ None -> t
+ | Some bo ->
+ head_beta_reduce ~delta ~upto (CicSubstitution.subst_vars ens bo))
+ | t -> t
(*
let are_convertible ?subst ?metasenv context t1 t2 ugraph =