exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
-let debug_print = fun _ -> ()
+let debug = false
+let debug_print =
+ if debug then
+ fun m -> prerr_endline (Lazy.force m)
+ else
+ fun _ -> ()
+;;
-let lift_from k n =
+let lift_map k map =
let rec liftaux k =
let module C = Cic in
function
if m < k then
C.Rel m
else
- C.Rel (m + n)
+ C.Rel (map k m)
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
| 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.LetIn (n,s,ty,t) ->
+ C.LetIn (n, liftaux k s, liftaux k ty, liftaux (k+1) t)
| C.Appl l -> C.Appl (List.map (liftaux k) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
in
liftaux k
+let lift_from k n =
+ lift_map k (fun _ m -> m + n)
+
let lift n t =
if n = 0 then
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.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.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
in
-(*
-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 (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) ->
| 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.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
let exp_named_subst'' =
substaux_in_exp_named_subst uri k exp_named_subst' params
in
+if (List.map fst exp_named_subst'' <> List.map fst (List.filter (fun (uri,_) -> List.mem uri params) exp_named_subst) @ List.map fst exp_named_subst') then (
+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'))) ;
+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.MutConstruct (uri,typeno,consno,exp_named_subst'')
| C.MutCase (sp,i,outt,t,pl) ->
C.MutCase (sp,i,substaux k outt, substaux k t,
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,lift (k-1) t)::(filter_and_lift tl)
| _::tl -> filter_and_lift tl
-(*
- | (uri,_)::tl ->
-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 (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
- List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @
- (filter_and_lift exp_named_subst)
+ let res =
+ List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @
+ (filter_and_lift exp_named_subst)
+ in
+ let rec reorder =
+ function
+ [] -> []
+ | uri::tl ->
+ let he =
+ try
+ [uri,List.assoc uri res]
+ with
+ Not_found -> []
+ in
+ he@reorder tl
+ in
+ reorder params
in
if exp_named_subst = [] then t
else substaux 1 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)
- | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
+ | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k + 1) t)
| C.Appl l -> C.Appl (List.map (aux k) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
aux 0 t
;;
+Deannotate.lift := lift;;