Skip to content


Browse files Browse the repository at this point in the history
Better unquote macro.
It's in its own file for now. Also fixes a bug preventing eliminators
being used at multiple types.
  • Loading branch information
ChickenProp committed Mar 10, 2021
1 parent b42f6f1 commit 6231daa
Show file tree
Hide file tree
Showing 3 changed files with 200 additions and 4 deletions.
4 changes: 2 additions & 2 deletions app/Main.hs
Expand Up @@ -6,11 +6,11 @@ import Control.Monad.Except (liftEither, runExceptT)
import qualified Data.Text.IO as Text
import qualified GHC.IO.Encoding as Encoding
import qualified Options.Applicative as O
import Shower (printer)

import App
import Env
import Eval
import Gist
import Syntax

data CmdLine = CmdLine
Expand Down Expand Up @@ -68,7 +68,7 @@ doCmdLine :: CmdLine -> IO ()
doCmdLine (CmdLine {..}) = runExceptT go >>= \case
Left err -> Text.putStrLn err
Right Nothing -> return ()
Right (Just res) -> printer res
Right (Just res) -> print (prettyGist res)
go = do
(fName, src) <- case program of
Expand Down
194 changes: 194 additions & 0 deletions examples/quote-2.hth
@@ -0,0 +1,194 @@
(def (: << (-> (-> $b $c) (-> (-> $a $b) (-> $a $c))))
(λ (f g x) (f (g x))))

(def (: ++ (-> (List $a) (-> (List $a) (List $a))))
(λ (a b)
(elim-List b (λ (a1 as) (Cons a1 (++ as b))) a)))

(def (: +:map (-> (-> $a $b) (-> (+ $x $a) (+ $x $b))))
(λ f (elim-+ (λ x (Left x)) (λ a (Right (f a))))))

(def (: +:map-m (-> (-> $a (+ $b $c)) (-> (List $a) (+ $b (List $c)))))
(λ f
(elim-List (Right Nil)
(λ (hd tl)
# This ugly bit is just `(:) <$> f hd <*> +:map-m f tl`
(let ((f-hd (f hd)))
(if~ f-hd (Left $x)
(if~ f-hd (Right $x)
(let ((recurs (+:map-m f tl)))
(if~ recurs (Left $y)
(if~ recurs (Right $y)
(Right (Cons x y))
(error! "impossible"))))
(error! "impossible"))))))))

(def (: List:map (-> (-> $a $b) (-> (List $a) (List $b))))
(λ f
(elim-List Nil (λ (hd tl) (Cons (f hd) (List:map f tl))))))

(def (: List:foldr (-> (-> $a (-> $b $b))
(-> $b
(-> (List $a)
(λ (f init)
(elim-List init (λ (hd tl) (f hd (List:foldr f init tl))))))

(type (Maybe $a) Nothing (Just $a))
(def (: Maybe:map (-> (-> $a $b) (-> (Maybe $a) (Maybe $b))))
(λ f (elim-Maybe Nothing (<< Just f))))

(type Bool False True)
(defmacro if
(λ ts
(if~ ts (Cons $else Nil)
(if~ ts (Cons $cond (Cons $then $rest))
(STTree (» Cons (STBare "if~")
(STBare "True")
(STTree (Cons (STBare "if") rest))
(error! "`if` must have an odd number of args")))))

(def (: all (-> (-> $a Bool) (-> (List $a) Bool)))
(λ f
(elim-List True
(λ (hd tl) (if (f hd) (all f tl) False)))))

(def (: STTree-2 (-> SyntaxTree (-> SyntaxTree SyntaxTree)))
(λ (a b) (STTree (» Cons a b Nil))))
(def (: STTree-3 (-> SyntaxTree (-> SyntaxTree (-> SyntaxTree SyntaxTree))))
(λ (a b c) (STTree (» Cons a b c Nil))))

(def (: quote-fun (-> SyntaxTree SyntaxTree))
((q-bare (λ x (STTree-2 (STBare "STBare") (STString x))))
(q-string (λ x (STTree-2 (STBare "STString") (STString x))))
(q-float (λ x (STTree-2 (STBare "STFloat") (STFloat x))))
((: q-tree (-> (List SyntaxTree) SyntaxTree))
(λ x
(STTree-2 (STBare "STTree")
(List:foldr (λ (hd tl)
(STTree-3 (STBare "Cons") hd tl))
(STBare "Nil")
(List:map quote-fun x))))))
(elim-SyntaxTree q-bare q-float q-string q-tree)))

(defmacro quote
(λ ts
(if~ ts (Cons $t Nil)
(quote-fun t)
(error! "Can only quote one thing"))))

(type QQTree
(QQLeaf SyntaxTree)
(QQ-↑ SyntaxTree)
(QQ-↑↑ SyntaxTree)
(QQNode (List QQTree)))

(def (: parse-QQTree (-> SyntaxTree (+ String QQTree)))
(letrec (((: immediate-leaves (-> (List QQTree) (Maybe (List SyntaxTree))))
(Just Nil)
(λ (hd tl)
(if~ hd (QQLeaf $t)
(Maybe:map (Cons t) (immediate-leaves tl))
((: build-tree (-> (List QQTree) QQTree))
(λ qs (elim-Maybe (QQNode qs)
(<< QQLeaf STTree)
(immediate-leaves qs)))))
(λ t
(if~ t (STTree $tree)
(if~ tree (Cons (STBare "↑") $rest)
(if~ rest (Cons $arg Nil)
(Right (QQ-↑ arg))
(Left "↑ given more than one arg"))
(if~ tree (Cons (STBare "↑↑") $rest)
(if~ rest (Cons $arg Nil)
(Right (QQ-↑↑ arg))
(Left "↑↑ given more than one arg"))
(+:map build-tree (+:map-m parse-QQTree tree))))
(Right (QQLeaf t))))))

(def (: unQQ-root (-> QQTree (+ String SyntaxTree)))
(<< Right quote-fun)
(λ _ (Left "Cannot unQQ a ↑↑ at the root"))
(λ qs
(λ ts
(Right (STTree-2 (quote STTree)
(List:foldr (λ (hd tl)
(STTree-3 (quote ++) hd tl))
(quote Nil)
(+:map-m unQQ-nested qs)))))

(def (: unQQ-nested (-> QQTree (+ String SyntaxTree)))
(let ((st-list1 (λ x (STTree (» Cons (quote Cons) x (quote Nil) Nil)))))
(» << Right st-list1 quote-fun)
(<< Right st-list1)
(λ qs
(λ ts
(Right (st-list1 (STTree-2 (quote STTree)
(List:foldr (λ (hd tl)
(STTree-3 (quote ++) hd tl))
(quote Nil)
(+:map-m unQQ-nested qs))))))

(def (: qq-fun (-> SyntaxTree (+ String SyntaxTree)))
(λ t (elim-+ Left unQQ-root (parse-QQTree t))))

(defmacro qq
(λ ts
(if~ ts (Cons $t Nil)
(elim-+ error! (λ x x) (qq-fun t))
(error! "Can only qq one thing"))))

(defmacro list
(letrec ((go (elim-List
(quote Nil)
(λ (hd tl)
(qq (Cons (↑ hd) (↑ (go tl))))))))

(defmacro if-qq
(λ ts
(if~ ts (Cons $else Nil)
(if~ ts (Cons $cond (Cons $then $rest))
(qq (if~ (↑ cond) True (↑ then) (if-qq (↑↑ rest))))
(error! "`if` must have an odd number of args")))))

(list 1 (if-qq False 2 True 3 False 4 5) 3)
6 changes: 4 additions & 2 deletions src/Env.hs
Expand Up @@ -177,8 +177,10 @@ declareTypeEliminator (TypeDecl' { tdName, tdVars, tdConstructors }) env = do
typeElimName (teType, typeElimVal) (feVars env)
return env { feVars = newVars }
resultTVar :: TVar Tc
resultTVar = TV HType "%a"
resultType :: MType Tc
resultType = TVar (TV HType "%a")
resultType = TVar resultTVar

valKind = foldr (\_ a -> HType :*-> a) HType tdVars
allVars = TV HType <$> tdVars
Expand All @@ -195,7 +197,7 @@ declareTypeEliminator (TypeDecl' { tdName, tdVars, tdConstructors }) env = do
typeElimType = do
mt <- foldr (+->) (valType +-> resultType)
<$> mapM (conElimType . snd) tdConstructors
return $ Forall allVars mt
return $ Forall (resultTVar : allVars) mt

typeElimName :: Name
typeElimName = "elim-" <> tdName
Expand Down

0 comments on commit 6231daa

Please sign in to comment.