From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 25 Apr 2009 20:30:15 +0000 (+0000)
Subject: The translation from old aliases to new references is now completely
X-Git-Tag: make_still_working~4050
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=070b11daefc90ecc20ebee73acc550aeac1c627b;p=helm.git

The translation from old aliases to new references is now completely
implemented. It cannot be correct, but it is not supposed to be anyway.
---

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index b5c08fba6..411f39361 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -91,30 +91,42 @@ let ncic_mk_choice = function
       (fun l->assert(l = []);
         let nuri = NUri.uri_of_string uri in
         try
-         let _,height,_,_,_ = NCicEnvironment.get_checked_obj nuri in
-          NCic.Const
-           (NReference.reference_of_spec nuri (NReference.Def height))
+         let _,height,_,_,obj = NCicEnvironment.get_checked_obj nuri in
+         let spec =
+          match obj with
+             NCic.Constant (_,_,None,_,_) -> NReference.Decl
+           | NCic.Constant (_,_,Some _,_,_) -> NReference.Def height
+           | NCic.Fixpoint (is_ind,fl,_) ->
+              (* CSC: bug here: name need not be the wanted name
+                 Solution: a real new _reference_ should arrive here *)
+              (match
+                HExtlib.list_index (fun (_,name',_,_,_) -> name=name') fl,is_ind
+               with
+                  None,_ -> assert false
+                | Some (i,(_,_,recno,_,_)),true-> NReference.Fix(i,recno,height)
+                | Some (i,(_,_,_,_,_)),false -> NReference.CoFix i)
+           | NCic.Inductive (inductive,leftno,il,_) ->
+              (match
+                HExtlib.list_index (fun (_,name',_,_) -> name=name') il
+               with
+                  None ->
+                   let cl =
+                    List.concat
+                     (HExtlib.list_mapi (fun (_,_,_,cl) i ->
+                       List.map (fun t -> i,t) cl) il)
+                   in
+                    (match
+                      HExtlib.list_index (fun i,(_,name',_) -> name=name') cl
+                     with
+                        None -> assert false
+                      | Some (j,(i,_)) -> NReference.Con (i,j,leftno))
+                | Some (i,_) -> NReference.Ind (inductive,i,leftno))
+         in
+          NCic.Const (NReference.reference_of_spec nuri spec)
         with
          NCicEnvironment.ObjectNotFound _ ->
-(*
-(*
-        if String.sub uri (String.length uri - 3) 3 = "def" then
-*)
-         let nuri = NUri.uri_of_string uri in(*
-          NUri.uri_of_string (String.sub uri 0 (String.length uri -3) ^ "def")
-         in
-*)
-          NCic.Const
-           (NReference.reference_of_spec nuri (NReference.Def 0))
-)
-*)
-(*
-        else
-*)
          let uri = UriManager.uri_of_string uri in
           fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
-(*
-*)
 ;;
 
 
diff --git a/helm/software/matita/tests/ng_commands.ma b/helm/software/matita/tests/ng_commands.ma
index dfe92269e..6a65ea039 100644
--- a/helm/software/matita/tests/ng_commands.ma
+++ b/helm/software/matita/tests/ng_commands.ma
@@ -38,12 +38,18 @@ alias id "P" = "cic:/matita/tests/ng_commands/P.con".
 
 ndefinition Q: Prop ≝ P.
 
-(*
 nlet rec nzero (n:nat) : nat ≝
  match n with
   [ O ⇒ O
   | S m ⇒ nzero m].
 
+alias id "nzero" = "cic:/matita/tests/ng_commands/nzero.con".
+
+ntheorem nzero_ok: nzero (S (S O)) = O.
+ napply (refl_eq ? O);
+nqed.
+
+(*
 ninductive nnat: Type ≝
    nO: nnat
  | nS: nnat → nnat. *)
\ No newline at end of file