chore: improve list handling

RDF/Triple.lean

@@ -2,6 +2,7 @@ import Lean
 import RDF.BlankNode
 import RDF.NamedNode
 import RDF.Literal
+import RDF.Vocab
 
 inductive Subject where
   | NamedNode : NamedNode → Subject
@@ -48,6 +49,15 @@ instance : Coe BlankNode Object where
 instance : Coe Literal Object where
   coe n := Object.Literal n
 
+instance : Coe Subject Object where
+  coe
+    | Subject.NamedNode n => Object.NamedNode n
+    | Subject.BlankNode n => Object.BlankNode n
+
+instance : Coe Predicate Object where
+  coe
+    | Predicate.NamedNode n => Object.NamedNode n
+
 structure Triple where
   subject : Subject
   predicate : Predicate
@@ -57,4 +67,23 @@ deriving Repr, DecidableEq, Lean.ToJson, Lean.FromJson
 instance : ToString Triple where
   toString triple := "⟪" ++ toString triple.subject ++ " " ++ toString triple.predicate ++ " " ++ toString triple.object ++ "⟫"
 
+structure RDFList where
+  head : Subject
+  triples : List Triple
+
 macro "⟪" s:term "," p:term "," o:term "⟫" : term => `(Triple.mk $s $p $o)
+
+-- FIXME: Improve blank node generation to prevent collisions
+def toList : List Object → RDFList
+  | [] => ⟨RDF.nil, []⟩
+  | x::xs =>
+    let ⟨head, triples⟩ := toList xs
+    let nextHead := BlankNode.mk ("b" ++ toString xs.length)
+    ⟨nextHead, ⟪nextHead, RDF.first, x⟫::⟪nextHead, RDF.rest, head⟫::triples⟩
+
+def tripleToList (s: Subject) (p: Predicate) (o: List Object) : List Triple :=
+  let ⟨head, triples⟩ := toList o
+  ⟪s, p, head⟫::triples
+
+syntax "⟪" term "," term "," "[" term,* "]" : term
+macro_rules | `(⟪ $s, $p, [ $o,* ] ⟫) => `(tripleToList $s $p [$o,*])

RDF/Vocab.lean

@@ -1,9 +1,57 @@
 import RDF.NamedNode
 
 namespace XSD
-  def mk (e: String) : NamedNode := ⟨"http://www.w3.org/2001/XMLSchema#".append e⟩
+  def mk (e: String) := #⟨"http://www.w3.org/2001/XMLSchema#" ++ e⟩
   def integer := mk "integer"
+  def anyURI := mk "anyURI"
+  def dateTime := mk "dateTime"
+  def double := mk "double"
+  def decimal := mk "decimal"
   def boolean := mk "boolean"
   def float := mk "float"
   def string := mk "string"
 end XSD
+
+namespace RDF
+  def mk (e: String) := #⟨"http://www.w3.org/1999/02/22-rdf-syntax-ns#" ++ e⟩
+  def HTML := mk "HTML"
+  def langString := mk "langString"
+  def PlainLiteral := mk "PlainLiteral"
+  def type := mk "type"
+  def Property := mk "Property"
+  def Statement := mk "Statement"
+  def subject := mk "subject"
+  def predicate := mk "predicate"
+  def object := mk "object"
+  def Bag := mk "Bag"
+  def Seq := mk "Seq"
+  def Alt := mk "Alt"
+  def value := mk "value"
+  def List := mk "List"
+  def nil := mk "nil"
+  def first := mk "first"
+  def rest := mk "rest"
+  def XMLLiteral := mk "XMLLiteral"
+  def JSON := mk "JSON"
+  def CompoundLiteral := mk "CompoundLiteral"
+  def language := mk "language"
+  def direction := mk "direction"
+end RDF
+
+namespace RDFS
+  def mk (e: String) := #⟨"http://www.w3.org/2000/01/rdf-schema#" ++ e⟩
+  def Resource := mk "Resource"
+  def Class := mk "Class"
+  def subClassOf := mk "subClassOf"
+  def subPropertyOf := mk "subPropertyOf"
+  def comment := mk "comment"
+  def label := mk "label"
+  def domain := mk "domain"
+  def seeAlso := mk "seeAlso"
+  def isDefinedBy := mk "isDefinedBy"
+  def Literal := mk "Literal"
+  def Container := mk "Container"
+  def ContainerMembershipProperty := mk "ContainerMembershipProperty"
+  def member := mk "member"
+  def Datatype := mk "Datatype"
+end RDFS

README.md

@@ -25,7 +25,7 @@ require RDF from git
 import RDF
 
 def main : IO Unit := do
-  IO.println (← IO.ofExcept $ RDFParse "[] </predicate> true, 1, \"hello\" \"hello\"@en ." "text/turtle" "http://example.org")
+  IO.println (← IO.ofExcept $ RDFParse "[] </predicate> true, 1, \"hello\" \"hello\"@en, (\"a\", \"b\", \"c\") ." "text/turtle" "http://example.org")
 ```
 
 ### Serializing a string
@@ -39,7 +39,6 @@ def main : IO Unit := do
     ⟪_:"b0", #⟨"http://example.org/predicate"⟩, (1:)⟫,
     ⟪_:"b0", #⟨"http://example.org/predicate"⟩, "hello"⟫,
     ⟪_:"b0", #⟨"http://example.org/predicate"⟩, "hello"@"en"⟫,
-    ⟪_:"b0", #⟨"http://example.org/predicate"⟩, "hello"@"en"⟫,
-  ]
+  ] ++ ⟪_:"b0", #⟨"http://example.org/predicate"⟩, ["a", "b", "c"]⟫
   IO.println $ RDFSerialize triples "text/turtle"
 ```