else
(fun () -> 0)
-let choice_of_uri (uri: string) =
- let cic = HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri) in
- (uri, (fun _ _ _ -> cic))
+let choice_of_uri uri =
+ let term = CicUtil.term_of_uri uri in
+ (uri, (fun _ _ _ -> term))
let grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
[
b = binder;
(vars, typ) =
- [ vars = LIST1 IDENT;
+ [ vars = LIST1 IDENT SEP SYMBOL ",";
typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
- | PAREN "("; vars = LIST1 IDENT;
+ | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
];
- SYMBOL ","; body = term ->
+ SYMBOL "."; body = term ->
let binder =
List.fold_right
(fun var body ->
[ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
];
reduction_kind: [
- [ "reduce" -> `Reduce
- | "simpl" -> `Simpl
- | "whd" -> `Whd ]
+ [ [ IDENT "reduce" | IDENT "Reduce" ] -> `Reduce
+ | [ IDENT "simplify" | IDENT "Simplify" ] -> `Simpl
+ | [ IDENT "whd" | IDENT "Whd" ] -> `Whd ]
];
tactic: [
- [ [ IDENT "absurd" | IDENT "Absurd" ] -> return_tactic loc TacticAst.Absurd
- | [ IDENT "apply" | IDENT "Apply" ];
- t = tactic_term -> return_tactic loc (TacticAst.Apply t)
+ [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term ->
+ return_tactic loc (TacticAst.Absurd t)
+ | [ IDENT "apply" | IDENT "Apply" ]; t = tactic_term ->
+ return_tactic loc (TacticAst.Apply t)
| [ IDENT "assumption" | IDENT "Assumption" ] ->
return_tactic loc TacticAst.Assumption
+ | [ IDENT "auto" | IDENT "Auto" ] -> return_tactic loc TacticAst.Auto
| [ IDENT "change" | IDENT "Change" ];
t1 = tactic_term; "with"; t2 = tactic_term;
where = tactic_where ->
| [ IDENT "discriminate" | IDENT "Discriminate" ];
hyp = IDENT ->
return_tactic loc (TacticAst.Discriminate hyp)
- | [ IDENT "elim" | IDENT "Elim" ]; IDENT "type";
- t = tactic_term ->
+ | [ IDENT "elimType" | IDENT "ElimType" ]; t = tactic_term ->
return_tactic loc (TacticAst.ElimType t)
| [ IDENT "elim" | IDENT "Elim" ];
t1 = tactic_term;
return_tactic loc (TacticAst.Fold (kind, t))
| [ IDENT "fourier" | IDENT "Fourier" ] ->
return_tactic loc TacticAst.Fourier
+ | [ IDENT "hint" | IDENT "Hint" ] -> return_tactic loc TacticAst.Hint
| [ IDENT "injection" | IDENT "Injection" ]; ident = IDENT ->
return_tactic loc (TacticAst.Injection ident)
| [ IDENT "intros" | IDENT "Intros" ];
| [ "let" | "Let" ];
t = tactic_term; "in"; where = IDENT ->
return_tactic loc (TacticAst.LetIn (t, where))
- (* TODO Reduce *)
+ | kind = reduction_kind;
+ pat = OPT [
+ "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] ->
+ pat
+ ];
+ terms = LIST0 term SEP SYMBOL "," ->
+ let tac =
+ (match (pat, terms) with
+ | None, [] -> TacticAst.Reduce (kind, None)
+ | None, terms -> TacticAst.Reduce (kind, Some (terms, `Goal))
+ | Some pat, [] -> TacticAst.Reduce (kind, Some ([], pat))
+ | Some pat, terms -> TacticAst.Reduce (kind, Some (terms, pat)))
+ in
+ return_tactic loc tac
| [ IDENT "reflexivity" | IDENT "Reflexivity" ] ->
return_tactic loc TacticAst.Reflexivity
| [ IDENT "replace" | IDENT "Replace" ];
return_tactic loc (TacticAst.Transitivity t)
]
];
- tactical0: [ [ t = tactical; SYMBOL "." -> t ] ];
+ tactical0: [ [ t = tactical; SYMBOL ";;" -> return_tactical loc t ] ];
tactical:
[ "command" NONA
[ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
return_command loc (TacticAst.Undo (int_opt steps))
| [ IDENT "redo" | IDENT "Redo" ]; steps = OPT NUM ->
return_command loc (TacticAst.Redo (int_opt steps))
+ | [ IDENT "baseuri" | IDENT "Baseuri" ]; uri = OPT QSTRING ->
+ return_command loc (TacticAst.Baseuri uri)
+ | [ IDENT "check" | IDENT "Check" ]; t = term ->
+ return_command loc (TacticAst.Check t)
]
];
END