Implementation of proof irrelevance finished.

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 58904b83303c40ab3ed28f65d2d762a9aaaedac6..0420c8119f2d6d9733e66e7799eb382e4ed874da 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -396,6 +396,61 @@ let subst_metasenv_and_fix_names status =
    status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
 ;;
 
+let is_proof_irrelevant context ty =
+  match
+    NCicReduction.whd ~subst:[] context
+     (NCicTypeChecker.typeof ~subst:[] ~metasenv:[] context ty)
+  with
+     NCic.Sort NCic.Prop -> true
+   | NCic.Sort _ -> false
+   | _ -> assert false
+;;
+
+let rec relevance_of ?(context=[]) ty =
+ match NCicReduction.whd ~subst:[] context ty with
+    NCic.Prod (n,s,t) ->
+     not (is_proof_irrelevant context s) ::
+      relevance_of ~context:((n,NCic.Decl s)::context) t
+  | _ -> []
+;;
+
+let compute_relevance uri =
+ function
+    NCic.Constant (_,name,bo,ty,attrs) ->
+     let relevance = relevance_of ty in
+      NCic.Constant (relevance,name,bo,ty,attrs)
+  | NCic.Fixpoint (ind,funs,attrs) ->
+     let funs =
+       List.map
+       (fun (_,name,recno,ty,bo) ->
+         let relevance = relevance_of ty in
+          relevance,name,recno,ty,bo
+        ) funs
+     in
+      NCic.Fixpoint (ind,funs,attrs)
+  | NCic.Inductive (ind,leftno,tys,attrs) ->
+     let context =
+      List.rev_map (fun (_,name,arity,_) -> name,NCic.Decl arity) tys in
+     let tysno = List.length tys in
+     let tys =
+       List.map
+        (fun (_,name,arity,cons) ->
+         let relevance = relevance_of arity in
+         let cons =
+          List.map
+           (fun (_,name,ty) ->
+             let dety =
+               NCicTypeChecker.debruijn uri tysno ~subst:[] [] ty in
+             let relevance = relevance_of ~context dety in
+              relevance,name,ty
+           ) cons
+         in
+          (relevance,name,arity,cons)
+        ) tys
+     in
+      NCic.Inductive (ind,leftno,tys,attrs)
+;;
+
 
 let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
   match cmd with
@@ -448,6 +503,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
               NCicUntrusted.map_obj_kind (fix ()) obj_kind 
           | _ -> obj_kind
         in
+        let obj_kind = compute_relevance uri obj_kind in
         let obj = uri,height,[],[],obj_kind in
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in

diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml
index ccbebc27164a16afb088bfa131a252dca37fe472..4a89e9d12bd8fa8797fdb8f738782c386aa51676 100644 (file)
--- a/matita/components/ng_kernel/nCicTypeChecker.ml
+++ b/matita/components/ng_kernel/nCicTypeChecker.ml
@@ -762,7 +762,7 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl =
        let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in
        List.iter
          (fun (k_relev,_,te) ->
-          let k_relev =
+           let k_relev =
             try snd (HExtlib.split_nth leftno k_relev)
             with Failure _ -> k_relev in
            let te = debruijn uri len [] ~subst te in
@@ -815,11 +815,11 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl =
              raise
                (TypeCheckerFailure
                  (lazy ("Non positive occurence in "^NUri.string_of_uri
-                uri)))
-           else check_relevance ~subst ~metasenv context k_relev te) 
+                 uri)))
+           else check_relevance ~subst ~metasenv context k_relev te)
          cl;
         check_relevance ~subst ~metasenv [] it_relev ty;
-       i+1)
+        i+1)
     tyl 1)
 
 and check_relevance ~subst ~metasenv context relevance ty =
@@ -834,10 +834,10 @@ and check_relevance ~subst ~metasenv context relevance ty =
     | C.Prod (name,so,de) ->
         let sort = typeof ~subst ~metasenv context so in
         (match (relevance,R.whd ~subst context sort) with
-         | [],_ -> ()
+          | [],_ -> ()
           | false::tl,C.Sort C.Prop -> aux ((name,(C.Decl so))::context) tl de
-         | true::_,C.Sort C.Prop
-         | false::_,C.Sort _
+          | true::_,C.Sort C.Prop
+          | false::_,C.Sort _
           | false::_,C.Meta _ -> error context ty
           | true::tl,C.Sort _
           | true::tl,C.Meta _ -> aux ((name,(C.Decl so))::context) tl de
@@ -1124,18 +1124,18 @@ and get_relevance ~metasenv ~subst context t args =
            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);
+             ~context so);
            prerr_endline ("sort: " ^ PP.ppterm ~subst ~metasenv:[]
-            ~context sort);*)
-          (match R.whd ~subst context sort with
+             ~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)
+                   | 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)))))
+                     "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
@@ -1280,7 +1280,7 @@ let typecheck_obj (uri,height,metasenv,subst,kind) =
         List.fold_left
          (fun (types,kl) (relevance,name,k,ty,_) ->
            let _ = typeof ~subst ~metasenv [] ty in
-           check_relevance ~subst ~metasenv [] relevance ty;
+            check_relevance ~subst ~metasenv [] relevance ty;
             ((name,C.Decl ty)::types, k::kl)
          ) ([],[]) fl
       in

diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml
index dd1e4b80c520b71e6d96b0e915f98f86e3716659..9227289c6808f73fb6abf2e7bf725ce7854c876f 100644 (file)
--- a/matita/components/ng_refiner/nCicUnification.ml
+++ b/matita/components/ng_refiner/nCicUnification.ml
@@ -823,10 +823,10 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
            ppterm ~metasenv ~subst ~context 
              (NCicReduction.unwind (k2,e2,t2,s2))));
          pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
-          let relevance = [] (* TO BE UNDERSTOOD 
+          let relevance =
             match t1 with
             | C.Const r -> NCicEnvironment.get_relevance r
-            | _ -> [] *) in
+            | _ -> [] in
           let unif_from_stack (metasenv, subst) (t1, t2, b) =
               try
                 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
@@ -839,7 +839,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
             match l1,l2,r with
             | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
             | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
-            | l1, l2, _ -> 
+            | l1, l2, _ ->
                NCicReduction.unwind (k1,e1,t1,List.rev l1),
                 NCicReduction.unwind (k2,e2,t2,List.rev l2),
                 todo
@@ -848,10 +848,11 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
             match t1, t2 with
             | NCic.Meta _, _ | _, NCic.Meta _ ->
                 (NCicReduction.unwind (k1,e1,t1,s1)),
-                (NCicReduction.unwind (k2,e2,t2,s2)),[]     
+                (NCicReduction.unwind (k2,e2,t2,s2)),[]
             | _ -> check_stack l1 l2 r []
           in
-        let hh1,hh2,todo = check_stack (List.rev s1) (List.rev s2) relevance in
+        let hh1,hh2,todo =
+          check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in
         try
           fo_unif_heads_and_cont_or_unwind_and_hints
             test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)