exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
+let debug_print = fun _ -> ()
+
let lift_from k n =
let rec liftaux k =
let module C = Cic in
lift_from 1 n t
;;
+(* delifts a term t of n levels strating from k, that is changes (Rel m)
+ * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails
+ *)
+let delift_from k n =
+ let rec liftaux k =
+ let module C = Cic in
+ function
+ C.Rel m ->
+ if m < k then
+ C.Rel m
+ else if m < k + n then
+ (failwith "delifting this term whould capture free variables")
+ else
+ C.Rel (m - n)
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
+ in
+ C.Var (uri,exp_named_subst')
+ | C.Meta (i,l) ->
+ let l' =
+ List.map
+ (function
+ None -> None
+ | Some t -> Some (liftaux k t)
+ ) l
+ in
+ C.Meta(i,l')
+ | C.Sort _ 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)
+ | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
+ | C.Appl l -> C.Appl (List.map (liftaux k) l)
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
+ in
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
+ in
+ C.MutInd (uri,tyno,exp_named_subst')
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
+ in
+ C.MutConstruct (uri,tyno,consno,exp_named_subst')
+ | C.MutCase (sp,i,outty,t,pl) ->
+ C.MutCase (sp, i, liftaux k outty, liftaux k t,
+ List.map (liftaux k) pl)
+ | C.Fix (i, fl) ->
+ let len = List.length fl in
+ let liftedfl =
+ List.map
+ (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
+ fl
+ in
+ C.Fix (i, liftedfl)
+ | C.CoFix (i, fl) ->
+ let len = List.length fl in
+ let liftedfl =
+ List.map
+ (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
+ fl
+ in
+ C.CoFix (i, liftedfl)
+ in
+ liftaux k
+
+let delift n t =
+ delift_from 1 n t
+
let subst arg =
let rec substaux k =
let module C = Cic in
(*CSC: per la roba che proviene da Coq questo non serve! *)
let subst_vars exp_named_subst =
(*
-prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
+debug_print ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
*)
let rec substaux k =
let module C = Cic in
let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
(match obj with
C.Constant _ -> raise ReferenceToConstant
- | C.Variable (_,_,_,params) -> params
+ | C.Variable (_,_,_,params,_) -> params
| C.CurrentProof _ -> raise ReferenceToCurrentProof
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
in
(*
-prerr_endline "\n\n---- BEGIN " ;
-prerr_endline ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-prerr_endline ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst)) ;
-prerr_endline ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst')) ;
+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
(*
-prerr_endline ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'')) ;
-prerr_endline "---- END\n\n " ;
+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'')
)
let params =
let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
(match obj with
- C.Constant (_,_,_,params) -> params
+ C.Constant (_,_,_,params,_) -> params
| C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof (_,_,_,_,params) -> params
+ | C.CurrentProof (_,_,_,_,params,_) -> params
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
in
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof _ -> raise ReferenceToCurrentProof
- | C.InductiveDefinition (_,params,_) -> params
+ | C.InductiveDefinition (_,params,_,_) -> params
)
in
let exp_named_subst'' =
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof _ -> raise ReferenceToCurrentProof
- | C.InductiveDefinition (_,params,_) -> params
+ | C.InductiveDefinition (_,params,_,_) -> params
)
in
let exp_named_subst'' =
| _::tl -> filter_and_lift tl
(*
| (uri,_)::tl ->
-prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
-if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
-prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-if List.mem uri params then prerr_endline "---- OK2" ;
+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
substaux 1
;;
-(* lift_meta [t_1 ; ... ; t_n] t *)
+(* subst_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 subst_meta l t =
let module C = Cic in
if l = [] then t else
let rec aux k = function
projects / helm.git / blobdiff