mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-08-15 18:20:26 +03:00
Cleanup
This commit is contained in:
Victor Maia
parent
9a7fe526e8
commit
b8092e84d5
193
src/checker.hvm
193
src/checker.hvm
@ -67,34 +67,6 @@ Main =
|
||||
]))
|
||||
])
|
||||
|
||||
//(Api.output [
|
||||
//(Result (Negate.) [(Checked [(Ct1 (List.) (Ct0 (Bool.))), (Ct0 (Bool.))] 2 (Unit)), (Checked [] 0 (Unit))]),
|
||||
//(Result (And.) [(Checked [] 0 (Unit)), (Checked [] 0 (Unit)), (Checked [] 0 (Unit)), (Checked [] 0 (Unit))]),
|
||||
//(Result (Nil.) []),
|
||||
//(Result (Main.) [(Errored (TypeMismatch (Ct0 (Nat.)) (Ct0 (Bool.))))]),
|
||||
//(Result (Cons.) []),
|
||||
//(Result (Zero.) []),
|
||||
//(Result (Nat.) []),
|
||||
//(Result (List.) []),
|
||||
//(Result (Succ.) []),
|
||||
//(Result (Bool.) []),
|
||||
//(Result (False.) []),
|
||||
//(Result (Not.) [(Checked [] 0 (Unit)), (Checked [] 0 (Unit))]),
|
||||
//(Result (True.) []),
|
||||
//(Result (Tail.) [(Errored (TypeMismatch (Ct1 (List.) (Inp 1)) (Ct1 (List.) (Var 0))))])
|
||||
//])
|
||||
|
||||
//(Api.output Nil) = Nil
|
||||
//(Api.output (Cons (Result fn checks) results)) =
|
||||
//(Text [
|
||||
|
||||
//])
|
||||
|
||||
|
||||
//(Api.output (Cons (Errored err) results)) = (Cons (Some err) (Api.errors results))
|
||||
//(Api.output (Cons other results)) = (Api.errors results)
|
||||
|
||||
|
||||
// Prelude
|
||||
// -------
|
||||
|
||||
@ -914,168 +886,3 @@ Main =
|
||||
// User-Defined Functions
|
||||
// ----------------------
|
||||
////INJECT////
|
||||
|
||||
Functions =
|
||||
let fns = Nil
|
||||
let fns = (Cons And. fns)
|
||||
let fns = (Cons Nil. fns)
|
||||
let fns = (Cons List. fns)
|
||||
let fns = (Cons Succ. fns)
|
||||
let fns = (Cons True. fns)
|
||||
let fns = (Cons Nat. fns)
|
||||
let fns = (Cons Not. fns)
|
||||
let fns = (Cons Bool. fns)
|
||||
let fns = (Cons Negate. fns)
|
||||
let fns = (Cons Tail. fns)
|
||||
let fns = (Cons Main. fns)
|
||||
let fns = (Cons False. fns)
|
||||
let fns = (Cons Cons. fns)
|
||||
let fns = (Cons Zero. fns)
|
||||
fns
|
||||
|
||||
// And
|
||||
// ---
|
||||
|
||||
(NameOf And.) = "And"
|
||||
(HashOf And.) = %And
|
||||
(TypeOf And.) = (All (Ct0 Bool.) λa (All (Ct0 Bool.) λb (Ct0 Bool.)))
|
||||
(Rule2 And. (Ct0 True.) (Ct0 True.)) = (Ct0 True.)
|
||||
(Rule2 And. (Ct0 True.) (Ct0 False.)) = (Ct0 False.)
|
||||
(Rule2 And. (Ct0 False.) (Ct0 True.)) = (Ct0 False.)
|
||||
(Rule2 And. (Ct0 False.) (Ct0 False.)) = (Ct0 False.)
|
||||
(Verify And.) =
|
||||
(Cons (LHS (Ct0 True.) (LHS (Ct0 True.) (RHS (Rule2 And. (Ct0 True.) (Ct0 True.)))))
|
||||
(Cons (LHS (Ct0 True.) (LHS (Ct0 False.) (RHS (Rule2 And. (Ct0 True.) (Ct0 False.)))))
|
||||
(Cons (LHS (Ct0 False.) (LHS (Ct0 True.) (RHS (Rule2 And. (Ct0 False.) (Ct0 True.)))))
|
||||
(Cons (LHS (Ct0 False.) (LHS (Ct0 False.) (RHS (Rule2 And. (Ct0 False.) (Ct0 False.)))))
|
||||
Nil))))
|
||||
|
||||
// Nil
|
||||
// ---
|
||||
|
||||
(NameOf Nil.) = "Nil"
|
||||
(HashOf Nil.) = %Nil
|
||||
(TypeOf Nil.) = (All Typ λa (Ct1 List. a))
|
||||
(Verify Nil.) =
|
||||
Nil
|
||||
|
||||
// List
|
||||
// ----
|
||||
|
||||
(NameOf List.) = "List"
|
||||
(HashOf List.) = %List
|
||||
(TypeOf List.) = (All Typ λa Typ)
|
||||
(Verify List.) =
|
||||
Nil
|
||||
|
||||
// Succ
|
||||
// ----
|
||||
|
||||
(NameOf Succ.) = "Succ"
|
||||
(HashOf Succ.) = %Succ
|
||||
(TypeOf Succ.) = (All (Ct0 Nat.) λpred (Ct0 Nat.))
|
||||
(Verify Succ.) =
|
||||
Nil
|
||||
|
||||
// True
|
||||
// ----
|
||||
|
||||
(NameOf True.) = "True"
|
||||
(HashOf True.) = %True
|
||||
(TypeOf True.) = (Ct0 Bool.)
|
||||
(Verify True.) =
|
||||
Nil
|
||||
|
||||
// Nat
|
||||
// ---
|
||||
|
||||
(NameOf Nat.) = "Nat"
|
||||
(HashOf Nat.) = %Nat
|
||||
(TypeOf Nat.) = Typ
|
||||
(Verify Nat.) =
|
||||
Nil
|
||||
|
||||
// Not
|
||||
// ---
|
||||
|
||||
(NameOf Not.) = "Not"
|
||||
(HashOf Not.) = %Not
|
||||
(TypeOf Not.) = (All (Ct0 Bool.) λa (Ct0 Bool.))
|
||||
(Rule1 Not. (Ct0 True.)) = (Ct0 False.)
|
||||
(Rule1 Not. (Ct0 False.)) = (Ct0 True.)
|
||||
(Verify Not.) =
|
||||
(Cons (LHS (Ct0 True.) (RHS (Rule1 Not. (Ct0 True.))))
|
||||
(Cons (LHS (Ct0 False.) (RHS (Rule1 Not. (Ct0 False.))))
|
||||
Nil))
|
||||
|
||||
// Bool
|
||||
// ----
|
||||
|
||||
(NameOf Bool.) = "Bool"
|
||||
(HashOf Bool.) = %Bool
|
||||
(TypeOf Bool.) = Typ
|
||||
(Verify Bool.) =
|
||||
Nil
|
||||
|
||||
// Negate
|
||||
// ------
|
||||
|
||||
(NameOf Negate.) = "Negate"
|
||||
(HashOf Negate.) = %Negate
|
||||
(TypeOf Negate.) = (All (Ct1 List. (Ct0 Bool.)) λxs (Ct1 List. (Ct0 Bool.)))
|
||||
(Rule1 Negate. (Ct3 Cons. (Ct0 Bool.) x xs)) = (Ct3 Cons. (Ct0 Bool.) (Fn1 Not. x) (Fn1 Negate. xs))
|
||||
(Rule1 Negate. (Ct1 Nil. (Ct0 Bool.))) = (Ct1 Nil. (Ct0 Bool.))
|
||||
(Verify Negate.) =
|
||||
(Cons (LHS (Ct3 Cons. (Ct0 Bool.) (Inp 0) (Inp 1)) (RHS (Rule1 Negate. (Ct3 Cons. (Ct0 Bool.) (Var 0) (Var 1)))))
|
||||
(Cons (LHS (Ct1 Nil. (Ct0 Bool.)) (RHS (Rule1 Negate. (Ct1 Nil. (Ct0 Bool.)))))
|
||||
Nil))
|
||||
|
||||
// Tail
|
||||
// ----
|
||||
|
||||
(NameOf Tail.) = "Tail"
|
||||
(HashOf Tail.) = %Tail
|
||||
(TypeOf Tail.) = (All Typ λa (All (Ct1 List. a) λxs (Ct1 List. a)))
|
||||
(Rule2 Tail. a (Ct3 Cons. t x xs)) = xs
|
||||
(Verify Tail.) =
|
||||
(Cons (LHS (Inp 0) (LHS (Ct3 Cons. (Inp 1) (Inp 2) (Inp 3)) (RHS (Rule2 Tail. (Var 0) (Ct3 Cons. (Var 1) (Var 2) (Var 3))))))
|
||||
Nil)
|
||||
|
||||
// Main
|
||||
// ----
|
||||
|
||||
(NameOf Main.) = "Main"
|
||||
(HashOf Main.) = %Main
|
||||
(TypeOf Main.) = (Ct1 List. (Ct0 Bool.))
|
||||
(Rule0 Main.) = (Fn2 Tail. (Ct0 Bool.) (Ct3 Cons. (Ct0 Bool.) (Ct0 Zero.) (Ct3 Cons. (Ct0 Bool.) (Ct0 False.) (Ct1 Nil. (Ct0 Bool.)))))
|
||||
(Verify Main.) =
|
||||
(Cons (RHS (Rule0 Main.))
|
||||
Nil)
|
||||
|
||||
// False
|
||||
// -----
|
||||
|
||||
(NameOf False.) = "False"
|
||||
(HashOf False.) = %False
|
||||
(TypeOf False.) = (Ct0 Bool.)
|
||||
(Verify False.) =
|
||||
Nil
|
||||
|
||||
// Cons
|
||||
// ----
|
||||
|
||||
(NameOf Cons.) = "Cons"
|
||||
(HashOf Cons.) = %Cons
|
||||
(TypeOf Cons.) = (All Typ λa (All a λx (All (Ct1 List. a) λxs (Ct1 List. a))))
|
||||
(Verify Cons.) =
|
||||
Nil
|
||||
|
||||
// Zero
|
||||
// ----
|
||||
|
||||
(NameOf Zero.) = "Zero"
|
||||
(HashOf Zero.) = %Zero
|
||||
(TypeOf Zero.) = (Ct0 Nat.)
|
||||
(Verify Zero.) =
|
||||
Nil
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user