mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-07-04 16:46:28 +03:00
fix equalSimilar not following described algo
This commit is contained in:
parent
981b8afe90
commit
057c8d51de
1
.gitignore
vendored
1
.gitignore
vendored
|
@ -6,3 +6,4 @@ plans.txt
|
|||
demo/
|
||||
.fill.tmp
|
||||
.check.hs
|
||||
guide.txt
|
||||
|
|
|
@ -1,5 +1,17 @@
|
|||
Equal.apply A B (f: ∀(x:A) B) (a: A) (b: A) (e: (Equal A a b))
|
||||
: (Equal B (f a) (f b))
|
||||
= match e {
|
||||
Equal.refl: (Equal.refl _ _)
|
||||
use Equal.{refl}
|
||||
|
||||
apply A B (f: ∀(x:A) B) (a: A) (b: A) (e: (Equal A a b)) : (Equal B (f a) (f b)) =
|
||||
match e {
|
||||
refl: {=}
|
||||
}
|
||||
|
||||
//Equal.apply
|
||||
//: ∀(A: *)
|
||||
//∀(B: *)
|
||||
//∀(f: ∀(x: A) B)
|
||||
//∀(a: A)
|
||||
//∀(b: A)
|
||||
//∀(e: (Equal A a b))
|
||||
//(Equal B (f a) (f b))
|
||||
//= λA λB λf λa λb λe
|
||||
//(e λx (Equal B (f a) (f x)) λP λx x)
|
||||
|
|
|
@ -1,8 +1,7 @@
|
|||
List.concat
|
||||
: ∀(T: *) ∀(xs: (List T)) ∀(ys: (List T)) (List T)
|
||||
= λT λxs λys
|
||||
use P = λxs ∀(ys: (List T)) (List T)
|
||||
use cons = λhead λtail λys
|
||||
(List.cons T head (List.concat T tail ys))
|
||||
use nil = λys ys
|
||||
(~xs P cons nil ys)
|
||||
use List.{cons,nil}
|
||||
|
||||
concat (T: *) (xs: (List T)) (ys: (List T)) : (List T) =
|
||||
match xs {
|
||||
cons: (cons T xs.head (concat T xs.tail ys))
|
||||
nil: ys
|
||||
}
|
||||
|
|
7
book/Nat.add.kind2
Normal file
7
book/Nat.add.kind2
Normal file
|
@ -0,0 +1,7 @@
|
|||
use Nat.{succ,zero}
|
||||
|
||||
add (a: Nat) (b: Nat) : Nat =
|
||||
match a {
|
||||
succ: (succ (add a.pred b))
|
||||
zero: b
|
||||
}
|
|
@ -1,16 +1,33 @@
|
|||
Nat.lemma.bft
|
||||
: ∀(n: Nat) (Equal Nat (Nat.half (Nat.double n)) n)
|
||||
= λn
|
||||
(~n
|
||||
λx (Equal Nat (Nat.half (Nat.double x)) x)
|
||||
λn
|
||||
(Equal.apply
|
||||
Nat
|
||||
Nat
|
||||
Nat.succ
|
||||
(Nat.half (Nat.double n))
|
||||
n
|
||||
(Nat.lemma.bft n)
|
||||
)
|
||||
λP λa a
|
||||
)
|
||||
use Nat.{succ,zero,half,double}
|
||||
|
||||
bft (n: Nat) : (Equal Nat (half (double n)) n) =
|
||||
match n {
|
||||
succ:
|
||||
let ind = (bft n.pred)
|
||||
let prf = (Equal.apply Nat Nat succ (half (double n.pred)) n.pred ind)
|
||||
prf
|
||||
zero: {=}
|
||||
}
|
||||
|
||||
//#found{a
|
||||
//(((Equal (_)) (Nat.succ {n.pred: Nat})) (Nat.half (Nat.double {(Nat.succ {n.pred: Nat}): Nat})))
|
||||
//[
|
||||
//{n: Nat}
|
||||
//λn (((Equal (_)) n) (Nat.half (Nat.double {n: Nat})))
|
||||
//{n.pred: Nat}
|
||||
//{ind: (((Equal (_)) (Nat.half (Nat.double n.pred))) n.pred)}
|
||||
//]}
|
||||
|
||||
//(~n
|
||||
//λx (Equal Nat (Nat.half (Nat.double x)) x)
|
||||
//λn
|
||||
//(Equal.apply
|
||||
//Nat
|
||||
//Nat
|
||||
//Nat.succ
|
||||
//(Nat.half (Nat.double n))
|
||||
//n
|
||||
//(Nat.lemma.bft n)
|
||||
//)
|
||||
//λP λa a
|
||||
//)
|
||||
|
|
22
book/Vector.concat.kind2
Normal file
22
book/Vector.concat.kind2
Normal file
|
@ -0,0 +1,22 @@
|
|||
use Vector.{cons,nil}
|
||||
use Nat.{succ,zero,add}
|
||||
|
||||
concat T (xs_len: Nat) (ys_len: Nat)
|
||||
(xs: (Vector T xs_len))
|
||||
(ys: (Vector T ys_len))
|
||||
: (Vector T (add xs_len ys_len))
|
||||
= match xs {
|
||||
cons : (cons T (add xs.len ys_len) xs.head (concat T xs.len ys_len xs.tail ys))
|
||||
nil : ys
|
||||
}
|
||||
|
||||
//concat
|
||||
//: ∀(T: *)
|
||||
//∀(xs_len: Nat) ∀(xs: (Vector T xs_len))
|
||||
//∀(ys_len: Nat) ∀(ys: (Vector T ys_len))
|
||||
//(Vector T (add xs_len ys_len))
|
||||
//= λT λxs_len λxs λys_len λys
|
||||
//(~xs _
|
||||
//λxs.len λxs.head λxs.tail
|
||||
//(Vector.cons T (Nat.add xs.len ys_len) xs.head (concat T xs.len xs.tail ys_len ys))
|
||||
//ys)
|
|
@ -5,7 +5,7 @@
|
|||
//use Nat.{succ,zero}
|
||||
|
||||
_main : Nat =
|
||||
(Nat.add 1 2)
|
||||
(Nat.half (Nat.double 3))
|
||||
|
||||
|
||||
//_main (a: Nat) (b: Nat) (e: (Equal A a b)) : (Equal A a b) =
|
||||
|
|
4
formal/README.md
Normal file
4
formal/README.md
Normal file
|
@ -0,0 +1,4 @@
|
|||
Kind2's Formal Verification!
|
||||
----------------------------
|
||||
|
||||
Here, we verify the soundness and consistency of Kind2's Core.
|
1
formal/kind2.agda
Normal file
1
formal/kind2.agda
Normal file
|
@ -0,0 +1 @@
|
|||
-- TODO :D
|
|
@ -362,7 +362,7 @@ termSimilar (All aNam aInp aBod) (All bNam bInp bBod) dep = do
|
|||
termSimilar (Lam aNam aBod) (Lam bNam bBod) dep =
|
||||
termEqual (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1)
|
||||
termSimilar (App aFun aArg) (App bFun bArg) dep = do
|
||||
eFun <- termEqual aFun bFun dep
|
||||
eFun <- termSimilar aFun bFun dep
|
||||
eArg <- termEqual aArg bArg dep
|
||||
envPure (eFun && eArg)
|
||||
termSimilar (Slf aNam aTyp aBod) (Slf bNam bTyp bBod) dep =
|
||||
|
@ -381,7 +381,7 @@ termSimilar (Mat aNam aX aZ aS aP) (Mat bNam bX bZ bS bP) dep = do
|
|||
eS <- termEqual (aS (Var (stringConcat aNam "-1") dep)) (bS (Var (stringConcat bNam "-1") dep)) dep
|
||||
eP <- termEqual (aP (Var aNam dep)) (bP (Var bNam dep)) dep
|
||||
envPure (eX && eZ && eS && eP)
|
||||
termSimilar a b dep = envPure False
|
||||
termSimilar a b dep = termIdentical a b dep
|
||||
|
||||
termIdentical :: Term -> Term -> Int -> Env Bool
|
||||
termIdentical a b dep = termIdenticalGo a b dep
|
||||
|
|
|
@ -333,12 +333,12 @@ impl Term {
|
|||
// - (EQUAL a b) ::= (App (App (App (Var "Equal") _) a) b)
|
||||
pub fn as_equal(&self) -> Option<Equal> {
|
||||
match self {
|
||||
Term::App { fun, arg } => {
|
||||
if let Term::App { fun: eq_fun, arg: rhs } = &**fun {
|
||||
Term::App { fun, arg: rhs } => {
|
||||
if let Term::App { fun: eq_fun, arg: lhs } = &**fun {
|
||||
if let Term::App { fun: eq_fun, arg: _ } = &**eq_fun {
|
||||
if let Term::Var { nam } = &**eq_fun {
|
||||
if nam == "Equal" {
|
||||
return Some(Equal { a: (**arg).clone(), b: (**rhs).clone() });
|
||||
return Some(Equal { a: (**lhs).clone(), b: (**rhs).clone() });
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -403,7 +403,6 @@ impl Term {
|
|||
|
||||
// Interprets a λ-encoded Algebraic Data Type definition as an ADT struct.
|
||||
pub fn as_adt(&self) -> Option<ADT> {
|
||||
|
||||
let name: String;
|
||||
let pvar: String;
|
||||
|
||||
|
@ -538,12 +537,12 @@ impl Term {
|
|||
let mut self_type = Term::Var { nam: adt.name.clone() };
|
||||
|
||||
// Then appends each type parameter
|
||||
for par in adt.pars.iter().rev() {
|
||||
for par in adt.pars.iter() {
|
||||
self_type = Term::App { fun: Box::new(self_type), arg: Box::new(Term::Var { nam: par.clone() }) };
|
||||
}
|
||||
|
||||
// And finally appends each index
|
||||
for (idx_name, _) in adt.idxs.iter().rev() {
|
||||
for (idx_name, _) in adt.idxs.iter() {
|
||||
self_type = Term::App { fun: Box::new(self_type), arg: Box::new(Term::Var { nam: idx_name.clone() }) };
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in New Issue
Block a user