irrelevance check half implemented but already impossible to

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index b1b0d321787925a5d7b3c7f8ad6ff0562af57665..56159ffa4e91846f28785b5af4c2b5667cec0d68 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -22,7 +22,35 @@ let mk_type n =
      [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
-let cprop = [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")];;
+let mk_cprop n = 
+  if n = 0 then 
+    [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+  else
+    [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+;;
+
+let is_proof_irrelevant context ty =
+  match
+    CicReduction.whd context
+     (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 -> []
+;;
 
 (* porcatissima *)
 type reference = Ref of NUri.uri * NReference.spec
@@ -122,6 +150,17 @@ let splat mk_pi ctx t =
     (t,[]) ctx
 ;;
 
+let osplat mk_pi ctx t =
+  List.fold_left
+    (fun t c -> 
+      match c with
+      | Some (name, Cic.Def (bo,ty)) -> Cic.LetIn (name, ty, bo, t)
+      | Some (name, Cic.Decl ty) when mk_pi -> Cic.Prod (name, ty, t)
+      | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t)
+      | None -> assert false)
+    t ctx
+;;
+
 let context_tassonomy ctx = 
     let rec split inner acc acc1 = function 
       | Ce _ :: tl when inner -> split inner (acc+1) (acc1+1) tl
@@ -561,13 +600,13 @@ let convert_term uri t =
         let rno_fixno = ref 0 in
         let fl, fixpoints,_ =
           List.fold_right2 
-            (fun (name,rno,_,bo) ty (l,fixpoints,idx) -> 
+            (fun (name,rno,oty,bo) ty (l,fixpoints,idx) -> 
                let bo, fixpoints_bo = aux false boctx bctx n_fl buri bo in
                let splty,fixpoints_splty = splat true ctx ty in
                let splbo,fixpoints_splbo = splat false ctx bo in
                let rno = rno + free_decls in
                if idx = fixno then rno_fixno := rno;
-               (([],name,rno,splty,splbo)::l),
+               ((get_relevance (osplat true octx oty),name,rno,splty,splbo)::l),
                fixpoints_bo@fixpoints_splty@fixpoints_splbo@fixpoints,idx+1)
             fl tys ([],fixpoints_tys,0)
         in
@@ -633,7 +672,8 @@ let convert_term uri t =
         let ty, fixpoints_ty = aux k octx ctx n_fix uri ty in
         NCic.LetIn ("cast", ty, t, NCic.Rel 1), fixpoints_t @ fixpoints_ty
     | Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[]
-    | Cic.Sort Cic.CProp -> NCic.Sort (NCic.Type cprop),[]
+    | Cic.Sort (Cic.CProp u) -> 
+          NCic.Sort (NCic.Type (mk_cprop (CicUniv.get_rank u))),[]
     | Cic.Sort (Cic.Type u) -> 
           NCic.Sort (NCic.Type (mk_type (CicUniv.get_rank u))),[] 
     | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type (mk_type 0)),[] 
@@ -755,29 +795,6 @@ let cook mode vars t =
   aux varsno [] vars
 ;;
 
-let is_proof_irrelevant context ty =
-  match
-    CicReduction.whd context
-     (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