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 rec liftaux k =
| 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) ->
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
aux 0 t
;;
+Deannotate.lift := lift;;