From 0caee5d7da2d106650189660f4c74928a42b8b16 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 26 Apr 2009 10:51:38 +0000 Subject: [PATCH] The backward compatible management of aliases for NG is now fully completed. Enjoy the NG Matita! --- .../grafite_engine/grafiteEngine.ml | 11 +++++---- .../components/lexicon/lexiconSync.ml | 15 +++++++++++- .../ng_cic_content/nTermCicContent.ml | 2 +- .../components/ng_kernel/nCicLibrary.ml | 23 +++++++++++++------ .../components/ng_kernel/nCicLibrary.mli | 1 + helm/software/matita/matitaEngine.ml | 10 +++++++- helm/software/matita/tests/ng_commands.ma | 4 ---- 7 files changed, 47 insertions(+), 19 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 6b341f77c..5caafb67b 100644 --- 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 f99535d19..616c3ef5a 100644 --- 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 be731ba92..a558d99cf 100644 --- 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 fa96a69b4..86822aa74 100644 --- 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 357927f06..fe3262109 100644 --- 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 cf8d6860b..7e5b20860 100644 --- 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 b59715649..86226fb02 100644 --- 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. -- 2.39.2