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
let return_tactical loc tactical = TacticAst.LocatedTactical (loc, tactical)
let return_command loc cmd = cmd
-let fail (x, y) msg =
+let fail floc msg =
+ let (x, y) = CicAst.loc_of_floc floc in
failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
let name_of_string = function
| "_" -> Cic.Anonymous
| s -> Cic.Name s
+let int_opt = function
+ | None -> None
+ | Some lexeme -> Some (int_of_string lexeme)
+
EXTEND
GLOBAL: term term0 tactic tactical tactical0 command;
int: [
try
int_of_string num
with Failure _ ->
- let (x, y) = loc in
+ let (x, y) = CicAst.loc_of_floc loc in
raise (Parse_error (sprintf
"integer literal expected at characters %d-%d" x y))
]
]
];
substituted_name: [ (* a subs.name is an explicit substitution subject *)
- [ s = [ IDENT | SYMBOL ];
+ [ s = IDENT;
subst = OPT [
- SYMBOL "\subst"; (* to avoid catching frequent "a [1]" cases *)
+ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *)
PAREN "[";
substs = LIST1 [
i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
term0: [ [ t = term; EOI -> return_term loc t ] ];
term:
[ "letin" NONA
- (* actually "in" and "and" are _not_ keywords. Parsing works anyway
- * since applications are required to be bound by parens *)
[ "let"; var = typed_name;
SYMBOL "="; (* SYMBOL <:unicode<def>> (* ≝ *); *)
- t1 = term;
- IDENT "in"; t2 = term ->
+ t1 = term; "in"; t2 = term ->
return_term loc (CicAst.LetIn (var, t1, t2))
| "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
defs = LIST1 [
SYMBOL "="; (* SYMBOL <:unicode<def>> (* ≝ *); *)
t1 = term ->
(var, t1, (match index with None -> 0 | Some i -> i))
- ] SEP (IDENT "and");
- IDENT "in"; body = term ->
+ ] SEP "and";
+ "in"; body = term ->
return_term loc (CicAst.LetRec (ind_kind, defs, body))
]
| "binder" RIGHTA
| "mult" LEFTA [ (* nothing here by default *) ]
| "power" LEFTA [ (* nothing here by default *) ]
| "inv" NONA [ (* nothing here by default *) ]
+ | "apply" LEFTA
+ [ t1 = term; t2 = term ->
+ let rec aux = function
+ | CicAst.Appl (hd :: tl) -> aux hd @ tl
+ | term -> [term]
+ in
+ CicAst.Appl (aux t1 @ [t2])
+ ]
| "simple" NONA
[ sort = sort -> CicAst.Sort sort
| n = substituted_name -> return_term loc n
- | PAREN "("; head = term; args = LIST1 term; PAREN ")" ->
- return_term loc (CicAst.Appl (head :: args))
| i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ())))
| IMPLICIT -> return_term loc CicAst.Implicit
| m = META;
]
];
tactic_where: [
- [ where = OPT [ IDENT "in"; ident = IDENT -> ident ] -> where ]
+ [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ]
];
tactic_term: [ [ t = term -> t ] ];
ident_list0: [
| "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 "change" | IDENT "Change" ];
| [ 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" ];
idents = OPT ident_list0 ->
let idents = match idents with None -> [] | Some idents -> idents in
return_tactic loc (TacticAst.Intros (num, idents))
+ | [ IDENT "intro" | IDENT "Intro" ] ->
+ return_tactic loc (TacticAst.Intros (Some 1, []))
| [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left
| [ "let" | "Let" ];
- t = tactic_term; IDENT "in"; where = IDENT ->
+ t = tactic_term; "in"; where = IDENT ->
return_tactic loc (TacticAst.LetIn (t, where))
(* TODO Reduce *)
| [ IDENT "reflexivity" | IDENT "Reflexivity" ] ->
return_tactic loc (TacticAst.Transitivity t)
]
];
- tactical0: [ [ t = tactical; SYMBOL "." -> t ] ];
+ tactical0: [ [ t = tactical; SYMBOL ";;" -> t ] ];
tactical:
- [ "sequence" LEFTA
+ [ "command" NONA
+ [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
+ | "sequence" LEFTA
[ tactics = LIST1 NEXT SEP SYMBOL ";" ->
return_tactical loc (TacticAst.Seq tactics)
]
| [ IDENT "id" | IDENT "Id" ] -> return_tactical loc TacticAst.IdTac
| PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
| tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
- | cmd = command -> return_tactical loc (TacticAst.Command cmd)
]
];
theorem_flavour: [ (* all flavours but Goal *)
]
];
command: [
- [ [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
+ [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort
+ | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
| [ IDENT "quit" | IDENT "Quit" ] -> return_command loc TacticAst.Quit
| [ IDENT "qed" | IDENT "Qed" ] ->
return_command loc (TacticAst.Qed None)
| [ IDENT "goal" | IDENT "Goal" ]; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
return_command loc (TacticAst.Theorem (`Goal, None, typ, body))
+ | [ IDENT "undo" | IDENT "Undo" ]; steps = OPT NUM ->
+ return_command loc (TacticAst.Undo (int_opt steps))
+ | [ IDENT "redo" | IDENT "Redo" ]; steps = OPT NUM ->
+ return_command loc (TacticAst.Redo (int_opt steps))
+ | [ IDENT "check" | IDENT "Check" ]; t = term ->
+ return_command loc (TacticAst.Check t)
]
];
END
let exc_located_wrapper f =
try
Lazy.force f
- with Stdpp.Exc_located ((x, y), exn) ->
+ with Stdpp.Exc_located (floc, exn) ->
+ let (x, y) = CicAst.loc_of_floc floc in
raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
(Printexc.to_string exn)))
else
try
Grammar.Entry.parse aliases (Stream.of_string s)
- with Stdpp.Exc_located ((x, y), exn) ->
+ with Stdpp.Exc_located (floc, exn) ->
+ let (x, y) = CicAst.loc_of_floc floc in
raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
(Printexc.to_string exn)))
end
projects / helm.git / blobdiff