HigherOrderCO/Kind
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind.git synced 2024-10-05 19:27:30 +03:00
Code Issues Packages Projects Releases Wiki Activity

improve errors

Browse Source
This commit is contained in:
Victor Taelin 2024-03-01 12:13:31 -03:00
parent fdbc3d013c
commit 37f9c47e98
3 changed files with 36 additions and 122 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

142
book/.check.hvm1
View File

File diff suppressed because one or more lines are too long

14
src/kind2.hvm1
View File

@ -541,7 +541,7 @@
(Checker.bind (Check 0 arg fun_typ.inp dep) λvty
(Checker.pure (fun_typ.bod arg)))
λfun λarg
(Checker.fail (Error 0 fun_typ (All "x" (Hol "_" []) (Hol "_" [])) (App fun arg) dep)))
(Checker.fail (Error 0 fun_typ (Hol "function" []) (App fun arg) dep)))
fun arg))
(Infer.match (Ann val typ) dep) =
(Checker.pure typ)
@ -577,17 +577,17 @@
(Checker.bind (Check 0 (s (Ann (Var (String.concat nam "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (String.concat nam "-1") dep))) (+ dep 1)) λs_typ
(Checker.pure (p x))))))
(Infer.match (Lam nam bod) dep) =
(Checker.fail (Error 0 (Hol "" []) (All "x" (Hol "_" []) (Hol "_" [])) (Lam nam bod) dep))
(Checker.fail (Error 0 (Hol "untyped_term" []) (Hol "type_annotation" []) (Lam nam bod) dep))
(Infer.match (Let nam val bod) dep) =
(Checker.fail (Error 0 (Hol "" []) (Hol "type" []) (Let nam val bod) dep))
(Checker.fail (Error 0 (Hol "untyped_term" []) (Hol "type_annotation" []) (Let nam val bod) dep))
(Infer.match (Hol nam ctx) dep) =
(Checker.fail (Error 0 (Hol "" []) (Hol "type" []) (Hol nam ctx) dep))
(Checker.fail (Error 0 (Hol "untyped_term" []) (Hol "type_annotation" []) (Hol nam ctx) dep))
(Infer.match (Met nam (Some val)) dep) =
(Infer.match val dep)
(Infer.match (Met nam None) dep) =
(Checker.fail (Error 0 (Hol "" []) (Hol "type" []) (Met nam None) dep))
(Checker.fail (Error 0 (Hol "untyped_term" []) (Hol "type_annotation" []) (Met nam None) dep))
(Infer.match (Var nam idx) dep) =
(Checker.fail (Error 0 (Hol "" []) (Hol "type" []) (Var nam idx) dep))
(Checker.fail (Error 0 (Hol "untyped_term" []) (Hol "type_annotation" []) (Var nam idx) dep))
(Infer.match (Src src val) dep) =
(Infer.match val dep)
@ -750,7 +750,7 @@
(Message.show (Error src detected expected value dep)) =
let det = (Show (Normal 1 detected dep) dep)
let exp = (Show (Normal 1 expected dep) dep)
let val = (Show (Normal 1 value dep) dep)
let val = (Show (Normal 0 value dep) dep)
(String.join ["#error{" exp " " det " " val " " (U60.show src) "}"])
(Message.show (Solve name term dep)) =
let term = (Show (Normal 1 term dep) dep)

2
src/main.rs
View File

@ -326,7 +326,7 @@ impl Message {
let exp = format!("- expected: \x1b[32m{}\x1b[0m", exp.show());
let det = format!("- detected: \x1b[31m{}\x1b[0m", det.show());
let bad = format!("- bad_term: \x1b[2m{}\x1b[0m", bad.show());
let file = book.get_file_name(src_fid(*src)).unwrap_or_else(|| "unknown".to_string());
let file = book.get_file_name(src_fid(*src)).unwrap_or_else(|| "unknown_file".to_string());
let text = std::fs::read_to_string(&file).unwrap_or_else(|_| "Could not read source file.".to_string());
let orig = highlight_error(src_ini(*src) as usize, src_end(*src) as usize, &text);
let src = format!("\x1b[4m{}\x1b[0m\n{}", file, orig);