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 = OPT IDENT;
- idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
- let types = match types with None -> [] | Some types -> types in
+ | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
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)
+ GrafiteAst.Decompose (loc, idents)
| IDENT "demodulate" -> GrafiteAst.Demodulate loc
| IDENT "destruct"; t = tactic_term ->
GrafiteAst.Destruct (loc, t)
GrafiteAst.Reflexivity loc
| IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
GrafiteAst.Replace (loc, p, t)
- | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec ->
+ | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
+ xnames = OPT [ "as"; n = ident_list0 -> n ] ->
let (pt,_,_) = p in
if pt <> None then
raise
(CicNotationParser.Parse_error
"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
else
- GrafiteAst.Rewrite (loc, d, t, p)
+ let n = match xnames with None -> [] | Some names -> names in
+ GrafiteAst.Rewrite (loc, d, t, p, n)
| IDENT "right" ->
GrafiteAst.Right loc
| IDENT "ring" ->
[ [ IDENT "check" ]; t = term ->
GrafiteAst.Check (loc, t)
| [ IDENT "inline"];
- style = OPT [ IDENT "procedural" ];
+ style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
suri = QSTRING; prefix = OPT QSTRING ->
let style = match style with
- | None -> GrafiteAst.Declarative
- | Some _ -> GrafiteAst.Procedural
+ | None -> GrafiteAst.Declarative
+ | Some depth -> GrafiteAst.Procedural depth
in
let prefix = match prefix with None -> "" | Some prefix -> prefix in
GrafiteAst.Inline (loc,style,suri,prefix)
GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
| "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
defs = CicNotationParser.let_defs ->
+ (* 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
+ insertion in the environment. We use the flavour
+ `MutualDefinition to rememer this. *)
let name,ty =
match defs with
| (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
| _ -> assert false
in
let body = Ast.Ident (name,None) in
- GrafiteAst.Obj (loc, Ast.Theorem(`Definition, name, ty,
- Some (Ast.LetRec (ind_kind, defs, body))))
+ let flavour =
+ if List.length defs = 1 then
+ `Definition
+ else
+ `MutualDefinition
+ in
+ GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
+ Some (Ast.LetRec (ind_kind, defs, body))))
| IDENT "inductive"; spec = inductive_spec ->
let (params, ind_types) = spec in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
(loc,GrafiteAst.Include (iloc,buri))))
| scom = lexicon_command ; SYMBOL "." ->
fun ~include_paths status ->
- let status = LexiconEngine.eval_command status scom in
+ let status = LexiconEngine.eval_command status scom in
status,LNone loc
| EOI -> raise End_of_file
]