From 981b8afe90a5ae3669f8c7bcca98190e66d89458 Mon Sep 17 00:00:00 2001 From: Victor Taelin Date: Thu, 14 Mar 2024 00:21:21 -0300 Subject: [PATCH] fix unchecked let --- book/Bool.match.kind2 | 12 ++++----- book/Char.equal.kind2 | 5 ++-- book/Char.escapes.kind2 | 53 +++++++++----------------------------- book/Char.is_between.kind2 | 8 +++--- book/Char.is_blank.kind2 | 5 ++-- book/Char.is_decimal.kind2 | 5 ++-- book/Char.is_name.kind2 | 4 ++- book/_main.kind2 | 28 +++++++++++--------- src/kind2.hs | 2 +- src/term/parse.rs | 5 ++-- 10 files changed, 49 insertions(+), 78 deletions(-) diff --git a/book/Bool.match.kind2 b/book/Bool.match.kind2 index bafb918d..35ec9b02 100644 --- a/book/Bool.match.kind2 +++ b/book/Bool.match.kind2 @@ -1,7 +1,7 @@ Bool.match -: ∀(b: Bool) - ∀(P: ∀(x: Bool) *) - ∀(t: (P Bool.true)) - ∀(f: (P Bool.false)) - (P b) -= λb λP λt λf (~b P t f) + (b: Bool) + (P: ∀(x: Bool) *) + (t: (P Bool.true)) + (f: (P Bool.false)) +: (P b) += (~b P t f) diff --git a/book/Char.equal.kind2 b/book/Char.equal.kind2 index ffa49dd4..23e2b3a4 100644 --- a/book/Char.equal.kind2 +++ b/book/Char.equal.kind2 @@ -1,3 +1,2 @@ -Char.equal -: ∀(a: Char) ∀(b: Char) Bool -= U60.equal \ No newline at end of file +Char.equal (a: Char) (b: Char) : Bool = + (U60.equal a b) diff --git a/book/Char.escapes.kind2 b/book/Char.escapes.kind2 index 602fbed2..e5056b87 100644 --- a/book/Char.escapes.kind2 +++ b/book/Char.escapes.kind2 @@ -1,43 +1,14 @@ Char.escapes : (List (Pair Char Char)) -= (List.cons - (Pair Char Char) - (Pair.new Char Char #98 #8) - (List.cons - (Pair Char Char) - (Pair.new Char Char #102 #12) - (List.cons - (Pair Char Char) - (Pair.new Char Char #110 #10) - (List.cons - (Pair Char Char) - (Pair.new Char Char #114 #13) - (List.cons - (Pair Char Char) - (Pair.new Char Char #116 #9) - (List.cons - (Pair Char Char) - (Pair.new Char Char #118 #11) - (List.cons - (Pair Char Char) - (Pair.new Char Char #92 #92) - (List.cons - (Pair Char Char) - (Pair.new Char Char #34 #34) - (List.cons - (Pair Char Char) - (Pair.new Char Char #48 #0) - (List.cons - (Pair Char Char) - (Pair.new Char Char #39 #39) - (List.nil (Pair Char Char)) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) \ No newline at end of file += [ + (Pair.new _ _ #98 #8) + (Pair.new _ _ #102 #12) + (Pair.new _ _ #110 #10) + (Pair.new _ _ #114 #13) + (Pair.new _ _ #116 #9) + (Pair.new _ _ #118 #11) + (Pair.new _ _ #92 #92) + (Pair.new _ _ #34 #34) + (Pair.new _ _ #48 #0) + (Pair.new _ _ #39 #39) +] diff --git a/book/Char.is_between.kind2 b/book/Char.is_between.kind2 index 1e1b9305..0216c672 100644 --- a/book/Char.is_between.kind2 +++ b/book/Char.is_between.kind2 @@ -1,7 +1,5 @@ -Char.is_between -: ∀(min: Char) ∀(max: Char) ∀(chr: Char) Bool -= λmin λmax λchr - (Bool.and +Char.is_between (min: Char) (max: Char) (chr: Char) : Bool += (Bool.and (U60.to_bool #(>= chr min)) (U60.to_bool #(<= chr max)) - ) \ No newline at end of file + ) diff --git a/book/Char.is_blank.kind2 b/book/Char.is_blank.kind2 index 2e1cc40c..716da4e7 100644 --- a/book/Char.is_blank.kind2 +++ b/book/Char.is_blank.kind2 @@ -1,3 +1,2 @@ -Char.is_blank -: ∀(a: Char) Bool -= λa (Bool.or (Char.equal a #10) (Char.equal a #32)) \ No newline at end of file +Char.is_blank (a: Char) : Bool = + (Bool.or (Char.equal a #10) (Char.equal a #32)) diff --git a/book/Char.is_decimal.kind2 b/book/Char.is_decimal.kind2 index 4ce61aa4..7d1c9ed6 100644 --- a/book/Char.is_decimal.kind2 +++ b/book/Char.is_decimal.kind2 @@ -1,3 +1,2 @@ -Char.is_decimal -: ∀(a: Char) Bool -= λa (Char.is_between #48 #57 a) \ No newline at end of file +Char.is_decimal (a: Char) : Bool = + (Char.is_between #48 #57 a) diff --git a/book/Char.is_name.kind2 b/book/Char.is_name.kind2 index a23b07a4..7443b782 100644 --- a/book/Char.is_name.kind2 +++ b/book/Char.is_name.kind2 @@ -16,4 +16,6 @@ Char.is_name ) ) ) - ) \ No newline at end of file + ) + + diff --git a/book/_main.kind2 b/book/_main.kind2 index e5c3f0b3..f625d8c5 100644 --- a/book/_main.kind2 +++ b/book/_main.kind2 @@ -2,19 +2,23 @@ //| cons (len: Nat) (head: A) (tail: (Vector A len)) : (Vector A (Nat.succ len)) //| nil : (Vector A Nat.zero) -use Nat.{succ,zero} +//use Nat.{succ,zero} -_main (a: Nat) (b: Nat) (e: (Equal A a b)) : (Equal A a b) = - match a { - succ: match b { - succ: e - zero: e - } - zero: match b { - succ: e - zero: ?D - } - } +_main : Nat = + (Nat.add 1 2) + + +//_main (a: Nat) (b: Nat) (e: (Equal A a b)) : (Equal A a b) = + //match a { + //succ: match b { + //succ: e + //zero: e + //} + //zero: match b { + //succ: e + //zero: ?D + //} + //} //λa λb λe //use a.P = _ diff --git a/src/kind2.hs b/src/kind2.hs index 1b510bec..d453b253 100644 --- a/src/kind2.hs +++ b/src/kind2.hs @@ -655,8 +655,8 @@ termCheckGo src (Hol termNam termCtx) typx dep = do termCheckGo src (Met uid spn) typx dep = do return () termCheckGo src (Ann chk val typ) typx dep = do + termCheckCompare src val typ typx dep if chk then do - termCheckCompare src val typ typx dep termCheck src val typ dep else do return () diff --git a/src/term/parse.rs b/src/term/parse.rs index 816b7c4f..aa2db94b 100644 --- a/src/term/parse.rs +++ b/src/term/parse.rs @@ -1,6 +1,5 @@ use crate::{*}; - impl<'i> KindParser<'i> { pub fn parse_oper(&mut self) -> Result { @@ -76,9 +75,9 @@ impl<'i> KindParser<'i> { val: Box::new(Term::App { fun: Box::new(Term::App { fun: Box::new(Term::Var { nam: "Equal.refl".to_string() }), - arg: Box::new(Term::Met {}) + arg: Box::new(Term::Met {}), }), - arg: Box::new(Term::Met {}) + arg: Box::new(Term::Met {}), }) }); }