From aa111df0ec5f05142e440500d8c0705b1cddfde9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 25 Jun 2019 11:20:31 -0700
Subject: [PATCH] feat(library/init/lean/syntax): add `Syntax.isIdOrAtom`

---
 library/init/lean/compiler/externattr.lean | 29 +++++++++++++++++++---
 library/init/lean/syntax.lean              | 13 ++++++++--
 2 files changed, 37 insertions(+), 5 deletions(-)

diff --git a/library/init/lean/compiler/externattr.lean b/library/init/lean/compiler/externattr.lean
index 56d1a5b218..ac36649bd7 100644
--- a/library/init/lean/compiler/externattr.lean
+++ b/library/init/lean/compiler/externattr.lean
@@ -42,15 +42,38 @@ structure ExternAttrData :=
 
 @[export lean.mk_extern_attr_data_core] def mkExternAttrData := ExternAttrData.mk
 
+/-
+private partial def syntaxToExternEntries (a : Array Syntax) : Nat → List ExternEntry → Except String (List ExternEntry)
+| i entries :=
+  if i == a.size then Except.ok entries
+  else match a.get i with
+    | Syntax.ident _ _ backend _ _ :=
+      let i := i + 1 in
+      if i == a.size then Except.error "string or identifier expected"
+      else match a.get i with
+        | Syntax.ident _ _ "inline" _ _ := Except.error ""
+        | Syntax.ident _ _
+    | _ := Except.error "identifier expected"
+-/
+
 private def syntaxToExternAttrData (s : Syntax) : Except String ExternAttrData :=
 match s with
 | Syntax.missing := Except.ok { entries := [ ExternEntry.adhoc `all ] }
 | Syntax.node _ args _ :=
   if args.size == 0 then Except.error "unexpected kind of argument"
   else
-    let i := 0 in
-    -- TODO
-    Except.ok { entries := [] }
+    let (arity, i) : Option Nat × Nat := match (args.get 0).isNatLit with
+      | some arity := (some arity, 1)
+      | none       := (none, 0) in
+    match (args.get i).isStrLit with
+    | some str :=
+      if args.size == i+1 then
+        Except.ok { arity := arity, entries := [ ExternEntry.standard `all str ] }
+      else
+        Except.error "invalid extern attribute"
+    | none :=
+      -- TODO
+      Except.ok { entries := [] }
 | _ := Except.error "unexpected kind of argument"
 
 -- def mkExternAttr : IO (ParametricAttribute ExternAttrData) :=
diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean
index a41c4669d5..df5da1b6c1 100644
--- a/library/init/lean/syntax.lean
+++ b/library/init/lean/syntax.lean
@@ -245,7 +245,9 @@ mkStrLit val
 def mkNumLitAux (val : Nat) : Syntax :=
 mkNumLit (toString val)
 
-def Syntax.isStrLit : Syntax → Option String
+namespace Syntax
+
+def isStrLit : Syntax → Option String
 | (Syntax.node k args _) :=
   if k == strLitKind && args.size == 1 then
     match args.get 0 with
@@ -314,7 +316,7 @@ else
   else if c.isDigit then decodeDecimalLitAux s 0 0
   else none
 
-def Syntax.isNatLit : Syntax → Option Nat
+def isNatLit : Syntax → Option Nat
 | (Syntax.node k args _) :=
   if k == strLitKind && args.size == 1 then
     match args.get 0 with
@@ -324,4 +326,11 @@ def Syntax.isNatLit : Syntax → Option Nat
     none
 | _ := none
 
+def isIdOrAtom : Syntax → Option String
+| (Syntax.atom _ val)           := some val
+| (Syntax.ident _ rawVal _ _ _) := some rawVal.toString
+| _ := none
+
+end Syntax
+
 end Lean