From: Enrico Tassi Date: Mon, 12 Dec 2011 20:14:53 +0000 (+0000) Subject: support -axiom to avoind indexing an axiom (since there is no qed) X-Git-Tag: make_still_working~2023 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f5b9e1d5511a13ca5bb424c149781087aa0c8e31;p=helm.git support -axiom to avoind indexing an axiom (since there is no qed) --- diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 2d55e8634..02e161780 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -99,7 +99,7 @@ type inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (* type command = | Include of loc * inclusion_mode * string (* _,buri,_,path *) | UnificationHint of loc * nterm * int (* term, precedence *) - | NObj of loc * nterm NotationPt.obj + | NObj of loc * nterm NotationPt.obj * bool | NDiscriminator of loc * nterm | NInverter of loc * string * nterm * bool list option * nterm option | NUnivConstraint of loc * NUri.uri * NUri.uri diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index c4eacfb5a..652f10b2a 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -168,8 +168,11 @@ let pp_ncommand status = function | NInverter (_,_,_,_,_) | NUnivConstraint (_) -> "not supported" | NCoercion (_) -> "not supported" - | NObj (_,obj) -> NotationPp.pp_obj (NotationPp.pp_term status) obj - | NQed (_) -> "qed" + | NObj (_,obj,index) -> + (if not index then "-" else "") ^ + NotationPp.pp_obj (NotationPp.pp_term status) obj + | NQed (_,true) -> "qed" + | NQed (_,false) -> "qed-" | NCopy (_,name,uri,map) -> "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ String.concat " and " diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index b1e0f4c85..c5e291959 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -587,7 +587,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = try let nstatus = eval_ncommand ~include_paths opts status - ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml)) + ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml,true)) in if nstatus#ng_mode <> `CommandMode then begin @@ -746,7 +746,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let status = subst_metasenv_and_fix_names status in let status = status#set_ng_mode `ProofMode in eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false)) - | GrafiteAst.NObj (loc,obj) -> + | GrafiteAst.NObj (loc,obj,index) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") else @@ -761,7 +761,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let status = status#set_ng_mode `ProofMode in (match nmenv with [] -> - eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,true)) + eval_ncommand ~include_paths opts status + ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,index)) | _ -> status) | GrafiteAst.NDiscriminator (loc, indty) -> if status#ng_mode <> `CommandMode then diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 1ac21965e..376c5c9cc 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -74,9 +74,9 @@ let mk_rec_corec ind_kind defs loc = let body = N.Ident (name,None) in (loc, N.Theorem(`Definition, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular)) -let nmk_rec_corec ind_kind defs loc = +let nmk_rec_corec ind_kind defs loc index = let loc,t = mk_rec_corec ind_kind defs loc in - G.NObj (loc,t) + G.NObj (loc,t,index) (* let nnon_punct_of_punct = function @@ -501,37 +501,39 @@ EXTEND loc,path,G.WithoutPreferences ]]; + index: [[ b = OPT SYMBOL "-" -> match b with None -> false | _ -> true ]]; + grafite_ncommand: [ [ - IDENT "qed" ; b = OPT SYMBOL "-" -> - let b = match b with None -> true | Some _ -> false in - G.NQed (loc,b) + IDENT "qed" ; i = index -> G.NQed (loc,i) | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular)) + G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular),true) | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); body = term -> - G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular)) - | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term -> - G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular)) + G.NObj (loc, + N.Theorem(nflavour, name, N.Implicit `JustOne, Some body,`Regular), + true) + | i = index; IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term -> + G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular),i) | IDENT "discriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty) | IDENT "inverter"; name = IDENT; IDENT "for" ; indty = tactic_term ; paramspec = OPT inverter_param_list ; outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> G.NInverter (loc,name,indty,paramspec,outsort) | LETCOREC ; defs = let_codefs -> - nmk_rec_corec `CoInductive defs loc + nmk_rec_corec `CoInductive defs loc true | LETREC ; defs = let_defs -> - nmk_rec_corec `Inductive defs loc + nmk_rec_corec `Inductive defs loc true | IDENT "inductive"; spec = inductive_spec -> let (params, ind_types) = spec in - G.NObj (loc, N.Inductive (params, ind_types)) + G.NObj (loc, N.Inductive (params, ind_types),true) | IDENT "coinductive"; 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 - G.NObj (loc, N.Inductive (params, ind_types)) + G.NObj (loc, N.Inductive (params, ind_types),true) | IDENT "universe"; IDENT "constraint"; u1 = tactic_term; SYMBOL <:unicode> ; u2 = tactic_term -> let urify = function @@ -553,7 +555,7 @@ EXTEND let compose = compose = None in G.NCoercion(loc,name,compose,spec) | IDENT "record" ; (params,name,ty,fields) = record_spec -> - G.NObj (loc, N.Record (params,name,ty,fields)) + G.NObj (loc, N.Record (params,name,ty,fields),true) | IDENT "copy" ; s = IDENT; IDENT "from"; u = URI; "with"; m = LIST0 [ u1 = URI; SYMBOL <:unicode>; u2 = URI -> u1,u2 ] -> G.NCopy (loc,s,NUri.uri_of_string u,