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

;; proust-pred-start: moving towards predicate logic
;; Prabhakar Ragde (April 2020)

;; There isn't actually any predicate logic handled here.
;; For simplicity, we go back to the proust-imp-basic situation,
;;   where the only logical connective was ->,
;;   corresponding to the function or "arrow" type.
;; All we really do here is merge types and expressions.
;; Holes/goals are gone and will not return until we use other systems.

;; Grammar:

;; expr = (λ x => expr)             ; lambda abstraction
;;      | (expr expr)               ; function application
;;      | x                         ; variable / uninterpreted base type
;;      | (expr : expr)             ; expression annotated with type
;;      | ?                         ; hole for unwritten code (forms goal)
;;      | (expr -> expr)            ; implication / function type

;; Structures for Expr (abstract syntax tree representing 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)
(struct Type () #:transparent) ; the type of base types and arrow types

;; A Context is a (Listof (List Symbol Expr))
;; association list mapping variables to expressions.

;; Parsing.

;; 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))]
    [`(,e : ,t) (Ann (parse-expr e) (parse-expr t))]
    [`(,t1 -> ,t2) (Arrow (parse-expr t1) (parse-expr t2))]
    [`(,t1 -> ,t2 -> ,r ...) (Arrow '_ (parse-expr t1) (parse-expr `(,t2 -> ,@r)))]
    [`(,e1 ,e2 ,e3 ,r ...) (parse-expr `((,e1 ,e2) ,e3 ,@r))]
    [(? symbol? x) x] ; variable / base type
    [else (error 'parse "bad syntax: ~a\n" s)]))

;; 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))]
    [(Ann e t) (format "(~a : ~a)" (pretty-print-expr e) (pretty-print-expr t))]
    [(Arrow t1 t2) (format "(~a -> ~a)" (pretty-print-expr t1) (pretty-print-expr t2))]
    [(? symbol? x) (symbol->string x)]))

;; 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-expr (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 Expr -> 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)
       (unless (type-check ctx type (Type))
         (error 'type-check "not a type: ~a" type))
       (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 e type)
  (error 'type-check "cannot typecheck ~a as ~a in context:\n~a"
         (pretty-print-expr e) (pretty-print-expr type) (pretty-print-context ctx)))

;; type-synth : Context Expr -> Type
;; Produces type of expr in context ctx (or error if can't).

(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)])]
    [(Arrow t w)
       (type-check ctx t (Type))
       (type-check ctx w (Type))
       (Type)]
    [(? symbol? x)
       (cond
         [(assoc x ctx) => second]
         [else (Type)])])) ; note change here

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

;; Completely inadequate testing copied from proust-imp-basic

(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 => (y x))) : (A -> ((A -> B) -> B))))
              true)
(check-expect (check-proof '((λ f => (λ g => (λ x => (f (g x))))) : ((B -> C) -> ((A -> B) -> (A -> C)))))
              true)
(test)