feat(library/init/lean/{expander,elaborator}): progress

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

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 :=

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]