+ lift (k -1) arg
+ with
+ Not_found ->
+ let params =
+ 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
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ )
+ in
+(*
+debug_print "\n\n---- BEGIN " ;
+debug_print ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
+debug_print ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst)) ;
+debug_print ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst')) ;
+*)
+ let exp_named_subst'' =
+ substaux_in_exp_named_subst uri k exp_named_subst' params
+ in
+(*
+debug_print ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'')) ;
+debug_print "---- END\n\n " ;
+*)
+ C.Var (uri,exp_named_subst'')
+ )
+ | C.Meta (i, l) as t ->
+ let l' =
+ List.map
+ (function
+ None -> None
+ | Some t -> Some (substaux k t)
+ ) l
+ in
+ C.Meta(i,l')
+ | C.Sort _ 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.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
+ | C.Appl (he::tl) ->
+ (* Invariant: no Appl applied to another Appl *)
+ let tl' = List.map (substaux k) tl in
+ begin
+ match substaux k he with
+ C.Appl l -> C.Appl (l@tl')
+ | _ as he' -> C.Appl (he'::tl')
+ end
+ | C.Appl _ -> assert false
+ | C.Const (uri,exp_named_subst') ->
+ let params =
+ 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.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ )
+ in
+ let exp_named_subst'' =
+ substaux_in_exp_named_subst uri k exp_named_subst' params
+ in
+ C.Const (uri,exp_named_subst'')
+ | C.MutInd (uri,typeno,exp_named_subst') ->
+ let params =
+ 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.InductiveDefinition (_,params,_,_) -> params
+ )
+ in
+ let exp_named_subst'' =
+ substaux_in_exp_named_subst uri k exp_named_subst' params
+ in
+ C.MutInd (uri,typeno,exp_named_subst'')
+ | C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
+ let params =
+ 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.InductiveDefinition (_,params,_,_) -> params
+ )
+ in
+ let exp_named_subst'' =
+ substaux_in_exp_named_subst uri k exp_named_subst' params
+ in
+ C.MutConstruct (uri,typeno,consno,exp_named_subst'')
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i,substaux k outt, substaux k t,
+ List.map (substaux k) pl)
+ | C.Fix (i,fl) ->
+ let len = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
+ fl
+ in
+ C.Fix (i, substitutedfl)
+ | C.CoFix (i,fl) ->
+ let len = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
+ fl
+ in
+ C.CoFix (i, substitutedfl)
+ and substaux_in_exp_named_subst uri k exp_named_subst' params =
+(*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
+(*CSC: e' vero???? una veloce prova non sembra confermare la teoria *)
+ let rec filter_and_lift =
+ function
+ [] -> []
+ | (uri,t)::tl when
+ List.for_all
+ (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst'
+ &&
+ List.mem uri params
+ ->
+ (uri,lift (k-1) t)::(filter_and_lift tl)
+ | _::tl -> filter_and_lift tl
+(*
+ | (uri,_)::tl ->
+debug_print ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
+if List.for_all (function (uri',_) -> not (UriManager.eq uri uri'))
+exp_named_subst' then debug_print "---- OK1" ;
+debug_print ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
+if List.mem uri params then debug_print "---- OK2" ;
+ filter_and_lift tl
+*)
+ in
+ List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @
+ (filter_and_lift exp_named_subst)
+ in
+ substaux 1