From db0fc4a4486810459c1955aff36bf6e35c1178be Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 24 Sep 2018 09:53:18 -0700 Subject: [PATCH] feat(library/init/lean/expander): very basic expander --- library/init/lean/expander.lean | 25 ++++++++++++++++- tests/lean/parser1.lean | 18 ++++-------- tests/lean/parser1.lean.expected.out | 42 ++++++---------------------- 3 files changed, 38 insertions(+), 47 deletions(-) diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean index 6f4bd6e22d..1863fce073 100644 --- a/library/init/lean/expander.lean +++ b/library/init/lean/expander.lean @@ -15,7 +15,17 @@ open parser.term open parser.command open parser.command.notation_spec -def mixfix.transform (stx : tysyntax mixfix.view) : option (tysyntax notation.view) := +@[derive monad] +def transform_m := option_t $ except message +abbreviation transformer := syntax → transform_m syntax + +section +local attribute [reducible] transform_m +instance coe_option_transform_m {α : Type} : has_coe (option α) (transform_m α) := +⟨λ o, match o with some a := pure a | none := failure⟩ +end + +def mixfix.transform (stx : tysyntax mixfix.view) : transform_m (tysyntax notation.view) := do v ← view stx, -- TODO: reserved token case notation_symbol.view.quoted quoted ← view v.symbol, @@ -42,5 +52,18 @@ do v ← view stx, | _ := sorry, pure $ review {spec := review spec, term := term} +local attribute [instance] name.has_lt_quick + +-- TODO(Sebastian): replace with attribute +def transformers : rbmap name transformer (<) := rbmap.from_list [ + (mixfix.name, mixfix.transform) +] _ + +def expand (stx : syntax) : except message syntax := +--TODO(Sebastian): recursion, hygiene, error messages +do syntax.node {kind := some k, ..} ← pure stx | pure stx, + some t ← pure $ transformers.find k.name | pure stx, + flip option.get_or_else stx <$> t stx + end expander end lean diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean index 65aaf3e34e..18dbe4f7de 100644 --- a/tests/lean/parser1.lean +++ b/tests/lean/parser1.lean @@ -1,7 +1,7 @@ -import init.lean.parser.module init.io +import init.lean.parser.module init.lean.expander init.io open lean open lean.parser -open lean.parser.syntax_node_kind.has_view +open lean.expander def show_result (p : syntax × message_log) (s : string) : except_t string io unit := let (stx, msgs) := p in @@ -57,16 +57,6 @@ universes u v -- parsed as `Type (max) (u) (v)`, will fail on elaboration ("max: must have at least two arguments", "function expected at 'Type'", "unknown identifier 'u'/'v'") #eval show_parse "#check Type max u v" --- expansion example -#eval (do { - (stx, ⟨[]⟩) ← monad_except.lift_except $ parse_module "prefix `+`:10 := _", - some {root := stx, ..} ← pure $ parser.parse.view stx, - some {commands := [stx], ..} ← pure $ view module stx, - some stx ← pure $ command.mixfix.expand stx | throw "expand fail", - io.println stx, - io.println stx.reprint -} : except_t string io unit) - -- slowly progressing... #eval do s ← io.fs.read_file "../../library/init/core.lean", @@ -77,5 +67,7 @@ universes u v | coroutine_result_core.done p := show_result p s *> pure (sum.inr ()) | coroutine_result_core.yielded cmd k := do { --io.println "command:" *> io.println cmd, - pure (sum.inl k) + match expand cmd with + | except.ok cmd' := pure (sum.inl k) + | except.error e := throw e.text } diff --git a/tests/lean/parser1.lean.expected.out b/tests/lean/parser1.lean.expected.out index a04afe9d8b..96c67648c2 100644 --- a/tests/lean/parser1.lean.expected.out +++ b/tests/lean/parser1.lean.expected.out @@ -117,30 +117,6 @@ result: (term.ident `u [])) (term.ident `v [])))]) (eoi "")] -(command.notation - "notation" - (command.notation_spec - (1 - (command.notation_spec.rules - [] - [(command.notation_spec.rule - (command.notation_spec.notation_symbol - (0 - (command.notation_spec.notation_quoted_symbol - "`" - "+" - "`" - [(command.notation_spec.precedence ":" (base10_lit "10"))]))) - [(command.notation_spec.transition - (2 - (command.notation_spec.argument - `b - [(command.notation_spec.action - ":" - (command.notation_spec.action_kind (0 (base10_lit "10"))))])))])]))) - ":=" - (term.hole "_")) -notation`+`:10 b:10 :=_ error at line 223, column 6: unexpected '=' error at line 225, column 44: @@ -841,7 +817,7 @@ partial syntax tree: (command.simple_decl_val ":=" (term.lambda - "λ" + (term.lambda_op (0 "λ")) [(term.binder (1 (term.binder_content @@ -1164,7 +1140,7 @@ partial syntax tree: (term.anonymous_constructor "⟨" [(term.lambda - "λ" + (term.lambda_op (0 "λ")) [(term.binder (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))] "," @@ -1274,7 +1250,7 @@ partial syntax tree: (term.anonymous_constructor "⟨" [(term.lambda - "λ" + (term.lambda_op (0 "λ")) [(term.binder (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))] "," @@ -1348,7 +1324,7 @@ partial syntax tree: (term.anonymous_constructor "⟨" [(term.lambda - "λ" + (term.lambda_op (0 "λ")) [(term.binder (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))] "," @@ -1438,7 +1414,7 @@ partial syntax tree: (term.anonymous_constructor "⟨" [(term.lambda - "λ" + (term.lambda_op (0 "λ")) [(term.binder (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))] "," @@ -1548,7 +1524,7 @@ partial syntax tree: (term.anonymous_constructor "⟨" [(term.lambda - "λ" + (term.lambda_op (0 "λ")) [(term.binder (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))] "," @@ -1622,7 +1598,7 @@ partial syntax tree: (term.anonymous_constructor "⟨" [(term.lambda - "λ" + (term.lambda_op (0 "λ")) [(term.binder (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))] "," @@ -1843,7 +1819,7 @@ partial syntax tree: (term.paren "(" [(term.lambda - "λ" + (term.lambda_op (0 "λ")) [(term.binder (1 (term.binder_content @@ -1962,7 +1938,7 @@ partial syntax tree: (term.paren "(" [(term.lambda - "λ" + (term.lambda_op (0 "λ")) [(term.binder (1 (term.binder_content