The backward compatible management of aliases for NG is now fully completed.

Enjoy the NG Matita!

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 6b341f77c314a581e130e7e9e7f55ad712821334..5caafb67b89cb2de2467d6b2a0d645f834e5015a 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -763,7 +763,7 @@ prerr_endline "CSC: here we should fix the height!!!";
                NCicLibrary.add_obj uri obj;
                {status with 
                  GrafiteTypes.ng_status = 
-                  GrafiteTypes.CommandMode lexicon_status },`Old []
+                  GrafiteTypes.CommandMode lexicon_status },`New [uri]
        | _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
   | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> 
      Setoids.add_relation id a aeq refl sym trans;
@@ -789,7 +789,7 @@ prerr_endline "CSC: here we should fix the height!!!";
            NCicLibrary.add_obj uri obj;
            {status with 
              GrafiteTypes.ng_status=GrafiteTypes.CommandMode lexicon_status },
-           `Old []
+           `New [uri]
       | _ ->
         let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
         { status with
@@ -797,7 +797,7 @@ prerr_endline "CSC: here we should fix the height!!!";
             GrafiteTypes.ProofMode
              { NTacStatus.gstatus = ninitial_stack; 
                istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}}
-             },`Old [])
+             },`New [])
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with
@@ -888,13 +888,14 @@ prerr_endline "CSC: here we should fix the height!!!";
       eval_tactical status
        (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
   | GrafiteAst.NTactic (_(*loc*), tac, punct) ->
-      (match  status.GrafiteTypes.ng_status with
+      (match status.GrafiteTypes.ng_status with
       | GrafiteTypes.CommandMode _ -> assert false
       | GrafiteTypes.ProofMode nstatus ->
          let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
          let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
          NTacStatus.pp_tac_status nstatus;
-         { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, `Old [])
+         { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
+         `New [])
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
      let status = 
       eval_tactical status

diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml
index f99535d19da9e5b7430eab6c043a7a015d8aed1a..616c3ef5a1f3f71f6a6cdc37e21eecbbeb454518 100644 (file)
--- a/helm/software/components/lexicon/lexiconSync.ml
+++ b/helm/software/components/lexicon/lexiconSync.ml
@@ -92,7 +92,20 @@ let add_aliases_for_objs status =
        (fun status uri ->
          let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
           add_aliases_for_object status uri obj) status uris
-  | `New nrefs -> assert false
+  | `New nrefs ->
+     List.fold_left
+      (fun status nref ->
+        let references = NCicLibrary.aliases_of nref in
+        let new_env =
+         List.map
+          (fun u ->
+            let name = NCicPp.r2s true u in
+             DisambiguateTypes.Id name,
+              LexiconAst.Ident_alias (name,NReference.string_of_reference u)
+          ) references
+        in
+         LexiconEngine.set_proof_aliases status new_env
+      ) status nrefs
  
 module OrderedId = 
 struct

diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml
index be731ba924fa9c1a2df699b0973568a1d11018de..a558d99cfe98200fad80997f097affca1eec43b4 100644 (file)
--- a/helm/software/components/ng_cic_content/nTermCicContent.ml
+++ b/helm/software/components/ng_cic_content/nTermCicContent.ml
@@ -64,7 +64,7 @@ let nast_of_cic ~idref ~output_type ~subst ~context =
           idref (Ast.Ident (name,None))
         with Failure "nth" | Invalid_argument "List.nth" -> 
           idref (Ast.Ident ("-" ^ string_of_int (n - List.length ctx),None)))
-    | NCic.Const r -> idref (Ast.Ident (NCicPp.r2s false r, None))
+    | NCic.Const r -> idref (Ast.Ident (NCicPp.r2s true r, None))
     | NCic.Meta (n,lc) when List.mem_assoc n subst -> 
         let _,_,t,_ = List.assoc n subst in
          k ctx (NCicSubstitution.subst_meta lc t)

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index fa96a69b44224ff44c3642ae02d323152aa48c45..86822aa74b28f56878e4fdeffd4cb6e563178654 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -20,36 +20,45 @@ let aliases = ref [];;
 let resolve name =
  try
   HExtlib.filter_map
-   (fun (name',nref) -> if name'=name then Some nref else None) !aliases
+   (fun (_,name',nref) -> if name'=name then Some nref else None) !aliases
  with
   Not_found -> raise (ObjectNotFound (lazy name))
 ;;
 
+let aliases_of uri =
+ try
+  HExtlib.filter_map
+   (fun (uri',_,nref) -> if NUri.eq uri' uri then Some nref else None) !aliases
+ with
+  Not_found -> raise (ObjectNotFound (lazy (NUri.string_of_uri uri)))
+;;
+
 let add_obj u obj =
  storage := (u,obj)::!storage;
   let _,height,_,_,obj = obj in
   let references =
    match obj with
       NCic.Constant (_,name,None,_,_) ->
-       [name,NReference.reference_of_spec u NReference.Decl]
+       [u,name,NReference.reference_of_spec u NReference.Decl]
     | NCic.Constant (_,name,Some _,_,_) ->
-       [name,NReference.reference_of_spec u (NReference.Def height)]
+       [u,name,NReference.reference_of_spec u (NReference.Def height)]
     | NCic.Fixpoint (is_ind,fl,_) ->
        HExtlib.list_mapi
         (fun (_,name,recno,_,_) i ->
           if is_ind then
-           name,NReference.reference_of_spec u (NReference.Fix(i,recno,height))
+           u,name,NReference.reference_of_spec u(NReference.Fix(i,recno,height))
           else
-           name,NReference.reference_of_spec u (NReference.CoFix i)) fl
+           u,name,NReference.reference_of_spec u (NReference.CoFix i)) fl
     | NCic.Inductive (inductive,leftno,il,_) ->
        List.flatten
         (HExtlib.list_mapi
          (fun (_,iname,_,cl) i ->
            HExtlib.list_mapi
             (fun (_,cname,_) j->
-              cname,NReference.reference_of_spec u (NReference.Con (i,j,leftno))
+              u,cname,
+               NReference.reference_of_spec u (NReference.Con (i,j,leftno))
             ) cl @
-           [iname,
+           [u,iname,
              NReference.reference_of_spec u
               (NReference.Ind (inductive,i,leftno))]
          ) il)

diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli
index 357927f06c86468703bd6bf3624f5aa55148d3e5..fe3262109bd7ba9d93054e25ed73832484d60436 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.mli
+++ b/helm/software/components/ng_kernel/nCicLibrary.mli
@@ -14,6 +14,7 @@
 exception ObjectNotFound of string Lazy.t
 
 val add_obj: NUri.uri -> NCic.obj -> unit
+val aliases_of: NUri.uri -> NReference.reference list
 val resolve: string -> NReference.reference list
 val get_obj: NUri.uri -> NCic.obj
 

diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index cf8d6860b14608d60ef443ce01919a03c1483f8c..7e5b20860811c87afe4891317be25770988d22f9 100644 (file)
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -103,7 +103,15 @@ let eval_ast ?do_heavy_checks lexicon_status
        UriManager.buri_of_uri (UriManager.uri_of_string v) = 
        baseuri
       with
-       UriManager.IllFormedUri _ -> false (* v is a description, not a URI *)
+       UriManager.IllFormedUri _ ->
+        try
+         (* this too! *)
+         let NReference.Ref (uri,_) = NReference.reference_of_string v in
+         let ouri = NCic2OCic.ouri_of_nuri uri in
+          UriManager.buri_of_uri ouri = baseuri
+        with
+         NReference.IllFormedReference _ ->
+          false (* v is a description, not a URI *)
      in
       if b then 
        lexicon_status,acc

diff --git a/helm/software/matita/tests/ng_commands.ma b/helm/software/matita/tests/ng_commands.ma
index b597156499e152dc8533c6e17bf7e2a870f9800a..86226fb02204aaf3110869b082c4946aa8d36108 100644 (file)
--- a/helm/software/matita/tests/ng_commands.ma
+++ b/helm/software/matita/tests/ng_commands.ma
@@ -12,10 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* ATTENZIONE: si puo' eseguire solo con MatitaC e dopo aver scelto
-   Debug → always show all disambiguation errors (that, moreover, slows
-   down the library a lot) *)
-
 include "nat/plus.ma".
 
 ndefinition thesis0: ∀A:Type.Type ≝ λA. A → A.