X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=024d321b4b359ab54f0859c6e5254f6481960ee0;hb=8a74607bfb8c49e529c4b55a8cad92dd0c68012f;hp=5f1b212bc160ed8b1ea034e725d5bf8e12167e32;hpb=a64572b00ce40f476577bf827488d23ddf763120;p=helm.git diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 5f1b212bc..024d321b4 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -32,13 +32,13 @@ let exc_located_wrapper f = try f () with - | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file - | Stdpp.Exc_located (floc, Stream.Error msg) -> + | Ploc.Exc (_, End_of_file) -> raise End_of_file + | Ploc.Exc (floc, Stream.Error msg) -> raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg)) - | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) -> + | Ploc.Exc (floc, HExtlib.Localized(_,exn)) -> raise (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn))) - | Stdpp.Exc_located (floc, exn) -> + | Ploc.Exc (floc, exn) -> raise (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn))) @@ -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 @@ -95,6 +95,7 @@ let mk_parser statement lstatus = (* let grammar = CicNotationParser.level2_ast_grammar lstatus in *) let term = CicNotationParser.term lstatus in let let_defs = CicNotationParser.let_defs lstatus in + let let_codefs = CicNotationParser.let_codefs lstatus in let protected_binder_vars = CicNotationParser.protected_binder_vars lstatus in (* {{{ parser initialization *) EXTEND @@ -128,7 +129,7 @@ EXTEND ]; pattern_spec: [ [ res = OPT [ - SYMBOL "{"; + "in" ; wanted_and_sps = [ "match" ; wanted = tactic_term ; sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] -> @@ -136,7 +137,7 @@ EXTEND | sps = sequent_pattern_spec -> None,Some sps ]; - SYMBOL "}" -> + SYMBOL ";" -> let wanted,hyp_paths,goal_path = match wanted_and_sps with wanted,None -> wanted, [], Some N.UserInput @@ -202,7 +203,7 @@ EXTEND G.NMacro(loc,G.Screenshot (loc, fname)) | IDENT "cases"; what = tactic_term ; where = pattern_spec -> G.NTactic(loc,[G.NCases (loc, what, where)]) - | IDENT "change"; what = pattern_spec; "with"; with_what = tactic_term -> + | IDENT "change"; "with"; with_what = tactic_term; what = pattern_spec -> G.NTactic(loc,[G.NChange (loc, what, with_what)]) | SYMBOL "-"; id = IDENT -> G.NTactic(loc,[G.NClear (loc, [id])]) @@ -252,6 +253,7 @@ EXTEND | IDENT "paramod" | IDENT "width" | IDENT "size" + | IDENT "nohyps" ] ]; auto_params: [ @@ -500,37 +502,39 @@ EXTEND loc,path,G.WithoutPreferences ]]; + index: [[ b = OPT SYMBOL "-" -> match b with None -> true | _ -> false ]]; + 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) + | IDENT "axiom"; i = index; 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_defs -> - nmk_rec_corec `CoInductive defs loc + | LETCOREC ; defs = let_codefs -> + 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 @@ -545,14 +549,14 @@ EXTEND G.UnificationHint (loc, t, n) | IDENT "coercion"; name = IDENT; compose = OPT [ IDENT "nocomposites" -> () ]; - SYMBOL ":"; ty = term; + spec = OPT [ SYMBOL ":"; ty = term; SYMBOL <:unicode>; t = term; "on"; id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term; - "to"; target = term -> + "to"; target = term -> t,ty,(id,source),target ] -> let compose = compose = None in - G.NCoercion(loc,name,compose,t,ty,(id,source),target) + 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,