X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=3b8e4ad221646ba6f0e949eb1250e2ba04e477bb;hb=bbe7741f3bbaacb93f2876c018dace82f5e929b8;hp=d18458e2bb711f486e9f5fe557c6390cffb48c3c;hpb=b939b80860c675c83554d5d2e1a19ee9d233a34d;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index d18458e2b..3b8e4ad22 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -47,7 +47,7 @@ let reset_counters () =
  metasenv_length := 0;
  context_length := 0
 let print_counters () =
-  prerr_endline (Printf.sprintf
+  debug_print (Printf.sprintf
 "apply_subst: %d
 apply_subst_context: %d
 apply_subst_metasenv: %d
@@ -71,8 +71,9 @@ context length: %d (avg = %.2f)
 exception MetaSubstFailure of string
 exception Uncertain of string
 exception AssertFailure of string
+exception DeliftingARelWouldCaptureAFreeVariable;;
 
-let debug_print = prerr_endline
+let debug_print = fun _ -> ()
 
 type substitution = (int * (Cic.context * Cic.term)) list
 
@@ -83,7 +84,7 @@ let rec deref subst =
       Cic.Meta(n,l) as t -> 
 	(try 
 	   deref subst
-	     (CicSubstitution.lift_meta 
+	     (CicSubstitution.subst_meta 
 		l (third (CicUtil.lookup_subst n subst))) 
 	 with 
 	   CicUtil.Subst_not_found _ -> t)
@@ -183,7 +184,7 @@ let apply_subst_gen ~appl_fun subst term =
     | C.Meta (i, l) -> 
         (try
           let (_, t,_) = lookup_subst i subst in
-          um_aux (S.lift_meta l t)
+          um_aux (S.subst_meta l t)
         with CicUtil.Subst_not_found _ -> 
 	  (* unconstrained variable, i.e. free in subst*)
           let l' =
@@ -231,17 +232,6 @@ let apply_subst_gen ~appl_fun subst term =
 ;;
 
 let apply_subst =
-(* CSC: old code that never performs beta reduction
-  let appl_fun um_aux he tl =
-    let tl' = List.map um_aux tl in
-      begin
-       match um_aux he with
-          Cic.Appl l -> Cic.Appl (l@tl')
-        | he' -> Cic.Appl (he'::tl')
-      end
-  in
-  apply_subst_gen ~appl_fun
-*)
   let appl_fun um_aux he tl =
     let tl' = List.map um_aux tl in
     let t' =
@@ -251,18 +241,7 @@ let apply_subst =
     in
      begin
       match he with
-         Cic.Meta (m,_) ->
-          let rec beta_reduce =
-           function
-              (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
-                let he'' = CicSubstitution.subst he' t in
-                 if tl' = [] then
-                  he''
-                 else
-                  beta_reduce (Cic.Appl(he''::tl'))
-            | t -> t
-          in
-           beta_reduce t'
+         Cic.Meta (m,_) -> CicReduction.head_beta_reduce t'
        | _ -> t'
      end
   in
@@ -594,10 +573,10 @@ let rec restrict subst to_be_restricted metasenv =
             (ppterm subst term)
 	  in 
           (* DEBUG
-          prerr_endline error_msg;
-          prerr_endline ("metasenv = \n" ^ (ppmetasenv metasenv subst));
-          prerr_endline ("subst = \n" ^ (ppsubst subst)); 
-          prerr_endline ("context = \n" ^ (ppcontext subst context)); *)
+          debug_print error_msg;
+          debug_print ("metasenv = \n" ^ (ppmetasenv metasenv subst));
+          debug_print ("subst = \n" ^ (ppsubst subst)); 
+          debug_print ("context = \n" ^ (ppcontext subst context)); *)
           raise (MetaSubstFailure error_msg))) 
       subst ([], []) 
   in
@@ -613,7 +592,7 @@ let delift n subst context metasenv l t =
    otherwise the occur check does not make sense *)
 
 (*
- prerr_endline ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
+ debug_print ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
  al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l)))); 
 *)
 
@@ -657,7 +636,7 @@ let delift n subst context metasenv l t =
      | C.Meta (i, l1) as t -> 
          (try
            let (_,t,_) = CicUtil.lookup_subst i subst in
-             deliftaux k (CicSubstitution.lift_meta l1 t)
+             deliftaux k (CicSubstitution.subst_meta l1 t)
          with CicUtil.Subst_not_found _ ->
            (* see the top level invariant *)
            if (i = n) then 
@@ -738,7 +717,7 @@ let delift n subst context metasenv l t =
       (* order (in the sense of alpha-conversion). See comment above  *)
       (* related to the delift function.                              *)
 (* debug_print "First Order UnificationFailure during delift" ;
-prerr_endline(sprintf
+debug_print(sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)
         (String.concat "; "
@@ -757,6 +736,144 @@ prerr_endline(sprintf
     res, metasenv, subst
 ;;
 
+(* delifts a term t of n levels strating from k, that is changes (Rel m)
+ * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails
+ *)
+let delift_rels_from subst metasenv k n =
+ let rec liftaux subst metasenv k =
+  let module C = Cic in
+   function
+      C.Rel m ->
+       if m < k then
+        C.Rel m, subst, metasenv
+       else if m < k + n then
+         raise DeliftingARelWouldCaptureAFreeVariable
+       else
+        C.Rel (m - n), subst, metasenv
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst',subst,metasenv = 
+        List.fold_right
+         (fun (uri,t) (l,subst,metasenv) ->
+           let t',subst,metasenv = liftaux subst metasenv k t in
+            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+       in
+        C.Var (uri,exp_named_subst'),subst,metasenv
+    | C.Meta (i,l) ->
+        (try
+          let (_, t,_) = lookup_subst i subst in
+           liftaux subst metasenv k (CicSubstitution.subst_meta l t)
+         with CicUtil.Subst_not_found _ -> 
+          let l',to_be_restricted,subst,metasenv =
+           let rec aux con l subst metasenv =
+            match l with
+               [] -> [],[],subst,metasenv
+             | he::tl ->
+                let tl',to_be_restricted,subst,metasenv =
+                 aux (con + 1) tl subst metasenv in
+                let he',more_to_be_restricted,subst,metasenv =
+                 match he with
+                    None -> None,[],subst,metasenv
+                  | Some t ->
+                     try
+                      let t',subst,metasenv = liftaux subst metasenv k t in
+                       Some t',[],subst,metasenv
+                     with
+                      DeliftingARelWouldCaptureAFreeVariable ->
+                       None,[i,con],subst,metasenv
+                in
+                 he'::tl',more_to_be_restricted@to_be_restricted,subst,metasenv
+           in
+            aux 1 l subst metasenv in
+          let metasenv,subst = restrict subst to_be_restricted metasenv in
+           C.Meta(i,l'),subst,metasenv)
+    | C.Sort _ as t -> t,subst,metasenv
+    | C.Implicit _ as t -> t,subst,metasenv
+    | C.Cast (te,ty) ->
+       let te',subst,metasenv = liftaux subst metasenv k te in
+       let ty',subst,metasenv = liftaux subst metasenv k ty in
+        C.Cast (te',ty'),subst,metasenv
+    | C.Prod (n,s,t) ->
+       let s',subst,metasenv = liftaux subst metasenv k s in
+       let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+        C.Prod (n,s',t'),subst,metasenv
+    | C.Lambda (n,s,t) ->
+       let s',subst,metasenv = liftaux subst metasenv k s in
+       let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+        C.Lambda (n,s',t'),subst,metasenv
+    | C.LetIn (n,s,t) ->
+       let s',subst,metasenv = liftaux subst metasenv k s in
+       let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+        C.LetIn (n,s',t'),subst,metasenv
+    | C.Appl l ->
+       let l',subst,metasenv =
+        List.fold_right
+         (fun t (l,subst,metasenv) ->
+           let t',subst,metasenv = liftaux subst metasenv k t in
+            t'::l,subst,metasenv) l ([],subst,metasenv) in
+       C.Appl l',subst,metasenv
+    | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst',subst,metasenv = 
+        List.fold_right
+         (fun (uri,t) (l,subst,metasenv) ->
+           let t',subst,metasenv = liftaux subst metasenv k t in
+            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+       in
+        C.Const (uri,exp_named_subst'),subst,metasenv
+    | C.MutInd (uri,tyno,exp_named_subst) ->
+       let exp_named_subst',subst,metasenv = 
+        List.fold_right
+         (fun (uri,t) (l,subst,metasenv) ->
+           let t',subst,metasenv = liftaux subst metasenv k t in
+            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+       in
+        C.MutInd (uri,tyno,exp_named_subst'),subst,metasenv
+    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+       let exp_named_subst',subst,metasenv = 
+        List.fold_right
+         (fun (uri,t) (l,subst,metasenv) ->
+           let t',subst,metasenv = liftaux subst metasenv k t in
+            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+       in
+        C.MutConstruct (uri,tyno,consno,exp_named_subst'),subst,metasenv
+    | C.MutCase (sp,i,outty,t,pl) ->
+       let outty',subst,metasenv = liftaux subst metasenv k outty in
+       let t',subst,metasenv = liftaux subst metasenv k t in
+       let pl',subst,metasenv =
+        List.fold_right
+         (fun t (l,subst,metasenv) ->
+           let t',subst,metasenv = liftaux subst metasenv k t in
+            t'::l,subst,metasenv) pl ([],subst,metasenv)
+       in
+        C.MutCase (sp,i,outty',t',pl'),subst,metasenv
+    | C.Fix (i, fl) ->
+       let len = List.length fl in
+       let liftedfl,subst,metasenv =
+        List.fold_right
+         (fun (name, i, ty, bo) (l,subst,metasenv) ->
+           let ty',subst,metasenv = liftaux subst metasenv k ty in
+           let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
+            (name,i,ty',bo')::l,subst,metasenv
+         ) fl ([],subst,metasenv)
+       in
+        C.Fix (i, liftedfl),subst,metasenv
+    | C.CoFix (i, fl) ->
+       let len = List.length fl in
+       let liftedfl,subst,metasenv =
+        List.fold_right
+         (fun (name, ty, bo) (l,subst,metasenv) ->
+           let ty',subst,metasenv = liftaux subst metasenv k ty in
+           let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
+            (name,ty',bo')::l,subst,metasenv
+         ) fl ([],subst,metasenv)
+       in
+        C.CoFix (i, liftedfl),subst,metasenv
+ in
+  liftaux subst metasenv k
+
+let delift_rels subst metasenv n t =
+  delift_rels_from subst metasenv 1 n t
+ 
+
 (**** END OF DELIFT ****)