From 11b2157bacf59cfc561c2ef6f92ee41ee2c1a006 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 3 Jun 2009 08:56:58 +0000 Subject: [PATCH] Huge commit with several changes: 1) CicNotationPres.render: type changed to make it more general (no dependency on the Hashtbl) and URI/REFERENCE agnostic. A compatibility function CicNotationPres.lookup_uri is provided to easily map the (old) Hashtbl to the (new) lookup function. 2) user interface partially changed to render NG objects in the CicBrowser and to follow NG hyperlinks 3) New CicNotationPt entries NRef (similar to Uri) and NRefPattern (similar to UriPattern) to avoid hijacking the old Uris (actually, uris + xpointers) to also hold new references. This allows to properly implement notation (for NG) and to properly handle hyperlinks. 4) all remaining Warnings for unused variables fixed (in some way or another, hopefully the correct one) 5) GrafiteEngine, NQed: the height of an object is now recomputed just before putting it in the environment. This fixes all the bugs related to reduction. 6) GrafiteParser/LexiconEngine: both old URIs and new references are now allowed in NG terms and in notations 7) ng_cic_content: rendering functions now return an "id |-> reference" table to correctly implement MathML hrefs 8) NReference: new compare function 9) NCicUntrusted: new height_of_obj_kind function (to be used in GrafiteEngine) 10) OCic2NCic: new reference_of_oxuri function to map old uris + xpointers into new references 11) bug fixed: after the commit by Enrico that starts using the extensible PTS, the old-to-new objects translations used to map Type into "Type" which was not declared. Type is now mapped into Type[0] and Type (as a "notation") is now a synonim of Type[0] (only during parsing for now) 12) bug fixed: after the commit by Enrico that cleans up terms for alpha-conversion and dummy products, the test in NCicTypeChecker that verifies the consistency of left parameters in constructor --- that used to do that NOT up to alpha-conversion --- used to fail when dummy products were found. The test is now relaxed to include alpha-conversion. 13) bug fixed: NCicTypeChecker did not verify that a .dec reference pointed to an axiom and that a .def reference did not point to an axiom. Fixed. --- .../METAS/meta.helm-acic_content.src | 2 +- helm/software/components/Makefile | 2 +- .../acic_content/acic2astMatcher.ml | 3 + .../components/acic_content/cicNotationPp.ml | 5 +- .../components/acic_content/cicNotationPt.ml | 2 + .../acic_content/cicNotationUtil.ml | 13 ++++- .../acic_content/cicNotationUtil.mli | 3 +- .../acic_content/termAcicContent.ml | 1 + .../components/binaries/transcript/.depend | 5 ++ .../binaries/transcript/.depend.opt | 5 ++ .../cic_disambiguation/cicDisambiguate.ml | 6 +- .../components/cic_proof_checking/cicPp.ml | 2 +- .../content_pres/cicNotationLexer.ml | 12 ++++ .../content_pres/cicNotationParser.ml | 1 + .../content_pres/cicNotationPres.ml | 15 ++--- .../content_pres/cicNotationPres.mli | 5 +- .../components/content_pres/content2pres.ml | 3 +- .../components/content_pres/sequent2pres.ml | 13 ++++- .../components/content_pres/sequent2pres.mli | 1 + .../components/disambiguation/disambiguate.ml | 1 + .../components/grafite/grafiteAstPp.ml | 4 ++ .../grafite_engine/grafiteEngine.ml | 42 +++++++------- .../grafite_parser/grafiteParser.ml | 4 ++ .../components/grafite_parser/test_parser.ml | 3 +- .../components/lexicon/lexiconEngine.ml | 15 +++-- .../components/lexicon/lexiconMarshal.ml | 1 + .../ng_cic_content/nTermCicContent.ml | 55 +++++++++++-------- .../ng_cic_content/nTermCicContent.mli | 8 ++- .../ng_cic_content/ncic2astMatcher.ml | 8 ++- .../ng_disambiguation/nCicDisambiguate.ml | 8 ++- .../components/ng_kernel/nCicTypeChecker.ml | 14 ++--- .../components/ng_kernel/nCicUntrusted.ml | 39 +++++++++++++ .../components/ng_kernel/nCicUntrusted.mli | 2 + .../components/ng_kernel/nReference.ml | 7 ++- .../components/ng_kernel/nReference.mli | 1 + .../components/ng_kernel/oCic2NCic.ml | 13 +++-- .../components/ng_kernel/oCic2NCic.mli | 2 + .../components/ng_tactics/nCicElim.ml | 2 +- .../components/syntax_extensions/.depend | 3 + helm/software/components/tactics/setoids.ml | 4 +- .../components/tptp_grafite/tptp2grafite.ml | 4 +- .../components/urimanager/uriManager.ml | 1 - helm/software/matita/applyTransformation.ml | 23 +++++--- helm/software/matita/applyTransformation.mli | 2 + helm/software/matita/matita.ml | 11 +++- helm/software/matita/matitaGuiTypes.mli | 1 + helm/software/matita/matitaMathView.ml | 42 +++++++++++++- helm/software/matita/matitaScript.ml | 4 +- helm/software/matita/matitaTypes.ml | 2 + helm/software/matita/matitaTypes.mli | 1 + 50 files changed, 315 insertions(+), 111 deletions(-) diff --git a/helm/software/components/METAS/meta.helm-acic_content.src b/helm/software/components/METAS/meta.helm-acic_content.src index 8e10b789e..0013afa41 100644 --- a/helm/software/components/METAS/meta.helm-acic_content.src +++ b/helm/software/components/METAS/meta.helm-acic_content.src @@ -1,4 +1,4 @@ -requires="helm-library" +requires="helm-library helm-ng_kernel" version="0.0.1" archive(byte)="acic_content.cma" archive(native)="acic_content.cmxa" diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile index f9897ec79..3303e7a59 100644 --- a/helm/software/components/Makefile +++ b/helm/software/components/Makefile @@ -23,8 +23,8 @@ MODULES = \ cic_exportation \ metadata \ library \ - acic_content \ ng_kernel \ + acic_content \ grafite \ ng_cic_content \ content_pres \ diff --git a/helm/software/components/acic_content/acic2astMatcher.ml b/helm/software/components/acic_content/acic2astMatcher.ml index 908aa942f..2062b6c06 100644 --- a/helm/software/components/acic_content/acic2astMatcher.ml +++ b/helm/software/components/acic_content/acic2astMatcher.ml @@ -35,6 +35,7 @@ struct type cic_mask_t = Blob | Uri of UriManager.uri + | NRef of NReference.reference | Appl of cic_mask_t list let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t) @@ -52,6 +53,7 @@ struct Hashtbl.hash mask, tl let mask_of_appl_pattern = function + | Ast.NRefPattern nref -> NRef nref, [] | Ast.UriPattern uri -> Uri uri, [] | Ast.ImplicitPattern | Ast.VarPattern _ -> Blob, [] @@ -71,6 +73,7 @@ struct | Ast.ImplicitPattern | Ast.VarPattern _ -> PatternMatcher.Variable | Ast.UriPattern _ + | Ast.NRefPattern _ | Ast.ApplPattern _ -> PatternMatcher.Constructor end diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index b2cb12f92..0d868c002 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -138,8 +138,8 @@ let rec pp_term ?(pp_parens = true) t = (String.concat " and " (List.map map definitions)) (pp_term term) | Ast.Ident (name, Some []) | Ast.Ident (name, None) - | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> - name + | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name + | Ast.NRef nref -> NReference.string_of_reference nref | Ast.Ident (name, Some substs) | Ast.Uri (name, Some substs) -> sprintf "%s \\subst [%s]" name (pp_substs substs) @@ -357,6 +357,7 @@ let pp_env env = let rec pp_cic_appl_pattern = function | Ast.UriPattern uri -> UriManager.string_of_uri uri + | Ast.NRefPattern nref -> NReference.string_of_reference nref | Ast.VarPattern name -> name | Ast.ImplicitPattern -> "?" | Ast.ApplPattern aps -> diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml index 46381e4bc..8dbfea799 100644 --- a/helm/software/components/acic_content/cicNotationPt.ml +++ b/helm/software/components/acic_content/cicNotationPt.ml @@ -92,6 +92,7 @@ type term = | UserInput (* place holder for user input, used by MatitaConsole, not to be used elsewhere *) | Uri of string * subst list option (* as Ident, for long names *) + | NRef of NReference.reference (* Syntax pattern extensions *) @@ -164,6 +165,7 @@ type argument_pattern = type cic_appl_pattern = | UriPattern of UriManager.uri + | NRefPattern of NReference.reference | VarPattern of string | ImplicitPattern | ApplPattern of cic_appl_pattern list diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml index 60fe6357d..b426863cf 100644 --- a/helm/software/components/acic_content/cicNotationUtil.ml +++ b/helm/software/components/acic_content/cicNotationUtil.ml @@ -62,6 +62,7 @@ let visit_ast ?(special_k = fun _ -> assert false) | Ast.Magic _ | Ast.Variable _) as t -> special_k t | (Ast.Ident _ + | Ast.NRef _ | Ast.Implicit | Ast.Num _ | Ast.Sort _ @@ -326,13 +327,21 @@ let dressn ~sep:sauces = let find_appl_pattern_uris ap = let rec aux acc = function - | Ast.UriPattern uri -> uri :: acc + | Ast.UriPattern uri -> `Uri uri :: acc + | Ast.NRefPattern nref -> `NRef nref :: acc | Ast.ImplicitPattern | Ast.VarPattern _ -> acc | Ast.ApplPattern apl -> List.fold_left aux acc apl in let uris = aux [] ap in - HExtlib.list_uniq (List.fast_sort UriManager.compare uris) + let cmp u1 u2 = + match u1,u2 with + `Uri u1, `Uri u2 -> UriManager.compare u1 u2 + | `NRef r1, `NRef r2 -> NReference.compare r1 r2 + | `Uri _,`NRef _ -> -1 + | `NRef _, `Uri _ -> 1 + in + HExtlib.list_uniq (List.fast_sort cmp uris) let rec find_branch = function diff --git a/helm/software/components/acic_content/cicNotationUtil.mli b/helm/software/components/acic_content/cicNotationUtil.mli index 5a4e1c536..77350a2ac 100644 --- a/helm/software/components/acic_content/cicNotationUtil.mli +++ b/helm/software/components/acic_content/cicNotationUtil.mli @@ -76,7 +76,8 @@ val group: CicNotationPt.term list -> CicNotationPt.term val ungroup: CicNotationPt.term list -> CicNotationPt.term list val find_appl_pattern_uris: - CicNotationPt.cic_appl_pattern -> UriManager.uri list + CicNotationPt.cic_appl_pattern -> + [`Uri of UriManager.uri | `NRef of NReference.reference] list val find_branch: CicNotationPt.term -> CicNotationPt.term diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index 9176a8b56..0c0b02328 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -507,6 +507,7 @@ let instantiate_appl_pattern in let rec aux = function | Ast.UriPattern uri -> term_of_uri uri + | Ast.NRefPattern _ -> assert false | Ast.ImplicitPattern -> mk_implicit false | Ast.VarPattern name -> lookup name | Ast.ApplPattern terms -> mk_appl (List.map aux terms) diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index bb6f22a64..87d1ed25c 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,6 +1,11 @@ gallina8Parser.cmi: types.cmo grafiteParser.cmi: types.cmo grafite.cmi: types.cmo +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmo gallina8Parser.cmi diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index efadc681e..f17459162 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,6 +1,11 @@ gallina8Parser.cmi: types.cmx grafiteParser.cmi: types.cmx grafite.cmi: types.cmx +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmx gallina8Parser.cmi diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml index b869536bf..749f1434d 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml @@ -392,8 +392,10 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri List.fold_right (build_term inductiveFuns) inductiveFuns cic_body) | CicNotationPt.Ident _ - | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed - | CicNotationPt.Ident (name, subst) + | CicNotationPt.Uri _ + | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed + | CicNotationPt.NRef _ -> assert false + | CicNotationPt.Ident (name,subst) | CicNotationPt.Uri (name, subst) as ast -> let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in (try diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml index 58f319f4a..97213404e 100644 --- a/helm/software/components/cic_proof_checking/cicPp.ml +++ b/helm/software/components/cic_proof_checking/cicPp.ml @@ -412,7 +412,7 @@ let rec check_rec ctx string_name = | Cic.Cast (te,ty) -> check_rec ctx string_name te | Cic.Prod (name,so,dest) -> let l_string_name = check_rec ctx string_name so in - check_rec (name::ctx) string_name dest + check_rec (name::ctx) l_string_name dest | Cic.Lambda (name,so,dest) -> let string_name = match name with diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml index 17a5bd5bb..21031d002 100644 --- a/helm/software/components/content_pres/cicNotationLexer.ml +++ b/helm/software/components/content_pres/cicNotationLexer.ml @@ -149,6 +149,17 @@ let regexp uri = ('.' ident)+ (* ext *) ("#xpointer(" number ('/' number)+ ")")? (* xpointer *) +let regexp nreference = + "cic:/" (* schema *) + uri_step ('/' uri_step)* (* path *) + '.' + ( "dec" + | "def" "(" number ")" + | "fix" "(" number "," number "," number ")" + | "cfx" "(" number ")" + | "ind" "(" number "," number "," number ")" + | "con" "(" number "," number "," number ")") (* ext + reference *) + let error lexbuf msg = let begin_cnum, end_cnum = Ulexing.loc lexbuf in raise (Error (begin_cnum, end_cnum, msg)) @@ -311,6 +322,7 @@ and level2_ast_token = | pident -> handle_keywords lexbuf (Hashtbl.mem !level2_ast_keywords) "PIDENT" | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf) | tex_token -> return lexbuf (expand_macro lexbuf) + | nreference -> return lexbuf ("NREF", Ulexing.utf8_lexeme lexbuf) | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf) | qstring -> return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf)) diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index bb3d29f06..117f0926e 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -748,6 +748,7 @@ EXTEND return_term loc (Ast.Ident (id, Some s)) | s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0)) | u = URI -> return_term loc (Ast.Uri (u, None)) + | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r)) | n = NUMBER -> return_term loc (Ast.Num (n, 0)) | IMPLICIT -> return_term loc (Ast.Implicit) | PLACEHOLDER -> return_term loc Ast.UserInput diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index 1a092909e..35f128a05 100644 --- a/helm/software/components/content_pres/cicNotationPres.ml +++ b/helm/software/components/content_pres/cicNotationPres.ml @@ -200,16 +200,17 @@ let add_parens child_prec curr_prec t = BoxPp.render_to_string (function x::_->x|_->assert false) ~map_unicode_to_tex:false 80 t);*)t) -let render ids_to_uris ?(prec=(-1)) = +let lookup_uri ids_to_uris id = + try + let uri = Hashtbl.find ids_to_uris id in + Some (UriManager.string_of_uri uri) + with Not_found -> None +;; + +let render ~lookup_uri ?(prec=(-1)) = let module A = Ast in let module P = Mpresentation in (* let use_unicode = true in *) - let lookup_uri id = - (try - let uri = Hashtbl.find ids_to_uris id in - Some (UriManager.string_of_uri uri) - with Not_found -> None) - in let make_href xmlattrs xref = let xref_uris = List.fold_right diff --git a/helm/software/components/content_pres/cicNotationPres.mli b/helm/software/components/content_pres/cicNotationPres.mli index 1d06d19ba..6a25e5672 100644 --- a/helm/software/components/content_pres/cicNotationPres.mli +++ b/helm/software/components/content_pres/cicNotationPres.mli @@ -35,11 +35,14 @@ val box_of_mpres: mathml_markup -> boxml_markup (** {2 Rendering} *) +val lookup_uri: (Cic.id,UriManager.uri) Hashtbl.t -> Cic.id -> string option + (** level 1 -> level 0 * @param ids_to_uris mapping id -> uri for hyperlinking * @param prec precedence level *) val render: - (Cic.id, UriManager.uri) Hashtbl.t -> ?prec:int -> CicNotationPt.term -> markup + lookup_uri:(Cic.id -> string option) -> ?prec:int -> CicNotationPt.term -> + markup (** level 0 -> xml stream *) val print_xml: markup -> Xml.token Stream.t diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index fc3a47b5e..46f53d886 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -982,5 +982,6 @@ let content2pres TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in CicNotationPres.box_of_mpres - (CicNotationPres.render ids_to_uris ~prec + (CicNotationPres.render + ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) ~prec (TermContentPres.pp_ast ast))) diff --git a/helm/software/components/content_pres/sequent2pres.ml b/helm/software/components/content_pres/sequent2pres.ml index b1bc38758..549f5c7c5 100644 --- a/helm/software/components/content_pres/sequent2pres.ml +++ b/helm/software/components/content_pres/sequent2pres.ml @@ -102,12 +102,19 @@ let sequent2pres ~ids_to_inner_sorts = TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in CicNotationPres.box_of_mpres - (CicNotationPres.render ids_to_uris + (CicNotationPres.render + ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) (TermContentPres.pp_ast ast))) -let nsequent2pres ~subst = +let nsequent2pres ~ids_to_nrefs ~subst = + let lookup_uri id = + try + let nref = Hashtbl.find ids_to_nrefs id in + Some (NReference.string_of_reference nref) + with Not_found -> None + in sequent2pres0 (fun ast -> CicNotationPres.box_of_mpres - (CicNotationPres.render (Hashtbl.create 1) + (CicNotationPres.render ~lookup_uri (TermContentPres.pp_ast ast))) diff --git a/helm/software/components/content_pres/sequent2pres.mli b/helm/software/components/content_pres/sequent2pres.mli index 6866cd3ae..a19e7b195 100644 --- a/helm/software/components/content_pres/sequent2pres.mli +++ b/helm/software/components/content_pres/sequent2pres.mli @@ -38,5 +38,6 @@ val sequent2pres : CicNotationPres.boxml_markup val nsequent2pres : + ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t -> subst:NCic.substitution -> CicNotationPt.term Content.conjecture -> CicNotationPres.boxml_markup diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml index fa63d1f48..ca6146e56 100644 --- a/helm/software/components/disambiguation/disambiguate.ml +++ b/helm/software/components/disambiguation/disambiguate.ml @@ -310,6 +310,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function [] subst in [ Node ([loc], Id name, terms) ])) | Ast.Uri _ -> [] + | Ast.NRef _ -> [] | Ast.Implicit -> [] | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ] | Ast.Meta (index, local_context) -> diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index b74677949..e335c1b63 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -101,6 +101,7 @@ let pp_ntactic ~map_unicode_to_tex = function | NId _ -> "nid" | NIntro (_,n) -> "#" ^ n | NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false + | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> assert false ;; let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = @@ -394,6 +395,9 @@ let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = | NonPunctuationTactical (_, tac, punct) -> pp_non_punctuation_tactical tac ^ pp_punctuation_tactical punct + | NNonPunctuationTactical (_, tac, punct) -> + pp_non_punctuation_tactical tac + ^ pp_punctuation_tactical punct | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "." let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index a0fdb92d7..8101dd667 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -760,8 +760,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let name = UriManager.name_of_uri uri in let obj = Cic.Constant (name,Some (Lazy.force bo),ty,[],attrs) in let status, lemmas = add_obj uri obj status in - {status with - GrafiteTypes.proof_status = GrafiteTypes.No_proof}, + {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, (*CSC: I throw away the arities *) `Old (uri::lemmas) | GrafiteAst.NQed loc -> @@ -769,30 +768,29 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status | GrafiteTypes.ProofMode { NTacStatus.istatus = {NTacStatus.pstatus = pstatus; lstatus=lexicon_status} } -> - let uri,height,menv,subst,obj = pstatus in + let uri,height,menv,subst,obj_kind = pstatus in if menv <> [] then raise (GrafiteTypes.Command_error"You can't Qed an incomplete theorem") else - let obj = -prerr_endline "CSC: here we should fix the height!!!"; - (uri,height,[],[], - NCicUntrusted.map_obj_kind - (NCicUntrusted.apply_subst subst []) - obj) in - NCicTypeChecker.typecheck_obj obj; - NCicLibrary.add_obj uri obj; - let objs = NCicElim.mk_elims obj in - let uris = - uri:: - List.map - (fun (uri,_,_,_,_) as obj -> - NCicTypeChecker.typecheck_obj obj; - NCicLibrary.add_obj uri obj; - uri - ) objs - in - {status with + let obj_kind = + NCicUntrusted.map_obj_kind + (NCicUntrusted.apply_subst subst []) obj_kind in + let height = NCicUntrusted.height_of_obj_kind uri obj_kind in + let obj = uri,height,[],[],obj_kind in + NCicTypeChecker.typecheck_obj obj; + NCicLibrary.add_obj uri obj; + let objs = NCicElim.mk_elims obj in + let uris = + uri:: + List.map + (fun (uri,_,_,_,_) as obj -> + NCicTypeChecker.typecheck_obj obj; + NCicLibrary.add_obj uri obj; + uri + ) objs + in + {status with GrafiteTypes.ng_status = GrafiteTypes.CommandMode lexicon_status },`New uris | _ -> raise (GrafiteTypes.Command_error "Not in proof mode")) diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index d0a97072c..ce7f5c6ca 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -709,6 +709,7 @@ EXTEND ]; level3_term: [ [ u = URI -> N.UriPattern (UriManager.uri_of_string u) + | r = NREF -> N.NRefPattern (NReference.reference_of_string r) | IMPLICIT -> N.ImplicitPattern | id = IDENT -> N.VarPattern id | LPAREN; terms = LIST1 SELF; RPAREN -> @@ -748,6 +749,9 @@ EXTEND | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> G.NObj (loc, N.Theorem (nflavour, name, typ, body)) + | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); + body = term -> + G.NObj (loc, N.Theorem (nflavour, name, N.Implicit, Some body)) | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> G.Obj (loc, N.Theorem (flavour, name, typ, body)) diff --git a/helm/software/components/grafite_parser/test_parser.ml b/helm/software/components/grafite_parser/test_parser.ml index 76c402c19..c87d41ed5 100644 --- a/helm/software/components/grafite_parser/test_parser.ml +++ b/helm/software/components/grafite_parser/test_parser.ml @@ -41,7 +41,8 @@ let dump_xml t id_to_uri fname = prerr_endline (sprintf "dumping MathML to %s ..." fname); flush stdout; let oc = open_out fname in - let markup = CicNotationPres.render id_to_uri t in + let markup = + CicNotationPres.render ~lookup_uri:(CicNotationPres.lookup_uri id_to_uri)t in let xml_stream = CicNotationPres.print_xml markup in Xml.pp_to_outchan xml_stream oc; close_out oc diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml index c86e16135..805da25c8 100644 --- a/helm/software/components/lexicon/lexiconEngine.ml +++ b/helm/software/components/lexicon/lexiconEngine.ml @@ -120,12 +120,15 @@ let rec eval_command ?(mode=L.WithPreferences) status cmd = -> let item = DisambiguateTypes.Id id in begin try - let uri = - match DisambiguateTypes.Environment.find item status.aliases with - L.Ident_alias (_, uri)-> UriManager.uri_of_string uri - | _ -> assert false - in - CicNotationPt.UriPattern uri + match DisambiguateTypes.Environment.find item status.aliases with + L.Ident_alias (_, uri) -> + (try + CicNotationPt.NRefPattern + (NReference.reference_of_string uri) + with + NReference.IllFormedReference _ -> + CicNotationPt.UriPattern (UriManager.uri_of_string uri)) + | _ -> assert false with Not_found -> prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^ (DisambiguateTypes.string_of_domain_item item)); diff --git a/helm/software/components/lexicon/lexiconMarshal.ml b/helm/software/components/lexicon/lexiconMarshal.ml index 7b9422db5..ba7e583d5 100644 --- a/helm/software/components/lexicon/lexiconMarshal.ml +++ b/helm/software/components/lexicon/lexiconMarshal.ml @@ -45,6 +45,7 @@ let rehash_cmd_uris = function | CicNotationPt.UriPattern uri -> CicNotationPt.UriPattern (rehash_uri uri) + | CicNotationPt.NRefPattern _ -> assert false | CicNotationPt.ApplPattern args -> CicNotationPt.ApplPattern (List.map aux args) | CicNotationPt.VarPattern _ diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index 2022797a2..da8061fde 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -32,6 +32,8 @@ module Ast = CicNotationPt let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () +type id = string + (* type interpretation_id = int @@ -47,15 +49,20 @@ let get_types uri = | _ -> assert false *) -let idref () = +let idref register_ref = let id = ref 0 in - function t -> + fun ?reference t -> incr id; - Ast.AttributedTerm (`IdRef ("i" ^ string_of_int !id), t) + let id = "i" ^ string_of_int !id in + (match reference with None -> () | Some r -> register_ref id r); + Ast.AttributedTerm (`IdRef id, t) ;; (* CODICE c&p da NCicPp *) -let nast_of_cic0 ~idref ~output_type ~subst k ~context = +let nast_of_cic0 + ~(idref: + ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term) + ~output_type ~subst k ~context = function | NCic.Rel n -> (try @@ -64,7 +71,7 @@ let nast_of_cic0 ~idref ~output_type ~subst k ~context = idref (Ast.Ident (name,None)) with Failure "nth" | Invalid_argument "List.nth" -> idref (Ast.Ident ("-" ^ string_of_int (n - List.length context),None))) - | NCic.Const r -> idref (Ast.Ident (NCicPp.r2s true r, None)) + | NCic.Const r -> idref ~reference:r (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 ~context (NCicSubstitution.subst_meta lc t) @@ -236,31 +243,31 @@ let instantiate32 idrefs env symbol args = else Ast.Appl (head :: List.map instantiate_arg args) let rec nast_of_cic1 ~idref ~output_type ~subst ~context term = -(* - let register_uri id uri = assert false in -*) match (get_compiled32 ()) term with | None -> nast_of_cic0 ~idref ~output_type ~subst (nast_of_cic1 ~idref ~output_type ~subst) ~context term | Some (env, ctors, pid) -> let idrefs = -(* - List.map - (fun term -> - let idref = idref term in - (try - register_uri idref - (CicUtil.uri_of_term (Deannotate.deannotate_term term)) - with Invalid_argument _ -> ()); - idref) - ctors -*) [] + List.map + (fun term -> + let attrterm = + idref + ~reference: + (match term with NCic.Const nref -> nref | _ -> assert false) + (CicNotationPt.Ident ("dummy",None)) + in + match attrterm with + Ast.AttributedTerm (`IdRef id, _) -> id + | _ -> assert false + ) ctors in let env = List.map (fun (name, term) -> - name, nast_of_cic1 ~idref ~output_type ~subst ~context term) env + name, + nast_of_cic1 ~idref ~output_type ~subst ~context term + ) env in let _, symbol, args, _ = try @@ -382,7 +389,11 @@ let instantiate_appl_pattern let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) = let module K = Content in - let nast_of_cic = nast_of_cic1 ~idref:(idref ()) ~output_type:`Term ~subst in + let ids_to_refs = Hashtbl.create 211 in + let register_ref = Hashtbl.add ids_to_refs in + let nast_of_cic = + nast_of_cic1 ~idref:(idref register_ref) ~output_type:`Term + ~subst in let context',_ = List.fold_right (fun item (res,context) -> @@ -411,6 +422,6 @@ let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) = })::res,item::context ) context ([],[]) in - "-1",i,context',nast_of_cic ~context ty + ("-1",i,context',nast_of_cic ~context ty), ids_to_refs ;; diff --git a/helm/software/components/ng_cic_content/nTermCicContent.mli b/helm/software/components/ng_cic_content/nTermCicContent.mli index fb6236553..5f1388bb2 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.mli +++ b/helm/software/components/ng_cic_content/nTermCicContent.mli @@ -82,4 +82,10 @@ val nast_of_cic : subst:NCic.substitution -> context:NCic.context -> NCic.term -> CicNotationPt.term *) -val nmap_sequent : subst:NCic.substitution -> int * NCic.conjecture -> CicNotationPt.term Content.conjecture + +type id = string + +val nmap_sequent: + subst:NCic.substitution -> int * NCic.conjecture -> + CicNotationPt.term Content.conjecture * + (id, NReference.reference) Hashtbl.t (* id -> reference *) diff --git a/helm/software/components/ng_cic_content/ncic2astMatcher.ml b/helm/software/components/ng_cic_content/ncic2astMatcher.ml index 099e0b26a..41d9aa08c 100644 --- a/helm/software/components/ng_cic_content/ncic2astMatcher.ml +++ b/helm/software/components/ng_cic_content/ncic2astMatcher.ml @@ -34,14 +34,14 @@ struct struct type cic_mask_t = Blob - | Uri of UriManager.uri + | NRef of NReference.reference | Appl of cic_mask_t list let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t) let mask_of_cic = function | NCic.Appl tl -> Appl (List.map (fun _ -> Blob) tl), tl - | NCic.Const nref -> Uri (NCic2OCic.ouri_of_reference nref), [] + | NCic.Const nref -> NRef nref, [] | _ -> Blob, [] let tag_of_term t = @@ -49,7 +49,8 @@ struct Hashtbl.hash mask, tl let mask_of_appl_pattern = function - | Ast.UriPattern uri -> Uri uri, [] + | Ast.UriPattern uri -> NRef (OCic2NCic.reference_of_oxuri uri), [] + | Ast.NRefPattern nref -> NRef nref, [] | Ast.ImplicitPattern | Ast.VarPattern _ -> Blob, [] | Ast.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl @@ -70,6 +71,7 @@ struct | Ast.ImplicitPattern | Ast.VarPattern _ -> PatternMatcher.Variable | Ast.UriPattern _ + | Ast.NRefPattern _ | Ast.ApplPattern _ -> PatternMatcher.Constructor end diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 5ded5b886..6e72042e8 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -312,7 +312,8 @@ let interpretate_term_and_interpretate_term_option NCic.LetIn (cic_name, cic_typ, cic_def, cic_body) | CicNotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term | CicNotationPt.Ident _ - | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed + | CicNotationPt.Uri _ + | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed | CicNotationPt.Ident (name, subst) -> assert (subst = None); (try @@ -321,12 +322,13 @@ let interpretate_term_and_interpretate_term_option try NCic.Const (List.assoc name obj_context) with Not_found -> Disambiguate.resolve ~env ~mk_choice (Id name) (`Args [])) - | CicNotationPt.Uri (name, subst) -> + | CicNotationPt.Uri (uri, subst) -> assert (subst = None); (try - NCic.Const (NRef.reference_of_string name) + NCic.Const (OCic2NCic.reference_of_oxuri(UriManager.uri_of_string uri)) with NRef.IllFormedReference _ -> CicNotationPt.fail loc "Ill formed reference") + | CicNotationPt.NRef nref -> NCic.Const nref | CicNotationPt.Implicit -> NCic.Implicit `Term | CicNotationPt.UserInput -> NCic.Implicit `Hole | CicNotationPt.Num (num, i) -> diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 8beca4cf0..0d3fc07d1 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -744,13 +744,11 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl = (fun context item1 item2 -> let convertible = match item1,item2 with - (n1,C.Decl ty1),(n2,C.Decl ty2) -> - n1 = n2 && + (_,C.Decl ty1),(_,C.Decl ty2) -> R.are_convertible ~metasenv ~subst context ty1 ty2 - | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) -> - n1 = n2 - && R.are_convertible ~metasenv ~subst context ty1 ty2 - && R.are_convertible ~metasenv ~subst context bo1 bo2 + | (_,C.Def (bo1,ty1)),(_,C.Def (bo2,ty2)) -> + R.are_convertible ~metasenv ~subst context ty1 ty2 && + R.are_convertible ~metasenv ~subst context bo1 bo2 | _,_ -> false in if not convertible then @@ -1079,8 +1077,8 @@ and type_of_constant ((Ref.Ref (uri,_)) as ref) = let _,_,recno1,arity,_ = List.nth fl i in if h1 <> h2 || recno1 <> recno2 then error (); arity - | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,Ref.Decl) -> ty - | (_,h1,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,Ref.Def h2) -> + | (_,_,_,_,C.Constant (_,_,None,ty,_)), Ref.Ref (_,Ref.Decl) -> ty + | (_,h1,_,_,C.Constant (_,_,Some _,ty,_)), Ref.Ref (_,Ref.Def h2) -> if h1 <> h2 then error (); ty | _ -> diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index baae7f9c2..dc26794a1 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -209,3 +209,42 @@ let rec apply_subst_metasenv subst = function (i,(name,apply_subst_context subst ctx,apply_subst subst ctx ty)) :: apply_subst_metasenv subst tl ;; + +let height_of_term tl = + let h = ref 0 in + let get_height (NReference.Ref (uri,_)) = + let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in + height in + let rec aux = + function + NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l + | NCic.Meta _ -> () + | NCic.Rel _ + | NCic.Sort _ -> () + | NCic.Implicit _ -> assert false + | NCic.Const nref -> h := max !h (get_height nref) + | NCic.Prod (_,t1,t2) + | NCic.Lambda (_,t1,t2) -> aux t1; aux t2 + | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t + | NCic.Appl l -> List.iter aux l + | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl + in + List.iter aux tl; + 1 + !h +;; + +let height_of_obj_kind uri = + function + NCic.Inductive _ + | NCic.Constant (_,_,None,_,_) + | NCic.Fixpoint (false,_,_) -> 0 + | NCic.Fixpoint (true,ifl,_) -> + let iflno = List.length ifl in + height_of_term + (List.fold_left + (fun l (_,_,_,ty,bo) -> + let bo = NCicTypeChecker.debruijn uri iflno [] bo in + ty::bo::l + ) [] ifl) + | NCic.Constant (_,_,Some bo,ty,_) -> height_of_term [bo;ty] +;; diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli index 1df92163d..9cde401b0 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.mli +++ b/helm/software/components/ng_kernel/nCicUntrusted.mli @@ -27,3 +27,5 @@ val mk_appl : NCic.term -> NCic.term list -> NCic.term (* the context is needed only to honour Barendregt's naming convention *) val apply_subst : NCic.substitution -> NCic.context -> NCic.term -> NCic.term val apply_subst_metasenv : NCic.substitution -> NCic.metasenv -> NCic.metasenv + +val height_of_obj_kind: NUri.uri -> NCic.obj_kind -> int diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml index be6760bf1..e209d05be 100644 --- a/helm/software/components/ng_kernel/nReference.ml +++ b/helm/software/components/ng_kernel/nReference.ml @@ -25,10 +25,15 @@ type reference = Ref of NUri.uri * spec let eq = (==);; +let compare (Ref (u1,s1)) (Ref (u2,s2)) = + let res = NUri.compare u1 u2 in + if res = 0 then compare s1 s2 else res +;; + module OrderedStrings = struct type t = string - let compare (s1 : t) (s2 : t) = compare s1 s2 + let compare (s1 : t) (s2 : t) = Pervasives.compare s1 s2 end ;; diff --git a/helm/software/components/ng_kernel/nReference.mli b/helm/software/components/ng_kernel/nReference.mli index d291b621b..d7f87e57c 100644 --- a/helm/software/components/ng_kernel/nReference.mli +++ b/helm/software/components/ng_kernel/nReference.mli @@ -26,6 +26,7 @@ type reference = private Ref of NUri.uri * spec val reference_of_spec: NUri.uri -> spec -> reference val eq: reference -> reference -> bool +val compare: reference -> reference -> int val string_of_reference: reference -> string val reference_of_string: string -> reference diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 2738b1c90..225269b70 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -16,10 +16,7 @@ module Ref = NReference let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);; let mk_type n = - if n = 0 then - [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")] - else - [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")] + [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")] ;; let mk_cprop n = @@ -871,3 +868,11 @@ let convert_term uri ctx t = aux false [] [] 0 uri t ;; *) + +let reference_of_oxuri u = + let t = CicUtil.term_of_uri u in + let t',l = convert_term (UriManager.uri_of_string "cic:/dummy/dummy.con") t in + match t',l with + NCic.Const nref, [] -> nref + | _,_ -> assert false +;; diff --git a/helm/software/components/ng_kernel/oCic2NCic.mli b/helm/software/components/ng_kernel/oCic2NCic.mli index ddb1baa3d..fa3717ee4 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.mli +++ b/helm/software/components/ng_kernel/oCic2NCic.mli @@ -15,6 +15,8 @@ val nuri_of_ouri: UriManager.uri -> NUri.uri val reference_of_ouri: UriManager.uri -> NReference.spec -> NReference.reference +val reference_of_oxuri: UriManager.uri -> NReference.reference + val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj list val convert_term: UriManager.uri -> Cic.term -> NCic.term * NCic.obj list diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml index 7dcd6417f..fba21753a 100644 --- a/helm/software/components/ng_tactics/nCicElim.ml +++ b/helm/software/components/ng_tactics/nCicElim.ml @@ -115,7 +115,7 @@ let mk_elims (uri,_,_,_,obj) = (BoxPp.render_to_string ~map_unicode_to_tex:false (function x::_ -> x | _ -> assert false) - 80 (CicNotationPres.render (Hashtbl.create 0) + 80 (CicNotationPres.render (fun _ -> None) (TermContentPres.pp_ast res))); [] | _ -> [] diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index f3c6a8bd1..25e67131f 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,2 +1,5 @@ +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/components/tactics/setoids.ml b/helm/software/components/tactics/setoids.ml index d85df1c4b..265ef99aa 100644 --- a/helm/software/components/tactics/setoids.ml +++ b/helm/software/components/tactics/setoids.ml @@ -958,7 +958,7 @@ let int_add_relation id a aeq refl sym trans = rel_X_relation_class = Cic.Sort Cic.Prop; (* dummy value, overwritten below *) rel_Xreflexive_relation_class = Cic.Sort Cic.Prop (* dummy value, overwritten below *) } in - let x_relation_class = + let _x_relation_class = let subst = let len = List.length a_quantifiers_rev in list_map_i (fun i _ -> Cic.Rel (len - i + 2)) 0 a_quantifiers_rev in @@ -979,7 +979,7 @@ let int_add_relation id a aeq refl sym trans = IsDefinition Definition) in *) () in let id_precise = id ^ "_precise_relation_class" in - let xreflexive_relation_class = + let _xreflexive_relation_class = let subst = let len = List.length a_quantifiers_rev in list_map_i (fun i _ -> Cic.Rel (len - i)) 0 a_quantifiers_rev diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml index dc58c831c..e2a05e1c7 100644 --- a/helm/software/components/tptp_grafite/tptp2grafite.ml +++ b/helm/software/components/tptp_grafite/tptp2grafite.ml @@ -349,8 +349,8 @@ let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filenam let width = max_int in let term_pp content_term = let pres_term = TermContentPres.pp_ast content_term in - let dummy_tbl = Hashtbl.create 1 in - let markup = CicNotationPres.render dummy_tbl pres_term in + let lookup_uri = fun _ -> None in + let markup = CicNotationPres.render ~lookup_uri pres_term in let s = BoxPp.render_to_string List.hd width markup ~map_unicode_to_tex:false in Pcre.substitute ~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s diff --git a/helm/software/components/urimanager/uriManager.ml b/helm/software/components/urimanager/uriManager.ml index 9107994a1..2d099a4e9 100644 --- a/helm/software/components/urimanager/uriManager.ml +++ b/helm/software/components/urimanager/uriManager.ml @@ -193,7 +193,6 @@ let bodyuri_of_uri (uri, _) = let ind_uri_split ((s, _) as uri) = let noxp = strip_xpointer uri in - let length = String.length s in try (let arg_index = String.rindex s '(' in try diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index d572a78d9..da4bccba0 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -66,9 +66,10 @@ let mml_of_cic_sequent metasenv sequent = (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts))) let nmml_of_cic_sequent metasenv subst sequent = - let content_sequent = NTermCicContent.nmap_sequent ~subst sequent in + let content_sequent,ids_to_refs = + NTermCicContent.nmap_sequent ~subst sequent in let pres_sequent = - Sequent2pres.nsequent2pres subst content_sequent in + Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in let xmlpres = mpres_document pres_sequent in Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres @@ -88,6 +89,11 @@ let mml_of_cic_object obj = (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses, ids_to_inner_sorts,ids_to_inner_types))) +let nmml_of_cic_object obj = + prerr_endline (NCicPp.ppobj obj); + assert false +;; + let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent = let unsh_sequent,(asequent,ids_to_terms, ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses) @@ -111,8 +117,10 @@ let txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type size let t, ids_to_uris = TermAcicContent.ast_of_acic ~output_type ids_to_inner_sorts t in let t = TermContentPres.pp_ast t in - let t = CicNotationPres.render ids_to_uris t in - BoxPp.render_to_string ~map_unicode_to_tex + let t = + CicNotationPres.render ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) t + in + BoxPp.render_to_string ~map_unicode_to_tex (function x::_ -> x | _ -> assert false) size t let txt_of_cic_term ~map_unicode_to_tex size metasenv context t = @@ -169,9 +177,10 @@ let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm = let ast, ids_to_uris = TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in let bobj = - CicNotationPres.box_of_mpres ( - CicNotationPres.render ~prec:90 ids_to_uris - (TermContentPres.pp_ast ast)) in + CicNotationPres.box_of_mpres ( + CicNotationPres.render ~prec:90 + ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) + (TermContentPres.pp_ast ast)) in let render = function _::x::_ -> x | _ -> assert false in let mpres = CicNotationPres.mpres_of_box bobj in let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index 1297be57f..f41f0a7a1 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -60,6 +60,8 @@ val mml_of_cic_object: (Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *) (Cic.id, Cic2acic.anntypes) Hashtbl.t)) (* ids_to_inner_types *) +val nmml_of_cic_object: NCic.obj -> Gdome.document + val txt_of_cic_term: map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term -> string diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 392a35ab7..9aa1fb2f1 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -81,8 +81,15 @@ let _ = let sequents_viewer = MatitaMathView.sequentsViewer_instance () in sequents_viewer#load_logo; cic_math_view#set_href_callback - (Some (fun uri -> (MatitaMathView.cicBrowser ())#load - (`Uri (UriManager.uri_of_string uri)))); + (Some (fun uri -> + let uri = + try + `Uri (UriManager.uri_of_string uri) + with + UriManager.IllFormedUri _ -> + `NRef (NReference.reference_of_string uri) + in + (MatitaMathView.cicBrowser ())#load uri)); let browser_observer _ _ = MatitaMathView.refresh_all_browsers () in let sequents_observer _ grafite_status = sequents_viewer#reset; diff --git a/helm/software/matita/matitaGuiTypes.mli b/helm/software/matita/matitaGuiTypes.mli index 51c700dc3..18515dac5 100644 --- a/helm/software/matita/matitaGuiTypes.mli +++ b/helm/software/matita/matitaGuiTypes.mli @@ -127,6 +127,7 @@ object method nload_sequent: NCic.metasenv -> NCic.substitution -> int -> unit method load_object: Cic.obj -> unit + method load_nobject: NCic.obj -> unit end class type sequentsViewer = diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 9c259a1cb..ade02fb80 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -629,6 +629,27 @@ object (self) end; self#load_root ~root:mathml#get_documentElement; current_mathml <- Some mathml); + + method load_nobject obj = + let mathml = ApplyTransformation.nmml_of_cic_object obj in +(* + self#set_cic_info + (Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj)); + (match current_mathml with + | Some current_mathml when use_diff -> + self#freeze; + XmlDiff.update_dom ~from:current_mathml mathml; + self#thaw + | _ -> +*) + if BuildTimeConf.debug then begin + let name = + "/tmp/cic_browser_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in + HLog.debug ("cic_browser: dumping MathML to ./" ^ name); + ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()) + end; + self#load_root ~root:mathml#get_documentElement; + (*current_mathml <- Some mathml*)(*)*); end let tab_label meta_markup = @@ -1064,7 +1085,14 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) handle_error (fun () -> self#loadInput (self#_getSelectedUri ())))); mathView#set_href_callback (Some (fun uri -> handle_error (fun () -> - self#load (`Uri (UriManager.uri_of_string uri))))); + let uri = + try + `Uri (UriManager.uri_of_string uri) + with + UriManager.IllFormedUri _ -> + `NRef (NReference.reference_of_string uri) + in + self#load uri))); gviz#connect_href (fun button_ev attrs -> let time = GdkEvent.Button.time button_ev in let uri = List.assoc "href" attrs in @@ -1214,6 +1242,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) -> self#dependencies dir uri () | `Uri uri -> self#_loadUriManagerUri uri + | `NRef nref -> self#_loadNReference nref | `Univs uri -> self#_loadUnivs uri | `Whelp (query, results) -> set_whelp_query query; @@ -1324,6 +1353,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in self#_loadObj obj + method private _loadNReference (NReference.Ref (uri,_)) = + let obj = NCicEnvironment.get_checked_obj uri in + self#_loadNObj obj + method private _loadUnivs uri = let uri = UriManager.strip_xpointer uri in let (_, u) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in @@ -1364,6 +1397,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_showMath; mathView#load_object obj + method private _loadNObj obj = + (* showMath must be done _before_ loading the document, since if the + * widget is not mapped (hidden by the notebook) the document is not + * rendered *) + self#_showMath; + mathView#load_nobject obj + method private _loadTermCic term metasenv = let context = self#script#proofContext in let dummyno = CicMkImplicit.new_meta metasenv [] in diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index fadc55105..b221919d2 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -346,8 +346,8 @@ let cic2grafite context menv t = let width = max_int in let term_pp content_term = let pres_term = TermContentPres.pp_ast content_term in - let dummy_tbl = Hashtbl.create 1 in - let markup = CicNotationPres.render dummy_tbl pres_term in + let lookup_uri = fun _ -> None in + let markup = CicNotationPres.render ~lookup_uri pres_term in let s = "(" ^ BoxPp.render_to_string ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") diff --git a/helm/software/matita/matitaTypes.ml b/helm/software/matita/matitaTypes.ml index adbc7d3b3..2584f61f6 100644 --- a/helm/software/matita/matitaTypes.ml +++ b/helm/software/matita/matitaTypes.ml @@ -49,6 +49,7 @@ type mathViewer_entry = | `HBugs of [ `Tutors ] (* list of available HBugs tutors *) | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ] | `Uri of UriManager.uri (* cic object uri *) + | `NRef of NReference.reference (* cic object uri *) | `Whelp of string * UriManager.uri list (* query and results *) | `Univs of UriManager.uri ] @@ -76,6 +77,7 @@ let string_of_entry = function String.sub suri 4 (len - 4) in (* strip "cic:" prefix *) (match dir with | `Fwd -> "forward" | `Back -> "backward") ^ suri) | `Uri uri -> UriManager.string_of_uri uri + | `NRef nref -> NReference.string_of_reference nref | `Whelp (query, _) -> query | `Univs uri -> "univs:" ^ UriManager.string_of_uri uri diff --git a/helm/software/matita/matitaTypes.mli b/helm/software/matita/matitaTypes.mli index 4dfb7c790..34e98cc1a 100644 --- a/helm/software/matita/matitaTypes.mli +++ b/helm/software/matita/matitaTypes.mli @@ -36,6 +36,7 @@ type mathViewer_entry = | `HBugs of [ `Tutors ] | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ] | `Uri of UriManager.uri + | `NRef of NReference.reference | `Whelp of string * UriManager.uri list | `Univs of UriManager.uri ] -- 2.39.2