tactical:
[ "sequence" LEFTA
[ tacticals = LIST1 NEXT SEP SYMBOL ";" ->
- TacticAst.Seq (loc, tacticals)
+ match tacticals with
+ [] -> assert false
+ | [tac] -> tac
+ | l -> TacticAst.Seq (loc, l)
]
| "then" NONA
- [ tac = tactical;
+ [ tac = tactical; SYMBOL ";";
PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" ->
(TacticAst.Then (loc, tac, tacs))
]
| "loops" RIGHTA
- [ [ IDENT "do" ]; count = int; tac = tactical ->
+ [ IDENT "do"; count = int; tac = tactical ->
TacticAst.Do (loc, count, tac)
- | [ IDENT "repeat" ]; tac = tactical ->
+ | IDENT "repeat"; tac = tactical ->
TacticAst.Repeat (loc, tac)
]
| "simple" NONA
- [ IDENT "tries";
- PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
- TacticAst.Tries (loc, tacs)
+ [ IDENT "first";
+ PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" ->
+ TacticAst.First (loc, tacs)
| IDENT "try"; tac = NEXT ->
TacticAst.Try (loc, tac)
+ | IDENT "solve";
+ PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" ->
+ TacticAst.Solve (loc, tacs)
| PAREN "("; tac = tactical; PAREN ")" -> tac
| tac = tactic -> TacticAst.Tactic (loc, tac)
]
let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
let rex = Str.regexp ("^"^ident^"$") in
if Str.string_match rex id 0 then
- let rex = Str.regexp
- ("^\\(cic:/\\|theory:/\\)"^ident^
- "\\(/"^ident^"+\\)*\\(\\."^ident^"\\)+"^
- "\\(#xpointer("^ num^"\\(/"^num^"\\)+)\\)?$")
- in
- if Str.string_match rex uri 0 then
+ if (try ignore (UriManager.uri_of_string uri); true
+ with UriManager.IllFormedUri _ -> false)
+ then
TacticAst.Ident_alias (id, uri)
else
raise (Parse_error (loc,sprintf "Not a valid uri: %s" uri))