X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;h=a30a036cb42dc7726c1720906d706f903b0fcf30;hb=489ee5290cce2247291b8c5c53b98d493e7f6b99;hp=38f2e7a6d484c617b8e838d523a3372843e599c6;hpb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 38f2e7a6d..a30a036cb 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 exception CannotSubstInMeta;;
 exception RelToHiddenHypothesis;;
 exception ReferenceToVariable;;
@@ -30,7 +32,9 @@ exception ReferenceToConstant;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
-let lift n =
+let debug_print = fun _ -> ()
+
+let lift_from k n =
  let rec liftaux k =
   let module C = Cic in
    function
@@ -95,10 +99,13 @@ let lift n =
        in
         C.CoFix (i, liftedfl)
  in
+ liftaux k
+
+let lift n t =
   if n = 0 then
-   (function t -> t)
+   t
   else
-   liftaux 1
+   lift_from 1 n t
 ;;
 
 let subst arg =
@@ -116,7 +123,7 @@ let subst arg =
         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
@@ -184,9 +191,9 @@ let subst arg =
 (*CSC: dovrebbe diventare da sinistra verso destra:                      *)
 (*CSC: t{a=a/A;b/a} ==> \H:a=a.H{b/a} ==> \H:b=b.H                       *)
 (*CSC: per la roba che proviene da Coq questo non serve!                 *)
-let subst_vars exp_named_subst =
+let subst_vars exp_named_subst t =
 (*
-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
@@ -202,30 +209,30 @@ prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
         with
          Not_found ->
           let params =
-           let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph 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 (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'')
        )
-    | C.Meta (i, l) as t -> 
+    | C.Meta (i, l) -> 
        let l' =
         List.map
          (function
@@ -251,11 +258,11 @@ prerr_endline "---- END\n\n " ;
     | C.Appl _ -> assert false
     | C.Const (uri,exp_named_subst')  ->
        let params =
-        let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+        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
@@ -265,12 +272,12 @@ prerr_endline "---- END\n\n " ;
          C.Const (uri,exp_named_subst'')
     | C.MutInd (uri,typeno,exp_named_subst') ->
        let params =
-        let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+        let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         (match obj with
             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'' =
@@ -279,12 +286,12 @@ prerr_endline "---- END\n\n " ;
          C.MutInd (uri,typeno,exp_named_subst'')
     | C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
        let params =
-        let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+        let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         (match obj with
             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'' =
@@ -326,23 +333,25 @@ 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
    List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @
     (filter_and_lift exp_named_subst)
  in
-  substaux 1
+  if exp_named_subst = [] then t
+  else substaux 1 t
 ;;
 
-(* 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
@@ -416,3 +425,4 @@ let lift_meta l t =
  in
   aux 0 t          
 ;;
+