From a4b9cc83b899c073f322c9031bed7770cbbfb1ee Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 19 Nov 2018 19:23:05 +0100 Subject: [PATCH] feat(library/init/lean/{expander,elaborator}): progress --- library/init/lean/elaborator.lean | 30 ++++++++++++++++++++++++++---- library/init/lean/expander.lean | 28 ++++++++++++++++++++++++---- library/init/lean/parser/term.lean | 6 ++++++ 3 files changed, 56 insertions(+), 8 deletions(-) diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index ae3ec7ab88..78a12a1dd0 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -78,10 +78,12 @@ def to_level : syntax → elaborator_m level | _ := error stx "ill-formed universe level") | _ := error stx $ "unexpected node: " ++ to_string k.name +def expr.mk_annotation (ann : name) (e : expr) := +expr.mdata (kvmap.set_name {} `annotation `anonymous_constructor) e + def to_pexpr : syntax → elaborator_m expr -| stx := do - some k ← pure stx.kind | error stx $ "unexpected atom: " ++ to_string stx, - match k with +| (syntax.ident id) := pure $ expr.const (mangle_ident id) [] +| stx@(syntax.raw_node {kind := k, ..}) := (match k with | @ident_univs := (match view ident_univs stx with | {id := id, univs := some univs} := expr.const (mangle_ident id) <$> univs.levels.mmap to_level | {id := id, univs := none} := pure $ expr.const (mangle_ident id) []) @@ -100,7 +102,27 @@ def to_pexpr : syntax → elaborator_m expr | @sort := (match view sort stx with | sort.view.Sort _ := pure $ expr.sort level.zero | sort.view.Type _ := pure $ expr.sort $ level.succ level.zero) - | _ := error stx $ "unexpected node: " ++ to_string k.name + | @anonymous_constructor := do + let v := view anonymous_constructor stx, + p ← to_pexpr $ mk_app' (review hole {}) (v.args.map prod.fst), + pure $ expr.mk_annotation `anonymous_constructor p + | @hole := pure $ expr.const "_" [] -- TODO + | @«have» := do + let v := view «have» stx, + let id := (mangle_ident <$> opt_ident.view.id <$> v.id).get_or_else `this, + let proof := match v.proof with + | have_proof.view.term hpt := hpt.term + | have_proof.view.from hpf := hpf.from.proof, + lam ← expr.lam id binder_info.default <$> to_pexpr v.prop <*> to_pexpr proof, + pure $ expr.mk_annotation `have lam + | @projection := do + let v := view projection stx, + let val := match v.proj with + | projection_spec.view.id id := data_value.of_name id.val + | projection_spec.view.num n := data_value.of_nat n.to_nat, + expr.mdata (kvmap.insert {} `field_notation val) <$> to_pexpr v.term + | _ := error stx $ "unexpected node: " ++ to_string k.name) +| stx := error stx $ "unexpected: " ++ to_string stx def declaration.elaborate : elaborator := λ stx, do diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean index 0fc7e92136..75362b1277 100644 --- a/library/init/lean/expander.lean +++ b/library/init/lean/expander.lean @@ -44,9 +44,6 @@ instance coe_ident_binder_id : has_coe syntax_ident binder_ident.view := instance coe_binders {α : Type} [has_coe_t α binder_ident.view] : has_coe (list α) term.binders.view := ⟨λ ids, {leading_ids := ids.map coe}⟩ -def mk_app (fn : syntax_ident) (args : list syntax) : syntax := -args.foldl (λ fn arg, syntax.mk_node app [fn, arg]) (syntax.ident fn) - def mk_simple_lambda (id : syntax_ident) (bi : binder_info) (dom body : syntax) : syntax := let bc : binder_content.view := {ids := [id], type := some {type := dom}} in review lambda { @@ -179,13 +176,36 @@ def reserve_mixfix.transform : transformer := spec ← mixfix_to_notation_spec v.kind v.symbol, pure $ review reserve_notation {spec := spec} +def paren.transform : transformer := +λ stx, do + let v := view paren stx, + match v.content with + | none := pure $ syntax.ident `unit.star + | some {term := t, special := none} := pure t + | some {term := t, special := paren_special.view.tuple tup} := + pure $ some $ (tup.tail.map prod.fst).foldr (λ t tup, mk_app `prod.mk [t, tup]) t + | some {term := t, special := paren_special.view.typed pst} := + pure $ mk_app `typed_expr [pst.type, t] + +def assume.transform : transformer := +λ stx, do + let v := view «assume» stx, + let binders : lambda_binders.view := match v.binders with + | assume_binders.view.anonymous aba := lambda_binders.view.simple $ + -- TODO(Sebastian): unhygienic! + simple_binder.view.explicit {id := "this", type := aba.type} + | assume_binders.view.binders abb := lambda_binders.view.extended abb, + pure $ review lambda {binders := binders, body := v.body} + local attribute [instance] name.has_lt_quick -- TODO(Sebastian): replace with attribute def transformers : rbmap name transformer (<) := rbmap.from_list [ (mixfix.name, mixfix.transform), (reserve_mixfix.name, reserve_mixfix.transform), - (lambda.name, lambda.transform) + (lambda.name, lambda.transform), + (paren.name, paren.transform), + (assume.name, assume.transform) ] _ structure expander_state := diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index 07335f9fb2..eb3d52a6c6 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -340,6 +340,12 @@ node! sort_app [fn: get_leading, arg: monad_lift (level.parser max_prec).run] def app.parser : trailing_term_parser := node! app [fn: get_leading, arg: term.parser max_prec] +def mk_app' (fn : syntax) (args : list syntax) : syntax := +args.foldl (λ fn arg, syntax.mk_node app [fn, arg]) fn + +def mk_app (fn : syntax_ident) (args : list syntax) : syntax := +mk_app' (syntax.ident fn) args + @[derive parser.has_tokens parser.has_view] def arrow.parser : trailing_term_parser := node! arrow [dom: get_leading, op: unicode_symbol "→" "->" 25, range: term.parser 24]