Bug fixed: the canonical contexts were traversed in the wrong direction

during restriction. As a consequence, some hypothesis were not correctly
restricted.

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 30069cdfec88d12f6549922d14d0c1a6561adf90..aed59c5f4cf6fb01605e434d044a8955cb5db3aa 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -42,11 +42,11 @@ let position n =
 
 exception Occur;;
 
-let rec force_does_not_occur subst to_be_restricted t =
+let rec force_does_not_occur k 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
@@ -113,7 +113,7 @@ let rec force_does_not_occur subst to_be_restricted t =
        in
        C.CoFix (i, fl')
  in
- let res = aux 0 t in
+ let res = aux k t in
  (!more_to_be_restricted, res)
  
 let rec restrict subst to_be_restricted metasenv =
@@ -126,23 +126,23 @@ let rec restrict subst to_be_restricted metasenv =
           | Some (n, _) -> CicPp.ppname n)
         indexes)
   in
-  let force_does_not_occur_in_context to_be_restricted = function
+  let force_does_not_occur_in_context k to_be_restricted = function
     | None -> [], None
     | Some (name, Cic.Decl t) ->
         let (more_to_be_restricted, t') =
-          force_does_not_occur subst to_be_restricted t
+          force_does_not_occur k 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
+          force_does_not_occur k 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
+                force_does_not_occur k subst to_be_restricted ty
               in
               more_to_be_restricted @ more_to_be_restricted',
               Some ty'
@@ -152,27 +152,21 @@ 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' =
+              force_does_not_occur_in_context i 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,18 +175,22 @@ 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
           let more_to_be_restricted', t' =
-            force_does_not_occur subst restricted t
+            force_does_not_occur 0 subst restricted t
           in
           let metasenv' = (n, context', t') :: metasenv in
           (try
             let s = List.assoc n subst in
             try
               let more_to_be_restricted'', s' =
-                force_does_not_occur subst restricted s
+                force_does_not_occur 0 subst restricted s
               in
               let subst' = (n, s') :: (List.remove_assoc n subst) in
               let more =
@@ -220,6 +218,16 @@ 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 module S = CicSubstitution in
+(* THIS CODE SHOULD NOT BE USEFUL AT ALL
+  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
@@ -559,7 +567,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 =
@@ -569,8 +581,14 @@ 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