mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-09-11 17:56:48 +03:00
848 lines
44 KiB
Plaintext
848 lines
44 KiB
Plaintext
// 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))
|
|
|
|
(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
|
|
|
|
// 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 (Met nam val)) = (Reduce.met lv nam val)
|
|
(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 nam val) dep) = (Met nam (Maybe.match val λx(Some (Normal lv x dep)) None))
|
|
(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 Logs A) | (Fail Logs String)
|
|
// type Checker A = Logs -> (Result A)
|
|
|
|
(Result.match (Done logs value) done fail) = (done logs value)
|
|
(Result.match (Fail logs error) done fail) = (fail logs error)
|
|
|
|
//(State.get fill got) = (got fill logs)
|
|
//(State.new) = []
|
|
|
|
(Checker.bind a b) = λlogs (Result.match (a logs) λlogsλvalue((b value) logs) λlogsλerror(Fail logs error))
|
|
(Checker.pure a) = λlogs (Done logs a)
|
|
(Checker.fail e) = λlogs (Fail logs e)
|
|
(Checker.run chk) = (chk [])
|
|
(Checker.log msg) = λlogs (Done (List.cons msg logs) 1)
|
|
(Checker.save) = λlogs (Done logs logs)
|
|
(Checker.load logs) = λeras (Done 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) λlogs
|
|
(Checker.bind (Identical a b dep) λequal
|
|
(If equal
|
|
(Checker.pure equal)
|
|
(Checker.bind (Checker.load logs) λ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.nam a.val) (Met b.nam b.val) dep) =
|
|
(Checker.pure (Same a.nam b.nam))
|
|
(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 (Same 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
|
|
(& 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.nam (Some a.val)) b dep) =
|
|
(Identical a.val b dep)
|
|
(Identical.go a (Met b.nam (Some b.val)) dep) =
|
|
(Identical a b.val dep)
|
|
(Identical.go (Met a.nam None) (Met b.nam None) dep) =
|
|
(Checker.pure (Same a.nam b.nam))
|
|
(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
|
|
(& 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 (Fill 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 nam None) b dep ctx) =
|
|
(Maybe.bind (Unify.solution b dep nam ctx) λneo
|
|
(Maybe.pure (Pair nam 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 _ (Some val))) 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 nam (Some val)) 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 nam None)) = 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 -> String -> (Map U60 Term) -> (Maybe Term)
|
|
(Unify.solution (All nam inp bod) dep hol ctx) =
|
|
(Maybe.bind (Unify.solution inp dep hol ctx) λinp
|
|
(Maybe.bind (Unify.solution (bod (Var nam dep)) (+ dep 1) hol ctx) λbod
|
|
(Maybe.pure (All nam inp λ_(bod)))))
|
|
(Unify.solution (Lam nam bod) dep hol ctx) =
|
|
(Maybe.bind (Unify.solution (bod (Var nam dep)) (+ 1 dep) hol ctx) λbod
|
|
(Maybe.pure (Lam nam λ_(bod))))
|
|
(Unify.solution (App fun arg) dep hol ctx) =
|
|
(Maybe.bind (Unify.solution fun dep hol ctx) λfun
|
|
(Maybe.bind (Unify.solution arg dep hol ctx) λarg
|
|
(Maybe.pure (App fun arg))))
|
|
(Unify.solution (Ann val typ) dep hol ctx) =
|
|
(Maybe.bind (Unify.solution val dep hol ctx) λval
|
|
(Maybe.bind (Unify.solution typ dep hol ctx) λtyp
|
|
(Maybe.pure (Ann val typ))))
|
|
(Unify.solution (Slf nam typ bod) dep hol ctx) =
|
|
(Unify.solution typ dep hol ctx)
|
|
(Unify.solution (Ins val) dep hol ctx) =
|
|
(Maybe.bind (Unify.solution val dep hol ctx) λval
|
|
(Maybe.pure (Ins val)))
|
|
(Unify.solution (Ref nam sub val) dep hol ctx) =
|
|
(Maybe.pure (Ref nam sub val))
|
|
(Unify.solution (Let nam val bod) dep hol ctx) =
|
|
(Maybe.bind (Unify.solution val dep hol ctx) λval
|
|
(Maybe.bind (Unify.solution (bod (Var nam dep)) (+ 1 dep) hol ctx) λbod
|
|
(Maybe.pure (Let nam val λ_(bod)))))
|
|
(Unify.solution (Met nam None) dep hol ctx) =
|
|
None // holes can't appear in the solution
|
|
//(If (Same nam hol) None (Maybe.pure (Met nam None)))
|
|
(Unify.solution (Met nam (Some val)) dep hol ctx) =
|
|
(Maybe.bind (Unify.solution val dep hol ctx) λval
|
|
(Maybe.pure (Met nam (Some val))))
|
|
(Unify.solution (Hol nam _) dep hol ctx) =
|
|
(Maybe.pure (Hol nam [])) // FIXME?
|
|
(Unify.solution Set dep hol ctx) =
|
|
(Maybe.pure Set)
|
|
(Unify.solution U60 dep hol ctx) =
|
|
(Maybe.pure U60)
|
|
(Unify.solution (Num val) dep hol ctx) =
|
|
(Maybe.pure (Num val))
|
|
(Unify.solution (Op2 opr fst snd) dep hol ctx) =
|
|
(Maybe.bind (Unify.solution fst dep hol ctx) λfst
|
|
(Maybe.bind (Unify.solution snd dep hol ctx) λsnd
|
|
(Maybe.pure (Op2 opr fst snd))))
|
|
(Unify.solution (Mat nam x z s p) dep hol ctx) =
|
|
(Maybe.bind (Unify.solution x dep hol ctx) λx
|
|
(Maybe.bind (Unify.solution z dep hol ctx) λz
|
|
(Maybe.bind (Unify.solution (s (Var (String.concat nam "-1") dep)) dep hol ctx) λs
|
|
(Maybe.bind (Unify.solution (p (Var nam dep)) dep hol ctx) λp
|
|
(Maybe.pure (Mat nam x z λ_(s) λ_(p)))))))
|
|
(Unify.solution (Txt val) dep hol ctx) =
|
|
(Maybe.pure (Txt val))
|
|
(Unify.solution (Var nam idx) dep hol ctx) =
|
|
(Maybe.bind (Map.get λaλb(== a b) idx ctx) λval
|
|
(Maybe.pure val))
|
|
(Unify.solution (Src src val) dep hol ctx) =
|
|
(Maybe.bind (Unify.solution val dep hol ctx) λval
|
|
(Maybe.pure (Src src val)))
|
|
(Unify.solution term dep hol 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.fail (NonFunApp (App fun arg) dep)))
|
|
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 (NonSlfIns (Ins val))))
|
|
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 (CantInfer (Lam nam bod) dep))
|
|
(Infer.match (Let nam val bod) dep) =
|
|
(Checker.fail (CantInfer (Let nam val bod) dep))
|
|
(Infer.match (Hol nam ctx) dep) =
|
|
(Checker.fail (CantInfer (Hol nam ctx) dep))
|
|
(Infer.match (Met nam (Some val)) dep) =
|
|
(Infer.match val dep)
|
|
(Infer.match (Met nam None) dep) =
|
|
(Checker.fail (CantInfer (Met nam None) dep))
|
|
(Infer.match (Var nam idx) dep) =
|
|
(Checker.fail (CantInfer (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 (FoundHole 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 term.nam None) 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 (TypeMismatch src detected expected value dep))
|
|
(Check.report src n detected expected value dep) =
|
|
(Checker.pure 0)
|
|
|
|
// Syntax
|
|
// ------
|
|
|
|
(Show (All nam inp bod) dep) = (String.join ["∀(" nam ": " (Show inp dep) ") " (Show (bod (Var nam dep)) (+ dep 1))])
|
|
(Show (Lam nam bod) dep) = (String.join ["λ" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
|
|
(Show (App fun arg) dep) = (String.join ["(" (Show.unwrap (Show fun dep)) " " (Show arg dep) ")"])
|
|
(Show (Ann val typ) dep) = (String.join ["{" (Show val dep) ": " (Show typ dep) "}"])
|
|
(Show (Slf nam typ bod) dep) = (String.join ["$(" nam ": " (Show typ dep) ") " (Show (bod (Var nam dep)) (+ dep 1))])
|
|
(Show (Ins val) dep) = (String.join ["~" (Show val dep)])
|
|
(Show (Ref nam sub val) dep) = nam
|
|
(Show (Let nam val bod) dep) = (String.join ["let " nam " = " (Show val dep) "; " (Show (bod (Var nam dep)) (+ dep 1))])
|
|
(Show Set dep) = (String.join ["*"])
|
|
(Show U60 dep) = "#U60"
|
|
(Show (Num val) dep) = (String.join ["#" (U60.show val)])
|
|
(Show (Op2 opr fst snd) dep) = (String.join ["#(" (Op2.show opr) " " (Show fst dep) " " (Show snd dep) ")"])
|
|
(Show (Mat nam x z s p) dep) = (String.join ["#match " nam " = " (Show x dep) " { #0: " (Show z dep) " #+: " (Show (s (Var (String.concat nam "-1") dep)) (+ dep 1)) " }: " (Show (p (Var nam dep)) dep)])
|
|
(Show (Txt txt) dep) = (String.join [Quote txt Quote])
|
|
(Show (Hol nam ctx) dep) = (String.join ["?" nam])
|
|
(Show (Met nam val) dep) = (String.join ["_" nam "[" (Maybe.match val λx(Show x 0) "") "]"])
|
|
(Show (Var nam idx) dep) = (String.join [nam])
|
|
(Show (Src src val) dep) = (Show val dep)
|
|
//(Show (Src src val) dep) = (String.join ["!" (Show val dep)])
|
|
//(Show (Var nam idx) dep) = (String.join [nam "'" (U60.show idx)])
|
|
|
|
(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 [NewLine "- " (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)
|
|
|
|
(Message.show (FoundHole name type ctx dep)) =
|
|
let bold = (String.color BRIGHT)
|
|
let reset = (String.color RESET)
|
|
let type = (Show (Normal 1 type dep) dep)
|
|
let ctx = (Context.show ctx dep)
|
|
(String.join [bold "HOLE:" reset " ?" name " :: " type ctx])
|
|
(Message.show (NonFunApp term dep)) =
|
|
let term = (Show term dep)
|
|
(String.join ["NON_FUNCTION: " term])
|
|
(Message.show (CantInfer term dep)) =
|
|
let term = (Show term dep)
|
|
(String.join ["CANT_INFER: " term])
|
|
(Message.show (TypeMismatch src detected expected value dep)) =
|
|
let det = (Show (Normal 1 detected dep) dep)
|
|
let exp = (Show (Normal 1 expected dep) dep)
|
|
let val = (Show (Normal 1 value dep) dep)
|
|
(String.join [(String.color BRIGHT) "TYPE_MISMATCH" NewLine
|
|
"- expected: " (String.color RESET) (String.color GREEN) exp NewLine (String.color RESET) (String.color BRIGHT)
|
|
"- detected: " (String.color RESET) (String.color RED) det NewLine (String.color RESET) (String.color BRIGHT)
|
|
"- bad_term: " (String.color RESET) (String.color DIM) val NewLine (String.color RESET)
|
|
"##LOC{" (U60.show src) "}LOC##" NewLine
|
|
])
|
|
(Message.show (Fill hole value dep)) =
|
|
let val = (Show (Normal 1 value dep) dep)
|
|
(String.join ["FILL: _" hole " = " val])
|
|
|
|
// 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:
|
|
λ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.solved sub))))
|
|
// case fail:
|
|
λ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 (Fill 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 message 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 (Message.show msg) (API.check.log msgs then))
|
|
(API.check.log List.nil then) = then
|
|
|
|
// Reports solved holdes
|
|
(API.check.solved (List.cons (Pair name None) xs)) = (HVM.print (String.join ["UNSOLVED: _" name]) (& 0 (API.check.solved xs)))
|
|
(API.check.solved (List.cons (Pair nam (Some x)) xs)) = (API.check.solved xs)
|
|
(API.check.solved List.nil) = 1
|
|
|
|
Book.Char = (Ref "Char" [] (Ann (Src 6597081301007 (U60)) (Src 6597077106696 (Set))))
|
|
Book.IO = (Ref "IO" [] (Ann (Src 2199043178912 (Lam "A" λxA (Src 2199049470368 (Slf "self" (Src 2199057858599 (App (Src 2199058907172 (Book.IO)) (Src 2199062052902 xA))) λxself (Src 2199068344736 (All "P" (Src 2199075684418 (All "x" (Src 2199083024447 (App (Src 2199084073020 (Book.IO)) (Src 2199087218750 xA))) λxx (Src 2199091413058 (Set)))) λxP (Src 2199096656288 (All "print" (Src 2199108190364 (All "text" (Src 2199118676065 (Book.String)) λxtext (Src 2199127064732 (All "then" (Src 2199137550464 (All "x" (Src 2199144890488 (Book.Unit)) λxx (Src 2199151181952 (App (Src 2199152230525 (Book.IO)) (Src 2199155376255 xA))))) λxthen (Src 2199159570588 (App (Src 2199160619140 xP) (Src 2199162716315 (App (App (App (Src 2199163764878 (Book.IO.print)) (Src 2199173202064 xA)) (Src 2199175299221 xtext)) (Src 2199180542106 xthen))))))))) λxprint (Src 2199191028128 (All "load" (Src 2199201513718 (All "file" (Src 2199211999418 (Book.String)) λxfile (Src 2199220388086 (All "then" (Src 2199230873819 (All "x" (Src 2199238213843 (Book.String)) λxx (Src 2199246602459 (App (Src 2199247651032 (Book.IO)) (Src 2199250796762 xA))))) λxthen (Src 2199254991094 (App (Src 2199256039647 xP) (Src 2199258136821 (App (App (App (Src 2199259185384 (Book.IO.load)) (Src 2199267573994 xA)) (Src 2199269671151 xfile)) (Src 2199274914036 xthen))))))))) λxload (Src 2199285399968 (All "save" (Src 2199295885669 (All "file" (Src 2199306371348 (Book.String)) λxfile (Src 2199314760037 (All "data" (Src 2199325245734 (Book.String)) λxdata (Src 2199333634405 (All "then" (Src 2199344120133 (All "x" (Src 2199351460157 (Book.Unit)) λxx (Src 2199357751621 (App (Src 2199358800194 (Book.IO)) (Src 2199361945924 xA))))) λxthen (Src 2199366140261 (App (Src 2199367188809 xP) (Src 2199369285988 (App (App (App (App (Src 2199370334546 (Book.IO.save)) (Src 2199378723156 xA)) (Src 2199380820313 xfile)) (Src 2199386063198 xdata)) (Src 2199391306083 xthen))))))))))) λxsave (Src 2199401791904 (All "done" (Src 2199412277652 (All "term" (Src 2199422763390 xA) λxterm (Src 2199425909140 (App (Src 2199426957698 xP) (Src 2199429054867 (App (App (Src 2199430103435 (Book.IO.done)) (Src 2199438492045 xA)) (Src 2199440589202 xterm))))))) λxdone (Src 2199451074976 (App (Src 2199452123546 xP) (Src 2199454220703 xself))))))))))))))))) (Src 2199028498448 (All "A" (Src 2199035838477 (Set)) λxA (Src 2199038984208 (Set))))))
|
|
Book.IO.done = (Ref "IO.done" [] (Ann (Src 3298583117930 (Lam "A" λxA (Src 3298587312234 (Lam "term" λxterm (Src 3298596749418 (Ins (Src 3298597797994 (Lam "P" λxP (Src 3298601992298 (Lam "print" λxprint (Src 3298610380906 (Lam "load" λxload (Src 3298617720938 (Lam "save" λxsave (Src 3298625060970 (Lam "done" λxdone (Src 3298634498154 (App (Src 3298635546724 xdone) (Src 3298640789609 xterm))))))))))))))))))) (Src 3298545369131 (All "A" (Src 3298552709138 (Set)) λxA (Src 3298557952043 (All "term" (Src 3298568437793 xA) λxterm (Src 3298573680683 (App (Src 3298574729256 (Book.IO)) (Src 3298577874986 xA)))))))))
|
|
Book.IO.load = (Ref "IO.load" [] (Ann (Src 1099601805470 (Lam "A" λxA (Src 1099605999774 (Lam "file" λxfile (Src 1099613339806 (Lam "then" λxthen (Src 1099622776990 (Ins (Src 1099623825566 (Lam "P" λxP (Src 1099628019870 (Lam "print" λxprint (Src 1099636408478 (Lam "load" λxload (Src 1099643748510 (Lam "save" λxsave (Src 1099651088542 (Lam "done" λxdone (Src 1099660525726 (App (App (Src 1099661574291 xload) (Src 1099666817176 xfile)) (Src 1099672060061 xthen))))))))))))))))))))) (Src 1099522113619 (All "A" (Src 1099529453586 (Set)) λxA (Src 1099534696531 (All "file" (Src 1099545182246 (Book.String)) λxfile (Src 1099555668051 (All "then" (Src 1099566153801 (All "x" (Src 1099573493825 (Book.String)) λxx (Src 1099581882441 (App (Src 1099582931014 (Book.IO)) (Src 1099586076744 xA))))) λxthen (Src 1099592368211 (App (Src 1099593416784 (Book.IO)) (Src 1099596562514 xA)))))))))))
|
|
Book.IO.print = (Ref "IO.print" [] (Ann (Src 4398135640222 (Lam "A" λxA (Src 4398139834526 (Lam "text" λxtext (Src 4398147174558 (Lam "then" λxthen (Src 4398156611742 (Ins (Src 4398157660318 (Lam "P" λxP (Src 4398161854622 (Lam "print" λxprint (Src 4398170243230 (Lam "load" λxload (Src 4398177583262 (Lam "save" λxsave (Src 4398184923294 (Lam "done" λxdone (Src 4398194360478 (App (App (Src 4398195409043 xprint) (Src 4398201700504 xtext)) (Src 4398206943389 xthen))))))))))))))))))))) (Src 4398058045522 (All "A" (Src 4398065385491 (Set)) λxA (Src 4398070628434 (All "text" (Src 4398081114151 (Book.String)) λxtext (Src 4398091599954 (All "then" (Src 4398102085704 (All "x" (Src 4398109425728 (Book.Unit)) λxx (Src 4398115717192 (App (Src 4398116765765 (Book.IO)) (Src 4398119911495 xA))))) λxthen (Src 4398126202962 (App (Src 4398127251535 (Book.IO)) (Src 4398130397265 xA)))))))))))
|
|
Book.IO.save = (Ref "IO.save" [] (Ann (Src 13194248585404 (Lam "A" λxA (Src 13194252779708 (Lam "file" λxfile (Src 13194260119740 (Lam "data" λxdata (Src 13194267459772 (Lam "then" λxthen (Src 13194276896956 (Ins (Src 13194277945532 (Lam "P" λxP (Src 13194282139836 (Lam "print" λxprint (Src 13194290528444 (Lam "load" λxload (Src 13194297868476 (Lam "save" λxsave (Src 13194305208508 (Lam "done" λxdone (Src 13194314645692 (App (App (App (Src 13194315694252 xsave) (Src 13194320937137 xfile)) (Src 13194326180022 xdata)) (Src 13194331422907 xthen))))))))))))))))))))))) (Src 13194150019173 (All "A" (Src 13194157359122 (Set)) λxA (Src 13194162602085 (All "file" (Src 13194173087782 (Book.String)) λxfile (Src 13194183573605 (All "data" (Src 13194194059322 (Book.String)) λxdata (Src 13194204545125 (All "then" (Src 13194215030875 (All "x" (Src 13194222370899 (Book.Unit)) λxx (Src 13194228662363 (App (Src 13194229710936 (Book.IO)) (Src 13194232856666 xA))))) λxthen (Src 13194239148133 (App (Src 13194240196706 (Book.IO)) (Src 13194243342436 xA)))))))))))))
|
|
Book.List = (Ref "List" [] (Ann (Src 7696605511870 (Lam "T" λxT (Src 7696611803326 (Slf "self" (Src 7696620191789 (App (Src 7696621240362 (Book.List)) (Src 7696626483244 xT))) λxself (Src 7696632774846 (All "P" (Src 7696640114763 (All "xs" (Src 7696648503368 (App (Src 7696649551941 (Book.List)) (Src 7696654794823 xT))) λxxs (Src 7696658989131 (Set)))) λxP (Src 7696664232126 (All "cons" (Src 7696674717845 (All "head" (Src 7696685203556 xT) λxhead (Src 7696688349333 (All "tail" (Src 7696698835064 (App (Src 7696699883637 (Book.List)) (Src 7696705126519 xT))) λxtail (Src 7696709320853 (App (Src 7696710369404 xP) (Src 7696712466580 (App (App (App (Src 7696713515143 (Book.List.cons)) (Src 7696724000905 xT)) (Src 7696726098062 xhead)) (Src 7696731340947 xtail))))))))) λxcons (Src 7696741826750 (All "nil" (Src 7696751263922 (App (Src 7696752312484 xP) (Src 7696754409649 (App (Src 7696755458222 (Book.List.nil)) (Src 7696764895408 xT))))) λxnil (Src 7696772235454 (App (Src 7696773284024 xP) (Src 7696775381181 xself))))))))))))) (Src 7696588734484 (All "T" (Src 7696596074511 (Set)) λxT (Src 7696601317396 (Set))))))
|
|
Book.List.cons = (Ref "List.cons" [] (Ann (Src 8796168519808 (Lam "T" λxT (Src 8796172714112 (Lam "head" λxhead (Src 8796180054144 (Lam "tail" λxtail (Src 8796189491328 (Ins (Src 8796190539904 (Lam "P" λxP (Src 8796194734208 (Lam "cons" λxcons (Src 8796202074240 (Lam "nil" λxnil (Src 8796210462848 (App (App (Src 8796211511413 xcons) (Src 8796216754298 xhead)) (Src 8796221997183 xtail))))))))))))))))) (Src 8796105605189 (All "T" (Src 8796112945172 (Set)) λxT (Src 8796118188101 (All "head" (Src 8796128673827 xT) λxhead (Src 8796133916741 (All "tail" (Src 8796144402489 (App (Src 8796145451062 (Book.List)) (Src 8796150693944 xT))) λxtail (Src 8796156985413 (App (Src 8796158033986 (Book.List)) (Src 8796163276868 xT)))))))))))
|
|
Book.List.nil = (Ref "List.nil" [] (Ann (Src 9895640301631 (Lam "T" λxT (Src 9895646593087 (Ins (Src 9895647641663 (Lam "P" λxP (Src 9895651835967 (Lam "cons" λxcons (Src 9895659175999 (Lam "nil" λxnil (Src 9895667564607 xnil))))))))))) (Src 9895616184351 (All "T" (Src 9895623524371 (Set)) λxT (Src 9895628767263 (App (Src 9895629815836 (Book.List)) (Src 9895635058718 xT)))))))
|
|
Book.String = (Ref "String" [] (Ann (Src 5497571770392 (App (Src 5497572818962 (Book.List)) (Src 5497578061847 (Book.Char)))) (Src 5497567576074 (Set))))
|
|
Book.String.cons = (Ref "String.cons" [] (Ann (Src 14293715124337 (Lam "head" λxhead (Src 14293722464369 (Lam "tail" λxtail (Src 14293731901553 (Ins (Src 14293732950129 (Lam "P" λxP (Src 14293737144433 (Lam "cons" λxcons (Src 14293744484465 (Lam "nil" λxnil (Src 14293752873073 (App (App (Src 14293753921638 xcons) (Src 14293759164523 xhead)) (Src 14293764407408 xtail))))))))))))))) (Src 14293665841210 (All "head" (Src 14293676326940 (Book.Char)) λxhead (Src 14293684715578 (All "tail" (Src 14293695201328 (Book.String)) λxtail (Src 14293705687098 (Book.String))))))))
|
|
Book.String.nil = (Ref "String.nil" [] (Ann (Src 15393185857581 (Ins (Src 15393186906157 (Lam "P" λxP (Src 15393191100461 (Lam "cons" λxcons (Src 15393198440493 (Lam "nil" λxnil (Src 15393206829101 xnil))))))))) (Src 15393176420371 (Book.String))))
|
|
Book.Unit = (Ref "Unit" [] (Ann (Src 10995127812181 (Slf "self" (Src 10995136200727 (Book.Unit)) λxself (Src 10995144589397 (All "P" (Src 10995151929392 (All "x" (Src 10995159269421 (Book.Unit)) λxx (Src 10995165560880 (Set)))) λxP (Src 10995170803797 (All "one" (Src 10995180240969 (App (Src 10995181289535 xP) (Src 10995183386696 (Book.Unit.one)))) λxone (Src 10995197018197 (App (Src 10995198066767 xP) (Src 10995200163924 xself))))))))) (Src 10995123617800 (Set))))
|
|
Book.Unit.one = (Ref "Unit.one" [] (Ann (Src 12094646779936 (Ins (Src 12094647828512 (Lam "P" λxP (Src 12094652022816 (Lam "one" λxone (Src 12094658314272 xone))))))) (Src 12094639439887 (Book.Unit))))
|
|
|
|
Main = (API.check Book.IO.load)
|