Non-deterministic normalization-by-evaluation in Olle Fredriksson's flavor.

GluedEval.hs

{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}

{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:

  https://github.com/ollef/sixty

The main idea is that during elaboration, we need different evaluation
strategies for different tasks; here in particular we have a distinction
between top and local scope, and we want to have control over unfolding
of top-level definitions.

- For generating terms (for error displaying, serialization, metavariable
  solutions), we want to avoid unfolding as much as possible, to avoid size
  blowups.

- For conversion checking, we want to have an efficient, preferably call-by-need
  evaluator which unfolds everything.

We want evaluation to be as fast as possible, and we also want to avoid
duplicating computation between the two unfolding modes which could be shared.

The solution here is to use normalization-by-evaluation extended with
lazy non-deterministic choice in the semantic domain. We extend values with

    ... | VTop Name Spine ~Val

where Name and Spine constitute a neutral expression whose head is a top-level
definition name, and ~Val is the lazy result of evaluating the same netural
expression, but with the top definition unfolded.

Hence, when we hit VTop during processing Val-s, we can choose between
unfolding and not unfolding.

We also have to implement the semantic action of projections and eliminations
on VTop. In our case, we only have function application:

    vapp :: Val -> Val -> Val
    vapp (VLam _ t)    ~u = t u
    vapp (VLoc x sp)   ~u = VLoc x (SApp sp u)
    vapp (VTop x sp t) ~u = VTop x (SApp sp u) (vapp t u)

vapp acts on both branches of VTop. The neutral part is eagerly computed,
since the computation there is trivial, delaying it would be more costly
than just performing it. In contrast, the "vapp t u" can be arbitrarily costly,
so it is delayed.

Note that "u" is duplicated in "VTop x (SApp sp u) (vapp t u)". This means
that "u" is computed at most once regardless of which evaluation branch we
compute (of course, we can compute both too).
-}

import Data.Maybe

type Name = String

data Tm
  = Loc Name    -- local var
  | Top Name    -- top-level var
  | App Tm Tm
  | Let Name Tm Tm
  | Lam Name Tm
  deriving Show

data Spine = SNil | SApp Spine ~Val

data Val = VLam Name (Val -> Val) | VLoc Name Spine | VTop Name Spine ~Val

type TopEnv    = [(Name, Val)]
type LocalEnv  = [(Name, Val)]

eval :: TopEnv -> LocalEnv -> Tm -> Val
eval top loc = \case
  Loc x     -> fromJust $ lookup x loc
  Top x     -> VTop x SNil (fromJust $ lookup x top)
  App t u   -> vapp (eval top loc t) (eval top loc u)
  Let x t u -> eval top ((x, eval top loc t) : loc) u
  Lam x t   -> VLam x \u -> eval top ((x, u):loc) t

vapp :: Val -> Val -> Val
vapp (VLam _ t)    ~u = t u
vapp (VLoc x sp)   ~u = VLoc x (SApp sp u)
vapp (VTop x sp t) ~u = VTop x (SApp sp u) (vapp t u)

fresh :: LocalEnv -> Name -> Name
fresh env x = case lookup x env of
  Nothing -> x
  Just{}  -> fresh env (x ++ "'")

type UnfoldTop = Bool

quoteSp :: LocalEnv -> UnfoldTop -> Tm -> Spine -> Tm
quoteSp loc unf h = \case
  SNil      -> h
  SApp sp u -> App (quoteSp loc unf h sp) (quote loc unf u)

quote :: LocalEnv -> UnfoldTop -> Val -> Tm
quote loc unf = \case
  VLoc x sp   -> quoteSp loc unf (Loc x) sp
  VLam x t    -> let x' = fresh loc x
                     v  = VLoc x' SNil
                 in Lam x' (quote ((x, v):loc) unf (t v))
  VTop x sp t -> if unf then quote loc unf t
                        else quoteSp loc unf (Top x) sp

evalTop :: [(Name, Tm)] -> Tm -> Val
evalTop top t = eval topvals [] t where
  topvals = foldl (\top (x, t) -> (x, eval top [] t) : top) [] top

nfTop :: UnfoldTop -> [(Name, Tm)] -> Tm -> Tm
nfTop unf top t = quote [] unf (evalTop top t)

------------------------------------------------------------

($$) = App
infixl 8 $$

top :: [(Name, Tm)]
top = [
    ("zero", Lam "s" $ Lam "z" $ Loc "z")
  , ("suc",  Lam "n" $ Lam "s" $ Lam "z" $
        Loc "s" $$ (Loc "n" $$ Loc "s" $$ Loc "z"))
  , ("add",  Lam "a" $ Lam "b" $ Lam "s" $ Lam "z" $
        Loc "a" $$ Loc "s" $$ (Loc "b" $$ Loc "s" $$ Loc "z"))
  , ("mul",  Lam "a" $ Lam "b" $ Lam "s" $ Lam "z" $
        Loc "a" $$ (Loc "b" $$ Loc "s") $$ Loc "s" $$ Loc "z")
  , ("5", Top "suc" $$ (Top "suc" $$ (Top "suc" $$ (Top "suc" $$
           (Top "suc" $$ Top "zero")))))
  , ("10", Top "add" $$ Top "5" $$ Top "5")
  , ("100", Top "mul" $$ Top "10" $$ Top "10")
  ]

tm = Let "five" (Top "suc" $$ (Top "suc" $$ (Top "suc" $$ (Top "suc" $$
             (Top "suc" $$ Top "zero"))))) $
     Top "mul" $$ Loc "five" $$ Top "5"