Proof-irrelevance check for all applications (first version)

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 4ff6af692bdb924fa651b937cdebe6b942131c99..c15e75a872a89c14c31e3035918fd16dfbcd2211 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -171,7 +171,7 @@ let whd = R.whd
 let (===) x y = Pervasives.compare x y = 0 ;;
 
 (* t1, t2 must be well-typed *)
-let are_convertible ?(subst=[])  =
+let are_convertible ?(subst=[]) get_relevance =
  let rec aux test_eq_only context t1 t2 =
    let rec alpha_eq test_eq_only t1 t2 =
      if t1 === t2 then
@@ -222,26 +222,15 @@ let are_convertible ?(subst=[])  =
               aux test_eq_only context t1 term
            with NCicUtils.Subst_not_found _ -> false)
 
-       | (C.Appl (C.Const r1::tl1), C.Appl (C.Const r2::tl2)) ->
-          r1 = r2 &&
-           let relevance = NCicEnvironment.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
+       | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
+           aux test_eq_only context hd1 hd2 &&
+          let relevance = get_relevance ~subst context hd1 in
            (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)
 
-       | (C.Appl l1, C.Appl l2) ->
-          (try List.for_all2 (aux test_eq_only context) l1 l2
-           with Invalid_argument _ -> false)
-
        | (C.Match (ref1,outtype1,term1,pl1),
           C.Match (ref2,outtype2,term2,pl2)) -> 
            Ref.eq ref1 ref2 &&

diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli
index 52b95cdda63353a3c73bcb81676879dcc30f1e04..5943c926053758ea35dd95bbebd933eea6a54b44 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.mli
+++ b/helm/software/components/ng_kernel/nCicReduction.mli
@@ -16,10 +16,12 @@ val whd :
   NCic.context -> NCic.term -> 
     NCic.term
 
-val are_convertible : 
-  ?subst:NCic.substitution -> 
-  NCic.context -> NCic.term -> NCic.term -> 
-  bool
+val are_convertible :
+  ?subst:NCic.substitution ->
+  (subst:NCic.substitution ->
+   NCic.context -> NCic.term -> bool list) ->
+  NCic.context -> NCic.term -> NCic.term -> bool
+
 
 (* performs head beta/(delta)/cast reduction; the default is to not perform
    delta reduction; if provided, ~upto is the maximum number of beta redexes

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index de633357c9b1692a2964e74e824dba2b7efcc683..8b8348023e4330275159eebd4a42f66e4a3818dd 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -138,39 +138,7 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) =
          (PP.ppterm ~subst ~metasenv ~context t2))))
 ;;
 
-let eat_prods ~subst ~metasenv context he ty_he args_with_ty = 
-  let rec aux ty_he = function 
-  | [] -> ty_he
-  | (arg, ty_arg)::tl ->
-      match R.whd ~subst context ty_he with 
-      | C.Prod (_,s,t) ->
-          if R.are_convertible ~subst context ty_arg s then
-            aux (S.subst ~avoid_beta_redexes:true arg t) tl
-          else
-            raise 
-              (TypeCheckerFailure 
-                (lazy (Printf.sprintf
-                  ("Appl: wrong application of %s: the parameter %s has type"^^
-                   "\n%s\nbut it should have type \n%s\nContext:\n%s\n")
-                  (PP.ppterm ~subst ~metasenv ~context he)
-                  (PP.ppterm ~subst ~metasenv ~context arg)
-                  (PP.ppterm ~subst ~metasenv ~context ty_arg)
-                  (PP.ppterm ~subst ~metasenv ~context s)
-                  (PP.ppcontext ~subst ~metasenv context))))
-       | _ ->
-          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_with_ty - res in
-                   (C.Appl
-                    (he::List.map fst
-                     (fst (HExtlib.split_nth eaten args_with_ty)))))))))
-  in
-    aux ty_he args_with_ty
-;;
+(* REMINDER: eat_prods was here *)
 
 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
@@ -417,7 +385,7 @@ let rec typeof ~subst ~metasenv context term =
     | C.LetIn (n,ty,t,bo) ->
        let ty_t = typeof_aux context t in
        let _ = typeof_aux context ty in
-       if not (R.are_convertible ~subst context ty_t ty) then
+       if not (R.are_convertible ~subst get_relevance context ty_t ty) then
          raise 
           (TypeCheckerFailure 
             (lazy (Printf.sprintf
@@ -488,7 +456,7 @@ let rec typeof ~subst ~metasenv context term =
               let ty_branch = 
                 type_of_branch ~subst context leftno outtype cons ty_cons 0 
               in
-              j+1, R.are_convertible ~subst context ty_p ty_branch,
+              j+1, R.are_convertible ~subst get_relevance context ty_p ty_branch,
               ty_p, ty_branch
             else
               j,false,old_p_ty,old_exp_p_ty
@@ -550,7 +518,7 @@ let rec typeof ~subst ~metasenv context term =
                 (_,C.Decl t1), (_,C.Decl t2)
               | (_,C.Def (t1,_)), (_,C.Def (t2,_))
               | (_,C.Def (_,t1)), (_,C.Decl t2) ->
-                 if not (R.are_convertible ~subst tl t1 t2) then
+                 if not (R.are_convertible ~subst get_relevance tl t1 t2) then
                   raise 
                       (TypeCheckerFailure 
                         (lazy (Printf.sprintf 
@@ -601,7 +569,7 @@ let rec typeof ~subst ~metasenv context term =
                     with Failure _ -> t)
               | _ -> t
              in
-             if not (R.are_convertible ~subst context optimized_t ct)
+             if not (R.are_convertible ~subst get_relevance context optimized_t ct)
              then
                raise 
                  (TypeCheckerFailure 
@@ -612,7 +580,7 @@ let rec typeof ~subst ~metasenv context term =
                      (PP.ppterm ~subst ~metasenv ~context t))))
           | t, (_,C.Decl ct) ->
               let type_t = typeof_aux context t in
-              if not (R.are_convertible ~subst context type_t ct) then
+              if not (R.are_convertible ~subst get_relevance context type_t ct) then
                 raise (TypeCheckerFailure 
                  (lazy (Printf.sprintf 
                   ("Not well typed metavariable local context: "^^
@@ -637,7 +605,7 @@ let rec typeof ~subst ~metasenv context term =
     let arity2 = R.whd ~subst context arity2 in
       match arity1,arity2 with
        | C.Prod (name,so1,de1), C.Prod (_,so2,de2) ->
-          if not (R.are_convertible ~subst context so1 so2) then
+          if not (R.are_convertible ~subst get_relevance context so1 so2) then
            raise (TypeCheckerFailure (lazy (Printf.sprintf
             "In outtype: expected %s, found %s"
             (PP.ppterm ~subst ~metasenv ~context so1)
@@ -646,7 +614,7 @@ let rec typeof ~subst ~metasenv context term =
           aux ((name, C.Decl so1)::context)
            (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2
        | C.Sort _, C.Prod (name,so,ta) ->
-          if not (R.are_convertible ~subst context so ind) then
+          if not (R.are_convertible ~subst get_relevance context so ind) then
            raise (TypeCheckerFailure (lazy (Printf.sprintf
             "In outtype: expected %s, found %s"
             (PP.ppterm ~subst ~metasenv ~context ind)
@@ -680,6 +648,39 @@ let rec typeof ~subst ~metasenv context term =
  in 
    typeof_aux context term
 
+and eat_prods ~subst ~metasenv context he ty_he args_with_ty = 
+  let rec aux ty_he = function 
+  | [] -> ty_he
+  | (arg, ty_arg)::tl ->
+      match R.whd ~subst context ty_he with 
+      | C.Prod (_,s,t) ->
+          if R.are_convertible ~subst get_relevance context ty_arg s then
+            aux (S.subst ~avoid_beta_redexes:true arg t) tl
+          else
+            raise 
+              (TypeCheckerFailure 
+                (lazy (Printf.sprintf
+                  ("Appl: wrong application of %s: the parameter %s has type"^^
+                   "\n%s\nbut it should have type \n%s\nContext:\n%s\n")
+                  (PP.ppterm ~subst ~metasenv ~context he)
+                  (PP.ppterm ~subst ~metasenv ~context arg)
+                  (PP.ppterm ~subst ~metasenv ~context ty_arg)
+                  (PP.ppterm ~subst ~metasenv ~context s)
+                  (PP.ppcontext ~subst ~metasenv context))))
+       | _ ->
+          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_with_ty - res in
+                   (C.Appl
+                    (he::List.map fst
+                     (fst (HExtlib.split_nth eaten args_with_ty)))))))))
+  in
+    aux ty_he args_with_ty
+
 and is_non_informative paramsno c =
  let rec aux context c =
    match R.whd context c with
@@ -716,11 +717,11 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl =
                 let convertible =
                  match item1,item2 with
                    (n1,C.Decl ty1),(n2,C.Decl ty2) ->
-                     n1 = n2 && R.are_convertible ~subst context ty1 ty2
+                     n1 = n2 && R.are_convertible ~subst get_relevance context ty1 ty2
                  | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
                      n1 = n2
-                     && R.are_convertible ~subst context ty1 ty2
-                     && R.are_convertible ~subst context bo1 bo2
+                     && R.are_convertible ~subst get_relevance context ty1 ty2
+                     && R.are_convertible ~subst get_relevance context bo1 bo2
                  | _,_ -> false
                 in
                  if not convertible then
@@ -1020,6 +1021,29 @@ and type_of_constant ((Ref.Ref (uri,_)) as ref) =
      if h1 <> h2 then error ();
      ty
   | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference"))
+
+and get_relevance ~subst context = function
+  | C.Const r -> 
+      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 = function
+        | C.Prod (name,so,de) -> 
+           let sort = typeof ~subst ~metasenv:[] context so in
+           (match sort with
+             | C.Sort C.Prop -> false::(aux ((name,(C.Decl so))::context) de)
+             | C.Sort _ -> true::(aux ((name,(C.Decl so))::context) de)
+             | _ -> 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)))))
+       | _ -> []
+      in aux context ty
 ;;
 
 let typecheck_context ~metasenv ~subst context =
@@ -1032,7 +1056,7 @@ let typecheck_context ~metasenv ~subst context =
        | name,C.Def (te,ty) ->
          ignore (typeof ~metasenv ~subst:[] context ty);
          let ty' = typeof ~metasenv ~subst:[] context te in
-          if not (R.are_convertible ~subst context ty' ty) then
+          if not (R.are_convertible ~subst get_relevance context ty' ty) then
            raise (AssertFailure (lazy (Printf.sprintf (
             "the type of the definiens for %s in the context is not "^^
             "convertible with the declared one.\n"^^
@@ -1070,7 +1094,7 @@ let typecheck_subst ~metasenv subst =
       typecheck_context ~metasenv ~subst context;
       ignore (typeof ~metasenv ~subst context ty);
       let ty' = typeof ~metasenv ~subst context bo in
-       if not (R.are_convertible ~subst context ty' ty) then
+       if not (R.are_convertible ~subst get_relevance context ty' ty) then
         raise (AssertFailure (lazy (Printf.sprintf (
          "the type of the definiens for %d in the substitution is not "^^
          "convertible with the declared one.\n"^^
@@ -1082,9 +1106,8 @@ let typecheck_subst ~metasenv subst =
     ) [] subst)
 ;;
 
-let check_rel1_irrelevant ~metasenv ~subst context = fun _ -> ()
-(*
-  let shift e (k, context) = k+1,e::context in
+let check_rel1_irrelevant ~metasenv ~subst context = fun _ -> ();;
+(*  let shift e (k, context) = k+1,e::context in
   let rec aux (evil, context as k) () t =
     match R.whd ~subst context t with
     | C.Rel i when i = evil -> (*
@@ -1111,12 +1134,10 @@ let check_rel1_irrelevant ~metasenv ~subst context = fun _ -> ()
     | C.Match (_, _, t, pl) -> List.iter (aux k ()) (t::pl)
     | t -> U.fold shift k aux () t
   in 
-    aux (1, context) ()
-*)
+    aux (1, context) () *)
 
-let check_relevance ~metasenv ~subst ~in_type relevance = fun _ -> ()
-(*
-  let shift e (in_type, context, relevance) = 
+let check_relevance ~metasenv ~subst ~in_type relevance = fun _ -> ();;
+(*  let shift e (in_type, context, relevance) = 
     assert (relevance = []); in_type, e::context, relevance
   in
   let rec aux2 (_,context,relevance as k) t = 
@@ -1173,8 +1194,7 @@ let check_relevance ~metasenv ~subst ~in_type relevance = fun _ -> ()
        aux k () t
   in
     aux2 (in_type, [], relevance)
-*)
-;;
+;;*)
 
 let typecheck_obj (uri,_height,metasenv,subst,kind) =
  (* height is not checked since it is only used to implement an optimization *)
@@ -1184,7 +1204,7 @@ let typecheck_obj (uri,_height,metasenv,subst,kind) =
    | C.Constant (relevance,_,Some te,ty,_) ->
       let _ = typeof ~subst ~metasenv [] ty in
       let ty_te = typeof ~subst ~metasenv [] te in
-      if not (R.are_convertible ~subst [] ty_te ty) then
+      if not (R.are_convertible ~subst get_relevance [] ty_te ty) then
        raise (TypeCheckerFailure (lazy (Printf.sprintf (
         "the type of the body is not convertible with the declared one.\n"^^
         "inferred type:\n%s\nexpected type:\n%s")
@@ -1215,7 +1235,7 @@ let typecheck_obj (uri,_height,metasenv,subst,kind) =
       in
       List.iter2 (fun (_,_,x,ty,_) bo ->
        let ty_bo = typeof ~subst ~metasenv types bo in
-       if not (R.are_convertible ~subst types ty_bo ty)
+       if not (R.are_convertible ~subst get_relevance types ty_bo ty)
        then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))
        else
         if inductive then begin