From e8a373c61ed58f91682b16c753d1926fa647fa7d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 15 May 2008 17:04:07 +0000
Subject: [PATCH] (Approximated) inference of relevance implemented: an
 argument X of t is irrelevant if it has sort Prop and the sort of t is not
 Prop.

---
 .../components/ng_kernel/oCic2NCic.ml         | 34 +++++++++++++++----
 1 file changed, 28 insertions(+), 6 deletions(-)

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 49b0e676b..d50b67c8e 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -731,12 +731,34 @@ let cook mode vars t =
   aux varsno [] vars
 ;;
 
+let is_proof_irrelevant context ty =
+  match
+    fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph)
+  with
+     Cic.Sort Cic.Prop -> true
+   | Cic.Sort _ -> false
+   | _ -> assert false
+;;
+
+exception InProp;;
+
+let get_relevance ty =
+ let rec aux context ty =
+  match CicReduction.whd context ty with
+      Cic.Prod (n,s,t) ->
+        not (is_proof_irrelevant context s)::aux (Some (n,Cic.Decl s)::context) t
+    | ty -> if is_proof_irrelevant context ty then raise InProp else []
+ in
+   try aux [] ty
+   with InProp -> []
+;;
+
 let convert_obj_aux uri = function
  | Cic.Constant (name, None, ty, vars, _) ->
      let ty = cook `Pi vars ty in
      let nty, fixpoints = convert_term uri ty in
      assert(fixpoints = []);
-     NCic.Constant ([], name, None, nty, (`Provided,`Theorem,`Regular)),
+     NCic.Constant (get_relevance ty, name, None, nty, (`Provided,`Theorem,`Regular)),
      fixpoints
  | Cic.Constant (name, Some bo, ty, vars, _) ->
      let bo = cook `Lambda vars bo in
@@ -744,7 +766,7 @@ let convert_obj_aux uri = function
      let nbo, fixpoints_bo = convert_term uri bo in
      let nty, fixpoints_ty = convert_term uri ty in
      assert(fixpoints_ty = []);
-     NCic.Constant ([], name, Some nbo, nty, (`Provided,`Theorem,`Regular)),
+     NCic.Constant (get_relevance ty, name, Some nbo, nty, (`Provided,`Theorem,`Regular)),
      fixpoints_bo @ fixpoints_ty
  | Cic.InductiveDefinition (itl,vars,leftno,_) -> 
      let ind = let _,x,_,_ = List.hd itl in x in
@@ -752,16 +774,16 @@ let convert_obj_aux uri = function
        List.fold_right
          (fun (name, _, ty, cl) (itl,acc) ->
             let ty = cook `Pi vars ty in
-            let ty, fix_ty = convert_term uri ty in
+            let nty, fix_ty = convert_term uri ty in
             let cl, fix_cl = 
               List.fold_right
                (fun (name, ty) (cl,acc) -> 
                  let ty = cook `Pi vars ty in
-                 let ty, fix_ty = convert_term uri ty in
-                 ([], name, ty)::cl, acc @ fix_ty)
+                 let nty, fix_ty = convert_term uri ty in
+                 (get_relevance ty, name, nty)::cl, acc @ fix_ty)
                cl ([],[])
             in
-            ([], name, ty, cl)::itl, fix_ty @ fix_cl @ acc)
+            (get_relevance ty, name, nty, cl)::itl, fix_ty @ fix_cl @ acc)
          itl ([],[])
      in
      NCic.Inductive(ind, leftno + List.length 
-- 
2.39.2