X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;h=a9fa1d9b19e8e86ca8c8b89621e6fa4e13c365e1;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=431fa4b50d1303c6b64a3a90462fea9f3fd8d90f;hpb=e8236af508187f6446f5af481d545d433628ee00;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index 431fa4b50..a9fa1d9b1 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -30,6 +30,8 @@ exception ReferenceToConstant;; exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; +let debug_print = fun _ -> () + let lift_from k n = let rec liftaux k = let module C = Cic in @@ -189,7 +191,7 @@ let subst arg = (*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 (lazy ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS")) ; *) let rec substaux k = let module C = Cic in @@ -214,17 +216,17 @@ prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ; ) 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 (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 (* -prerr_endline ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'')) ; -prerr_endline "---- 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'') ) @@ -329,10 +331,11 @@ prerr_endline "---- END\n\n " ; | _::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 (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 @@ -342,10 +345,10 @@ if List.mem uri params then prerr_endline "---- OK2" ; 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 @@ -419,3 +422,4 @@ let lift_meta l t = in aux 0 t ;; +