Passing all test cases now

Changes

2 changed files (+62/-16)

• Main.lean
  • @@ -57,7 +57,7 @@ inductive Term
    | fls_elim : Typ × Term → Term def Typ.toString : Typ → String - | new α => s!"(cons \"new\" \"{α}\")" + | new α => s!"(list \"new\" \"{α}\")" | fn α β => s!"(list \"fn\" {α.toString} {β.toString})" | prod α β => s!"(list \"prod\" {α.toString} {β.toString})" | sum α β => s!"(list \"sum\" {α.toString} {β.toString})"
  • @@ -70,17 +70,17 @@ mutual
    def toString (t : Typ × Term) := s!"(cons {t.1} {t.2.toString})" def Term.toString : Term → String - | .var x => s!"(cons \"var\" '{x})" + | .var x => s!"(list \"var\" '{x})" | .lam x b => s!"(list \"lam\" '{x} {toString b})" | .app f x => s!"(list \"app\" {toString f} {toString x})" | .and x y => s!"(list \"and\" {toString x} {toString y})" - | .and1 x => s!"(cons \"and1\" {toString x})" - | .and2 y => s!"(cons \"and2\" {toString y})" - | .or z => s!"(cons \"or\" {toString z})" + | .and1 x => s!"(list \"and1\" {toString x})" + | .and2 y => s!"(list \"and2\" {toString y})" + | .or z => s!"(list \"or\" {toString z})" | .zero => s!"'(\"zero\")" - | .succ x => s!"(cons \"succ\" {toString x})" + | .succ x => s!"(list \"succ\" {toString x})" | .nat_elim τ a b c => s!"(list \"nat_elim\" {τ} {toString a} {toString b} {toString c})" - | .fls_elim x => s!"(cons \"fls_elim\" {toString x})" + | .fls_elim x => s!"(list \"fls_elim\" {toString x})" end instance : ToString (Typ × Term) := ⟨toString⟩
  • @@ -121,6 +121,7 @@ def check (env : Std.HashMap String Typ) : Typ → Term → Bool
    theorem false_empty : check (.ofList []) .fls t == false := by sorry + -- TODO: Implement eval so we can state 2 + 2 = 4 -- def eval env (venv : Std.HashMap String Term) τ t (h : check env τ t) (henv : ∀ x, x ∈ env.keys → x ∈ venv.keys) : Term := -- match τ, t with -- | _, .var x =>
  • @@ -141,16 +142,22 @@ def a_imp_b_imp_ba := (Typ.fn (.new "A") (.fn (.new "B") (.prod (.new "B") (.new
    #guard check (.ofList []) a_imp_b_imp_ba.1 a_imp_b_imp_ba.2 + #eval IO.println a_imp_b_imp_ba + /-- A ∧ B → B ∧ A -/ def ab_imp_ba := (Typ.fn (.prod (.new "A") (.new "B")) (.prod (.new "B") (.new "A")), Term.lam "ab" (.prod (.new "B") (.new "A"), .and (.new "B", .and2 (.prod (.new "A") (.new "B"), .var "ab")) (.new "A", .and1 (.prod (.new "A") (.new "B"), .var "ab")))) #guard check (.ofList []) ab_imp_ba.1 ab_imp_ba.2 + #eval IO.println ab_imp_ba + /-- ¬(A ∨ B) → ¬A -/ def not_ab_imp_not_a := (Typ.fn (.fn (.sum (.new "A") (.new "B")) .fls) (.fn (.new "A") .fls), Term.lam "f" (.fn (.new "A") .fls, .lam "x" (.fls, .app (.fn (.sum (.new "A") (.new "B")) .fls, .var "f") (.sum (.new "A") (.new "B"), .or (.new "A", .var "x"))))) #guard check (.ofList []) not_ab_imp_not_a.1 not_ab_imp_not_a.2 + #eval IO.println not_ab_imp_not_a + /-- 2 exists (yeah I know this is not super exciting) -/ def two := (Typ.nat, Term.succ (.nat, (.succ (.nat, .zero))))
• main.lurk
  • @@ -1,27 +1,66 @@
    + ; Get second element of list (0-indexed) !(def arg1 (lambda (x) (car (cdr x)))) + ; Get left element of tuple at second position in list + !(def arg1a (lambda (x) (car (arg1 x)))) + + !(def arg1b (lambda (x) (cdr (arg1 x)))) + + ; Get third element of list !(def arg2 (lambda (x) (car (cdr (cdr x))))) - !(def arg21 (lambda (x) (car (arg2 x)))) + !(def arg2a (lambda (x) (car (arg2 x)))) - !(def arg22 (lambda (x) (cdr (arg2 x)))) + !(def arg2b (lambda (x) (cdr (arg2 x)))) ; Boolean and !(def and (lambda (x y) (if x (if y t nil) nil))) + ; Boolean or + !(def or (lambda (x y) (if x t (if y t nil)))) + ; NEED defrec instead of def for recursive functions + ; TODO: Implement nats !(defrec check (lambda (env typ term) (if (eq (car term) "var") - (eq typ (eval (cdr term) env)) + (eq typ (eval (arg1 term) env)) (if (and (eq (car typ) "fn") (eq (car term) "lam")) - (and (eq (arg2 typ) (arg21 term)) (check (eval (list 'let (list (list (arg1 term) (list 'quote (arg1 typ)))) '(current-env)) env) (arg21 term) (arg22 term))) - nil)))) + (and (eq (arg2 typ) (arg2a term)) + ; Crazy eval magic + (check (eval (list 'let (list (list (arg1 term) (list 'quote (arg1 typ)))) '(current-env)) env) (arg2a term) (arg2b term))) + (if (and (eq (car term) "app") (eq (car (arg1a term)) "fn")) + (and (eq (arg1 (arg1a term)) (arg2a term)) (and (eq (arg2 (arg1a term)) typ) + (and (check env (arg1a term) (arg1b term)) + (check env (arg2a term) (arg2b term))))) + (if (and (eq (car typ) "prod") (eq (car term) "and")) + (and (eq (arg1a term) (arg1 typ)) (and (eq (arg2a term) (arg2 typ)) + (and (check env (arg1a term) (arg1b term)) (check env (arg2a term) (arg2b term))))) + (if (and (eq (car term) "and1") (eq (car (arg1a term)) "prod")) + (and (eq (arg1 (arg1a term)) typ) + (check env (arg1a term) (arg1b term))) + (if (and (eq (car term) "and2") (eq (car (arg1a term)) "prod")) + (and (eq (arg2 (arg1a term)) typ) + (check env (arg1a term) (arg1b term))) + (if (and (eq (car typ) "sum") (eq (car term) "or")) + (and (or (eq (arg1a term) (arg1 typ)) (eq (arg1a term) (arg2 typ))) + (check env (arg1a term) (arg1b term))) + (if (and (eq (car term) "fls_elim") (eq (car (arg1a term)))) + t + nil)))))))))) ; Autogenerated by Main.lean - !(def a_imp_a (cons (list "fn" (cons "new" "A") (cons "new" "A")) (list "lam" 'a (cons (cons "new" "A") (cons "var" 'a))))) + !(def a_imp_a (cons (list "fn" (list "new" "A") (list "new" "A")) (list "lam" 'a (cons (list "new" "A") (list "var" 'a))))) (check (empty-env) (car a_imp_a) (cdr a_imp_a)) - ; !(def env (empty-env)) - ; !(def typ (car a_imp_a)) - ; !(def term (cdr a_imp_a)) + !(def a_imp_b_imp_ba (cons (list "fn" (list "new" "A") (list "fn" (list "new" "B") (list "prod" (list "new" "B") (list "new" "A")))) (list "lam" 'a (cons (list "fn" (list "new" "B") (list "prod" (list "new" "B") (list "new" "A"))) (list "lam" 'b (cons (list "prod" (list "new" "B") (list "new" "A")) (list "and" (cons (list "new" "B") (list "var" 'b)) (cons (list "new" "A") (list "var" 'a))))))))) + + (check (empty-env) (car a_imp_b_imp_ba) (cdr a_imp_b_imp_ba)) + + !(def ab_imp_ba (cons (list "fn" (list "prod" (list "new" "A") (list "new" "B")) (list "prod" (list "new" "B") (list "new" "A"))) (list "lam" 'ab (cons (list "prod" (list "new" "B") (list "new" "A")) (list "and" (cons (list "new" "B") (list "and2" (cons (list "prod" (list "new" "A") (list "new" "B")) (list "var" 'ab)))) (cons (list "new" "A") (list "and1" (cons (list "prod" (list "new" "A") (list "new" "B")) (list "var" 'ab))))))))) + + (check (empty-env) (car ab_imp_ba) (cdr ab_imp_ba)) + + !(def not_ab_imp_not_a (cons (list "fn" (list "fn" (list "sum" (list "new" "A") (list "new" "B")) '("fls")) (list "fn" (list "new" "A") '("fls"))) (list "lam" 'f (cons (list "fn" (list "new" "A") '("fls")) (list "lam" 'x (cons '("fls") (list "app" (cons (list "fn" (list "sum" (list "new" "A") (list "new" "B")) '("fls")) (list "var" 'f)) (cons (list "sum" (list "new" "A") (list "new" "B")) (list "or" (cons (list "new" "A") (list "var" 'x))))))))))) + + (check (empty-env) (car not_ab_imp_not_a) (cdr not_ab_imp_not_a))