#lang racket
; 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)
(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" s)]))

;; parse-type : sexp -> Type

(define (parse-type t)
  (match t
    [`(,t1 -> ,t2) (Arrow (parse-type t1) (parse-type t2))]
    [`(,t1 -> ,t2 -> ,r ...) (Arrow (parse-type t1) (parse-type `(,t2 -> ,@r)))]
    [(? symbol? X) X] 
    [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)]
    [(Ann e t) (format "(~a : ~a)" (pretty-print-expr e) (pretty-print-type t))]))

;; 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 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)))]))

;; 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)])]
    [else (if (equal? (type-synth ctx expr) type) true (cannot-check ctx expr type))]))

;; 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)))

;; 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)])]))

;; 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)))

;; Not nearly enough tests but this is a start

(require test-engine/racket-tests)

(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)