| C.Cast (te,ty) -> C.Cast (aux te, aux ty)
| C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
- | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
+ | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux s, aux ty, aux t)
| C.Appl l ->
(* Invariant enforced: no application of an application *)
(match List.map aux l with
find_image_aux (what,with_what)
in
let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in
- let add_ctx1 ctx n s = (Some (n, Cic.Def (s,None)))::ctx in
+ let add_ctx1 ctx n s ty = (Some (n, Cic.Def (s,ty)))::ctx in
let rec substaux k ctx what t =
try
S.lift (k-1) (find_image ctx what t)
| C.Lambda (n,s,t) ->
C.Lambda
(n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
C.LetIn
- (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (List.map (S.lift 1) what) t)
+ (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (S.lift 1) what) t)
| C.Appl (he::tl) ->
(* Invariant: no Appl applied to another Appl *)
let tl' = List.map (substaux k ctx what) tl in
C.Prod (n, substaux k s, substaux (k + 1) t)
| C.Lambda (n,s,t) ->
C.Lambda (n, substaux k s, substaux (k + 1) t)
- | C.LetIn (n,s,t) ->
- C.LetIn (n, substaux k s, substaux (k + 1) t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
| C.Appl (he::tl) ->
(* Invariant: no Appl applied to another Appl *)
let tl' = List.map (substaux k) tl in
C.Prod (n, subst_term k v, subst_term (succ k) t)
| C.Lambda (n, v, t) ->
C.Lambda (n, subst_term k v, subst_term (succ k) t)
- | C.LetIn (n, v, t) ->
- C.LetIn (n, subst_term k v, subst_term (succ k) t)
+ | C.LetIn (n, v, ty, t) ->
+ C.LetIn (n, subst_term k v, subst_term k ty, subst_term (succ k) t)
| C.Fix (i, fixes) ->
let fixesno = List.length fixes in
let fixes = List.map (subst_fix fixesno k) fixes in
with
Failure _ -> assert false)
| Cic.Const (uri,exp_named_subst) as t ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
(match o with
Cic.Constant (_,Some body,_,_,_) ->
CicReduction.head_beta_reduce
| Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
| Cic.Var (uri,exp_named_subst) as t ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
(match o with
Cic.Constant _ -> raise ReferenceToConstant
| Cic.CurrentProof _ -> raise ReferenceToCurrentProof
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
in
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
C.Constant _ -> raise ReferenceToConstant
| C.CurrentProof _ -> raise ReferenceToCurrentProof
| he::tl -> reduceaux context tl (S.subst he t)
(* when name is Anonimous the substitution should be superfluous *)
)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
reduceaux context l (S.subst (reduceaux context [] s) t)
| C.Appl (he::tl) ->
let tl' = List.map (reduceaux context []) tl in
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
in
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
C.Constant (_,Some body,_,_,_) ->
if List.exists is_active l then
C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
| C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
let (arity, r) =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph mutind in
match o with
C.InductiveDefinition (tl,ingredients,r,_) ->
let (_,_,arity,_) = List.nth tl i in
(* be superfluous *)
aux (he::rev_constant_args) tl (S.subst he t)
end
- | C.LetIn (_,s,t) ->
+ | C.LetIn (_,s,_,t) ->
aux rev_constant_args l (S.subst s t)
| C.Fix (i,fl) ->
let (_,recindex,_,body) = List.nth fl i in
(* when name is Anonimous the substitution should *)
(* be superfluous *)
aux tl (S.subst he t))
- | C.LetIn (_,s,t) -> aux l (S.subst s t)
+ | C.LetIn (_,s,_,t) -> aux l (S.subst s t)
| Cic.Appl (Cic.Const (uri,_) :: args) as t when is_fix uri ->
let recno =
prerr_endline ("cerco : " ^ string_of_int (guess_recno uri)
prerr_endline (CicPp.ppterm t2 ^ "\n");
let subst1, _, _ =
CicUnification.fo_unif metasenv ctx t1 t2
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
prerr_endline "UNIFICANO\n\n\n";
subst := subst1;