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