HigherOrderCO/Kind
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind.git synced 2024-08-16 22:00:46 +03:00
Code Issues Packages Projects Releases Wiki Activity

use compiled GHC checker only

Browse Source
This commit is contained in:
Victor Taelin 2024-06-22 23:00:56 -03:00
parent 80e3ff76c2
commit 314aaeee1c
35 changed files with 1501 additions and 3256 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
.gitignore vendored
View File

@ -10,3 +10,10 @@ demo/
guide.txt
.hvm
.hvm/
-e
# Compiled Haskell files
*.hi
*.o
-e
# Hidden files
.*

68
Cargo.lock generated
View File

@ -95,12 +95,45 @@ version = "0.7.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "98cc8fbded0c607b7ba9dd60cd98df59af97e84d24e49c8557331cfc26d301ce"
[[package]]
name = "cok"
version = "0.1.10"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5db78a7c258c3747ffe44f7ae428f04f7170f2bd5b1eb94a1ac8e59637f2165e"
dependencies = [
"doe",
"json",
]
[[package]]
name = "colorchoice"
version = "1.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7"
[[package]]
name = "doe"
version = "0.1.84"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8272b55c803e9dacfaf99376663c2a418d0314b2d10bf7867cb7aee394abf2ff"
[[package]]
name = "easy_file"
version = "0.1.20"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "433be7f574726e20abb3be988ddd2b6ba785cf46a2e0cd5fbd7a1055edd8dbe5"
[[package]]
name = "ghc"
version = "0.1.13"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "c13ab5284e48662282c570eaaef082bbf6bf9342af1b4e69c8bcea7c9411907f"
dependencies = [
"cok",
"easy_file",
"walkdir",
]
[[package]]
name = "highlight_error"
version = "0.1.1"
@ -121,12 +154,19 @@ dependencies = [
"version_check",
]
[[package]]
name = "json"
version = "0.12.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "078e285eafdfb6c4b434e0d31e8cfcb5115b651496faca5749b88fafd4f23bfd"
[[package]]
name = "kind2"
version = "0.1.0"
dependencies = [
"TSPL",
"clap",
"ghc",
"highlight_error",
"im",
]
@ -146,6 +186,15 @@ dependencies = [
"rand_core",
]
[[package]]
name = "same-file"
version = "1.0.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "93fc1dc3aaa9bfed95e02e6eadabb4baf7e3078b0bd1b4d7b6b0b68378900502"
dependencies = [
"winapi-util",
]
[[package]]
name = "sized-chunks"
version = "0.6.5"
@ -180,6 +229,25 @@ version = "0.9.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f"
[[package]]
name = "walkdir"
version = "2.5.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "29790946404f91d9c5d06f9874efddea1dc06c5efe94541a7d6863108e3a5e4b"
dependencies = [
"same-file",
"winapi-util",
]
[[package]]
name = "winapi-util"
version = "0.1.8"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4d4cc384e1e73b93bafa6fb4f1df8c41695c8a91cf9c4c64358067d15a7b6c6b"
dependencies = [
"windows-sys",
]
[[package]]
name = "windows-sys"
version = "0.52.0"

8
Cargo.toml
View File

@ -2,13 +2,21 @@
name = "kind2"
version = "0.1.0"
edition = "2021"
default-run = "kind2"
[[bin]]
name = "kind2"
path = "src/main.rs"
[[bin]]
name = "kindc"
path = "src/kindc.rs"
[dependencies]
TSPL = "0.0.9"
highlight_error = "0.1.1"
im = "15.1.0"
clap = "4.5.2"
[build-dependencies]
ghc = "0.1.0"

17
book/Bool/match.kind2
View File

@ -6,19 +6,4 @@ match
(t: (P true))
(f: (P false))
: (P b)
= (~b λx(_) t f)
//(x λk(_) t f) : (P b)
//x : (P: Bool -> *) (t: (P T)) (f: (P F)) (P x)
//_ : Bool -> *
//t : (λk(_) T) == P true
//f : (λk(_) F) == P false
//(λk(_) x) == (P x)
//_ x == P x
= (~b P t f)

2
book/HVM/load.kind2
View File

@ -5,4 +5,4 @@ load <A> (file: String) (cont: String -> A) : A =
//HVM.load
//: ∀(A: *) ∀(file: String) ∀(cont: ∀(x: String) A) A
//= λA λfile λcont (cont String.nil)
//= λA λfile λcont (cont String/nil)

2
book/Kind/Book/String/cons.kind2
View File

@ -1,3 +1,3 @@
Kind.Book.String.cons
Kind.Book.String/cons
: Kind.Term
= (Kind.hol "TODO" (List.nil Kind.Term))

2
book/Kind/Book/String/nil.kind2
View File

@ -1,3 +1,3 @@
Kind.Book.String.nil
Kind.Book.String/nil
: Kind.Term
= (Kind.hol "TODO" (List.nil Kind.Term))

4
book/Kind/reduce/txt.kind2
View File

@ -6,9 +6,9 @@ Kind.reduce.txt
(Kind.reduce
Bool.true
(Kind.app
(Kind.app Kind.Book.String.cons (Kind.num x))
(Kind.app Kind.Book.String/cons (Kind.num x))
(Kind.txt xs)
)
)
use nil = (Kind.reduce Bool.true Kind.Book.String.nil)
use nil = (Kind.reduce Bool.true Kind.Book.String/nil)
(~txt P cons nil)

8
book/List/match.kind2 Normal file
View File

@ -0,0 +1,8 @@
match <A>
(P: (List A) -> *)
(c: ∀(head: A) ∀(tail: (List A)) (P (List/cons/ A head tail)))
(n: (P (List/nil/ A)))
(xs: (List A))
: (P xs) =
(~xs P c n)

10
book/List/reverse.kind2 Normal file
View File

@ -0,0 +1,10 @@
use List/{cons,nil}
List/reverse/go <A> (list: (List A)) (result: (List A)) : (List A) =
match list {
nil: result
cons: (List/reverse/go list.tail (List/cons list.head result))
}
reverse <A> (list: (List A)) : (List A) =
(List/reverse/go list [])

2
book/Nat/add.kind2
View File

@ -2,6 +2,6 @@ use Nat/{succ,zero}
add (a: Nat) (b: Nat) : Nat =
match a {
succ: (succ (add a.pred b))
succ: (succ (add a.pred a))
zero: b
}

15
book/Nat/lemma/bft.kind2
View File

@ -1,7 +1,16 @@
use Nat/{succ,zero,half,double}
bft (n: Nat) : (half (double n)) == n =
bft (n: Nat) : (Equal Nat (half (double n)) n) =
match n {
succ: (Equal/apply succ (bft n.pred))
zero: {=}
succ:
let ind = (bft n.pred)
(~ind λaλbλx(Equal Nat (succ a) (succ b))
λa (Equal/refl/ Nat (succ a)))
//match ind {
//Equal/refl: ?a
//}
//let prf = (Equal/apply succ ind)
//?a
zero:
{=}
}

3
book/Nat/match.kind2 Normal file
View File

@ -0,0 +1,3 @@
match (P: Nat -> *) (s: ∀(pred: Nat) (P (Nat/succ pred))) (z: (P Nat/zero)) (n: Nat) : (P n) =
(~n P s z)

4
book/Parser/is_eof.kind2
View File

@ -5,8 +5,8 @@ Parser.is_eof
use cons = λcode.head λcode.tail
(Parser.Result.done
Bool
(String.cons code.head code.tail)
(String/cons code.head code.tail)
Bool.false
)
use nil = (Parser.Result.done Bool String.nil Bool.true)
use nil = (Parser.Result.done Bool String/nil Bool.true)
(~(String.skip code) P cons nil)

8
book/Parser/pick_while/go.kind2
View File

@ -8,15 +8,15 @@ Parser.pick_while.go
use true = λhead λtail
use P = λx (Parser.Result String)
use done = λcode λvalue
(Parser.Result.done String code (String.cons head value))
(Parser.Result.done String code (String/cons head value))
use fail = λerror (Parser.Result.fail String error)
(~(Parser.pick_while.go cond tail) P done fail)
use false = λhead λtail
(Parser.Result.done
String
(String.cons head tail)
String.nil
(String/cons head tail)
String/nil
)
(~(cond head) P true false head tail)
use nil = (Parser.Result.done String String.nil String.nil)
use nil = (Parser.Result.done String String/nil String/nil)
(~code P cons nil)

6
book/Parser/test.kind2
View File

@ -13,7 +13,7 @@ Parser.test
use done = λcode λvalue
(Parser.Result.done
Bool
(String.cons code.head code)
(String/cons code.head code)
value
)
use fail = λerror (Parser.Result.fail Bool error)
@ -21,7 +21,7 @@ Parser.test
use false = λcode.head λcode.tail
(Parser.Result.done
Bool
(String.cons code.head code.tail)
(String/cons code.head code.tail)
Bool.false
)
(~(Char.equal test.head code.head)
@ -31,7 +31,7 @@ Parser.test
code.head
code.tail
)
use nil = (Parser.Result.done Bool String.nil Bool.false)
use nil = (Parser.Result.done Bool String/nil Bool.false)
(~code P cons nil)
use nil = λcode (Parser.Result.done Bool code Bool.true)
(~test P cons nil code)

2
book/String/cons.kind2
View File

@ -1,2 +1,2 @@
String.cons (head: Char) (tail: String) : String =
String/cons (head: Char) (tail: String) : String =
~λP λcons λnil (cons head tail)

2
book/String/nil.kind2
View File

@ -1,2 +1,2 @@
String.nil : String =
String/nil : String =
~λP λcons λnil nil

2
book/String/quote.kind2
View File

@ -1,3 +1,3 @@
String.quote
: String
= (String.cons 34 String.nil)
= (String/cons 34 String/nil)

2
book/U60/name/go.kind2
View File

@ -4,7 +4,7 @@ U60.name.go
switch n = n {
0: λnil nil
_: λnil
(String.cons
(String/cons
(+ 97 (% n-1 26))
(U60.name.go (/ n-1 26) nil)
)

14
book/_tmp.hvm2
View File

@ -1,14 +0,0 @@
_Char = 0
_List = λ_T 0
_List.cons = λ_T λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
_List.map = λ_A λ_B λ_xs let _xs.P = 0 let _xs.cons = λ_xs.head λ_xs.tail λ_f (((_List.cons 0) (_f _xs.head)) ((((_List.map 0) 0) _xs.tail) _f)) let _xs.nil = λ_f (_List.nil 0) (((_xs _xs.P) _xs.cons) _xs.nil)
_List.nil = λ_T λ_P λ_cons λ_nil _nil
_Nat = 0
_Nat.succ = λ_n λ_P λ_succ λ_zero (_succ _n)
_Nat.zero = λ_P λ_succ λ_zero _zero
_String = (_List _Char)
_String.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
_String.nil = λ_P λ_cons λ_nil _nil
main = (_List.map (_List.cons 0 1 (_List.cons 0 2 (_List.nil 0))) λx(+ x 10))

19
book/_tmp.kind2
View File

@ -1,19 +0,0 @@
WARNING: unsolved metas.
WARNING: unsolved metas.
WARNING: unsolved metas.
WARNING: unsolved metas.
WARNING: unsolved metas.
_Char = 0
_List = λ_T 0
_List.cons = λ_T λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
_List.map = λ_A λ_B λ_xs let _xs.P = 0 let _xs.cons = λ_xs.head λ_xs.tail λ_f (((_List.cons 0) (_f _xs.head)) ((((_List.map 0) 0) _xs.tail) _f)) let _xs.nil = λ_f (_List.nil 0) (((_xs _xs.P) _xs.cons) _xs.nil)
_List.nil = λ_T λ_P λ_cons λ_nil _nil
_Nat = 0
_Nat.succ = λ_n λ_P λ_succ λ_zero (_succ _n)
_Nat.zero = λ_P λ_succ λ_zero _zero
_String = (_List _Char)
_String.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
_String.nil = λ_P λ_cons λ_nil _nil
main = _List.map

5
book/main.kind2 Normal file
View File

@ -0,0 +1,5 @@
use Nat/{succ,zero}
main : (List U60) =
let list = [10, 20]
list

2
book/test0.kind2
View File

@ -9,4 +9,4 @@ test0
∀(b: B)
A
= λA λB λaa λab λba λbb λa λb
(ba (ab (aa (aa b))))
(ba (ab (aa a)))

2
book/test4.kind2
View File

@ -1,3 +1,3 @@
test4
: String
= (~"abc" λx String λh λt t String.nil)
= (~"abc" λx String λh λt t String/nil)

19
build.rs Normal file
View File

@ -0,0 +1,19 @@
use std::process::Command;
use std::env;
//use std::path::Path;
fn main() {
let out_dir = env::current_dir().unwrap();
let dest_path = out_dir.join("target").join("kindc");
let status = Command::new("ghc")
.args(&["-O2", "-o", dest_path.to_str().unwrap(), "src/kindc.hs"])
.status()
.expect("Failed to execute GHC");
if !status.success() {
panic!("GHC compilation failed");
}
println!("cargo:rerun-if-changed=src/kindc.hs");
}

44
src/book/compile.rs
View File

@ -2,43 +2,6 @@ use crate::{*};
impl Book {
pub fn to_hvm1_checker(&self) -> String {
todo!()
//let mut used = BTreeSet::new();
//let mut code = String::new();
//for (name, term) in &self.defs {
//let metas = term.count_metas();
//let mut lams = String::new();
//for i in 0 .. term.count_metas() {
//lams = format!("{} λ_{}", lams, i);
//}
//let subs = (0 .. metas).map(|h| format!("(Pair \"{}\" None)", h)).collect::<Vec<_>>().join(",");
//code.push_str(&format!("Book.{} = (Ref \"{}\" [{}] {}{})\n", name, name, subs, lams, term.to_hvm1(im::Vector::new(), &mut 0)));
//used.insert(name.clone());
//}
//code
}
pub fn to_hvm2_checker(&self) -> String {
let mut code = String::new();
let mut meta = 0;
for (name, term) in &self.defs {
let expr = term.to_hvm2_checker(im::Vector::new(), &mut meta);
code.push_str(&format!("Book.{} = (Ref \"{}\" {})\n", name.replace("/", "."), name, expr));
}
code
}
pub fn to_hs_checker(&self) -> String {
let mut code = String::new();
let mut meta = 0;
for (name, term) in &self.defs {
let expr = term.to_hs_checker(im::Vector::new(), &mut meta);
code.push_str(&format!("{} = (Ref \"{}\" {})\n", Term::to_hs_name(name), name, expr));
}
code
}
pub fn to_hvm2(&self) -> String {
let mut code = String::new();
for (name, term) in &self.defs {
@ -47,4 +10,11 @@ impl Book {
code
}
pub fn to_kindc(&self) -> String {
let mut code = String::new();
for (name, term) in &self.defs {
code.push_str(&format!("{} = {};\n", name, term.to_kindc(&mut 0)));
}
code
}
}

1006
src/kind2.hs
View File

File diff suppressed because it is too large Load Diff

898
src/kind2.hvm1
View File

@ -1,898 +0,0 @@
// Types
// -----
//data Maybe
//= (Some value)
//| None
//data Bool
//= False
//| True
//data Pair
//= (Pair fst snd)
//data Term
//= (All nam inp bod)
//| (Lam nam bod)
//| (App fun arg)
//| (Ann val typ)
//| (Slf nam typ bod)
//| (Ins val)
//| (Ref nam sub val)
//| (Let nam val bod)
//| (Set)
//| (U60)
//| (Num val)
//| (Op2 opr fst snd)
//| (Mat nam x z s p)
//| (Txt txt)
//| (Hol nam ctx)
//| (Var nam idx)
//| (Src src val)
// Prelude
// -------
(U60.seq 0 cont) = (cont 0)
(U60.seq n cont) = (cont n)
(String.seq (String.cons x xs) cont) = (U60.seq x λx(String.seq xs λxs(cont (String.cons x xs))))
(String.seq String.nil cont) = (cont String.nil)
(Print dep [] value) = value
(Print dep msg value) = (String.seq (String.join msg) λstr(HVM.log str value))
//(Print dep [] value) = value
//(Print dep msg value) = (If (> dep 10) 1 (HVM.print (String.join msg) value))
(NewLine) = (String.cons 10 String.nil)
(Quote) = (String.cons 34 String.nil)
(And True b) = b
(And False b) = False
(Or True b) = True
(Or False b) = b
(If 0 t f) = f
(If n t f) = t
(When None some none) = none
(When (Some val) some none) = (some val)
(U60.show n) = (U60.show.go n String.nil)
(U60.show.go n res) = (U60.show.go.match (< n 10) n res)
(U60.show.go.match 0 n res) = (U60.show.go (/ n 10) (String.cons (+ '0' (% n 10)) res))
(U60.show.go.match i n res) = (String.cons (+ '0' n) res)
(U60.name n) = (U60.name.go (+ n 1))
(U60.name.go 0) = ""
(U60.name.go n) = (String.cons (+ 97 (% (- n 1) 26)) (U60.name.go (/ (- n 1) 26)))
(Same String.nil String.nil) = 1
(Same String.nil (String.cons y ys)) = 0
(Same (String.cons x xs) String.nil) = 0
(Same (String.cons x xs) (String.cons y ys)) = (& (== x y) (Same xs ys))
(Find name List.nil) = None
(Find name (List.cons (Pair nam val) tail)) = (If (Same nam name) (Some val) (Find name tail))
(List.map f (List.cons x xs)) = (List.cons (f x) (List.map f xs))
(List.map f List.nil) = List.nil
(String.concat String.nil ys) = ys
(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys))
(String.join List.nil) = ""
(String.join (List.cons x xs)) = (String.concat x (String.join xs))
(String.tail String.nil) = String.nil
(String.tail (String.cons x xs)) = xs
(Pair.fst (Pair fst snd)) = fst
(Pair.snd (Pair fst snd)) = snd
(Pair.get (Pair fst snd) fun) = (fun fst snd)
(Maybe.match (Some value) some none) = (some value)
(Maybe.match None some none) = none
(Maybe.pure x) = (Some x)
(Maybe.bind a b) = (Maybe.match a λvalue(b value) None)
// Converts an U60 to a bitstring
(U60.to_bits 0) = E
(U60.to_bits 1) = (I E)
(U60.to_bits n) = (If (== (% n 2) 0) (O (U60.to_bits (/ n 2))) (I (U60.to_bits (/ n 2))))
(String.color RESET) = (String.cons 27 "[0m")
(String.color BRIGHT) = (String.cons 27 "[1m")
(String.color DIM) = (String.cons 27 "[2m")
(String.color UNDERSCORE) = (String.cons 27 "[4m")
(String.color BLINK) = (String.cons 27 "[5m")
(String.color REVERSE) = (String.cons 27 "[7m")
(String.color HIDDEN) = (String.cons 27 "[8m")
(String.color BLACK) = (String.cons 27 "[30m")
(String.color RED) = (String.cons 27 "[31m")
(String.color GREEN) = (String.cons 27 "[32m")
(String.color YELLOW) = (String.cons 27 "[33m")
(String.color BLUE) = (String.cons 27 "[34m")
(String.color MAGENTA) = (String.cons 27 "[35m")
(String.color CYAN) = (String.cons 27 "[36m")
(String.color WHITE) = (String.cons 27 "[37m")
(String.color GRAY) = (String.cons 27 "[90m")
(String.color BG_BLACK) = (String.cons 27 "[40m")
(String.color BG_RED) = (String.cons 27 "[41m")
(String.color BG_GREEN) = (String.cons 27 "[42m")
(String.color BG_YELLOW) = (String.cons 27 "[43m")
(String.color BG_BLUE) = (String.cons 27 "[44m")
(String.color BG_MAGENTA) = (String.cons 27 "[45m")
(String.color BG_CYAN) = (String.cons 27 "[46m")
(String.color BG_WHITE) = (String.cons 27 "[47m")
(String.color BG_GRAY) = (String.cons 27 "[100m")
(String.color x) = "?"
// BitsMap
// -------
(Map.new) = List.nil
(Map.has eq k (List.cons (Pair key val) map)) = (If (eq key k) 1 (Map.has eq k map))
(Map.has eq k List.nil) = 0
(Map.ins eq k v (List.cons (Pair key val) map)) = ((If (eq key k) λmap(None) λmap(Maybe.bind (Map.ins eq k v map) λmap(Some (List.cons (Pair key val) map)))) map)
(Map.ins eq k v List.nil) = (Some (List.cons (Pair k v) List.nil))
(Map.set eq k v (List.cons (Pair key val) map)) = ((If (eq key k) λmap(List.cons (Pair k v) map) λmap(List.cons (Pair key val) (Map.set eq k v map))) map)
(Map.set eq k v List.nil) = (List.cons (Pair k v) List.nil)
(Map.get eq k (List.cons (Pair key val) map)) = (If (eq key k) (Some val) (Map.get eq k map))
(Map.get eq k List.nil) = None
// data BM A = BM.leaf | (BM.node A BM BM)
// Returns true if value is present on BM
(BM.has E (BM.node (Some val) lft rgt)) = 1
(BM.has (O bits) (BM.node val lft rgt)) = (BM.has bits lft)
(BM.has (I bits) (BM.node val lft rgt)) = (BM.has bits rgt)
(BM.has key val) = 0
// Gets a value from a BM
(BM.get E (BM.leaf)) = None
(BM.get E (BM.node val lft rgt)) = val
(BM.get (O bits) (BM.leaf)) = None
(BM.get (O bits) (BM.node val lft rgt)) = (BM.get bits lft)
(BM.get (I bits) (BM.leaf)) = None
(BM.get (I bits) (BM.node val lft rgt)) = (BM.get bits rgt)
// Sets a value on a BM
(BM.set E val (BM.leaf)) = (BM.node (Some val) BM.leaf BM.leaf)
(BM.set E val (BM.node _ lft rgt)) = (BM.node (Some val) lft rgt)
(BM.set (O bits) val (BM.leaf)) = (BM.node None (BM.set bits val BM.leaf) BM.leaf)
(BM.set (O bits) val (BM.node v lft rgt)) = (BM.node v (BM.set bits val lft) rgt)
(BM.set (I bits) val (BM.leaf)) = (BM.node None BM.leaf (BM.set bits val BM.leaf))
(BM.set (I bits) val (BM.node v lft rgt)) = (BM.node v lft (BM.set bits val rgt))
// Map wrapper with U60 keys
(U60.Map.new) = BM.leaf
(U60.Map.has key map) = (BM.has (U60.to_bits key) map)
(U60.Map.get key map) = (BM.get (U60.to_bits key) map)
(U60.Map.set key val map) = (BM.set (U60.to_bits key) val map)
// Holes
// -----
(Subst (List.cons (Pair nam None) subs) val) = (Subst subs (val None))
(Subst (List.cons (Pair nam (Some x)) subs) val) = (Subst subs (val (Some x)))
(Subst List.nil val) = val
// Evaluation
// ----------
// Evaluation levels:
// - 0: reduces refs never
// - 1: reduces refs on redexes
// - 2: reduces refs always
(Reduce lv (App fun arg)) = (Reduce.app lv (Reduce lv fun) arg)
(Reduce lv (Ann val typ)) = (Reduce lv val)
(Reduce lv (Ins val)) = (Reduce lv val)
(Reduce lv (Ref nam sub val)) = (Reduce.ref lv nam sub (Reduce lv val))
(Reduce lv (Let nam val bod)) = (Reduce lv (bod val))
(Reduce lv (Op2 opr fst snd)) = (Reduce.op2 lv opr (Reduce lv fst) (Reduce lv snd))
(Reduce lv (Mat nam x z s p)) = (Reduce.mat lv nam (Reduce lv x) z s p)
(Reduce lv (Txt txt)) = (Reduce.txt lv txt)
(Reduce lv (Src src val)) = (Reduce lv val)
(Reduce lv val) = val
(Reduce.app 2 (Ref _ _ val) arg) = (Reduce.app 2 val arg) // FIXME: should this be here? (no.)
(Reduce.app 1 (Ref _ _ val) arg) = (Reduce.app 1 val arg) // FIXME: should this be here? (no.)
(Reduce.app lv (Lam nam bod) arg) = (Reduce lv (bod (Reduce 0 arg)))
(Reduce.app lv fun arg) = (App fun arg)
(Reduce.op2 1 op (Ref _ _ x) (Num snd)) = (Reduce.op2 1 op x snd)
(Reduce.op2 2 op (Ref _ _ x) (Num snd)) = (Reduce.op2 2 op x snd)
(Reduce.op2 1 op (Num fst) (Ref _ _ x)) = (Reduce.op2 1 op fst x)
(Reduce.op2 2 op (Num fst) (Ref _ _ x)) = (Reduce.op2 2 op fst x)
(Reduce.op2 lv ADD (Num fst) (Num snd)) = (Num (+ fst snd))
(Reduce.op2 lv SUB (Num fst) (Num snd)) = (Num (- fst snd))
(Reduce.op2 lv MUL (Num fst) (Num snd)) = (Num (* fst snd))
(Reduce.op2 lv DIV (Num fst) (Num snd)) = (Num (/ fst snd))
(Reduce.op2 lv MOD (Num fst) (Num snd)) = (Num (% fst snd))
(Reduce.op2 lv EQ (Num fst) (Num snd)) = (Num (== fst snd))
(Reduce.op2 lv NE (Num fst) (Num snd)) = (Num (!= fst snd))
(Reduce.op2 lv LT (Num fst) (Num snd)) = (Num (< fst snd))
(Reduce.op2 lv GT (Num fst) (Num snd)) = (Num (> fst snd))
(Reduce.op2 lv LTE (Num fst) (Num snd)) = (Num (<= fst snd))
(Reduce.op2 lv GTE (Num fst) (Num snd)) = (Num (>= fst snd))
(Reduce.op2 lv AND (Num fst) (Num snd)) = (Num (& fst snd))
(Reduce.op2 lv OR (Num fst) (Num snd)) = (Num (| fst snd))
(Reduce.op2 lv XOR (Num fst) (Num snd)) = (Num (^ fst snd))
(Reduce.op2 lv LSH (Num fst) (Num snd)) = (Num (<< fst snd))
(Reduce.op2 lv RSH (Num fst) (Num snd)) = (Num (>> fst snd))
(Reduce.op2 lv opr fst snd) = (Op2 opr fst snd)
(Reduce.mat 2 nam (Ref _ _ x) z s p) = (Reduce.mat 2 nam x z s p)
(Reduce.mat 1 nam (Ref _ _ x) z s p) = (Reduce.mat 1 nam x z s p)
(Reduce.mat lv nam (Num 0) z s p) = (Reduce lv z)
(Reduce.mat lv nam (Num n) z s p) = (Reduce lv (s (Num (- n 1))))
(Reduce.mat lv nam (Op2 ADD (Num 1) k) z s p) = (Reduce lv (s k))
(Reduce.mat lv nam val z s p) = (Mat nam val z s p)
(Reduce.ref 2 nam sub val) = (Reduce 2 (Subst sub val))
(Reduce.ref 1 nam sub val) = (Ref nam sub val)
(Reduce.ref lv nam sub val) = (Ref nam sub val)
//(Reduce.met lv nam None) = (Met nam None)
//(Reduce.met lv nam (Some x)) = (Reduce lv x)
(Reduce.txt lv (String.cons x xs)) = (Reduce lv (App (App Book.String.cons (Num x)) (Txt xs)))
(Reduce.txt lv String.nil) = (Reduce lv Book.String.nil)
(Reduce.txt lv val) = (Txt val)
(Normal lv term dep) = (Normal.go lv (Normal.prefer (Reduce 0 term) (Reduce lv term)) dep)
(Normal.prefer soft (Lam _ _)) = soft
(Normal.prefer soft (Slf _ _ _)) = soft
(Normal.prefer soft (All _ _ _)) = soft
(Normal.prefer soft hard) = hard
(Normal.go lv (All nam inp bod) dep) = (All nam (Normal lv inp dep) λx(Normal lv (bod (Var nam dep)) (+ dep 1)))
(Normal.go lv (Lam nam bod) dep) = (Lam nam λx(Normal lv (bod (Var nam dep)) (+ 1 dep)))
(Normal.go lv (App fun arg) dep) = (App (Normal lv fun dep) (Normal lv arg dep))
(Normal.go lv (Ann val typ) dep) = (Ann (Normal lv val dep) (Normal lv typ dep))
(Normal.go lv (Slf nam typ bod) dep) = (Slf nam typ λx(Normal lv (bod (Var nam dep)) (+ 1 dep)))
(Normal.go lv (Ins val) dep) = (Ins (Normal lv val dep))
(Normal.go lv (Ref nam sub val) dep) = (Ref nam sub (Normal lv val dep))
(Normal.go lv (Let nam val bod) dep) = (Let nam (Normal lv val dep) λx(Normal lv (bod (Var nam dep)) (+ 1 dep)))
(Normal.go lv (Hol nam ctx) dep) = (Hol nam ctx)
(Normal.go lv (Met uid) dep) = (Met uid)
(Normal.go lv Set dep) = Set
(Normal.go lv U60 dep) = U60
(Normal.go lv (Num val) dep) = (Num val)
(Normal.go lv (Op2 opr fst snd) dep) = (Op2 opr (Normal lv fst dep) (Normal lv snd dep))
(Normal.go lv (Mat nam x z s p) dep) = (Mat nam (Normal lv x dep) (Normal lv z dep) λk(Normal lv (s (Var (String.concat nam "-1") dep)) dep) λk(Normal lv (p (Var nam dep)) dep))
(Normal.go lv (Txt val) dep) = (Txt val)
(Normal.go lv (Var nam idx) dep) = (Var nam idx)
(Normal.go lv (Src src val) dep) = (Src src (Normal lv val dep))
// Checker
// -------
// type Result A = (Done Fill Logs A) | (Fail Fill Logs String)
// type Checker A = Fill -> Logs -> (Result A)
(Result.match (Done fill logs value) done fail) = (done fill logs value)
(Result.match (Fail fill logs error) done fail) = (fail fill logs error)
//(State.get fill got) = (got fill logs)
//(State.new) = []
(Checker.bind a b) = λfill λlogs (Result.match (a fill logs) λfillλlogsλvalue((b value) fill logs) λfillλlogsλerror(Fail fill logs error))
(Checker.pure a) = λfill λlogs (Done fill logs a)
(Checker.fail e) = λfill λlogs (Fail fill logs e)
(Checker.run chk) = (chk [] BM.leaf)
(Checker.log msg) = λfill λlogs (Done fill (List.cons msg logs) 1)
(Checker.save) = λfill λlogs
(Done fill logs (Pair fill logs))
(Checker.load (Pair fill logs)) =
λ_ λ_ (Done fill logs 0)
// Equality
// --------
// The conversion checkers works as follows:
// - 1. If the two sides are structurally identical, they're equal.
// - 2. Otherwise, reduce both sides.
// - 3. If the two sides are structurally identical, they're equal.
// - 4. Otherwise, recurse on both sides and check if all fields are equal.
// This algorithm will return true when both sides reduce to the same normal
// form, but it will halt early if both sides become identical at any point
// during the reduction, allowing checking recursive terms. This is enough to
// cover any interesting term. Note we need to be careful with self-types, which
// must be "un-unrolled" to avoid loops. Read `docs/equality.md` for more info.
// Checks if two term are equal
(Equal a b dep) =
//(Print dep ["Equal: " NewLine "- " (Show a dep) NewLine "- " (Show b dep)]
(Compare a b dep
let a = (Reduce 2 a)
let b = (Reduce 2 b)
(Compare a b dep
(Similar a b dep)))
// Checks if two terms are structurally identical
// If yes, returns 1 (identical) or 2 (suspended)
// If not, undoes effects (logs, unifications, etc.)
(Compare a b dep else) =
(Checker.bind (Checker.save) λstate
(Checker.bind (Identical a b dep) λequal
(If equal
(Checker.pure equal)
(Checker.bind (Checker.load state) λx (else)))))
// Checks if all components of a term are equal
(Similar (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) =
(Checker.bind (Equal a.inp b.inp dep) λe.inp
(Checker.bind (Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)) λe.bod
(Checker.pure (& e.inp e.bod))))
(Similar (Lam a.nam a.bod) (Lam b.nam b.bod) dep) =
(Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
(Similar (App a.fun a.arg) (App b.fun b.arg) dep) =
(Checker.bind (Equal a.fun b.fun dep) λe.fun
(Checker.bind (Equal a.arg b.arg dep) λe.arg
(Checker.pure (& e.fun e.arg))))
(Similar (Slf a.nam a.typ a.bod) (Slf b.nam b.typ b.bod) dep) =
(Similar (Reduce 0 a.typ) (Reduce 0 b.typ) dep) // <- must call Similar, NOT Equal
(Similar (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) =
(Checker.pure (Same a.nam b.nam))
(Similar (Met a.uid) (Met b.uid) dep) =
(Checker.pure (== a.uid b.uid))
(Similar (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) =
(Checker.bind (Equal a.fst b.fst dep) λe.fst
(Checker.bind (Equal a.snd b.snd dep) λe.snd
(Checker.pure (& e.fst e.snd))))
(Similar (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) =
(Checker.bind (Equal a.x b.x dep) λe.x
(Checker.bind (Equal a.z b.z dep) λe.z
(Checker.bind (Equal (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) λe.s
(Checker.bind (Equal (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep) λe.p
(Checker.pure (& e.x (& e.z (& e.s e.p))))))))
(Similar a b dep) =
(Checker.pure 0)
// Checks if two terms are structurally identical
(Identical a b dep) =
//(Print dep ["Identical?" NewLine "- " (Show a dep) NewLine "- " (Show b dep)]
(Unify.try b a dep
(Unify.try a b dep
(Identical.go a b dep)))
(Identical.go (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) =
(Checker.bind (Identical a.inp b.inp dep) λi.inp
(Checker.bind (Identical (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)) λi.bod
(Checker.pure (& i.inp i.bod))))
(Identical.go (Lam a.nam a.bod) (Lam b.nam b.bod) dep) =
(Identical (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
(Identical.go (App a.fun a.arg) (App b.fun b.arg) dep) =
(Checker.bind (Identical a.fun b.fun dep) λi.fun
(Checker.bind (Identical a.arg b.arg dep) λi.arg
(Checker.pure (& i.fun i.arg))))
(Identical.go (Slf a.nam a.typ a.bod) (Slf b.nam b.typ b.bod) dep) =
(Identical a.typ b.typ dep)
(Identical.go (Ins a.val) b dep) =
(Identical a.val b dep)
(Identical.go a (Ins b.val) dep) =
(Identical a b.val dep)
(Identical.go (Let a.nam a.val a.bod) b dep) =
(Identical (a.bod a.val) b dep)
(Identical.go a (Let b.nam b.val b.bod) dep) =
(Identical a (b.bod b.val) dep)
(Identical.go Set Set dep) =
(Checker.pure 1)
(Identical.go (Ann a.val a.typ) b dep) =
(Identical a.val b dep)
(Identical.go a (Ann b.val b.typ) dep) =
(Identical a b.val dep)
//(Identical.go (Met a.uid) b dep) =
//(Identical a.val b dep)
//(Identical.go a (Met b.uid) dep) =
//(Identical a b.val dep)
(Identical.go (Met a.uid) (Met b.uid) dep) =
(Checker.pure (== a.uid b.uid))
(Identical.go (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) =
(Checker.pure (Same a.nam b.nam))
(Identical.go U60 U60 dep) =
(Checker.pure 1)
(Identical.go (Num a.val) (Num b.val) dep) =
(Checker.pure (== a.val b.val))
(Identical.go (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) =
(Checker.bind (Identical a.fst b.fst dep) λi.fst
(Checker.bind (Identical a.snd b.snd dep) λi.snd
(Checker.pure (& i.fst i.snd))))
(Identical.go (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) =
(Checker.bind (Identical a.x b.x dep) λi.x
(Checker.bind (Identical a.z b.z dep) λi.z
(Checker.bind (Identical (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) λi.s
(Checker.bind (Identical (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep) λi.p
(Checker.pure (& i.x (& i.z (& i.s i.p))))))))
(Identical.go (Txt a.txt) (Txt b.txt) dep) =
(Checker.pure (Same a.txt b.txt))
(Identical.go (Src a.src a.val) b dep) =
(Identical a.val b dep)
(Identical.go a (Src b.src b.val) dep) =
(Identical a b.val dep)
(Identical.go (Ref a.nam a.sub a.val) (Ref b.nam b.sub b.val) dep) =
(Checker.pure (Same a.nam b.nam))
(Identical.go (Var a.nam a.idx) (Var b.nam b.idx) dep) =
(Checker.pure (== a.idx b.idx))
(Identical.go a b dep) =
(Checker.pure 0)
// Unification
// -----------
// The unification algorithm is a simple pattern unifier, based on smalltt:
// > https://github.com/AndrasKovacs/elaboration-zoo/blob/master/03-holes/Main.hs
// The 'Unify.try' fn will attempt to match the following pattern:
// (?A x y z ...) = B
// Where:
// 1. The LHS spine, `x y z ...`, consists of distinct variables.
// 2. Every free var of the RHS, `B`, occurs in the spine.
// 3. The LHS hole, `?A`, doesn't occur in the RHS, `B`.
// If it is successful, it outputs the following substitution:
// ?A = λx λy λz ... B
// In this checker, we don't allow holes to occur in solutions at all.
// Unify.try : Term -> Term -> U60 -> (Checker U60) -> (Checker U60)
(Unify.try a b dep else) =
// Attempts to unify the pattern
(Maybe.match (Unify.solve a b dep Map.new)
// If successful, logs the solution
λkv(Pair.get kv λkλv
(Checker.bind (Checker.log (Solve k v dep)) λx
(Checker.pure 1)))
// Otherwise, signals to skip equality if this is a pattern
(If (Unify.skip a)
(Checker.pure 1)
(else)))
// If LHS is a solveable pattern, generates its solution.
// Unify.solve : Term -> Term -> U60 -> (Map U60 Term) -> (Maybe (Pair nam Term))
(Unify.solve (App fun (Var nam idx)) b dep ctx) =
(Maybe.bind (Map.ins λaλb(== a b) idx $x ctx) λctx
(Maybe.bind (Unify.solve fun b dep ctx) λkv
(Pair.get kv λkλv(Maybe.pure (Pair k (Lam nam λ$x(v)))))))
(Unify.solve (Met uid) b dep ctx) =
(Maybe.bind (Unify.solution b dep uid ctx) λneo
(Maybe.pure (Pair uid neo)))
(Unify.solve (App fun (Ann val _)) b dep ctx) = (Unify.solve (App fun val) b dep ctx)
(Unify.solve (App fun (Ins val)) b dep ctx) = (Unify.solve (App fun val) b dep ctx)
(Unify.solve (App fun (Src _ val)) b dep ctx) = (Unify.solve (App fun val) b dep ctx)
//(Unify.solve (App fun (Met uid)) b dep ctx) = (Unify.solve (App fun val) b dep ctx)
(Unify.solve (Ann val typ) b dep ctx) = (Unify.solve val b dep ctx)
(Unify.solve (Ins val) b dep ctx) = (Unify.solve val b dep ctx)
(Unify.solve (Src src val) b dep ctx) = (Unify.solve val b dep ctx)
//(Unify.solve (Met uid) b dep ctx) = (Unify.solve val b dep ctx)
(Unify.solve other b dep ctx) = None
// If LHS is an unsolveable pattern, skips its type-checking.
// Unify.skip : Term -> Bool
(Unify.skip (App fun arg)) = (Unify.skip fun)
(Unify.skip (Ann val typ)) = (Unify.skip val)
(Unify.skip (Ins val)) = (Unify.skip val)
(Unify.skip (Src src val)) = (Unify.skip val)
(Unify.skip (Met uid)) = 1
(Unify.skip (Hol nam ctx)) = 1
(Unify.skip other) = 0
// Attempts to convert RHS to a solution, checking the criteria.
// Unify.solution : Term -> U60 -> U60 -> (Map U60 Term) -> (Maybe Term)
(Unify.solution (All nam inp bod) dep uid ctx) =
(Maybe.bind (Unify.solution inp dep uid ctx) λinp
(Maybe.bind (Unify.solution (bod (Var nam dep)) (+ dep 1) uid ctx) λbod
(Maybe.pure (All nam inp λ_(bod)))))
(Unify.solution (Lam nam bod) dep uid ctx) =
(Maybe.bind (Unify.solution (bod (Var nam dep)) (+ 1 dep) uid ctx) λbod
(Maybe.pure (Lam nam λ_(bod))))
(Unify.solution (App fun arg) dep uid ctx) =
(Maybe.bind (Unify.solution fun dep uid ctx) λfun
(Maybe.bind (Unify.solution arg dep uid ctx) λarg
(Maybe.pure (App fun arg))))
(Unify.solution (Ann val typ) dep uid ctx) =
(Maybe.bind (Unify.solution val dep uid ctx) λval
(Maybe.bind (Unify.solution typ dep uid ctx) λtyp
(Maybe.pure (Ann val typ))))
(Unify.solution (Slf nam typ bod) dep uid ctx) =
(Unify.solution typ dep uid ctx)
(Unify.solution (Ins val) dep uid ctx) =
(Maybe.bind (Unify.solution val dep uid ctx) λval
(Maybe.pure (Ins val)))
(Unify.solution (Ref nam sub val) dep uid ctx) =
(Maybe.pure (Ref nam sub val))
(Unify.solution (Let nam val bod) dep uid ctx) =
(Maybe.bind (Unify.solution val dep uid ctx) λval
(Maybe.bind (Unify.solution (bod (Var nam dep)) (+ 1 dep) uid ctx) λbod
(Maybe.pure (Let nam val λ_(bod)))))
(Unify.solution (Met uid) dep uid ctx) =
None // holes can't appear in the solution
//(If (Same nam hol) None (Maybe.pure (Met nam None)))
//(Unify.solution (Met uid) dep hol ctx) =
//(Maybe.bind (Unify.solution val dep hol ctx) λval
//(Maybe.pure (Met uid)))
(Unify.solution (Hol nam _) dep hol ctx) =
(Maybe.pure (Hol nam [])) // FIXME?
(Unify.solution Set dep uid ctx) =
(Maybe.pure Set)
(Unify.solution U60 dep uid ctx) =
(Maybe.pure U60)
(Unify.solution (Num val) dep uid ctx) =
(Maybe.pure (Num val))
(Unify.solution (Op2 opr fst snd) dep uid ctx) =
(Maybe.bind (Unify.solution fst dep uid ctx) λfst
(Maybe.bind (Unify.solution snd dep uid ctx) λsnd
(Maybe.pure (Op2 opr fst snd))))
(Unify.solution (Mat nam x z s p) dep uid ctx) =
(Maybe.bind (Unify.solution x dep uid ctx) λx
(Maybe.bind (Unify.solution z dep uid ctx) λz
(Maybe.bind (Unify.solution (s (Var (String.concat nam "-1") dep)) dep uid ctx) λs
(Maybe.bind (Unify.solution (p (Var nam dep)) dep uid ctx) λp
(Maybe.pure (Mat nam x z λ_(s) λ_(p)))))))
(Unify.solution (Txt val) dep uid ctx) =
(Maybe.pure (Txt val))
(Unify.solution (Var nam idx) dep uid ctx) =
(Maybe.bind (Map.get λaλb(== a b) idx ctx) λval
(Maybe.pure val))
(Unify.solution (Src src val) dep uid ctx) =
(Maybe.bind (Unify.solution val dep uid ctx) λval
(Maybe.pure (Src src val)))
(Unify.solution term dep uid ctx) =
(HVM.log (UNREACHALBE (Show term dep)) None)
// Type-Checking
// -------------
(IfAll (All nam inp bod) yep nop) = (yep nam inp bod)
(IfAll other yep nop) = nop
(IfSlf (Slf nam typ bod) yep nop) = (yep nam typ bod)
(IfSlf other yep nop) = nop
//(Infer term dep) = (Print dep ["Infer: " (Show term dep)] (Infer.match term dep))
(Infer term dep) = (Infer.match term dep)
(Infer.match (All nam inp bod) dep) =
(Checker.bind (Check 0 inp Set dep) λinp_typ
(Checker.bind (Check 0 (bod (Ann (Var nam dep) inp)) Set (+ 1 dep)) λbod_typ
(Checker.pure Set)))
(Infer.match (App fun arg) dep) =
(Checker.bind (Infer fun dep) λfun_typ
((IfAll (Reduce 2 fun_typ)
λfun_nam λfun_typ.inp λfun_typ.bod λfun λarg
(Checker.bind (Check 0 arg fun_typ.inp dep) λvty
(Checker.pure (fun_typ.bod arg)))
λfun λarg
(Checker.pure 1))
fun arg))
(Infer.match (Ann val typ) dep) =
(Checker.pure typ)
(Infer.match (Slf nam typ bod) dep) =
(Checker.bind (Check 0 (bod (Ann (Var nam dep) typ)) Set (+ dep 1)) λslf
(Checker.pure Set))
(Infer.match (Ins val) dep) =
(Checker.bind (Infer val dep) λvty
((IfSlf (Reduce 2 vty)
λvty.nam λvty.typ λvty.bod λval
(Checker.pure (vty.bod (Ins val)))
λval
(Checker.fail (Error 0 vty (Hol "self-type" []) (Ins val) dep)))
val))
(Infer.match (Ref nam sub val) dep) =
(Infer val dep)
(Infer.match Set dep) =
(Checker.pure Set)
(Infer.match U60 dep) =
(Checker.pure Set)
(Infer.match (Num num) dep) =
(Checker.pure U60)
(Infer.match (Txt txt) dep) =
(Checker.pure Book.String)
(Infer.match (Op2 opr fst snd) dep) =
(Checker.bind (Check 0 fst U60 dep) λfst
(Checker.bind (Check 0 snd U60 dep) λsnd
(Checker.pure U60)))
(Infer.match (Mat nam x z s p) dep) =
(Checker.bind (Check 0 x U60 dep) λx_typ
(Checker.bind (Check 0 (p (Ann (Var nam dep) U60)) Set dep) λp_typ
(Checker.bind (Check 0 z (p (Num 0)) dep) λz_typ
(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 "untyped_term" []) (Hol "type_annotation" []) (Lam nam bod) dep))
(Infer.match (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 "untyped_term" []) (Hol "type_annotation" []) (Hol nam ctx) dep))
//(Infer.match (Met nam (Some val)) dep) =
//(Infer.match val dep)
(Infer.match (Met uid) dep) =
(Checker.fail (Error 0 (Hol "untyped_term" []) (Hol "type_annotation" []) (Met uid) dep))
(Infer.match (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)
//(Check src term type dep) = (Print dep ["Check: " (Show term dep) " :: " (Show type dep) " ~> " (Show (Reduce 1 type) dep)] (Check.match src term type dep))
(Check src term type dep) = (Check.match src term type dep)
(Check.match src (Lam term.nam term.bod) type dep) =
((IfAll (Reduce 2 type)
λtype.nam λtype.inp λtype.bod λterm.bod
let ann = (Ann (Var term.nam dep) type.inp)
let term = (term.bod ann)
let type = (type.bod ann)
(Check 0 term type (+ dep 1))
λterm.bod
(Infer (Lam term.nam term.bod) dep))
term.bod)
(Check.match src (Ins term.val) type dep) =
((IfSlf (Reduce 2 type)
λtype.nam λtype.typ λtype.bod λterm.val
(Check 0 term.val (type.bod (Ins term.val)) dep)
λterm.val
(Infer (Ins term.val) dep))
term.val)
(Check.match src (Let term.nam term.val term.bod) type dep) =
(Check 0 (term.bod term.val) type (+ 1 dep))
(Check.match src (Hol term.nam term.ctx) type dep) =
(Checker.bind (Checker.log (Found term.nam type term.ctx dep)) λx
(Checker.pure 0))
//(Check.match src (Met term.nam (Some term.val)) type dep) =
//(Check src term.val type dep)
(Check.match src (Met uid) type dep) =
(Checker.pure 0)
(Check.match src (Ref term.nam term.sub (Ann term.val term.typ)) type dep) = // better printing
(Checker.bind (Equal type term.typ dep) λequal
(Check.report src equal term.typ type (Ref term.nam term.sub term.val) dep))
(Check.match src (Src term.src term.val) type dep) =
(Check term.src term.val type dep)
//(Check.match src (Ref term.nam term.val) type dep) =
//(Check term.val type dep)
(Check.match src term type dep) =
(Check.verify src term type dep)
(Check.verify src term type dep) =
(Checker.bind (Infer term dep) λinfer
(Checker.bind (Equal type infer dep) λequal
(Check.report src equal infer type term dep)))
(Check.report src 0 detected expected value dep) =
(Checker.fail (Error src detected expected value dep))
(Check.report src n detected expected value dep) =
(Checker.pure 0)
// Syntax
// ------
(Show (All nam inp bod) dep) =
let nam = nam
let inp = (Show inp dep)
let bod = (Show (bod (Var nam dep)) (+ dep 1))
(String.join ["∀(" nam ": " inp ") " bod])
(Show (Lam nam bod) dep) =
let nam = nam
let bod = (Show (bod (Var nam dep)) (+ dep 1))
(String.join ["λ" nam " " bod])
(Show (App fun arg) dep) =
let fun = (Show.unwrap (Show fun dep))
let arg = (Show arg dep)
(String.join ["(" fun " " arg ")"])
(Show (Ann val typ) dep) =
let val = (Show val dep)
let typ = (Show typ dep)
(String.join ["{" val ": " typ "}"])
(Show (Slf nam typ bod) dep) =
let nam = nam
let typ = (Show typ dep)
let bod = (Show (bod (Var nam dep)) (+ dep 1))
(String.join ["$(" nam ": " typ ") " bod])
(Show (Ins val) dep) =
let val = (Show val dep)
(String.join ["~" val])
(Show (Ref nam sub val) dep) =
nam
(Show (Let nam val bod) dep) =
let nam = nam
let val = (Show val dep)
let bod = (Show (bod (Var nam dep)) (+ dep 1))
(String.join ["let " nam " = " val "; " bod])
(Show Set dep) =
"*"
(Show U60 dep) =
"#U60"
(Show (Num val) dep) =
let val = (U60.show val)
(String.join ["#" val])
(Show (Op2 opr fst snd) dep) =
let opr = (Op2.show opr)
let fst = (Show fst dep)
let snd = (Show snd dep)
(String.join ["#(" opr " " fst " " snd ")"])
(Show (Mat nam x z s p) dep) =
let nam = nam
let x = (Show x dep)
let z = (Show z dep)
let s = (Show (s (Var (String.concat nam "-1") dep)) (+ dep 1))
let p = (Show (p (Var nam dep)) dep)
(String.join ["#match " nam " = " x " { #0: " z " #+: " s " }: " p])
(Show (Txt txt) dep) =
(String.join [Quote txt Quote])
(Show (Hol nam ctx) dep) =
(String.join ["? " nam])
(Show (Met uid) dep) =
"_"
//(Show (Met nam (Some val)) dep) =
//(Show val dep)
(Show (Var nam idx) dep) =
nam
(Show (Src src val) dep) =
(Show val dep)
//(Show.many List.nil dep) = ""
//(Show.many (List.cons x xs) dep) = (String.join [" " (Show x dep) (Show.many xs dep)])
(Show.trim (String.cons ' ' xs)) = xs
(Show.trim str) = str
(Show.unwrap (String.cons '(' xs)) = (Show.begin xs)
(Show.unwrap str) = str
(Show.begin (String.cons x (String.cons y String.nil))) = (String.cons x String.nil)
(Show.begin (String.cons x xs)) = (String.cons x (Show.begin xs))
(Show.begin String.nil) = String.nil
(Op2.show ADD) = "+"
(Op2.show SUB) = "-"
(Op2.show MUL) = "*"
(Op2.show DIV) = "/"
(Op2.show MOD) = "%"
(Op2.show EQ) = "=="
(Op2.show NE) = "!="
(Op2.show LT) = "<"
(Op2.show GT) = ">"
(Op2.show LTE) = "<="
(Op2.show GTE) = ">="
(Op2.show AND) = "&"
(Op2.show OR) = "|"
(Op2.show XOR) = "^"
(Op2.show LSH) = "<<"
(Op2.show RSH) = ">>"
(Context.show List.nil dep) = ""
(Context.show (List.cons x xs) dep) = (String.join [" " (Context.show.ann x dep) (Context.show xs dep)])
(Context.show.ann (Ann val typ) dep) = (String.join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 typ dep) dep) "}"])
(Context.show.ann term dep) = (Show (Normal 0 term dep) dep)
(Info.show (Found name type ctx dep)) =
let type = (Show (Normal 1 type dep) dep)
let ctx = (String.tail (Context.show ctx dep))
(String.join ["#found{" name " " type " [" ctx "]}"])
(Info.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 0 value dep) dep)
(String.join ["#error{" exp " " det " " val " " (U60.show src) "}"])
(Info.show (Solve name term dep)) =
let term = (Show (Normal 1 term dep) dep)
(String.join ["#solve{" name " " term "}"])
(Info.show (Vague name)) =
(String.join ["#vague{" name "}"])
// Compilation
// -----------
(Str.view str) = (str 0 λheadλtail(String.cons head (Str.view tail)) String.nil)
(Str.make (String.cons x xs)) = λP λcons λnil (cons x (Str.make xs))
(Str.make String.nil) = λP λcons λnil nil
Compile.primitives = [
(Pair "HVM.log" λA λB λmsg λret (HVM.log msg ret))
(Pair "HVM.print" λA λmsg λret (HVM.print (Str.view msg) ret))
(Pair "HVM.save" λA λname λdata λret (HVM.save (Str.view name) (Str.view data) ret))
(Pair "HVM.load" λA λname λret (HVM.load (Str.view name) λdata (ret (Str.make data))))
]
(Compile (All nam inp bod)) = 0
(Compile (Lam nam bod)) = λx(Compile (bod (Var "" x)))
(Compile (App fun arg)) = ((Compile fun) (Compile arg))
(Compile (Ann val typ)) = (Compile val)
(Compile (Slf nam typ bod)) = 0
(Compile (Ins val)) = (Compile val)
(Compile (Ref nam sub val)) = (Compile.ref Compile.primitives nam val)
(Compile (Let nam val bod)) = (Compile (bod val))
(Compile Set) = 0
(Compile U60) = 0
(Compile (Num val)) = val
(Compile (Op2 opr fst snd)) = (Compile.op2 opr (Compile fst) (Compile snd))
(Compile (Mat nam x z s p)) = (Compile.mat (Compile x) (Compile z) λx(Compile (s (Var "" x))))
(Compile (Txt txt)) = (Str.make txt)
(Compile (Hol nam ctx)) = 0
(Compile (Var nam val)) = val
(Compile (Src src val)) = (Compile val)
//(Compile.txt (String.cons x xs)) = (App (App Book.String.cons (Num x)) (Compile.txt xs))
//(Compile.txt String.nil) = Book.String.nil
(Compile.op2 ADD fst snd) = (+ fst snd)
(Compile.op2 SUB fst snd) = (- fst snd)
(Compile.op2 MUL fst snd) = (* fst snd)
(Compile.op2 DIV fst snd) = (/ fst snd)
(Compile.op2 MOD fst snd) = (% fst snd)
(Compile.op2 EQ fst snd) = (== fst snd)
(Compile.op2 NE fst snd) = (!= fst snd)
(Compile.op2 LT fst snd) = (< fst snd)
(Compile.op2 GT fst snd) = (> fst snd)
(Compile.op2 LTE fst snd) = (<= fst snd)
(Compile.op2 GTE fst snd) = (>= fst snd)
(Compile.op2 AND fst snd) = (& fst snd)
(Compile.op2 OR fst snd) = (| fst snd)
(Compile.op2 XOR fst snd) = (^ fst snd)
(Compile.op2 LSH fst snd) = (<< fst snd)
(Compile.op2 RSH fst snd) = (>> fst snd)
(Compile.mat 0 z s) = z
(Compile.mat n z s) = (s (- n 1))
(Compile.ref (List.cons (Pair prim_name prim_func) prims) nam val) = (If (Same prim_name nam) prim_func (Compile.ref prims nam val))
(Compile.ref List.nil nam val) = (Compile val)
// API
// ---
// Normalizes a definition.
(API.normal (Ref nam sub val)) =
(Compile (Subst sub val))
// Checks a definition.
(API.check (Ref nam sub def)) =
//(HVM.print (String.join ["API.check: " (Show (Subst sub def) 0)])
(Result.match (Checker.run (API.check.do (Subst sub def)))
// case done:
λfill λlogs λvalue
//(API.check.log logs
(Pair.get (API.check.fill sub logs) λfilled λsub
(If filled
// case true:
(API.check (Ref nam sub def))
// case false:
(API.check.log logs 1)))
// case fail:
λfill λlogs λerror
(API.check.log logs
(API.check.log [error] 0)))
// Calls the type-checker *under* the metavar binders.
//(API.check.fn (List.cons _ subs) val) = λx (API.check.fn subs (val x))
//(API.check.fn List.nil val) = (API.check.do val)
// Calls check on typed defs and infer on untyped defs.
(API.check.do (Ann val typ)) = (Check 0 val typ 0)
(API.check.do val) = (Infer val 0)
// Moves solutions from the checker logs to a ref's subst list.
(API.check.fill sub (List.cons (Solve k v d) xs)) = (Pair.get (API.check.fill sub xs) λokλmap(Pair 1 (Map.set λxλy(Same x y) k (Some v) sub)))
(API.check.fill sub (List.cons info xs)) = (API.check.fill sub xs)
(API.check.fill sub List.nil) = (Pair 0 sub)
// Prints all messages returned by the checker.
(API.check.log (List.cons msg msgs) then) = (HVM.print (Info.show msg) (API.check.log msgs then))
(API.check.log List.nil then) = then
// Reports solved holdes
(API.check.vague (List.cons (Pair name None) xs)) = (HVM.print (Info.show (Vague name)) (& 0 (API.check.vague xs)))
(API.check.vague (List.cons (Pair name (Some x)) xs)) = (API.check.vague xs)
(API.check.vague List.nil) = 1

904
src/kind2.hvm2
View File

@ -1,904 +0,0 @@
// This is a Haskell implementation of Kind2's type checker. Since Kind2 isn't
// bootstrapped, we can't use Kind2 itself to type-check it, and developing a
// complex checker in an untyped language (like HVM) is hard. As such, this
// Haskell view helps me develop and debug the checker, and it is done in a way
// that makes it easy to manually compile it to HVM, keeping an HVM view. It can
// also be useful to let us benchmark all versions (GHC/HVM1/HVM2), giving us a
// good idea on how these compare in performance.
// Kind2 Types
// -----------
data Maybe
= (Some val)
| None
data Bool
= False
| True
data Oper
= ADD | SUB | MUL | DIV
| MOD | EQ | NE | LT
| GT | LTE | GTE | AND
| OR | XOR | LSH | RSH
data Term
= (All nam inp bod) // All String Term (Term -> Term)
| (Lam nam bod) // Lam String (Term -> Term)
| (App fun arg) // App Term Term
| (Ann chk val typ) // Ann Bool Term Term
| (Slf nam typ bod) // Slf String Term (Term -> Term)
| (Ins val) // Ins Term
| (Ref nam val) // Ref String Term
| (Let nam val bod) // Let String Term (Term -> Term)
| (Use nam val bod) // Use String Term (Term -> Term)
| Set // Set
| U60 // U60
| (Num val) // Num U60
| (Op2 opr fst snd) // Op2 Oper Term Term
| (Swi nam x z s p) // Swi String Term Term (Term -> Term) (Term -> Term)
| (Hol nam ctx) // Hol String [Term]
| (Met uid spn) // Met U60 [Term]
| (Var nam idx) // Var String U60
| (Src src val) // Src U60 Term
| (Txt val) // Txt String
| (Nat val) // Nat Integer
data Info
= (Found name type ctx dep) // Found String Term [Term] Int
| (Solve name term dep) // Solve U60 Term U60
| (Error src detected expected value dep) // Error U60 Term Term Term Int
| (Vague name) // Vague String
| (Print value dep) // Print Term Int
data Check = (Check a t1 t2 b) // Check U60 Term Term U60
data State = (State map check info) // State (Map Term) [Check] [Info] -- state type
data Res = (Done state a) | (Fail state) // Done State a | Fail State -- result type
data Env = (Env env) // Env (State -> Res a) -- environment computation
data Bits = (O bits) | (I bits) | E
data Map = (Leaf) | (Node v lft rgt) // Leaf | Node (Maybe a) (Map a) (Map a)
// Prelude
// -------
// Note: many of these functions are present in Haskell, but we re-implement
// them here in order to have identical equivalents on HVM's view.
data Error
= Unreachable
| InvalidTopLevelDefinition
If True then else = then
If False then else = else
if 0 then else = else
if n then else = then
and True b = b
and False _ = False
or True b = True
or a True = True
or _ _ = False
not True = False
not False = True
eq lft rgt = (if (== lft rgt) True False)
// map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (List.cons x xs) = (List.cons (f x) (map f xs))
// even :: U60 -> Bool
even n = (eq (% n 2) 0)
// reverse :: [a] -> [a]
reverse l = (reverseGo l [])
reverseGo [] a = a
reverseGo (List.cons x xs) a = (reverseGo xs (List.cons x a))
// elem :: (a -> a -> Bool) -> a -> [a] -> Bool
elem cmp a [] = False
elem cmp a (List.cons x xs) = (If (cmp a x) True (elem cmp a xs))
// u60Show :: U60 -> String
u60Show n = (u60ShowGo n "")
u60ShowGo n res = (u60ShowGoMatch (< n 10) n res)
u60ShowGoMatch 0 n res = (u60ShowGo (/ n 10) (String.cons (+ '0' (% n 10)) res))
u60ShowGoMatch _ n res = (String.cons (+ '0' n) res)
// u60Name :: U60 -> String
u60Name n = (u60NameGo (+ n 1))
u60NameGo 0 = ""
u60NameGo n = (String.cons (+ 'a' (% (- n 1) 26)) (u60NameGo (/ (- n 1) 26)))
// listFind :: Eq a => a -> [(a, b)] -> Maybe b
listFind _ [] = None
listFind name (List.cons (nam, val) tail) = (If (stringEqual name nam) (Some val) (listFind name tail))
// listMap :: (a -> b) -> [a] -> [b]
listMap f [] = []
listMap f (List.cons x xs) = (List.cons (f x) (listMap f xs))
// listPush :: a -> [a] -> [a]
listPush x [] = [x]
listPush x (List.cons y ys) = (List.cons y (listPush x ys))
// newLine :: String
newLine = "\n"
// quote :: String
quote = "\""
// stringEqual :: String -> String -> Bool
stringEqual "" "" = True
stringEqual "" _ = False
stringEqual _ "" = False
stringEqual (String.cons x xs) (String.cons y ys) = (if (== x y) (stringEqual xs ys) False)
// stringConcat :: String -> String -> String
stringConcat "" ys = ys
stringConcat (String.cons x xs) ys = (String.cons x (stringConcat xs ys))
// stringJoin :: [String] -> String
stringJoin [] = ""
stringJoin (List.cons x xs) = (stringConcat x (stringJoin xs))
// stringTail :: String -> String
stringTail "" = ""
stringTail (String.cons _ xs) = xs
// pairFst :: (a, b) -> a
pairFst (fst, _) = fst
// pairSnd :: (a, b) -> b
pairSnd (_, snd) = snd
// pairGet :: (a, b) -> (a -> b -> c) -> c
pairGet (fst, snd) fun = (fun fst snd)
// maybeMatch :: Maybe a -> (a -> b) -> b -> b
maybeMatch (Some value) some _ = (some value)
maybeMatch None _ none = none
// maybePure :: a -> Maybe a
maybePure x = (Some x)
// maybeBind :: Maybe a -> (a -> Maybe b) -> Maybe b
maybeBind a b = (maybeMatch a b None)
// key :: U60 -> Bits
key 0 = E
key 1 = (I E)
key n = (If (even n)
(O (key (/ n 2)))
(I (key (/ n 2))))
// mapNew :: Map a
mapNew = Leaf
// mapHas :: Bits -> Map a -> Bool
mapHas E (Node (Some _) _ _) = True
mapHas (O bits) (Node _ lft _) = (mapHas bits lft)
mapHas (I bits) (Node _ _ rgt) = (mapHas bits rgt)
mapHas _ _ = False
// mapGet :: Bits -> Map a -> Maybe a
mapGet E (Node val _ _) = val
mapGet (O bits) (Node _ lft _) = (mapGet bits lft)
mapGet (I bits) (Node _ _ rgt) = (mapGet bits rgt)
mapGet _ Leaf = None
// mapSet :: Bits -> a -> Map a -> Map a
mapSet E val Leaf = (Node (Some val) Leaf Leaf)
mapSet E val (Node _ lft rgt) = (Node (Some val) lft rgt)
mapSet (O bits) val Leaf = (Node None (mapSet bits val Leaf) Leaf)
mapSet (O bits) val (Node v lft rgt) = (Node v (mapSet bits val lft) rgt)
mapSet (I bits) val Leaf = (Node None Leaf (mapSet bits val Leaf))
mapSet (I bits) val (Node v lft rgt) = (Node v lft (mapSet bits val rgt))
// Environment
// -----------
// infoIsSolve :: Info -> Bool
infoIsSolve (Solve _ _ _) = True
infoIsSolve _ = False
// Pattern matches on a computation result
// resMatch :: Res a -> (State -> a -> b) -> (State -> Info -> b) -> b
// resMatch (Done state value) done _ = (Done state value)
// resMatch (Fail state) _ fail = (Fail state)
// Monadic bind function
// envBind :: Env a -> (a -> Env b) -> Env b
envBind (Env a) b = (Env (λstate (match (a state) {
(Done state_ value): let (Env b_) = (b value); (b_ state_)
(Fail state_) : (Fail state_)
})))
// envPure :: a -> Env a
envPure a = (Env λstate (Done state a))
// envFail :: Env a
envFail = (Env λstate (Fail state))
// envRun :: Env a -> Res a
envRun (Env chk) = (chk (State mapNew [] []))
// envLog :: Info -> Env U60
envLog log = (Env λstate let (State fill susp logs) = state; (Done (State fill susp (List.cons log logs)) 1))
// envSnapshot :: Env State
envSnapshot = (Env λstate (Done state state))
// envRewind :: State -> Env U60
envRewind state = (Env λ_ (Done state 0))
// envSusp :: Check -> Env *
envSusp chk = (Env λstate let (State fill susp logs) = state; (Done (State fill (listPush chk susp) logs) *))
// envFill :: U60 -> Term -> Env *
envFill k v = (Env λstate let (State fill susp logs) = state; (Done (State (mapSet (key k) v fill) susp logs) *))
// envGetFill :: Env (Map Term)
envGetFill = (Env λstate let (State fill susp logs) = state; (Done (State fill susp logs) fill))
// envTakeSusp :: Env [Check]
envTakeSusp = (Env λstate let (State fill susp logs) = state; (Done (State fill [] logs) susp))
// instance Functor Env where
// fmap f (Env chk) = Env λlogs -> case chk logs of
// Done logs' a -> Done logs' (f a)
// Fail logs' -> Fail logs'
// instance Applicative Env where
// pure = envPure
// (Env chkF) <*> (Env chkA) = Env λlogs -> case chkF logs of
// Done logs' f -> case chkA logs' of
// Done logs'' a -> Done logs'' (f a)
// Fail logs'' -> Fail logs''
// Fail logs' -> Fail logs'
// instance Monad Env where
// (Env a) >>= b = envBind (Env a) b
// Evaluation
// ----------
// Evaluation levels:
// - 0: reduces refs never
// - 1: reduces refs on redexes
// - 2: reduces refs always
// termReduce :: Map Term -> U60 -> Term -> Term
termReduce fill lv (App fun arg) = (termReduceApp fill lv (termReduce fill lv fun) arg)
termReduce fill lv (Ann chk val typ) = (termReduce fill lv val)
termReduce fill lv (Ins val) = (termReduce fill lv val)
termReduce fill lv (Ref nam val) = (termReduceRef fill lv nam (termReduce fill lv val))
termReduce fill lv (Let nam val bod) = (termReduce fill lv (bod val))
termReduce fill lv (Use nam val bod) = (termReduce fill lv (bod val))
termReduce fill lv (Op2 opr fst snd) = (termReduceOp2 fill lv opr (termReduce fill lv fst) (termReduce fill lv snd))
termReduce fill lv (Swi nam x z s p) = (termReduceSwi fill lv nam (termReduce fill lv x) z s p)
termReduce fill lv (Txt txt) = (termReduceTxt fill lv txt)
termReduce fill lv (Nat val) = (termReduceNat fill lv val)
termReduce fill lv (Src src val) = (termReduce fill lv val)
termReduce fill lv (Met uid spn) = (termReduceMet fill lv uid spn)
termReduce fill lv val = val
// termReduceApp :: Map Term -> U60 -> Term -> Term -> Term
termReduceApp fill 2 (Ref nam val) arg = (termReduceApp fill 2 val arg)
termReduceApp fill 1 (Ref nam val) arg = (termReduceApp fill 1 val arg)
termReduceApp fill lv (Met uid spn) arg = (termReduce fill lv (Met uid (listPush arg spn)))
termReduceApp fill lv (Lam nam bod) arg = (termReduce fill lv (bod (termReduce fill 0 arg)))
termReduceApp fill lv fun arg = (App fun arg)
// termReduceMet :: Map Term -> U60 -> U60 -> [Term] -> Term
termReduceMet fill lv uid spn = match (mapGet (key uid) fill) {
(Some val): (termReduce fill lv (termReduceMetSpine val spn))
(None) : (Met uid spn)
}
// termReduceMetSpine :: Term -> [Term] -> Term
termReduceMetSpine val [] = val
termReduceMetSpine val (List.cons x xs) = (termReduceMetSpine (App val x) xs)
// termReduceOp2 :: Map Term -> U60 -> Oper -> Term -> Term -> Term
termReduceOp2 fill 1 op (Ref _ x) (Num snd) = (termReduceOp2 fill 1 op x (Num snd))
termReduceOp2 fill 2 op (Ref _ x) (Num snd) = (termReduceOp2 fill 2 op x (Num snd))
termReduceOp2 fill 1 op (Num fst) (Ref _ x) = (termReduceOp2 fill 1 op (Num fst) x)
termReduceOp2 fill 2 op (Num fst) (Ref _ x) = (termReduceOp2 fill 2 op (Num fst) x)
termReduceOp2 fill lv ADD (Num fst) (Num snd) = (Num (+ fst snd))
termReduceOp2 fill lv SUB (Num fst) (Num snd) = (Num (- fst snd))
termReduceOp2 fill lv MUL (Num fst) (Num snd) = (Num (* fst snd))
termReduceOp2 fill lv DIV (Num fst) (Num snd) = (Num (/ fst snd))
termReduceOp2 fill lv MOD (Num fst) (Num snd) = (Num (% fst snd))
termReduceOp2 fill lv EQ (Num fst) (Num snd) = (Num (== fst snd))
termReduceOp2 fill lv NE (Num fst) (Num snd) = (Num (!= fst snd))
termReduceOp2 fill lv LT (Num fst) (Num snd) = (Num (< fst snd))
termReduceOp2 fill lv GT (Num fst) (Num snd) = (Num (> fst snd))
termReduceOp2 fill lv LTE (Num fst) (Num snd) = (Num (<= fst snd))
termReduceOp2 fill lv GTE (Num fst) (Num snd) = (Num (>= fst snd))
termReduceOp2 fill lv AND (Num fst) (Num snd) = (Num (& fst snd))
termReduceOp2 fill lv OR (Num fst) (Num snd) = (Num (| fst snd))
termReduceOp2 fill lv XOR (Num fst) (Num snd) = (Num (^ fst snd))
termReduceOp2 fill lv LSH (Num fst) (Num snd) = (Num (<< fst snd))
termReduceOp2 fill lv RSH (Num fst) (Num snd) = (Num (>> fst snd))
termReduceOp2 fill lv opr fst snd = (Op2 opr fst snd)
// termReduceSwi :: Map Term -> U60 -> String -> Term -> Term -> (Term -> Term) -> (Term -> Term) -> Term
termReduceSwi fill 2 nam (Ref _ x) z s p = (termReduceSwi fill 2 nam x z s p)
termReduceSwi fill 1 nam (Ref _ x) z s p = (termReduceSwi fill 1 nam x z s p)
termReduceSwi fill lv nam (Num 0) z s p = (termReduce fill lv z)
termReduceSwi fill lv nam (Num n) z s p = (termReduce fill lv (s (Num (- n 1))))
termReduceSwi fill lv nam (Op2 ADD (Num 1) k) z s p = (termReduce fill lv (s k))
termReduceSwi fill lv nam val z s p = (Swi nam val z s p)
// termReduceRef :: Map Term -> U60 -> String -> Term -> Term
termReduceRef fill 2 nam val = (termReduce fill 2 val)
termReduceRef fill 1 nam val = (Ref nam val)
termReduceRef fill lv nam val = (Ref nam val)
// termReduceTxt :: Map Term -> U60 -> String -> Term
termReduceTxt fill lv "" = (termReduce fill lv Book.String.nil)
termReduceTxt fill lv (String.cons x xs) = (termReduce fill lv (App (App Book.String.cons (Num x)) (Txt xs)))
// termReduceNat :: Map Term -> Int -> Integer -> Term
termReduceNat fill lv 0 = Book.Nat.zero
termReduceNat fill lv n = (App Book.Nat.succ (termReduceNat fill lv (- n 1)))
// Normalization
// -------------
// termNormal :: Map Term -> U60 -> Term -> U60 -> Term
// termNormal fill lv term dep = termNormalGo fill lv (termNormalPrefer fill (termReduce fill 0 term) (termReduce fill lv term)) dep where
termNormal fill lv term dep = (termNormalGo fill lv (termReduce fill lv term) dep)
// termNormalPrefer fill soft (Lam _ _) = soft
// termNormalPrefer fill soft (Slf _ _ _) = soft
// termNormalPrefer fill soft (All _ _ _) = soft
// termNormalPrefer fill soft hard = hard
termNormalGo fill lv (All nam inp bod) dep = (All nam (termNormal fill lv inp dep) (λx (termNormal fill lv (bod (Var nam dep)) (+ dep 1))))
termNormalGo fill lv (Lam nam bod) dep = (Lam nam (λx (termNormal fill lv (bod (Var nam dep)) (+ dep 1))))
termNormalGo fill lv (App fun arg) dep = (App (termNormal fill lv fun dep) (termNormal fill lv arg dep))
termNormalGo fill lv (Ann chk val typ) dep = (Ann chk (termNormal fill lv val dep) (termNormal fill lv typ dep))
termNormalGo fill lv (Slf nam typ bod) dep = (Slf nam typ (λx (termNormal fill lv (bod (Var nam dep)) (+ dep 1))))
termNormalGo fill lv (Ins val) dep = (Ins (termNormal fill lv val dep))
termNormalGo fill lv (Ref nam val) dep = (Ref nam (termNormal fill lv val dep))
termNormalGo fill lv (Let nam val bod) dep = (Let nam (termNormal fill lv val dep) (λx (termNormal fill lv (bod (Var nam dep)) (+ dep 1))))
termNormalGo fill lv (Use nam val bod) dep = (Use nam (termNormal fill lv val dep) (λx (termNormal fill lv (bod (Var nam dep)) (+ dep 1))))
termNormalGo fill lv (Hol nam ctx) dep = (Hol nam ctx)
termNormalGo fill lv Set dep = (Set)
termNormalGo fill lv U60 dep = (U60)
termNormalGo fill lv (Num val) dep = (Num val)
termNormalGo fill lv (Op2 opr fst snd) dep = (Op2 opr (termNormal fill lv fst dep) (termNormal fill lv snd dep))
termNormalGo fill lv (Swi nam x z s p) dep = (Swi nam (termNormal fill lv x dep) (termNormal fill lv z dep) (λk (termNormal fill lv (s (Var (stringConcat nam "-1") dep)) dep)) (λk (termNormal fill lv (p (Var nam dep)) dep)))
termNormalGo fill lv (Txt val) dep = (Txt val)
termNormalGo fill lv (Nat val) dep = (Nat val)
termNormalGo fill lv (Var nam idx) dep = (Var nam idx)
termNormalGo fill lv (Src src val) dep = (Src src (termNormal fill lv val dep))
termNormalGo fill lv (Met uid spn) dep = (Met uid spn) // TODO: normalize spine
// Equality
// --------
// termEqual :: Term -> Term -> U60 -> Env Bool
termEqual a b dep =
// (trace (stringJoin ["equal:\n- ", (termShow a dep), "\n- ", (termShow b dep)])
(envBind envGetFill λfill
let a_ = (termReduce fill 2 a)
let b_ = (termReduce fill 2 b)
(termTryIdentical a_ b_ dep (termSimilar a_ b_ dep)))
// termTryIdentical :: Term -> Term -> U60 -> Env Bool -> Env Bool
termTryIdentical a b dep cont =
(envBind envSnapshot λstate
(envBind (termIdentical a b dep) λequal
(If equal
(envPure True)
(envBind (envRewind state) λ_ cont))))
// termSimilar :: Term -> Term -> U60 -> Env Bool
termSimilar (All aNam aInp aBod) (All bNam bInp bBod) dep =
(envBind (termEqual aInp bInp dep) λeInp
(envBind (termEqual (aBod (Var aNam dep)) (bBod (Var bNam dep)) (+ dep 1)) λeBod
(envPure (and eInp eBod))))
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 =
(envBind (termSimilar aFun bFun dep) λeFun
(envBind (termEqual aArg bArg dep) λeArg
(envPure (and eFun eArg))))
termSimilar (Slf aNam aTyp aBod) (Slf bNam bTyp bBod) dep =
(termSimilar (termReduce mapNew 0 aTyp) (termReduce mapNew 0 bTyp) dep)
// termSimilar (Hol aNam aCtx) (Hol bNam bCtx) dep =
// (envPure (eq aNam bNam))
// termSimilar (Met aUid aSpn) (Met bUid bSpn) dep =
// (envPure (eq aUid bUid))
termSimilar (Op2 aOpr aFst aSnd) (Op2 bOpr bFst bSnd) dep =
(envBind (termEqual aFst bFst dep) λeFst
(envBind (termEqual aSnd bSnd dep) λeSnd
(envPure (and eFst eSnd))))
termSimilar (Swi aNam aX aZ aS aP) (Swi bNam bX bZ bS bP) dep =
(envBind (termEqual aX bX dep) λeX
(envBind (termEqual aZ bZ dep) λeZ
(envBind (termEqual (aS (Var (stringConcat aNam "-1") dep)) (bS (Var (stringConcat bNam "-1") dep)) dep) λeS
(envBind (termEqual (aP (Var aNam dep)) (bP (Var bNam dep)) dep) λeP
(envPure (and (and (and eX eZ) eS) eP))))))
termSimilar a b dep = (termIdentical a b dep)
// termIdentical :: Term -> Term -> U60 -> Env Bool
termIdentical a b dep = (termIdenticalGo a b dep)
// termIdenticalGo :: Term -> Term -> U60 -> Env Bool
termIdenticalGo (All aNam aInp aBod) (All bNam bInp bBod) dep =
(envBind (termIdentical aInp bInp dep) (λiInp
(envBind (termIdentical (aBod (Var aNam dep)) (bBod (Var bNam dep)) (+ dep 1)) λiBod
(envPure (and iInp iBod)))))
termIdenticalGo (Lam aNam aBod) (Lam bNam bBod) dep =
(termIdentical (aBod (Var aNam dep)) (bBod (Var bNam dep)) (+ dep 1))
termIdenticalGo (App aFun aArg) (App bFun bArg) dep =
(envBind (termIdentical aFun bFun dep) λiFun
(envBind (termIdentical aArg bArg dep) λiArg
(envPure (and iFun iArg))))
termIdenticalGo (Slf aNam aTyp aBod) (Slf bNam bTyp bBod) dep =
(termIdentical aTyp bTyp dep)
termIdenticalGo (Ins aVal) b dep =
(termIdentical aVal b dep)
termIdenticalGo a (Ins bVal) dep =
(termIdentical a bVal dep)
termIdenticalGo (Let aNam aVal aBod) b dep =
(termIdentical (aBod aVal) b dep)
termIdenticalGo a (Let bNam bVal bBod) dep =
(termIdentical a (bBod bVal) dep)
termIdenticalGo (Use aNam aVal aBod) b dep =
(termIdentical (aBod aVal) b dep)
termIdenticalGo a (Use bNam bVal bBod) dep =
(termIdentical a (bBod bVal) dep)
termIdenticalGo Set Set dep =
(envPure True)
termIdenticalGo (Ann chk aVal aTyp) b dep =
(termIdentical aVal b dep)
termIdenticalGo a (Ann chk bVal bTyp) dep =
(termIdentical a bVal dep)
// termIdenticalGo (Met aUid aSpn) (Met bUid bSpn) dep =
// envPure (eq aUid bUid)
termIdenticalGo a (Met bUid bSpn) dep =
// traceShow (stringJoin ["unify: ", (u60Show bUid), " x=", (termShow (Met bUid bSpn) dep), " t=", (termShow a dep)])
(termUnify bUid bSpn a dep)
termIdenticalGo (Met aUid aSpn) b dep =
// traceShow (stringJoin ["unify: ", (u60Show aUid), " x=", (termShow (Met aUid aSpn) dep), " t=", (termShow b dep)])
(termUnify aUid aSpn b dep)
termIdenticalGo (Hol aNam aCtx) b dep =
(envPure True)
termIdenticalGo a (Hol bNam bCtx) dep =
(envPure True)
termIdenticalGo U60 U60 dep =
(envPure True)
termIdenticalGo (Num aVal) (Num bVal) dep =
(envPure (eq aVal bVal))
termIdenticalGo (Op2 aOpr aFst aSnd) (Op2 bOpr bFst bSnd) dep =
(envBind (termIdentical aFst bFst dep) λiFst
(envBind (termIdentical aSnd bSnd dep) λiSnd
(envPure (and iFst iSnd))))
termIdenticalGo (Swi aNam aX aZ aS aP) (Swi bNam bX bZ bS bP) dep =
(envBind (termIdentical aX bX dep) λiX
(envBind (termIdentical aZ bZ dep) λiZ
(envBind (termIdentical (aS (Var (stringConcat aNam "-1") dep)) (bS (Var (stringConcat bNam "-1") dep)) dep) λiS
(envBind (termIdentical (aP (Var aNam dep)) (bP (Var bNam dep)) dep) λiP
(envPure (and (and (and iX iZ) iS) iP))))))
termIdenticalGo (Txt aTxt) (Txt bTxt) dep =
(envPure (stringEqual aTxt bTxt))
termIdenticalGo (Nat aVal) (Nat bVal) dep =
(envPure (eq aVal bVal))
termIdenticalGo (Src aSrc aVal) b dep =
(termIdentical aVal b dep)
termIdenticalGo a (Src bSrc bVal) dep =
(termIdentical a bVal dep)
termIdenticalGo (Ref aNam aVal) (Ref bNam bVal) dep =
(envPure (stringEqual aNam bNam))
termIdenticalGo (Var aNam aIdx) (Var bNam bIdx) dep =
(envPure (eq aIdx bIdx))
termIdenticalGo a b dep =
(envPure False)
// Unification
// -----------
// The unification algorithm is a simple pattern unifier, based on smalltt:
// > https://github.com/AndrasKovacs/elaboration-zoo/blob/master/03-holes/Main.hs
// The pattern unification problem provides a solution to the following problem:
// (?X x y z ...) = K
// When:
// 1. The LHS spine, `x y z ...`, consists of distinct variables.
// 2. Every free var of the RHS, `K`, occurs in the spine.
// 3. The LHS hole, `?A`, doesn't occur in the RHS, `K`.
// If these conditions are met, ?X is solved as:
// ?X = λx λy λz ... K
// In this implementation, checking condition `2` is not necessary, because we
// subst holes directly where they occur (rather than on top-level definitions),
// so, it is impossible for unbound variables to appear.
// If possible, solves a `(?X x y z ...) = K` problem, generating a subst.
// termUnify :: U60 -> [Term] -> Term -> U60 -> Env Bool
termUnify uid spn b dep =
(envBind envGetFill λfill
let unsolved = (not (mapHas (key uid) fill))
let solvable = (termUnifyValid fill spn [])
let no_loops = (not (termUnifyIsRec fill uid b dep))
(If (and (and unsolved solvable) no_loops)
let solution = (termUnifySolve fill uid spn b)
// (trace (stringJoin ["solve: ", (u60Show uid), " ", (termShow solution dep)])
(envBind (envFill uid solution) λ_
(envPure True))
(envPure match b {
(Met bUid bSpn): (envPure (eq uid bUid))
other : (envPure False)
})))
// Checks if an problem is solveable by pattern unification.
// termUnifyValid :: Map Term -> [Term] -> [U60] -> Bool
termUnifyValid fill [] vars = True
termUnifyValid fill (List.cons x spn) vars = match (termReduce fill 0 x) {
(Var nam idx): (not (and (elem eq idx vars) (termUnifyValid fill spn (List.cons idx vars))))
otherwise : False
}
// Generates the solution, adding binders and renaming variables.
// termUnifySolve :: Map Term -> U60 -> [Term] -> Term -> Term
termUnifySolve fill uid [] b = b
termUnifySolve fill uid (List.cons x spn) b = match (termReduce fill 0 x) {
(Var nam idx): (Lam nam λx (termUnifySubst idx x (termUnifySolve fill uid spn b)))
otherwise : (trace "unreachable" Unreachable)
}
// Checks if a hole uid occurs recursively inside a term
// termUnifyIsRec :: Map Term -> Int -> Term -> Int -> Bool
termUnifyIsRec fill uid (All nam inp bod) dep = (or (termUnifyIsRec fill uid inp dep) (termUnifyIsRec fill uid (bod (Var nam dep)) (+ dep 1)))
termUnifyIsRec fill uid (Lam nam bod) dep = (or (termUnifyIsRec fill uid (bod (Var nam dep)) (+ dep 1)))
termUnifyIsRec fill uid (App fun arg) dep = (or (termUnifyIsRec fill uid fun dep) (termUnifyIsRec fill uid arg dep))
termUnifyIsRec fill uid (Ann chk val typ) dep = (or (termUnifyIsRec fill uid val dep) (termUnifyIsRec fill uid typ dep))
termUnifyIsRec fill uid (Slf nam typ bod) dep = (or (termUnifyIsRec fill uid typ dep) (termUnifyIsRec fill uid (bod (Var nam dep)) (+ dep 1)))
termUnifyIsRec fill uid (Ins val) dep = (or (termUnifyIsRec fill uid val dep))
termUnifyIsRec fill uid (Let nam val bod) dep = (or (termUnifyIsRec fill uid val dep) (termUnifyIsRec fill uid (bod (Var nam dep)) (+ dep 1)))
termUnifyIsRec fill uid (Use nam val bod) dep = (or (termUnifyIsRec fill uid val dep) (termUnifyIsRec fill uid (bod (Var nam dep)) (+ dep 1)))
termUnifyIsRec fill uid (Hol nam ctx) dep = False
termUnifyIsRec fill uid (Op2 opr fst snd) dep = (or (termUnifyIsRec fill uid fst dep) (termUnifyIsRec fill uid snd dep))
termUnifyIsRec fill uid (Swi nam x z s p) dep = (or (termUnifyIsRec fill uid x dep) (or (termUnifyIsRec fill uid z dep) (or (termUnifyIsRec fill uid (s (Var (stringConcat nam "-1") dep)) (+ dep 1)) (termUnifyIsRec fill uid (p (Var nam dep)) dep))))
termUnifyIsRec fill uid (Src src val) dep = (termUnifyIsRec fill uid val dep)
termUnifyIsRec fill uid (Met bUid bSpn) dep = match (termReduceMet fill 2 bUid bSpn) {
(Met bUid bSpn): (eq uid bUid)
term : (termUnifyIsRec fill uid term dep)
}
termUnifyIsRec fill uid _ dep = False
// Substitutes a Bruijn level variable by a `neo` value in `term`.
// termUnifySubst :: U60 -> Term -> Term -> Term
// termUnifySubst lvl neo term = term
termUnifySubst lvl neo (All nam inp bod) = (All nam (termUnifySubst lvl neo inp) (λx (termUnifySubst lvl neo (bod x))))
termUnifySubst lvl neo (Lam nam bod) = (Lam nam (λx (termUnifySubst lvl neo (bod x))))
termUnifySubst lvl neo (App fun arg) = (App (termUnifySubst lvl neo fun) (termUnifySubst lvl neo arg))
termUnifySubst lvl neo (Ann chk val typ) = (Ann chk (termUnifySubst lvl neo val) (termUnifySubst lvl neo typ))
termUnifySubst lvl neo (Slf nam typ bod) = (Slf nam (termUnifySubst lvl neo typ) (λx (termUnifySubst lvl neo (bod x))))
termUnifySubst lvl neo (Ins val) = (Ins (termUnifySubst lvl neo val))
termUnifySubst lvl neo (Ref nam val) = (Ref nam (termUnifySubst lvl neo val))
termUnifySubst lvl neo (Let nam val bod) = (Let nam (termUnifySubst lvl neo val) (λx (termUnifySubst lvl neo (bod x))))
termUnifySubst lvl neo (Use nam val bod) = (Use nam (termUnifySubst lvl neo val) (λx (termUnifySubst lvl neo (bod x))))
termUnifySubst lvl neo (Met uid spn) = (Met uid (map (termUnifySubst lvl neo) spn))
termUnifySubst lvl neo (Hol nam ctx) = (Hol nam (map (termUnifySubst lvl neo) ctx))
termUnifySubst lvl neo Set = Set
termUnifySubst lvl neo U60 = U60
termUnifySubst lvl neo (Num n) = (Num n)
termUnifySubst lvl neo (Op2 opr fst snd) = (Op2 opr (termUnifySubst lvl neo fst) (termUnifySubst lvl neo snd))
termUnifySubst lvl neo (Swi nam x z s p) = (Swi nam (termUnifySubst lvl neo x) (termUnifySubst lvl neo z) (λk (termUnifySubst lvl neo (s k))) (λk (termUnifySubst lvl neo (p k))))
termUnifySubst lvl neo (Txt txt) = (Txt txt)
termUnifySubst lvl neo (Nat val) = (Nat val)
termUnifySubst lvl neo (Var nam idx) = (if (== lvl idx) neo (Var nam idx))
termUnifySubst lvl neo (Src src val) = (Src src (termUnifySubst lvl neo val))
// Type-Checking
// -------------
// termIfAll :: Term -> (String -> Term -> (Term -> Term) -> a) -> a -> a
termIfAll (All nam inp bod) yep _ = (yep nam inp bod)
termIfAll _ _ nop = nop
// termIfSlf :: Term -> (String -> Term -> (Term -> Term) -> a) -> a -> a
termIfSlf (Slf nam typ bod) yep _ = (yep nam typ bod)
termIfSlf _ _ nop = nop
// termInfer :: Term -> U60 -> Env Term
termInfer term dep =
// trace (stringJoin ["infer: ", (termShow term dep)])
(termInferGo term dep)
// termInferGo :: Term -> U60 -> Env Term
termInferGo (All nam inp bod) dep =
(envBind (envSusp (Check 0 inp Set dep)) λ_
(envBind (envSusp (Check 0 (bod (Ann False (Var nam dep) inp)) Set (+ dep 1))) λ_
(envPure Set)))
termInferGo (App fun arg) dep =
(envBind (termInfer fun dep) λftyp
(envBind envGetFill λfill
match (termReduce fill 2 ftyp) {
(All ftyp_nam ftyp_inp ftyp_bod):
(envBind (envSusp (Check 0 arg ftyp_inp dep)) λ_
(envPure (ftyp_bod arg)))
otherwise:
(envBind (envLog (Error 0 (Hol "function" []) ftyp (App fun arg) dep)) λ_
envFail)
}))
termInferGo (Ann chk val typ) dep =
(envBind (If chk
(termCheck 0 val typ dep)
(envPure *)) λ_
(envPure typ))
termInferGo (Slf nam typ bod) dep =
(envBind (envSusp (Check 0 (bod (Ann False (Var nam dep) typ)) Set (+ dep 1))) λ_
(envPure Set))
termInferGo (Ins val) dep =
(envBind (termInfer val dep) λvtyp
(envBind envGetFill λfill
match (termReduce fill 2 vtyp) {
(Slf vtyp_nam vtyp_typ vtyp_bod):
(envPure (vtyp_bod (Ins val)))
otherwise:
(envBind (envLog (Error 0 (Hol "self-type" []) vtyp (Ins val) dep)) λ_
envFail)
}))
termInferGo (Ref nam val) dep =
(termInfer val dep)
termInferGo Set dep =
(envPure Set)
termInferGo U60 dep =
(envPure Set)
termInferGo (Num num) dep =
(envPure U60)
termInferGo (Txt txt) dep =
(envPure Book.String)
termInferGo (Nat val) dep =
(envPure Book.Nat)
termInferGo (Op2 opr fst snd) dep =
(envBind (envSusp (Check 0 fst U60 dep)) λ_
(envBind (envSusp (Check 0 snd U60 dep)) λ_
(envPure U60)))
termInferGo (Swi nam x z s p) dep =
(envBind (envSusp (Check 0 x U60 dep)) λ_
(envBind (envSusp (Check 0 (p (Ann False (Var nam dep) U60)) Set dep)) λ_
(envBind (envSusp (Check 0 z (p (Num 0)) dep)) λ_
(envBind (envSusp (Check 0 (s (Ann False (Var (stringConcat nam "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (stringConcat nam "-1") dep))) (+ dep 1))) λ_
(envPure (p x))))))
termInferGo (Let nam val bod) dep =
(envBind (termInfer val dep) λtyp
(termInfer (bod (Ann False (Var nam dep) typ)) dep))
termInferGo (Use nam val bod) dep =
(termInfer (bod val) dep)
termInferGo (Lam nam bod) dep =
(envBind (envLog (Error 0 (Hol "type_annotation" []) (Hol "untyped_lambda" []) (Lam nam bod) dep)) λ_
envFail)
termInferGo (Hol nam ctx) dep =
(envBind (envLog (Error 0 (Hol "type_annotation" []) (Hol "untyped_hole" []) (Hol nam ctx) dep)) λ_
envFail)
termInferGo (Met uid spn) dep =
(envBind (envLog (Error 0 (Hol "type_annotation" []) (Hol "untyped_meta" []) (Met uid spn) dep)) λ_
envFail)
termInferGo (Var nam idx) dep =
(envBind (envLog (Error 0 (Hol "type_annotation" []) (Hol "untyped_variable" []) (Var nam idx) dep)) λ_
envFail)
termInferGo (Src src val) dep =
(termInfer val dep)
// termCheck :: U60 -> Term -> Term -> U60 -> Env *
termCheck src val typ dep =
// (trace (stringJoin ["check: ", (termShow val dep), "\n :: ", (termShow typ dep)])
(termCheckGo src val typ dep)
// termCheckGo :: U60 -> Term -> Term -> U60 -> Env *
termCheckGo src (Lam termNam termBod) typx dep =
(envBind envGetFill λfill
match (termReduce fill 2 typx) {
(All typeNam typeInp typeBod):
let ann = (Ann False (Var termNam dep) typeInp)
let term = (termBod ann)
let typx = (typeBod ann)
(termCheck 0 term typx (+ dep 1))
otherwise:
(envBind (termInfer (Lam termNam termBod) dep) λ_
(envPure *))
})
termCheckGo src (Ins termVal) typx dep =
(envBind envGetFill λfill
match (termReduce fill 2 typx) {
(Slf typeNam typeTyp typeBod):
(termCheck 0 termVal (typeBod (Ins termVal)) dep)
_:
(envBind (termInfer (Ins termVal) dep) λ_
(envPure *))
})
termCheckGo src (Let termNam termVal termBod) typx dep =
(envBind (termInfer termVal dep) λtermTyp
(termCheck 0 (termBod (Ann False (Var termNam dep) termTyp)) typx dep))
termCheckGo src (Use termNam termVal termBod) typx dep =
(termCheck 0 (termBod termVal) typx dep)
termCheckGo src (Hol termNam termCtx) typx dep =
(envBind (envLog (Found termNam typx termCtx dep)) λ_
(envPure *))
termCheckGo src (Met uid spn) typx dep =
(envPure *)
termCheckGo src (Ann chk val typ) typx dep =
(envBind (termCheckCompare src val typ typx dep) λ_
(If chk
(termCheck src val typ dep)
(envPure *)))
// termCheckGo src (Ref termNam (Ann termVal termTyp)) typx dep =
// (envBind (termEqual typx termTyp dep) λequal
// (termCheckReport src equal termTyp typx termVal dep)
termCheckGo src (Src termSrc termVal) typx dep =
(termCheck termSrc termVal typx dep)
termCheckGo src term typx dep =
(envBind (termInfer term dep) λinfer
(termCheckCompare src term typx infer dep))
termCheckCompare src term expected detected dep =
(envBind (termEqual expected detected dep) λequal
(If equal
(envBind envTakeSusp λsusp
(envBind (listCheck susp) λ_
(envPure *)))
(envBind (envLog (Error src expected detected term dep)) λ_
envFail)))
// listCheck :: [a] -> Env *
listCheck [] = (envPure *)
listCheck (List.cons x xs) =
let (Check src val typ dep) = x;
(envBind (termCheck src val typ dep) λ_ (listCheck xs))
// termCheckReport :: U60 -> Bool -> Term -> Term -> Term -> U60 -> Env *
// termCheckReport src False detected expected value dep =
// (envLog (Error src detected expected value dep)
// envFail)
// termCheckReport src True detected expected value dep =
// (envPure *)
// termCheckDef :: Term -> Env *
termCheckDef (Ref nam (Ann chk val typ)) = (envBind (termCheck 0 val typ 0) λ_ (envPure *))
termCheckDef (Ref nam val) = (envBind (termInfer val 0) λ_ (envPure *))
termCheckDef other = (trace "invalid top-level definition" InvalidTopLevelDefinition)
// Stringification
// ---------------
// termShow :: Term -> U60 -> String
termShow (All nam inp bod) dep =
let nam_ = nam
let inp_ = (termShow inp dep)
let bod_ = (termShow (bod (Var nam dep)) (+ dep 1))
(stringJoin ["∀(", nam_, ": ", inp_, ") ", bod_])
termShow (Lam nam bod) dep =
let nam_ = nam
let bod_ = (termShow (bod (Var nam dep)) (+ dep 1))
(stringJoin ["λ", nam_, " ", bod_])
termShow (App fun arg) dep =
let fun_ = (termShow fun dep)
let arg_ = (termShow arg dep)
(stringJoin ["(", fun_, " ", arg_, ")"])
termShow (Ann chk val typ) dep =
let val_ = (termShow val dep)
let typ_ = (termShow typ dep)
(stringJoin ["{", val_, ": ", typ_, "}"])
termShow (Slf nam typ bod) dep =
(termShow typ dep)
termShow (Ins val) dep =
let val_ = (termShow val dep)
(stringJoin ["~", val_])
termShow (Ref nam val) dep = nam
termShow (Let nam val bod) dep =
let nam_ = nam
let val_ = (termShow val dep)
let bod_ = (termShow (bod (Var nam dep)) (+ dep 1))
(stringJoin ["let ", nam_, " = ", val_, "; ", bod_])
termShow (Use nam val bod) dep =
let nam_ = nam
let val_ = (termShow val dep)
let bod_ = (termShow (bod (Var nam dep)) (+ dep 1))
(stringJoin ["use ", nam_, " = ", val_, "; ", bod_])
termShow Set dep = "*"
termShow U60 dep = "U60"
termShow (Num val) dep =
let val_ = (u60Show val)
(stringJoin [val_])
termShow (Op2 opr fst snd) dep =
let opr_ = (operShow opr)
let fst_ = (termShow fst dep)
let snd_ = (termShow snd dep)
(stringJoin ["(", opr_, " ", fst_, " ", snd_, ")"])
termShow (Swi nam x z s p) dep =
let nam_ = nam
let x_ = (termShow x dep)
let z_ = (termShow z dep)
let s_ = (termShow (s (Var (stringConcat nam "-1") dep)) (+ dep 1))
let p_ = (termShow (p (Var nam dep)) dep)
(stringJoin ["switch ", nam_, " = ", x_, " { 0: ", z_, " _: ", s_, " }: ", p_])
termShow (Txt txt) dep = (stringJoin [quote, txt, quote])
termShow (Nat val) dep = (u60Show val)
termShow (Hol nam ctx) dep = (stringJoin ["?", nam])
termShow (Met uid spn) dep = (stringJoin ["(_", (termShowSpn (reverse spn) dep), ")"])
termShow (Var nam idx) dep = nam
// termShow (Var nam idx) dep = stringJoin [nam, "^", (u60Show idx)]
termShow (Src src val) dep = (termShow val dep)
// termShow (Src src val) dep = stringJoin ["!", (termShow val dep)]
// termShowSpn :: [Term] -> U60 -> String
termShowSpn [] dep = ""
termShowSpn (List.cons x xs) dep = (stringJoin [" ", (termShow x dep), (termShowSpn xs dep)])
// operShow :: Oper -> String
operShow ADD = "+"
operShow SUB = "-"
operShow MUL = "*"
operShow DIV = "/"
operShow MOD = "%"
operShow EQ = "=="
operShow NE = "!="
operShow LT = "<"
operShow GT = ">"
operShow LTE = "<="
operShow GTE = ">="
operShow AND = "&"
operShow OR = "|"
operShow XOR = "^"
operShow LSH = "<<"
operShow RSH = ">>"
// contextShow :: Map Term -> [Term] -> U60 -> String
contextShow fill [] dep = ""
contextShow fill (List.cons x xs) dep = (stringJoin [" ", (contextShowAnn fill x dep), (contextShow fill xs dep)])
// contextShowAnn :: Map Term -> Term -> U60 -> String
contextShowAnn fill (Ann chk val typ) dep = (stringJoin ["{", (termShow (termNormal fill 0 val dep) dep), ": ", (termShow (termNormal fill 0 typ dep) dep), "}"])
contextShowAnn fill term dep = (termShow (termNormal fill 0 term dep) dep)
// infoShow :: Map Term -> Info -> String
infoShow fill (Found name typ ctx dep) =
let typ_ = (termShow (termNormal fill 1 typ dep) dep)
let ctx_ = (stringTail (contextShow fill ctx dep))
(stringJoin ["#found{", name, " ", typ_, " [", ctx_, "]}"])
infoShow fill (Error src expected detected value dep) =
let exp = (termShow (termNormal fill 1 expected dep) dep)
let det = (termShow (termNormal fill 1 detected dep) dep)
let val = (termShow (termNormal fill 0 value dep) dep)
(stringJoin ["#error{", exp, " ", det, " ", val, " ", (u60Show src), "}"])
infoShow fill (Solve name term dep) =
let term_ = (termShow (termNormal fill 1 term dep) dep)
(stringJoin ["#solve{", name, " ", term_, "}"])
infoShow fill (Vague name) =
(stringJoin ["#vague{", name, "}"])
infoShow fill (Print value dep) =
let val = (termShow (termNormal fill 0 value dep) dep)
(stringJoin ["#print{", val, "}"])
// API
// ---
// Normalizes a term
// apiNormal :: Term -> IO *
apiNormal term = (putStrLn (infoShow mapNew (Print (termNormal mapNew 2 term 0) 0)) *)
// apiCheck :: Term -> IO *
apiCheck term = match (envRun (termCheckDef term)) {
(Done state value): (apiPrintLogs state)
(Fail state) : (apiPrintLogs state)
}
// apiPrintLogs :: State -> IO *
apiPrintLogs (State fill susp (List.cons log logs)) =
(putStrLn (infoShow fill log)
(apiPrintLogs (State fill susp logs)))
apiPrintLogs (State fill susp []) =
*
putStrLn = HVM.print
trace = HVM.print

1216
src/kindc.hs Normal file
View File

File diff suppressed because it is too large Load Diff

16
src/kindc.rs Normal file
View File

@ -0,0 +1,16 @@
use std::process::Command;
use std::path::PathBuf;
fn main() {
let kindc_path = PathBuf::from(env!("CARGO_MANIFEST_DIR"))
.join("target")
.join("kindc");
let args: Vec<String> = std::env::args().skip(1).collect();
Command::new(kindc_path)
.args(&args)
.status()
.expect("Failed to run kindc");
}

1
src/main.kindc Normal file
View File

@ -0,0 +1 @@
main : ∀(P: *) ∀(x: P) P = λP λx x;

152
src/main.rs
View File

@ -1,24 +1,6 @@
// PROJECT FILES:
//./term/mod.rs//
//./term/show.rs//
//./term/parse.rs//
//./term/compile.rs//
//./sugar/mod.rs//
//./show/mod.rs//
//./info/mod.rs//
//./info/parse.rs//
//./info/show.rs//
//./book/mod.rs//
//./book/compile.rs//
//./book/parse.rs//
//./book/show.rs//
// PROJECT CLI (main.rs):
use clap::{Arg, ArgAction, Command};
use std::fs;
use std::io::Write;
use std::path::PathBuf;
use std::process::Command as SysCommand;
mod book;
@ -38,84 +20,40 @@ use TSPL::Parser;
TSPL::new_parser!(KindParser);
fn generate_check_hvm2(book: &Book, command: &str, arg: &str) -> String {
let kind_hvm2 = include_str!("./kind2.hvm2");
let book_hvm2 = book.to_hvm2_checker();
let main_hvm2 = match command {
"check" => format!("main = (apiCheck Book.{})\n", arg.replace("/", ".")),
"run" => format!("main = (apiNormal Book.{})\n", arg.replace("/", ".")),
_ => panic!("invalid command"),
};
format!("{}\n{}\n{}", kind_hvm2, book_hvm2, main_hvm2)
fn generate_kindc(book: &Book, arg: &str) -> String {
let book_kindc = book.to_kindc();
let main_kindc = format!("main = {};\n", Term::to_kindc_name(arg));
format!("{}{}", book_kindc, main_kindc)
}
fn generate_check_hs(book: &Book, command: &str, arg: &str) -> String {
let kind_hs = include_str!("./kind2.hs")
.lines()
.filter(|line| !line.starts_with("xString"))
.collect::<Vec<_>>()
.join("\n");
let book_hs = book.to_hs_checker();
let main_hs = match command {
"check" => format!("main = (apiCheck {})\n", Term::to_hs_name(arg)),
"run" => format!("main = (apiNormal {})\n", Term::to_hs_name(arg)),
_ => panic!("invalid command"),
};
format!("{}\n{}\n{}", kind_hs, book_hs, main_hs)
}
fn generate_hvm2(book: &Book, arg: &str) -> String {
let book_hvm2 = book.to_hvm2();
let main_hvm2 = format!("main = {}\n", Term::to_hvm2_name(arg));
format!("{}\n{}", book_hvm2, main_hvm2)
}
fn run_kore(book: &Book, cmd: &str, file: &str, runtime: &str) -> (Vec<Info>, String) {
let command = match runtime {
"hs" => {
let check_hs = generate_check_hs(&book, cmd, file);
let mut file = fs::File::create(".check.hs").expect("Failed to create '.check.hs'.");
file.write_all(check_hs.as_bytes()).expect("Failed to write '.check.hs'.");
SysCommand::new("runghc").arg(".check.hs").output().expect("Failed to execute command")
}
"hvm2" => {
let check_hvm2 = generate_check_hvm2(&book, cmd, file);
let mut file = fs::File::create(".check.hvm2").expect("Failed to create '.check.hvm2'.");
file.write_all(check_hvm2.as_bytes()).expect("Failed to write '.check.hvm2'.");
SysCommand::new("hvml").arg("run").arg("-L").arg(".check.hvm2").output().expect("Failed to execute command")
}
_ => panic!("invalid runtime"),
};
let stdout = String::from_utf8_lossy(&command.stdout);
let stderr = String::from_utf8_lossy(&command.stderr);
fn run_kindc(book: &Book, cmd: &str, file: &str) -> (Vec<Info>, String) {
let kindc_content = generate_kindc(book, file);
let mut temp_file = fs::File::create(".main.kindc").expect("Failed to create '.main.kindc'.");
temp_file.write_all(kindc_content.as_bytes()).expect("Failed to write '.main.kindc'.");
let output = SysCommand::new("kindc").arg(cmd).arg(".main.kindc").output().expect("Failed to execute kindc command");
let stdout = String::from_utf8_lossy(&output.stdout);
let stderr = String::from_utf8_lossy(&output.stderr);
(Info::parse_infos(&stdout), stderr.to_string())
}
fn check(name: &str, runtime: &str) {
fn check(name: &str) {
let book = load_book(name);
let (infos, stderr) = run_kore(&book, "check", name, runtime);
let (infos, stderr) = run_kindc(&book, "check", name);
for info in &infos {
println!("{}", info.pretty(&book));
}
if stderr.is_empty() && infos.is_empty() {
println!("check!");
}
eprintln!("{stderr}");
}
fn normal(name: &str, _level: u32, runtime: &str) {
fn normal(name: &str, _level: u32) {
let book = load_book(name);
let (infos, stderr) = run_kore(&book, "run", name, runtime);
let (infos, stderr) = run_kindc(&book, "run", name);
for info in &infos {
println!("{}", info.pretty(&book));
}
eprintln!("{stderr}");
}
@ -132,46 +70,10 @@ fn auto_format(file_name: &str) {
fn compile(name: &str) {
let book = load_book(name);
let code = generate_hvm2(&book, name);
let code = generate_kindc(&book, name);
println!("{code}");
}
fn compare_runtimes() {
let book_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("book");
let mut paths: Vec<_> = fs::read_dir(&book_dir)
.expect("failed to read book directory")
.map(|r| r.expect("failed to read entry").path())
.filter_map(|r| r.extension().is_some_and(|e| e == "kind2").then_some(r))
.collect();
paths.sort();
for path in paths {
let name = path.file_stem().unwrap().to_str().unwrap();
let Some(book) = Book::boot(book_dir.to_str().unwrap(), name).ok() else {
continue;
};
print!("{name:<30}: ");
for rt in ["hs", "hvm2"] {
std::io::stdout().flush().expect("failed to flush stdout");
let (infos, stderr) = run_kore(&book, "check", name, rt);
if stderr.is_empty() {
if infos.is_empty() {
print!("\x1b[32;1m+\x1b[0m ");
} else {
print!("\x1b[31;1m-\x1b[0m ");
}
} else {
print!("\x1b[33;1m*\x1b[0m ");
}
}
println!();
}
}
fn load_book(name: &str) -> Book {
let cwd = std::env::current_dir().expect("failed to get current directory");
Book::boot(cwd.to_str().unwrap(), name).unwrap_or_else(|e| {
@ -187,11 +89,7 @@ fn main() {
.arg_required_else_help(true)
.subcommand(Command::new("check")
.about("Type-checks a term")
.arg(Arg::new("name").required(true))
.arg(Arg::new("runtime")
.long("use")
.value_parser(["hs", "hvm2"])
.default_value("hs")))
.arg(Arg::new("name").required(true)))
.subcommand(Command::new("normal")
.about("Normalizes a term")
.arg(Arg::new("name").required(true))
@ -199,31 +97,24 @@ fn main() {
.long("level")
.short('l')
.action(ArgAction::Set)
.value_parser(clap::value_parser!(u32)))
.arg(Arg::new("runtime")
.long("use")
.value_parser(["hs", "hvm2"])
.default_value("hs")))
.value_parser(clap::value_parser!(u32))))
.subcommand(Command::new("format")
.about("Auto-formats a file")
.arg(Arg::new("name").required(true)))
.subcommand(Command::new("compile")
.about("Compiles to HVM2")
.about("Compiles to KINDC")
.arg(Arg::new("name").required(true)))
.subcommand(Command::new("compare").about("Runs internal comparison tests"))
.get_matches();
match matches.subcommand() {
Some(("check", sub_matches)) => {
let name = sub_matches.get_one::<String>("name").expect("required");
let runtime = sub_matches.get_one::<String>("runtime").expect("defaulted");
check(name, runtime);
check(name);
}
Some(("normal", sub_matches)) => {
let name = sub_matches.get_one::<String>("name").expect("required");
let level = sub_matches.get_one::<u32>("level").copied().unwrap_or(0);
let runtime = sub_matches.get_one::<String>("runtime").expect("defaulted");
normal(name, level, runtime);
normal(name, level);
}
Some(("format", sub_matches)) => {
let name = sub_matches.get_one::<String>("name").expect("required");
@ -233,7 +124,6 @@ fn main() {
let name = sub_matches.get_one::<String>("name").expect("required");
compile(name);
}
Some(("compare", _)) => compare_runtimes(),
_ => unreachable!(),
}
}

285
src/term/compile.rs
View File

@ -1,7 +1,6 @@
use crate::{*};
impl Oper {
pub fn to_ctr(&self) -> &'static str {
match self {
Oper::Add => "ADD",
@ -43,213 +42,9 @@ impl Oper {
Oper::Rsh => ">>",
}
}
pub fn to_hvm1_checker(&self) -> &'static str {
self.to_ctr()
}
pub fn to_hvm2_checker(&self) -> &'static str {
self.to_ctr()
}
pub fn to_hs_checker(&self) -> &'static str {
self.to_ctr()
}
}
impl Term {
pub fn to_hvm1_checker(&self, _env: im::Vector<String>, _met: &mut usize) -> String {
todo!()
}
pub fn to_hvm2_checker(&self, env: im::Vector<String>, met: &mut usize) -> String {
fn binder(name: &str) -> String {
format!("x{}", name.replace("-", "._.").replace("/", "."))
}
match self {
Term::All { era: _, nam, inp, bod } => {
let inp = inp.to_hvm2_checker(env.clone(), met);
let bod = bod.to_hvm2_checker(cons(&env, nam.clone()), met);
format!("(All \"{}\" {} λ{} {})", nam, inp, binder(nam), bod)
}
Term::Lam { era: _, nam, bod } => {
let bod = bod.to_hvm2_checker(cons(&env, nam.clone()), met);
format!("(Lam \"{}\" λ{} {})", nam, binder(nam), bod)
}
Term::App { era: _, fun, arg } => {
let fun = fun.to_hvm2_checker(env.clone(), met);
let arg = arg.to_hvm2_checker(env.clone(), met);
format!("(App {} {})", fun, arg)
}
Term::Ann { chk, val, typ } => {
let val = val.to_hvm2_checker(env.clone(), met);
let typ = typ.to_hvm2_checker(env.clone(), met);
format!("(Ann {} {} {})", if *chk { "True" } else { "False" }, val, typ)
}
Term::Slf { nam, typ, bod } => {
let typ = typ.to_hvm2_checker(env.clone(), met);
let bod = bod.to_hvm2_checker(cons(&env, nam.clone()), met);
format!("(Slf \"{}\" {} λ{} {})", nam, typ, binder(nam), bod)
}
Term::Ins { val } => {
let val = val.to_hvm2_checker(env.clone(), met);
format!("(Ins {})", val)
}
Term::Set => "(Set)".to_string(),
Term::U60 => "(U60)".to_string(),
Term::Num { val } => {
format!("(Num {})", val)
}
Term::Op2 { opr, fst, snd } => {
let fst = fst.to_hvm2_checker(env.clone(), met);
let snd = snd.to_hvm2_checker(env.clone(), met);
format!("(Op2 {} {} {})", opr.to_hvm2_checker(), fst, snd)
}
Term::Swi { nam, x, z, s, p } => {
let x = x.to_hvm2_checker(env.clone(), met);
let z = z.to_hvm2_checker(env.clone(), met);
let s = s.to_hvm2_checker(cons(&env, format!("{}-1", nam)), met);
let p = p.to_hvm2_checker(cons(&env, nam.clone()), met);
format!("(Swi \"{}\" {} {} λ{} {} λ{} {})", nam, x, z, binder(&format!("{}-1", nam)), s, binder(nam), p)
}
Term::Let { nam, val, bod } => {
let val = val.to_hvm2_checker(env.clone(), met);
let bod = bod.to_hvm2_checker(cons(&env, nam.clone()), met);
format!("(Let \"{}\" {} λ{} {})", nam, val, binder(nam), bod)
}
Term::Use { nam, val, bod } => {
let val = val.to_hvm2_checker(env.clone(), met);
let bod = bod.to_hvm2_checker(cons(&env, nam.clone()), met);
format!("(Use \"{}\" {} λ{} {})", nam, val, binder(nam), bod)
}
Term::Hol { nam } => {
let env_str = env.iter().map(|n| binder(n)).collect::<Vec<_>>().join(",");
format!("(Hol \"{}\" [{}])", nam, env_str)
}
Term::Met {} => {
let uid = *met;
*met += 1;
format!("(Met {} [])", uid)
}
Term::Var { nam } => {
if env.contains(nam) {
format!("{}", binder(nam))
} else {
format!("(Book.{})", nam.replace("/", "."))
}
}
Term::Src { src, val } => {
let val = val.to_hvm2_checker(env, met);
format!("(Src {} {})", src.to_u64(), val)
}
Term::Nat { nat } => {
format!("(Nat {})", nat)
}
Term::Txt { txt } => {
format!("(Txt \"{}\")", txt.replace("\n", "\\n"))
}
Term::Mch { .. } => {
unreachable!()
}
}
}
pub fn to_hs_name(name: &str) -> String {
format!("x{}", name.replace("-", "_").replace(".","_").replace("/","_"))
}
pub fn to_hs_checker(&self, env: im::Vector<String>, met: &mut usize) -> String {
match self {
Term::All { era: _, nam, inp, bod } => {
let inp = inp.to_hs_checker(env.clone(), met);
let bod = bod.to_hs_checker(cons(&env, nam.clone()), met);
format!("(All \"{}\" {} $ \\{} -> {})", nam, inp, Term::to_hs_name(nam), bod)
},
Term::Lam { era: _, nam, bod } => {
let bod = bod.to_hs_checker(cons(&env, nam.clone()), met);
format!("(Lam \"{}\" $ \\{} -> {})", nam, Term::to_hs_name(nam), bod)
},
Term::App { era: _, fun, arg } => {
let fun = fun.to_hs_checker(env.clone(), met);
let arg = arg.to_hs_checker(env.clone(), met);
format!("(App {} {})", fun, arg)
},
Term::Ann { chk, val, typ } => {
let val = val.to_hs_checker(env.clone(), met);
let typ = typ.to_hs_checker(env.clone(), met);
format!("(Ann {} {} {})", if *chk { "True" } else { "False" }, val, typ)
},
Term::Slf { nam, typ, bod } => {
let typ = typ.to_hs_checker(env.clone(), met);
let bod = bod.to_hs_checker(cons(&env, nam.clone()), met);
format!("(Slf \"{}\" {} $ \\{} -> {})", nam, typ, Term::to_hs_name(nam), bod)
},
Term::Ins { val } => {
let val = val.to_hs_checker(env.clone(), met);
format!("(Ins {})", val)
},
Term::Set => {
"(Set)".to_string()
},
Term::U60 => {
"(U60)".to_string()
},
Term::Num { val } => {
format!("(Num {})", val)
},
Term::Op2 { opr, fst, snd } => {
let fst = fst.to_hs_checker(env.clone(), met);
let snd = snd.to_hs_checker(env.clone(), met);
format!("(Op2 {} {} {})", opr.to_hs_checker(), fst, snd)
},
Term::Swi { nam, x, z, s, p } => {
let x = x.to_hs_checker(env.clone(), met);
let z = z.to_hs_checker(env.clone(), met);
let s = s.to_hs_checker(cons(&env, format!("{}-1", nam)), met);
let p = p.to_hs_checker(cons(&env, nam.clone()), met);
format!("(Swi \"{}\" {} {} (\\{} -> {}) (\\{} -> {}))", nam, x, z, Term::to_hs_name(&format!("{}-1", nam)), s, Term::to_hs_name(nam), p)
},
Term::Let { nam, val, bod } => {
let val = val.to_hs_checker(env.clone(), met);
let bod = bod.to_hs_checker(cons(&env, nam.clone()), met);
format!("(Let \"{}\" {} $ \\{} -> {})", nam, val, Term::to_hs_name(nam), bod)
},
Term::Use { nam, val, bod } => {
let val = val.to_hs_checker(env.clone(), met);
let bod = bod.to_hs_checker(cons(&env, nam.clone()), met);
format!("(Use \"{}\" {} $ \\{} -> {})", nam, val, Term::to_hs_name(nam), bod)
},
Term::Hol { nam } => {
let env_str = env.iter().map(|n| Term::to_hs_name(n)).collect::<Vec<_>>().join(",");
format!("(Hol \"{}\" [{}])", nam, env_str)
},
Term::Met {} => {
let uid = *met;
*met += 1;
format!("(Met {} [])", uid)
//format!("(Met {} [{}])", uid, env.iter().rev().map(|n| Term::to_hs_name(n)).collect::<Vec<_>>().join(","))
},
Term::Var { nam } => {
format!("{}", Term::to_hs_name(nam))
},
Term::Src { src, val } => {
let val = val.to_hs_checker(env, met);
format!("(Src {} {})", src.to_u64(), val)
},
Term::Nat { nat } => {
format!("(Nat {})", nat)
},
Term::Txt { txt } => {
format!("(Txt \"{}\")", txt.replace("\n", "\\n"))
},
Term::Mch { .. } => {
unreachable!()
},
}
}
pub fn to_hvm2(&self) -> String {
match self {
Term::All { era: _, nam: _, inp: _, bod: _ } => {
@ -341,6 +136,82 @@ impl Term {
pub fn to_hvm2_name(name: &str) -> String {
format!("_{}", name.replace("/","."))
}
}
impl Term {
pub fn to_kindc(&self, met: &mut usize) -> String {
match self {
Term::All { era: _, nam, inp, bod } => {
format!("∀({}: {}) {}", nam, inp.to_kindc(met), bod.to_kindc(met))
},
Term::Lam { era: _, nam, bod } => {
format!("λ{} {}", nam, bod.to_kindc(met))
},
Term::App { era: _, fun, arg } => {
format!("({} {})", fun.to_kindc(met), arg.to_kindc(met))
},
Term::Ann { chk, val, typ } => {
format!("{{{}:{} {}}}", val.to_kindc(met), if *chk { ":" } else { "" }, typ.to_kindc(met))
},
Term::Slf { nam, typ, bod } => {
format!("$({}: {}) {}", nam, typ.to_kindc(met), bod.to_kindc(met))
},
Term::Ins { val } => {
format!("~{}", val.to_kindc(met))
},
Term::Set => "*".to_string(),
Term::U60 => "U60".to_string(),
Term::Num { val } => val.to_string(),
Term::Op2 { opr, fst, snd } => {
format!("({} {} {})", opr.to_kindc(), fst.to_kindc(met), snd.to_kindc(met))
},
Term::Swi { nam, x, z, s, p } => {
format!("switch {} = {} {{ 0: {} _: {} }}: {}", nam, x.to_kindc(met), z.to_kindc(met), s.to_kindc(met), p.to_kindc(met))
},
Term::Let { nam, val, bod } => {
format!("let {} = {}; {}", nam, val.to_kindc(met), bod.to_kindc(met))
},
Term::Use { nam, val, bod } => {
format!("use {} = {}; {}", nam, val.to_kindc(met), bod.to_kindc(met))
},
Term::Hol { nam } => format!("?{}", nam),
Term::Met { .. } => {
let uid = *met;
*met += 1;
format!("_{}", uid)
},
Term::Var { nam } => nam.clone(),
Term::Src { src, val } => format!("!{} {}", src.to_u64(), val.to_kindc(met)),
Term::Nat { nat } => format!("#{}", nat),
Term::Txt { txt } => format!("\"{}\"", txt.replace("\n", "\\n")),
Term::Mch { .. } => unreachable!(),
}
}
pub fn to_kindc_name(name: &str) -> String {
name.to_string()
}
}
impl Oper {
pub fn to_kindc(&self) -> &'static str {
match self {
Oper::Add => "+",
Oper::Sub => "-",
Oper::Mul => "*",
Oper::Div => "/",
Oper::Mod => "%",
Oper::Eq => "==",
Oper::Ne => "!=",
Oper::Lt => "<",
Oper::Gt => ">",
Oper::Lte => "<=",
Oper::Gte => ">=",
Oper::And => "&",
Oper::Or => "|",
Oper::Xor => "^",
Oper::Lsh => "<<",
Oper::Rsh => ">>",
}
}
}