Typo fixed.

[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 9f0bfc21133253c1f80f7ade3f62d5217cebc43f..6a9dd715a5bc6e79a9da108af9a9171e0083a39f 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -16,11 +16,11 @@ module Ref = NReference
 let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);;
 
 (* porcatissima *)
-type reference = Ref of int *  NUri.uri * NReference.spec
+type reference = Ref of NUri.uri * NReference.spec
 let reference_of_ouri u indinfo =
   let u = nuri_of_ouri u in
   NReference.reference_of_string
-   (NReference.string_of_reference (Obj.magic (Ref (max_int,u,indinfo))))
+   (NReference.string_of_reference (Obj.magic (Ref (u,indinfo))))
 ;;
 
 type ctx = 
@@ -323,10 +323,10 @@ let alpha t1 t2 ref ref' =
     | NCic.Prod (_,s1,t1), NCic.Prod (_,s2,t2) -> aux s1 s2; aux t1 t2
     | NCic.LetIn (_,s1,ty1,t1), NCic.LetIn (_,s2,ty2,t2) -> 
          aux s1 s2; aux ty1 ty2; aux t1 t2
-    | NCic.Const (NReference.Ref (_,uu1,xp1)), 
-      NCic.Const (NReference.Ref (_,uu2,xp2))  when 
-         let NReference.Ref (_,u1,_) = ref in
-         let NReference.Ref (_,u2,_) = ref' in
+    | NCic.Const (NReference.Ref (uu1,xp1)), 
+      NCic.Const (NReference.Ref (uu2,xp2))  when 
+         let NReference.Ref (u1,_) = ref in
+         let NReference.Ref (u2,_) = ref' in
            NUri.eq uu1 u1 && NUri.eq uu2 u2 && xp1 = xp2
       -> ()
     | NCic.Const r1, NCic.Const r2 when NReference.eq r1 r2 -> ()
@@ -356,13 +356,13 @@ let find_in_cache name obj ref =
    (function (ref',obj') ->
      let recno, fixno =
       match ref with
-         NReference.Ref (_,_,NReference.Fix (fixno,recno)) -> recno,fixno
-       | NReference.Ref (_,_,NReference.CoFix (fixno)) -> ~-1,fixno
+         NReference.Ref (_,NReference.Fix (fixno,recno,_)) -> recno,fixno
+       | NReference.Ref (_,NReference.CoFix (fixno)) -> ~-1,fixno
        | _ -> assert false in
      let recno',fixno' =
       match ref' with
-         NReference.Ref (_,_,NReference.Fix (fixno',recno)) -> recno,fixno'
-       | NReference.Ref (_,_,NReference.CoFix (fixno')) -> ~-1,fixno'
+         NReference.Ref (_,NReference.Fix (fixno',recno,_)) -> recno,fixno'
+       | NReference.Ref (_,NReference.CoFix (fixno')) -> ~-1,fixno'
        | _ -> assert false in
      if recno = recno' && fixno = fixno' && same_obj ref ref' (obj,obj') then (
 (*
@@ -379,14 +379,14 @@ prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==>
   begin
     match obj, ref with 
     | (_,_,_,_,NCic.Fixpoint (true,fl,_)) , 
-      NReference.Ref (x,y,NReference.Fix _) ->
+      NReference.Ref (y,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 (x,y,NReference.CoFix _) ->
+      NReference.Ref (y,NReference.CoFix _) ->
        ignore(List.fold_left (fun i (_,name,rno,_,_) ->
          let ref = NReference.mk_cofix i ref in
          Hashtbl.add cache name (ref,obj);
@@ -471,7 +471,7 @@ let convert_term uri t =
             (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)) 
+                reference_of_ouri buri (Ref.Fix (idx,recno,1)) 
               in
               bctx @ [Fix (lazy (r,name,ty))],
                fixpoints_ty@fixpoints,ty::tys,idx-1)
@@ -481,9 +481,9 @@ let convert_term uri t =
         let free_decls = Lazy.force free_decls in
         let bctx = 
           List.map (function ce -> match strictify ce with
-            | `Fix (Ref.Ref (_,_,Ref.Fix (idx, recno)),name, ty) ->
+            | `Fix (Ref.Ref (_,Ref.Fix (idx, recno,height)),name, ty) ->
               Fix (lazy (reference_of_ouri buri
-                    (Ref.Fix (idx,recno+free_decls)),name,ty))
+                    (Ref.Fix (idx,recno+free_decls,height)),name,ty))
             | _ -> assert false) bad_bctx @ ctx
         in
         let n_fl = List.length fl in
@@ -509,7 +509,7 @@ let convert_term uri t =
         let obj = 
           nuri_of_ouri buri,max_int,[],[],
             NCic.Fixpoint (true, fl, (`Generated, `Definition)) in
-        let r = reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno)) in
+        let r = reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno,1)) in
         let obj,r =
          let _,name,_,_,_ = List.nth fl fixno in
          match find_in_cache name obj r with
@@ -587,7 +587,7 @@ 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)
+               NCic.Const (reference_of_ouri curi (Ref.Def 1))
         | Cic.Constant (_,None,_,_,_) ->
                NCic.Const (reference_of_ouri curi Ref.Decl)
         | _ -> assert false)