]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/oCic2NCic.ml
Patch to add a debugging string to HExtlib.split_nth reverted
[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml
index 6a9dd715a5bc6e79a9da108af9a9171e0083a39f..2738b1c901835183078c7a24b0f3470475f13f02 100644 (file)
@@ -15,6 +15,45 @@ module Ref = NReference
 
 let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);;
 
+let mk_type n = 
+  if n = 0 then
+     [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+  else
+     [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".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
+    | _ -> []
+ in aux [] ty
+(*    | 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
 let reference_of_ouri u indinfo =
@@ -33,6 +72,16 @@ let strictify =
   | Fix l -> `Fix (Lazy.force l)
 ;;
 
+let count_vars vars =
+ List.length 
+  (List.filter (fun v -> 
+     match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph v) with
+        Cic.Variable (_,Some _,_,_,_) -> false
+      | Cic.Variable (_,None,_,_,_) -> true
+      | _ -> assert false) vars)
+;;
+
+
 (***** A function to restrict the context of a term getting rid of unsed
        variables *******)
 
@@ -66,7 +115,7 @@ let restrict octx ctx ot =
    | ((_,objs,None)::tl, Cic.Lambda(name,oso,ota), NCic.Lambda(name',so,ta)) ->
        split_lambdas_and_letins ((Some(name,(Cic.Decl oso)))::octx)
         (Ce (lazy ((name',NCic.Decl so),objs))::ctx) tl (ota,ta)
-   | ((_,objs,Some r)::tl,Cic.Lambda(name,oso,ota),NCic.Lambda(name',so,ta)) ->
+   | ((_,_,Some r)::tl,Cic.Lambda(name,oso,ota),NCic.Lambda(name',so,ta)) ->
        split_lambdas_and_letins ((Some(name,(Cic.Decl oso)))::octx)
         (Fix (lazy (r,name',so))::ctx) tl (ota,ta)
    | ((_,objs,None)::tl,Cic.LetIn(name,obo,oty,ota),NCic.LetIn(nam',bo,ty,ta))->
@@ -103,6 +152,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
@@ -151,7 +211,7 @@ let splat_args_for_rel ctx t ?rels n_fix =
 ;;
 
 let splat_args ctx t n_fix rels =
-  let bound, free, _, primo_ce_dopo_fix = context_tassonomy ctx in
+  let bound, _, _, primo_ce_dopo_fix = context_tassonomy ctx in
   if ctx = [] then t
   else
    let rec aux = function
@@ -185,7 +245,7 @@ let fix_outty curi tyno t context outty =
           0, Cic.Sort _ -> 0
         | 0, Cic.Prod (name,so,ty) ->
            1 + count_prods 0 (Some (name, Cic.Decl so)::context) ty
-        | n, Cic.Prod (name,so,ty) ->
+        | _, Cic.Prod (name,so,ty) ->
            count_prods (leftno - 1) (Some (name, Cic.Decl so)::context) ty
         | _,_ -> assert false
       in
@@ -379,15 +439,15 @@ prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==>
   begin
     match obj, ref with 
     | (_,_,_,_,NCic.Fixpoint (true,fl,_)) , 
-      NReference.Ref (y,NReference.Fix _) ->
+      NReference.Ref (_,NReference.Fix _) ->
        ignore(List.fold_left (fun i (_,name,rno,_,_) ->
          let ref = NReference.mk_fix i rno ref in
          Hashtbl.add cache name (ref,obj);
          i+1
        ) 0 fl)
     | (_,_,_,_,NCic.Fixpoint (false,fl,_)) , 
-      NReference.Ref (y,NReference.CoFix _) ->
-       ignore(List.fold_left (fun i (_,name,rno,_,_) ->
+      NReference.Ref (_,NReference.CoFix _) ->
+       ignore(List.fold_left (fun i (_,name,_,_,_) ->
          let ref = NReference.mk_cofix i ref in
          Hashtbl.add cache name (ref,obj);
          i+1
@@ -398,10 +458,52 @@ prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==>
  with Found ref -> Some ref
 ;;
 
-(* we are lambda-lifting also variables that do not occur *)
-(* ctx does not distinguish successive blocks of cofix, since there may be no
- *   lambda separating them *)
-let convert_term uri t = 
+let cache1 = UriManager.UriHashtbl.create 313;;
+let rec get_height =
+   function u ->
+     try
+       UriManager.UriHashtbl.find cache1 u
+     with
+      Not_found ->
+        let h = ref 0 in
+         let res =
+          match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph u) with
+             Cic.Constant (_,Some bo,ty,params,_)
+           | Cic.Variable (_,Some bo,ty,params,_) ->
+               ignore (height_of_term ~h bo);
+               ignore (height_of_term ~h ty);
+               List.iter (function uri -> h := max !h (get_height uri)) params;
+               1 + !h
+           | _ -> 0
+         in
+           UriManager.UriHashtbl.add cache1 u res;
+           res
+and height_of_term ?(h=ref 0) t =
+ let rec aux =
+  function
+   Cic.Rel _
+ | Cic.Sort _ -> ()
+ | Cic.Implicit _ -> assert false
+ | Cic.Var (uri,exp_named_subst)
+ | Cic.Const (uri,exp_named_subst)
+ | Cic.MutInd (uri,_,exp_named_subst)
+ | Cic.MutConstruct (uri,_,_,exp_named_subst) ->
+    h := max !h (get_height uri);
+    List.iter (function (_,t) -> aux t) exp_named_subst
+ | Cic.Meta (_,l) -> List.iter (function None -> () | Some t -> aux t) l
+ | Cic.Cast (t1,t2)
+ | Cic.Prod (_,t1,t2)
+ | Cic.Lambda (_,t1,t2) -> aux t1; aux t2
+ | Cic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
+ | Cic.Appl l -> List.iter aux l
+ | Cic.MutCase (_,_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
+ | Cic.Fix (_, fl) -> List.iter (fun (_, _, ty, bo) ->  aux ty; aux bo) fl; incr h
+ | Cic.CoFix (_, fl) -> List.iter (fun (_, ty, bo) ->  aux ty; aux bo) fl; incr h
+ in
+   aux t;
+   1 + !h
+;;
+
   (* k=true if we are converting a term to be pushed in a ctx or if we are
             converting the type of a fix;
      k=false if we are converting a term to be put in the body of a fix;
@@ -464,14 +566,14 @@ let convert_term uri t =
         let buri = 
           UriManager.uri_of_string 
            (UriManager.buri_of_uri uri^"/"^
-            UriManager.name_of_uri uri ^ "___" ^ get_fresh () ^ ".con")
-        in
+            UriManager.name_of_uri uri ^ "___" ^ get_fresh () ^ ".con") in
+        let height = height_of_term fix - 1 in
         let bad_bctx, fixpoints_tys, tys, _ = 
           List.fold_right 
             (fun (name,recno,ty,_) (bctx, fixpoints, tys, idx) -> 
               let ty, fixpoints_ty = aux true octx ctx n_fix uri ty in
               let r =  (* recno is dummy here, must be lifted by the ctx len *)
-                reference_of_ouri buri (Ref.Fix (idx,recno,1)) 
+                reference_of_ouri buri (Ref.Fix (idx,recno,height)) 
               in
               bctx @ [Fix (lazy (r,name,ty))],
                fixpoints_ty@fixpoints,ty::tys,idx-1)
@@ -496,20 +598,21 @@ 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
         let obj = 
-          nuri_of_ouri buri,max_int,[],[],
+          nuri_of_ouri buri,height,[],[],
             NCic.Fixpoint (true, fl, (`Generated, `Definition)) in
-        let r = reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno,1)) in
+(*prerr_endline ("H(" ^ UriManager.string_of_uri buri ^ ") = " ^ string_of_int * height);*)
+        let r = reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno,height)) in
         let obj,r =
          let _,name,_,_,_ = List.nth fl fixno in
          match find_in_cache name obj r with
@@ -567,10 +670,11 @@ 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.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 (CicUniv.get_rank u)),[] 
-    | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type 0),[] 
+          NCic.Sort (NCic.Type (mk_type (CicUniv.get_rank u))),[] 
+    | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type (mk_type 0)),[] 
        (* calculate depth in the univ_graph*)
     | Cic.Appl l -> 
         let l, fixpoints =
@@ -587,34 +691,39 @@ let convert_term uri t =
        aux_ens k curi octx ctx n_fix uri ens
         (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
         | Cic.Constant (_,Some _,_,_,_) ->
-               NCic.Const (reference_of_ouri curi (Ref.Def 1))
+               NCic.Const (reference_of_ouri curi (Ref.Def (get_height curi)))
         | Cic.Constant (_,None,_,_,_) ->
                NCic.Const (reference_of_ouri curi Ref.Decl)
         | _ -> assert false)
     | Cic.MutInd (curi, tyno, ens) -> 
-       let is_inductive =
+       let is_inductive, lno =
         match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
-           Cic.InductiveDefinition ([],_,_,_) -> true
-         | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+           Cic.InductiveDefinition ([],vars,lno,_) -> true, lno + count_vars vars
+         | Cic.InductiveDefinition ((_,b,_,_)::_,vars,lno,_) -> b, lno + count_vars vars
          | _ -> assert false
        in
         aux_ens k curi octx ctx n_fix uri ens
-         (NCic.Const (reference_of_ouri curi (Ref.Ind (is_inductive,tyno))))
+         (NCic.Const (reference_of_ouri curi (Ref.Ind (is_inductive,tyno,lno))))
     | Cic.MutConstruct (curi, tyno, consno, ens) -> 
+       let lno =
+        match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+           Cic.InductiveDefinition (_,vars,lno,_) -> lno + count_vars vars
+         | _ -> assert false
+       in
        aux_ens k curi octx ctx n_fix uri ens
-        (NCic.Const (reference_of_ouri curi (Ref.Con (tyno,consno))))
+        (NCic.Const (reference_of_ouri curi (Ref.Con (tyno,consno,lno))))
     | Cic.Var (curi, ens) ->
        (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
            Cic.Variable (_,Some bo,_,_,_) ->
             aux k octx ctx n_fix uri (CicSubstitution.subst_vars ens bo)
          | _ -> assert false)
     | Cic.MutCase (curi, tyno, outty, t, branches) ->
-        let is_inductive =
+        let is_inductive,lno =
          match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
-            Cic.InductiveDefinition ([],_,_,_) -> true
-          | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+            Cic.InductiveDefinition ([],vars,lno,_) -> true, lno + count_vars vars
+          | Cic.InductiveDefinition ((_,b,_,_)::_,vars,lno,_) -> b, lno + count_vars vars
           | _ -> assert false in
-        let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno)) in
+        let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno,lno)) in
         let outty, fixpoints_outty = aux k octx ctx n_fix uri outty in
         let t, fixpoints_t = aux k octx ctx n_fix uri t in
         let branches, fixpoints =
@@ -652,7 +761,12 @@ let convert_term uri t =
        match ens with
           [] -> he,objs
         | _::_ -> NCic.Appl (he::ens),objs
-  in
+;;
+
+(* we are lambda-lifting also variables that do not occur *)
+(* ctx does not distinguish successive blocks of cofix, since there may be no
+ *   lambda separating them *)
+let convert_term uri t = 
    aux false [] [] 0 uri t
 ;;
 
@@ -689,7 +803,7 @@ let convert_obj_aux uri = function
      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
@@ -697,7 +811,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
@@ -705,26 +819,19 @@ 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 
-       (List.filter (fun v -> 
-          match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph v) with
-             Cic.Variable (_,Some _,_,_,_) -> false
-           | Cic.Variable (_,None,_,_,_) -> true
-           | _ -> assert false)
-          vars)
-       , itl, (`Provided, `Regular)),
+     NCic.Inductive(ind, leftno + count_vars vars, itl, (`Provided, `Regular)),
      fix_itl
  | Cic.Variable _ 
  | Cic.CurrentProof _ -> assert false
@@ -733,6 +840,34 @@ let convert_obj_aux uri = function
 let convert_obj uri obj = 
   reset_seed ();
   let o, fixpoints = convert_obj_aux uri obj in
-  let obj = nuri_of_ouri uri,max_int, [], [], o in
+  let obj = nuri_of_ouri uri,get_height uri, [], [], o in
+(*prerr_endline ("H(" ^ UriManager.string_of_uri uri ^ ") = " ^ string_of_int * (get_height uri));*)
   fixpoints @ [obj]
 ;;
+
+let clear () =
+  Hashtbl.clear cache;
+  UriManager.UriHashtbl.clear cache1
+;;
+
+(*
+let convert_context uri =
+  let name_of = function Cic.Name s -> s | _ -> "_" in
+  List.fold_right
+    (function 
+    | (Some (s, Cic.Decl t) as e) -> fun (nc,auxc,oc) ->
+       let t, _ = aux true oc auxc 0 uri t in
+       (name_of s, NCic.Decl t) :: nc, 
+       Ce (lazy ((name_of s, NCic.Decl t),[])) :: auxc,  e :: oc
+    | (Some (Cic.Name s, Cic.Def (t,ty)) as e) -> fun (nc,auxc,oc) ->
+       let t, _ = aux true oc auxc 0 uri t in
+       let t, _ = aux true oc auxc 0 uri ty in
+       (name_of s, NCic.Def (t,ty)) :: nc, 
+       Ce (lazy ((name_of s, NCic.Def (t,ty)),[])) :: auxc,  e :: oc
+    | None -> nc, , e :: oc
+;;
+
+let convert_term uri ctx t = 
+   aux false [] [] 0 uri t
+;;
+*)