From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 7 Apr 2008 09:57:46 +0000 (+0000)
Subject: reference type made private, added mk_constructor to be used
X-Git-Tag: make_still_working~5441
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=09dc8295b3ec33bfa731189788330ba21b5f1428;p=helm.git

reference type made private, added mk_constructor to be used
to create the i-th constructor of an inductive type (used in match typechecking).

fixed name capture in oCic2nCic when typing fixpoint types
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index ceb14d17c..46caae5ac 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -736,7 +736,7 @@ let rec typeof ~subst ~metasenv context term =
 *)
        eat_prods ~subst ~metasenv context ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
-   | C.Match (Ref.Ref (dummy_depth,uri,Ref.Ind tyno) as r,outtype,term,pl) ->
+   | C.Match (Ref.Ref (_,_,Ref.Ind tyno) as r,outtype,term,pl) ->
       let outsort = typeof_aux context outtype in
       let leftno = E.get_indty_leftno r in
       let parameters, arguments =
@@ -784,7 +784,7 @@ let rec typeof ~subst ~metasenv context term =
           (fun (j,b,old_p_ty,old_exp_p_ty) p ->
             if b then
               let cons = 
-                let cons = Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)) in
+                let cons = Ref.mk_constructor j r in
                 if parameters = [] then C.Const cons
                 else C.Appl (C.Const cons::parameters)
               in
@@ -804,7 +804,7 @@ let rec typeof ~subst ~metasenv context term =
          (TypeCheckerFailure 
           (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^
           "has type %s\nnot convertible with %s") (NCicPp.ppterm (C.Const 
-          (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)))))
+          (Ref.mk_constructor j r)))
           (NCicPp.ppterm ~context (List.nth pl (j-1)))
           (NCicPp.ppterm ~context p_ty) (NCicPp.ppterm ~context exp_p_ty)))); 
       let res = outtype::arguments@[term] in
diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml
index d83fee65a..4ecf74645 100644
--- a/helm/software/components/ng_kernel/nReference.ml
+++ b/helm/software/components/ng_kernel/nReference.ml
@@ -113,9 +113,16 @@ let string_of_reference (Ref (_,u,indinfo)) =
   | Con (i,j) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
 ;;
 
+let mk_constructor j = function
+  | Ref (d, u, Ind i) -> 
+      reference_of_string (string_of_reference (Ref (d, u, Con (i,j))))
+  | _ -> assert false
+;;
+
 let reference_of_ouri u indinfo =
   let u = NUri.nuri_of_ouri u in
   reference_of_string (string_of_reference (Ref (~-1,u,indinfo)))
 ;;
 
 let ouri_of_reference (Ref (_,u,_)) = NUri.ouri_of_nuri u;;
+
diff --git a/helm/software/components/ng_kernel/nReference.mli b/helm/software/components/ng_kernel/nReference.mli
index 26145ee79..de468c3c1 100644
--- a/helm/software/components/ng_kernel/nReference.mli
+++ b/helm/software/components/ng_kernel/nReference.mli
@@ -21,11 +21,14 @@ type spec =
  | Ind of int
  | Con of int * int (* indtyno, constrno *)
 
-type reference = Ref of int *  NUri.uri * spec
+type reference = private Ref of int *  NUri.uri * spec
 
 val eq: reference -> reference -> bool
 val string_of_reference: reference -> string 
 
+(* given the reference of an inductive type, returns the i-th contructor *)
+val mk_constructor: int -> reference -> reference
+
 
 (* CACCA *)
 val reference_of_ouri: UriManager.uri -> spec ->  reference
diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 2b59549d6..2244c12f8 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -113,13 +113,13 @@ let convert_term uri t =
         let rno = ref 0 in
         let bctx, fixpoints_tys, tys, _ = 
           List.fold_right 
-            (fun (name,recno,ty,_) (ctx, fixpoints, tys, idx) -> 
+            (fun (name,recno,ty,_) (bctx, fixpoints, tys, idx) -> 
               let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
               if idx = k then rno := recno;
               let r = 
                 NReference.reference_of_ouri buri (NReference.Fix (idx,recno)) 
               in
-              Fix (r,name,ty) :: ctx, fixpoints_ty@fixpoints,ty::tys,idx+1)
+              Fix (r,name,ty) :: bctx, fixpoints_ty@fixpoints,ty::tys,idx+1)
             fl ([], [], [], 0)
         in
         let bctx = bctx @ ctx in