readback.rkt

#lang typed/racket
(provide (all-defined-out))
(require "ast.rkt"
         "eval.rkt")

(: readback-value : Value -> NormalExpr)
(define (readback-value v)
  (match v
    [(V:Lambda f) (NE:Lambda (readback-value (Inst f (genV))))]
    [(V:Pair u v) (NE:Pair (readback-value u) (readback-value v))]
    [(V:Constructor c v) (NE:Constructor c (readback-value v))]
    [(V:Unit) (NE:Unit)]
    [(V:One) (NE:One)]
    [(V:Type level) (NE:Type level)]
    [(V:Pi t g) (NE:Pi (readback-value t) (readback-value (Inst g (genV))))]
    [(V:Sigma t g) (NE:Sigma (readback-value t) (readback-value (Inst g (genV))))]
    [(V:Sum c) (NE:Sum (readback-casetree c))]
    [(V:Neu l) (NE:Neu (readback-neu l))]
    [else (error 'unreachable)]))

(: readback-neu : Neutral -> NormalNeutral)
(define (readback-neu n)
  (match n))

(: readback-casetree : CaseTree -> NormalCaseTree)
(define (readback-casetree tele)
  (for/hash : NormalCaseTree ([(name case) (in-hash tele)])
    (values name
            (readback-case case))))

(: readback-case : Case -> NormalCase)
(define (readback-case case)
  (GCase (if (Value? (GCase-expr case))
             (readback-value (GCase-expr case))
             (GCase-expr case))
         (readback-telescope (GCase-context case))))

(: readback-telescope : (GTelescope Value) -> (GTelescope NormalExpr))
(define (readback-telescope tele)
  (match tele
    [(Tele:Nil) (Tele:Nil)]
    [(Tele:UpDec ctx decl)
     (Tele:UpDec (readback-telescope ctx) decl)]
    [(Tele:UpVar ctx pat val)
     (Tele:UpVar (readback-telescope ctx)
                 pat
                 (readback-value (cast val Value)))]
    [else (error 'unreachable)]))