X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;h=17ee01b5333c3638e041d5cde49453123e5275c3;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=68276d74bac39f9a68b34cc5349c463908eae610;hpb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 68276d74b..17ee01b53 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -25,6 +25,10 @@
 
 exception CannotSubstInMeta;;
 exception RelToHiddenHypothesis;;
+exception ReferenceToVariable;;
+exception ReferenceToConstant;;
+exception ReferenceToCurrentProof;;
+exception ReferenceToInductiveDefinition;;
 
 let lift n =
  let rec liftaux k =
@@ -35,7 +39,11 @@ let lift n =
         C.Rel m
        else
         C.Rel (m + n)
-    | C.Var _  as t -> t
+    | 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
@@ -46,18 +54,29 @@ let lift n =
        in
         C.Meta(i,l')
     | C.Sort _ as t -> t
-    | C.Implicit 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 _ as t -> t
-    | C.Abst _  as t -> t
-    | C.MutInd _ as t -> t
-    | C.MutConstruct _ as t -> t
-    | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
-       C.MutCase (sp, cookingsno, i, liftaux k outty, liftaux k t,
+    | 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
@@ -92,7 +111,11 @@ let subst arg =
          | n when n < k -> t
          | _            -> C.Rel (n - 1)
        )
-    | C.Var _ as t  -> t
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        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 -> 
        let l' =
         List.map
@@ -103,7 +126,7 @@ let subst arg =
        in
         C.Meta(i,l')
     | C.Sort _ as t -> t
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> 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)
@@ -117,12 +140,23 @@ let subst arg =
           | _ as he' -> C.Appl (he'::tl')
         end
     | C.Appl _ -> assert false
-    | C.Const _ as t -> t
-    | C.Abst _ as t -> t
-    | C.MutInd _ as t -> t
-    | C.MutConstruct _ as t -> t
-    | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
-       C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t,
+    | C.Const (uri,exp_named_subst)  ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
+       in
+        C.Const (uri,exp_named_subst')
+    | C.MutInd (uri,typeno,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
+       in
+        C.MutInd (uri,typeno,exp_named_subst')
+    | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
+       in
+        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,
         List.map (substaux k) pl)
     | C.Fix (i,fl) ->
        let len = List.length fl in
@@ -144,41 +178,172 @@ let subst arg =
   substaux 1
 ;;
 
-let undebrujin_inductive_def uri =
- function
-    Cic.InductiveDefinition (dl,params,n_ind_params) ->
-     let dl' =
-      List.map
-       (fun (name,inductive,arity,constructors) ->
-         let constructors' =
-          List.map
-           (fun (name,ty,r) ->
-             let ty' =
-              let counter = ref (List.length dl) in
-               List.fold_right
-                (fun _ ->
-                  decr counter ;
-                  subst (Cic.MutInd (uri,0,!counter))
-                ) dl ty
-             in
-              (name,ty',r)
-           ) constructors
+(*CSC: i controlli di tipo debbono essere svolti da destra a             *)
+(*CSC: sinistra: i{B/A;b/a} ==> a{B/A;b/a} ==> a{b/a{B/A}} ==> b         *)
+(*CSC: la sostituzione ora e' implementata in maniera simultanea, ma     *)
+(*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 =
+(*
+prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
+*)
+ let rec substaux k =
+  let module C = Cic in
+   function
+      C.Rel _ as t -> t
+    | C.Var (uri,exp_named_subst') ->
+       (try
+         let (_,arg) =
+          List.find
+           (function (varuri,_) -> UriManager.eq uri varuri) exp_named_subst
          in
-          (name,inductive,arity,constructors')
-       ) dl
-      in
-       Cic.InductiveDefinition (dl', params, n_ind_params)
-  | obj -> obj
+          lift (k -1) arg
+        with
+         Not_found ->
+          let params =
+           (match CicEnvironment.get_cooked_obj ~trust:true uri with
+               C.Constant _ -> raise ReferenceToConstant
+             | 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')) ;
+*)
+           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 " ;
+*)
+            C.Var (uri,exp_named_subst'')
+       )
+    | C.Meta (i, l) as t -> 
+       let l' =
+        List.map
+         (function
+             None -> None
+           | Some t -> Some (substaux k t)
+         ) l
+       in
+        C.Meta(i,l')
+    | C.Sort _ as t -> t
+    | C.Implicit _ as t -> 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.Appl (he::tl) ->
+       (* Invariant: no Appl applied to another Appl *)
+       let tl' = List.map (substaux k) tl in
+        begin
+         match substaux k he with
+            C.Appl l -> C.Appl (l@tl')
+          | _ as he' -> C.Appl (he'::tl')
+        end
+    | C.Appl _ -> assert false
+    | C.Const (uri,exp_named_subst')  ->
+       let params =
+        (match CicEnvironment.get_cooked_obj ~trust:true uri with
+            C.Constant (_,_,_,params) -> params
+          | C.Variable _ -> raise ReferenceToVariable
+          | C.CurrentProof (_,_,_,_,params) -> params
+          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+        )
+       in
+        let exp_named_subst'' =
+         substaux_in_exp_named_subst uri k exp_named_subst' params
+        in
+         C.Const (uri,exp_named_subst'')
+    | C.MutInd (uri,typeno,exp_named_subst') ->
+       let params =
+        (match CicEnvironment.get_cooked_obj ~trust:true uri with
+            C.Constant _ -> raise ReferenceToConstant
+          | C.Variable _ -> raise ReferenceToVariable
+          | C.CurrentProof _ -> raise ReferenceToCurrentProof
+          | C.InductiveDefinition (_,params,_) -> params
+        )
+       in
+        let exp_named_subst'' =
+         substaux_in_exp_named_subst uri k exp_named_subst' params
+        in
+         C.MutInd (uri,typeno,exp_named_subst'')
+    | C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
+       let params =
+        (match CicEnvironment.get_cooked_obj ~trust:true uri with
+            C.Constant _ -> raise ReferenceToConstant
+          | C.Variable _ -> raise ReferenceToVariable
+          | C.CurrentProof _ -> raise ReferenceToCurrentProof
+          | C.InductiveDefinition (_,params,_) -> params
+        )
+       in
+        let exp_named_subst'' =
+         substaux_in_exp_named_subst uri k exp_named_subst' params
+        in
+         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,
+        List.map (substaux k) pl)
+    | C.Fix (i,fl) ->
+       let len = List.length fl in
+       let substitutedfl =
+        List.map
+         (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
+          fl
+       in
+        C.Fix (i, substitutedfl)
+    | C.CoFix (i,fl) ->
+       let len = List.length fl in
+       let substitutedfl =
+        List.map
+         (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
+          fl
+       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,t)::tl when
+        List.for_all
+         (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst'
+        &&
+         List.mem uri params
+       ->
+        (uri,lift (k-1) t)::(filter_and_lift tl)
+    | _::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" ;
+        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
 ;;
 
-(* l is the relocation list *)
-
+(* lift_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 module C = Cic in
-    if l = [] then t else 
-    let rec aux k = function
+ let module C = Cic in
+  if l = [] then t else 
+   let rec aux k = function
       C.Rel n as t -> 
-	if n <= k then t else 
+        if n <= k then t else 
          (try
            match List.nth l (n-k-1) with
               None -> raise RelToHiddenHypothesis
@@ -186,7 +351,11 @@ let lift_meta l t =
           with
            (Failure _) -> assert false
          )
-    | C.Var _ as t  -> t
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
+       in
+        C.Var (uri,exp_named_subst')
     | C.Meta (i,l) ->
        let l' =
         List.map
@@ -201,19 +370,29 @@ let lift_meta l t =
        in
         C.Meta(i,l')
     | C.Sort _ as t -> t
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> 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.Appl l -> C.Appl (List.map (aux k) l)
-    | C.Const _ as t -> t
-    | C.Abst _ as t -> t
-    | C.MutInd _ as t -> t
-    | C.MutConstruct _ as t -> t
-    | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
-       C.MutCase (sp,cookingsno,i,aux k outt, aux k t,
-        List.map (aux k) pl)
+    | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
+       in
+        C.Const (uri,exp_named_subst')
+    | C.MutInd (uri,typeno,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
+       in
+        C.MutInd (uri,typeno,exp_named_subst')
+    | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
+       in
+        C.MutConstruct (uri,typeno,consno,exp_named_subst')
+    | C.MutCase (sp,i,outt,t,pl) ->
+       C.MutCase (sp,i,aux k outt, aux k t, List.map (aux k) pl)
     | C.Fix (i,fl) ->
        let len = List.length fl in
        let substitutedfl =
@@ -233,105 +412,3 @@ let lift_meta l t =
  in
   aux 0 t          
 ;;
-
-(************************************************************************)
-(*CSC: spostare in cic_unification *)
-
-(* the delift function takes in input an ordered list of integers [n1,...,nk]
-   and a term t, and relocates rel(nk) to k. Typically, the list of integers 
-   is a parameter of a metavariable occurrence. *)
-
-exception NotInTheList;;
-
-let position n =
-  let rec aux k =
-   function 
-       [] -> raise NotInTheList
-     | (Some (Cic.Rel m))::_ when m=n -> k
-     | _::tl -> aux (k+1) tl in
-  aux 1
-;;
- 
-let restrict to_be_restricted =
-  let rec erase i n = 
-    function
-	[] -> []
-      |	_::tl when List.mem (n,i) to_be_restricted ->
-	  None::(erase (i+1) n tl) 
-      | he::tl -> he::(erase (i+1) n tl) in
-  let rec aux =
-    function 
-	[] -> []
-      |	(n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
-  aux
-;;
-
-
-let delift context metasenv l t =
- let to_be_restricted = ref [] in
- let rec deliftaux k =
-  let module C = Cic in
-   function
-      C.Rel m -> 
-        if m <=k then
-         C.Rel m   (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
-                   (*CSC: deliftato la regola per il LetIn                 *)
-        else
-	 (match List.nth context (m-k-1) with
-	   Some (_,C.Def t) -> deliftaux k (lift m t)
-	 | Some (_,C.Decl t) ->
-            (* It may augment to_be_restricted *)
-            ignore (deliftaux k (lift m t)) ;
-            C.Rel ((position (m-k) l) + k)
-	 | None -> raise RelToHiddenHypothesis)
-    | C.Var _  as t -> t
-    | C.Meta (i, l1) as t -> 
-       let rec deliftl j =
-        function
-           [] -> []
-         | None::tl -> None::(deliftl (j+1) tl)
-         | (Some t)::tl ->
-            let l1' = (deliftl (j+1) tl) in
-             try
-              Some (deliftaux k t)::l1'
-             with
-                RelToHiddenHypothesis
-              | NotInTheList ->
-                 to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
-       in
-        let l' = deliftl 1 l1 in
-         C.Meta(i,l')
-    | C.Sort _ as t -> t
-    | C.Implicit as t -> t
-    | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
-    | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
-    | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
-    | C.Appl l -> C.Appl (List.map (deliftaux k) l)
-    | C.Const _ as t -> t
-    | C.Abst _  as t -> t
-    | C.MutInd _ as t -> t
-    | C.MutConstruct _ as t -> t
-    | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
-       C.MutCase (sp, cookingsno, i, deliftaux k outty, deliftaux k t,
-        List.map (deliftaux k) pl)
-    | C.Fix (i, fl) ->
-       let len = List.length fl in
-       let liftedfl =
-        List.map
-         (fun (name, i, ty, bo) -> (name, i, deliftaux k ty, deliftaux (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, deliftaux k ty, deliftaux (k+len) bo))
-          fl
-       in
-        C.CoFix (i, liftedfl)
- in
-   let res = deliftaux 0 t in
-   res, restrict !to_be_restricted metasenv
-;;