repos / temple.lean4.git

Syntax.lean

  1import Parser
  2
  3namespace TempleSyntax
  4
  5inductive Term
  6| text : String -> Term
  7| var : String -> Term
  8| op : String -> List String -> Term
  9| forloop : String -> String -> List Term -> Term
 10deriving BEq, Repr, Inhabited
 11
 12partial instance : ToString Term where
 13  toString :=
 14    let rec toStr x :=
 15      have : ToString Term := ⟨toStr⟩
 16      match x with
 17      | .text t => "\"" ++ t ++ "\""
 18      | .var name => "{{ " ++ name ++ " }}"
 19      | .op name args => "{% " ++ name ++ " " ++ (String.join $ args.intersperse " ") ++ " %}"
 20      | .forloop var collection body =>
 21        "{% for " ++ var ++ " in " ++ collection ++ " %}\n"
 22          ++ (String.join $ List.intersperse "\n" $ body.map toStr)
 23          ++ "\n{% endfor %}"
 24    toStr
 25
 26abbrev TempleParser := SimpleParser Substring Char
 27
 28namespace TempleParser
 29open Parser Char
 30
 31@[inline] def spaces : TempleParser Unit :=
 32  withErrorMessage "<spaces>" do
 33    dropMany (char ' ')
 34
 35@[inline] def spaces1 : TempleParser Unit :=
 36  withErrorMessage "<spaces1>" do
 37    dropMany1 (char ' ')
 38
 39partial def textInner (acc : String) : TempleParser String :=
 40  withErrorMessage "<text>" do
 41    try
 42      let savePos <- getPosition
 43      match <- option? (chars "{{" <|> chars "{%") with
 44        | some _ => do
 45          setPosition savePos
 46          return acc
 47        | none => do
 48          let c <- anyToken
 49          textInner $ String.push acc c
 50    catch _ => return acc
 51
 52@[inline] partial def text : TempleParser Term :=
 53  withErrorMessage "<text>" do
 54    let t <- textInner ""
 55    if t == "" then throwUnexpected else return Term.text t
 56
 57@[inline] def name : TempleParser String :=
 58  withErrorMessage "<name>" do
 59    foldl String.push "" $ ASCII.alphanum <|> char '_'
 60
 61@[inline] def var : TempleParser Term :=
 62  withErrorMessage "<var>" do
 63    let n <- spaces *> chars "{{" *> spaces *> name <* spaces <* chars "}}"
 64    return Term.var n
 65
 66@[inline] def op : TempleParser Term :=
 67  withErrorMessage "<op>" do
 68    let n <- spaces *> chars "{%" *> spaces *> name
 69    let firstArg <- spaces1 *> name
 70    let args <- spaces1 *> (sepBy1 spaces1 name) <* spaces <* chars "%}"
 71    return Term.op n (List.cons firstArg $ args.toList.filter (fun a => !a.isEmpty))
 72
 73mutual
 74  partial def forloop : TempleParser Term :=
 75    withErrorMessage "<forloop>" do
 76      let _ <- chars "{%" *> spaces *> chars "for"
 77      let v <- spaces1 *> name <* spaces1 <* chars "in"
 78      let collection <- spaces1 *> name <* spaces <* chars "%}"
 79
 80      let parsedTerms <- terms
 81
 82      let _ <- chars "{%" *> spaces *> chars "endfor" *> spaces <* chars "%}"
 83      return Term.forloop v collection parsedTerms
 84
 85  partial def terms : TempleParser (List Term) :=
 86    withErrorMessage "<term>" do
 87      let t <- withErrorMessage "<term>: expected terms"
 88        $ takeMany $ forloop <|> op <|> var <|> text
 89      return t.toList
 90end
 91
 92end TempleParser
 93
 94def parse (input : String) : IO (List Term) :=
 95  match (TempleParser.terms <* Parser.endOfInput).run input.toSubstring with
 96  | .ok _ t => return t
 97  | .error _ e => throw $ IO.userError s!"Parsing error: {e}"
 98
 99section Test
100
101#eval! show IO Bool from do
102  let t <- parse "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{»  æыв{ { {  }} { % { { {фыÔ¨ÍÓÎÓˆd"
103  return t == [.text "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{»  æыв{ { {  }} { % { { {фыÔ¨ÍÓÎÓˆd"]
104
105#eval! show IO Bool from do
106  let t <- parse "{{ myVariable }}"
107  return t == [.var "myVariable"]
108
109#eval! show IO Bool from do
110  let t <- parse "hello {{ myVariable }}"
111  return t == [.text "hello ", .var "myVariable"]
112
113#eval! show IO Bool from do
114  let t <- parse "{% my_operator s   d %}"
115  return t == [.op "my_operator" [ "s", "d" ]]
116
117#eval! show IO Bool from do
118  let t <- parse "{% for    x     in      fruits %}sadasd{{hello}}{% endfor %}"
119  return t == [.forloop "x" "fruits" [ .text "sadasd", .var "hello" ]]
120
121#eval! show IO Bool from do
122  let t <- parse "{% for x in fruits %}hello{% for y in fruits %}world{{x}}{{y}}{% endfor %}good{% endfor %}"
123  return t == [.forloop "x" "fruits"
124    [ .text "hello", .forloop "y" "fruits" [ .text "world", .var "x", .var "y" ], .text "good" ]]
125
126end Test
127
128end TempleSyntax