exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
-let lift n =
+let lift_from k n =
let rec liftaux k =
let module C = Cic in
function
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
in
C.CoFix (i, liftedfl)
in
+ liftaux k
+
+let lift n t =
if n = 0 then
- (function t -> t)
+ t
else
- liftaux 1
+ lift_from 1 n t
;;
let subst arg =
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
| C.Prod (n,s,t) -> 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)
with
Not_found ->
let params =
- (match CicEnvironment.get_cooked_obj ~trust:true uri with
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (match obj with
C.Constant _ -> raise ReferenceToConstant
| C.Variable (_,_,_,params) -> params
| C.CurrentProof _ -> raise ReferenceToCurrentProof
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
| C.Prod (n,s,t) -> 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.Appl _ -> assert false
| C.Const (uri,exp_named_subst') ->
let params =
- (match CicEnvironment.get_cooked_obj ~trust:true uri with
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (match obj with
C.Constant (_,_,_,params) -> params
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof (_,_,_,_,params) -> params
C.Const (uri,exp_named_subst'')
| C.MutInd (uri,typeno,exp_named_subst') ->
let params =
- (match CicEnvironment.get_cooked_obj ~trust:true uri with
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (match obj with
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof _ -> raise ReferenceToCurrentProof
C.MutInd (uri,typeno,exp_named_subst'')
| C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
let params =
- (match CicEnvironment.get_cooked_obj ~trust:true uri with
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (match obj with
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof _ -> raise ReferenceToCurrentProof
substaux 1
;;
-(* l is the relocation list *)
+(* lift_meta [t_1 ; ... ; t_n] t *)
+(* returns the term [t] where [Rel i] is substituted with [t_i] *)
+(* [t_i] is lifted as usual when it crosses an abstraction *)
let lift_meta l t =
- let module C = Cic in
- if l = [] then t else
- let rec aux k = function
+ let module C = Cic in
+ if l = [] then t else
+ let rec aux k = function
C.Rel n as t ->
- if n <= k then t else
+ if n <= k then t else
(try
match List.nth l (n-k-1) with
None -> raise RelToHiddenHypothesis
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
| C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)