From 77af124c20be698edc2c91bbc4fc488d2fea6ba1 Mon Sep 17 00:00:00 2001 From: felipegchi Date: Mon, 16 Jan 2023 09:20:12 -0300 Subject: [PATCH 1/2] fix: inlining, tests for eval and tests --- .github/workflows/cargo.yml | 27 - crates/kind-checker/src/checker.hvm | 1084 +++++++++-------- crates/kind-pass/src/inline/mod.rs | 1 + .../suite/eval/AllFieldsDestruct.golden | 3 +- .../kind-tests/suite/eval/DoNotation.golden | 3 +- crates/kind-tests/suite/eval/Getters.golden | 3 +- .../kind-tests/suite/eval/MatchMotive.golden | 3 +- crates/kind-tests/suite/eval/PatChar.golden | 3 +- crates/kind-tests/suite/eval/Setters.golden | 3 +- .../kind-tests/suite/eval/SimpleOpen.golden | 3 +- crates/kind-tests/suite/eval/TestWith.golden | 3 +- crates/kind-tests/suite/eval/User.golden | 3 +- crates/kind-tests/suite/eval/VecMatch.golden | 3 +- crates/kind-tests/suite/eval/With.golden | 3 +- .../suite/run/AllFieldsDestruct.golden | 1 + .../suite/run/AllFieldsDestruct.kind2 | 10 + crates/kind-tests/suite/run/DoNotation.golden | 1 + crates/kind-tests/suite/run/DoNotation.kind2 | 12 + crates/kind-tests/suite/run/Getters.golden | 1 + crates/kind-tests/suite/run/Getters.kind2 | 10 + .../kind-tests/suite/run/MatchMotive.golden | 1 + crates/kind-tests/suite/run/MatchMotive.kind2 | 19 + .../suite/{eval => run}/NoMatch.golden | 2 +- .../suite/{eval => run}/NoMatch.kind2 | 0 crates/kind-tests/suite/run/PatChar.golden | 1 + crates/kind-tests/suite/run/PatChar.kind2 | 6 + crates/kind-tests/suite/run/Setters.golden | 1 + crates/kind-tests/suite/run/Setters.kind2 | 12 + crates/kind-tests/suite/run/SimpleOpen.golden | 1 + crates/kind-tests/suite/run/SimpleOpen.kind2 | 16 + crates/kind-tests/suite/run/TestWith.golden | 1 + crates/kind-tests/suite/run/TestWith.kind2 | 19 + crates/kind-tests/suite/run/User.golden | 1 + crates/kind-tests/suite/run/User.kind2 | 12 + crates/kind-tests/suite/run/VecMatch.golden | 1 + crates/kind-tests/suite/run/VecMatch.kind2 | 20 + crates/kind-tests/suite/run/With.golden | 1 + crates/kind-tests/suite/run/With.kind2 | 16 + crates/kind-tests/tests/mod.rs | 16 +- tests/test_wikind.sh | 9 - 40 files changed, 764 insertions(+), 571 deletions(-) create mode 100644 crates/kind-tests/suite/run/AllFieldsDestruct.golden create mode 100644 crates/kind-tests/suite/run/AllFieldsDestruct.kind2 create mode 100644 crates/kind-tests/suite/run/DoNotation.golden create mode 100644 crates/kind-tests/suite/run/DoNotation.kind2 create mode 100644 crates/kind-tests/suite/run/Getters.golden create mode 100644 crates/kind-tests/suite/run/Getters.kind2 create mode 100644 crates/kind-tests/suite/run/MatchMotive.golden create mode 100644 crates/kind-tests/suite/run/MatchMotive.kind2 rename crates/kind-tests/suite/{eval => run}/NoMatch.golden (89%) rename crates/kind-tests/suite/{eval => run}/NoMatch.kind2 (100%) create mode 100644 crates/kind-tests/suite/run/PatChar.golden create mode 100644 crates/kind-tests/suite/run/PatChar.kind2 create mode 100644 crates/kind-tests/suite/run/Setters.golden create mode 100644 crates/kind-tests/suite/run/Setters.kind2 create mode 100644 crates/kind-tests/suite/run/SimpleOpen.golden create mode 100644 crates/kind-tests/suite/run/SimpleOpen.kind2 create mode 100644 crates/kind-tests/suite/run/TestWith.golden create mode 100644 crates/kind-tests/suite/run/TestWith.kind2 create mode 100644 crates/kind-tests/suite/run/User.golden create mode 100644 crates/kind-tests/suite/run/User.kind2 create mode 100644 crates/kind-tests/suite/run/VecMatch.golden create mode 100644 crates/kind-tests/suite/run/VecMatch.kind2 create mode 100644 crates/kind-tests/suite/run/With.golden create mode 100644 crates/kind-tests/suite/run/With.kind2 delete mode 100755 tests/test_wikind.sh diff --git a/.github/workflows/cargo.yml b/.github/workflows/cargo.yml index d29897b8..f5721c39 100644 --- a/.github/workflows/cargo.yml +++ b/.github/workflows/cargo.yml @@ -41,33 +41,6 @@ jobs: - uses: actions-rs/cargo@v1 with: command: test - - wikind_test: - name: 鈿楋笍 Wikind Test - runs-on: ${{ matrix.os }} - timeout-minutes: 20 - strategy: - matrix: - os: [ubuntu-latest] - steps: - - uses: actions/checkout@v2 - - uses: actions-rs/toolchain@v1 - with: - profile: minimal - toolchain: nightly - override: true - - - uses: Swatinem/rust-cache@v2 - - uses: actions-rs/cargo@v1 - with: - command: build - - - name: Run wikind - run: | - chmod +x ./tests/test_wikind.sh - ./tests/test_wikind.sh - shell: bash - # cargo_fmt: # name: 馃拝 Cargo Fmt # continue-on-error: true diff --git a/crates/kind-checker/src/checker.hvm b/crates/kind-checker/src/checker.hvm index 54ed649d..c0c1599e 100644 --- a/crates/kind-checker/src/checker.hvm +++ b/crates/kind-checker/src/checker.hvm @@ -1,175 +1,288 @@ -(Main) = let imports = [(Dynamic.new 位a 位b (Kind.Term.set_origin a b)), (Dynamic.new (Kind.API.check_all)), (Dynamic.new (Kind.API.eval_main)), (Dynamic.new 位a (Kind.Coverage.check a))]; (Kind.API.check_all) -(Kind.API.eval_main) = (Kind.Printer.text [(Kind.Term.show (Kind.Term.FN0 (Main.) 0)), (String.pure (Char.newline)), (String.pure (Char.newline))]) -(Kind.Term.show term) = let sugars = [(Kind.Term.show.sugar.string term), (Kind.Term.show.sugar.list term), (Kind.Term.show.sugar.sigma term)]; (Maybe.try sugars (Kind.Term.show.go term)) -(Kind.Term.show.sugar.sigma (Kind.Term.ct2 (Sigma.) orig typ (Kind.Term.lam orig_ name body))) = (Maybe.some (Kind.Printer.text ["([", (Kind.Name.show name), ": ", (Kind.Term.show typ), "] -> ", (Kind.Term.show (body (Kind.Term.var orig_ name 0))), ")"])) -(Kind.Term.show.sugar.sigma term) = (Maybe.none) -(Kind.Printer.text []) = "" -(Kind.Printer.text (List.cons x xs)) = (String.concat x (Kind.Printer.text xs)) -(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys)) -(String.concat "" ys) = ys -(Kind.Name.show name) = (Kind.Name.show.go name "") -(Kind.Name.show.go name chrs) = (U60.if (== name 0) chrs let val = (% name 64); let chr = (U60.if (== val 0) 46 (U60.if (& (<= 1 val) (<= val 10)) (+ (- val 1) 48) (U60.if (& (<= 11 val) (<= val 36)) (+ (- val 11) 65) (U60.if (& (<= 37 val) (<= val 62)) (+ (- val 37) 97) (U60.if (== val 63) 95 63))))); (Kind.Name.show.go (/ name 64) (String.cons chr chrs))) -(U60.if 0 t f) = f -(U60.if n t f) = t -(Kind.Term.show.sugar.string term) = (Maybe.bind (Kind.Term.show.sugar.string.go term) 位res let quot = "'"; (Maybe.some (Kind.Printer.text [quot, res, quot]))) -(Kind.Term.show.sugar.string.go (Kind.Term.ct0 (String.nil.) orig)) = (Maybe.some "") -(Kind.Term.show.sugar.string.go (Kind.Term.ct2 (String.cons.) orig (Kind.Term.u60 orig1 x0) x1)) = (Maybe.bind (Kind.Term.show.sugar.string.go x1) 位tail (Maybe.some (String.cons x0 tail))) -(Kind.Term.show.sugar.string.go other) = (Maybe.none) -(Maybe.bind (Maybe.none) mb) = (Maybe.none) -(Maybe.bind (Maybe.some val) mb) = (mb val) -(Kind.Term.show.go (Kind.Term.typ orig)) = "Type" -(Kind.Term.show.go (Kind.Term.var orig name index)) = (Kind.Printer.text [(Kind.Name.show name)]) -(Kind.Term.show.go (Kind.Term.hol orig numb)) = (Kind.Printer.text ["_"]) -(Kind.Term.show.go (Kind.Term.all orig name type body)) = (Kind.Term.show.forall orig name type body) -(Kind.Term.show.go (Kind.Term.lam orig name body)) = (Kind.Printer.text ["(", (Kind.Name.show name), " => ", (Kind.Term.show (body (Kind.Term.var orig name 0))), ")"]) -(Kind.Term.show.go (Kind.Term.let orig name exp body)) = (Kind.Printer.text ["let ", (Kind.Name.show name), " = ", (Kind.Term.show exp), "; ", (Kind.Term.show (body (Kind.Term.var orig name 0)))]) -(Kind.Term.show.go (Kind.Term.ann orig expr type)) = (Kind.Printer.text ["{", (Kind.Term.show expr), " :: ", (Kind.Term.show type), "}"]) -(Kind.Term.show.go (Kind.Term.sub orig name indx redx expr)) = (Kind.Printer.text [(Kind.Term.show expr), " ## ", (Kind.Name.show name), "/", (Show.to_string (U60.show redx))]) -(Kind.Term.show.go (Kind.Term.app orig func argm)) = (Kind.Printer.text ["(", (Kind.Term.show func), " ", (Kind.Term.show argm), ")"]) -(Kind.Term.show.go (Kind.Term.ct0 ctid orig)) = (Kind.Axiom.NameOf ctid) -(Kind.Term.show.go (Kind.Term.ct1 ctid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), ")"]) -(Kind.Term.show.go (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), ")"]) -(Kind.Term.show.go (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), ")"]) -(Kind.Term.show.go (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), ")"]) -(Kind.Term.show.go (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), ")"]) -(Kind.Term.show.go (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), ")"]) -(Kind.Term.show.go (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), ")"]) -(Kind.Term.show.go (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), ")"]) -(Kind.Term.show.go (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), ")"]) -(Kind.Term.show.go (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), ")"]) -(Kind.Term.show.go (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), ")"]) -(Kind.Term.show.go (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), ")"]) -(Kind.Term.show.go (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), ")"]) -(Kind.Term.show.go (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), ")"]) -(Kind.Term.show.go (Kind.Term.ct15 ctid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), ")"]) -(Kind.Term.show.go (Kind.Term.ct16 ctid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), ")"]) -(Kind.Term.show.go (Kind.Term.fn0 fnid orig)) = (Kind.Axiom.NameOf fnid) -(Kind.Term.show.go (Kind.Term.fn1 fnid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), ")"]) -(Kind.Term.show.go (Kind.Term.fn2 fnid orig x0 x1)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), ")"]) -(Kind.Term.show.go (Kind.Term.fn3 fnid orig x0 x1 x2)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), ")"]) -(Kind.Term.show.go (Kind.Term.fn4 fnid orig x0 x1 x2 x3)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), ")"]) -(Kind.Term.show.go (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), ")"]) -(Kind.Term.show.go (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), ")"]) -(Kind.Term.show.go (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), ")"]) -(Kind.Term.show.go (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), ")"]) -(Kind.Term.show.go (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), ")"]) -(Kind.Term.show.go (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), ")"]) -(Kind.Term.show.go (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), ")"]) -(Kind.Term.show.go (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), ")"]) -(Kind.Term.show.go (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), ")"]) -(Kind.Term.show.go (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), ")"]) -(Kind.Term.show.go (Kind.Term.fn15 fnid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), ")"]) -(Kind.Term.show.go (Kind.Term.fn16 fnid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), ")"]) -(Kind.Term.show.go (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = (Kind.Printer.text [(Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), " ", (Kind.Term.show x14)]) -(Kind.Term.show.go (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = (Kind.Printer.text [(Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), " ", (Kind.Term.show x14), " ", (Kind.Term.show x15)]) -(Kind.Term.show.go (Kind.Term.hlp orig)) = "?" -(Kind.Term.show.go (Kind.Term.U60 orig)) = "U60" -(Kind.Term.show.go (Kind.Term.u60 orig numb)) = (Show.to_string (U60.show numb)) -(Kind.Term.show.go (Kind.Term.op2 orig operator left right)) = (Kind.Printer.text ["(", (Kind.Operator.show operator), " ", (Kind.Term.show left), " ", (Kind.Term.show right), ")"]) -(Show.to_string show) = (show "") -(Kind.Operator.show (Kind.Operator.add)) = "+" -(Kind.Operator.show (Kind.Operator.sub)) = "-" -(Kind.Operator.show (Kind.Operator.mul)) = "*" -(Kind.Operator.show (Kind.Operator.div)) = "/" -(Kind.Operator.show (Kind.Operator.mod)) = "%" -(Kind.Operator.show (Kind.Operator.and)) = "&" -(Kind.Operator.show (Kind.Operator.or)) = "|" -(Kind.Operator.show (Kind.Operator.xor)) = "^" -(Kind.Operator.show (Kind.Operator.shl)) = "<<" -(Kind.Operator.show (Kind.Operator.shr)) = ">>" -(Kind.Operator.show (Kind.Operator.ltn)) = "<" -(Kind.Operator.show (Kind.Operator.lte)) = "<=" -(Kind.Operator.show (Kind.Operator.eql)) = "==" -(Kind.Operator.show (Kind.Operator.gte)) = ">=" -(Kind.Operator.show (Kind.Operator.gtn)) = ">" -(Kind.Operator.show (Kind.Operator.neq)) = "!=" -(Kind.Term.show.forall orig name type body) = (U60.if (== name 63) (Kind.Printer.text ["(", (Kind.Term.show type), " -> ", (Kind.Term.show (body (Kind.Term.var orig name 0))), ")"]) (Kind.Printer.text ["((", (Kind.Name.show name), ": ", (Kind.Term.show type), ") -> ", (Kind.Term.show (body (Kind.Term.var orig name 0))), ")"])) -(U60.show 0) = 位str (String.cons 48 str) -(U60.show n) = 位str let next = (String.cons (+ 48 (% n 10)) str); let func = (U60.if (< n 10) 位h h 位h ((U60.show (/ n 10)) h)); (func next) -(Maybe.try [] alt) = alt -(Maybe.try (List.cons maybe xs) alt) = (Maybe.match maybe (Maybe.try xs alt) 位value value) -(Maybe.match (Maybe.none) none some) = none -(Maybe.match (Maybe.some value_) none some) = (some value_) -(Kind.Term.show.sugar.list term) = (Maybe.bind (Kind.Term.show.sugar.list.go term) 位res (Maybe.some (Kind.Printer.text ["[", (String.join " " res), "]"]))) -(String.join sep list) = (String.intercalate sep list) -(String.intercalate sep xs) = (String.flatten (List.intersperse sep xs)) -(String.flatten []) = "" -(String.flatten (List.cons head tail)) = (String.concat head (String.flatten tail)) -(List.intersperse sep []) = [] -(List.intersperse sep [xh]) = [xh] -(List.intersperse sep (List.cons xh xt)) = (List.cons xh (List.cons sep (List.intersperse sep xt))) -(Kind.Term.show.sugar.list.go (Kind.Term.ct0 (List.nil.) orig)) = (Maybe.some []) -(Kind.Term.show.sugar.list.go (Kind.Term.ct2 (List.cons.) orig x0 x1)) = (Maybe.bind (Kind.Term.show.sugar.list.go x1) 位tail (Maybe.some (List.cons (Kind.Term.show x0) tail))) -(Kind.Term.show.sugar.list.go other) = (Maybe.none) -(Kind.Term.set_origin new_origin (Kind.Term.typ old_orig)) = (Kind.Term.typ new_origin) -(Kind.Term.set_origin new_origin (Kind.Term.var old_orig name idx)) = (Kind.Term.var new_origin name idx) -(Kind.Term.set_origin new_origin (Kind.Term.hol old_orig numb)) = (Kind.Term.hol new_origin numb) -(Kind.Term.set_origin new_origin (Kind.Term.all old_orig name typ body)) = (Kind.Term.all new_origin name typ body) -(Kind.Term.set_origin new_origin (Kind.Term.lam old_orig name body)) = (Kind.Term.lam new_origin name body) -(Kind.Term.set_origin new_origin (Kind.Term.let old_orig name expr body)) = (Kind.Term.let new_origin name expr body) -(Kind.Term.set_origin new_origin (Kind.Term.ann old_orig expr typ)) = (Kind.Term.ann new_origin expr typ) -(Kind.Term.set_origin new_origin (Kind.Term.sub old_orig name indx redx expr)) = (Kind.Term.sub new_origin name indx redx expr) -(Kind.Term.set_origin new_origin (Kind.Term.app old_orig func arg)) = (Kind.Term.app new_origin func arg) -(Kind.Term.set_origin new_origin (Kind.Term.hlp old_orig)) = (Kind.Term.hlp new_origin) -(Kind.Term.set_origin new_origin (Kind.Term.U60 old_orig)) = (Kind.Term.U60 new_origin) -(Kind.Term.set_origin new_origin (Kind.Term.u60 old_orig num)) = (Kind.Term.u60 new_origin num) -(Kind.Term.set_origin new_origin (Kind.Term.op2 old_orig op left right)) = (Kind.Term.op2 new_origin op left right) -(Kind.Term.set_origin new_origin (Kind.Term.ct0 ctid old_orig)) = (Kind.Term.ct0 ctid new_origin) -(Kind.Term.set_origin new_origin (Kind.Term.ct1 ctid old_orig x0)) = (Kind.Term.ct1 ctid new_origin x0) -(Kind.Term.set_origin new_origin (Kind.Term.ct2 ctid old_orig x0 x1)) = (Kind.Term.ct2 ctid new_origin x0 x1) -(Kind.Term.set_origin new_origin (Kind.Term.ct3 ctid old_orig x0 x1 x2)) = (Kind.Term.ct3 ctid new_origin x0 x1 x2) -(Kind.Term.set_origin new_origin (Kind.Term.ct4 ctid old_orig x0 x1 x2 x3)) = (Kind.Term.ct4 ctid new_origin x0 x1 x2 x3) -(Kind.Term.set_origin new_origin (Kind.Term.ct5 ctid old_orig x0 x1 x2 x3 x4)) = (Kind.Term.ct5 ctid new_origin x0 x1 x2 x3 x4) -(Kind.Term.set_origin new_origin (Kind.Term.ct6 ctid old_orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.ct6 ctid new_origin x0 x1 x2 x3 x4 x5) -(Kind.Term.set_origin new_origin (Kind.Term.ct7 ctid old_orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.ct7 ctid new_origin x0 x1 x2 x3 x4 x5 x6) -(Kind.Term.set_origin new_origin (Kind.Term.ct8 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.ct8 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7) -(Kind.Term.set_origin new_origin (Kind.Term.ct9 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.ct9 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8) -(Kind.Term.set_origin new_origin (Kind.Term.ct10 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.ct10 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) -(Kind.Term.set_origin new_origin (Kind.Term.ct11 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.ct11 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) -(Kind.Term.set_origin new_origin (Kind.Term.ct12 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.ct12 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) -(Kind.Term.set_origin new_origin (Kind.Term.ct13 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.ct13 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) -(Kind.Term.set_origin new_origin (Kind.Term.ct14 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.ct14 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) -(Kind.Term.set_origin new_origin (Kind.Term.ct15 ctid old_orig args)) = (Kind.Term.ct15 ctid new_origin args) -(Kind.Term.set_origin new_origin (Kind.Term.ct16 ctid old_orig args)) = (Kind.Term.ct16 ctid new_origin args) -(Kind.Term.set_origin new_origin (Kind.Term.fn0 fnid old_orig)) = (Kind.Term.fn0 fnid new_origin) -(Kind.Term.set_origin new_origin (Kind.Term.fn1 fnid old_orig x0)) = (Kind.Term.fn1 fnid new_origin x0) -(Kind.Term.set_origin new_origin (Kind.Term.fn2 fnid old_orig x0 x1)) = (Kind.Term.fn2 fnid new_origin x0 x1) -(Kind.Term.set_origin new_origin (Kind.Term.fn3 fnid old_orig x0 x1 x2)) = (Kind.Term.fn3 fnid new_origin x0 x1 x2) -(Kind.Term.set_origin new_origin (Kind.Term.fn4 fnid old_orig x0 x1 x2 x3)) = (Kind.Term.fn4 fnid new_origin x0 x1 x2 x3) -(Kind.Term.set_origin new_origin (Kind.Term.fn5 fnid old_orig x0 x1 x2 x3 x4)) = (Kind.Term.fn5 fnid new_origin x0 x1 x2 x3 x4) -(Kind.Term.set_origin new_origin (Kind.Term.fn6 fnid old_orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.fn6 fnid new_origin x0 x1 x2 x3 x4 x5) -(Kind.Term.set_origin new_origin (Kind.Term.fn7 fnid old_orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.fn7 fnid new_origin x0 x1 x2 x3 x4 x5 x6) -(Kind.Term.set_origin new_origin (Kind.Term.fn8 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.fn8 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7) -(Kind.Term.set_origin new_origin (Kind.Term.fn9 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.fn9 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8) -(Kind.Term.set_origin new_origin (Kind.Term.fn10 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.fn10 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) -(Kind.Term.set_origin new_origin (Kind.Term.fn11 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.fn11 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) -(Kind.Term.set_origin new_origin (Kind.Term.fn12 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.fn12 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) -(Kind.Term.set_origin new_origin (Kind.Term.fn13 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.fn13 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) -(Kind.Term.set_origin new_origin (Kind.Term.fn14 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.fn14 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) -(Kind.Term.set_origin new_origin (Kind.Term.fn15 ctid old_orig args)) = (Kind.Term.fn15 ctid new_origin args) -(Kind.Term.set_origin new_origin (Kind.Term.fn16 ctid old_orig args)) = (Kind.Term.fn16 ctid new_origin args) +(Main) = let imports = [(Dynamic.new 位a 位b (Kind.Term.set_origin a b)), (Dynamic.new (Kind.API.check_all)), (Dynamic.new (Kind.API.eval_main))]; (Kind.API.check_all) (Kind.API.check_all) = let output = (Kind.API.output (List.reverse (Kind.API.check_functions (Kind.Axiom.Functions)))); output -(List.reverse xs) = (List.reverse.go xs []) -(List.reverse.go [] ys) = ys -(List.reverse.go (List.cons x xs) ys) = (List.reverse.go xs (List.cons x ys)) (Kind.API.check_functions []) = [] (Kind.API.check_functions (List.cons f fs)) = let head = (Pair.new f (Kind.API.check_function f)); let tail = (Kind.API.check_functions fs); (List.cons head tail) (Kind.API.check_function fnid) = let rules = (Kind.Axiom.RuleOf fnid); let type = (Kind.Axiom.TypeOf fnid); let type_check = (Kind.Checker.run (Kind.Checker.unify (Kind.Checker.check type (Kind.Term.typ 0))) (Bool.true)); let rule_check = (Kind.API.check_function.rules rules (Kind.Term.eval type)); let res = (List.cons type_check rule_check); (Bool.if (Kind.Axiom.CoverCheck fnid) let cover_check = (Kind.Checker.run (Kind.Coverage.check fnid) (Bool.true)); (List.cons cover_check res) res) -(Kind.Checker.unify checker) = (Kind.Checker.bind checker 位x_1 (Kind.Checker.bind (Kind.Checker.get_equations) 位equations (Kind.Checker.unify.go equations [] (Bool.false)))) +(Kind.Checker.check (Kind.Term.lam orig name body) type) = (Kind.Checker.bind (Kind.Checker.get_subst) 位subst let fun = (Kind.Term.if_all type 位t_orig 位t_name 位t_type 位t_body 位orig 位name 位body (Kind.Checker.bind (Kind.Checker.get_depth) 位dep (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name dep)) (t_body (Kind.Term.var t_orig t_name dep))) name t_type []) 位chk (Kind.Checker.pure (Unit.new)))) 位orig 位name 位body (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.cant_infer_lambda ctx orig)))); (fun orig name body)) +(Kind.Checker.check (Kind.Term.let orig name expr body) type) = (Kind.Checker.bind (Kind.Checker.get_depth) 位dep (Kind.Checker.bind (Kind.Checker.infer expr) 位expr_typ (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name dep)) type) name expr_typ [(Kind.Term.eval expr)]) 位body_chk (Kind.Checker.pure (Unit.new))))) +(Kind.Checker.check (Kind.Term.hlp orig) type) = (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.bind (Kind.Checker.error (Kind.Error.inspection ctx orig type) (Unit.new)) 位x_13 (Kind.Checker.pure (Unit.new)))) +(Kind.Checker.check (Kind.Term.var orig name idx) type) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) 位rhs (Bool.if rhs (Kind.Checker.compare rhs (Kind.Term.var orig name idx) type) (Kind.Checker.extend name type []))) +(Kind.Checker.check (Kind.Term.hol orig numb) type) = (Kind.Checker.pure (Unit.new)) +(Kind.Checker.check term type) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) 位rhs (Kind.Checker.compare rhs term type)) +(Kind.Checker.get_subst) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs subst) +(Kind.Checker.get_right_hand_side) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs rhs) +(Kind.Checker.extend name type vals) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked (Kind.Context.extend context name type vals) (+ depth 1) rhs subst eqts errs (Unit.new)) +(Kind.Context.extend (Kind.Context.empty) name type values) = (Kind.Context.entry name type values (Kind.Context.empty)) +(Kind.Context.extend (Kind.Context.entry n t v rest) name type values) = (Kind.Context.entry n t v (Kind.Context.extend rest name type values)) +(Kind.Checker.get_context) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs context) +(Kind.Term.if_all (Kind.Term.all orig name typ body) func_if else) = (func_if orig name typ body) +(Kind.Term.if_all other func_if else) = else +(Kind.Term.eval (Kind.Term.typ orig)) = (Kind.Term.typ orig) +(Kind.Term.eval (Kind.Term.var orig name index)) = (Kind.Term.var orig name index) +(Kind.Term.eval (Kind.Term.hol orig numb)) = (Kind.Term.hol orig numb) +(Kind.Term.eval (Kind.Term.all orig name typ body)) = (Kind.Term.all orig name (Kind.Term.eval typ) 位x (Kind.Term.eval (body x))) +(Kind.Term.eval (Kind.Term.lam orig name body)) = (Kind.Term.lam orig name 位x (Kind.Term.eval (body x))) +(Kind.Term.eval (Kind.Term.let orig name expr body)) = (Kind.Term.eval_let orig name (Kind.Term.eval expr) 位x (Kind.Term.eval (body x))) +(Kind.Term.eval (Kind.Term.ann orig expr typ)) = (Kind.Term.eval_ann orig (Kind.Term.eval expr) (Kind.Term.eval typ)) +(Kind.Term.eval (Kind.Term.sub orig name indx redx expr)) = (Kind.Term.eval_sub orig name indx redx (Kind.Term.eval expr)) +(Kind.Term.eval (Kind.Term.app orig expr typ)) = (Kind.Term.eval_app orig (Kind.Term.eval expr) (Kind.Term.eval typ)) +(Kind.Term.eval (Kind.Term.hlp orig)) = (Kind.Term.hlp orig) +(Kind.Term.eval (Kind.Term.U60 orig)) = (Kind.Term.U60 orig) +(Kind.Term.eval (Kind.Term.u60 orig num)) = (Kind.Term.u60 orig num) +(Kind.Term.eval (Kind.Term.F60 orig)) = (Kind.Term.F60 orig) +(Kind.Term.eval (Kind.Term.f60 orig num)) = (Kind.Term.f60 orig num) +(Kind.Term.eval (Kind.Term.op2 orig op left right)) = (Kind.Term.eval_op orig op (Kind.Term.eval left) (Kind.Term.eval right)) +(Kind.Term.eval (Kind.Term.ct0 ctid orig)) = (Kind.Term.ct0 ctid orig) +(Kind.Term.eval (Kind.Term.ct1 ctid orig x0)) = (Kind.Term.ct1 ctid orig (Kind.Term.eval x0)) +(Kind.Term.eval (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Term.ct2 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1)) +(Kind.Term.eval (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Term.ct3 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2)) +(Kind.Term.eval (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) = (Kind.Term.ct4 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3)) +(Kind.Term.eval (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Term.ct5 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4)) +(Kind.Term.eval (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.ct6 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5)) +(Kind.Term.eval (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.ct7 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6)) +(Kind.Term.eval (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.ct8 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7)) +(Kind.Term.eval (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.ct9 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8)) +(Kind.Term.eval (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.ct10 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9)) +(Kind.Term.eval (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.ct11 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10)) +(Kind.Term.eval (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.ct12 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11)) +(Kind.Term.eval (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.ct13 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12)) +(Kind.Term.eval (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.ct14 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13)) +(Kind.Term.eval (Kind.Term.ct15 fnid orig x0)) = (Kind.Term.ct15 fnid orig (Kind.Term.eval x0)) +(Kind.Term.eval (Kind.Term.ct16 fnid orig x0)) = (Kind.Term.ct16 fnid orig (Kind.Term.eval x0)) +(Kind.Term.eval (Kind.Term.fn0 fnid orig)) = (Kind.Term.FN0 fnid orig) +(Kind.Term.eval (Kind.Term.fn1 fnid orig x0)) = (Kind.Term.FN1 fnid orig (Kind.Term.eval x0)) +(Kind.Term.eval (Kind.Term.fn2 fnid orig x0 x1)) = (Kind.Term.FN2 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1)) +(Kind.Term.eval (Kind.Term.fn3 fnid orig x0 x1 x2)) = (Kind.Term.FN3 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2)) +(Kind.Term.eval (Kind.Term.fn4 fnid orig x0 x1 x2 x3)) = (Kind.Term.FN4 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3)) +(Kind.Term.eval (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4)) = (Kind.Term.FN5 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4)) +(Kind.Term.eval (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.FN6 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5)) +(Kind.Term.eval (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.FN7 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6)) +(Kind.Term.eval (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.FN8 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7)) +(Kind.Term.eval (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.FN9 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8)) +(Kind.Term.eval (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.FN10 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9)) +(Kind.Term.eval (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.FN11 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10)) +(Kind.Term.eval (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.FN12 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11)) +(Kind.Term.eval (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.FN13 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12)) +(Kind.Term.eval (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.FN14 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13)) +(Kind.Term.eval (Kind.Term.fn15 fnid orig x0)) = (Kind.Term.FN15 fnid orig (Kind.Term.eval x0)) +(Kind.Term.eval (Kind.Term.fn16 fnid orig x0)) = (Kind.Term.FN16 fnid orig (Kind.Term.eval x0)) +(Kind.Term.eval (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = (Kind.Term.args15 (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13) (Kind.Term.eval x14)) +(Kind.Term.eval (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = (Kind.Term.args16 (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13) (Kind.Term.eval x14) (Kind.Term.eval x15)) +(Kind.Term.eval_let orig name expr body) = (body expr) +(Kind.Term.eval_op orig (Kind.Operator.add) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (+ a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.sub) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (- a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.mul) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (* a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.div) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (/ a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.mod) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (% a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.and) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (& a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.or) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (| a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.xor) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (^ a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.shl) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (<< a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.shr) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (>> a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.ltn) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (< a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.lte) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (<= a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.eql) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (== a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.gte) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (>= a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.gtn) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (> a.num b.num)) +(Kind.Term.eval_op orig (Kind.Operator.neq) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (!= a.num b.num)) +(Kind.Term.eval_op orig op left right) = (Kind.Term.op2 orig op left right) +(Kind.Term.eval_app orig (Kind.Term.lam orig1 name body) arg) = (body arg) +(Kind.Term.eval_app orig func arg) = (Kind.Term.app orig func arg) +(Kind.Term.eval_ann orig expr type) = expr +(Kind.Term.eval_sub orig name indx redx expr) = expr +(Kind.Checker.infer (Kind.Term.var orig name index)) = (Kind.Checker.bind (Kind.Checker.find index (Maybe.none) 位n 位t 位v (Maybe.some t)) 位got_type (Maybe.match got_type (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) 位got_type.value (Kind.Checker.pure got_type.value))) +(Kind.Checker.infer (Kind.Term.hol orig numb)) = (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.cant_infer_hole ctx orig))) +(Kind.Checker.infer (Kind.Term.typ orig)) = (Kind.Checker.pure (Kind.Term.typ orig)) +(Kind.Checker.infer (Kind.Term.all orig name type body)) = (Kind.Checker.bind (Kind.Checker.get_depth) 位depth (Kind.Checker.bind (Kind.Checker.check type (Kind.Term.typ orig)) 位x_2 (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name depth)) (Kind.Term.typ orig)) name (Kind.Term.eval type) []) 位x_1 (Kind.Checker.pure (Kind.Term.typ orig))))) +(Kind.Checker.infer (Kind.Term.lam orig name body)) = (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.cant_infer_lambda ctx orig))) +(Kind.Checker.infer (Kind.Term.app orig func argm)) = (Kind.Checker.bind (Kind.Checker.infer func) 位fn_infer (Kind.Checker.bind (Kind.Checker.infer.forall fn_infer 位fn_orig 位fn_name 位fn_type 位fn_body (Kind.Checker.bind (Kind.Checker.check argm fn_type) 位x_3 (Kind.Checker.pure (fn_body (Kind.Term.eval argm)))) (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.invalid_call ctx orig)))) 位ap_infer (Kind.Checker.pure ap_infer))) +(Kind.Checker.infer (Kind.Term.let orig name expr body)) = (Kind.Checker.bind (Kind.Checker.get_depth) 位dep (Kind.Checker.bind (Kind.Checker.infer expr) 位expr_typ (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.infer (body (Kind.Term.var orig name dep))) name expr_typ [(Kind.Term.eval expr)]) 位body_typ (Kind.Checker.pure body_typ)))) +(Kind.Checker.infer (Kind.Term.ann orig expr type)) = let type = (Kind.Term.eval type); (Kind.Checker.bind (Kind.Checker.check expr type) 位x_4 (Kind.Checker.pure type)) +(Kind.Checker.infer (Kind.Term.sub orig name indx redx expr)) = (Kind.Checker.bind (Kind.Checker.get_depth) 位dep (Kind.Checker.bind (Kind.Checker.find indx (Maybe.none) 位n 位t 位v (Maybe.some (Pair.new t v))) 位got (Maybe.match got (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) 位got.value (Pair.match got.value 位got.value.fst 位got.value.snd (Maybe.match (List.at.u60 got.value.snd redx) (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) 位reduction.value (Kind.Checker.bind (Kind.Checker.infer expr) 位expr_typ (Kind.Checker.pure (Kind.Term.eval (Kind.Term.replace expr_typ indx reduction.value))))))))) +(Kind.Checker.infer (Kind.Term.ct0 ctid orig)) = (Kind.Checker.pure (Kind.Term.eval (Kind.Axiom.TypeOf ctid))) +(Kind.Checker.infer (Kind.Term.ct1 ctid orig x0)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0)) +(Kind.Checker.infer (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1)) +(Kind.Checker.infer (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2)) +(Kind.Checker.infer (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3)) +(Kind.Checker.infer (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4)) +(Kind.Checker.infer (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5)) +(Kind.Checker.infer (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6)) +(Kind.Checker.infer (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7)) +(Kind.Checker.infer (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8)) +(Kind.Checker.infer (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9)) +(Kind.Checker.infer (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10)) +(Kind.Checker.infer (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11)) +(Kind.Checker.infer (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12)) +(Kind.Checker.infer (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13)) +(Kind.Checker.infer (Kind.Term.ct15 ctid orig x0)) = let expr = (Kind.Checker.infer_args x0); (Kind.Checker.infer (expr (Kind.Term.ct0 ctid orig) orig)) +(Kind.Checker.infer (Kind.Term.ct16 ctid orig x0)) = let expr = (Kind.Checker.infer_args x0); (Kind.Checker.infer (expr (Kind.Term.ct0 ctid orig) orig)) +(Kind.Checker.infer (Kind.Term.fn0 fnid orig)) = (Kind.Checker.pure (Kind.Term.eval (Kind.Axiom.TypeOf fnid))) +(Kind.Checker.infer (Kind.Term.fn1 fnid orig x0)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0)) +(Kind.Checker.infer (Kind.Term.fn2 fnid orig x0 x1)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1)) +(Kind.Checker.infer (Kind.Term.fn3 fnid orig x0 x1 x2)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2)) +(Kind.Checker.infer (Kind.Term.fn4 fnid orig x0 x1 x2 x3)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3)) +(Kind.Checker.infer (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4)) +(Kind.Checker.infer (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5)) +(Kind.Checker.infer (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6)) +(Kind.Checker.infer (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6) x7)) +(Kind.Checker.infer (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8)) +(Kind.Checker.infer (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9)) +(Kind.Checker.infer (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10)) +(Kind.Checker.infer (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11)) +(Kind.Checker.infer (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12)) +(Kind.Checker.infer (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13)) +(Kind.Checker.infer (Kind.Term.fn15 fnid orig x0)) = let expr = (Kind.Checker.infer_args x0); (Kind.Checker.infer (expr (Kind.Term.fn0 fnid orig) orig)) +(Kind.Checker.infer (Kind.Term.fn16 fnid orig x0)) = let expr = (Kind.Checker.infer_args x0); (Kind.Checker.infer (expr (Kind.Term.fn0 fnid orig) orig)) +(Kind.Checker.infer (Kind.Term.hlp orig)) = (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.inspection ctx orig (Kind.Term.hlp 0)))) +(Kind.Checker.infer (Kind.Term.U60 orig)) = (Kind.Checker.pure (Kind.Term.typ 0)) +(Kind.Checker.infer (Kind.Term.u60 orig numb)) = (Kind.Checker.pure (Kind.Term.U60 0)) +(Kind.Checker.infer (Kind.Term.F60 orig)) = (Kind.Checker.pure (Kind.Term.typ 0)) +(Kind.Checker.infer (Kind.Term.f60 orig numb)) = (Kind.Checker.pure (Kind.Term.F60 0)) +(Kind.Checker.infer (Kind.Term.op2 orig oper left right)) = (Kind.Checker.bind (Kind.Checker.check left (Kind.Term.U60 0)) 位x_6 (Kind.Checker.bind (Kind.Checker.check right (Kind.Term.U60 0)) 位x_5 (Kind.Checker.pure (Kind.Term.U60 0)))) +(Kind.Checker.infer (Kind.Term.args15 x_7 x_8 x_9 x_10 x_11 x_12 x_13 x_14 x_15 x_16 x_17 x_18 x_19 x_20 x_21)) = (Kind.Axiom.Null) +(Kind.Checker.infer (Kind.Term.args16 x_22 x_23 x_24 x_25 x_26 x_27 x_28 x_29 x_30 x_31 x_32 x_33 x_34 x_35 x_36 x_37)) = (Kind.Axiom.Null) +(List.at.u60 [] idx) = (Maybe.none) +(List.at.u60 (List.cons head tail) 0) = (Maybe.some head) +(List.at.u60 (List.cons head tail) idx) = (List.at.u60 tail (- idx 1)) +(Kind.Term.replace (Kind.Term.typ orig) idx val) = (Kind.Term.typ orig) +(Kind.Term.replace (Kind.Term.var orig name index) idx val) = (Bool.if (U60.equal idx index) val (Kind.Term.var orig name index)) +(Kind.Term.replace (Kind.Term.all orig name typ body) idx val) = (Kind.Term.all orig name (Kind.Term.replace typ idx val) 位x (Kind.Term.replace (body x) idx val)) +(Kind.Term.replace (Kind.Term.lam orig name body) idx val) = (Kind.Term.lam orig name 位x (Kind.Term.replace (body x) idx val)) +(Kind.Term.replace (Kind.Term.let orig name expr body) idx val) = (Kind.Term.let orig name (Kind.Term.replace expr idx val) 位x (Kind.Term.replace (body x) idx val)) +(Kind.Term.replace (Kind.Term.ann orig expr typ) idx val) = (Kind.Term.ann orig (Kind.Term.replace expr idx val) (Kind.Term.replace typ idx val)) +(Kind.Term.replace (Kind.Term.sub orig name indx redx expr) idx val) = (Kind.Term.sub orig name indx redx (Kind.Term.replace expr idx val)) +(Kind.Term.replace (Kind.Term.app orig expr typ) idx val) = (Kind.Term.app orig (Kind.Term.replace expr idx val) (Kind.Term.replace typ idx val)) +(Kind.Term.replace (Kind.Term.hlp orig) idx val) = (Kind.Term.hlp orig) +(Kind.Term.replace (Kind.Term.U60 orig) idx val) = (Kind.Term.U60 orig) +(Kind.Term.replace (Kind.Term.u60 orig num) idx val) = (Kind.Term.u60 orig num) +(Kind.Term.replace (Kind.Term.F60 orig) idx val) = (Kind.Term.F60 orig) +(Kind.Term.replace (Kind.Term.f60 orig num) idx val) = (Kind.Term.f60 orig num) +(Kind.Term.replace (Kind.Term.op2 orig op left right) idx val) = (Kind.Term.op2 orig op (Kind.Term.replace left idx val) (Kind.Term.replace right idx val)) +(Kind.Term.replace (Kind.Term.ct0 ctid orig) idx val) = (Kind.Term.ct0 ctid orig) +(Kind.Term.replace (Kind.Term.ct1 ctid orig x0) idx val) = (Kind.Term.ct1 ctid orig (Kind.Term.replace x0 idx val)) +(Kind.Term.replace (Kind.Term.ct2 ctid orig x0 x1) idx val) = (Kind.Term.ct2 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val)) +(Kind.Term.replace (Kind.Term.ct3 ctid orig x0 x1 x2) idx val) = (Kind.Term.ct3 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val)) +(Kind.Term.replace (Kind.Term.ct4 ctid orig x0 x1 x2 x3) idx val) = (Kind.Term.ct4 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val)) +(Kind.Term.replace (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4) idx val) = (Kind.Term.ct5 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val)) +(Kind.Term.replace (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5) idx val) = (Kind.Term.ct6 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val)) +(Kind.Term.replace (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6) idx val) = (Kind.Term.ct7 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val)) +(Kind.Term.replace (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7) idx val) = (Kind.Term.ct8 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val)) +(Kind.Term.replace (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8) idx val) = (Kind.Term.ct9 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val)) +(Kind.Term.replace (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) idx val) = (Kind.Term.ct10 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val)) +(Kind.Term.replace (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) idx val) = (Kind.Term.ct11 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val)) +(Kind.Term.replace (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) idx val) = (Kind.Term.ct12 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val)) +(Kind.Term.replace (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) idx val) = (Kind.Term.ct13 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val)) +(Kind.Term.replace (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) idx val) = (Kind.Term.ct14 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val) (Kind.Term.replace x13 idx val)) +(Kind.Term.replace (Kind.Term.ct15 ctid orig x0) idx val) = (Kind.Term.ct15 ctid orig (Kind.Term.replace x0 idx val)) +(Kind.Term.replace (Kind.Term.ct16 ctid orig x0) idx val) = (Kind.Term.ct16 ctid orig (Kind.Term.replace x0 idx val)) +(Kind.Term.replace (Kind.Term.fn0 fnid orig) idx val) = (Kind.Term.FN0 fnid orig) +(Kind.Term.replace (Kind.Term.fn1 fnid orig x0) idx val) = (Kind.Term.FN1 fnid orig (Kind.Term.replace x0 idx val)) +(Kind.Term.replace (Kind.Term.fn2 fnid orig x0 x1) idx val) = (Kind.Term.FN2 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val)) +(Kind.Term.replace (Kind.Term.fn3 fnid orig x0 x1 x2) idx val) = (Kind.Term.FN3 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val)) +(Kind.Term.replace (Kind.Term.fn4 fnid orig x0 x1 x2 x3) idx val) = (Kind.Term.FN4 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val)) +(Kind.Term.replace (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4) idx val) = (Kind.Term.FN5 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val)) +(Kind.Term.replace (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5) idx val) = (Kind.Term.FN6 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val)) +(Kind.Term.replace (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6) idx val) = (Kind.Term.FN7 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val)) +(Kind.Term.replace (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7) idx val) = (Kind.Term.FN8 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val)) +(Kind.Term.replace (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8) idx val) = (Kind.Term.FN9 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val)) +(Kind.Term.replace (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) idx val) = (Kind.Term.FN10 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val)) +(Kind.Term.replace (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) idx val) = (Kind.Term.FN11 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val)) +(Kind.Term.replace (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) idx val) = (Kind.Term.FN12 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val)) +(Kind.Term.replace (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) idx val) = (Kind.Term.FN13 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val)) +(Kind.Term.replace (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) idx val) = (Kind.Term.FN14 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val) (Kind.Term.replace x13 idx val)) +(Kind.Term.replace (Kind.Term.fn15 ctid orig x0) idx val) = (Kind.Term.FN15 ctid orig (Kind.Term.replace x0 idx val)) +(Kind.Term.replace (Kind.Term.fn16 ctid orig x0) idx val) = (Kind.Term.FN16 ctid orig (Kind.Term.replace x0 idx val)) +(Kind.Term.replace (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) idx val) = (Kind.Term.args15 (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val) (Kind.Term.replace x13 idx val) (Kind.Term.replace x14 idx val)) +(Kind.Term.replace (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) idx val) = (Kind.Term.args16 (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val) (Kind.Term.replace x13 idx val) (Kind.Term.replace x14 idx val) (Kind.Term.replace x15 idx val)) +(Kind.Term.replace (Kind.Term.hol orig numb) idx val) = (Kind.Term.hol orig numb) +(U60.equal a b) = (U60.to_bool (== a b)) +(U60.to_bool 0) = (Bool.false) +(U60.to_bool n) = (Bool.true) +(Bool.if (Bool.true) t f) = t +(Bool.if (Bool.false) t f) = f +(Kind.Checker.pure res) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs res) +(Kind.Checker.infer_args (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = 位term 位orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig term x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13) x14) +(Kind.Checker.infer_args (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = 位term 位orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig term x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13) x14) x15) +(Kind.Checker.infer_args term) = 位x_ 位orig term +(Kind.Checker.infer.forall (Kind.Term.all orig name type body) then_fn else_val) = (then_fn orig name type body) +(Kind.Checker.infer.forall (Kind.Term.var orig name index) then_fn else_val) = (Kind.Checker.bind (Kind.Checker.find index [] 位n 位t 位v v) 位reducs (Kind.Checker.bind (Kind.Checker.infer.forall.try_values reducs then_fn else_val) 位result (Kind.Checker.pure result))) +(Kind.Checker.infer.forall other then_fn else_val) = else_val (Kind.Checker.bind checker then) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Checker.bind.result (checker context depth rhs subst eqts errs) then) (Kind.Checker.bind.result (Kind.Result.checked context depth rhs sub equations errs ret) then) = (then ret context depth rhs sub equations errs) (Kind.Checker.bind.result (Kind.Result.errored context sub errs) then) = (Kind.Result.errored context sub errs) -(Kind.Checker.get_equations) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs eqts) -(Kind.Checker.unify.go [] [] changed) = (Kind.Checker.pure (Unit.new)) -(Kind.Checker.unify.go [] unsolved (Bool.true)) = (Kind.Checker.unify.go unsolved [] (Bool.false)) -(Kind.Checker.unify.go [] unsolved (Bool.false)) = (Kind.Checker.unify.go.fail unsolved) -(Kind.Checker.unify.go (List.cons (Kind.Equation.new ctx orig left right) equations) unsolved changed) = (Kind.Checker.bind (Kind.Checker.with_context (Kind.Checker.equal (Kind.Term.eval left) (Kind.Term.eval right)) ctx) 位is_equal let unify = (Bool.if is_equal 位equations 位unsolved (Kind.Checker.unify.go equations unsolved (Bool.true)) 位equations 位unsolved let eqt = (Kind.Equation.new ctx orig left right); (Kind.Checker.unify.go equations (List.cons eqt unsolved) changed)); (unify equations unsolved)) -(Bool.if (Bool.true) t f) = t -(Bool.if (Bool.false) t f) = f -(Kind.Checker.unify.go.fail []) = (Kind.Checker.pure (Unit.new)) -(Kind.Checker.unify.go.fail (List.cons (Kind.Equation.new ctx orig left right) eqts)) = (Kind.Checker.bind (Kind.Checker.error (Kind.Error.type_mismatch ctx orig left right) (Unit.new)) 位x_1 (Kind.Checker.unify.go.fail eqts)) +(Kind.Checker.find index alt fun) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs (Kind.Context.find context index alt fun)) +(Kind.Context.find (Kind.Context.entry name type vals rest) 0 alt fun) = (fun name type vals) +(Kind.Context.find (Kind.Context.entry name type vals rest) n alt fun) = (Kind.Context.find rest (- n 1) alt fun) +(Kind.Context.find (Kind.Context.empty) n alt fun) = alt +(Kind.Checker.infer.forall.try_values (List.cons (Kind.Term.all orig name type body) terms) then_fn else_val) = (then_fn orig name type body) +(Kind.Checker.infer.forall.try_values (List.cons other terms) then_fn else_val) = (Kind.Checker.infer.forall.try_values terms then_fn else_val) +(Kind.Checker.infer.forall.try_values [] then_fn else_val) = else_val +(Maybe.match (Maybe.none) none some) = none +(Maybe.match (Maybe.some value_) none some) = (some value_) +(Kind.Checker.get_depth) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs depth) +(Pair.match (Pair.new fst_ snd_) new) = (new fst_ snd_) +(Kind.Checker.extended checker name type vals) = (Kind.Checker.bind (Kind.Checker.extend name type vals) 位x_2 (Kind.Checker.bind checker 位got (Kind.Checker.bind (Kind.Checker.shrink) 位x_1 (Kind.Checker.pure got)))) +(Kind.Checker.shrink) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked (Kind.Context.shrink context) (- depth 1) rhs subst eqts errs (Unit.new)) +(Kind.Context.shrink (Kind.Context.empty)) = (Kind.Context.empty) +(Kind.Context.shrink (Kind.Context.entry name type vals (Kind.Context.empty))) = (Kind.Context.empty) +(Kind.Context.shrink (Kind.Context.entry name type vals rest)) = (Kind.Context.entry name type vals (Kind.Context.shrink rest)) +(Kind.Checker.fail err) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.errored context subst (List.cons err errs)) (Kind.Checker.error err ret) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts (List.cons err errs) ret) -(Kind.Checker.pure res) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs res) +(Kind.Checker.compare rhs term type) = (Kind.Term.get_origin term 位orig 位term (Kind.Checker.bind (Kind.Checker.infer term) 位term_typ let fun = (Bool.if rhs 位term_typ 位type (Kind.Checker.new_equation orig type term_typ) 位term_typ 位type (Kind.Checker.bind (Kind.Checker.equal (Kind.Term.eval term_typ) (Kind.Term.eval type)) 位is_equal (Bool.if is_equal (Kind.Checker.pure (Unit.new)) (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.impossible_case ctx orig type term_typ)))))); (fun term_typ type))) +(Kind.Term.get_origin (Kind.Term.typ orig) got) = (got orig (Kind.Term.typ orig)) +(Kind.Term.get_origin (Kind.Term.var orig name index) got) = (got orig (Kind.Term.var orig name index)) +(Kind.Term.get_origin (Kind.Term.hol orig numb) got) = (got orig (Kind.Term.hol orig numb)) +(Kind.Term.get_origin (Kind.Term.all orig name typ body) got) = (got orig (Kind.Term.all orig name typ body)) +(Kind.Term.get_origin (Kind.Term.lam orig name body) got) = (got orig (Kind.Term.lam orig name body)) +(Kind.Term.get_origin (Kind.Term.let orig name expr body) got) = (got orig (Kind.Term.let orig name expr body)) +(Kind.Term.get_origin (Kind.Term.ann orig expr typ) got) = (got orig (Kind.Term.ann orig expr typ)) +(Kind.Term.get_origin (Kind.Term.sub orig name indx redx expr) got) = (got orig (Kind.Term.sub orig name indx redx expr)) +(Kind.Term.get_origin (Kind.Term.app orig func arg) got) = (got orig (Kind.Term.app orig func arg)) +(Kind.Term.get_origin (Kind.Term.hlp orig) got) = (got orig (Kind.Term.hlp orig)) +(Kind.Term.get_origin (Kind.Term.U60 orig) got) = (got orig (Kind.Term.U60 orig)) +(Kind.Term.get_origin (Kind.Term.u60 orig num) got) = (got orig (Kind.Term.u60 orig num)) +(Kind.Term.get_origin (Kind.Term.F60 orig) got) = (got orig (Kind.Term.F60 orig)) +(Kind.Term.get_origin (Kind.Term.f60 orig num) got) = (got orig (Kind.Term.f60 orig num)) +(Kind.Term.get_origin (Kind.Term.op2 orig op left right) got) = (got orig (Kind.Term.op2 orig op left right)) +(Kind.Term.get_origin (Kind.Term.ct0 ctid orig) got) = (got orig (Kind.Term.ct0 ctid orig)) +(Kind.Term.get_origin (Kind.Term.ct1 ctid orig x0) got) = (got orig (Kind.Term.ct1 ctid orig x0)) +(Kind.Term.get_origin (Kind.Term.ct2 ctid orig x0 x1) got) = (got orig (Kind.Term.ct2 ctid orig x0 x1)) +(Kind.Term.get_origin (Kind.Term.ct3 ctid orig x0 x1 x2) got) = (got orig (Kind.Term.ct3 ctid orig x0 x1 x2)) +(Kind.Term.get_origin (Kind.Term.ct4 ctid orig x0 x1 x2 x3) got) = (got orig (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) +(Kind.Term.get_origin (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4) got) = (got orig (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) +(Kind.Term.get_origin (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5) got) = (got orig (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) +(Kind.Term.get_origin (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6) got) = (got orig (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6)) +(Kind.Term.get_origin (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7) got) = (got orig (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) +(Kind.Term.get_origin (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8) got) = (got orig (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) +(Kind.Term.get_origin (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) got) = (got orig (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) +(Kind.Term.get_origin (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) got) = (got orig (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) +(Kind.Term.get_origin (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) got) = (got orig (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) +(Kind.Term.get_origin (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) got) = (got orig (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) +(Kind.Term.get_origin (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) got) = (got orig (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) +(Kind.Term.get_origin (Kind.Term.ct15 fnid orig args) got) = (got orig (Kind.Term.ct15 fnid orig args)) +(Kind.Term.get_origin (Kind.Term.ct16 fnid orig args) got) = (got orig (Kind.Term.ct16 fnid orig args)) +(Kind.Term.get_origin (Kind.Term.fn0 fnid orig) got) = (got orig (Kind.Term.fn0 fnid orig)) +(Kind.Term.get_origin (Kind.Term.fn1 fnid orig x0) got) = (got orig (Kind.Term.fn1 fnid orig x0)) +(Kind.Term.get_origin (Kind.Term.fn2 fnid orig x0 x1) got) = (got orig (Kind.Term.fn2 fnid orig x0 x1)) +(Kind.Term.get_origin (Kind.Term.fn3 fnid orig x0 x1 x2) got) = (got orig (Kind.Term.fn3 fnid orig x0 x1 x2)) +(Kind.Term.get_origin (Kind.Term.fn4 fnid orig x0 x1 x2 x3) got) = (got orig (Kind.Term.fn4 fnid orig x0 x1 x2 x3)) +(Kind.Term.get_origin (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4) got) = (got orig (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4)) +(Kind.Term.get_origin (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5) got) = (got orig (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5)) +(Kind.Term.get_origin (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6) got) = (got orig (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6)) +(Kind.Term.get_origin (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7) got) = (got orig (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7)) +(Kind.Term.get_origin (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8) got) = (got orig (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) +(Kind.Term.get_origin (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) got) = (got orig (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) +(Kind.Term.get_origin (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) got) = (got orig (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) +(Kind.Term.get_origin (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) got) = (got orig (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) +(Kind.Term.get_origin (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) got) = (got orig (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) +(Kind.Term.get_origin (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) got) = (got orig (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) +(Kind.Term.get_origin (Kind.Term.fn15 fnid orig args) got) = (got orig (Kind.Term.fn15 fnid orig args)) +(Kind.Term.get_origin (Kind.Term.fn16 fnid orig args) got) = (got orig (Kind.Term.fn16 fnid orig args)) +(Kind.Term.get_origin (Kind.Term.args15 x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9 x_10 x_11 x_12 x_13 x_14 x_15) got) = (Kind.Axiom.Null) +(Kind.Term.get_origin (Kind.Term.args16 x_16 x_17 x_18 x_19 x_20 x_21 x_22 x_23 x_24 x_25 x_26 x_27 x_28 x_29 x_30 x_31) got) = (Kind.Axiom.Null) +(Kind.Checker.new_equation orig left right) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst (List.append eqts (Kind.Equation.new context orig left right)) errs (Unit.new)) +(List.append [] x) = [x] +(List.append (List.cons xs.h xs.t) x) = (List.cons xs.h (List.append xs.t x)) (Kind.Checker.equal (Kind.Term.typ orig) (Kind.Term.typ orig1)) = (Kind.Checker.pure (Bool.true)) (Kind.Checker.equal (Kind.Term.all a.orig a.name a.type a.body) (Kind.Term.all b.orig b.name b.type b.body)) = (Kind.Checker.bind (Kind.Checker.get_depth) 位dep (Kind.Checker.bind (Kind.Checker.equal a.type b.type) 位type (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.equal (a.body (Kind.Term.var a.orig a.name dep)) (b.body (Kind.Term.var b.orig b.name dep))) (Kind.Axiom.Null) (Kind.Axiom.Null) []) 位body (Kind.Checker.pure (Bool.and type body))))) (Kind.Checker.equal (Kind.Term.lam a.orig a.name a.body) (Kind.Term.lam b.orig b.name b.body)) = (Kind.Checker.bind (Kind.Checker.get_depth) 位dep (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.equal (a.body (Kind.Term.var a.orig a.name dep)) (b.body (Kind.Term.var b.orig b.name dep))) (Kind.Axiom.Null) (Kind.Axiom.Null) []) 位body (Kind.Checker.pure body))) @@ -222,29 +335,16 @@ (Kind.Checker.equal (Kind.Term.fn15 a.fnid a.orig a.args) (Kind.Term.fn15 b.fnid b.orig b.args)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) 位xargs (Kind.Checker.pure (Bool.and fnid xargs))) (Kind.Checker.equal (Kind.Term.fn16 a.fnid a.orig a.args) (Kind.Term.fn16 b.fnid b.orig b.args)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) 位xargs (Kind.Checker.pure (Bool.and fnid xargs))) (Kind.Checker.equal a b) = (Kind.Checker.bind (Kind.Checker.get_subst) 位sub (Bool.if (Bool.or (Kind.Term.fillable a sub) (Kind.Term.fillable b sub)) (Kind.Checker.equal (Kind.Term.fill a sub) (Kind.Term.fill b sub)) (Kind.Checker.pure (Bool.false)))) -(Kind.Operator.equal (Kind.Operator.and) (Kind.Operator.and)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.sub) (Kind.Operator.sub)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.mul) (Kind.Operator.mul)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.div) (Kind.Operator.div)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.mod) (Kind.Operator.mod)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.and) (Kind.Operator.and)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.or) (Kind.Operator.or)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.xor) (Kind.Operator.xor)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.shl) (Kind.Operator.shl)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.shr) (Kind.Operator.shr)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.ltn) (Kind.Operator.ltn)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.lte) (Kind.Operator.lte)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.eql) (Kind.Operator.eql)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.gte) (Kind.Operator.gte)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.gtn) (Kind.Operator.gtn)) = (Bool.true) -(Kind.Operator.equal (Kind.Operator.neq) (Kind.Operator.neq)) = (Bool.true) -(Kind.Operator.equal a b) = (Bool.false) +(Bool.or (Bool.true) b) = (Bool.true) +(Bool.or (Bool.false) b) = b (Kind.Term.fillable term (Kind.Subst.end)) = (Bool.false) (Kind.Term.fillable (Kind.Term.typ orig) sub) = (Bool.false) (Kind.Term.fillable (Kind.Term.var orig name index) sub) = (Bool.false) (Kind.Term.fillable (Kind.Term.hlp orig) sub) = (Bool.false) (Kind.Term.fillable (Kind.Term.U60 orig) sub) = (Bool.false) (Kind.Term.fillable (Kind.Term.u60 orig num) sub) = (Bool.false) +(Kind.Term.fillable (Kind.Term.F60 orig) sub) = (Bool.false) +(Kind.Term.fillable (Kind.Term.f60 orig num) sub) = (Bool.false) (Kind.Term.fillable (Kind.Term.all orig name typ body) sub) = (Bool.or (Kind.Term.fillable typ sub) (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub)) (Kind.Term.fillable (Kind.Term.lam orig name body) sub) = (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub) (Kind.Term.fillable (Kind.Term.app orig expr typ) sub) = (Bool.or (Kind.Term.fillable expr sub) (Kind.Term.fillable typ sub)) @@ -297,19 +397,6 @@ (Kind.Subst.look (Kind.Subst.sub term rest) n) = (Kind.Subst.look rest (- n 1)) (Maybe.is_some (Maybe.none)) = (Bool.false) (Maybe.is_some (Maybe.some v)) = (Bool.true) -(Bool.or (Bool.true) b) = (Bool.true) -(Bool.or (Bool.false) b) = b -(Bool.and (Bool.true) b) = b -(Bool.and (Bool.false) b) = (Bool.false) -(Kind.Checker.get_subst) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs subst) -(Kind.Checker.extended checker name type vals) = (Kind.Checker.bind (Kind.Checker.extend name type vals) 位x_2 (Kind.Checker.bind checker 位got (Kind.Checker.bind (Kind.Checker.shrink) 位x_1 (Kind.Checker.pure got)))) -(Kind.Checker.shrink) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked (Kind.Context.shrink context) (- depth 1) rhs subst eqts errs (Unit.new)) -(Kind.Context.shrink (Kind.Context.empty)) = (Kind.Context.empty) -(Kind.Context.shrink (Kind.Context.entry name type vals (Kind.Context.empty))) = (Kind.Context.empty) -(Kind.Context.shrink (Kind.Context.entry name type vals rest)) = (Kind.Context.entry name type vals (Kind.Context.shrink rest)) -(Kind.Checker.extend name type vals) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked (Kind.Context.extend context name type vals) (+ depth 1) rhs subst eqts errs (Unit.new)) -(Kind.Context.extend (Kind.Context.empty) name type values) = (Kind.Context.entry name type values (Kind.Context.empty)) -(Kind.Context.extend (Kind.Context.entry n t v rest) name type values) = (Kind.Context.entry n t v (Kind.Context.extend rest name type values)) (Kind.Checker.equal.hol a.orig a.numb b) = (Kind.Checker.bind (Kind.Checker.look a.numb) 位got (Kind.Checker.bind (Kind.Checker.equal.hol.val got a.orig a.numb b) 位res (Kind.Checker.pure res))) (Kind.Checker.equal.hol.val (Maybe.none) orig numb b) = (Kind.Checker.bind (Kind.Checker.fill numb b) 位x_1 (Kind.Checker.pure (Bool.true))) (Kind.Checker.equal.hol.val (Maybe.some val) orig numb b) = (Kind.Checker.equal val b) @@ -321,22 +408,6 @@ (Kind.Subst.fill (Kind.Subst.unfilled rest) n term) = (Kind.Subst.unfilled (Kind.Subst.fill rest (- n 1) term)) (Kind.Subst.fill (Kind.Subst.sub keep rest) n term) = (Kind.Subst.sub keep (Kind.Subst.fill rest (- n 1) term)) (Kind.Checker.look index) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs (Kind.Subst.look subst index)) -(Kind.Checker.equal.var (Bool.false) orig name idx b) = (Kind.Checker.bind (Kind.Checker.add_value idx b) 位x_1 (Kind.Checker.pure (Bool.true))) -(Kind.Checker.equal.var (Bool.true) a.orig a.name a.idx (Kind.Term.var b.orig b.name b.idx)) = (Bool.if (U60.equal a.idx b.idx) (Kind.Checker.pure (Bool.true)) (Kind.Checker.bind (Kind.Checker.find a.idx [] 位n 位t 位v v) 位a.val (Kind.Checker.bind (Kind.Checker.find b.idx [] 位n 位t 位v v) 位b.val (Kind.Checker.bind (Kind.Checker.equal.var.try_values a.val (Kind.Term.var b.orig b.name b.idx)) 位a.chk (Kind.Checker.bind (Kind.Checker.equal.var.try_values b.val (Kind.Term.var a.orig a.name a.idx)) 位b.chk (Kind.Checker.pure (Bool.or a.chk b.chk))))))) -(Kind.Checker.equal.var (Bool.true) a.orig a.name a.idx b) = (Kind.Checker.bind (Kind.Checker.get_subst) 位sub (Bool.if (Kind.Term.fillable b sub) (Kind.Checker.equal (Kind.Term.var a.orig a.name a.idx) (Kind.Term.fill b sub)) (Kind.Checker.bind (Kind.Checker.find a.idx [] 位n 位t 位v v) 位a.val (Kind.Checker.bind (Kind.Checker.equal.var.try_values a.val b) 位res (Kind.Checker.pure res))))) -(Kind.Checker.equal.var.try_values [] term) = (Kind.Checker.pure (Bool.false)) -(Kind.Checker.equal.var.try_values (List.cons x xs) term) = (Kind.Checker.bind (Kind.Checker.equal x term) 位head (Bool.if head (Kind.Checker.pure (Bool.true)) (Kind.Checker.equal.var.try_values xs term))) -(Kind.Checker.find index alt fun) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs (Kind.Context.find context index alt fun)) -(Kind.Context.find (Kind.Context.entry name type vals rest) 0 alt fun) = (fun name type vals) -(Kind.Context.find (Kind.Context.entry name type vals rest) n alt fun) = (Kind.Context.find rest (- n 1) alt fun) -(Kind.Context.find (Kind.Context.empty) n alt fun) = alt -(U60.equal a b) = (U60.to_bool (== a b)) -(U60.to_bool 0) = (Bool.false) -(U60.to_bool n) = (Bool.true) -(Kind.Checker.add_value idx val) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked (Kind.Context.add_value context idx val) depth rhs subst eqts errs (Unit.new)) -(Kind.Context.add_value (Kind.Context.entry name type vals rest) 0 val) = (Kind.Context.entry name type (List.cons val vals) rest) -(Kind.Context.add_value (Kind.Context.entry name type vals rest) n val) = (Kind.Context.entry name type vals (Kind.Context.add_value rest (- n 1) val)) -(Kind.Context.add_value (Kind.Context.empty) n val) = (Kind.Context.empty) (Kind.Term.fill term (Kind.Subst.end)) = term (Kind.Term.fill (Kind.Term.typ orig) sub) = (Kind.Term.typ orig) (Kind.Term.fill (Kind.Term.var orig name index) sub) = (Kind.Term.var orig name index) @@ -348,6 +419,8 @@ (Kind.Term.fill (Kind.Term.app orig expr typ) sub) = (Kind.Term.eval_app orig (Kind.Term.fill expr sub) (Kind.Term.fill typ sub)) (Kind.Term.fill (Kind.Term.hlp orig) sub) = (Kind.Term.hlp orig) (Kind.Term.fill (Kind.Term.U60 orig) sub) = (Kind.Term.U60 orig) +(Kind.Term.fill (Kind.Term.F60 orig) sub) = (Kind.Term.F60 orig) +(Kind.Term.fill (Kind.Term.f60 orig num) sub) = (Kind.Term.f60 orig num) (Kind.Term.fill (Kind.Term.u60 orig num) sub) = (Kind.Term.u60 orig num) (Kind.Term.fill (Kind.Term.op2 orig op left right) sub) = (Kind.Term.op2 orig op (Kind.Term.fill left sub) (Kind.Term.fill right sub)) (Kind.Term.fill (Kind.Term.ct0 ctid orig) sub) = (Kind.Term.ct0 ctid orig) @@ -387,145 +460,91 @@ (Kind.Term.fill (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) sub) = (Kind.Term.args15 (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub) (Kind.Term.fill x2 sub) (Kind.Term.fill x3 sub) (Kind.Term.fill x4 sub) (Kind.Term.fill x5 sub) (Kind.Term.fill x6 sub) (Kind.Term.fill x7 sub) (Kind.Term.fill x8 sub) (Kind.Term.fill x9 sub) (Kind.Term.fill x10 sub) (Kind.Term.fill x11 sub) (Kind.Term.fill x12 sub) (Kind.Term.fill x13 sub) (Kind.Term.fill x14 sub)) (Kind.Term.fill (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) sub) = (Kind.Term.args16 (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub) (Kind.Term.fill x2 sub) (Kind.Term.fill x3 sub) (Kind.Term.fill x4 sub) (Kind.Term.fill x5 sub) (Kind.Term.fill x6 sub) (Kind.Term.fill x7 sub) (Kind.Term.fill x8 sub) (Kind.Term.fill x9 sub) (Kind.Term.fill x10 sub) (Kind.Term.fill x11 sub) (Kind.Term.fill x12 sub) (Kind.Term.fill x13 sub) (Kind.Term.fill x14 sub) (Kind.Term.fill x15 sub)) (Kind.Term.fill (Kind.Term.hol orig numb) sub) = let substRes = (Kind.Subst.look sub numb); (Maybe.match substRes (Kind.Term.hol orig numb) 位value (Kind.Term.fill value sub)) -(Kind.Term.eval_ann orig expr type) = expr -(Kind.Term.eval_let orig name expr body) = (body expr) -(Kind.Term.eval_sub orig name indx redx expr) = expr -(Kind.Term.eval_app orig (Kind.Term.lam orig1 name body) arg) = (body arg) -(Kind.Term.eval_app orig func arg) = (Kind.Term.app orig func arg) -(Kind.Checker.get_depth) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs depth) -(Kind.Checker.get_right_hand_side) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs rhs) -(Kind.Checker.with_context checker new_context) = (Kind.Checker.bind (Kind.Checker.set_context new_context) 位old_context (Kind.Checker.bind checker 位got (Kind.Checker.bind (Kind.Checker.set_context old_context) 位x_1 (Kind.Checker.pure got)))) -(Kind.Checker.set_context new_context) = 位old_context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked new_context depth rhs subst eqts errs old_context) -(Kind.Term.eval (Kind.Term.typ orig)) = (Kind.Term.typ orig) -(Kind.Term.eval (Kind.Term.var orig name index)) = (Kind.Term.var orig name index) -(Kind.Term.eval (Kind.Term.hol orig numb)) = (Kind.Term.hol orig numb) -(Kind.Term.eval (Kind.Term.all orig name typ body)) = (Kind.Term.all orig name (Kind.Term.eval typ) 位x (Kind.Term.eval (body x))) -(Kind.Term.eval (Kind.Term.lam orig name body)) = (Kind.Term.lam orig name 位x (Kind.Term.eval (body x))) -(Kind.Term.eval (Kind.Term.let orig name expr body)) = (Kind.Term.eval_let orig name (Kind.Term.eval expr) 位x (Kind.Term.eval (body x))) -(Kind.Term.eval (Kind.Term.ann orig expr typ)) = (Kind.Term.eval_ann orig (Kind.Term.eval expr) (Kind.Term.eval typ)) -(Kind.Term.eval (Kind.Term.sub orig name indx redx expr)) = (Kind.Term.eval_sub orig name indx redx (Kind.Term.eval expr)) -(Kind.Term.eval (Kind.Term.app orig expr typ)) = (Kind.Term.eval_app orig (Kind.Term.eval expr) (Kind.Term.eval typ)) -(Kind.Term.eval (Kind.Term.hlp orig)) = (Kind.Term.hlp orig) -(Kind.Term.eval (Kind.Term.U60 orig)) = (Kind.Term.U60 orig) -(Kind.Term.eval (Kind.Term.u60 orig num)) = (Kind.Term.u60 orig num) -(Kind.Term.eval (Kind.Term.op2 orig op left right)) = (Kind.Term.eval_op orig op (Kind.Term.eval left) (Kind.Term.eval right)) -(Kind.Term.eval (Kind.Term.ct0 ctid orig)) = (Kind.Term.ct0 ctid orig) -(Kind.Term.eval (Kind.Term.ct1 ctid orig x0)) = (Kind.Term.ct1 ctid orig (Kind.Term.eval x0)) -(Kind.Term.eval (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Term.ct2 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1)) -(Kind.Term.eval (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Term.ct3 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2)) -(Kind.Term.eval (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) = (Kind.Term.ct4 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3)) -(Kind.Term.eval (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Term.ct5 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4)) -(Kind.Term.eval (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.ct6 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5)) -(Kind.Term.eval (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.ct7 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6)) -(Kind.Term.eval (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.ct8 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7)) -(Kind.Term.eval (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.ct9 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8)) -(Kind.Term.eval (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.ct10 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9)) -(Kind.Term.eval (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.ct11 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10)) -(Kind.Term.eval (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.ct12 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11)) -(Kind.Term.eval (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.ct13 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12)) -(Kind.Term.eval (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.ct14 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13)) -(Kind.Term.eval (Kind.Term.ct15 fnid orig x0)) = (Kind.Term.ct15 fnid orig (Kind.Term.eval x0)) -(Kind.Term.eval (Kind.Term.ct16 fnid orig x0)) = (Kind.Term.ct16 fnid orig (Kind.Term.eval x0)) -(Kind.Term.eval (Kind.Term.fn0 fnid orig)) = (Kind.Term.FN0 fnid orig) -(Kind.Term.eval (Kind.Term.fn1 fnid orig x0)) = (Kind.Term.FN1 fnid orig (Kind.Term.eval x0)) -(Kind.Term.eval (Kind.Term.fn2 fnid orig x0 x1)) = (Kind.Term.FN2 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1)) -(Kind.Term.eval (Kind.Term.fn3 fnid orig x0 x1 x2)) = (Kind.Term.FN3 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2)) -(Kind.Term.eval (Kind.Term.fn4 fnid orig x0 x1 x2 x3)) = (Kind.Term.FN4 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3)) -(Kind.Term.eval (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4)) = (Kind.Term.FN5 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4)) -(Kind.Term.eval (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.FN6 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5)) -(Kind.Term.eval (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.FN7 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6)) -(Kind.Term.eval (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.FN8 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7)) -(Kind.Term.eval (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.FN9 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8)) -(Kind.Term.eval (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.FN10 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9)) -(Kind.Term.eval (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.FN11 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10)) -(Kind.Term.eval (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.FN12 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11)) -(Kind.Term.eval (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.FN13 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12)) -(Kind.Term.eval (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.FN14 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13)) -(Kind.Term.eval (Kind.Term.fn15 fnid orig x0)) = (Kind.Term.FN15 fnid orig (Kind.Term.eval x0)) -(Kind.Term.eval (Kind.Term.fn16 fnid orig x0)) = (Kind.Term.FN16 fnid orig (Kind.Term.eval x0)) -(Kind.Term.eval (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = (Kind.Term.args15 (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13) (Kind.Term.eval x14)) -(Kind.Term.eval (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = (Kind.Term.args16 (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13) (Kind.Term.eval x14) (Kind.Term.eval x15)) -(Kind.Term.eval_op orig (Kind.Operator.add) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (+ a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.sub) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (- a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.mul) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (* a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.div) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (/ a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.mod) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (% a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.and) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (& a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.or) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (| a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.xor) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (^ a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.shl) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (<< a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.shr) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (>> a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.ltn) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (< a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.lte) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (<= a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.eql) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (== a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.gte) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (>= a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.gtn) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (> a.num b.num)) -(Kind.Term.eval_op orig (Kind.Operator.neq) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (!= a.num b.num)) -(Kind.Term.eval_op orig op left right) = (Kind.Term.op2 orig op left right) -(Kind.Coverage.check fnid) = let rules = (Kind.Axiom.RuleOf fnid); let type = (Kind.Axiom.TypeOf fnid); let problem = (Kind.Coverage.Problem.new type rules (Maybe.default (Maybe.map 位x (Kind.Coverage.Rule.size x) (List.head rules)) 0)); (Kind.Checker.bind (Kind.Coverage.solve problem) 位result (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.bind (Maybe.match result (Kind.Checker.pure (Unit.new)) 位result.value (Kind.Checker.fail (Kind.Error.uncovered_pattern ctx (Kind.Axiom.OrigOf fnid) result.value))) 位x_1 (Kind.Checker.pure (Unit.new))))) -(Kind.Checker.get_context) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs context) -(List.head []) = (Maybe.none) -(List.head (List.cons head tail)) = (Maybe.some head) -(Kind.Checker.fail err) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.errored context subst (List.cons err errs)) +(Kind.Checker.equal.var (Bool.false) orig name idx b) = (Kind.Checker.bind (Kind.Checker.add_value idx b) 位x_1 (Kind.Checker.pure (Bool.true))) +(Kind.Checker.equal.var (Bool.true) a.orig a.name a.idx (Kind.Term.var b.orig b.name b.idx)) = (Bool.if (U60.equal a.idx b.idx) (Kind.Checker.pure (Bool.true)) (Kind.Checker.bind (Kind.Checker.find a.idx [] 位n 位t 位v v) 位a.val (Kind.Checker.bind (Kind.Checker.find b.idx [] 位n 位t 位v v) 位b.val (Kind.Checker.bind (Kind.Checker.equal.var.try_values a.val (Kind.Term.var b.orig b.name b.idx)) 位a.chk (Kind.Checker.bind (Kind.Checker.equal.var.try_values b.val (Kind.Term.var a.orig a.name a.idx)) 位b.chk (Kind.Checker.pure (Bool.or a.chk b.chk))))))) +(Kind.Checker.equal.var (Bool.true) a.orig a.name a.idx b) = (Kind.Checker.bind (Kind.Checker.get_subst) 位sub (Bool.if (Kind.Term.fillable b sub) (Kind.Checker.equal (Kind.Term.var a.orig a.name a.idx) (Kind.Term.fill b sub)) (Kind.Checker.bind (Kind.Checker.find a.idx [] 位n 位t 位v v) 位a.val (Kind.Checker.bind (Kind.Checker.equal.var.try_values a.val b) 位res (Kind.Checker.pure res))))) +(Kind.Checker.add_value idx val) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked (Kind.Context.add_value context idx val) depth rhs subst eqts errs (Unit.new)) +(Kind.Context.add_value (Kind.Context.entry name type vals rest) 0 val) = (Kind.Context.entry name type (List.cons val vals) rest) +(Kind.Context.add_value (Kind.Context.entry name type vals rest) n val) = (Kind.Context.entry name type vals (Kind.Context.add_value rest (- n 1) val)) +(Kind.Context.add_value (Kind.Context.empty) n val) = (Kind.Context.empty) +(Kind.Checker.equal.var.try_values [] term) = (Kind.Checker.pure (Bool.false)) +(Kind.Checker.equal.var.try_values (List.cons x xs) term) = (Kind.Checker.bind (Kind.Checker.equal x term) 位head (Bool.if head (Kind.Checker.pure (Bool.true)) (Kind.Checker.equal.var.try_values xs term))) +(Kind.Operator.equal (Kind.Operator.and) (Kind.Operator.and)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.sub) (Kind.Operator.sub)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.mul) (Kind.Operator.mul)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.div) (Kind.Operator.div)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.mod) (Kind.Operator.mod)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.and) (Kind.Operator.and)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.or) (Kind.Operator.or)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.xor) (Kind.Operator.xor)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.shl) (Kind.Operator.shl)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.shr) (Kind.Operator.shr)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.ltn) (Kind.Operator.ltn)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.lte) (Kind.Operator.lte)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.eql) (Kind.Operator.eql)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.gte) (Kind.Operator.gte)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.gtn) (Kind.Operator.gtn)) = (Bool.true) +(Kind.Operator.equal (Kind.Operator.neq) (Kind.Operator.neq)) = (Bool.true) +(Kind.Operator.equal a b) = (Bool.false) +(Bool.and (Bool.true) b) = b +(Bool.and (Bool.false) b) = (Bool.false) +(Kind.Coverage.check fnid) = (Kind.Checker.bind (Kind.Checker.set_right_hand_side (Bool.false)) 位x_1 let rules = (Kind.Axiom.RuleOf fnid); let type = (Kind.Axiom.TypeOf fnid); let size = (Maybe.default (Maybe.map 位x (Kind.Coverage.Rule.size x) (List.head rules)) 0); let new_type = (Kind.Coverage.Type.from_term type size); let problem = (Kind.Coverage.Problem.new new_type rules); (Kind.Checker.bind (Kind.Coverage.solve problem) 位result (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Maybe.match result (Kind.Checker.pure (Unit.new)) 位result.value (Kind.Checker.fail (Kind.Error.uncovered_pattern ctx (Kind.Axiom.OrigOf fnid) result.value)))))) (Maybe.default (Maybe.none) dflt) = dflt (Maybe.default (Maybe.some val) dflt) = val -(Maybe.map f (Maybe.none)) = (Maybe.none) -(Maybe.map f (Maybe.some v)) = (Maybe.some (f v)) -(Kind.Coverage.Rule.size (Kind.Rule.lhs x xs)) = (+ 1 (Kind.Coverage.Rule.size xs)) -(Kind.Coverage.Rule.size x_1) = 0 -(Kind.Coverage.solve problem) = (Kind.Coverage.done problem (Kind.Term.if_all (Kind.Coverage.Problem.type.get problem) 位orig_ 位name_ 位type 位body (Bool.if (Kind.Coverage.catches problem) (Kind.Coverage.intro_all type body problem) (Kind.Coverage.specialize (Kind.Term.eval type) body problem)) (Kind.Checker.pure (Maybe.none)))) -(Kind.Coverage.catches (Kind.Coverage.Problem.new type rows count)) = (List.all rows 位x (Kind.Coverage.Row.catches x)) -(List.all [] cond) = (Bool.true) -(List.all (List.cons head tail) cond) = (Bool.if (cond head) (List.all tail cond) (Bool.false)) -(Kind.Coverage.Row.catches (Kind.Rule.lhs (Kind.Term.var x_1 x_2 x_3) x_4)) = (Bool.true) -(Kind.Coverage.Row.catches x_5) = (Bool.false) -(Kind.Term.if_all (Kind.Term.all orig name typ body) func_if else) = (func_if orig name typ body) -(Kind.Term.if_all other func_if else) = else -(Kind.Coverage.intro_all type body (Kind.Coverage.Problem.new x_1 rows count)) = (Kind.Checker.bind (Kind.Checker.get_depth) 位depth (Kind.Checker.bind (Kind.Checker.extend 63 type []) 位x_2 let var = (Kind.Term.var 0 63 depth); let new_type = (body var); let new_rows = (List.map rows 位x (Kind.Coverage.Row.intro_all x)); (Kind.Checker.bind (Kind.Coverage.solve (Kind.Coverage.Problem.new new_type new_rows (- count 1))) 位term_result (Kind.Checker.pure (Maybe.map 位scrutinee (List.cons (Kind.Term.Quoted.var 0 63 depth) scrutinee) term_result))))) -(Kind.Coverage.Row.intro_all (Kind.Rule.lhs term rule)) = rule -(Kind.Coverage.Row.intro_all rule) = rule -(List.map [] f) = [] -(List.map (List.cons head tail) f) = (List.cons (f head) (List.map tail f)) -(Kind.Coverage.specialize type body problem) = (Kind.Coverage.Choice.match (Kind.Coverage.get_name type) 位type_name (Maybe.match (Kind.Axiom.Family.Constructors type_name) (Kind.Checker.pure (Maybe.some [(Kind.Term.Quoted.var 0 63 0)])) 位constructors (Kind.Coverage.specialize_list type_name constructors type body problem)) (Bool.if (List.any (Kind.Coverage.Problem.rows.get problem) 位x (Kind.Coverage.Row.catches x)) (Kind.Coverage.intro_all type body problem) (Kind.Coverage.solve (Kind.Coverage.Problem.rows.set problem []))) (Kind.Checker.pure (Maybe.some []))) -(List.any [] cond) = (Bool.false) -(List.any (List.cons head tail) cond) = (Bool.if (cond head) (Bool.true) (List.all tail cond)) -(Kind.Coverage.Choice.match (Kind.Coverage.Choice.on_cons name_) on_cons on_U60 none) = (on_cons name_) -(Kind.Coverage.Choice.match (Kind.Coverage.Choice.on_U60) on_cons on_U60 none) = on_U60 -(Kind.Coverage.Choice.match (Kind.Coverage.Choice.none) on_cons on_U60 none) = none -(Kind.Coverage.Problem.rows.get (Kind.Coverage.Problem.new type_ rows_ count_)) = rows_ -(Kind.Coverage.Problem.rows.set (Kind.Coverage.Problem.new type rows count) _new_var) = (Kind.Coverage.Problem.new type _new_var count) -(Kind.Coverage.get_name (Kind.Term.ct0 name x_1)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct1 name x_2 x_3)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct2 name x_4 x_5 x_6)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct3 name x_7 x_8 x_9 x_10)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct4 name x_11 x_12 x_13 x_14 x_15)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct5 name x_16 x_17 x_18 x_19 x_20 x_21)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct6 name x_22 x_23 x_24 x_25 x_26 x_27 x_28)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct8 name x_29 x_30 x_31 x_32 x_33 x_34 x_35 x_36 x_37)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct7 name x_38 x_39 x_40 x_41 x_42 x_43 x_44 x_45)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct9 name x_46 x_47 x_48 x_49 x_50 x_51 x_52 x_53 x_54 x_55)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct10 name x_56 x_57 x_58 x_59 x_60 x_61 x_62 x_63 x_64 x_65 x_66)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct11 name x_67 x_68 x_69 x_70 x_71 x_72 x_73 x_74 x_75 x_76 x_77 x_78)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct12 name x_79 x_80 x_81 x_82 x_83 x_84 x_85 x_86 x_87 x_88 x_89 x_90 x_91)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct13 name x_92 x_93 x_94 x_95 x_96 x_97 x_98 x_99 x_100 x_101 x_102 x_103 x_104 x_105)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct14 name x_106 x_107 x_108 x_109 x_110 x_111 x_112 x_113 x_114 x_115 x_116 x_117 x_118 x_119 x_120)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct15 name x_121 x_122)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct16 name x_123 x_124)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.ct16 name x_125 x_126)) = (Kind.Coverage.Choice.on_cons name) -(Kind.Coverage.get_name (Kind.Term.U60 x_127)) = (Kind.Coverage.Choice.on_U60) -(Kind.Coverage.get_name x_128) = (Kind.Coverage.Choice.none) +(Kind.Coverage.solve problem) = (Kind.Checker.local (Kind.Coverage.done problem (Kind.Coverage.if_all (Kind.Coverage.Problem.type.get problem) 位orig_ 位name_ 位type 位constraints 位body (Bool.if (Kind.Coverage.catches problem) (Kind.Coverage.intro_all type body problem) (Kind.Coverage.specialize (Kind.Term.eval type) body problem)) 位constraint (Bool.if (List.is_nil (Kind.Coverage.Problem.rows.get problem)) (Kind.Checker.pure (Maybe.some [])) (Kind.Checker.pure (Maybe.none)))))) +(Kind.Coverage.done (Kind.Coverage.Problem.new type rows) or_else) = let result = (Kind.Coverage.Type.remove_constraints type); let type_res = (Pair.fst result); let constraints = (Pair.snd result); (Kind.Checker.bind (Kind.Coverage.solve_constraints constraints) 位solved (Bool.if solved or_else (Kind.Checker.pure (Maybe.none)))) +(Kind.Coverage.solve_constraints []) = (Kind.Checker.pure (Bool.true)) +(Kind.Coverage.solve_constraints (List.cons pair xs)) = let expected_type = (Pair.snd pair); (Kind.Checker.bind (Kind.Checker.infer (Pair.fst pair)) 位infered_type (Kind.Checker.bind (Kind.Checker.equal expected_type infered_type) 位result (Bool.if result (Kind.Coverage.solve_constraints xs) (Kind.Checker.pure (Bool.false))))) +(Pair.fst (Pair.new fst snd)) = fst +(Pair.snd (Pair.new fst snd)) = snd +(Kind.Coverage.Type.remove_constraints (Kind.Coverage.Type.cons orig name typ constraints body)) = (Pair.new (Kind.Coverage.Type.cons orig name typ [] body) constraints) +(Kind.Coverage.Type.remove_constraints (Kind.Coverage.Type.end constraints body)) = (Pair.new (Kind.Coverage.Type.end [] body) constraints) +(Kind.Coverage.if_all (Kind.Coverage.Type.cons orig name typ constraints body) func_if else) = (func_if orig name typ constraints body) +(Kind.Coverage.if_all (Kind.Coverage.Type.end constraints body) func_if else) = (else constraints) +(Kind.Coverage.specialize type body (Kind.Coverage.Problem.new cur_type rows)) = let problem = (Kind.Coverage.Problem.new cur_type rows); (Maybe.default (Maybe.bind (Kind.Coverage.get_name type) 位type_name (Maybe.bind (Kind.Axiom.Family.Constructors type_name) 位constructors (Maybe.some (Kind.Coverage.specialize_list type_name constructors type body problem)))) (Kind.Coverage.intro_or_incomplete type body problem)) +(Kind.Coverage.get_name (Kind.Term.ct0 name x_1)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct1 name x_2 x_3)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct2 name x_4 x_5 x_6)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct3 name x_7 x_8 x_9 x_10)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct4 name x_11 x_12 x_13 x_14 x_15)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct5 name x_16 x_17 x_18 x_19 x_20 x_21)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct6 name x_22 x_23 x_24 x_25 x_26 x_27 x_28)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct8 name x_29 x_30 x_31 x_32 x_33 x_34 x_35 x_36 x_37)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct7 name x_38 x_39 x_40 x_41 x_42 x_43 x_44 x_45)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct9 name x_46 x_47 x_48 x_49 x_50 x_51 x_52 x_53 x_54 x_55)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct10 name x_56 x_57 x_58 x_59 x_60 x_61 x_62 x_63 x_64 x_65 x_66)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct11 name x_67 x_68 x_69 x_70 x_71 x_72 x_73 x_74 x_75 x_76 x_77 x_78)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct12 name x_79 x_80 x_81 x_82 x_83 x_84 x_85 x_86 x_87 x_88 x_89 x_90 x_91)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct13 name x_92 x_93 x_94 x_95 x_96 x_97 x_98 x_99 x_100 x_101 x_102 x_103 x_104 x_105)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct14 name x_106 x_107 x_108 x_109 x_110 x_111 x_112 x_113 x_114 x_115 x_116 x_117 x_118 x_119 x_120)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct15 name x_121 x_122)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct16 name x_123 x_124)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.ct16 name x_125 x_126)) = (Maybe.some name) +(Kind.Coverage.get_name (Kind.Term.U60 x_127)) = (Maybe.none) +(Kind.Coverage.get_name x_128) = (Maybe.none) +(Maybe.bind (Maybe.none) mb) = (Maybe.none) +(Maybe.bind (Maybe.some val) mb) = (mb val) (Kind.Coverage.specialize_list type_name [] type body problem) = (Kind.Checker.pure (Maybe.none)) (Kind.Coverage.specialize_list type_name (List.cons name rest) type body problem) = (Kind.Checker.bind (Kind.Coverage.specialize_on type_name name type body problem) 位result (Maybe.match result (Kind.Coverage.specialize_list type_name rest type body problem) 位result.value (Kind.Checker.pure (Maybe.some result.value)))) -(Kind.Coverage.specialize_on type_name constructor_name type body (Kind.Coverage.Problem.new current_problem_type rows count)) = (Maybe.match (Kind.Coverage.Maker.Mk constructor_name 0 type) (Kind.Checker.pure (Maybe.some [])) 位constructor_maker let new_type = (Kind.Coverage.Maker.make constructor_maker body); let params = (Kind.Axiom.Family.Params type_name); let args = (Kind.Axiom.ArgsCount constructor_name); (Kind.Checker.bind (Kind.Coverage.specialize_rules type_name constructor_name rows) 位new_rows let new_problem = (Kind.Coverage.Problem.new new_type new_rows (+ (- count 1) (- args params))); (Kind.Checker.bind (Kind.Coverage.solve new_problem) 位term_result (Maybe.match term_result (Kind.Checker.pure (Maybe.none)) 位scrutinee let size = (Kind.Coverage.Maker.size constructor_maker); let took = (List.take scrutinee (U60.to_nat size)); let rest = (List.drop scrutinee (U60.to_nat size)); let pat = (Kind.Term.Quoted.ctr constructor_name 0 took); (Kind.Checker.pure (Maybe.some (List.cons pat rest))))))) -(List.drop xs (Nat.zero)) = xs -(List.drop (List.cons head tail) (Nat.succ pred)) = (List.drop tail pred) -(U60.to_nat 0) = (Nat.zero) -(U60.to_nat n) = (Nat.succ (U60.to_nat (- n 1))) +(Kind.Coverage.specialize_on type_name constructor_name type body (Kind.Coverage.Problem.new current_problem_type rows)) = (Maybe.match (Kind.Coverage.Maker.Mk constructor_name 0 type) (Kind.Checker.pure (Maybe.some [])) 位constructor_maker let new_type = (Kind.Coverage.Maker.make constructor_maker type body); let params = (Kind.Axiom.Family.Params type_name); let args = (Kind.Axiom.ArgsCount constructor_name); (Kind.Checker.bind (Kind.Coverage.specialize_rules type_name constructor_name rows) 位new_rows let new_problem = (Kind.Coverage.Problem.new new_type new_rows); (Kind.Checker.bind (Kind.Coverage.solve new_problem) 位term_result (Maybe.match term_result (Kind.Checker.pure (Maybe.none)) 位scrutinee let size = (Kind.Coverage.Maker.size constructor_maker); let took = (List.take scrutinee (U60.to_nat size)); let rest = (List.drop scrutinee (U60.to_nat size)); let pat = (Kind.Term.Quoted.ctr constructor_name 0 took); (Kind.Checker.pure (Maybe.some (List.cons pat rest))))))) +(Kind.Coverage.Maker.size (Kind.Coverage.Maker.Cons x_1 x_2 body)) = (+ 1 (Kind.Coverage.Maker.size (body (Kind.Term.var 0 0 0)))) +(Kind.Coverage.Maker.size (Kind.Coverage.Maker.End x_3)) = 0 (List.take (List.cons head tail) (Nat.succ pred)) = (List.cons head (List.take tail pred)) (List.take [] (Nat.succ pred)) = [] (List.take xs (Nat.zero)) = [] +(Kind.Coverage.Maker.make (Kind.Coverage.Maker.Cons name typ body) cur_type and_then) = (Kind.Coverage.Type.cons 0 97 typ [] 位arg (Kind.Coverage.Maker.make (body arg) cur_type and_then)) +(Kind.Coverage.Maker.make (Kind.Coverage.Maker.End other) cur_type and_then) = (and_then other) +(U60.to_nat 0) = (Nat.zero) +(U60.to_nat n) = (Nat.succ (U60.to_nat (- n 1))) +(List.drop xs (Nat.zero)) = xs +(List.drop (List.cons head tail) (Nat.succ pred)) = (List.drop tail pred) +(List.drop xs x_1) = xs (Kind.Coverage.specialize_rules type_name name (List.cons rule rules)) = let splitted = (Kind.Coverage.split_rule rule); (Maybe.match splitted (Kind.Coverage.specialize_rules type_name name rules) 位value let params = (Kind.Axiom.Family.Params type_name); let row = (Kind.Coverage.specialize_rule name (Pair.fst value) (Pair.snd value)); (Kind.Checker.bind (Kind.Coverage.specialize_rules type_name name rules) 位next (Kind.Checker.pure (Maybe.match row next 位value (List.cons (Kind.Coverage.drop_rule params value) next))))) (Kind.Coverage.specialize_rules type_name name []) = (Kind.Checker.pure []) +(Kind.Coverage.drop_rule 0 rule) = rule +(Kind.Coverage.drop_rule n (Kind.Rule.lhs x_1 rule)) = (Kind.Coverage.drop_rule (- n 1) rule) +(Kind.Coverage.split_rule (Kind.Rule.lhs term rest)) = (Maybe.some (Pair.new term rest)) +(Kind.Coverage.split_rule x_1) = (Maybe.none) (Kind.Coverage.specialize_rule n (Kind.Term.ct0 name orig) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some rule) (Maybe.none)) (Kind.Coverage.specialize_rule n (Kind.Term.ct1 name orig x0) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 rule)) (Maybe.none)) (Kind.Coverage.specialize_rule n (Kind.Term.ct2 name orig x0 x1) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 rule))) (Maybe.none)) @@ -549,194 +568,61 @@ (Kind.Coverage.specialize_rule n x_1 rule) = (Maybe.none) (Kind.Coverage.craft 0 rule) = rule (Kind.Coverage.craft n rule) = (Kind.Coverage.craft (- n 1) (Kind.Rule.lhs (Kind.Term.var 0 65 0) rule)) -(Pair.fst (Pair.new fst snd)) = fst -(Kind.Coverage.drop_rule 0 rule) = rule -(Kind.Coverage.drop_rule n (Kind.Rule.lhs x_1 rule)) = (Kind.Coverage.drop_rule (- n 1) rule) -(Pair.snd (Pair.new fst snd)) = snd -(Kind.Coverage.split_rule (Kind.Rule.lhs term rest)) = (Maybe.some (Pair.new term rest)) -(Kind.Coverage.split_rule x_1) = (Maybe.none) -(Kind.Coverage.Maker.size (Kind.Coverage.Maker.Cons x_1 x_2 body)) = (+ 1 (Kind.Coverage.Maker.size (body (Kind.Term.var 0 0 0)))) -(Kind.Coverage.Maker.size (Kind.Coverage.Maker.End x_3)) = 0 -(Kind.Coverage.Maker.make (Kind.Coverage.Maker.Cons name typ body) and_then) = (Kind.Term.all 0 97 typ 位arg (Kind.Coverage.Maker.make (body arg) and_then)) -(Kind.Coverage.Maker.make (Kind.Coverage.Maker.End other) and_then) = (and_then other) -(Kind.Coverage.done (Kind.Coverage.Problem.new type rows count) or_else) = (Bool.if (Bool.or (List.is_nil rows) (U60.to_bool (== count 0))) (Bool.if (List.is_nil rows) (Kind.Checker.pure (Maybe.some (List.repeat (Kind.Coverage.count_forall type (Nat.zero)) (Kind.Term.Quoted.var 0 63 0)))) (Kind.Checker.pure (Maybe.none))) or_else) -(List.repeat (Nat.zero) val) = [] -(List.repeat (Nat.succ pred) val) = (List.cons val (List.repeat pred val)) +(Kind.Coverage.intro_or_incomplete type body (Kind.Coverage.Problem.new cur_type rows)) = let problem = (Kind.Coverage.Problem.new cur_type rows); (Bool.if (List.any (Kind.Coverage.Problem.rows.get problem) 位x (Kind.Coverage.Row.catches x)) (Kind.Coverage.intro_all type body problem) (Kind.Checker.bind (Kind.Checker.generate_var type) 位var let new_problem = (Kind.Coverage.Problem.new (body var) []); (Kind.Checker.bind (Kind.Coverage.solve (Kind.Coverage.Problem.rows.set new_problem [])) 位term_result (Kind.Checker.pure (Maybe.map 位scrutinee (List.cons (Kind.Term.Quoted.var 0 63 0) scrutinee) term_result))))) +(Kind.Coverage.Row.catches (Kind.Rule.lhs (Kind.Term.var x_1 x_2 x_3) x_4)) = (Bool.true) +(Kind.Coverage.Row.catches x_5) = (Bool.false) +(Kind.Coverage.intro_all type body (Kind.Coverage.Problem.new x_1 rows)) = (Kind.Checker.bind (Kind.Checker.generate_var type) 位var let new_type = (body var); let new_rows = (List.map rows 位x (Kind.Coverage.Row.intro_all x)); let new_problem = (Kind.Coverage.Problem.new new_type new_rows); (Kind.Checker.bind (Kind.Coverage.solve new_problem) 位term_result (Kind.Checker.pure (Maybe.map 位scrutinee (List.cons (Kind.Term.Quoted.var 0 63 0) scrutinee) term_result)))) +(List.map [] f) = [] +(List.map (List.cons head tail) f) = (List.cons (f head) (List.map tail f)) +(Maybe.map f (Maybe.none)) = (Maybe.none) +(Maybe.map f (Maybe.some v)) = (Maybe.some (f v)) +(Kind.Checker.generate_var type) = (Kind.Checker.bind (Kind.Checker.get_depth) 位depth (Kind.Checker.bind (Kind.Checker.extend 63 type []) 位x_1 (Kind.Checker.pure (Kind.Term.var 0 63 depth)))) +(Kind.Coverage.Row.intro_all (Kind.Rule.lhs term rule)) = rule +(Kind.Coverage.Row.intro_all rule) = rule +(Kind.Coverage.Problem.rows.set (Kind.Coverage.Problem.new type rows) _new_var) = (Kind.Coverage.Problem.new type _new_var) +(Kind.Coverage.Problem.rows.get (Kind.Coverage.Problem.new type_ rows_)) = rows_ +(List.any [] cond) = (Bool.false) +(List.any (List.cons head tail) cond) = (Bool.if (cond head) (Bool.true) (List.any tail cond)) (List.is_nil []) = (Bool.true) (List.is_nil (List.cons head tail)) = (Bool.false) -(Kind.Coverage.count_forall (Kind.Term.all x_1 x_2 x_3 body) acc) = (Kind.Coverage.count_forall (body (Kind.Term.var 0 63 0)) (Nat.succ acc)) -(Kind.Coverage.count_forall x_4 acc) = acc -(Kind.Coverage.Problem.type.get (Kind.Coverage.Problem.new type_ rows_ count_)) = type_ +(Kind.Coverage.Problem.type.get (Kind.Coverage.Problem.new type_ rows_)) = type_ +(Kind.Checker.local checker) = 位old_context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.match (checker old_context depth rhs subst eqts errs) 位res.ctx 位res.depth 位res.rhs 位res.sub 位res.equations 位res.errors 位res.ret (Kind.Result.checked old_context depth rhs subst eqts errs res.ret) 位res.ctx 位res.sub 位res.errors (Kind.Result.errored res.ctx res.sub res.errors)) +(Kind.Result.match (Kind.Result.checked ctx_ depth_ rhs_ sub_ equations_ errors_ ret_) checked errored) = (checked ctx_ depth_ rhs_ sub_ equations_ errors_ ret_) +(Kind.Result.match (Kind.Result.errored ctx_ sub_ errors_) checked errored) = (errored ctx_ sub_ errors_) +(Kind.Coverage.catches (Kind.Coverage.Problem.new type rows)) = (List.all rows 位x (Kind.Coverage.Row.catches x)) +(List.all [] cond) = (Bool.true) +(List.all (List.cons head tail) cond) = (Bool.if (cond head) (List.all tail cond) (Bool.false)) +(Kind.Coverage.Type.from_term term 0) = (Kind.Coverage.Type.end [] term) +(Kind.Coverage.Type.from_term (Kind.Term.all orig name typ body) n) = (Kind.Coverage.Type.cons orig name typ [] 位arg (Kind.Coverage.Type.from_term (body arg) (- n 1))) +(Kind.Coverage.Type.from_term term n) = (Kind.Coverage.Type.end [] term) +(Kind.Coverage.Rule.size (Kind.Rule.lhs x xs)) = (+ 1 (Kind.Coverage.Rule.size xs)) +(Kind.Coverage.Rule.size x_1) = 0 +(Kind.Checker.set_right_hand_side to_rhs) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth to_rhs subst eqts errs (Unit.new)) +(List.head []) = (Maybe.none) +(List.head (List.cons head tail)) = (Maybe.some head) +(Kind.Checker.unify checker) = (Kind.Checker.bind checker 位x_1 (Kind.Checker.bind (Kind.Checker.get_equations) 位equations (Kind.Checker.unify.go equations [] (Bool.false)))) +(Kind.Checker.get_equations) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst eqts errs eqts) +(Kind.Checker.unify.go [] [] changed) = (Kind.Checker.pure (Unit.new)) +(Kind.Checker.unify.go [] unsolved (Bool.true)) = (Kind.Checker.unify.go unsolved [] (Bool.false)) +(Kind.Checker.unify.go [] unsolved (Bool.false)) = (Kind.Checker.unify.go.fail unsolved) +(Kind.Checker.unify.go (List.cons (Kind.Equation.new ctx orig left right) equations) unsolved changed) = (Kind.Checker.bind (Kind.Checker.with_context (Kind.Checker.equal (Kind.Term.eval left) (Kind.Term.eval right)) ctx) 位is_equal let unify = (Bool.if is_equal 位equations 位unsolved (Kind.Checker.unify.go equations unsolved (Bool.true)) 位equations 位unsolved let eqt = (Kind.Equation.new ctx orig left right); (Kind.Checker.unify.go equations (List.cons eqt unsolved) changed)); (unify equations unsolved)) +(Kind.Checker.unify.go.fail []) = (Kind.Checker.pure (Unit.new)) +(Kind.Checker.unify.go.fail (List.cons (Kind.Equation.new ctx orig left right) eqts)) = (Kind.Checker.bind (Kind.Checker.error (Kind.Error.type_mismatch ctx orig left right) (Unit.new)) 位x_1 (Kind.Checker.unify.go.fail eqts)) +(Kind.Checker.with_context checker new_context) = (Kind.Checker.bind (Kind.Checker.set_context new_context) 位old_context (Kind.Checker.bind checker 位got (Kind.Checker.bind (Kind.Checker.set_context old_context) 位x_1 (Kind.Checker.pure got)))) +(Kind.Checker.set_context new_context) = 位old_context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked new_context depth rhs subst eqts errs old_context) (Kind.Checker.run checker rhs) = (checker (Kind.Context.empty) 0 rhs (Kind.Subst.end) [] []) (Kind.API.check_function.rules [] type) = [] (Kind.API.check_function.rules (List.cons rule rules) type) = let head = (Kind.Checker.run (Kind.Checker.unify (Kind.Checker.rule rule type)) (Bool.false)); let tail = (Kind.API.check_function.rules rules type); (List.cons head tail) (Kind.Checker.rule (Kind.Rule.lhs arg args) (Kind.Term.all orig name type body)) = (Kind.Checker.bind (Kind.Checker.check arg type) 位x_2 (Kind.Checker.bind (Kind.Checker.rule args (body arg)) 位x_1 (Kind.Checker.pure (Unit.new)))) (Kind.Checker.rule (Kind.Rule.lhs arg args) other) = (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.too_many_arguments ctx (Kind.Term.get_origin arg 位orig 位term orig)))) (Kind.Checker.rule (Kind.Rule.rhs expr) type) = (Kind.Checker.bind (Kind.Checker.set_right_hand_side (Bool.true)) 位x_4 (Kind.Checker.bind (Kind.Checker.check expr type) 位x_3 (Kind.Checker.pure (Unit.new)))) -(Kind.Checker.set_right_hand_side to_rhs) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth to_rhs subst eqts errs (Unit.new)) -(Kind.Checker.check (Kind.Term.lam orig name body) type) = (Kind.Checker.bind (Kind.Checker.get_subst) 位subst let fun = (Kind.Term.if_all type 位t_orig 位t_name 位t_type 位t_body 位orig 位name 位body (Kind.Checker.bind (Kind.Checker.get_depth) 位dep (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name dep)) (t_body (Kind.Term.var t_orig t_name dep))) name t_type []) 位chk (Kind.Checker.pure (Unit.new)))) 位orig 位name 位body (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.cant_infer_lambda ctx orig)))); (fun orig name body)) -(Kind.Checker.check (Kind.Term.let orig name expr body) type) = (Kind.Checker.bind (Kind.Checker.get_depth) 位dep (Kind.Checker.bind (Kind.Checker.infer expr) 位expr_typ (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name dep)) type) name expr_typ [(Kind.Term.eval expr)]) 位body_chk (Kind.Checker.pure (Unit.new))))) -(Kind.Checker.check (Kind.Term.hlp orig) type) = (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.bind (Kind.Checker.error (Kind.Error.inspection ctx orig type) (Unit.new)) 位x_13 (Kind.Checker.pure (Unit.new)))) -(Kind.Checker.check (Kind.Term.var orig name idx) type) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) 位rhs (Bool.if rhs (Kind.Checker.compare rhs (Kind.Term.var orig name idx) type) (Kind.Checker.extend name type []))) -(Kind.Checker.check (Kind.Term.hol orig numb) type) = (Kind.Checker.pure (Unit.new)) -(Kind.Checker.check term type) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) 位rhs (Kind.Checker.compare rhs term type)) -(Kind.Checker.infer (Kind.Term.var orig name index)) = (Kind.Checker.bind (Kind.Checker.find index (Maybe.none) 位n 位t 位v (Maybe.some t)) 位got_type (Maybe.match got_type (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) 位got_type.value (Kind.Checker.pure got_type.value))) -(Kind.Checker.infer (Kind.Term.hol orig numb)) = (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.cant_infer_hole ctx orig))) -(Kind.Checker.infer (Kind.Term.typ orig)) = (Kind.Checker.pure (Kind.Term.typ orig)) -(Kind.Checker.infer (Kind.Term.all orig name type body)) = (Kind.Checker.bind (Kind.Checker.get_depth) 位depth (Kind.Checker.bind (Kind.Checker.check type (Kind.Term.typ orig)) 位x_2 (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name depth)) (Kind.Term.typ orig)) name (Kind.Term.eval type) []) 位x_1 (Kind.Checker.pure (Kind.Term.typ orig))))) -(Kind.Checker.infer (Kind.Term.lam orig name body)) = (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.cant_infer_lambda ctx orig))) -(Kind.Checker.infer (Kind.Term.app orig func argm)) = (Kind.Checker.bind (Kind.Checker.infer func) 位fn_infer (Kind.Checker.bind (Kind.Checker.infer.forall fn_infer 位fn_orig 位fn_name 位fn_type 位fn_body (Kind.Checker.bind (Kind.Checker.check argm fn_type) 位x_3 (Kind.Checker.pure (fn_body (Kind.Term.eval argm)))) (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.invalid_call ctx orig)))) 位ap_infer (Kind.Checker.pure ap_infer))) -(Kind.Checker.infer (Kind.Term.let orig name expr body)) = (Kind.Checker.bind (Kind.Checker.get_depth) 位dep (Kind.Checker.bind (Kind.Checker.infer expr) 位expr_typ (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.infer (body (Kind.Term.var orig name dep))) name expr_typ [(Kind.Term.eval expr)]) 位body_typ (Kind.Checker.pure body_typ)))) -(Kind.Checker.infer (Kind.Term.ann orig expr type)) = let type = (Kind.Term.eval type); (Kind.Checker.bind (Kind.Checker.check expr type) 位x_4 (Kind.Checker.pure type)) -(Kind.Checker.infer (Kind.Term.sub orig name indx redx expr)) = (Kind.Checker.bind (Kind.Checker.get_depth) 位dep (Kind.Checker.bind (Kind.Checker.find indx (Maybe.none) 位n 位t 位v (Maybe.some (Pair.new t v))) 位got (Maybe.match got (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) 位got.value (Pair.new.match got.value 位got.value.fst 位got.value.snd (Maybe.match (List.at.u60 got.value.snd redx) (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) 位reduction.value (Kind.Checker.bind (Kind.Checker.infer expr) 位expr_typ (Kind.Checker.pure (Kind.Term.eval (Kind.Term.replace expr_typ indx reduction.value))))))))) -(Kind.Checker.infer (Kind.Term.ct0 ctid orig)) = (Kind.Checker.pure (Kind.Term.eval (Kind.Axiom.TypeOf ctid))) -(Kind.Checker.infer (Kind.Term.ct1 ctid orig x0)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0)) -(Kind.Checker.infer (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1)) -(Kind.Checker.infer (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2)) -(Kind.Checker.infer (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3)) -(Kind.Checker.infer (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4)) -(Kind.Checker.infer (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5)) -(Kind.Checker.infer (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6)) -(Kind.Checker.infer (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7)) -(Kind.Checker.infer (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8)) -(Kind.Checker.infer (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9)) -(Kind.Checker.infer (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10)) -(Kind.Checker.infer (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11)) -(Kind.Checker.infer (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12)) -(Kind.Checker.infer (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13)) -(Kind.Checker.infer (Kind.Term.ct15 ctid orig x0)) = let expr = (Kind.Checker.infer_args x0); (Kind.Checker.infer (expr (Kind.Term.ct0 ctid orig) orig)) -(Kind.Checker.infer (Kind.Term.ct16 ctid orig x0)) = let expr = (Kind.Checker.infer_args x0); (Kind.Checker.infer (expr (Kind.Term.ct0 ctid orig) orig)) -(Kind.Checker.infer (Kind.Term.fn0 fnid orig)) = (Kind.Checker.pure (Kind.Term.eval (Kind.Axiom.TypeOf fnid))) -(Kind.Checker.infer (Kind.Term.fn1 fnid orig x0)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0)) -(Kind.Checker.infer (Kind.Term.fn2 fnid orig x0 x1)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1)) -(Kind.Checker.infer (Kind.Term.fn3 fnid orig x0 x1 x2)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2)) -(Kind.Checker.infer (Kind.Term.fn4 fnid orig x0 x1 x2 x3)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3)) -(Kind.Checker.infer (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4)) -(Kind.Checker.infer (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5)) -(Kind.Checker.infer (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6)) -(Kind.Checker.infer (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6) x7)) -(Kind.Checker.infer (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8)) -(Kind.Checker.infer (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9)) -(Kind.Checker.infer (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10)) -(Kind.Checker.infer (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11)) -(Kind.Checker.infer (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12)) -(Kind.Checker.infer (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13)) -(Kind.Checker.infer (Kind.Term.fn15 fnid orig x0)) = let expr = (Kind.Checker.infer_args x0); (Kind.Checker.infer (expr (Kind.Term.fn0 fnid orig) orig)) -(Kind.Checker.infer (Kind.Term.fn16 fnid orig x0)) = let expr = (Kind.Checker.infer_args x0); (Kind.Checker.infer (expr (Kind.Term.fn0 fnid orig) orig)) -(Kind.Checker.infer (Kind.Term.hlp orig)) = (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.inspection ctx orig (Kind.Term.hlp 0)))) -(Kind.Checker.infer (Kind.Term.U60 orig)) = (Kind.Checker.pure (Kind.Term.typ 0)) -(Kind.Checker.infer (Kind.Term.u60 orig numb)) = (Kind.Checker.pure (Kind.Term.U60 0)) -(Kind.Checker.infer (Kind.Term.op2 orig oper left right)) = (Kind.Checker.bind (Kind.Checker.check left (Kind.Term.U60 0)) 位x_6 (Kind.Checker.bind (Kind.Checker.check right (Kind.Term.U60 0)) 位x_5 (Kind.Checker.pure (Kind.Term.U60 0)))) -(Kind.Term.replace (Kind.Term.typ orig) idx val) = (Kind.Term.typ orig) -(Kind.Term.replace (Kind.Term.var orig name index) idx val) = (Bool.if (U60.equal idx index) val (Kind.Term.var orig name index)) -(Kind.Term.replace (Kind.Term.all orig name typ body) idx val) = (Kind.Term.all orig name (Kind.Term.replace typ idx val) 位x (Kind.Term.replace (body x) idx val)) -(Kind.Term.replace (Kind.Term.lam orig name body) idx val) = (Kind.Term.lam orig name 位x (Kind.Term.replace (body x) idx val)) -(Kind.Term.replace (Kind.Term.let orig name expr body) idx val) = (Kind.Term.let orig name (Kind.Term.replace expr idx val) 位x (Kind.Term.replace (body x) idx val)) -(Kind.Term.replace (Kind.Term.ann orig expr typ) idx val) = (Kind.Term.ann orig (Kind.Term.replace expr idx val) (Kind.Term.replace typ idx val)) -(Kind.Term.replace (Kind.Term.sub orig name indx redx expr) idx val) = (Kind.Term.sub orig name indx redx (Kind.Term.replace expr idx val)) -(Kind.Term.replace (Kind.Term.app orig expr typ) idx val) = (Kind.Term.app orig (Kind.Term.replace expr idx val) (Kind.Term.replace typ idx val)) -(Kind.Term.replace (Kind.Term.hlp orig) idx val) = (Kind.Term.hlp orig) -(Kind.Term.replace (Kind.Term.U60 orig) idx val) = (Kind.Term.U60 orig) -(Kind.Term.replace (Kind.Term.u60 orig num) idx val) = (Kind.Term.u60 orig num) -(Kind.Term.replace (Kind.Term.op2 orig op left right) idx val) = (Kind.Term.op2 orig op (Kind.Term.replace left idx val) (Kind.Term.replace right idx val)) -(Kind.Term.replace (Kind.Term.ct0 ctid orig) idx val) = (Kind.Term.ct0 ctid orig) -(Kind.Term.replace (Kind.Term.ct1 ctid orig x0) idx val) = (Kind.Term.ct1 ctid orig (Kind.Term.replace x0 idx val)) -(Kind.Term.replace (Kind.Term.ct2 ctid orig x0 x1) idx val) = (Kind.Term.ct2 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val)) -(Kind.Term.replace (Kind.Term.ct3 ctid orig x0 x1 x2) idx val) = (Kind.Term.ct3 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val)) -(Kind.Term.replace (Kind.Term.ct4 ctid orig x0 x1 x2 x3) idx val) = (Kind.Term.ct4 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val)) -(Kind.Term.replace (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4) idx val) = (Kind.Term.ct5 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val)) -(Kind.Term.replace (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5) idx val) = (Kind.Term.ct6 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val)) -(Kind.Term.replace (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6) idx val) = (Kind.Term.ct7 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val)) -(Kind.Term.replace (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7) idx val) = (Kind.Term.ct8 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val)) -(Kind.Term.replace (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8) idx val) = (Kind.Term.ct9 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val)) -(Kind.Term.replace (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) idx val) = (Kind.Term.ct10 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val)) -(Kind.Term.replace (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) idx val) = (Kind.Term.ct11 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val)) -(Kind.Term.replace (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) idx val) = (Kind.Term.ct12 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val)) -(Kind.Term.replace (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) idx val) = (Kind.Term.ct13 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val)) -(Kind.Term.replace (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) idx val) = (Kind.Term.ct14 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val) (Kind.Term.replace x13 idx val)) -(Kind.Term.replace (Kind.Term.fn0 fnid orig) idx val) = (Kind.Term.FN0 fnid orig) -(Kind.Term.replace (Kind.Term.fn1 fnid orig x0) idx val) = (Kind.Term.FN1 fnid orig (Kind.Term.replace x0 idx val)) -(Kind.Term.replace (Kind.Term.fn2 fnid orig x0 x1) idx val) = (Kind.Term.FN2 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val)) -(Kind.Term.replace (Kind.Term.fn3 fnid orig x0 x1 x2) idx val) = (Kind.Term.FN3 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val)) -(Kind.Term.replace (Kind.Term.fn4 fnid orig x0 x1 x2 x3) idx val) = (Kind.Term.FN4 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val)) -(Kind.Term.replace (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4) idx val) = (Kind.Term.FN5 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val)) -(Kind.Term.replace (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5) idx val) = (Kind.Term.FN6 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val)) -(Kind.Term.replace (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6) idx val) = (Kind.Term.FN7 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val)) -(Kind.Term.replace (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7) idx val) = (Kind.Term.FN8 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val)) -(Kind.Term.replace (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8) idx val) = (Kind.Term.FN9 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val)) -(Kind.Term.replace (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) idx val) = (Kind.Term.FN10 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val)) -(Kind.Term.replace (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) idx val) = (Kind.Term.FN11 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val)) -(Kind.Term.replace (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) idx val) = (Kind.Term.FN12 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val)) -(Kind.Term.replace (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) idx val) = (Kind.Term.FN13 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val)) -(Kind.Term.replace (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) idx val) = (Kind.Term.FN14 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val) (Kind.Term.replace x13 idx val)) -(Kind.Term.replace (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) idx val) = (Kind.Term.args15 (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val) (Kind.Term.replace x13 idx val) (Kind.Term.replace x14 idx val)) -(Kind.Term.replace (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) idx val) = (Kind.Term.args16 (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val) (Kind.Term.replace x13 idx val) (Kind.Term.replace x14 idx val) (Kind.Term.replace x15 idx val)) -(Kind.Term.replace (Kind.Term.hol orig numb) idx val) = (Kind.Term.hol orig numb) -(Kind.Checker.infer.forall (Kind.Term.all orig name type body) then_fn else_val) = (then_fn orig name type body) -(Kind.Checker.infer.forall (Kind.Term.var orig name index) then_fn else_val) = (Kind.Checker.bind (Kind.Checker.find index [] 位n 位t 位v v) 位reducs (Kind.Checker.bind (Kind.Checker.infer.forall.try_values reducs then_fn else_val) 位result (Kind.Checker.pure result))) -(Kind.Checker.infer.forall other then_fn else_val) = else_val -(Kind.Checker.infer.forall.try_values (List.cons (Kind.Term.all orig name type body) terms) then_fn else_val) = (then_fn orig name type body) -(Kind.Checker.infer.forall.try_values (List.cons other terms) then_fn else_val) = (Kind.Checker.infer.forall.try_values terms then_fn else_val) -(Kind.Checker.infer.forall.try_values [] then_fn else_val) = else_val -(Pair.new.match (Pair.new fst_ snd_) new) = (new fst_ snd_) -(List.at.u60 [] idx) = (Maybe.none) -(List.at.u60 (List.cons head tail) 0) = (Maybe.some head) -(List.at.u60 (List.cons head tail) idx) = (List.at.u60 tail (- idx 1)) -(Kind.Checker.infer_args (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = 位term 位orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig term x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13) x14) -(Kind.Checker.infer_args (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = 位term 位orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig term x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13) x14) x15) -(Kind.Checker.compare rhs term type) = (Kind.Term.get_origin term 位orig 位term (Kind.Checker.bind (Kind.Checker.infer term) 位term_typ let fun = (Bool.if rhs 位term_typ 位type (Kind.Checker.new_equation orig type term_typ) 位term_typ 位type (Kind.Checker.bind (Kind.Checker.equal (Kind.Term.eval term_typ) (Kind.Term.eval type)) 位is_equal (Bool.if is_equal (Kind.Checker.pure (Unit.new)) (Kind.Checker.bind (Kind.Checker.get_context) 位ctx (Kind.Checker.fail (Kind.Error.impossible_case ctx orig type term_typ)))))); (fun term_typ type))) -(Kind.Checker.new_equation orig left right) = 位context 位depth 位rhs 位subst 位eqts 位errs (Kind.Result.checked context depth rhs subst (List.append eqts (Kind.Equation.new context orig left right)) errs (Unit.new)) -(List.append [] x) = [x] -(List.append (List.cons xs.h xs.t) x) = (List.cons xs.h (List.append xs.t x)) -(Kind.Term.get_origin (Kind.Term.typ orig) got) = (got orig (Kind.Term.typ orig)) -(Kind.Term.get_origin (Kind.Term.var orig name index) got) = (got orig (Kind.Term.var orig name index)) -(Kind.Term.get_origin (Kind.Term.hol orig numb) got) = (got orig (Kind.Term.hol orig numb)) -(Kind.Term.get_origin (Kind.Term.all orig name typ body) got) = (got orig (Kind.Term.all orig name typ body)) -(Kind.Term.get_origin (Kind.Term.lam orig name body) got) = (got orig (Kind.Term.lam orig name body)) -(Kind.Term.get_origin (Kind.Term.let orig name expr body) got) = (got orig (Kind.Term.let orig name expr body)) -(Kind.Term.get_origin (Kind.Term.ann orig expr typ) got) = (got orig (Kind.Term.ann orig expr typ)) -(Kind.Term.get_origin (Kind.Term.sub orig name indx redx expr) got) = (got orig (Kind.Term.sub orig name indx redx expr)) -(Kind.Term.get_origin (Kind.Term.app orig func arg) got) = (got orig (Kind.Term.app orig func arg)) -(Kind.Term.get_origin (Kind.Term.hlp orig) got) = (got orig (Kind.Term.hlp orig)) -(Kind.Term.get_origin (Kind.Term.U60 orig) got) = (got orig (Kind.Term.U60 orig)) -(Kind.Term.get_origin (Kind.Term.u60 orig num) got) = (got orig (Kind.Term.u60 orig num)) -(Kind.Term.get_origin (Kind.Term.op2 orig op left right) got) = (got orig (Kind.Term.op2 orig op left right)) -(Kind.Term.get_origin (Kind.Term.ct0 ctid orig) got) = (got orig (Kind.Term.ct0 ctid orig)) -(Kind.Term.get_origin (Kind.Term.ct1 ctid orig x0) got) = (got orig (Kind.Term.ct1 ctid orig x0)) -(Kind.Term.get_origin (Kind.Term.ct2 ctid orig x0 x1) got) = (got orig (Kind.Term.ct2 ctid orig x0 x1)) -(Kind.Term.get_origin (Kind.Term.ct3 ctid orig x0 x1 x2) got) = (got orig (Kind.Term.ct3 ctid orig x0 x1 x2)) -(Kind.Term.get_origin (Kind.Term.ct4 ctid orig x0 x1 x2 x3) got) = (got orig (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) -(Kind.Term.get_origin (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4) got) = (got orig (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) -(Kind.Term.get_origin (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5) got) = (got orig (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) -(Kind.Term.get_origin (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6) got) = (got orig (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6)) -(Kind.Term.get_origin (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7) got) = (got orig (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) -(Kind.Term.get_origin (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8) got) = (got orig (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) -(Kind.Term.get_origin (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) got) = (got orig (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) -(Kind.Term.get_origin (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) got) = (got orig (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) -(Kind.Term.get_origin (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) got) = (got orig (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) -(Kind.Term.get_origin (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) got) = (got orig (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) -(Kind.Term.get_origin (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) got) = (got orig (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) -(Kind.Term.get_origin (Kind.Term.ct15 fnid orig args) got) = (got orig (Kind.Term.ct15 fnid orig args)) -(Kind.Term.get_origin (Kind.Term.ct16 fnid orig args) got) = (got orig (Kind.Term.ct16 fnid orig args)) -(Kind.Term.get_origin (Kind.Term.fn0 fnid orig) got) = (got orig (Kind.Term.fn0 fnid orig)) -(Kind.Term.get_origin (Kind.Term.fn1 fnid orig x0) got) = (got orig (Kind.Term.fn1 fnid orig x0)) -(Kind.Term.get_origin (Kind.Term.fn2 fnid orig x0 x1) got) = (got orig (Kind.Term.fn2 fnid orig x0 x1)) -(Kind.Term.get_origin (Kind.Term.fn3 fnid orig x0 x1 x2) got) = (got orig (Kind.Term.fn3 fnid orig x0 x1 x2)) -(Kind.Term.get_origin (Kind.Term.fn4 fnid orig x0 x1 x2 x3) got) = (got orig (Kind.Term.fn4 fnid orig x0 x1 x2 x3)) -(Kind.Term.get_origin (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4) got) = (got orig (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4)) -(Kind.Term.get_origin (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5) got) = (got orig (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5)) -(Kind.Term.get_origin (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6) got) = (got orig (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6)) -(Kind.Term.get_origin (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7) got) = (got orig (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7)) -(Kind.Term.get_origin (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8) got) = (got orig (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) -(Kind.Term.get_origin (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) got) = (got orig (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) -(Kind.Term.get_origin (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) got) = (got orig (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) -(Kind.Term.get_origin (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) got) = (got orig (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) -(Kind.Term.get_origin (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) got) = (got orig (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) -(Kind.Term.get_origin (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) got) = (got orig (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) -(Kind.Term.get_origin (Kind.Term.fn15 fnid orig args) got) = (got orig (Kind.Term.fn15 fnid orig args)) -(Kind.Term.get_origin (Kind.Term.fn16 fnid orig args) got) = (got orig (Kind.Term.fn16 fnid orig args)) +(List.reverse xs) = (List.reverse.go xs []) +(List.reverse.go [] ys) = ys +(List.reverse.go (List.cons x xs) ys) = (List.reverse.go xs (List.cons x ys)) (Kind.API.output []) = [] -(Kind.API.output (List.cons pair rest)) = (Pair.new.match pair 位fst 位snd (List.concat (Kind.API.output.function fst snd) (Kind.API.output rest))) +(Kind.API.output (List.cons pair rest)) = (Pair.match pair 位fst 位snd (List.concat (Kind.API.output.function fst snd) (Kind.API.output rest))) +(List.concat [] ys) = ys +(List.concat (List.cons head tail) ys) = (List.cons head (List.concat tail ys)) (Kind.API.output.function fnid []) = [] (Kind.API.output.function fnid (List.cons (Kind.Result.checked ctx dep rhs sub eqt err val) checks)) = (Kind.API.output.function.show_errors err sub fnid checks) (Kind.API.output.function fnid (List.cons (Kind.Result.errored ctx sub err) checks)) = (Kind.API.output.function.show_errors err sub fnid checks) @@ -801,8 +687,164 @@ (Kind.Term.quote.go (Kind.Term.hlp orig)) = (Kind.Term.Quoted.hlp orig) (Kind.Term.quote.go (Kind.Term.U60 orig)) = (Kind.Term.Quoted.u60 orig) (Kind.Term.quote.go (Kind.Term.u60 orig numb)) = (Kind.Term.Quoted.num orig numb) +(Kind.Term.quote.go (Kind.Term.F60 orig)) = (Kind.Term.Quoted.f60 orig) +(Kind.Term.quote.go (Kind.Term.f60 orig numb)) = (Kind.Term.Quoted.numf60 orig numb) (Kind.Term.quote.go (Kind.Term.op2 orig operator left right)) = (Kind.Term.Quoted.op2 orig operator (Kind.Term.quote.go left) (Kind.Term.quote.go right)) +(Kind.Term.quote.go (Kind.Term.args15 x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9 x_10 x_11 x_12 x_13 x_14 x_15)) = (Kind.Axiom.Null) +(Kind.Term.quote.go (Kind.Term.args16 x_16 x_17 x_18 x_19 x_20 x_21 x_22 x_23 x_24 x_25 x_26 x_27 x_28 x_29 x_30 x_31)) = (Kind.Axiom.Null) (Kind.Term.quote.args (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = [(Kind.Term.quote.go x0), (Kind.Term.quote.go x1), (Kind.Term.quote.go x2), (Kind.Term.quote.go x3), (Kind.Term.quote.go x4), (Kind.Term.quote.go x5), (Kind.Term.quote.go x6), (Kind.Term.quote.go x7), (Kind.Term.quote.go x8), (Kind.Term.quote.go x9), (Kind.Term.quote.go x10), (Kind.Term.quote.go x11), (Kind.Term.quote.go x12), (Kind.Term.quote.go x13), (Kind.Term.quote.go x14)] (Kind.Term.quote.args (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = [(Kind.Term.quote.go x0), (Kind.Term.quote.go x1), (Kind.Term.quote.go x2), (Kind.Term.quote.go x3), (Kind.Term.quote.go x4), (Kind.Term.quote.go x5), (Kind.Term.quote.go x6), (Kind.Term.quote.go x7), (Kind.Term.quote.go x8), (Kind.Term.quote.go x9), (Kind.Term.quote.go x10), (Kind.Term.quote.go x11), (Kind.Term.quote.go x12), (Kind.Term.quote.go x13), (Kind.Term.quote.go x14), (Kind.Term.quote.go x15)] -(List.concat [] ys) = ys -(List.concat (List.cons head tail) ys) = (List.cons head (List.concat tail ys)) +(Kind.Term.quote.args x_1) = (Kind.Axiom.Null) +(Kind.Term.set_origin new_origin (Kind.Term.typ old_orig)) = (Kind.Term.typ new_origin) +(Kind.Term.set_origin new_origin (Kind.Term.var old_orig name idx)) = (Kind.Term.var new_origin name idx) +(Kind.Term.set_origin new_origin (Kind.Term.hol old_orig numb)) = (Kind.Term.hol new_origin numb) +(Kind.Term.set_origin new_origin (Kind.Term.all old_orig name typ body)) = (Kind.Term.all new_origin name typ body) +(Kind.Term.set_origin new_origin (Kind.Term.lam old_orig name body)) = (Kind.Term.lam new_origin name body) +(Kind.Term.set_origin new_origin (Kind.Term.let old_orig name expr body)) = (Kind.Term.let new_origin name expr body) +(Kind.Term.set_origin new_origin (Kind.Term.ann old_orig expr typ)) = (Kind.Term.ann new_origin expr typ) +(Kind.Term.set_origin new_origin (Kind.Term.sub old_orig name indx redx expr)) = (Kind.Term.sub new_origin name indx redx expr) +(Kind.Term.set_origin new_origin (Kind.Term.app old_orig func arg)) = (Kind.Term.app new_origin func arg) +(Kind.Term.set_origin new_origin (Kind.Term.hlp old_orig)) = (Kind.Term.hlp new_origin) +(Kind.Term.set_origin new_origin (Kind.Term.U60 old_orig)) = (Kind.Term.U60 new_origin) +(Kind.Term.set_origin new_origin (Kind.Term.u60 old_orig num)) = (Kind.Term.u60 new_origin num) +(Kind.Term.set_origin new_origin (Kind.Term.F60 old_orig)) = (Kind.Term.F60 new_origin) +(Kind.Term.set_origin new_origin (Kind.Term.f60 old_orig num)) = (Kind.Term.f60 new_origin num) +(Kind.Term.set_origin new_origin (Kind.Term.op2 old_orig op left right)) = (Kind.Term.op2 new_origin op left right) +(Kind.Term.set_origin new_origin (Kind.Term.ct0 ctid old_orig)) = (Kind.Term.ct0 ctid new_origin) +(Kind.Term.set_origin new_origin (Kind.Term.ct1 ctid old_orig x0)) = (Kind.Term.ct1 ctid new_origin x0) +(Kind.Term.set_origin new_origin (Kind.Term.ct2 ctid old_orig x0 x1)) = (Kind.Term.ct2 ctid new_origin x0 x1) +(Kind.Term.set_origin new_origin (Kind.Term.ct3 ctid old_orig x0 x1 x2)) = (Kind.Term.ct3 ctid new_origin x0 x1 x2) +(Kind.Term.set_origin new_origin (Kind.Term.ct4 ctid old_orig x0 x1 x2 x3)) = (Kind.Term.ct4 ctid new_origin x0 x1 x2 x3) +(Kind.Term.set_origin new_origin (Kind.Term.ct5 ctid old_orig x0 x1 x2 x3 x4)) = (Kind.Term.ct5 ctid new_origin x0 x1 x2 x3 x4) +(Kind.Term.set_origin new_origin (Kind.Term.ct6 ctid old_orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.ct6 ctid new_origin x0 x1 x2 x3 x4 x5) +(Kind.Term.set_origin new_origin (Kind.Term.ct7 ctid old_orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.ct7 ctid new_origin x0 x1 x2 x3 x4 x5 x6) +(Kind.Term.set_origin new_origin (Kind.Term.ct8 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.ct8 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7) +(Kind.Term.set_origin new_origin (Kind.Term.ct9 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.ct9 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8) +(Kind.Term.set_origin new_origin (Kind.Term.ct10 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.ct10 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) +(Kind.Term.set_origin new_origin (Kind.Term.ct11 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.ct11 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) +(Kind.Term.set_origin new_origin (Kind.Term.ct12 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.ct12 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) +(Kind.Term.set_origin new_origin (Kind.Term.ct13 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.ct13 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) +(Kind.Term.set_origin new_origin (Kind.Term.ct14 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.ct14 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) +(Kind.Term.set_origin new_origin (Kind.Term.ct15 ctid old_orig args)) = (Kind.Term.ct15 ctid new_origin args) +(Kind.Term.set_origin new_origin (Kind.Term.ct16 ctid old_orig args)) = (Kind.Term.ct16 ctid new_origin args) +(Kind.Term.set_origin new_origin (Kind.Term.fn0 fnid old_orig)) = (Kind.Term.fn0 fnid new_origin) +(Kind.Term.set_origin new_origin (Kind.Term.fn1 fnid old_orig x0)) = (Kind.Term.fn1 fnid new_origin x0) +(Kind.Term.set_origin new_origin (Kind.Term.fn2 fnid old_orig x0 x1)) = (Kind.Term.fn2 fnid new_origin x0 x1) +(Kind.Term.set_origin new_origin (Kind.Term.fn3 fnid old_orig x0 x1 x2)) = (Kind.Term.fn3 fnid new_origin x0 x1 x2) +(Kind.Term.set_origin new_origin (Kind.Term.fn4 fnid old_orig x0 x1 x2 x3)) = (Kind.Term.fn4 fnid new_origin x0 x1 x2 x3) +(Kind.Term.set_origin new_origin (Kind.Term.fn5 fnid old_orig x0 x1 x2 x3 x4)) = (Kind.Term.fn5 fnid new_origin x0 x1 x2 x3 x4) +(Kind.Term.set_origin new_origin (Kind.Term.fn6 fnid old_orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.fn6 fnid new_origin x0 x1 x2 x3 x4 x5) +(Kind.Term.set_origin new_origin (Kind.Term.fn7 fnid old_orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.fn7 fnid new_origin x0 x1 x2 x3 x4 x5 x6) +(Kind.Term.set_origin new_origin (Kind.Term.fn8 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.fn8 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7) +(Kind.Term.set_origin new_origin (Kind.Term.fn9 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.fn9 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8) +(Kind.Term.set_origin new_origin (Kind.Term.fn10 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.fn10 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) +(Kind.Term.set_origin new_origin (Kind.Term.fn11 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.fn11 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) +(Kind.Term.set_origin new_origin (Kind.Term.fn12 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.fn12 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) +(Kind.Term.set_origin new_origin (Kind.Term.fn13 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.fn13 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) +(Kind.Term.set_origin new_origin (Kind.Term.fn14 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.fn14 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) +(Kind.Term.set_origin new_origin (Kind.Term.fn15 ctid old_orig args)) = (Kind.Term.fn15 ctid new_origin args) +(Kind.Term.set_origin new_origin (Kind.Term.fn16 ctid old_orig args)) = (Kind.Term.fn16 ctid new_origin args) +(Kind.Term.set_origin new_origin (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) +(Kind.Term.set_origin new_origin (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) +(Kind.API.eval_main) = (Kind.Printer.text [(Kind.Term.show (Kind.Term.FN0 (Main.) 0)), " +", " +"]) +(Kind.Term.show term) = let sugars = [(Kind.Term.show.sugar.string term), (Kind.Term.show.sugar.list term), (Kind.Term.show.sugar.sigma term)]; (Maybe.try sugars (Kind.Term.show.go term)) +(Kind.Term.show.go (Kind.Term.typ orig)) = "Type" +(Kind.Term.show.go (Kind.Term.var orig name index)) = (Kind.Printer.text [(Kind.Name.show name)]) +(Kind.Term.show.go (Kind.Term.hol orig numb)) = (Kind.Printer.text ["_"]) +(Kind.Term.show.go (Kind.Term.all orig name type body)) = (Kind.Term.show.forall orig name type body) +(Kind.Term.show.go (Kind.Term.lam orig name body)) = (Kind.Printer.text ["(", (Kind.Name.show name), " => ", (Kind.Term.show (body (Kind.Term.var orig name 0))), ")"]) +(Kind.Term.show.go (Kind.Term.let orig name exp body)) = (Kind.Printer.text ["let ", (Kind.Name.show name), " = ", (Kind.Term.show exp), "; ", (Kind.Term.show (body (Kind.Term.var orig name 0)))]) +(Kind.Term.show.go (Kind.Term.ann orig expr type)) = (Kind.Printer.text ["{", (Kind.Term.show expr), " :: ", (Kind.Term.show type), "}"]) +(Kind.Term.show.go (Kind.Term.sub orig name indx redx expr)) = (Kind.Printer.text [(Kind.Term.show expr), " ## ", (Kind.Name.show name), "/", (Show.to_string (U60.show redx))]) +(Kind.Term.show.go (Kind.Term.app orig func argm)) = (Kind.Printer.text ["(", (Kind.Term.show func), " ", (Kind.Term.show argm), ")"]) +(Kind.Term.show.go (Kind.Term.ct0 ctid orig)) = (Kind.Axiom.NameOf ctid) +(Kind.Term.show.go (Kind.Term.ct1 ctid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), ")"]) +(Kind.Term.show.go (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), ")"]) +(Kind.Term.show.go (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), ")"]) +(Kind.Term.show.go (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), ")"]) +(Kind.Term.show.go (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), ")"]) +(Kind.Term.show.go (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), ")"]) +(Kind.Term.show.go (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), ")"]) +(Kind.Term.show.go (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), ")"]) +(Kind.Term.show.go (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), ")"]) +(Kind.Term.show.go (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), ")"]) +(Kind.Term.show.go (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), ")"]) +(Kind.Term.show.go (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), ")"]) +(Kind.Term.show.go (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), ")"]) +(Kind.Term.show.go (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), ")"]) +(Kind.Term.show.go (Kind.Term.ct15 ctid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), ")"]) +(Kind.Term.show.go (Kind.Term.ct16 ctid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), ")"]) +(Kind.Term.show.go (Kind.Term.fn0 fnid orig)) = (Kind.Axiom.NameOf fnid) +(Kind.Term.show.go (Kind.Term.fn1 fnid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), ")"]) +(Kind.Term.show.go (Kind.Term.fn2 fnid orig x0 x1)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), ")"]) +(Kind.Term.show.go (Kind.Term.fn3 fnid orig x0 x1 x2)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), ")"]) +(Kind.Term.show.go (Kind.Term.fn4 fnid orig x0 x1 x2 x3)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), ")"]) +(Kind.Term.show.go (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), ")"]) +(Kind.Term.show.go (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), ")"]) +(Kind.Term.show.go (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), ")"]) +(Kind.Term.show.go (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), ")"]) +(Kind.Term.show.go (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), ")"]) +(Kind.Term.show.go (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), ")"]) +(Kind.Term.show.go (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), ")"]) +(Kind.Term.show.go (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), ")"]) +(Kind.Term.show.go (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), ")"]) +(Kind.Term.show.go (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), ")"]) +(Kind.Term.show.go (Kind.Term.fn15 fnid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), ")"]) +(Kind.Term.show.go (Kind.Term.fn16 fnid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), ")"]) +(Kind.Term.show.go (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = (Kind.Printer.text [(Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), " ", (Kind.Term.show x14)]) +(Kind.Term.show.go (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = (Kind.Printer.text [(Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), " ", (Kind.Term.show x14), " ", (Kind.Term.show x15)]) +(Kind.Term.show.go (Kind.Term.hlp orig)) = "?" +(Kind.Term.show.go (Kind.Term.U60 orig)) = "U60" +(Kind.Term.show.go (Kind.Term.u60 orig numb)) = (Show.to_string (U60.show numb)) +(Kind.Term.show.go (Kind.Term.F60 orig)) = "F60" +(Kind.Term.show.go (Kind.Term.f60 orig numb)) = (Show.to_string (U60.show numb)) +(Kind.Term.show.go (Kind.Term.op2 orig operator left right)) = (Kind.Printer.text ["(", (Kind.Operator.show operator), " ", (Kind.Term.show left), " ", (Kind.Term.show right), ")"]) +(Kind.Name.show name) = (Kind.Name.show.go name "") +(Kind.Name.show.go name chrs) = (U60.if (== name 0) chrs let val = (% name 64); let chr = (U60.if (== val 0) 46 (U60.if (& (<= 1 val) (<= val 10)) (+ (- val 1) 48) (U60.if (& (<= 11 val) (<= val 36)) (+ (- val 11) 65) (U60.if (& (<= 37 val) (<= val 62)) (+ (- val 37) 97) (U60.if (== val 63) 95 63))))); (Kind.Name.show.go (/ name 64) (String.cons chr chrs))) +(U60.if 0 t f) = f +(U60.if n t f) = t +(Show.to_string show) = (show "") +(Kind.Operator.show (Kind.Operator.add)) = "+" +(Kind.Operator.show (Kind.Operator.sub)) = "-" +(Kind.Operator.show (Kind.Operator.mul)) = "*" +(Kind.Operator.show (Kind.Operator.div)) = "/" +(Kind.Operator.show (Kind.Operator.mod)) = "%" +(Kind.Operator.show (Kind.Operator.and)) = "&" +(Kind.Operator.show (Kind.Operator.or)) = "|" +(Kind.Operator.show (Kind.Operator.xor)) = "^" +(Kind.Operator.show (Kind.Operator.shl)) = "<<" +(Kind.Operator.show (Kind.Operator.shr)) = ">>" +(Kind.Operator.show (Kind.Operator.ltn)) = "<" +(Kind.Operator.show (Kind.Operator.lte)) = "<=" +(Kind.Operator.show (Kind.Operator.eql)) = "==" +(Kind.Operator.show (Kind.Operator.gte)) = ">=" +(Kind.Operator.show (Kind.Operator.gtn)) = ">" +(Kind.Operator.show (Kind.Operator.neq)) = "!=" +(Kind.Printer.text []) = "" +(Kind.Printer.text (List.cons x xs)) = (String.concat x (Kind.Printer.text xs)) +(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys)) +(String.concat "" ys) = ys +(U60.show 0) = 位str (String.cons 48 str) +(U60.show n) = 位str let next = (String.cons (+ 48 (% n 10)) str); let func = (U60.if (< n 10) 位h h 位h ((U60.show (/ n 10)) h)); (func next) +(Kind.Term.show.forall orig name type body) = (U60.if (== name 63) (Kind.Printer.text ["(", (Kind.Term.show type), " -> ", (Kind.Term.show (body (Kind.Term.var orig name 0))), ")"]) (Kind.Printer.text ["((", (Kind.Name.show name), ": ", (Kind.Term.show type), ") -> ", (Kind.Term.show (body (Kind.Term.var orig name 0))), ")"])) +(Kind.Term.show.sugar.sigma (Kind.Term.ct2 (Sigma.) orig typ (Kind.Term.lam orig_ name body))) = (Maybe.some (Kind.Printer.text ["([", (Kind.Name.show name), ": ", (Kind.Term.show typ), "] -> ", (Kind.Term.show (body (Kind.Term.var orig_ name 0))), ")"])) +(Kind.Term.show.sugar.sigma term) = (Maybe.none) +(Kind.Term.show.sugar.string term) = (Maybe.bind (Kind.Term.show.sugar.string.go term) 位res let quot = "'"; (Maybe.some (Kind.Printer.text [quot, res, quot]))) +(Kind.Term.show.sugar.string.go (Kind.Term.ct0 (String.nil.) orig)) = (Maybe.some "") +(Kind.Term.show.sugar.string.go (Kind.Term.ct2 (String.cons.) orig (Kind.Term.u60 orig1 x0) x1)) = (Maybe.bind (Kind.Term.show.sugar.string.go x1) 位tail (Maybe.some (String.cons x0 tail))) +(Kind.Term.show.sugar.string.go other) = (Maybe.none) +(Kind.Term.show.sugar.list term) = (Maybe.bind (Kind.Term.show.sugar.list.go term) 位res (Maybe.some (Kind.Printer.text ["[", (String.join " " res), "]"]))) +(Kind.Term.show.sugar.list.go (Kind.Term.ct0 (List.nil.) orig)) = (Maybe.some []) +(Kind.Term.show.sugar.list.go (Kind.Term.ct2 (List.cons.) orig x0 x1)) = (Maybe.bind (Kind.Term.show.sugar.list.go x1) 位tail (Maybe.some (List.cons (Kind.Term.show x0) tail))) +(Kind.Term.show.sugar.list.go other) = (Maybe.none) +(String.join sep list) = (String.intercalate sep list) +(String.intercalate sep xs) = (String.flatten (List.intersperse sep xs)) +(List.intersperse sep []) = [] +(List.intersperse sep [xh]) = [xh] +(List.intersperse sep (List.cons xh xt)) = (List.cons xh (List.cons sep (List.intersperse sep xt))) +(String.flatten []) = "" +(String.flatten (List.cons head tail)) = (String.concat head (String.flatten tail)) +(Maybe.try [] alt) = alt +(Maybe.try (List.cons maybe xs) alt) = (Maybe.match maybe (Maybe.try xs alt) 位value value) diff --git a/crates/kind-pass/src/inline/mod.rs b/crates/kind-pass/src/inline/mod.rs index 0e90d141..0bf3b8f1 100644 --- a/crates/kind-pass/src/inline/mod.rs +++ b/crates/kind-pass/src/inline/mod.rs @@ -78,6 +78,7 @@ impl InlineState { FxHashMap::from_iter(inlinable.names.iter().cloned().zip(args.clone())); *expr = inlinable.body.clone(); subst_on_expr(expr, subst); + self.inline_expr(expr) } else { for arg in args { self.inline_expr(arg); diff --git a/crates/kind-tests/suite/eval/AllFieldsDestruct.golden b/crates/kind-tests/suite/eval/AllFieldsDestruct.golden index eb1f4948..4e034c34 100644 --- a/crates/kind-tests/suite/eval/AllFieldsDestruct.golden +++ b/crates/kind-tests/suite/eval/AllFieldsDestruct.golden @@ -1 +1,2 @@ -500 \ No newline at end of file +500 + diff --git a/crates/kind-tests/suite/eval/DoNotation.golden b/crates/kind-tests/suite/eval/DoNotation.golden index 6d072348..71df2d14 100644 --- a/crates/kind-tests/suite/eval/DoNotation.golden +++ b/crates/kind-tests/suite/eval/DoNotation.golden @@ -1 +1,2 @@ -(Maybe.some 1009) \ No newline at end of file +(Maybe.some _ 1009) + diff --git a/crates/kind-tests/suite/eval/Getters.golden b/crates/kind-tests/suite/eval/Getters.golden index f1efb205..0911ebed 100644 --- a/crates/kind-tests/suite/eval/Getters.golden +++ b/crates/kind-tests/suite/eval/Getters.golden @@ -1 +1,2 @@ -300 \ No newline at end of file +300 + diff --git a/crates/kind-tests/suite/eval/MatchMotive.golden b/crates/kind-tests/suite/eval/MatchMotive.golden index e440e5c8..8148ef7a 100644 --- a/crates/kind-tests/suite/eval/MatchMotive.golden +++ b/crates/kind-tests/suite/eval/MatchMotive.golden @@ -1 +1,2 @@ -3 \ No newline at end of file +3 + diff --git a/crates/kind-tests/suite/eval/PatChar.golden b/crates/kind-tests/suite/eval/PatChar.golden index b44fe09a..e59f4a56 100644 --- a/crates/kind-tests/suite/eval/PatChar.golden +++ b/crates/kind-tests/suite/eval/PatChar.golden @@ -1 +1,2 @@ -65 \ No newline at end of file +65 + diff --git a/crates/kind-tests/suite/eval/Setters.golden b/crates/kind-tests/suite/eval/Setters.golden index cdb660b8..440e3e7c 100644 --- a/crates/kind-tests/suite/eval/Setters.golden +++ b/crates/kind-tests/suite/eval/Setters.golden @@ -1 +1,2 @@ -700 \ No newline at end of file +700 + diff --git a/crates/kind-tests/suite/eval/SimpleOpen.golden b/crates/kind-tests/suite/eval/SimpleOpen.golden index d8263ee9..9a7456b5 100644 --- a/crates/kind-tests/suite/eval/SimpleOpen.golden +++ b/crates/kind-tests/suite/eval/SimpleOpen.golden @@ -1 +1,2 @@ -2 \ No newline at end of file +2 + diff --git a/crates/kind-tests/suite/eval/TestWith.golden b/crates/kind-tests/suite/eval/TestWith.golden index e440e5c8..8148ef7a 100644 --- a/crates/kind-tests/suite/eval/TestWith.golden +++ b/crates/kind-tests/suite/eval/TestWith.golden @@ -1 +1,2 @@ -3 \ No newline at end of file +3 + diff --git a/crates/kind-tests/suite/eval/User.golden b/crates/kind-tests/suite/eval/User.golden index 9fb8a725..3454a946 100644 --- a/crates/kind-tests/suite/eval/User.golden +++ b/crates/kind-tests/suite/eval/User.golden @@ -1 +1,2 @@ -(Teste []) \ No newline at end of file +(Teste (List.nil _)) + diff --git a/crates/kind-tests/suite/eval/VecMatch.golden b/crates/kind-tests/suite/eval/VecMatch.golden index e440e5c8..8148ef7a 100644 --- a/crates/kind-tests/suite/eval/VecMatch.golden +++ b/crates/kind-tests/suite/eval/VecMatch.golden @@ -1 +1,2 @@ -3 \ No newline at end of file +3 + diff --git a/crates/kind-tests/suite/eval/With.golden b/crates/kind-tests/suite/eval/With.golden index 8e2afd34..4181564b 100644 --- a/crates/kind-tests/suite/eval/With.golden +++ b/crates/kind-tests/suite/eval/With.golden @@ -1 +1,2 @@ -17 \ No newline at end of file +17 + diff --git a/crates/kind-tests/suite/run/AllFieldsDestruct.golden b/crates/kind-tests/suite/run/AllFieldsDestruct.golden new file mode 100644 index 00000000..eb1f4948 --- /dev/null +++ b/crates/kind-tests/suite/run/AllFieldsDestruct.golden @@ -0,0 +1 @@ +500 \ No newline at end of file diff --git a/crates/kind-tests/suite/run/AllFieldsDestruct.kind2 b/crates/kind-tests/suite/run/AllFieldsDestruct.kind2 new file mode 100644 index 00000000..bddee184 --- /dev/null +++ b/crates/kind-tests/suite/run/AllFieldsDestruct.kind2 @@ -0,0 +1,10 @@ +#derive[match] +record Pudim { + owo : U60 + uwu : U60 +} + +Main : U60 +Main = + let Pudim.new owo uwu .. = Pudim.new (uwu = 300) (owo = 200) + (+ owo uwu) \ No newline at end of file diff --git a/crates/kind-tests/suite/run/DoNotation.golden b/crates/kind-tests/suite/run/DoNotation.golden new file mode 100644 index 00000000..6d072348 --- /dev/null +++ b/crates/kind-tests/suite/run/DoNotation.golden @@ -0,0 +1 @@ +(Maybe.some 1009) \ No newline at end of file diff --git a/crates/kind-tests/suite/run/DoNotation.kind2 b/crates/kind-tests/suite/run/DoNotation.kind2 new file mode 100644 index 00000000..dd28d9ec --- /dev/null +++ b/crates/kind-tests/suite/run/DoNotation.kind2 @@ -0,0 +1,12 @@ +Main : Maybe U60 +Main = + do Maybe { + Maybe.some 3 + Maybe.pure 2 + ask res = Maybe.pure 2 + ask res2 = Maybe.pure 3 + match Maybe t = (Maybe.some 4) { + some val => Maybe.pure (+ 1000 (+ val (+ res res2))) + none => Maybe.none + } + } \ No newline at end of file diff --git a/crates/kind-tests/suite/run/Getters.golden b/crates/kind-tests/suite/run/Getters.golden new file mode 100644 index 00000000..f1efb205 --- /dev/null +++ b/crates/kind-tests/suite/run/Getters.golden @@ -0,0 +1 @@ +300 \ No newline at end of file diff --git a/crates/kind-tests/suite/run/Getters.kind2 b/crates/kind-tests/suite/run/Getters.kind2 new file mode 100644 index 00000000..00615476 --- /dev/null +++ b/crates/kind-tests/suite/run/Getters.kind2 @@ -0,0 +1,10 @@ +#derive[getters] +record Pair (a: Type) (b: Type) { + fst : a + snd : b +} + +Main : U60 +Main = + let a = (Pair.new 100 200 :: Pair U60 U60) + (+ (Pair.fst.get a) (Pair.snd.get a)) \ No newline at end of file diff --git a/crates/kind-tests/suite/run/MatchMotive.golden b/crates/kind-tests/suite/run/MatchMotive.golden new file mode 100644 index 00000000..e440e5c8 --- /dev/null +++ b/crates/kind-tests/suite/run/MatchMotive.golden @@ -0,0 +1 @@ +3 \ No newline at end of file diff --git a/crates/kind-tests/suite/run/MatchMotive.kind2 b/crates/kind-tests/suite/run/MatchMotive.kind2 new file mode 100644 index 00000000..e6a0a433 --- /dev/null +++ b/crates/kind-tests/suite/run/MatchMotive.kind2 @@ -0,0 +1,19 @@ +#derive[match] +type Maybe (a: Type) { + some (val: a) + none +} + +Str : Type +Str.nil : Str + +MotiveGen (n: Maybe U60) : Type +MotiveGen (Maybe.some _) = U60 +MotiveGen Maybe.none = Str + +Main : U60 +Main = + match Maybe t = Maybe.some 3 { + some => t.val + none => Str.nil + } : (x => MotiveGen x) \ No newline at end of file diff --git a/crates/kind-tests/suite/eval/NoMatch.golden b/crates/kind-tests/suite/run/NoMatch.golden similarity index 89% rename from crates/kind-tests/suite/eval/NoMatch.golden rename to crates/kind-tests/suite/run/NoMatch.golden index be0d9bf2..7cc1c9a8 100644 --- a/crates/kind-tests/suite/eval/NoMatch.golden +++ b/crates/kind-tests/suite/run/NoMatch.golden @@ -1,6 +1,6 @@ ERROR Required functions are not implemented for this type. - /--[suite/eval/NoMatch.kind2:3:5] + /--[suite/run/NoMatch.kind2:3:5] | | / 3 | | match NoMatch t = NoMatch.pudding { diff --git a/crates/kind-tests/suite/eval/NoMatch.kind2 b/crates/kind-tests/suite/run/NoMatch.kind2 similarity index 100% rename from crates/kind-tests/suite/eval/NoMatch.kind2 rename to crates/kind-tests/suite/run/NoMatch.kind2 diff --git a/crates/kind-tests/suite/run/PatChar.golden b/crates/kind-tests/suite/run/PatChar.golden new file mode 100644 index 00000000..b44fe09a --- /dev/null +++ b/crates/kind-tests/suite/run/PatChar.golden @@ -0,0 +1 @@ +65 \ No newline at end of file diff --git a/crates/kind-tests/suite/run/PatChar.kind2 b/crates/kind-tests/suite/run/PatChar.kind2 new file mode 100644 index 00000000..6c88c307 --- /dev/null +++ b/crates/kind-tests/suite/run/PatChar.kind2 @@ -0,0 +1,6 @@ +Lol (n: U60) : U60 +Lol 'A' = 'A' +Lol _ = 0 + +Main : U60 +Main = (Lol 'A') \ No newline at end of file diff --git a/crates/kind-tests/suite/run/Setters.golden b/crates/kind-tests/suite/run/Setters.golden new file mode 100644 index 00000000..cdb660b8 --- /dev/null +++ b/crates/kind-tests/suite/run/Setters.golden @@ -0,0 +1 @@ +700 \ No newline at end of file diff --git a/crates/kind-tests/suite/run/Setters.kind2 b/crates/kind-tests/suite/run/Setters.kind2 new file mode 100644 index 00000000..1411a6bd --- /dev/null +++ b/crates/kind-tests/suite/run/Setters.kind2 @@ -0,0 +1,12 @@ +#derive[getters, setters] +record Pair (a: Type) (b: Type) { + fst : a + snd : b +} + +Main : U60 +Main = + let a = (Pair.new 100 200 :: Pair U60 U60) + let b = Pair.fst.set a 500 + let c = Pair.snd.set a (+ (Pair.fst.get b) (Pair.snd.get b)) + Pair.snd.get c \ No newline at end of file diff --git a/crates/kind-tests/suite/run/SimpleOpen.golden b/crates/kind-tests/suite/run/SimpleOpen.golden new file mode 100644 index 00000000..d8263ee9 --- /dev/null +++ b/crates/kind-tests/suite/run/SimpleOpen.golden @@ -0,0 +1 @@ +2 \ No newline at end of file diff --git a/crates/kind-tests/suite/run/SimpleOpen.kind2 b/crates/kind-tests/suite/run/SimpleOpen.kind2 new file mode 100644 index 00000000..f4b495e5 --- /dev/null +++ b/crates/kind-tests/suite/run/SimpleOpen.kind2 @@ -0,0 +1,16 @@ +#derive[match] +record Pudim { + owo : U60 + uwu : U60 +} + +#keep +Ok (n: Pudim) : U60 +Ok n = + open Pudim n + (+ n.owo n.uwu) + +Main : U60 +Main = + let Pudim.new owo .. = Pudim.new (uwu = 300) (owo = 200) + 2 \ No newline at end of file diff --git a/crates/kind-tests/suite/run/TestWith.golden b/crates/kind-tests/suite/run/TestWith.golden new file mode 100644 index 00000000..e440e5c8 --- /dev/null +++ b/crates/kind-tests/suite/run/TestWith.golden @@ -0,0 +1 @@ +3 \ No newline at end of file diff --git a/crates/kind-tests/suite/run/TestWith.kind2 b/crates/kind-tests/suite/run/TestWith.kind2 new file mode 100644 index 00000000..7aed11f6 --- /dev/null +++ b/crates/kind-tests/suite/run/TestWith.kind2 @@ -0,0 +1,19 @@ +#derive[match] +type Nat { + succ (pred: Nat) + zero +} + +Run (n: Nat) : Type +Run (Nat.succ n) = U60 +Run (Nat.zero) = U60 + +Lero (n: Nat) (f: Run n) : U60 +Lero t1 n f = + match Nat n with (f : Run n) { + succ => (+ f 2) + zero => (+ f 1) + } + +Main : U60 +Main = Lero (Nat.succ Nat.zero) 1 \ No newline at end of file diff --git a/crates/kind-tests/suite/run/User.golden b/crates/kind-tests/suite/run/User.golden new file mode 100644 index 00000000..9fb8a725 --- /dev/null +++ b/crates/kind-tests/suite/run/User.golden @@ -0,0 +1 @@ +(Teste []) \ No newline at end of file diff --git a/crates/kind-tests/suite/run/User.kind2 b/crates/kind-tests/suite/run/User.kind2 new file mode 100644 index 00000000..368cb9e8 --- /dev/null +++ b/crates/kind-tests/suite/run/User.kind2 @@ -0,0 +1,12 @@ + +#kdl_run +Main : U60 +Main = Teste List.nil + +type List (t: Type) { + cons (x: t) (xs: List t) + nil +} + +Teste (n: List U60) : U60 +Teste (List.cons 2 xs) = 2 \ No newline at end of file diff --git a/crates/kind-tests/suite/run/VecMatch.golden b/crates/kind-tests/suite/run/VecMatch.golden new file mode 100644 index 00000000..e440e5c8 --- /dev/null +++ b/crates/kind-tests/suite/run/VecMatch.golden @@ -0,0 +1 @@ +3 \ No newline at end of file diff --git a/crates/kind-tests/suite/run/VecMatch.kind2 b/crates/kind-tests/suite/run/VecMatch.kind2 new file mode 100644 index 00000000..36c46ba8 --- /dev/null +++ b/crates/kind-tests/suite/run/VecMatch.kind2 @@ -0,0 +1,20 @@ +type Nat { + succ (pred : Nat) + zero +} + +#derive[match] +type Vec (t: Type) ~ (n: Nat) { + cons (x : t) (xs : Vec t size) : Vec t (Nat.succ size) + nil : Vec t Nat.zero +} + +Vec.count (v: Vec t n) : U60 +Vec.count vec = + match Vec vec { + cons xs .. => (+ 1 (Vec.count xs)) + nil => 0 + } + +Main : U60 +Main = Vec.count (Vec.cons 10 (Vec.cons 20 (Vec.cons 30 Vec.nil))) \ No newline at end of file diff --git a/crates/kind-tests/suite/run/With.golden b/crates/kind-tests/suite/run/With.golden new file mode 100644 index 00000000..8e2afd34 --- /dev/null +++ b/crates/kind-tests/suite/run/With.golden @@ -0,0 +1 @@ +17 \ No newline at end of file diff --git a/crates/kind-tests/suite/run/With.kind2 b/crates/kind-tests/suite/run/With.kind2 new file mode 100644 index 00000000..0779bb36 --- /dev/null +++ b/crates/kind-tests/suite/run/With.kind2 @@ -0,0 +1,16 @@ +#derive[match] +type Maybe (t: Type) { + some (val: t) + none +} + +Main : U60 +Main = + let t = Maybe.some 3 + let e = 4 + let f = 10 + match Maybe t with e f { + some val => (+ val (+ e f)) + none => (* e f) + } + diff --git a/crates/kind-tests/tests/mod.rs b/crates/kind-tests/tests/mod.rs index b5ccc464..3825588b 100644 --- a/crates/kind-tests/tests/mod.rs +++ b/crates/kind-tests/tests/mod.rs @@ -86,8 +86,8 @@ fn test_checker_issues() -> Result<(), Error> { #[test] #[timeout(15000)] -fn test_eval() -> Result<(), Error> { - test_kind2(Path::new("./suite/eval"), |path, session| { +fn test_run() -> Result<(), Error> { + test_kind2(Path::new("./suite/run"), |path, session| { let entrypoints = vec!["Main".to_string()]; let check = driver::erase_book(session, path, entrypoints) .map(|file| driver::compile_book_to_hvm(file, false)) @@ -99,6 +99,18 @@ fn test_eval() -> Result<(), Error> { Ok(()) } +#[test] +#[timeout(15000)] +fn test_eval() -> Result<(), Error> { + test_kind2(Path::new("./suite/eval"), |path, session| { + let check = driver::desugar_book(session, path) + .map(|file| driver::eval_in_checker(&file)); + + check.ok().map(|x| x.0) + })?; + Ok(()) +} + #[test] #[timeout(15000)] fn test_eval_issues() -> Result<(), Error> { diff --git a/tests/test_wikind.sh b/tests/test_wikind.sh deleted file mode 100755 index 07ef0ba6..00000000 --- a/tests/test_wikind.sh +++ /dev/null @@ -1,9 +0,0 @@ -set -e - -git clone https://github.com/Kindelia/Wikind.git - -for file in ./Wikind/**/*.kind2; do - cargo run --release -- --root=Wikind check $file -done - -rm Wikind \ No newline at end of file From 663c87ffc01bc584bdbe8504f5a002337a8541ab Mon Sep 17 00:00:00 2001 From: felipegchi Date: Mon, 16 Jan 2023 09:26:21 -0300 Subject: [PATCH 2/2] tests: added tests --- .../suite/issues/eval/CallStr.golden | 3 ++- .../suite/issues/eval/ISSUE-472.golden | 3 +++ .../suite/issues/eval/ISSUE-472.kind2 | 23 +++++++++++++++++++ .../suite/issues/run/CallStr.golden | 1 + .../kind-tests/suite/issues/run/CallStr.kind2 | 3 +++ .../suite/issues/run/ISSUE-472.golden | 2 ++ .../suite/issues/run/ISSUE-472.kind2 | 23 +++++++++++++++++++ crates/kind-tests/tests/mod.rs | 12 ++++++++++ 8 files changed, 69 insertions(+), 1 deletion(-) create mode 100644 crates/kind-tests/suite/issues/eval/ISSUE-472.golden create mode 100644 crates/kind-tests/suite/issues/eval/ISSUE-472.kind2 create mode 100644 crates/kind-tests/suite/issues/run/CallStr.golden create mode 100644 crates/kind-tests/suite/issues/run/CallStr.kind2 create mode 100644 crates/kind-tests/suite/issues/run/ISSUE-472.golden create mode 100644 crates/kind-tests/suite/issues/run/ISSUE-472.kind2 diff --git a/crates/kind-tests/suite/issues/eval/CallStr.golden b/crates/kind-tests/suite/issues/eval/CallStr.golden index 8660dd84..db94bda7 100644 --- a/crates/kind-tests/suite/issues/eval/CallStr.golden +++ b/crates/kind-tests/suite/issues/eval/CallStr.golden @@ -1 +1,2 @@ -"ata" \ No newline at end of file +'ata' + diff --git a/crates/kind-tests/suite/issues/eval/ISSUE-472.golden b/crates/kind-tests/suite/issues/eval/ISSUE-472.golden new file mode 100644 index 00000000..4c43d39b --- /dev/null +++ b/crates/kind-tests/suite/issues/eval/ISSUE-472.golden @@ -0,0 +1,3 @@ +' +' + diff --git a/crates/kind-tests/suite/issues/eval/ISSUE-472.kind2 b/crates/kind-tests/suite/issues/eval/ISSUE-472.kind2 new file mode 100644 index 00000000..0c7d1be9 --- /dev/null +++ b/crates/kind-tests/suite/issues/eval/ISSUE-472.kind2 @@ -0,0 +1,23 @@ +Char : Type +Char = U60 + +#inline +String.new_line : (String) +String.new_line = (String.pure (Char.newline)) + +Main : _ +Main = String.new_line + +#inline +Char.newline : (Char) +Char.newline = 10 + +#derive[match] +type String { + nil + cons (head: (Char)) (tail: (String)) +} + +#inline +String.pure (x: (Char)) : (String) +String.pure x = (String.cons x (String.nil)) \ No newline at end of file diff --git a/crates/kind-tests/suite/issues/run/CallStr.golden b/crates/kind-tests/suite/issues/run/CallStr.golden new file mode 100644 index 00000000..8660dd84 --- /dev/null +++ b/crates/kind-tests/suite/issues/run/CallStr.golden @@ -0,0 +1 @@ +"ata" \ No newline at end of file diff --git a/crates/kind-tests/suite/issues/run/CallStr.kind2 b/crates/kind-tests/suite/issues/run/CallStr.kind2 new file mode 100644 index 00000000..e1a7f558 --- /dev/null +++ b/crates/kind-tests/suite/issues/run/CallStr.kind2 @@ -0,0 +1,3 @@ +Main : U60 { + "ata" +} \ No newline at end of file diff --git a/crates/kind-tests/suite/issues/run/ISSUE-472.golden b/crates/kind-tests/suite/issues/run/ISSUE-472.golden new file mode 100644 index 00000000..6e568be9 --- /dev/null +++ b/crates/kind-tests/suite/issues/run/ISSUE-472.golden @@ -0,0 +1,2 @@ +" +" \ No newline at end of file diff --git a/crates/kind-tests/suite/issues/run/ISSUE-472.kind2 b/crates/kind-tests/suite/issues/run/ISSUE-472.kind2 new file mode 100644 index 00000000..0c7d1be9 --- /dev/null +++ b/crates/kind-tests/suite/issues/run/ISSUE-472.kind2 @@ -0,0 +1,23 @@ +Char : Type +Char = U60 + +#inline +String.new_line : (String) +String.new_line = (String.pure (Char.newline)) + +Main : _ +Main = String.new_line + +#inline +Char.newline : (Char) +Char.newline = 10 + +#derive[match] +type String { + nil + cons (head: (Char)) (tail: (String)) +} + +#inline +String.pure (x: (Char)) : (String) +String.pure x = (String.cons x (String.nil)) \ No newline at end of file diff --git a/crates/kind-tests/tests/mod.rs b/crates/kind-tests/tests/mod.rs index 3825588b..38c49510 100644 --- a/crates/kind-tests/tests/mod.rs +++ b/crates/kind-tests/tests/mod.rs @@ -115,6 +115,18 @@ fn test_eval() -> Result<(), Error> { #[timeout(15000)] fn test_eval_issues() -> Result<(), Error> { test_kind2(Path::new("./suite/issues/eval"), |path, session| { + let check = driver::desugar_book(session, path) + .map(|file| driver::eval_in_checker(&file)); + + check.ok().map(|x| x.0) + })?; + Ok(()) +} + +#[test] +#[timeout(15000)] +fn test_run_issues() -> Result<(), Error> { + test_kind2(Path::new("./suite/issues/run"), |path, session| { let entrypoints = vec!["Main".to_string()]; let check = driver::erase_book(session, path, entrypoints) .map(|file| driver::compile_book_to_hvm(file, false))