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*
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
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;
| 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
| 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)))
+(*
+*)
;;
| 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)=
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
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
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 =
]
];
ntheorem_flavour: [
- [ [ IDENT "ntheorem" ] -> `Theorem
+ [ [ IDENT "ndefinition" ] -> `Definition
+ | [ IDENT "nfact" ] -> `Fact
+ | [ IDENT "nlemma" ] -> `Lemma
+ | [ IDENT "nremark" ] -> `Remark
+ | [ IDENT "ntheorem" ] -> `Theorem
]
];
theorem_flavour: [
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) *)
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;
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
projects / helm.git / commitdiff