~james/remy

feat(frontend): report token offsets for parse failures

commit
9a908c16a977ca9df2dada000c4243ea210d427b browse tree
parent
a0e486f13b8e3c62454c0192400c1ca5d86a581e
author
james <j@cpl0.zip>
signature
Verified ~james signed with a key registered by ~james
date
2026-09-27 11:00 UTC

3 files changed, +65 −5

src/Examples.thy modified

@@ -113,4 +113,12 @@ lemma comment_tokens:
113113 "lex (''(+ x; ignore ) tokens'' @ newline @ ''y) ; end'') [] [] = [''('', ''+'', ''x'', ''y'', '')'']"
114114 by eval
115115
116+lemma missing_operand_offset:
117+ "source_error ''(+ x)'' = ''syntax error at token 3'' @ newline"
118+ by eval
119+
120+lemma trailing_token_offset:
121+ "source_error ''(+ x y) 1'' = ''syntax error at token 5'' @ newline"
122+ by eval
123+
116124 end

src/Frontend.thy modified

@@ -153,8 +153,57 @@ termination by (relation "measure id") (auto simp: div_less_dividend)
153153
154154 definition newline :: string where "newline = [CHR 0x0A]"
155155
156+datatype problem = Unexpected nat | Exhausted nat
157+
158+datatype 'a outcome = Failed problem | Parsed 'a
159+
160+fun parsed_bind :: "'a outcome \<Rightarrow> ('a \<Rightarrow> 'b outcome) \<Rightarrow> 'b outcome" where
161+ "parsed_bind (Failed p) f = Failed p"
162+| "parsed_bind (Parsed x) f = f x"
163+
164+fun close_at :: "expression \<Rightarrow> string list \<Rightarrow> nat \<Rightarrow> (expression \<times> string list \<times> nat) outcome" where
165+ "close_at e [] pos = Failed (Unexpected pos)"
166+| "close_at e (s # rest) pos = (if s = '')'' then Parsed (e,rest,Suc pos) else Failed (Unexpected pos))"
167+
168+lemma close_at_cursor:
169+ "close_at e tokens pos = Parsed (a,rest,nextpos) \<Longrightarrow> a = e \<and> nextpos = Suc pos"
170+ by (cases tokens) (auto split: if_splits)
171+
172+function diagnose :: "nat \<Rightarrow> string list \<Rightarrow> string list \<Rightarrow> nat \<Rightarrow>
173+ (expression \<times> string list \<times> nat) outcome" where
174+ "diagnose fuel names tokens pos = (if fuel = 0 then Failed (Exhausted pos)
175+ else case tokens of [] \<Rightarrow> Failed (Unexpected pos) | s # rest \<Rightarrow>
176+ if s \<noteq> ''('' then (case atom names s of None \<Rightarrow> Failed (Unexpected pos)
177+ | Some e \<Rightarrow> Parsed (e,rest,Suc pos))
178+ else case rest of [] \<Rightarrow> Failed (Unexpected (Suc pos)) | op # args \<Rightarrow>
179+ if op = ''let'' then (case args of [] \<Rightarrow> Failed (Unexpected (pos + 2)) | name # body \<Rightarrow>
180+ if \<not> valid_name name then Failed (Unexpected (pos + 2)) else
181+ parsed_bind (diagnose (fuel - 1) names body (pos + 3)) (\<lambda>(a,tail,nextpos).
182+ parsed_bind (diagnose (fuel - 1) (name # names) tail nextpos) (\<lambda>(b,tail,lastpos).
183+ close_at (Let a b) tail lastpos)))
184+ else if op = ''if'' then
185+ parsed_bind (diagnose (fuel - 1) names args (pos + 2)) (\<lambda>(c,tail,nextpos).
186+ parsed_bind (diagnose (fuel - 1) names tail nextpos) (\<lambda>(a,tail,nextpos).
187+ parsed_bind (diagnose (fuel - 1) names tail nextpos) (\<lambda>(b,tail,lastpos).
188+ close_at (Cond c a b) tail lastpos)))
189+ else case operator op of None \<Rightarrow> Failed (Unexpected (Suc pos)) | Some f \<Rightarrow>
190+ parsed_bind (diagnose (fuel - 1) names args (pos + 2)) (\<lambda>(a,tail,nextpos).
191+ parsed_bind (diagnose (fuel - 1) names tail nextpos) (\<lambda>(b,tail,lastpos).
192+ close_at (Binary f a b) tail lastpos)))"
193+ by pat_completeness auto
194+termination by (relation "measure (\<lambda>(fuel,names,tokens,pos). fuel)") auto
195+
196+declare diagnose.simps [simp del]
197+
198+definition source_error :: "string \<Rightarrow> string" where
199+ "source_error s = (case diagnose 128 [] (lex s [] []) 0 of
200+ Failed (Unexpected pos) \<Rightarrow> ''syntax error at token '' @ decimal pos @ newline
201+ | Failed (Exhausted pos) \<Rightarrow> ''invalid source or resource limit'' @ newline
202+ | Parsed (e,rest,pos) \<Rightarrow> if rest \<noteq> [] then ''syntax error at token '' @ decimal pos @ newline
203+ else ''invalid source or resource limit'' @ newline)"
204+
156205 definition artifact :: "string \<Rightarrow> (bool \<times> string) \<times> string" where
157- "artifact s = (case prepare s of None \<Rightarrow> ((False,[]), ''invalid source or resource limit'' @ newline)
206+ "artifact s = (case prepare s of None \<Rightarrow> ((False,[]), source_error s)
158207 | Some e \<Rightarrow> let opt = optimise e; bytes = executable e in
159208 ((True, map char_of_nat bytes), decimal (nodes e) @ '' nodes -> '' @ decimal (nodes opt) @
160209 '' nodes, '' @ decimal (length bytes) @ '' bytes, '' @ decimal (demand opt) @ '' stack words'' @ newline))"
@@ -171,13 +220,13 @@ definition row :: "expression \<Rightarrow> nat \<Rightarrow> nat list" where
171220 [sample i X, sample i Y, sample i T, evaluate e [] (sample i)])"
172221
173222 definition vectors :: "string \<Rightarrow> bool \<times> string" where
174- "vectors s = (case prepare s of None \<Rightarrow> (False, ''invalid source or resource limit'' @ newline)
223+ "vectors s = (case prepare s of None \<Rightarrow> (False, source_error s)
175224 | Some e \<Rightarrow> (True, map char_of_nat (concat (map (row e) [0..<512]))))"
176225
177226 definition reference :: "string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> bool \<times> string" where
178- "reference source x y t = (case (prepare source, number x, number y, number t) of
179- (Some e,Some a,Some b,Some c) \<Rightarrow>
227+ "reference source x y t = (case prepare source of None \<Rightarrow> (False,source_error source) | Some e \<Rightarrow>
228+ case (number x, number y, number t) of (Some a,Some b,Some c) \<Rightarrow>
180229 (True, decimal (unat (evaluate e [] (\<lambda>v. word_of_nat (case v of X \<Rightarrow> a | Y \<Rightarrow> b | T \<Rightarrow> c)))) @ newline)
181- | _ \<Rightarrow> (False,''invalid source or input'' @ newline))"
230+ | _ \<Rightarrow> (False,''invalid input'' @ newline))"
182231
183232 end

tests/cli.py modified

@@ -29,6 +29,9 @@ def main():
2929 for text in ['(+ x; ignore ) tokens\ny) ; end', '(+ x; comment\r\ny)', '(+ x y);end']:
3030 source.write_text(text)
3131 assert int(invoke('eval',source,'3','4','0')) == 7, text
32+ for text, position in [('(+ x)',3),('(div x y)',1),('(let a 3 b)',4),('(+ x y',4),('(+ x y) 1',5)]:
33+ source.write_text(text)
34+ assert f'token {position}\n' in invoke(source,binary,ok=False), text
3235 for text in ['0x','0x10000000000000000','0xfg','0xffextra','-0x1']:
3336 source.write_text(text)
3437 binary.write_bytes(b'preserve')