repos / temple.lean4.git

Eval.lean

 1import Init.System.IO
 2
 3import Temple.Syntax
 4import Temple.DeBruijn
 5import Temple.DeBruijnEval
 6
 7namespace TempleEval
 8
 9open IO.FS
10
11open TempleDeBruijnEval
12
13def runStringWith (c : UserContext) (s : String) : IO String := do
14  let terms <- TempleSyntax.parse s
15  let deBruijnTerms := List.map TempleDeBruijn.fromSyntaxTerm terms
16  let results <- deBruijnTerms.mapM $ TempleDeBruijnEval.eval c
17  return String.join results
18
19@[inline] def runString (s : String) : IO String := runStringWith { } s
20
21@[inline] def runWith (c : UserContext) (fn : System.FilePath) : IO String := do
22  let s <- IO.FS.readFile fn
23  runStringWith c s
24
25@[inline] def run (fn : System.FilePath) : IO String := do
26  let s <- IO.FS.readFile fn
27  runString s
28
29section Test
30
31#eval show IO String from
32  runStringWith {} "hello"
33
34#eval show IO String from
35  runStringWith { data := Std.HashMap.ofList [ ("world", .text "world") ] } "hello {{ world }}"
36
37#eval show IO String from
38  runStringWith { data := Std.HashMap.ofList [ ("world", .text "world"), ("xs", .list $ [ "1", "2", "3" ].map .text ) ] }
39    "hello {{ world }}
40
41    {% for x in xs %}
42      #{{ x }}
43    {% endfor %}
44    "
45
46#eval show IO String from
47  let dataItems := Std.HashMap.ofList
48        [ ("world", .text "world")
49        , ("xs", .list $ [ "1", "2", "3" ].map .text )
50        , ("ys", .list $ [ "4", "5", "6" ].map .text )
51        ]
52  runStringWith { data := dataItems }
53    "hello {{ world }}
54{% for x in xs %}
55  {% for y in ys %}#{{ x }} {{y}} {% endfor %}
56{% endfor %}"
57
58#eval show IO String from
59  let dataItems := Std.HashMap.ofList
60        [ ("world", .text "world")
61        , ("xs", .list $ [ .text "1", .list [ .text "2", .text "3"], .text "4" ] )
62        ]
63  runStringWith { data := dataItems }
64    "hello {{ world }}
65{% for x in xs %}
66  {% for y in x %}#{{ x }}{{y}} {% endfor %}
67{% endfor %}"
68
69#eval show IO String from
70  let dataItems := Std.HashMap.ofList
71        [ ("world", .text "world")
72        , ("xs", .list [ .text "hello", .text "world"] )
73        ]
74
75  runStringWith { data := dataItems }
76    "hello {{ world }}
77{% for x in xs %}
78  {% toUpper x %}
79{% endfor %}"
80
81end Test
82
83end TempleEval