pire-0.2.5

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

Desugar

Description

desugaring of Pire's abstract syntax in terms of Bound

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 to have desugaring of 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:

>>> _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 $ 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: desugar to nested LamPA's w/ () scopes

note that some effort was made to have desugaring of 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:

>>> nopos $ parse expr "\\  y x z . x"
LamPAs [(RuntimeP,"y",Nothing),(RuntimeP,"x",Nothing),(RuntimeP,"z",Nothing)] (Scope (V (B 1)))
>>> 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 ())))))))))
>>> 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 :: Eq a => Expr a a -> Expr a a Source #

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" []))