learning lcai in racket

learning.rkt

#lang racket

(require test-engine/racket-tests)

; file contains Unicode characters - download rather than cut/paste from browser

;; proust-prop-imp-basic: minimal proof assistant for implicational fragment of propositional logic
;; Prabhakar Ragde (April 2020)

;; Can only check full proof terms, no incremental interactive building here

;; Grammar:

;; expr = (λ x => expr)             ; lambda abstraction
;;      | (expr expr)               ; function application
;;      | x                         ; variable
;;      | (expr : type)             ; annotated expression

;; type = X
;;      | (type -> type)            ; implication / function

;; Structures for Expr (abstract syntax tree representing proof terms)

(struct Lam (var body) #:transparent) ;; transparent makes every field public
(struct App (rator rand) #:transparent)
(struct Ann (expr type) #:transparent)

;; Structures for Type (abstract syntax tree representing types)

(struct Arrow (domain range) #:transparent)

;; A Context is a (Listof (List Symbol Type))
;; (Association list mapping propositional variables to types.)

;; Parsing
;; All very straightforward, could write a macro
;; that operates on a grammar DSL, but haven't

;; parse-expr : sexp -> Expr

(define (parse-expr s)
  (match s
    [`(λ ,(? symbol? x) => ,e) (Lam x (parse-expr e))]
    [`(,e1 ,e2) (App (parse-expr e1) (parse-expr e2))]
    [(? symbol? x) x]
    [`(,e : ,t) (Ann (parse-expr e) (parse-type t))]
    [`(,e1 ,e2 ,e3 ,r ...) (parse-expr `((,e1 ,e2) ,e3 ,@r))]
    [else (error 'parse "bad syntax: ~a\n" s)]))

;; parse-type : sexp -> Type

(define (parse-type t)
  (match t
    [`(,t1 -> ,t2) (Arrow (parse-type t1) (parse-type t2))]
    [(? symbol? X) X]
    [`(,t1 -> ,t2 -> ,r ...) (Arrow (parse-type t1) (parse-type `(,t2 -> ,@r)))]
    [else (error 'parse "bad syntax: ~a\n" t)]))

;; Unparsing, that is, pretty-printing

;; pretty-print-expr : Expr -> String

(define (pretty-print-expr e)
  (match e
    [(Lam x b) (format "(λ ~a => ~a)" x (pretty-print-expr b))]
    [(App e1 e2) (format "(~a ~a)" (pretty-print-expr e1) (pretty-print-expr e2))]
    [(? symbol? x) (format "~a" x)]
    ['? (Hole #f)] 
    [(Ann e t) (format "(~a : ~a)" (pretty-print-expr e) (pretty-print-type t))]
    [(Hole n) (format "?~a" n)]))

;; pretty-print-type : Type -> String

(define (pretty-print-type t)
  (match t
    [(Arrow t1 t2) (format "(~a -> ~a)"  (pretty-print-type t1) (pretty-print-type t2))]
    [else (symbol->string t)]))

;; pretty-print-context : Context -> String

(define (pretty-print-context ctx)
  (cond
    [(empty? ctx) ""]
    [else (string-append (format "\n~a : ~a" (first (first ctx)) (pretty-print-type (second (first ctx))))
                         (pretty-print-context (rest ctx)))]))

;; cannot-check: Context Expr Type -> void
;; Prints generic error message for type-check
;; Error messages can be improved by replacing uses of this with something more specific

(define (cannot-check ctx expr type)
  (error 'type-check "cannot typecheck ~a as ~a in context:\n~a"
         (pretty-print-expr expr) (pretty-print-type type) (pretty-print-context ctx)))

;; cannot-synth: Context Expr -> void
;; Prints generic error message for type-synth
;; Again, can improve things by being more specific at use sites

(define (cannot-synth ctx expr)
  (error 'type-synth "cannot synthesize type of ~a in context:\n~a"
         (pretty-print-expr expr) (pretty-print-context ctx)))

;; This is the heart of the verifier.
;; type-check and type-synth are mutually-recursive functions that
;;   check an expression has a type in a context, and
;;   synthesize the type of an expression in a context, respectively
;; They implement bidirectional type checking.

;; type-check : Context Expr Type -> boolean
;; produces true if expr has type t in context ctx (or error if not)

(define (type-check ctx expr type)
  (match expr
    [(Lam x t)
       (match type
         [(Arrow tt tw) (type-check (cons `(,x ,tt) ctx) t tw)]
         [else (cannot-check ctx expr type)])]
    [(Hole n) (when refining (hash-set! goal-table n (list type ctx))) true]
    [else (if (equal? (type-synth ctx expr) type) true (cannot-check ctx expr type))]))

;; type-synth : Context Expr -> Type
;; Produces type of expr in context ctx (or error if can't)
;; All failing cases spelled out rather than put into "else" at end

(define (type-synth ctx expr)
  (match expr
    [(Lam _ _) (cannot-synth ctx expr)]
    [(Ann e t) (type-check ctx e t) t]
    [(App f a)
       (define tf (type-synth ctx f))
        (match tf
          [(Arrow tt tw) #:when (type-check ctx a tt) tw]
          [else (cannot-synth ctx expr)])]
    [(? symbol? x)
       (cond
         [(assoc x ctx) => second]
         [else (cannot-synth ctx expr)])]))

(struct Hole (num) #:transparent)

(define current-expr #f)
(define goal-table (make-hash))
(define hole-ctr 0)
(define (use-hole-ctr) (begin0 hole-ctr (set! hole-ctr (add1 hole-ctr))))
(define refining #f)

;(set-task! '(A -> B -> A))

(define (set-task! s)
  (define t (parse-type s))
  (set! goal-table (make-hash))
  (set! hole-ctr 1)
  (printf "Type := ~a\n" (format (pretty-print-type t)))
  (set! current-expr (Ann (Hole 0) t))
  (hash-set! goal-table 0 (list t empty))
  (printf "Task is now\n")
  (print-task))

(define (print-task) (printf "~a\n" (pretty-print-expr current-expr)))

; refine : Nat sexpt -> void

(define (refine n s)
  (match-define (list t ctx)
    (hash-ref goal-table n (lambda () (error 'refine "no goal numbered ~a" n))))
  (define e (parse-expr s))
  (printf "Expression := ~a\n" (format (pretty-print-expr e)))
  (printf "Context := ~a\n" (format (pretty-print-context ctx)))
  (type-check ctx e t)
  (define en (number-new-holes e))
  (set! refining #t)
  (type-check ctx en t)
  (set! refining #f)
  (hash-remove! goal-table n)
  (set! current-expr (replace-goal-with n en current-expr))
  (define ngoals (hash-count goal-table))
  (printf "Task with ~a is now\n" (format "~a goal~a" ngoals (if (= ngoals 1) "" "s")))
  (print-task)
  (print-goal))

(define print-goal
  (case-lambda
    [() (hash-for-each goal-table (lambda (n g) (print-goal n)))]
    [(n) (match-define (list t ctx)
           (hash-ref goal-table n (lambda () (error 'refine "no goal of that number"))))
         (printf "Goal ~a has type ~a\n" n (pretty-print-type t))
         (unless (empty? ctx)
           (printf "in context~a\n" (pretty-print-context ctx)))]))

(define (replace-goal-with n repl e)
  (match e
    [(Lam x b) (Lam x (replace-goal-with n repl b))]
    [(App e1 e2) (App (replace-goal-with n repl e1) (replace-goal-with n repl e2))]
    [(? symbol? x) x]
    [(Ann e t) (Ann (replace-goal-with n repl e) t)]
    [(Hole m) (if (= m n) repl (Hole m))]))



(define (number-new-holes e)
  (match e
    [(Lam x b) (Lam x (number-new-holes b))]
    [(App e1 e2) (App (number-new-holes e1) (number-new-holes e2))]
    [(? symbol? x) x]
    [(Ann e t) (Ann (number-new-holes e) t)]
    [(Hole m) (if m (Hole m) (Hole (use-hole-ctr)))]))

(define (check-proof p) (type-synth empty (parse-expr p)) true)

(check-expect (check-proof '((λ x => (λ y => x)) : (A -> (B -> A))))
              true)
(check-expect (check-proof '((λ x => (λ y => x)) : (A -> B -> A)))
              true)
(check-expect (check-proof '((λ x => (λ y => (y x))) : (A -> ((A -> B) -> B))))
              true)
(check-expect (check-proof '((λ x => (λ y => (y x))) : (A -> (A -> B) -> B)))
              true)
(test)