nandi.uk
This repository has no description
1namespace Mlang.Nickel
2
3inductive Term where
4 | null : Term
5 | bool : Bool → Term
6 | int : Int → Term
7 | string : String → Term
8 | array : List Term → Term
9 | record : List (String × Term) → Term
10 deriving Repr, Inhabited, BEq
11
12abbrev ParseM := Except String
13abbrev Input := List Char
14
15def charsToString (chars : List Char) : String :=
16 String.ofList chars
17
18def isDigit (c : Char) : Bool :=
19 '0' <= c && c <= '9'
20
21def isIdentStart (c : Char) : Bool :=
22 c.isAlpha || c = '_'
23
24def isIdentContinue (c : Char) : Bool :=
25 isIdentStart c || isDigit c || c = '-'
26
27partial def skipSpace : Input → Input
28 | c :: rest => if c.isWhitespace then skipSpace rest else c :: rest
29 | [] => []
30
31partial def spanChars (p : Char → Bool) : Input → List Char × Input
32 | [] => ([], [])
33 | c :: rest =>
34 if p c then
35 let (taken, tail) := spanChars p rest
36 (c :: taken, tail)
37 else
38 ([], c :: rest)
39
40def consumeChar (expected : Char) : Input → ParseM Input
41 | c :: rest =>
42 if c = expected then pure rest
43 else throw s!"expected '{expected}', got '{c}'"
44 | [] => throw s!"expected '{expected}', got end of input"
45
46partial def takeStringChars : Input → ParseM (List Char × Input)
47 | [] => throw "unterminated string literal"
48 | '"' :: rest => pure ([], rest)
49 | '\\' :: '"' :: rest => do
50 let (chars, tail) ← takeStringChars rest
51 pure ('"' :: chars, tail)
52 | '\\' :: '\\' :: rest => do
53 let (chars, tail) ← takeStringChars rest
54 pure ('\\' :: chars, tail)
55 | '\\' :: 'n' :: rest => do
56 let (chars, tail) ← takeStringChars rest
57 pure ('\n' :: chars, tail)
58 | c :: rest => do
59 let (chars, tail) ← takeStringChars rest
60 pure (c :: chars, tail)
61
62def parseString (input : Input) : ParseM (String × Input) := do
63 let input ← consumeChar '"' input
64 let (chars, rest) ← takeStringChars input
65 pure (charsToString chars, rest)
66
67def parseInt (input : Input) : ParseM (Int × Input) := do
68 let (sign, rest) :=
69 match input with
70 | '-' :: tail => ("-", tail)
71 | _ => ("", input)
72 let (digits, rest) := spanChars isDigit rest
73 if digits.isEmpty then
74 throw "expected integer literal"
75 else
76 match String.toInt? (sign ++ charsToString digits) with
77 | some n => pure (n, rest)
78 | none => throw "invalid integer literal"
79
80def parseIdent (input : Input) : ParseM (String × Input) := do
81 match input with
82 | c :: rest =>
83 if isIdentStart c then
84 let (tailChars, tail) := spanChars isIdentContinue rest
85 pure (charsToString (c :: tailChars), tail)
86 else
87 throw s!"expected identifier, got '{c}'"
88 | [] => throw "expected identifier, got end of input"
89
90mutual
91 partial def parseTerm (input : Input) : ParseM (Term × Input) := do
92 let input := skipSpace input
93 match input with
94 | [] => throw "expected Nickel term"
95 | '"' :: _ =>
96 let (s, rest) ← parseString input
97 pure (.string s, rest)
98 | '[' :: rest =>
99 parseArray rest
100 | '{' :: rest =>
101 parseRecord rest
102 | 't' :: _ | 'f' :: _ | 'n' :: _ =>
103 let (name, rest) ← parseIdent input
104 match name with
105 | "true" => pure (.bool true, rest)
106 | "false" => pure (.bool false, rest)
107 | "null" => pure (.null, rest)
108 | _ => throw s!"unexpected identifier '{name}'"
109 | '-' :: _ =>
110 let (n, rest) ← parseInt input
111 pure (.int n, rest)
112 | c :: _ =>
113 if isDigit c then
114 let (n, rest) ← parseInt input
115 pure (.int n, rest)
116 else
117 throw s!"unexpected character '{c}'"
118
119 partial def parseArray (input : Input) : ParseM (Term × Input) := do
120 let input := skipSpace input
121 if let ']' :: rest := input then
122 pure (.array [], rest)
123 else
124 let (first, rest) ← parseTerm input
125 parseArrayTail [first] rest
126
127 partial def parseArrayTail (items : List Term) (input : Input) : ParseM (Term × Input) := do
128 let input := skipSpace input
129 match input with
130 | ']' :: rest => pure (.array items.reverse, rest)
131 | ',' :: rest => do
132 let (next, rest) ← parseTerm rest
133 parseArrayTail (next :: items) rest
134 | c :: _ => throw s!"expected ',' or ']', got '{c}'"
135 | [] => throw "unterminated array"
136
137 partial def parseRecord (input : Input) : ParseM (Term × Input) := do
138 let input := skipSpace input
139 if let '}' :: rest := input then
140 pure (.record [], rest)
141 else
142 let (key, rest) ← parseFieldKey input
143 let rest := skipSpace rest
144 let rest ← consumeChar '=' rest
145 let (value, rest) ← parseTerm rest
146 parseRecordTail [(key, value)] rest
147
148 partial def parseRecordTail (fields : List (String × Term)) (input : Input) : ParseM (Term × Input) := do
149 let input := skipSpace input
150 match input with
151 | '}' :: rest => pure (.record fields.reverse, rest)
152 | ',' :: rest => do
153 let (key, rest) ← parseFieldKey rest
154 let rest := skipSpace rest
155 let rest ← consumeChar '=' rest
156 let (value, rest) ← parseTerm rest
157 parseRecordTail ((key, value) :: fields) rest
158 | c :: _ => throw s!"expected ',' or '}}', got '{c}'"
159 | [] => throw "unterminated record"
160
161 partial def parseFieldKey (input : Input) : ParseM (String × Input) := do
162 let input := skipSpace input
163 match input with
164 | '"' :: _ => parseString input
165 | _ => parseIdent input
166end
167
168def parse (source : String) : ParseM Term := do
169 let (term, rest) ← parseTerm source.toList
170 let rest := skipSpace rest
171 if rest.isEmpty then
172 pure term
173 else
174 throw s!"unexpected trailing input: {charsToString rest}"
175
176partial def render : Term → String
177 | .null => "null"
178 | .bool true => "true"
179 | .bool false => "false"
180 | .int n => toString n
181 | .string s => s!"\"{s}\""
182 | .array xs =>
183 "[" ++ String.intercalate ", " (xs.map render) ++ "]"
184 | .record fields =>
185 let rendered := fields.map (fun (k, v) => s!"{k} = {render v}")
186 "{ " ++ String.intercalate ", " rendered ++ " }"
187
188end Mlang.Nickel