final relevance check

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 61bb201b7f685e0e6c3bf615c4b4406aba719cb5..61591e4f89698fc32092f054753f43648193f11d 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -171,8 +171,19 @@ let whd = R.whd
 
 let (===) x y = Pervasives.compare x y = 0 ;;
 
+exception Dance;;
+
+let prof = HExtlib.profiling_enabled := true;HExtlib.profile "cache failures";;
+let prof2 = HExtlib.profiling_enabled := true;HExtlib.profile "dancing sorts";;
 (* t1, t2 must be well-typed *)
 let are_convertible ?(subst=[]) get_relevance =
+ let get_relevance_p ~subst context t args =
+   (match prof with {HExtlib.profile = p} -> p)
+   (fun (a,b,c,d) -> get_relevance ~subst:a b c d)
+   (subst,context,t,args)
+ in
+ let dance () = (match prof2 with {HExtlib.profile = p} -> p) (fun () -> ()) ()
+ in
  let rec aux test_eq_only context t1 t2 =
    let rec alpha_eq test_eq_only t1 t2 =
      if t1 === t2 then
@@ -222,7 +233,41 @@ let are_convertible ?(subst=[]) get_relevance =
              let term = NCicSubstitution.subst_meta l2 term in
               aux test_eq_only context t1 term
            with NCicUtils.Subst_not_found _ -> false)
-
+       
+       | (C.Appl ((C.Const r1) as hd1::tl1), C.Appl (C.Const r2::tl2)) 
+           when (Ref.eq r1 r2 && 
+             List.length (E.get_relevance r1) >= List.length tl1) ->
+         let relevance = E.get_relevance r1 in
+         let relevance = match r1 with
+             | Ref.Ref (_,Ref.Con (_,_,lno)) ->
+                 let _,relevance = HExtlib.split_nth lno relevance in
+                   HExtlib.mk_list false lno @ relevance
+             | _ -> relevance
+         in
+        let fail = ref ~-1 in
+         let res = (try
+             HExtlib.list_forall_default3
+              (fun t1 t2 b -> fail := !fail+1; not b || aux test_eq_only context t1 t2)
+              tl1 tl2 true relevance
+            with Invalid_argument _ -> false)
+         in res
+        (* if res then true
+         else
+          let relevance = get_relevance_p ~subst context hd1 tl1 in
+          let _,relevance = HExtlib.split_nth !fail relevance in
+          let b,relevance = (match relevance with
+            | [] -> assert false
+            | b::tl -> b,tl) in
+          let _,tl1 = HExtlib.split_nth (!fail+1) tl1 in
+          let _,tl2 = HExtlib.split_nth (!fail+1) tl2 in
+          if (not b) then
+             (dance ();
+             try
+               HExtlib.list_forall_default3
+                (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
+                tl1 tl2 true relevance
+             with Invalid_argument _ -> false)
+          else false *)
        | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
            aux test_eq_only context hd1 hd2 &&
           let relevance = get_relevance ~subst context hd1 tl1 in

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 56d06a71b673f7edee75136c29204a3d43dd2041..464186f2e0d1cdf91798761326cc524637733bdb 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1053,44 +1053,39 @@ and type_of_constant ((Ref.Ref (uri,_)) as ref) =
      ty
   | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference"))
 
-and get_relevance ~subst context te args = 
-  match te with 
-  | C.Const r when List.length (E.get_relevance r) >= List.length args -> 
-      let relevance = E.get_relevance r in 
-      (match r with
-        | Ref.Ref (_,Ref.Con (_,_,lno)) ->
-            let _,relevance = HExtlib.split_nth lno relevance in
-              HExtlib.mk_list false lno @ relevance
-        | _ -> relevance)
-  | t ->
-      let ty = typeof ~subst ~metasenv:[] context t in
-      let rec aux context ty = function
-        | [] -> [] 
-       | arg::tl -> match R.whd ~subst context ty with
-          | C.Prod (name,so,de) -> 
-             let sort = typeof ~subst ~metasenv:[] context so in
-             let new_ty = S.subst ~avoid_beta_redexes:true arg de in
-             (match R.whd ~subst context sort with
-                | C.Sort C.Prop -> 
-                    false::(aux ((name,(C.Decl so))::context) new_ty tl)
-                | C.Sort _
-                | C.Meta _ -> true::(aux ((name,(C.Decl so))::context) de tl)
-                | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
-                       "Prod: the type %s of the source of %s is not a sort" 
-                        (PP.ppterm ~subst ~metasenv:[] ~context sort)
-                        (PP.ppterm ~subst ~metasenv:[] ~context so)))))
-          | _ ->
-             raise 
-               (TypeCheckerFailure
-                 (lazy (Printf.sprintf
-                   "Appl: %s is not a function, it cannot be applied"
-                   (PP.ppterm ~subst ~metasenv:[] ~context
-                    (let res = List.length tl in
-                     let eaten = List.length args - res in
-                      (C.Appl
-                       (t::fst
-                        (HExtlib.split_nth eaten args))))))))
-      in aux context ty args
+and get_relevance ~subst context t args = 
+   let ty = typeof ~subst ~metasenv:[] context t in
+   let rec aux context ty = function
+     | [] -> [] 
+     | arg::tl -> match R.whd ~subst context ty with
+       | C.Prod (name,so,de) -> 
+           let sort = typeof ~subst ~metasenv:[] context so in
+           let new_ty = S.subst ~avoid_beta_redexes:true arg de in
+           (*prerr_endline ("so: " ^ PP.ppterm ~subst ~metasenv:[]
+            ~context so);
+           prerr_endline ("sort: " ^ PP.ppterm ~subst ~metasenv:[]
+            ~context sort);*)
+          (match R.whd ~subst context sort with
+              | C.Sort C.Prop ->
+                  false::(aux context new_ty tl)
+              | C.Sort _
+             | C.Meta _ -> true::(aux context new_ty tl)
+              | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
+               "Prod: the type %s of the source of %s is not a sort" 
+                (PP.ppterm ~subst ~metasenv:[] ~context sort)
+                (PP.ppterm ~subst ~metasenv:[] ~context so)))))
+       | _ ->
+          raise 
+            (TypeCheckerFailure
+              (lazy (Printf.sprintf
+                "Appl: %s is not a function, it cannot be applied"
+                (PP.ppterm ~subst ~metasenv:[] ~context
+                 (let res = List.length tl in
+                  let eaten = List.length args - res in
+                   (C.Appl
+                    (t::fst
+                     (HExtlib.split_nth eaten args))))))))
+   in aux context ty args
 ;;
 
 let typecheck_context ~metasenv ~subst context =