max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/lean/parser/parser_t): rename module and type to parsec to avoid nested use of parser

Browse source
This commit is contained in:
Sebastian Ullrich 2018-07-11 18:53:40 +02:00
parent e57117a9b3
commit 72b255d4e1
15 changed files with 123 additions and 123 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/lean/ir/lirc.lean
View file

@ -15,9 +15,9 @@ We use it for testing.
namespace lean
namespace ir
open lean.parser
open lean.parser.monad_parser
open lean.parser.monad_parsec
def parse_input_aux : nat → list decl → fnid2string → parser (list decl × fnid2string)
def parse_input_aux : nat → list decl → fnid2string → parsec (list decl × fnid2string)
| 0 ds m := return (ds.reverse, m)
| (n+1) ds m :=
(eoi >> return (ds.reverse, m))
@ -29,7 +29,7 @@ def parse_input_aux : nat → list decl → fnid2string → parser (list decl ×
| none := parse_input_aux n (d::ds) m)
def parse_input (s : string) : except format (list decl × fnid2string) :=
match parser.parse (whitespace >> parse_input_aux s.length [] mk_fnid2string) s with
match parsec.parse (whitespace >> parse_input_aux s.length [] mk_fnid2string) s with
| except.ok r := return r
| except.error m := throw (m.to_string s)

58
library/init/lean/ir/parser.lean
View file

@ -4,22 +4,22 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.lean.ir.ir init.lean.parser.parser_t
import init.lean.ir.ir init.lean.parser.parsec
import init.lean.parser.identifier init.lean.parser.string_literal
import init.lean.ir.reserved
namespace lean
namespace ir
open lean.parser
open lean.parser.monad_parser
open lean.parser.monad_parsec
def symbol (s : string) : parser unit :=
def symbol (s : string) : parsec unit :=
(str s >> whitespace) <?> ("'" ++ s ++ "'")
def keyword (s : string) : parser unit :=
def keyword (s : string) : parsec unit :=
(try $ str s >> not_followed_by_sat is_id_rest >> whitespace) <?> ("'" ++ s ++ "'")
def parse_type : parser type :=
def parse_type : parsec type :=
(keyword "bool" >> return type.bool)
<|> (keyword "byte" >> return type.byte)
<|> (keyword "uint16" >> return type.uint16)
@ -33,7 +33,7 @@ def parse_type : parser type :=
<|> (keyword "double" >> return type.double)
<|> (keyword "object" >> return type.object)
def parse_assign_unop : parser assign_unop :=
def parse_assign_unop : parsec assign_unop :=
(keyword "not" >> return assign_unop.not)
<|> (keyword "neg" >> return assign_unop.neg)
<|> (keyword "ineg" >> return assign_unop.ineg)
@ -53,7 +53,7 @@ def parse_assign_unop : parser assign_unop :=
<|> (keyword "tag" >> return assign_unop.tag)
<|> (keyword "tag_ref" >> return assign_unop.tag_ref)
def parse_assign_binop : parser assign_binop :=
def parse_assign_binop : parsec assign_binop :=
(keyword "add" >> return assign_binop.add)
<|> (keyword "sub" >> return assign_binop.sub)
<|> (keyword "mul" >> return assign_binop.mul)
@ -82,7 +82,7 @@ def parse_assign_binop : parser assign_binop :=
<|> (keyword "string_push" >> return assign_binop.string_push)
<|> (keyword "string_append" >> return assign_binop.string_append)
def parse_unop : parser unop :=
def parse_unop : parsec unop :=
(keyword "inc_ref" >> return unop.inc_ref)
<|> (keyword "dec_ref" >> return unop.dec_ref)
<|> (keyword "inc" >> return unop.inc)
@ -93,44 +93,44 @@ def parse_unop : parser unop :=
<|> (keyword "array_pop" >> return unop.array_pop)
<|> (keyword "sarray_pop" >> return unop.sarray_pop)
def parse_literal : parser literal :=
def parse_literal : parsec literal :=
(keyword "tt" >> return (literal.bool tt))
<|> (keyword "ff" >> return (literal.bool ff))
<|> (do n ← lexeme num <?> "numeral", return (literal.num n))
<|> (do n ← (ch '-' >> lexeme num), return (literal.num (- n)))
<|> literal.str <$> parse_string_literal
def parse_uint16 : parser uint16 :=
def parse_uint16 : parsec uint16 :=
try (do p ← pos,
n ← lexeme num,
when (n ≥ uint16_sz) $ unexpected_at "big numeral, it does not fit in an uint16" p,
return $ uint16.of_nat n)
<?> "uint16"
def parse_usize : parser usize :=
def parse_usize : parsec usize :=
try (do p ← pos,
n ← lexeme num,
when (n ≥ usize_sz) $ unexpected_at "big numeral, it does not fit in an usize" p,
return $ usize.of_nat n)
<?> "usize"
def identifier : parser name :=
def identifier : parsec name :=
try (do p ← pos,
n ← lean.parser.identifier,
when (is_reserved_name n) $ unexpected_at "keyword" p,
return n)
<?> "identifier"
def parse_var : parser var :=
def parse_var : parsec var :=
lexeme identifier <?> "variable"
def parse_fnid : parser fnid :=
def parse_fnid : parsec fnid :=
lexeme identifier <?> "function name"
def parse_blockid : parser blockid :=
def parse_blockid : parsec blockid :=
lexeme identifier <?> "label"
def parse_nary_call (x : var) : parser instr :=
def parse_nary_call (x : var) : parsec instr :=
do xs ← many1 parse_var,
symbol ":=",
keyword "call",
@ -138,7 +138,7 @@ do xs ← many1 parse_var,
ys ← many parse_var,
return $ instr.call ([x] ++ xs) fid ys
def parse_typed_assignment (x : var) : parser instr :=
def parse_typed_assignment (x : var) : parsec instr :=
do symbol ":",
ty ← parse_type,
symbol ":=",
@ -148,7 +148,7 @@ do symbol ":",
<|> (instr.assign_binop x ty <$> parse_assign_binop <*> parse_var <*> parse_var)
<|> (instr.assign_lit x ty <$> parse_literal)
def parse_untyped_assignment (x : var) : parser instr :=
def parse_untyped_assignment (x : var) : parsec instr :=
do symbol ":=",
(keyword "closure" >> instr.closure x <$> parse_fnid <*> many parse_var)
<|> (keyword "apply" >> instr.apply x <$> many1 parse_var)
@ -158,13 +158,13 @@ do symbol ":=",
<|> (keyword "array" >> instr.array x <$> parse_var <*> parse_var)
<|> (keyword "sarray" >> instr.sarray x <$> parse_type <*> parse_var <*> parse_var)
def parse_assignment : parser instr :=
def parse_assignment : parsec instr :=
do x ← parse_var,
c ← curr,
if c = ':' then (parse_untyped_assignment x <|> parse_typed_assignment x)
else parse_nary_call x
def parse_instr : parser instr :=
def parse_instr : parsec instr :=
(keyword "array_write" >> instr.array_write <$> parse_var <*> parse_var <*> parse_var)
<|> (keyword "set" >> instr.set <$> parse_var <*> parse_uint16 <*> parse_var)
<|> (keyword "sset" >> instr.sset <$> parse_var <*> parse_usize <*> parse_var)
@ -172,27 +172,27 @@ def parse_instr : parser instr :=
<|> (instr.unop <$> parse_unop <*> parse_var)
<|> parse_assignment
def parse_phi : parser phi :=
def parse_phi : parsec phi :=
do (x, ty) ← try $ do { x ← parse_var, symbol ":", ty ← parse_type, symbol ":=", keyword "phi", return (x, ty) },
ys ← many1 parse_var,
return {x := x, ty := ty, ys := ys}
def parse_terminator : parser terminator :=
def parse_terminator : parsec terminator :=
(keyword "jmp" >> terminator.jmp <$> parse_blockid)
<|> (keyword "ret" >> terminator.ret <$> many parse_var)
<|> (keyword "case" >> terminator.case <$> parse_var <*> (symbol "[" >> sep_by1 parse_blockid (symbol ",") <* symbol "]"))
def parse_block : parser block :=
def parse_block : parsec block :=
do id ← try (parse_blockid <* symbol ":"),
ps ← many (parse_phi <* symbol ";"),
is ← many (parse_instr <* symbol ";"),
t ← parse_terminator <* symbol ";",
return { id := id, phis := ps, instrs := is, term := t }
def parse_arg : parser arg :=
def parse_arg : parsec arg :=
do symbol "(", x ← parse_var, symbol ":", ty ← parse_type, symbol ")", return {n := x, ty := ty}
def parse_header (is_const : bool) : parser header :=
def parse_header (is_const : bool) : parsec header :=
do n ← parse_fnid,
as ← if is_const then return [] else many parse_arg,
r ← if is_const
@ -200,16 +200,16 @@ do n ← parse_fnid,
else try (symbol ":" >> many1 (result.mk <$> parse_type)) <|> return [],
return { name := n, args := as, return := r, is_const := is_const }
def parse_def : parser decl :=
def parse_def : parsec decl :=
keyword "def" >> decl.defn <$> parse_header ff <*> (symbol ":=" >> many parse_block)
def parse_defconst : parser decl :=
def parse_defconst : parsec decl :=
keyword "defconst" >> decl.defn <$> parse_header tt <*> (symbol ":=" >> many parse_block)
def parse_external : parser decl :=
def parse_external : parsec decl :=
keyword "external" >> decl.external <$> parse_header ff
def parse_decl : parser decl :=
def parse_decl : parsec decl :=
parse_def <|> parse_defconst <|> parse_external
end ir

14
library/init/lean/name_mangling.lean
View file

@ -7,7 +7,7 @@ prelude
import init.lean.name init.lean.parser.string_literal
namespace lean
open lean.parser
open lean.parser.monad_parser
open lean.parser.monad_parsec
private def string.mangle_aux : nat → string.iterator → string → string
| 0 it r := r
@ -37,7 +37,7 @@ private def string.mangle_aux : nat → string.iterator → string → string
def string.mangle (s : string) : string :=
string.mangle_aux s.length s.mk_iterator ""
private def parse_mangled_string_aux : nat → string → parser string
private def parse_mangled_string_aux : nat → string → parsec string
| 0 r := return r
| (i+1) r :=
(eoi >> return r)
@ -49,11 +49,11 @@ private def parse_mangled_string_aux : nat → string → parser string
<|> (do str "_u", d₄ ← parse_hex_digit, d₃ ← parse_hex_digit, d₂ ← parse_hex_digit, d₁ ← parse_hex_digit,
parse_mangled_string_aux i (r.push (char.of_nat (d₄ * 4096 + d₃ * 256 + d₂ * 16 + d₁))))
private def parse_mangled_string : parser string :=
private def parse_mangled_string : parsec string :=
do r ← remaining, parse_mangled_string_aux r ""
def string.demangle (s : string) : option string :=
(parser.parse parse_mangled_string s).to_option
(parsec.parse parse_mangled_string s).to_option
private def name.mangle_aux (pre : string) : name → string
| name.anonymous := pre
@ -68,7 +68,7 @@ private def name.mangle_aux (pre : string) : name → string
def name.mangle (n : name) (pre : string := "_l") : string :=
name.mangle_aux pre n
private def parse_mangled_name_aux : nat → name → parser name
private def parse_mangled_name_aux : nat → name → parsec name
| 0 r := return r
| (i+1) r :=
(eoi >> return r)
@ -78,10 +78,10 @@ private def parse_mangled_name_aux : nat → name → parser name
<|> (do ch '_', n ← num, ch '_',
parse_mangled_name_aux i (r.mk_numeral n))
private def parse_mangled_name (pre : string) : parser name :=
private def parse_mangled_name (pre : string) : parsec name :=
do str pre, r ← remaining, parse_mangled_name_aux r name.anonymous
def name.demangle (s : string) (pre : string := "_l") : option name :=
(parser.parse (parse_mangled_name pre) s).to_option
(parsec.parse (parse_mangled_name pre) s).to_option
end lean

6
library/init/lean/parser/identifier.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.data.char.basic init.lean.parser.parser_t
import init.data.char.basic init.lean.parser.parsec
namespace lean
@ -38,8 +38,8 @@ def is_id_end_escape (c : char) : bool :=
c = id_end_escape
namespace parser
variables {m : Type → Type} [monad m] [monad_parser m] [alternative m]
open monad_parser
variables {m : Type → Type} [monad m] [monad_parsec m] [alternative m]
open monad_parsec
def id_part_default : m string :=
do c ← satisfy is_id_first,

82
library/init/lean/parser/parser_t.lean → library/init/lean/parser/parsec.lean
View file

@ -55,26 +55,26 @@ inductive result (α : Type)
@[inline] def result.mk_eps {α : Type} (a : α) (it : iterator) : result α :=
result.ok_eps a it dlist.empty
def parser (α : Type) :=
def parsec (α : Type) :=
iterator → result α
namespace parser
namespace parsec
open result
variables {α β : Type}
def run (p : parser α) (s : string) (fname := "") : except message α :=
def run (p : parsec α) (s : string) (fname := "") : except message α :=
match p s.mk_iterator with
| ok a _ := except.ok a
| ok_eps a _ _ := except.ok a
| error msg _ := except.error msg
protected def pure (a : α) : parser α :=
protected def pure (a : α) : parsec α :=
λ it, mk_eps a it
def eps : parser unit :=
parser.pure ()
def eps : parsec unit :=
parsec.pure ()
protected def failure : parser α :=
protected def failure : parsec α :=
λ it, error { unexpected := "failure", pos := it.offset } ff
def merge (msg₁ msg₂ : message) : message :=
@ -87,7 +87,7 @@ def merge (msg₁ msg₂ : message) : message :=
3- If `q` succeeds but does not consume input, then execute `q`
and merge error messages if both do not consume any input.
-/
protected def bind (p : parser α) (q : α → parser β) : parser β :=
protected def bind (p : parsec α) (q : α → parsec β) : parsec β :=
λ it, match p it with
| ok a it :=
(match q a it with
@ -101,16 +101,16 @@ protected def bind (p : parser α) (q : α → parser β) : parser β :=
| other := other)
| error msg c := error msg c
instance : monad parser :=
{ bind := @parser.bind, pure := @parser.pure }
instance : monad parsec :=
{ bind := @parsec.bind, pure := @parsec.pure }
instance : monad_fail parser :=
instance : monad_fail parsec :=
{ fail := λ _ s it, error { unexpected := s, pos := it.offset } ff }
def expect (msg : message) (exp : string) : message :=
{expected := dlist.singleton exp, ..msg}
@[inline] def label (p : parser α) (ex : string) : parser α :=
@[inline] def label (p : parsec α) (ex : string) : parsec α :=
λ it, match p it with
| ok_eps a it _ := ok_eps a it (dlist.singleton ex)
| error msg ff := error (expect msg ex) ff
@ -133,7 +133,7 @@ together.
```
Without the `try` combinator we will not be able to backtrack on the `let` keyword.
-/
def try (p : parser α) : parser α :=
def try (p : parsec α) : parsec α :=
λ it, match p it with
| error msg _ := error msg ff
| other := other
@ -153,7 +153,7 @@ def try (p : parser α) : parser α :=
it combines their error messages (even if one of
them succeeded).
-/
protected def orelse (p q : parser α) : parser α :=
protected def orelse (p q : parsec α) : parsec α :=
λ it, match p it with
| ok_eps a it' ex₁ :=
(match q it with
@ -167,42 +167,42 @@ protected def orelse (p q : parser α) : parser α :=
| other := other)
| other := other
instance : alternative parser :=
{ orelse := @parser.orelse,
failure := @parser.failure }
instance : alternative parsec :=
{ orelse := @parsec.orelse,
failure := @parsec.failure }
/-- Parse `p` without consuming any input. -/
def lookahead (p : parser α) : parser α :=
def lookahead (p : parsec α) : parsec α :=
λ it, match p it with
| ok a s' := mk_eps a it
| other := other
/-- `not_followed_by p` succeeds when parser `p` fails -/
def not_followed_by (p : parser α) (msg : string := "input") : parser unit :=
def not_followed_by (p : parsec α) (msg : string := "input") : parsec unit :=
λ it, match p it with
| ok _ _ := error { pos := it.offset, unexpected := msg } ff
| ok_eps _ _ _ := error { pos := it.offset, unexpected := msg } ff
| error _ _ := mk_eps () it
end parser
end parsec
/- Type class for abstracting from concrete monad stacks containing a `parser_t` somewhere. -/
class monad_parser (m : Type → Type) :=
/- Type class for abstracting from concrete monad stacks containing a `parsec` somewhere. -/
class monad_parsec (m : Type → Type) :=
-- analogous to e.g. `monad_state.lift`
(lift {} {α : Type} : parser α → m α)
(lift {} {α : Type} : parsec α → m α)
-- Analogous to e.g. `monad_reader_adapter.map` before simplification (see there).
-- Its usage seems to be way too common to justify moving it into a separate type class.
(map {} {α : Type} : (∀ {α}, parser α → parser α) → m α → m α)
(map {} {α : Type} : (∀ {α}, parsec α → parsec α) → m α → m α)
instance {m : Type → Type} [monad m] : monad_parser parser :=
instance {m : Type → Type} [monad m] : monad_parsec parsec :=
{ lift := λ α p, p,
map := λ α f x, f x }
instance monad_parser_trans {m n : Type → Type} [has_monad_lift m n] [monad_functor m m n n] [monad_parser m] : monad_parser n :=
{ lift := λ α p, monad_lift (monad_parser.lift p : m α),
map := λ α f x, monad_map (λ β x, (monad_parser.map @f x : m β)) x }
instance monad_parsec_trans {m n : Type → Type} [has_monad_lift m n] [monad_functor m m n n] [monad_parsec m] : monad_parsec n :=
{ lift := λ α p, monad_lift (monad_parsec.lift p : m α),
map := λ α f x, monad_map (λ β x, (monad_parsec.map @f x : m β)) x }
namespace monad_parser
variables {m : Type → Type} [monad m] [monad_parser m] [alternative m] {α β : Type}
namespace monad_parsec
variables {m : Type → Type} [monad m] [monad_parsec m] [alternative m] {α β : Type}
@[inline] def error {α : Type} (unexpected : string := "") (expected : dlist string := dlist.empty) : m α :=
lift $ λ it, result.error ⟨it.offset, unexpected, expected⟩ ff
@ -211,7 +211,7 @@ def left_over : m iterator :=
lift $ λ it, result.mk_eps it it
@[inline] def label (p : m α) (ex : string) : m α :=
map (λ _ p, @parser.label _ p ex) p
map (λ _ p, @parsec.label _ p ex) p
infixr ` <?> `:2 := label
@ -233,17 +233,17 @@ together.
Without the `try` combinator we will not be able to backtrack on the `let` keyword.
-/
@[inline] def try (p : m α) : m α :=
map (λ _ p, parser.try p) p
map (λ _ p, parsec.try p) p
/-- Parse `p` without consuming any input. -/
@[inline] def lookahead (p : m α) : m α :=
map (λ _ p, parser.lookahead p) p
map (λ _ p, parsec.lookahead p) p
-- TODO(Sebastian): `monad_functor` is too weak to lift this, probably needs something like `monad_control`
/-
/-- `not_followed_by p` succeeds when parser `p` fails -/
@[inline] def not_followed_by (p : m α) (msg : string := "input") : m unit :=
map (λ _ _ inst p, @parser_t.not_followed_by _ inst _ p msg) p
map (λ _ _ inst p, @parsec_t.not_followed_by _ inst _ p msg) p
-/
/-- Faster version of `not_followed_by (satisfy p)` -/
@ -480,21 +480,21 @@ error msg
def unexpected_at (msg : string) (pos : position) : m α :=
lift $ λ _, result.error {unexpected := msg, pos := pos} ff
end monad_parser
end monad_parsec
namespace parser
open monad_parser
namespace parsec
open monad_parsec
variables {m : Type → Type} [monad m] {α β : Type}
def parse (p : parser α) (s : string) (fname := "") : except message α :=
def parse (p : parsec α) (s : string) (fname := "") : except message α :=
run p s fname
def parse_with_eoi (p : parser α) (s : string) (fname := "") : except message α :=
def parse_with_eoi (p : parsec α) (s : string) (fname := "") : except message α :=
run (p <* eoi) s fname
def parse_with_left_over (p : parser α) (s : string) (fname := "") : except message (α × iterator) :=
def parse_with_left_over (p : parsec α) (s : string) (fname := "") : except message (α × iterator) :=
run (prod.mk <$> p <*> left_over) s fname
end parser
end parsec
end parser
end lean

10
library/init/lean/parser/reader/basic.lean
View file

@ -6,7 +6,7 @@ Author: Sebastian Ullrich
Reader for the Lean language
-/
prelude
import init.lean.parser.parser_t init.lean.parser.syntax init.lean.parser.macro
import init.lean.parser.parsec init.lean.parser.syntax init.lean.parser.macro
import init.lean.parser.identifier
namespace lean
@ -22,7 +22,7 @@ structure token_config :=
It should return a syntax tree with a "hole" for the
`source_info` surrounding the token, which will be supplied
by the `token` reader. -/
(token_reader : option (parser (source_info → syntax)) := none)
(token_reader : option (parsec (source_info → syntax)) := none)
structure reader_state :=
(tokens : list token_config)
@ -34,7 +34,7 @@ def reader_state.empty : reader_state :=
structure reader_config := mk
@[irreducible] def read_m := reader_t reader_config $ state_t reader_state $ parser
@[irreducible] def read_m := reader_t reader_config $ state_t reader_state $ parsec
structure reader :=
(read : read_m syntax)
@ -46,7 +46,7 @@ instance : monad read_m := infer_instance
instance : alternative read_m := infer_instance
instance : monad_reader reader_config read_m := infer_instance
instance : monad_state reader_state read_m := infer_instance
instance : monad_parser read_m := infer_instance
instance : monad_parsec read_m := infer_instance
--TODO(Sebastian): expose `reader_state.errors`
protected def run {α : Type} (cfg : reader_config) (st : reader_state) (s : string) (r : read_m α) :
@ -55,7 +55,7 @@ prod.fst <$> ((r.run cfg).run st).parse_with_eoi s
end read_m
namespace reader
open monad_parser
open monad_parsec
protected def parse (cfg : reader_config) (s : string) (r : reader) :
except parser.message syntax :=

2
library/init/lean/parser/reader/module.lean
View file

@ -10,7 +10,7 @@ import init.lean.parser.reader.token
namespace lean.parser
namespace reader
open monad_parser
open monad_parsec
def «prelude» := {macro . name := `prelude}

4
library/init/lean/parser/reader/token.lean
View file

@ -17,7 +17,7 @@ import init.lean.parser.reader.basic init.util
namespace lean.parser
namespace reader
open lean.parser.monad_parser
open lean.parser.monad_parsec
open string
def match_token : read_m (option token_config) :=
@ -95,7 +95,7 @@ do (r, i) ← with_source_info $ do {
do str tk,
pure $ λ i, syntax.atom ⟨some i, atomic_val.string tk⟩
-- variable-length token
| some ⟨tk, some r⟩ := str tk *> monad_parser.lift r
| some ⟨tk, some r⟩ := str tk *> monad_parsec.lift r
| none := number' <|> ident'
},
pure (r i)

12
library/init/lean/parser/string_literal.lean
View file

@ -4,19 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.lean.parser.parser_t
import init.lean.parser.parsec
namespace lean
namespace parser
open monad_parser
open monad_parsec
def parse_hex_digit : parser nat :=
def parse_hex_digit : parsec nat :=
( (do d ← digit, return $ d.val - '0'.val)
<|> (do c ← satisfy (λ c, 'a'.val ≤ c.val && c.val ≤ 'f'.val), return $ 10 + (c.val - 'a'.val))
<|> (do c ← satisfy (λ c, 'A'.val ≤ c.val && c.val ≤ 'F'.val), return $ 10 + (c.val - 'A'.val)))
<?> "hexadecimal"
def parse_quoted_char : parser char :=
def parse_quoted_char : parsec char :=
do p ← pos,
c ← any,
if c = '\\' then return '\\'
@ -36,7 +36,7 @@ do p ← pos,
return $ char.of_nat (16*(16*(16*d₁ + d₂) + d₃) + d₄) }
else unexpected_at "quoted character" p
def parse_string_literal_aux : nat → string → parser string
def parse_string_literal_aux : nat → string → parsec string
| 0 s := ch '\"' >> return s
| (n+1) s := do
c ← any,
@ -44,7 +44,7 @@ def parse_string_literal_aux : nat → string → parser string
else if c = '\"' then return s
else parse_string_literal_aux n (s.push c)
def parse_string_literal : parser string :=
def parse_string_literal : parsec string :=
do ch '\"',
r ← remaining,
parse_string_literal_aux r ""

2
library/init/lean/parser/syntax.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Sebastian Ullrich
-/
prelude
import init.lean.name init.lean.parser.parser_t
import init.lean.name init.lean.parser.parsec
namespace lean
namespace parser

36
tests/lean/parser1.lean → tests/lean/parsec1.lean
View file

@ -1,19 +1,19 @@
import system.io init.lean.parser.identifier init.lean.ir.parser init.lean.ir.format
open lean.parser
open lean.parser.monad_parser
open lean.parser.monad_parsec
def test {α} [decidable_eq α] (p : parser α) (s : string) (e : α) : io unit :=
match parser.parse p s with
def test {α} [decidable_eq α] (p : parsec α) (s : string) (e : α) : io unit :=
match parsec.parse p s with
| except.ok a := if a = e then return () else io.print_ln "unexpected result"
| except.error e := io.print_ln (e.to_string s)
def test_failure {α} (p : parser α) (s : string) : io unit :=
match parser.parse p s with
def test_failure {α} (p : parsec α) (s : string) : io unit :=
match parsec.parse p s with
| except.ok a := io.print_ln "unexpected success"
| except.error e := return ()
def show_result {α} [has_to_string α] (p : parser α) (s : string) : io unit :=
match parser.parse p s with
def show_result {α} [has_to_string α] (p : parsec α) (s : string) : io unit :=
match parsec.parse p s with
| except.ok a := io.print_ln "result: " >> io.print_ln (repr $ to_string a)
| except.error e := io.print_ln (e.to_string s)
@ -37,12 +37,12 @@ match parser.parse p s with
#eval test (str "ab" >> pure () <|> (ch 'a' >> ch 'c' >> pure ())) "ac" ()
#eval test (try (ch 'a' >> ch 'b') <|> (ch 'a' >> ch 'c')) "ac" 'c'
#eval test (lookahead (ch 'a')) "abc" 'a'
#eval test_failure (parser.not_followed_by (lookahead (ch 'a'))) "abc"
#eval test_failure (parsec.not_followed_by (lookahead (ch 'a'))) "abc"
def symbol (c : char) : parser char :=
def symbol (c : char) : parsec char :=
lexeme (ch c) <?> repr c
def paren {α} (p : parser α) : parser α :=
def paren {α} (p : parsec α) : parsec α :=
symbol '(' >> lexeme p <* symbol ')'
#eval test (paren num) "( 10 )" 10
@ -50,7 +50,7 @@ symbol '(' >> lexeme p <* symbol ')'
#eval test (paren num) "(0)" 0
#eval test (paren num) "(0 )" 0
def var : parser string :=
def var : parsec string :=
do c ← satisfy (λ a, a.is_alpha || a = '_'),
r ← lexeme $ take_while (λ a, a.is_digit || a.is_alpha || a = '_'),
return (c.to_string ++ r)
@ -96,7 +96,7 @@ open lean
#eval test_failure parse_string_literal "\"\\u03b\\u03b1\""
#eval test_failure parse_string_literal "\"\\u03bz\\u03b1\""
def parse_instr_pp : parser string :=
def parse_instr_pp : parsec string :=
do cmd ← lean.ir.parse_instr,
return $ to_string cmd
@ -151,18 +151,18 @@ instance eq_expr : decidable_eq Expr
| is_false h' := is_false (λ he, Expr.no_confusion he (λ h₁ h₂, absurd h₂ h')))
| is_false h := is_false (λ he, Expr.no_confusion he (λ h₁ h₂, absurd h₁ h))
def parse_atom (p : parser Expr) : parser Expr :=
def parse_atom (p : parsec Expr) : parsec Expr :=
(Var <$> lexeme var <?> "variable")
<|>
(Num <$> lexeme num <?> "numeral")
<|>
(paren p)
def parse_add (p : parser Expr) : parser Expr :=
def parse_add (p : parsec Expr) : parsec Expr :=
do l ← parse_atom p,
(do symbol '+', r ← p, return $ Add l r) <|> return l
def parse_expr : parser Expr :=
def parse_expr : parsec Expr :=
whitespace >> fix (λ F, parse_add F) <* eoi
#eval test parse_expr "10" (Num 10)
@ -181,9 +181,9 @@ whitespace >> fix (λ F, parse_add F) <* eoi
namespace paper_ex
#print "Failure 3"
def digit : parser char := monad_parser.digit <?> "digit"
def letter : parser char := monad_parser.alpha <?> "letter"
def tst : parser char := (digit <|> return '0') >> letter
def digit : parsec char := monad_parsec.digit <?> "digit"
def letter : parsec char := monad_parsec.alpha <?> "letter"
def tst : parsec char := (digit <|> return '0') >> letter
#eval test tst "*" 'a'
#print "---------"
end paper_ex

0
tests/lean/parser1.lean.expected.out → tests/lean/parsec1.lean.expected.out
View file

2
tests/lean/run/display_hw_term_hack_deps.lean
View file

@ -1,5 +1,5 @@
import init.lean.parser.syntax
import init.lean.parser.parser_t
import init.lean.parser.parsec
import init.lean.ir.type_check init.lean.ir.ssa_check init.lean.ir.elim_phi init.lean.ir.parser
open tactic

2
tests/lean/run/name_mangling.lean
View file

@ -3,7 +3,7 @@ open lean lean.parser
open tactic
meta def check (s : string) : tactic unit :=
match id.run $ parser.parse identifier s with
match id.run $ parsec.parse identifier s with
| except.ok n :=
trace (name.mangle n) >>
if name.demangle (name.mangle n) = some n then exact `(true)

10
tests/lean/run/parser_ir1.lean
View file

@ -4,7 +4,7 @@ import init.lean.ir.elim_phi init.lean.ir.type_check
import init.lean.ir.extract_cpp
open lean.parser
open lean.parser.monad_parser
open lean.parser.monad_parsec
open lean.ir
def check_decl (d : decl) : io unit :=
@ -12,8 +12,8 @@ match type_check d with
| except.ok _ := return ()
| except.error e := io.print_ln (to_string e)
def show_result (p : parser decl) (s : string) : io unit :=
match parser.parse p s with
def show_result (p : parsec decl) (s : string) : io unit :=
match parsec.parse p s with
| except.ok d := io.print_ln (lean.to_fmt d) >> check_decl d
| except.error e := io.print_ln (e.to_string s)
@ -45,7 +45,7 @@ end:
#eval show_result (whitespace >> parse_def) IR2
def tst_elim_phi (s : string) : io unit :=
do (except.ok d) ← return $ parser.parse (whitespace >> parse_def) s,
do (except.ok d) ← return $ parsec.parse (whitespace >> parse_def) s,
check_decl d,
io.print_ln (lean.to_fmt (elim_phi d))
@ -66,7 +66,7 @@ main:
#eval show_result (whitespace >> parse_def) IR3
def tst_extract_cpp (s : string) : io unit :=
do (except.ok d) ← return $ parser.parse (whitespace >> parse_def) s,
do (except.ok d) ← return $ parsec.parse (whitespace >> parse_def) s,
check_decl d,
match extract_cpp [elim_phi d] with
| except.ok code := io.print_ln code