exception ReferenceToConstant;;
exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
-exception DeliftingWouldCaptureAFreeVariable;;
let debug_print = fun _ -> ()
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
- raise DeliftingWouldCaptureAFreeVariable
- 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
List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
in
C.Var (uri,exp_named_subst')
- | C.Meta (i, l) as t ->
+ | C.Meta (i, l) ->
let l' =
List.map
(function
(*CSC: per la roba che proviene da Coq questo non serve! *)
let subst_vars exp_named_subst =
(*
-debug_print ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
+debug_print (lazy ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS")) ;
*)
let rec substaux k =
let module C = Cic in
)
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')) ;
+debug_print (lazy "\n\n---- BEGIN ") ;
+debug_print (lazy ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
+debug_print (lazy ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst))) ;
+debug_print (lazy ("----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 " ;
+debug_print (lazy ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst''))) ;
+debug_print (lazy "---- END\n\n ") ;
*)
C.Var (uri,exp_named_subst'')
)
- | C.Meta (i, l) as t ->
+ | C.Meta (i, l) ->
let l' =
List.map
(function
| _::tl -> filter_and_lift tl
(*
| (uri,_)::tl ->
-debug_print ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
+debug_print (lazy ("---- 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" ;
+exp_named_subst' then debug_print (lazy "---- OK1") ;
+debug_print (lazy ("++++ 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 (lazy "---- OK2") ;
filter_and_lift tl
*)
in