pire-0.2.5

Copyright(c) Andreas Reuleaux 2015-2018
LicenseBSD2
MaintainerAndreas Reuleaux <rx@a-rx.info>
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Desugar

Description

desugaring

Synopsis

Documentation

_desugar :: Expr t a -> Expr t a Source #

_desugar: desugar to nested (single binder) LamPAs w/ Int scopes

note that some effort was made for desugaring to be of (general) type Expr t a -> Expr t a: had we used Bound's instantiate, we would have desugaring of type Expr a a -> Expr a a.

these should be the same:

>>> _desugar $ nopos $ parse expr "\\  y . \\ x . x"
LamPAs [(RuntimeP,"y",Nothing)] (Scope (LamPAs [(RuntimeP,"x",Nothing)] (Scope (V (B 0)))))
>>> _desugar $ nopos $ parse expr "\\  y x . x"
LamPAs [(RuntimeP,"y",Nothing)] (Scope (LamPAs [(RuntimeP,"x",Nothing)] (Scope (V (B 0)))))

likewise, more complicated:

>>> ppr $ _desugar $ nopos $ parse expr "\\  y . \\x . \\ z . x"
LamPAs [(RuntimeP,"y",Nothing)]
       (Scope (LamPAs [(RuntimeP,"x",Nothing)]
                      (Scope (LamPAs [(RuntimeP,"z",Nothing)]
                                     (Scope (V (F (V (B 0)))))))))
>>> ppr $ _desugar $ nopos $ parse expr "\\  y x z . x"
LamPAs [(RuntimeP,"y",Nothing)]
       (Scope (LamPAs [(RuntimeP,"x",Nothing)]
                      (Scope (LamPAs [(RuntimeP,"z",Nothing)]
                                     (Scope (V (F (V (B 0)))))))))

desugar :: Expr t a -> Expr t a Source #

desugar to nested LamPA's w/ unit scopes (bound vars as ())

note that some effort was made for desugaring to be of (general) type Expr t a -> Expr t a: had we used Bound's instantiate, we would have desugaring of type Expr a a -> Expr a a.

wo/ desugaring:

>>> nopos $ parse expr "\\  y x . x"
LamPAs [(RuntimeP,"y",Nothing),(RuntimeP,"x",Nothing)] (Scope (V (B 1)))

now w/ desugaring, these should be the same:

>>> desugar $ nopos $ parse expr "\\  y . \\ x . x"
LamPA (RuntimeP,"y",Nothing) (Scope (LamPA (RuntimeP,"x",Nothing) (Scope (V (B ())))))
>>> desugar $ nopos $ parse expr "\\  y x . x"
LamPA (RuntimeP,"y",Nothing) (Scope (LamPA (RuntimeP,"x",Nothing) (Scope (V (B ())))))

likewise, more complicated:

>>> ppr $ nopos $ parse expr "\\  y x z . x"
LamPAs [(RuntimeP,"y",Nothing),(RuntimeP,"x",Nothing),(RuntimeP,"z",Nothing)]
       (Scope (V (B 1)))
>>> ppr $ desugar $ nopos $ parse expr "\\  y . \\x . \\ z . x"
LamPA (RuntimeP,"y",Nothing)
      (Scope (LamPA (RuntimeP,"x",Nothing)
                    (Scope (LamPA (RuntimeP,"z",Nothing)
                                  (Scope (V (F (V (B ())))))))))
>>> ppr $ desugar $ nopos $ parse expr "\\  y x z . x"
LamPA (RuntimeP,"y",Nothing)
      (Scope (LamPA (RuntimeP,"x",Nothing)
                    (Scope (LamPA (RuntimeP,"z",Nothing)
                                  (Scope (V (F (V (B ())))))))))

_naive :: Eq a => Expr a a -> Expr a a Source #

naive desugaring to nested (single binder) LamPAs w/ Int scopes (instantiating scopes)

naive :: Eq a => Expr a a -> Expr a a Source #

naive desugaring to nested LamPAs w/ unit scopes (instantiating scopes)

desugarNum :: (IsString t, IsString a) => Expr t a -> Expr t a Source #

desugar natural numbers

>>> nopos $ parse expr "2"
Nat 2
>>> desugarNum $ nopos $ parse expr "2"
DCon "Succ" [Arg RuntimeP (DCon "Succ" [Arg RuntimeP (DCon "Zero" [] (Just (TCon "Nat" [])))] (Just (TCon "Nat" [])))] (Just (TCon "Nat" []))