From e085135177f7b3b74b410d47a4f3bca1784b60b1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 24 Apr 2009 20:47:36 +0000 Subject: [PATCH] - Grammar for all obj commands ported to NG (let recs and inductives still need implementation and raise assert false) - New feature: every object can be both interactive or not, depending on the number of metavariables in the metasenv after disambiguation - New objects are now put in the same namespace as old ones. The creation of aliases takes care of this by looking for new objects before looking for old ones. Note: this way the check is done twice, also when mapping aliases to terms. However, this is temporary code while the two "libraries" coexist. --- .../content_pres/cicNotationLexer.ml | 4 ++ .../grafite_engine/grafiteEngine.ml | 55 ++++++++----------- .../grafite_parser/grafiteDisambiguate.ml | 50 ++++++++++++++++- .../grafite_parser/grafiteDisambiguate.mli | 5 ++ .../grafite_parser/grafiteParser.ml | 34 ++++++++++-- helm/software/matita/tests/ng_commands.ma | 49 +++++++++++++++++ 6 files changed, 159 insertions(+), 38 deletions(-) create mode 100644 helm/software/matita/tests/ng_commands.ma diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml index ac3b11422..b13c7887f 100644 --- a/helm/software/components/content_pres/cicNotationLexer.ml +++ b/helm/software/components/content_pres/cicNotationLexer.ml @@ -52,6 +52,8 @@ let regexp we_proved = "we" utf8_blank+ "proved" let regexp we_have = "we" utf8_blank+ "have" let regexp let_rec = "let" utf8_blank+ "rec" let regexp let_corec = "let" utf8_blank+ "corec" +let regexp nlet_rec = "nlet" utf8_blank+ "rec" +let regexp nlet_corec = "nlet" utf8_blank+ "corec" let regexp ident_decoration = '\'' | '?' | '`' let regexp ident_cont = ident_letter | xml_digit | '_' let regexp ident = ident_letter ident_cont* ident_decoration* @@ -284,6 +286,8 @@ and level2_ast_token = lexer | let_rec -> return lexbuf ("LETREC","") | let_corec -> return lexbuf ("LETCOREC","") + | nlet_rec -> return lexbuf ("NLETREC","") + | nlet_corec -> return lexbuf ("NLETCOREC","") | we_proved -> return lexbuf ("WEPROVED","") | we_have -> return lexbuf ("WEHAVE","") | utf8_blank+ -> ligatures_token level2_ast_token lexbuf diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 26e3aab2d..ebba1988d 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -753,7 +753,6 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status else let obj = prerr_endline "CSC: here we should fix the height!!!"; -prerr_endline (NUri.string_of_uri uri); uri,height,[],[],NTacStatus.apply_subst_obj subst obj in NCicLibrary.add_obj uri obj; @@ -767,38 +766,32 @@ prerr_endline (NUri.string_of_uri uri); | GrafiteAst.Set (loc, name, value) -> status, [] (* GrafiteTypes.set_option status name value,[] *) | GrafiteAst.NObj (loc,obj) -> - let ty, name = - match obj with - | CicNotationPt.Theorem (_,name,ty,_) -> ty, name - | _ -> assert false - in - (* CSC: ".con"??? it is like that for now *) - let suri = "cic:/ng_matita/" ^ name ^ ".con" in - let nlexicon_status = + let lexicon_status = match status.GrafiteTypes.ng_status with | GrafiteTypes.ProofMode _ -> assert false - | GrafiteTypes.CommandMode ls -> ls - in - let nmenv, nsubst, nlexicon_status, nty = - GrafiteDisambiguate.disambiguate_nterm None - nlexicon_status [] [] [] (text,prefix_len,ty) - in - let nmenv, nsubst, nlexicon_status, nbo = - GrafiteDisambiguate.disambiguate_nterm (Some nty) - nlexicon_status [] nmenv nsubst ("",0,CicNotationPt.Implicit) - in - let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in - prerr_endline ("nuovo lemma: " ^ NCicPp.ppmetasenv ~subst:nsubst nmenv); - { status with - GrafiteTypes.ng_status = - GrafiteTypes.ProofMode { NTacStatus.gstatus = ninitial_stack; - istatus = { - NTacStatus.pstatus = - NUri.uri_of_string suri, 0, nmenv, nsubst, - (NCic.Constant ([],"",Some nbo,nty,(`Provided,`Definition,`Regular))); - lstatus = nlexicon_status} } - }, - [] + | GrafiteTypes.CommandMode ls -> ls in + let lexicon_status,obj = + GrafiteDisambiguate.disambiguate_nobj lexicon_status + ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in + let uri,height,nmenv,nsubst,nobj = obj in + (match nmenv with + [] -> + (* CSC: cut&paste code from NQed *) + let obj = +prerr_endline "CSC: here we should fix the height!!!"; + uri,height,[],[],NTacStatus.apply_subst_obj nsubst nobj + in + NCicLibrary.add_obj uri obj; + {status with + GrafiteTypes.ng_status=GrafiteTypes.CommandMode lexicon_status },[] + | _ -> + let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in + { status with + GrafiteTypes.ng_status = + GrafiteTypes.ProofMode + { NTacStatus.gstatus = ninitial_stack; + istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}} + },[]) | GrafiteAst.Obj (loc,obj) -> let ext,name = match obj with diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 4ea3a95b3..b5c08fba6 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -89,15 +89,32 @@ let ncic_mk_choice = function | LexiconAst.Ident_alias (name, uri) -> uri, `Sym_interp (fun l->assert(l = []); - if String.sub uri 5 9 = "ng_matita" then - let nuri = + 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)) + 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))) +(* +*) ;; @@ -740,7 +757,36 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = | exn -> (* try_new None; *) raise exn +;; +let disambiguate_nobj lexicon_status ?baseuri (text,prefix_len,obj) = + let uri = + let baseuri = + match baseuri with Some x -> x | None -> raise BaseUriNotSetYet + in + let name = + match obj with + | CicNotationPt.Inductive (_,(name,_,_,_)::_) + | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind" + | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con" + | CicNotationPt.Inductive _ -> assert false + in + UriManager.uri_of_string (baseuri ^ "/" ^ name) + in + let diff, _, _, cic = + singleton "third" + (NCicDisambiguate.disambiguate_obj + ~lookup_in_library + ~description_of_alias:LexiconAst.description_of_alias + ~mk_choice:ncic_mk_choice + ~mk_implicit + ~uri:(OCic2NCic.nuri_of_ouri uri) + ~coercion_db:(NCicCoercion.db ()) + ~aliases:lexicon_status.LexiconEngine.aliases + ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) + (text,prefix_len,obj)) in + let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in + lexicon_status, cic ;; let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)= diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli index b8814d4d8..f13fc418c 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli @@ -61,6 +61,11 @@ val disambiguate_nterm : CicNotationPt.term Disambiguate.disambiguator_input -> NCic.metasenv * NCic.substitution * LexiconEngine.status * NCic.term +val disambiguate_nobj : + LexiconEngine.status -> ?baseuri:string -> + (CicNotationPt.term CicNotationPt.obj) Disambiguate.disambiguator_input -> + LexiconEngine.status * NCic.obj + type pattern = CicNotationPt.term Disambiguate.disambiguator_input option * (string * NCic.term) list * NCic.term option diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index be6dab1a6..389e2eb21 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -67,7 +67,7 @@ let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t) let default_associativity = Gramext.NonA -let mk_rec_corec ind_kind defs loc = +let mk_rec_corec ng ind_kind defs loc = (* In case of mutual definitions here we produce just the syntax tree for the first one. The others will be generated from the completely specified term just before @@ -93,7 +93,11 @@ let mk_rec_corec ind_kind defs loc = else `MutualDefinition in - GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty, + if ng then + GrafiteAst.NObj (loc, Ast.Theorem(flavour, name, ty, + Some (Ast.LetRec (ind_kind, defs, body)))) + else + GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty, Some (Ast.LetRec (ind_kind, defs, body)))) type by_continuation = @@ -515,7 +519,11 @@ EXTEND ] ]; ntheorem_flavour: [ - [ [ IDENT "ntheorem" ] -> `Theorem + [ [ IDENT "ndefinition" ] -> `Definition + | [ IDENT "nfact" ] -> `Fact + | [ IDENT "nlemma" ] -> `Lemma + | [ IDENT "nremark" ] -> `Remark + | [ IDENT "ntheorem" ] -> `Theorem ] ]; theorem_flavour: [ @@ -735,13 +743,22 @@ EXTEND Ast.Theorem (flavour, name, Ast.Implicit, Some body)) | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term -> GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None)) + | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term -> + GrafiteAst.NObj (loc, Ast.Theorem (`Axiom, name, typ, None)) | LETCOREC ; defs = let_defs -> - mk_rec_corec `CoInductive defs loc + mk_rec_corec false `CoInductive defs loc | LETREC ; defs = let_defs -> - mk_rec_corec `Inductive defs loc + mk_rec_corec false `Inductive defs loc + | NLETCOREC ; defs = let_defs -> + mk_rec_corec true `CoInductive defs loc + | NLETREC ; defs = let_defs -> + mk_rec_corec true `Inductive defs loc | IDENT "inductive"; spec = inductive_spec -> let (params, ind_types) = spec in GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) + | IDENT "ninductive"; spec = inductive_spec -> + let (params, ind_types) = spec in + GrafiteAst.NObj (loc, Ast.Inductive (params, ind_types)) | IDENT "coinductive"; spec = inductive_spec -> let (params, ind_types) = spec in let ind_types = (* set inductive flags to false (coinductive) *) @@ -749,6 +766,13 @@ EXTEND ind_types in GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) + | IDENT "ncoinductive"; spec = inductive_spec -> + let (params, ind_types) = spec in + let ind_types = (* set inductive flags to false (coinductive) *) + List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) + ind_types + in + GrafiteAst.NObj (loc, Ast.Inductive (params, ind_types)) | IDENT "coercion" ; t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ; arity = OPT int ; saturations = OPT int; diff --git a/helm/software/matita/tests/ng_commands.ma b/helm/software/matita/tests/ng_commands.ma new file mode 100644 index 000000000..dfe92269e --- /dev/null +++ b/helm/software/matita/tests/ng_commands.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "nat/plus.ma". + +ndefinition thesis0: ∀A:Type.Type ≝ λA. A → A. + +alias id "thesis0" = "cic:/matita/tests/ng_commands/thesis0.con". + +ndefinition thesis: ∀A:Type.Type ≝ λA. ?. + napply (A → A); +nqed. + +alias id "thesis" = "cic:/matita/tests/ng_commands/thesis.con". + +ntheorem foo: ∀A:Type.thesis A.#A;#x;napply x; +nqed. + +alias id "foo" = "cic:/matita/tests/ng_commands/foo.con". + +ntheorem goo: ∀A:Type.A → A. #A; napply (foo ?); +nqed. + +naxiom P: Prop. + +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]. + +ninductive nnat: Type ≝ + nO: nnat + | nS: nnat → nnat. *) \ No newline at end of file -- 2.39.2