Skip to content
Permalink
Browse files

calling extrinsically typed evaluation and then ugly printing it

  • Loading branch information...
jmchapman committed Mar 15, 2019
1 parent 0601dfa commit 303952ea86035d75e26897a80a96bda18391c505
Showing with 163 additions and 36 deletions.
  1. +89 −0 MAlonzo/Code/Scoped.hs
  2. +12 −6 Main.lagda
  3. +35 −1 Scoped.lagda
  4. +27 −29 Untyped/Term.lagda
@@ -8,6 +8,7 @@ import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
mul64, quot64, rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Nat
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Builtin
@@ -18,10 +19,12 @@ import qualified MAlonzo.Code.Data.Maybe
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.String
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.Data.Vec
import qualified MAlonzo.Code.Raw
import qualified MAlonzo.Code.Relation.Nullary

import qualified Data.Text as T
import Scoped
name2 = "Scoped.ScopedKind"
d2 = ()
@@ -332,3 +335,89 @@ d348 v0 v1 v2
(MAlonzo.Code.Data.Maybe.Base.C18
(coe (\ v4 v5 -> C108 v5) erased v3))
_ -> MAlonzo.RTE.mazUnreachableError
name408 = "Scoped.uglyWeirdFin"
d408 :: T30 -> T38 -> MAlonzo.Code.Agda.Builtin.String.T6
d408 v0 v1
= case coe v1 of
C42 -> coe (Data.Text.pack "0")
C46 v3
-> case coe v0 of
C34 v4
-> coe
MAlonzo.Code.Data.String.Base.d10 (Data.Text.pack "(S ")
(coe
MAlonzo.Code.Data.String.Base.d10 (d408 (coe v4) (coe v3))
(Data.Text.pack ")"))
_ -> MAlonzo.RTE.mazUnreachableError
C50 v3
-> case coe v0 of
C36 v4
-> coe
MAlonzo.Code.Data.String.Base.d10 (Data.Text.pack "(T ")
(coe
MAlonzo.Code.Data.String.Base.d10 (d408 (coe v4) (coe v3))
(Data.Text.pack ")"))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
name414 = "Scoped.showNat"
d414 :: Integer -> MAlonzo.Code.Agda.Builtin.String.T6
d414 = T.pack . show
name416 = "Scoped.uglyBuiltin"
d416 ::
MAlonzo.Code.Builtin.T2 -> MAlonzo.Code.Agda.Builtin.String.T6
d416 v0
= let v1 = Data.Text.pack "other" in
case coe v0 of
MAlonzo.Code.Builtin.C4 -> coe (Data.Text.pack "addInteger")
_ -> coe v1
name420 = "Scoped.ugly"
d420 :: T30 -> T76 -> MAlonzo.Code.Agda.Builtin.String.T6
d420 v0 v1
= case coe v1 of
C80 v3
-> coe
MAlonzo.Code.Data.String.Base.d10 (Data.Text.pack "(` ")
(coe
MAlonzo.Code.Data.String.Base.d10 (d408 (coe v0) (coe v3))
(Data.Text.pack ")"))
C84 v3 v4
-> coe
MAlonzo.Code.Data.String.Base.d10 (Data.Text.pack "(\923 ")
(coe
MAlonzo.Code.Data.String.Base.d10
(d420 (coe (C36 (coe v0))) (coe v4)) (Data.Text.pack ")"))
C88 v3 v4
-> coe
MAlonzo.Code.Data.String.Base.d10 (Data.Text.pack "( ")
(coe
MAlonzo.Code.Data.String.Base.d10 (d420 (coe v0) (coe v3))
(coe
MAlonzo.Code.Data.String.Base.d10 (Data.Text.pack " \183\8902 ")
(coe
MAlonzo.Code.Data.String.Base.d10 (Data.Text.pack "TYPE")
(Data.Text.pack ")"))))
C92 v3 v4
-> coe
MAlonzo.Code.Data.String.Base.d10 (Data.Text.pack "(\411 ")
(coe
MAlonzo.Code.Data.String.Base.d10
(d420 (coe (C34 (coe v0))) (coe v4)) (Data.Text.pack ")"))
C96 v3 v4
-> coe
MAlonzo.Code.Data.String.Base.d10 (Data.Text.pack "( ")
(coe
MAlonzo.Code.Data.String.Base.d10 (d420 (coe v0) (coe v3))
(coe
MAlonzo.Code.Data.String.Base.d10 (Data.Text.pack " \183 ")
(coe
MAlonzo.Code.Data.String.Base.d10 (d420 (coe v0) (coe v4))
(Data.Text.pack ")"))))
C100 v3 -> coe (Data.Text.pack "(con ")
C104 v3 -> coe (Data.Text.pack "error _")
C108 v3
-> coe
MAlonzo.Code.Data.String.Base.d10 (Data.Text.pack "(builtin ")
(coe
MAlonzo.Code.Data.String.Base.d10 (d416 (coe v3))
(Data.Text.pack ")"))
_ -> MAlonzo.RTE.mazUnreachableError
@@ -175,19 +175,25 @@ postulate
{-# COMPILE GHC readFile = \ s -> BSL.readFile (T.unpack s) #-}
{-# COMPILE GHC showTerm = T.pack . show #-}
open import Function
open import Untyped.Term
open import Untyped.Reduction
open import Scoped

open import Untyped.Term as U
import Untyped.Reduction as U
import Scoped as S
import Scoped.Reduction as S


-- untyped evaluation
utestPLC : ByteString → Maybe String
utestPLC plc = mmap (U.ugly ∘ (λ (t : 0 ⊢) → proj₁ (U.run t 100)) ∘ erase⊢) (mbind (deBruijnifyTm nil) (mmap convP (parse plc)))

testPLC : ByteString → Maybe String
testPLC plc = mmap (ugly ∘ (λ (t : 0 ⊢) → proj₁ (run t 100)) ∘ erase⊢) (mbind (deBruijnifyTm nil) (mmap convP (parse plc)))
-- extrinsically typed evaluation
stestPLC : ByteString → Maybe String
stestPLC plc = mmap (S.ugly ∘ (λ (t : ScopedTm Z) → proj₁ (S.run t 100))) (mbind (deBruijnifyTm nil) (mmap convP (parse plc)))

testFile : String → IO String
testFile fn = do
t ← readFile fn
return (maybe id "blerk" (testPLC t))
return (maybe id "blerk" (utestPLC t))

{-# FOREIGN GHC import System.Environment #-}

@@ -79,7 +79,7 @@ deBruijnifyK * = *
deBruijnifyK (K ⇒ J) = deBruijnifyK K ⇒ deBruijnifyK J
deBruijnifyK # = #

open import Data.Vec hiding (_>>=_; map)
open import Data.Vec hiding (_>>=_; map; _++_)
open import Data.Maybe
open import Data.String
open import Relation.Nullary
@@ -158,3 +158,37 @@ deBruijnifyTm g (con t) = map con (checkSize t)
deBruijnifyTm g (error A) = map error (deBruijnifyTy ∥ g ∥Vec A)
deBruijnifyTm g (builtin b) = just (builtin b)
\end{code}

\begin{code}
open import Data.String

uglyWeirdFin : ∀{n} → WeirdFin n → String
uglyWeirdFin Z = "0"
uglyWeirdFin (T x) = "(T " ++ uglyWeirdFin x ++ ")"
uglyWeirdFin (S x) = "(S " ++ uglyWeirdFin x ++ ")"

{-
uglyTermCon : TermCon → String
uglyTermCon (integer x) = "(integer " ++ Data.Integer.show x ++ ")"
uglyTermCon (bytestring x) = "bytestring"
uglyTermCon size = "size"
-}
postulate showNat : ℕ → String

{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC showNat = T.pack . show #-}

uglyBuiltin : Builtin → String
uglyBuiltin addInteger = "addInteger"
uglyBuiltin _ = "other"
ugly : ∀{n} → ScopedTm n → String
ugly (` x) = "(` " ++ uglyWeirdFin x ++ ")"
ugly (ƛ _ t) = "(ƛ " ++ ugly t ++ ")"
ugly (t · u) = "( " ++ ugly t ++ " · " ++ ugly u ++ ")"
ugly (Λ _ t) = "(Λ " ++ ugly t ++ ")"
ugly (t ·⋆ A) = "( " ++ ugly t ++ " ·⋆ " ++ "TYPE" ++ ")"

ugly (con c) = "(con " -- ++ uglyTermCon c ++ ")"
ugly (builtin b) = "(builtin " ++ uglyBuiltin b ++ ")"
ugly (error _) = "error _"
\end{code}
@@ -76,26 +76,27 @@ eraseTel {As = x ∷ As} (t ,, tel) = erase t ∷ eraseTel tel

-- conversion for scoped to untyped

open import Scoped
import Scoped as S

eraseℕ : Weirdℕ → ℕ
eraseℕ Z = zero
eraseℕ (S n) = suc (eraseℕ n)
eraseℕ (T n) = eraseℕ n
eraseℕ : S.Weirdℕ → ℕ
eraseℕ S.Z = zero
eraseℕ (S.S n) = suc (eraseℕ n)
eraseℕ (S.T n) = eraseℕ n

eraseFin : ∀{n} → WeirdFin n → Fin (eraseℕ n)
eraseFin Z = zero
eraseFin (S x) = suc (eraseFin x)
eraseFin (T x) = eraseFin x
eraseFin : ∀{n} → S.WeirdFin n → Fin (eraseℕ n)
eraseFin S.Z = zero
eraseFin (S.S x) = suc (eraseFin x)
eraseFin (S.T x) = eraseFin x

eraseCon : SizedTermCon → TermCon
eraseCon (integer s i x) = integer i
eraseCon (bytestring s b x) = bytestring b
eraseCon (size x) = size
eraseCon (string x) = size -- this is wrong
eraseCon : S.SizedTermCon → TermCon
eraseCon (S.integer s i x) = integer i
eraseCon (S.bytestring s b x) = bytestring b
eraseCon (S.size x) = size
eraseCon (S.string x) = size -- this is wrong

open import Data.Sum

-- should do this when de Bruijnifying so it can be shared
builtinMatcher : ∀{n} → n ⊢ → (Builtin × List (n ⊢)) ⊎ n ⊢
builtinMatcher (` x) = inj₂ (` x)
builtinMatcher (ƛ t) = inj₂ (ƛ t)
@@ -115,17 +116,17 @@ builtinEater b ts u | Dec.yes p = builtin b (ts Data.List.++ [ u ])
builtinEater b ts u | Dec.no ¬p = builtin b ts · u


erase⊢ : ∀{n} → ScopedTm n → eraseℕ n ⊢
erase⊢ (` x) = ` (eraseFin x)
erase⊢ (Λ K t) = erase⊢ t
erase⊢ (t ·⋆ A) = erase⊢ t
erase⊢ (ƛ A t) = ƛ (erase⊢ t)
erase⊢ (t · u) with builtinMatcher (erase⊢ t)
erase⊢ (t · u) | inj₁ (b ,, ts) = builtinEater b ts (erase⊢ u)
erase⊢ (t · u) | inj₂ t' = t' · erase⊢ u
erase⊢ (con c) = con (eraseCon c)
erase⊢ (error A) = error
erase⊢ (builtin b) = builtin b []
erase⊢ : ∀{n} → S.ScopedTm n → eraseℕ n ⊢
erase⊢ (S.` x) = ` (eraseFin x)
erase⊢ (S.Λ K t) = erase⊢ t
erase⊢ (t S.·⋆ A) = erase⊢ t
erase⊢ (S.ƛ A t) = ƛ (erase⊢ t)
erase⊢ (t S.· u) with builtinMatcher (erase⊢ t)
erase⊢ (t S.· u) | inj₁ (b ,, ts) = builtinEater b ts (erase⊢ u)
erase⊢ (t S.· u) | inj₂ t' = t' · erase⊢ u
erase⊢ (S.con c) = con (eraseCon c)
erase⊢ (S.error A) = error
erase⊢ (S.builtin b) = builtin b []

\end{code}

@@ -142,10 +143,7 @@ uglyTermCon (integer x) = "(integer " ++ Data.Integer.show x ++ ")"
uglyTermCon (bytestring x) = "bytestring"
uglyTermCon size = "size"

postulate showNat : ℕ → String

{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC showNat = T.pack . show #-}

uglyBuiltin : Builtin → String
uglyBuiltin addInteger = "addInteger"
@@ -155,6 +153,6 @@ ugly (` x) = "(` " ++ uglyFin x ++ ")"
ugly (ƛ t) = "(ƛ " ++ ugly t ++ ")"
ugly (t · u) = "( " ++ ugly t ++ " · " ++ ugly u ++ ")"
ugly (con c) = "(con " ++ uglyTermCon c ++ ")"
ugly (builtin b ts) = "(builtin " ++ uglyBuiltin b ++ " " ++ showNat (Data.List.length ts) ++ ")"
ugly (builtin b ts) = "(builtin " ++ uglyBuiltin b ++ " " ++ S.showNat (Data.List.length ts) ++ ")"
ugly error = "error"
\end{code}

0 comments on commit 303952e

Please sign in to comment.
You can’t perform that action at this time.