X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicMetaSubst.ml;h=8db1cf82f31c3759a33cb4f5b14e850d2a5c6c22;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=8d53495bff9024f6adc8247f739da57d83470829;hpb=81ef66d9ad4cf863a770664190f96653e9777a57;p=helm.git

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index 8d53495bf..8db1cf82f 100644
--- a/helm/software/components/cic_unification/cicMetaSubst.ml
+++ b/helm/software/components/cic_unification/cicMetaSubst.ml
@@ -198,7 +198,7 @@ let apply_subst_gen ~appl_fun subst term =
     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
+    | C.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t)
     | C.Appl (hd :: tl) -> appl_fun um_aux hd tl
     | C.Appl _ -> assert false
     | C.Const (uri,exp_named_subst) ->
@@ -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;
@@ -269,11 +274,7 @@ let rec apply_subst_context subst context =
           let t' = apply_subst subst t in
           Some (n, Cic.Decl t') :: context
       | Some (n, Cic.Def (t, ty)) ->
-          let ty' =
-            match ty with
-            | None -> None
-            | Some ty -> Some (apply_subst subst ty)
-          in
+          let ty' = apply_subst subst ty in
           let t' = apply_subst subst t in
           Some (n, Cic.Def (t', ty')) :: context
       | None -> None :: context)
@@ -284,6 +285,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))
@@ -293,67 +297,78 @@ let apply_subst_metasenv subst metasenv =
 
 (***** Pretty printing functions ******)
 
-let ppterm subst term = CicPp.ppterm (apply_subst subst term)
-
-let ppterm_in_name_context subst term name_context =
- CicPp.pp (apply_subst subst term) name_context
+let ppterm ~metasenv subst term =
+ CicPp.ppterm ~metasenv (apply_subst subst term)
 
-let ppterm_in_context subst term context =
+let ppterm_in_context ~metasenv subst term context =
  let name_context =
   List.map (function None -> None | Some (n,_) -> Some n) context
  in
-  ppterm_in_name_context subst term name_context
+  CicPp.pp ~metasenv (apply_subst 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 ppcontext' ?(sep = "\n") subst context =
+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 
-   (fun context_entry (i,name_context) ->
+   (fun context_entry (i,context) ->
      match context_entry with
         Some (n,Cic.Decl t) ->
          sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
-          (ppterm_in_name_context subst t name_context), (Some n)::name_context
+          (ppterm_in_context ~metasenv subst t context),
+          context_entry::context
       | Some (n,Cic.Def (bo,ty)) ->
          sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
-          (match ty with
-              None -> "_"
-            | Some ty -> ppterm_in_name_context subst ty name_context)
-          (ppterm_in_name_context subst bo name_context), (Some n)::name_context
+          (ppterm_in_context ~metasenv subst ty context)
+          (ppterm_in_context ~metasenv subst bo context),
+          context_entry::context
        | None ->
-          sprintf "%s_ :? _" (separate i), None::name_context
+          sprintf "%s_ :? _" (separate i), context_entry::context
     ) context ("",[])
 
-let ppsubst_unfolded subst =
+let ppsubst_unfolded ~metasenv subst =
   String.concat "\n"
     (List.map
-      (fun (idx, (c, t,_)) ->
-        let context,name_context = ppcontext' ~sep:"; " subst c in
-         sprintf "%s |- ?%d:= %s" context idx
-          (ppterm_in_name_context subst t name_context))
+      (fun (idx, (c, t,ty)) ->
+        let scontext,context = ppcontext' ~metasenv ~sep:"; " subst c in
+         sprintf "%s |- ?%d : %s := %s" scontext idx
+(ppterm_in_context ~metasenv [] ty context)
+          (ppterm_in_context ~metasenv subst t context))
        subst)
 (* 
         Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
       subst) *)
 ;;
 
-let ppsubst subst =
+let ppsubst ~metasenv subst =
   String.concat "\n"
     (List.map
-      (fun (idx, (c, t, _)) ->
-        let context,name_context = ppcontext' ~sep:"; " [] c in
-         sprintf "%s |- ?%d:= %s" context idx
-          (ppterm_in_name_context [] t name_context))
+      (fun (idx, (c, t, ty)) ->
+        let scontext,context = ppcontext' ~metasenv ~sep:"; " [] c in
+         sprintf "%s |- ?%d : %s := %s" scontext idx (ppterm_in_context ~metasenv [] ty context)
+          (ppterm_in_context ~metasenv [] t context))
        subst)
 ;;
 
-let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
+let ppcontext ~metasenv ?sep subst context =
+ fst (ppcontext' ~metasenv ?sep subst context)
 
 let ppmetasenv ?(sep = "\n") subst metasenv =
   String.concat sep
     (List.map
       (fun (i, c, t) ->
-        let context,name_context = ppcontext' ~sep:"; " subst c in
-         sprintf "%s |- ?%d: %s" context i
-          (ppterm_in_name_context subst t name_context))
+        let scontext,context = ppcontext' ~metasenv ~sep:"; " subst c in
+         sprintf "%s |- ?%d: %s" scontext i
+          (ppterm_in_context ~metasenv subst t context))
       (List.filter
         (fun (i, _, _) -> not (List.mem_assoc i subst))
         metasenv))
@@ -420,7 +435,8 @@ let rec force_does_not_occur subst to_be_restricted t =
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
     | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
     | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
-    | C.LetIn (name,so,dest) -> C.LetIn (name, aux k so, aux (k+1) dest)
+    | C.LetIn (name,so,ty,dest) ->
+       C.LetIn (name, aux k so, aux k ty, aux (k+1) dest)
     | C.Appl l -> C.Appl (List.map (aux k) l)
     | C.Var (uri,exp_named_subst) ->
         let exp_named_subst' =
@@ -465,6 +481,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
@@ -489,14 +508,11 @@ let rec restrict subst to_be_restricted metasenv =
           force_does_not_occur subst to_be_restricted bo
         in
         let more_to_be_restricted, ty' =
-          match ty with
-          | None ->  more_to_be_restricted, None
-          | Some ty ->
-              let more_to_be_restricted', ty' =
-                force_does_not_occur subst to_be_restricted ty
-              in
-              more_to_be_restricted @ more_to_be_restricted',
-              Some ty'
+         let more_to_be_restricted', ty' =
+           force_does_not_occur subst to_be_restricted ty
+         in
+         more_to_be_restricted @ more_to_be_restricted',
+         ty'
         in
         more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
   in
@@ -583,7 +599,7 @@ let rec restrict subst to_be_restricted metasenv =
           let error_msg = lazy (sprintf
             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
             n (names_of_context_indexes context to_be_restricted) n
-            (ppterm subst term))
+            (ppterm ~metasenv subst term))
 	  in 
           (* DEBUG
           debug_print (lazy error_msg);
@@ -593,9 +609,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*)
@@ -611,7 +625,14 @@ let delift n subst context metasenv l t =
 
  let module S = CicSubstitution in
   let l =
-   let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
+   let (_, canonical_context, _) =
+    try
+     CicUtil.lookup_meta n metasenv
+    with CicUtil.Meta_not_found _ ->
+     raise (MetaSubstFailure (lazy
+      ("delifting error: the metavariable " ^ string_of_int n ^ " is not " ^
+       "declared in the metasenv")))
+    in
    List.map2 (fun ct lt ->
      match (ct, lt) with
      | None, _ -> None
@@ -622,25 +643,29 @@ 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,_)) ->
+                (try
+                  C.Rel ((position (m-k) l) + k)
+                 with
+                  NotInTheList ->
                 (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
                 (*CSC: first order unification. Does it help or does it harm? *)
                 (*CSC: ANSWER: it hurts performances since it is possible to  *)
                 (*CSC: have an exponential explosion of the size of the proof.*)
                 (*CSC: However, without this bit of reduction some "apply" in *)
                 (*CSC: the library fail (e.g. nat/nth_prime.ma).              *)
-                deliftaux k (S.lift m t)
+                  deliftaux k (S.lift m t))
              | Some (_,C.Decl 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) ->
@@ -657,7 +682,7 @@ let delift n subst context metasenv l t =
            if (i = n) then 
             raise (MetaSubstFailure (lazy (sprintf
               "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
-              i (ppterm subst t))))
+              i (ppterm ~metasenv subst t))))
           else
             begin
            (* I do not consider the term associated to ?i in subst since *)
@@ -684,7 +709,8 @@ let delift n subst context metasenv l 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.LetIn (n,s,ty,t) ->
+        C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t)
      | C.Appl l -> C.Appl (List.map (deliftaux k) l)
      | C.Const (uri,exp_named_subst) ->
         let exp_named_subst' =
@@ -741,10 +767,10 @@ debug_print(lazy (sprintf
           )))); *)
       let msg = (lazy (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
-        (ppterm subst t)
+        (ppterm ~metasenv subst t)
         (String.concat "; "
           (List.map
-            (function Some t -> ppterm subst t | None -> "_")
+            (function Some t -> ppterm ~metasenv subst t | None -> "_")
             l))))
       in
        if
@@ -768,9 +794,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
@@ -825,10 +851,11 @@ let delift_rels_from subst metasenv k n =
        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) ->
+    | C.LetIn (n,s,ty,t) ->
        let s',subst,metasenv = liftaux subst metasenv k s in
+       let ty',subst,metasenv = liftaux subst metasenv k ty in
        let t',subst,metasenv = liftaux subst metasenv (k+1) t in
-        C.LetIn (n,s',t'),subst,metasenv
+        C.LetIn (n,s',ty',t'),subst,metasenv
     | C.Appl l ->
        let l',subst,metasenv =
         List.fold_right
@@ -909,6 +936,6 @@ let fpp_gen ppf s =
   Format.pp_print_newline ppf ();
   Format.pp_print_flush ppf ()
 
-let fppsubst ppf subst = fpp_gen ppf (ppsubst subst)
+let fppsubst ppf subst = fpp_gen ppf (ppsubst ~metasenv:[] subst)
 let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
 let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv)