X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=41802530bb2e004e8f68807ed9b552423885b770;hb=136fb0fde826e200ee8a0e902dbb6278b2afdeb8;hp=04f32eb2c77aaddf3ce18896f93cf6e9f95c497a;hpb=b3769ff3eb77ec8fa27ac46ec1076941a16bd3a5;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 04f32eb2c..41802530b 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -46,29 +46,29 @@ let rec force_does_not_occur subst to_be_restricted t =
  let module C = Cic in
  let more_to_be_restricted = ref [] in
  let rec aux k = function
-      C.Rel r when List.mem (r+k) to_be_restricted -> raise Occur
+      C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
     | C.Rel _
     | C.Sort _ as t -> t
     | C.Implicit -> assert false
     | C.Meta (n, l) ->
-        (try
-          aux k (CicSubstitution.lift_meta l (List.assoc n subst))
-        with Not_found ->
-          let l' =
-            let i = ref 0 in
-            List.map
-              (function
-                | None -> None
-                | Some t ->
-                    incr i;
-                    try
-                      Some (aux k t)
-                    with Occur ->
-                      more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
-                      None)
-              l
-          in
-          C.Meta (n, l'))
+       (* we do not retrieve the term associated to ?n in subst since *)
+       (* in this way we can restrict if something goes wrong         *)
+       let l' =
+         let i = ref 0 in
+         List.map
+           (function t ->
+             incr i ;
+             match t with
+                None -> None
+              | Some t ->
+                 try
+                   Some (aux k t)
+                 with Occur ->
+                   more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
+                   None)
+           l
+       in
+        C.Meta (n, l')
     | 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)
@@ -121,10 +121,13 @@ let rec restrict subst to_be_restricted metasenv =
     String.concat ", "
       (List.map
         (fun i ->
-          match List.nth context i with
-          | None -> assert false
-          | Some (n, _) -> CicPp.ppname n)
-        indexes)
+          try
+           match List.nth context i with
+           | None -> assert false
+           | Some (n, _) -> CicPp.ppname n
+          with
+           Failure _ -> assert false
+        ) indexes)
   in
   let force_does_not_occur_in_context to_be_restricted = function
     | None -> [], None
@@ -132,7 +135,7 @@ let rec restrict subst to_be_restricted metasenv =
         let (more_to_be_restricted, t') =
           force_does_not_occur subst to_be_restricted t
         in
-        more_to_be_restricted, Some (name, Cic.Decl t)
+        more_to_be_restricted, Some (name, Cic.Decl t')
     | Some (name, Cic.Def (bo, ty)) ->
         let (more_to_be_restricted, bo') =
           force_does_not_occur subst to_be_restricted bo
@@ -152,27 +155,30 @@ let rec restrict subst to_be_restricted metasenv =
   let rec erase i to_be_restricted n = function
     | [] -> [], to_be_restricted, []
     | hd::tl ->
-        let restrict_me = List.mem i to_be_restricted in
+        let more_to_be_restricted,restricted,tl' =
+         erase (i+1) to_be_restricted n tl
+        in
+        let restrict_me = List.mem i restricted in
         if restrict_me then
-          let more_to_be_restricted, restricted, new_tl =
-            erase (i+1) (i :: to_be_restricted) n tl
-          in
-          more_to_be_restricted, restricted, None :: new_tl
+         more_to_be_restricted, restricted, None:: tl'
         else
           (try
-            let more_to_be_restricted, hd' =
-              force_does_not_occur_in_context to_be_restricted hd
-            in
-            let more_to_be_restricted', restricted, tl' =
-              erase (i+1) to_be_restricted n tl
+            let more_to_be_restricted', hd' =
+              let delifted_restricted =
+               let rec aux =
+                function
+                   [] -> []
+                 | j::tl when j > i -> (j - i)::aux tl
+                 | _::tl -> aux tl
+               in
+                aux restricted
+              in
+               force_does_not_occur_in_context delifted_restricted hd
             in
-            more_to_be_restricted @ more_to_be_restricted',
-            restricted, hd' :: tl'
+             more_to_be_restricted @ more_to_be_restricted',
+             restricted, hd' :: tl'
           with Occur ->
-            let more_to_be_restricted, restricted, tl' =
-              erase (i+1) (i :: to_be_restricted) n tl
-            in
-            more_to_be_restricted, restricted, None :: tl')
+            more_to_be_restricted, (i :: restricted), None :: tl')
   in
   let (more_to_be_restricted, metasenv, subst) =
     List.fold_right
@@ -181,6 +187,10 @@ let rec restrict subst to_be_restricted metasenv =
           List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
         in
         let (more_to_be_restricted, restricted, context') =
+         (* just an optimization *)
+         if to_be_restricted = [] then
+          [],[],context
+         else
           erase 1 to_be_restricted n context
         in
         try
@@ -219,15 +229,15 @@ let rec restrict subst to_be_restricted metasenv =
 
 (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
 let delift n subst context metasenv l t =
- let l =
-  let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
-  List.map2 (fun ct lt ->
-    match (ct, lt) with
-    | None, _ -> None
-    | Some _, _ -> lt)
-    canonical_context l
- in
  let module S = CicSubstitution in
+  let l =
+   let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
+   List.map2 (fun ct lt ->
+     match (ct, lt) with
+     | None, _ -> None
+     | Some _, _ -> lt)
+     canonical_context l
+  in
   let to_be_restricted = ref [] in
   let rec deliftaux k =
    let module C = Cic in
@@ -267,24 +277,23 @@ let delift n subst context metasenv l t =
             "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
             i (CicPp.ppterm t)))
         else
-          (try
-            deliftaux k (S.lift_meta l (List.assoc i subst))
-          with Not_found ->
-            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
-                     NotInTheList
-                   | MetaSubstFailure _ ->
-                      to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
-            in
-             let l' = deliftl 1 l1 in
-              C.Meta(i,l'))
+         (* I do not consider the term associated to ?i in subst since *)
+         (* in this way I can restrict if something goes wrong.        *)
+          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
+                   NotInTheList
+                 | MetaSubstFailure _ ->
+                    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)
@@ -485,25 +494,36 @@ let apply_subst_metasenv subst metasenv =
 
 let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 
-let ppcontext ?(sep = "\n") subst context =
-  String.concat sep
-    (List.rev_map (function
-      | Some (n, Cic.Decl t) ->
-          sprintf "%s : %s" (CicPp.ppname n) (ppterm subst t)
-      | Some (n, Cic.Def (t, ty)) ->
-          sprintf "%s : %s := %s"
-            (CicPp.ppname n)
-            (match ty with None -> "_" | Some ty -> ppterm subst ty)
-            (ppterm subst t)
-      | None -> "_")
-      context)
+let ppterm_in_context subst term name_context =
+ CicPp.pp (apply_subst subst term) name_context
+
+let ppcontext' ?(sep = "\n") subst context =
+ let separate s = if s = "" then "" else s ^ sep in
+  List.fold_right 
+   (fun context_entry (i,name_context) ->
+     match context_entry with
+        Some (n,Cic.Decl t) ->
+         sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
+          (ppterm_in_context subst t name_context), (Some n)::name_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_context subst ty name_context)
+          (ppterm_in_context subst bo name_context), (Some n)::name_context
+       | None ->
+          sprintf "%s_ :? _" (separate i), None::name_context
+    ) context ("",[])
+
+let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
 
 let ppmetasenv ?(sep = "\n") metasenv subst =
   String.concat sep
     (List.map
       (fun (i, c, t) ->
-        sprintf "%s |- ?%d: %s" (ppcontext ~sep:"; " subst c) i
-          (ppterm subst t))
+        let context,name_context = ppcontext' ~sep:"; " subst c in
+         sprintf "%s |- ?%d: %s" context i
+          (ppterm_in_context subst t name_context))
       (List.filter
         (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
         metasenv))
@@ -557,7 +577,11 @@ let are_convertible subst context t1 t2 =
   let t2 = apply_subst subst t2 in
   CicReduction.are_convertible context t1 t2
 
+let tempi_type_of_aux_subst = ref 0.0;;
+let tempi_type_of_aux = ref 0.0;;
+
 let type_of_aux' metasenv subst context term =
+let time1 = Unix.gettimeofday () in
   let term = apply_subst subst term in
   let context = apply_subst_context subst context in
   let metasenv =
@@ -567,8 +591,26 @@ let type_of_aux' metasenv subst context term =
         (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
         metasenv)
   in
+let time2 = Unix.gettimeofday () in
+let res =
   try
     CicTypeChecker.type_of_aux' metasenv context term
   with CicTypeChecker.TypeCheckerFailure msg ->
     raise (MetaSubstFailure ("Type checker failure: " ^ msg))
+in
+let time3 = Unix.gettimeofday () in
+ tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ; 
+ tempi_type_of_aux := !tempi_type_of_aux +. time2 -. time1 ; 
+ res
+
+(** {2 Format-like pretty printers} *)
+
+let fpp_gen ppf s =
+  Format.pp_print_string ppf s;
+  Format.pp_print_newline ppf ();
+  Format.pp_print_flush ppf ()
+
+let fppsubst ppf subst = fpp_gen ppf (ppsubst subst)
+let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
+let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv metasenv [])