X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=9373e54b43a1de051f743a2581220677abaf4df8;hb=2499f5fdcf4dbfecc6f4fafe925b24ae76f14be8;hp=c0ce1c27d359097b676a436c05923127ffc53dda;hpb=679f6296c9a979213425104fa606809d9f1e3bad;p=helm.git diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index c0ce1c27d..9373e54b4 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -53,6 +53,12 @@ let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t) let default_precedence = 50 let default_associativity = Gramext.NonA +type by_continuation = + BYC_done + | BYC_weproved of CicNotationPt.term * string * CicNotationPt.term option + | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term + | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term + EXTEND GLOBAL: term statement; arg: [ @@ -68,8 +74,7 @@ EXTEND [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] ]; reduction_kind: [ - [ IDENT "demodulate" -> `Demodulate - | IDENT "normalize" -> `Normalize + [ IDENT "normalize" -> `Normalize | IDENT "reduce" -> `Reduce | IDENT "simplify" -> `Simpl | IDENT "unfold"; t = OPT tactic_term -> `Unfold t @@ -136,8 +141,8 @@ EXTEND LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int -> string_of_int v | v = IDENT -> v ] -> i,v ] -> GrafiteAst.Auto (loc,params) - | IDENT "clear"; id = IDENT -> - GrafiteAst.Clear (loc,id) + | IDENT "clear"; ids = LIST1 IDENT -> + GrafiteAst.Clear (loc, ids) | IDENT "clearbody"; id = IDENT -> GrafiteAst.ClearBody (loc,id) | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> @@ -148,11 +153,13 @@ EXTEND GrafiteAst.Contradiction loc | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] -> GrafiteAst.Cut (loc, ident, t) - | IDENT "decompose"; types = OPT ident_list0; what = IDENT; - (num, idents) = intros_spec -> + | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT; + idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] -> let types = match types with None -> [] | Some types -> types in + let idents = match idents with None -> [] | Some idents -> idents in let to_spec id = GrafiteAst.Ident id in GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents) + | IDENT "demodulate" -> GrafiteAst.Demodulate loc | IDENT "discriminate"; t = tactic_term -> GrafiteAst.Discriminate (loc, t) | IDENT "elim"; what = tactic_term; using = using; @@ -194,12 +201,14 @@ EXTEND | IDENT "inversion"; t = tactic_term -> GrafiteAst.Inversion (loc, t) | IDENT "lapply"; + linear = OPT [ IDENT "linear" ]; depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; what = tactic_term; to_what = OPT [ "to" ; t = tactic_term_list1 -> t ]; ident = OPT [ "as" ; ident = IDENT -> ident ] -> - let to_what = match to_what with None -> [] | Some to_what -> to_what in - GrafiteAst.LApply (loc, depth, to_what, what, ident) + let linear = match linear with None -> false | Some _ -> true in + let to_what = match to_what with None -> [] | Some to_what -> to_what in + GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) | IDENT "left" -> GrafiteAst.Left loc | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> GrafiteAst.LetIn (loc, t, where) @@ -224,12 +233,72 @@ EXTEND GrafiteAst.Ring loc | IDENT "split" -> GrafiteAst.Split loc + | IDENT "subst" -> + GrafiteAst.Subst loc | IDENT "symmetry" -> GrafiteAst.Symmetry loc | IDENT "transitivity"; t = tactic_term -> GrafiteAst.Transitivity (loc, t) + (* Produzioni Aggiunte *) + | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term -> + GrafiteAst.Assume (loc, id, t) + | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']-> + GrafiteAst.Suppose (loc, t, id, t1) + | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc]; + cont=by_continuation -> + let t' = match t with LNone _ -> None | LSome t -> Some t in + (match cont with + BYC_done -> GrafiteAst.Bydone (loc, t') + | BYC_weproved (ty,id,t1) -> + GrafiteAst.By_term_we_proved(loc, t', ty, id, t1) + | BYC_letsuchthat (id1,t1,id2,t2) -> + (match t with + LNone floc -> + raise (HExtlib.Localized + (floc,CicNotationParser.Parse_error + "tactic_term expected here")) + | LSome t -> GrafiteAst.ExistsElim (loc, t, id1, t1, id2, t2)) + | BYC_wehaveand (id1,t1,id2,t2) -> + (match t with + LNone floc -> + raise (HExtlib.Localized + (floc,CicNotationParser.Parse_error + "tactic_term expected here")) + | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2))) + | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']-> + GrafiteAst.We_need_to_prove (loc, t, id, t1) + | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> + GrafiteAst.We_proceed_by_induction_on (loc, t, t1) + | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN -> + GrafiteAst.Byinduction(loc, t, id) + | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term -> + GrafiteAst.Thesisbecomes(loc, t) + | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ; + SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] -> + GrafiteAst.Case(loc,id,params) + | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation -> + GrafiteAst.RewritingStep(loc, Some termine, t1, t2, cont) + | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation -> + GrafiteAst.RewritingStep(loc, None, t1, t2, cont) + ] +]; + by_continuation: [ + [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,id,t1) + | IDENT "done" -> BYC_done + | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ; + IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; + RPAREN -> BYC_letsuchthat (id1,t1,id2,t2) + | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ; + "and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN -> + BYC_wehaveand (id1,t1,id2,t2) ] - ]; +]; + rewriting_step_continuation : [ + [ IDENT "done" -> None + | IDENT "we" ; IDENT "proved" ; id=IDENT -> Some (Cic.Name id) + | -> Some Cic.Anonymous + ] +]; atomic_tactical: [ "sequence" LEFTA [ t1 = SELF; SYMBOL ";"; t2 = SELF -> @@ -258,6 +327,7 @@ EXTEND | IDENT "solve"; SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"-> GrafiteAst.Solve (loc, tacs) + | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac) | LPAREN; tac = SELF; RPAREN -> tac | tac = tactic -> GrafiteAst.Tactic (loc, tac) ] @@ -316,8 +386,14 @@ EXTEND SYMBOL ":"; typ = term; SYMBOL <:unicode>; SYMBOL "{" ; fields = LIST0 [ name = IDENT ; - coercion = [ SYMBOL ":" -> false | SYMBOL ":"; SYMBOL ">" -> true ] ; - ty = term -> (name,ty,coercion) + coercion = [ + SYMBOL ":" -> false,0 + | SYMBOL ":"; SYMBOL ">" -> true,0 + | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity + ]; + ty = term -> + let b,n = coercion in + (name,ty,b,n) ] SEP SYMBOL ";"; SYMBOL "}" -> let params = List.fold_right @@ -329,13 +405,7 @@ EXTEND ] ]; macro: [ - [ [ IDENT "quit" ] -> GrafiteAst.Quit loc -(* | [ IDENT "abort" ] -> GrafiteAst.Abort loc *) -(* | [ IDENT "undo" ]; steps = OPT NUMBER -> - GrafiteAst.Undo (loc, int_opt steps) - | [ IDENT "redo" ]; steps = OPT NUMBER -> - GrafiteAst.Redo (loc, int_opt steps) *) - | [ IDENT "check" ]; t = term -> + [ [ IDENT "check" ]; t = term -> GrafiteAst.Check (loc, t) | [ IDENT "hint" ] -> GrafiteAst.Hint loc | [ IDENT "whelp"; "match" ] ; t = term -> @@ -348,7 +418,6 @@ EXTEND GrafiteAst.WElim (loc, t) | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> GrafiteAst.WHint (loc,t) - | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name) ] ]; alias_spec: [ @@ -460,6 +529,7 @@ EXTEND IDENT "set"; n = QSTRING; v = QSTRING -> GrafiteAst.Set (loc, n, v) | IDENT "drop" -> GrafiteAst.Drop loc + | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s) | IDENT "qed" -> GrafiteAst.Qed loc | IDENT "variant" ; name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode> ; newname = IDENT -> @@ -497,8 +567,9 @@ EXTEND ind_types in GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) - | IDENT "coercion" ; suri = URI -> - GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true) + | IDENT "coercion" ; suri = URI ; arity = OPT int -> + let arity = match arity with None -> 0 | Some x -> x in + GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity) | IDENT "record" ; (params,name,ty,fields) = record_spec -> GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields)) | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> @@ -536,15 +607,18 @@ EXTEND fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com)) | (iloc,fname,mode) = include_command ; SYMBOL "." -> fun ~include_paths status -> - let path = DependenciesParser.baseuri_of_script ~include_paths fname in + let buri, fullpath = + DependenciesParser.baseuri_of_script ~include_paths fname + in let status = - LexiconEngine.eval_command status (LexiconAst.Include (iloc,path,mode)) + LexiconEngine.eval_command status + (LexiconAst.Include (iloc,buri,mode,fullpath)) in status, LSome (GrafiteAst.Executable (loc,GrafiteAst.Command - (loc,GrafiteAst.Include (iloc,path)))) + (loc,GrafiteAst.Include (iloc,buri)))) | scom = lexicon_command ; SYMBOL "." -> fun ~include_paths status -> let status = LexiconEngine.eval_command status scom in