Use finite field elements instead of strings for better perf Actually I have no idea if this actually improves perf or not...

Changes

2 changed files (+29/-29)

• Main.lean
  • @@ -57,12 +57,12 @@ inductive Term
    | fls_elim : Typ × Term → Term def Typ.toString : Typ → String - | new α => s!"(list \"new\" \"{α}\")" - | fn α β => s!"(list \"fn\" {α.toString} {β.toString})" - | prod α β => s!"(list \"prod\" {α.toString} {β.toString})" - | sum α β => s!"(list \"sum\" {α.toString} {β.toString})" - | nat => s!"'(\"nat\")" - | fls => s!"'(\"fls\")" + | new α => s!"(list 0n \"{α}\")" + | fn α β => s!"(list 1n {α.toString} {β.toString})" + | prod α β => s!"(list 2n {α.toString} {β.toString})" + | sum α β => s!"(list 3n {α.toString} {β.toString})" + | nat => s!"'(4n)" + | fls => s!"'(5n)" instance : ToString Typ := ⟨Typ.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!"(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!"(list \"and1\" {toString x})" - | .and2 y => s!"(list \"and2\" {toString y})" - | .or z => s!"(list \"or\" {toString z})" - | .zero => s!"'(\"zero\")" - | .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!"(list \"fls_elim\" {toString x})" + | .var x => s!"(list 10n '{x})" + | .lam x b => s!"(list 11n '{x} {toString b})" + | .app f x => s!"(list 12n {toString f} {toString x})" + | .and x y => s!"(list 13n {toString x} {toString y})" + | .and1 x => s!"(list 14n {toString x})" + | .and2 y => s!"(list 15n {toString y})" + | .or z => s!"(list 16n {toString z})" + | .zero => s!"'(17n)" + | .succ x => s!"(list 18n {toString x})" + | .nat_elim τ a b c => s!"(list 19n {τ} {toString a} {toString b} {toString c})" + | .fls_elim x => s!"(list 20n {toString x})" end instance : ToString (Typ × Term) := ⟨toString⟩
• main.lurk
  • @@ -22,46 +22,46 @@
    ;; NEED defrec instead of def for recursive functions ;; TODO: Implement nats !(defrec check (lambda (env typ term) - (if (eq (car term) "var") + (if (= (car term) 10n) (eq typ (eval (arg1 term) env)) - (if (and (eq (car typ) "fn") (eq (car term) "lam")) + (if (and (= (car typ) 1n) (= (car term) 11n)) (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")) + (if (and (= (car term) 12n) (= (car (arg1a term)) 1n)) (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")) + (if (and (= (car typ) 2n) (= (car term) 13n)) (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")) + (if (and (= (car term) 14n) (= (car (arg1a term)) 2n)) (and (eq (arg1 (arg1a term)) typ) (check env (arg1a term) (arg1b term))) - (if (and (eq (car term) "and2") (eq (car (arg1a term)) "prod")) + (if (and (= (car term) 15n) (= (car (arg1a term)) 2n)) (and (eq (arg2 (arg1a term)) typ) (check env (arg1a term) (arg1b term))) - (if (and (eq (car typ) "sum") (eq (car term) "or")) + (if (and (= (car typ) 3n) (= (car term) 16n)) (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)))) + (if (and (= (car term) 20n) (eq (car (arg1a term)))) t nil)))))))))) ; Autogenerated by Main.lean - !(def a_imp_a (cons (list "fn" (list "new" "A") (list "new" "A")) (list "lam" 'a (cons (list "new" "A") (list "var" 'a))))) + !(def a_imp_a (cons (list 1n (list 0n "A") (list 0n "A")) (list 11n 'a (cons (list 0n "A") (list 10n 'a))))) (check (empty-env) (car a_imp_a) (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))))))))) + !(def a_imp_b_imp_ba (cons (list 1n (list 0n "A") (list 1n (list 0n "B") (list 2n (list 0n "B") (list 0n "A")))) (list 11n 'a (cons (list 1n (list 0n "B") (list 2n (list 0n "B") (list 0n "A"))) (list 11n 'b (cons (list 2n (list 0n "B") (list 0n "A")) (list 13n (cons (list 0n "B") (list 10n 'b)) (cons (list 0n "A") (list 10n '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))))))))) + !(def ab_imp_ba (cons (list 1n (list 2n (list 0n "A") (list 0n "B")) (list 2n (list 0n "B") (list 0n "A"))) (list 11n 'ab (cons (list 2n (list 0n "B") (list 0n "A")) (list 13n (cons (list 0n "B") (list 15n (cons (list 2n (list 0n "A") (list 0n "B")) (list 10n 'ab)))) (cons (list 0n "A") (list 14n (cons (list 2n (list 0n "A") (list 0n "B")) (list 10n '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))))))))))) + !(def not_ab_imp_not_a (cons (list 1n (list 1n (list 3n (list 0n "A") (list 0n "B")) '(5n)) (list 1n (list 0n "A") '(5n))) (list 11n 'f (cons (list 1n (list 0n "A") '(5n)) (list 11n 'x (cons '(5n) (list 12n (cons (list 1n (list 3n (list 0n "A") (list 0n "B")) '(5n)) (list 10n 'f)) (cons (list 3n (list 0n "A") (list 0n "B")) (list 16n (cons (list 0n "A") (list 10n 'x))))))))))) (check (empty-env) (car not_ab_imp_not_a) (cdr not_ab_imp_not_a))