let to_spec id = GrafiteAst.Ident id in
GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
| IDENT "demodulate" -> GrafiteAst.Demodulate loc
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 "destruct"; t = tactic_term ->
+ GrafiteAst.Destruct (loc, t)
| IDENT "elim"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
GrafiteAst.Elim (loc, what, using, num, idents)
| IDENT "elim"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
GrafiteAst.Elim (loc, what, using, num, idents)
| IDENT "intro"; ident = OPT IDENT ->
let idents = match ident with None -> [] | Some id -> [id] in
GrafiteAst.Intros (loc, Some 1, idents)
| IDENT "intro"; ident = OPT IDENT ->
let idents = match ident with None -> [] | Some id -> [id] in
GrafiteAst.Intros (loc, Some 1, idents)
(* Produzioni Aggiunte *)
| IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
GrafiteAst.Assume (loc, id, t)
(* Produzioni Aggiunte *)
| IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
GrafiteAst.Assume (loc, id, t)
GrafiteAst.Suppose (loc, t, id, t1)
| IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
cont=by_continuation ->
GrafiteAst.Suppose (loc, t, id, t1)
| IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
cont=by_continuation ->
| IDENT "solve";
SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
GrafiteAst.Solve (loc, tacs)
| IDENT "solve";
SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
GrafiteAst.Solve (loc, tacs)
| LPAREN; tac = SELF; RPAREN -> tac
| tac = tactic -> GrafiteAst.Tactic (loc, tac)
]
| LPAREN; tac = SELF; RPAREN -> tac
| tac = tactic -> GrafiteAst.Tactic (loc, tac)
]
- 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)
- | 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 ->
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->