X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fcic_unification%2FcicMetaSubst.ml;h=f082fc23092d6aa1074e54426dbb4ad2994ac170;hb=d6a96d7ae2a320e390ce60b0ee30feebf9f2ee28;hp=c097eacf281869b9ff532d8e127ec80ac5d75d82;hpb=b20889b47bf949b17a6297ac39a5c0df0301de9e;p=helm.git

diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml
index c097eacf2..f082fc230 100644
--- a/components/cic_unification/cicMetaSubst.ml
+++ b/components/cic_unification/cicMetaSubst.ml
@@ -247,9 +247,11 @@ let apply_subst =
        | _ -> t'
      end
   in
-  fun s t ->
+  fun subst t ->
 (*     incr apply_subst_counter; *)
-    apply_subst_gen ~appl_fun s t
+match subst with
+   [] -> t
+ | _ -> apply_subst_gen ~appl_fun subst t
 ;;
 
 let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst"
@@ -257,7 +259,10 @@ let apply_subst s t =
   profiler.HExtlib.profile (apply_subst s) t
 
 
-let rec apply_subst_context subst context =
+let apply_subst_context subst context =
+ match subst with
+    [] -> context
+  | _ ->
 (*
   incr apply_subst_context_counter;
   context_length := !context_length + List.length context;
@@ -284,6 +289,9 @@ let apply_subst_metasenv subst metasenv =
   incr apply_subst_metasenv_counter;
   metasenv_length := !metasenv_length + List.length metasenv;
 *)
+match subst with
+   [] -> metasenv
+ | _ ->
   List.map
     (fun (n, context, ty) ->
       (n, apply_subst_context subst context, apply_subst subst ty))
@@ -305,6 +313,17 @@ let ppterm_in_context ~metasenv subst term context =
  in
   ppterm_in_name_context ~metasenv subst term name_context
 
+let ppterm_in_context_ref = ref ppterm_in_context
+let set_ppterm_in_context f =
+ ppterm_in_context_ref := f
+let use_low_level_ppterm_in_context = ref false
+
+let ppterm_in_context ~metasenv subst term context =
+ if !use_low_level_ppterm_in_context then
+  ppterm_in_context ~metasenv subst term context
+ else
+  !ppterm_in_context_ref ~metasenv subst term context
+
 let ppcontext' ~metasenv ?(sep = "\n") subst context =
  let separate s = if s = "" then "" else s ^ sep in
   List.fold_right 
@@ -327,9 +346,10 @@ let ppcontext' ~metasenv ?(sep = "\n") subst context =
 let ppsubst_unfolded ~metasenv subst =
   String.concat "\n"
     (List.map
-      (fun (idx, (c, t,_)) ->
+      (fun (idx, (c, t,ty)) ->
         let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
-         sprintf "%s |- ?%d:= %s" context idx
+         sprintf "%s |- ?%d : %s := %s" context idx
+(ppterm_in_name_context ~metasenv [] ty name_context)
           (ppterm_in_name_context ~metasenv subst t name_context))
        subst)
 (* 
@@ -340,9 +360,9 @@ let ppsubst_unfolded ~metasenv subst =
 let ppsubst ~metasenv subst =
   String.concat "\n"
     (List.map
-      (fun (idx, (c, t, _)) ->
+      (fun (idx, (c, t, ty)) ->
         let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in
-         sprintf "%s |- ?%d:= %s" context idx
+         sprintf "%s |- ?%d : %s := %s" context idx (ppterm_in_name_context ~metasenv [] ty name_context)
           (ppterm_in_name_context ~metasenv [] t name_context))
        subst)
 ;;
@@ -468,6 +488,9 @@ let rec force_does_not_occur subst to_be_restricted t =
  (!more_to_be_restricted, res)
  
 let rec restrict subst to_be_restricted metasenv =
+ match to_be_restricted with
+ | [] -> metasenv, subst
+ | _ ->
   let names_of_context_indexes context indexes =
     String.concat ", "
       (List.map
@@ -596,9 +619,7 @@ let rec restrict subst to_be_restricted metasenv =
           raise (MetaSubstFailure error_msg))) 
       subst ([], []) 
   in
-  match more_to_be_restricted @ more_to_be_restricted' with
-  | [] -> (metasenv, subst)
-  | l -> restrict subst l metasenv
+   restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv
 ;;
 
 (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)(*Andrea: maybe not*)
@@ -625,11 +646,11 @@ let delift n subst context metasenv l t =
   let rec deliftaux k =
    let module C = Cic in
     function
-       C.Rel m -> 
+     | C.Rel m as t-> 
          if m <=k then
-          C.Rel m
+          t
          else
-          (try
+           (try
             match List.nth context (m-k-1) with
                Some (_,C.Def (t,_)) ->
                 (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
@@ -643,7 +664,7 @@ let delift n subst context metasenv l t =
                 C.Rel ((position (m-k) l) + k)
              | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))
            with
-            Failure _ ->
+            Failure _ -> 
              raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux"))
           )
      | C.Var (uri,exp_named_subst) ->
@@ -771,9 +792,9 @@ let delift_rels_from subst metasenv k n =
  let rec liftaux subst metasenv k =
   let module C = Cic in
    function
-      C.Rel m ->
+      C.Rel m as t ->
        if m < k then
-        C.Rel m, subst, metasenv
+        t, subst, metasenv
        else if m < k + n then
          raise DeliftingARelWouldCaptureAFreeVariable
        else