mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-25 09:17:27 +03:00
Merge pull request #27 from unisonweb/topic/views
Support for document-formatted operators (DFOs)
This commit is contained in:
commit
451e777ee8
@ -217,6 +217,6 @@ prefixes s = Metadata Metadata.Term
|
||||
Nothing
|
||||
main :: IO ()
|
||||
main = do
|
||||
store <- Store.store "store" :: IO (Store IO (Symbol.Symbol (Maybe ())))
|
||||
store <- Store.store "store" :: IO (Store IO (Symbol.Symbol ()))
|
||||
node <- makeNode store
|
||||
S.server 8080 node
|
||||
|
@ -49,6 +49,13 @@ isFreeIn v t = Set.member v (freeVars t)
|
||||
annotate :: a -> Term f v a -> Term f v a
|
||||
annotate a (Term fvs _ out) = Term fvs a out
|
||||
|
||||
vmap :: (Functor f, Foldable f, Ord v2) => (v -> v2) -> Term f v a -> Term f v2 a
|
||||
vmap f (Term _ a out) = case out of
|
||||
Var v -> annotatedVar a (f v)
|
||||
Tm fa -> tm' a (fmap (vmap f) fa)
|
||||
Cycle r -> cycle' a (vmap f r)
|
||||
Abs v body -> abs' a (f v) (vmap f body)
|
||||
|
||||
-- | Modifies the annotations in this tree
|
||||
instance Functor f => Functor (Term f v) where
|
||||
fmap f (Term fvs a sub) = Term fvs (f a) (fmap (fmap f) sub)
|
||||
|
@ -9,16 +9,20 @@
|
||||
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE DeriveFunctor #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
module Unison.Doc where
|
||||
|
||||
import Control.Comonad.Cofree (Cofree(..)) -- (:<)
|
||||
import Control.Comonad.Cofree (Cofree(..), unwrap) -- (:<)
|
||||
import Control.Comonad (extract)
|
||||
import Control.Monad.State.Strict
|
||||
import Data.Functor
|
||||
import Data.Text (Text)
|
||||
import Data.List (intersperse)
|
||||
import Data.String (IsString)
|
||||
import Unison.Path (Path)
|
||||
import qualified Unison.Path as Path
|
||||
import qualified Data.Text as Text
|
||||
|
||||
data Padded e r =
|
||||
Padded { top :: e, bottom :: e, left :: e, right :: e, element :: r } deriving Functor
|
||||
@ -136,6 +140,52 @@ preferredWidth width (p :< d) = case d of
|
||||
root :: Cofree f p -> p
|
||||
root (p :< _) = p
|
||||
|
||||
-- | The embedded elements of this document
|
||||
elements :: Doc e p -> [e]
|
||||
elements d = go (unwrap d) [] where
|
||||
one a = (a:)
|
||||
many xs tl = foldr (:) tl xs
|
||||
go (Append d1 d2) = go (unwrap d1) . go (unwrap d2)
|
||||
go (Group d) = go (unwrap d)
|
||||
go (Nest e d) = one e . go (unwrap d)
|
||||
go (Breakable e) = one e
|
||||
go (Embed e) = one e
|
||||
go (Pad (Padded t b l r inner)) = many [t, b, l, r] . go (unwrap inner)
|
||||
go _ = id
|
||||
|
||||
-- | Map over all `e` elements in this `Doc e p`.
|
||||
emap :: (e -> e2) -> Doc e p -> Doc e2 p
|
||||
emap f (p :< d) = p :< case d of
|
||||
Append d1 d2 -> Append (emap f d1) (emap f d2)
|
||||
Group d -> Group (emap f d)
|
||||
Nest e d -> Nest (f e) (emap f d)
|
||||
Breakable e -> Breakable (f e)
|
||||
Embed e -> Embed (f e)
|
||||
Pad (Padded t b l r inner) -> Pad (Padded (f t) (f b) (f l) (f r) (emap f inner))
|
||||
Linebreak -> Linebreak
|
||||
Empty -> Empty
|
||||
|
||||
-- | Substitute all `e` elements in this `Doc e p`. The
|
||||
-- function must return an `embed e2` when targeting elements
|
||||
-- embedded in a `nest` or `pad`, otherwise the substitution fails
|
||||
-- with `Nothing`.
|
||||
ebind :: (e -> Doc e2 p) -> Doc e p -> Maybe (Doc e2 p)
|
||||
ebind f (p :< d) = case d of
|
||||
Embed e -> Just (f e)
|
||||
d -> (p :<) <$> case d of
|
||||
Embed _ -> error "GHC can't figure out this is not possible"
|
||||
Append d1 d2 -> Append <$> ebind f d1 <*> ebind f d2
|
||||
Group d -> Group <$> ebind f d
|
||||
Nest e d -> Nest <$> e2 e <*> ebind f d
|
||||
Breakable e -> Breakable <$> e2 e
|
||||
Pad (Padded t b l r inner) -> Pad <$> (Padded <$> e2 t <*> e2 b <*> e2 l <*> e2 r <*> ebind f inner)
|
||||
Linebreak -> Just Linebreak
|
||||
Empty -> Just Empty
|
||||
where
|
||||
e2 e = case unwrap (f e) of
|
||||
Embed e2 -> Just e2
|
||||
_ -> Nothing
|
||||
|
||||
-- | The empty document
|
||||
empty :: Path p => Doc e p
|
||||
empty = Path.root :< Empty
|
||||
@ -179,7 +229,7 @@ nest :: Path p => e -> Doc e p -> Doc e p
|
||||
nest e (p :< d) = p :< Nest e (Path.root :< d)
|
||||
|
||||
-- | Specify that layout may insert a line break at this point in the document.
|
||||
-- If a line break is not inserts, the given `e` is inserted instead.
|
||||
-- If a line break is not inserted, the given `e` is inserted instead.
|
||||
breakable :: Path p => e -> Doc e p
|
||||
breakable e = breakable' Path.root e
|
||||
|
||||
@ -267,10 +317,17 @@ renderString = render' (Renderer' concat "\n") id
|
||||
formatString :: Int -> Doc String p -> String
|
||||
formatString availableWidth d = renderString (layout length availableWidth d)
|
||||
|
||||
formatText :: Int -> Doc Text p -> String
|
||||
formatText availableWidth d =
|
||||
formatString availableWidth (emap Text.unpack d)
|
||||
|
||||
docs :: Path p => [Doc e p] -> Doc e p
|
||||
docs [] = empty
|
||||
docs ds = foldr1 append ds
|
||||
|
||||
embeds :: Path p => [e] -> Doc e p
|
||||
embeds = docs . map embed
|
||||
|
||||
delimit :: Path p => Doc e p -> [Doc e p] -> Doc e p
|
||||
delimit d = docs . intersperse d
|
||||
|
||||
@ -281,3 +338,8 @@ sep delim ds = group (foldr1 combine ds)
|
||||
|
||||
sep' :: Path p => e -> [e] -> Doc e p
|
||||
sep' delim ds = sep delim (map embed ds)
|
||||
|
||||
parenthesize :: (IsString s, Path p) => Bool -> Doc s p -> Doc s p
|
||||
parenthesize b d =
|
||||
let r = root d
|
||||
in if b then docs [embed' r "(", d, embed' r ")"] else d
|
||||
|
@ -6,6 +6,8 @@
|
||||
|
||||
module Unison.Path where
|
||||
|
||||
import Control.Applicative
|
||||
|
||||
-- | Satisfies:
|
||||
-- * `extend root p == p` and `extend p root == p`
|
||||
-- * `extend` is associative, `extend (extend p1 p2) p3 == extend p1 (extend p2 p3)`
|
||||
@ -23,8 +25,19 @@ class Path p where
|
||||
lca :: Path p => p -> p -> p
|
||||
lca p p2 = fst (factor p p2)
|
||||
|
||||
instance Eq a => Path (Maybe a) where
|
||||
root = Nothing
|
||||
extend = (<|>)
|
||||
factor p1 p2 | p1 == p2 = (p1, (Nothing, Nothing))
|
||||
factor p1 p2 = (Nothing, (p1,p2))
|
||||
|
||||
instance Eq a => Path [a] where
|
||||
root = []
|
||||
extend = (++)
|
||||
factor p1 p2 = (take shared p1, (drop shared p1, drop shared p2))
|
||||
where shared = length (zipWith (==) p1 p2)
|
||||
|
||||
instance Path () where
|
||||
root = ()
|
||||
extend _ _ = ()
|
||||
factor u _ = (u,(u,u))
|
||||
|
@ -5,6 +5,8 @@ module Unison.Symbol where
|
||||
import Data.Aeson.TH
|
||||
import Data.Text (Text)
|
||||
import Unison.Var (Var(..))
|
||||
import Unison.View (View)
|
||||
import qualified Unison.View as View
|
||||
import qualified Data.Set as Set
|
||||
import qualified Data.Text as Text
|
||||
|
||||
@ -18,9 +20,13 @@ freshId (Symbol id _ _) = id
|
||||
annotation :: Symbol a -> a
|
||||
annotation (Symbol _ _ a) = a
|
||||
|
||||
instance Var (Symbol (Maybe a)) where
|
||||
annotate :: a -> Symbol b -> Symbol a
|
||||
annotate a (Symbol id name _) = Symbol id name a
|
||||
|
||||
instance View op => Var (Symbol op) where
|
||||
name (Symbol _ n _) = n
|
||||
named n = Symbol 0 n Nothing
|
||||
named n = Symbol 0 n View.prefix
|
||||
clear (Symbol id n _) = Symbol id n View.prefix
|
||||
qualifiedName s = name s `Text.append` (Text.pack (show (freshId s)))
|
||||
freshIn vs s | Set.null vs = s -- already fresh!
|
||||
freshIn vs s | Set.notMember s vs = s -- already fresh!
|
||||
@ -36,14 +42,14 @@ instance Eq (Symbol a) where
|
||||
instance Ord (Symbol a) where
|
||||
Symbol id1 name1 _ `compare` Symbol id2 name2 _ = (id1,name1) `compare` (id2,name2)
|
||||
|
||||
instance Show (Symbol (Maybe a)) where
|
||||
instance View op => Show (Symbol op) where
|
||||
show s | freshId s == 0 = Text.unpack (name s)
|
||||
show s = Text.unpack (name s) ++ show (freshId s)
|
||||
|
||||
symbol :: Text -> Symbol ()
|
||||
symbol n = Symbol 0 n ()
|
||||
symbol :: View op => Text -> Symbol op
|
||||
symbol n = Symbol 0 n View.prefix
|
||||
|
||||
prefix :: Text -> Symbol ()
|
||||
prefix :: View op => Text -> Symbol op
|
||||
prefix name = symbol name
|
||||
|
||||
deriveJSON defaultOptions ''Symbol
|
||||
|
@ -1,8 +1,9 @@
|
||||
{-# LANGUAGE DeriveFunctor #-}
|
||||
{-# LANGUAGE DeriveFoldable #-}
|
||||
{-# LANGUAGE DeriveFunctor #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE DeriveTraversable #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE PatternSynonyms #-}
|
||||
{-# LANGUAGE Rank2Types #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
@ -22,19 +23,27 @@ import Data.Vector (Vector, (!?))
|
||||
import GHC.Generics
|
||||
import Prelude.Extras (Eq1(..), Show1(..))
|
||||
import Text.Show
|
||||
import Unison.Doc (Doc)
|
||||
import Unison.Hash (Hash)
|
||||
import Unison.Reference (Reference)
|
||||
import Unison.Symbol (Symbol)
|
||||
import Unison.Type (Type)
|
||||
import Unison.Var (Var)
|
||||
import qualified Control.Monad.Writer.Strict as Writer
|
||||
import qualified Data.Aeson as Aeson
|
||||
import qualified Data.Monoid as Monoid
|
||||
import qualified Data.Set as Set
|
||||
import qualified Data.Text as Text
|
||||
import qualified Data.Vector as Vector
|
||||
import qualified Unison.ABT as ABT
|
||||
import qualified Unison.Reference as Reference
|
||||
import qualified Unison.Distance as Distance
|
||||
import qualified Unison.Doc as D
|
||||
import qualified Unison.JSON as J
|
||||
import qualified Unison.Reference as Reference
|
||||
import qualified Unison.Symbol as Symbol
|
||||
import qualified Unison.Type as Type
|
||||
import qualified Unison.Var as Var
|
||||
import qualified Unison.View as View
|
||||
|
||||
-- | Literals in the Unison language
|
||||
data Literal
|
||||
@ -73,10 +82,14 @@ pattern Text' s <- Lit' (Text s)
|
||||
pattern Blank' <- (ABT.out -> ABT.Tm Blank)
|
||||
pattern Ref' r <- (ABT.out -> ABT.Tm (Ref r))
|
||||
pattern App' f x <- (ABT.out -> ABT.Tm (App f x))
|
||||
pattern Apps' f args <- (unApps -> Just (f, args))
|
||||
pattern AppsP' f args <- (unApps' -> Just (f, args))
|
||||
pattern Ann' x t <- (ABT.out -> ABT.Tm (Ann x t))
|
||||
pattern Vector' xs <- (ABT.out -> ABT.Tm (Vector xs))
|
||||
pattern Lam' v body <- (ABT.out -> ABT.Tm (Lam (ABT.Term _ _ (ABT.Abs v body))))
|
||||
pattern LamsP' vs body <- (unLams' -> Just (vs, body))
|
||||
pattern Let1' v b e <- (ABT.out -> ABT.Tm (Let b (ABT.Abs' v e)))
|
||||
pattern Lets' bs e <- Let' bs e _ False
|
||||
pattern Let' bs e relet rec <- (unLets -> Just (bs,e,relet,rec))
|
||||
pattern LetRec' bs e <- (unLetRec -> Just (bs,e))
|
||||
|
||||
@ -171,6 +184,30 @@ unLet t = fixup (go t) where
|
||||
fixup ([], _) = Nothing
|
||||
fixup bst = Just bst
|
||||
|
||||
unApps :: Term v -> Maybe (Term v, [Term v])
|
||||
unApps t = case go t [] of [] -> Nothing; f:args -> Just (f,args)
|
||||
where
|
||||
go (App' i o) acc = go i (o:acc)
|
||||
go fn args = fn:args
|
||||
|
||||
unApps' :: Term v -> Maybe ((Term v,Path), [(Term v,Path)])
|
||||
unApps' t = addPaths <$> unApps t
|
||||
where
|
||||
addPaths (f,args) = case appPaths (length args) of
|
||||
(fp,ap) -> ((f,fp), args `zip` ap)
|
||||
|
||||
appPaths :: Int -> (Path, [Path])
|
||||
appPaths numArgs = (fnp, argsp)
|
||||
where
|
||||
fnp = replicate numArgs Fn
|
||||
argsp = take numArgs . drop 1 $ iterate (Fn:) [Arg]
|
||||
|
||||
unLams' :: Term v -> Maybe ([(v, Path)], (Term v, Path))
|
||||
unLams' (Lam' v body) = case unLams' body of
|
||||
Nothing -> Just ([(v, [])], (body, [Body])) -- todo, need a path for forall vars
|
||||
Just (vs, (body,bodyp)) -> Just ((v, []) : vs, (body, Body:bodyp))
|
||||
unLams' _ = Nothing
|
||||
|
||||
dependencies' :: Ord v => Term v -> Set Reference
|
||||
dependencies' t = Set.fromList . Writer.execWriter $ ABT.visit' f t
|
||||
where f t@(Ref r) = Writer.tell [r] *> pure t
|
||||
@ -190,6 +227,7 @@ data PathElement
|
||||
| Body -- ^ Points at the body of a lambda or let
|
||||
| Binding !Int -- ^ Points at a particular binding in a let
|
||||
| Index !Int -- ^ Points at the index of a vector
|
||||
| Annotation Type.Path -- ^ Points into the type of an `Ann`
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
type Path = [PathElement]
|
||||
@ -207,6 +245,7 @@ focus1 (Binding i) (LetRec bs body) =
|
||||
>>= \b -> Just (b, \b -> LetRec (take i bs ++ [b] ++ drop (i+1) bs) body)
|
||||
focus1 (Index i) (Vector vs) =
|
||||
vs !? i >>= \v -> Just (v, \v -> Vector (Vector.update vs (Vector.singleton (i,v))))
|
||||
focus1 (Annotation pt) (Ann e t) = Just (e, \e -> Ann e t) -- todo: revisit
|
||||
focus1 _ _ = Nothing
|
||||
|
||||
-- | Return the list of all prefixes of the input path
|
||||
@ -262,6 +301,70 @@ betaReduce :: Var v => Term v -> Term v
|
||||
betaReduce (App' (Lam' n body) arg) = ABT.subst arg n body
|
||||
betaReduce e = e
|
||||
|
||||
type ViewableTerm = Term (Symbol View.DFO)
|
||||
|
||||
toString :: ViewableTerm -> String
|
||||
toString t = D.formatText 80 (view Type.defaultSymbol t)
|
||||
|
||||
view :: (Reference -> Symbol View.DFO) -> ViewableTerm -> Doc Text Path
|
||||
view ref t = go no View.low t where
|
||||
no = const False
|
||||
sym v = D.embed (Var.name v)
|
||||
op t = case t of
|
||||
Lit' l -> Symbol.annotate View.prefix . (\r -> Symbol.prefix r :: Symbol ()) . Text.pack . show $ l
|
||||
Var' v -> v
|
||||
_ -> Symbol.annotate View.prefix (Symbol.prefix "" :: Symbol ())
|
||||
formatBinding :: Path -> Symbol View.DFO -> ViewableTerm -> Doc Text Path
|
||||
formatBinding path name body = case body of
|
||||
LamsP' vs (body,bodyp) ->
|
||||
let lhs = fmap fixup $ go no View.low (apps (var name) (map (var . fst) vs))
|
||||
fixup _ = [] -- todo, could use paths to individual variables
|
||||
rhs = D.sub' bodyp $ go no View.low body
|
||||
in D.group . D.sub' path $ D.docs [lhs, D.embed " =", D.breakable " ", D.nest " " rhs]
|
||||
_ -> D.sub' path $ D.docs [sym name, D.embed " =", D.breakable " ", D.nest " " $ go no View.low body ]
|
||||
go :: (ViewableTerm -> Bool) -> View.Precedence -> ViewableTerm -> Doc Text Path
|
||||
go inChain p t = case t of
|
||||
Lets' bs e ->
|
||||
let
|
||||
pe = replicate (length bs) Body
|
||||
bps = tail (tails pe)
|
||||
formattedBs = [ formatBinding bp name b | ((name,b), bp) <- bs `zip` bps ]
|
||||
in D.group $ D.docs [D.embed "let", D.breakable " "] `D.append`
|
||||
D.nest " " (D.delimit (D.breakable "; ") formattedBs) `D.append`
|
||||
D.docs [D.embed "in", D.breakable " ", D.sub' pe . D.nest " " $ go no View.low e ]
|
||||
LetRec' bs e ->
|
||||
let
|
||||
bps = map Binding [0 .. length bs - 1]
|
||||
formattedBs = [ formatBinding [bp] name b | ((name,b), bp) <- bs `zip` bps ]
|
||||
in D.group $ D.docs [D.embed "let rec", D.breakable " "] `D.append`
|
||||
D.nest " " (D.delimit (D.breakable "; ") formattedBs) `D.append`
|
||||
D.docs [D.embed "in", D.breakable " ", D.sub Body . D.nest " " $ go no View.low e ]
|
||||
AppsP' (fn,fnP) args ->
|
||||
let
|
||||
Symbol.Symbol _ name view = op fn
|
||||
(taken, remaining) = splitAt (View.arity view) args
|
||||
fmt (child,path) = (\p -> D.sub' path (go (fn ==) p child), path)
|
||||
applied = fromMaybe unsaturated (View.instantiate view fnP name (map fmt taken))
|
||||
unsaturated = D.sub' fnP $ go no View.high fn
|
||||
in
|
||||
(if inChain fn then id else D.group) $ case remaining of
|
||||
[] -> applied
|
||||
args -> D.parenthesize (p > View.high) . D.group . D.docs $
|
||||
[ applied, D.breakable " "
|
||||
, D.nest " " . D.group . D.delimit (D.breakable " ") $
|
||||
[ D.sub' p (go no (View.increase View.high) s) | (s,p) <- args ] ]
|
||||
LamsP' vs (body,bodyp) ->
|
||||
if p == View.low then D.sub' bodyp (go no p body)
|
||||
else D.parenthesize True . D.group $
|
||||
D.delimit (D.embed " ") (map (sym . fst) vs) `D.append`
|
||||
D.docs [D.embed "→", D.breakable " ", D.nest " " $ D.sub' bodyp (go no View.low body)]
|
||||
Ann' e t -> D.group . D.parenthesize (p /= View.low) $
|
||||
D.docs [ go no p e, D.embed " :", D.breakable " "
|
||||
, D.nest " " $ (\p -> [Annotation p]) <$> Type.view ref t ]
|
||||
Var' v -> sym v
|
||||
Lit' _ -> D.embed (Var.name $ op t)
|
||||
_ -> error $ "layout match failure"
|
||||
|
||||
-- mostly boring serialization code below ...
|
||||
|
||||
deriveJSON defaultOptions ''Literal
|
||||
|
@ -12,19 +12,27 @@ module Unison.Type where
|
||||
|
||||
import Data.Aeson (ToJSON(..), FromJSON(..))
|
||||
import Data.Aeson.TH
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Set (Set)
|
||||
import Data.Text (Text)
|
||||
import GHC.Generics
|
||||
import Prelude.Extras (Eq1(..),Show1(..))
|
||||
import Unison.Doc (Doc)
|
||||
import Unison.Note (Noted)
|
||||
import Unison.Reference (Reference)
|
||||
import Unison.Symbol (Symbol(..))
|
||||
import Unison.Var (Var)
|
||||
import qualified Data.Set as Set
|
||||
import qualified Data.Text as Text
|
||||
import qualified Unison.ABT as ABT
|
||||
import qualified Unison.Doc as D
|
||||
import qualified Unison.Hash as Hash
|
||||
import qualified Unison.JSON as J
|
||||
import qualified Unison.Kind as K
|
||||
import qualified Unison.Reference as Reference
|
||||
import qualified Unison.Symbol as Symbol
|
||||
import qualified Unison.Var as Var
|
||||
import qualified Unison.View as View
|
||||
|
||||
-- | Type literals
|
||||
data Literal
|
||||
@ -87,6 +95,7 @@ pattern Apps' f args <- (unApps -> Just (f, args))
|
||||
pattern AppsP' f args <- (unApps' -> Just (f, args))
|
||||
pattern Constrain' t u <- ABT.Tm' (Constrain t u)
|
||||
pattern Forall' v body <- ABT.Tm' (Forall (ABT.Abs' v body))
|
||||
pattern ForallsP' vs body <- (unForalls' -> Just (vs, body))
|
||||
pattern Existential' v <- ABT.Tm' (Existential (ABT.Var' v))
|
||||
pattern Universal' v <- ABT.Tm' (Universal (ABT.Var' v))
|
||||
|
||||
@ -101,6 +110,12 @@ unArrows' :: Type v -> Maybe [(Type v,Path)]
|
||||
unArrows' t = addPaths <$> unArrows t
|
||||
where addPaths ts = ts `zip` arrowPaths (length ts)
|
||||
|
||||
unForalls' :: Type v -> Maybe ([(v, Path)], (Type v, Path))
|
||||
unForalls' (Forall' v body) = case unForalls' body of
|
||||
Nothing -> Just ([(v, [])], (body, [Body])) -- todo, need a path for forall vars
|
||||
Just (vs, (body,bodyp)) -> Just ((v, []) : vs, (body, Body:bodyp))
|
||||
unForalls' _ = Nothing
|
||||
|
||||
unApps :: Type v -> Maybe (Type v, [Type v])
|
||||
unApps t = case go t [] of [] -> Nothing; f:args -> Just (f,args)
|
||||
where
|
||||
@ -177,44 +192,67 @@ data PathElement
|
||||
| Input -- ^ Points at the left of an `Arrow`
|
||||
| Output -- ^ Points at the right of an `Arrow`
|
||||
| Body -- ^ Points at the body of a forall
|
||||
deriving (Eq,Ord)
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
type Path = [PathElement]
|
||||
|
||||
layout :: (Var v, ToJSON v) => (Reference -> v) -> Type v -> D.Doc Text Path
|
||||
layout ref t = go (0 :: Int) t
|
||||
type ViewableType = Type (Symbol View.DFO)
|
||||
|
||||
defaultSymbol :: Reference -> Symbol View.DFO
|
||||
defaultSymbol (Reference.Builtin t) = Symbol.prefix t
|
||||
defaultSymbol (Reference.Derived h) = Symbol.prefix (Text.cons '#' $ short h)
|
||||
where
|
||||
(<>) = D.append
|
||||
lit l = case l of
|
||||
Number -> "Number"
|
||||
Text -> "Text"
|
||||
Vector -> "Vector"
|
||||
Distance -> "Distance"
|
||||
Ref r -> Var.name (ref r) -- no infix type operators at the moment
|
||||
paren b d =
|
||||
let r = D.root d
|
||||
in if b then D.embed' r "(" <> d <> D.embed' r ")" else d
|
||||
arr = D.breakable " " <> D.embed "→ "
|
||||
sp = D.breakable " "
|
||||
short h = Text.take 8 . Hash.base64 $ h
|
||||
|
||||
toString :: ViewableType -> String
|
||||
toString t = D.formatText 80 (view defaultSymbol t)
|
||||
|
||||
view :: (Reference -> Symbol View.DFO) -> ViewableType -> Doc Text Path
|
||||
view ref t = go no View.low t
|
||||
where
|
||||
no = const False
|
||||
sym v = D.embed (Var.name v)
|
||||
go p t = case t of
|
||||
Lit' l -> D.embed (lit l)
|
||||
op :: ViewableType -> Symbol View.DFO
|
||||
op t = case t of
|
||||
Lit' (Ref r) -> ref r
|
||||
Lit' l -> Symbol.annotate View.prefix . (\r -> Symbol.prefix r :: Symbol ()) . Text.pack . show $ l
|
||||
Universal' v -> v
|
||||
Existential' v -> v
|
||||
_ -> Symbol.annotate View.prefix (Symbol.prefix "" :: Symbol ())
|
||||
go :: (ViewableType -> Bool) -> View.Precedence -> ViewableType -> Doc Text Path
|
||||
go inChain p t = case t of
|
||||
ArrowsP' spine ->
|
||||
paren (p > 0) . D.group . D.delimit arr $ [ D.sub' p (go 1 s) | (s,p) <- spine ]
|
||||
let arr = D.breakable " " `D.append` D.embed "→ "
|
||||
in D.parenthesize (p > View.low) . D.group . D.delimit arr $
|
||||
[ D.sub' p (go no (View.increase View.low) s) | (s,p) <- spine ]
|
||||
AppsP' (fn,fnP) args ->
|
||||
paren (p > 9) . D.group . D.docs $
|
||||
[ D.sub' fnP (go 9 fn)
|
||||
, D.breakable " "
|
||||
, D.nest " " . D.group . D.delimit sp $ [ D.sub' p (go 10 s) | (s,p) <- args ] ]
|
||||
Constrain' t _ -> go p t
|
||||
let
|
||||
Symbol _ name view = op fn
|
||||
(taken, remaining) = splitAt (View.arity view) args
|
||||
fmt (child,path) = (\p -> D.sub' path (go (fn ==) p child), path)
|
||||
applied = fromMaybe unsaturated (View.instantiate view fnP name (map fmt taken))
|
||||
unsaturated = D.sub' fnP $ go no View.high fn
|
||||
in
|
||||
(if inChain fn then id else D.group) $ case remaining of
|
||||
[] -> applied
|
||||
args -> D.parenthesize (p > View.high) . D.group . D.docs $
|
||||
[ applied, D.breakable " "
|
||||
, D.nest " " . D.group . D.delimit (D.breakable " ") $
|
||||
[ D.sub' p (go no (View.increase View.high) s) | (s,p) <- args ] ]
|
||||
ForallsP' vs (body,bodyp) ->
|
||||
if p == View.low then D.sub' bodyp (go no p body)
|
||||
else D.parenthesize True . D.group $
|
||||
D.embed "∀ " `D.append`
|
||||
D.delimit (D.embed " ") (map (sym . fst) vs) `D.append`
|
||||
D.docs [D.embed ".", D.breakable " ", D.nest " " $ D.sub' bodyp (go no View.low body)]
|
||||
Constrain' t _ -> go inChain p t
|
||||
Ann' t _ -> go inChain p t -- ignoring kind annotations for now
|
||||
Universal' v -> sym v
|
||||
Existential' v -> D.embed ("'" `mappend` Var.name v)
|
||||
Ann' t _ -> go p t -- ignoring kind annotations for now
|
||||
Forall' v body -> case p of
|
||||
0 -> D.sub Body (go p body)
|
||||
_ -> paren True . D.group . D.docs $
|
||||
[D.embed "∀ ", sym v, D.embed ".", sp, D.nest " " $ D.sub Body (go 0 body)]
|
||||
_ -> error $ "layout match failure on: " ++ show (toJSON t)
|
||||
Lit' _ -> D.embed (Var.name $ op t)
|
||||
_ -> error $ "layout match failure"
|
||||
|
||||
deriveJSON defaultOptions ''PathElement
|
||||
|
||||
instance J.ToJSON1 F where
|
||||
toJSON1 f = toJSON f
|
||||
|
@ -4,9 +4,30 @@ import Data.Set (Set)
|
||||
import Data.Text (Text)
|
||||
import qualified Data.Set as Set
|
||||
|
||||
-- | A class for variables. Variables may have auxiliary information which
|
||||
-- may not form part of their identity according to `Eq` / `Ord`. Laws:
|
||||
--
|
||||
-- * `name (named n) == n`:
|
||||
-- `name` returns the name set by `named`.
|
||||
-- * `Set.notMember (freshIn vs v) vs`:
|
||||
-- `freshIn` returns a variable not used in the `Set`
|
||||
-- * `name (freshIn vs v) == name v`:
|
||||
-- `freshIn` does not alter the name
|
||||
-- * `Set.notMember (qualifiedName $ freshIn vs v) (Set.map qualifiedName vs)`:
|
||||
-- `qualifiedName` incorporates all additional id info from freshening into
|
||||
-- the name of the variable.
|
||||
-- * `clear (freshIn vs v) === clear (freshIn vs (named (name v)))`:
|
||||
-- `clear` strips any auxiliary information and returns a variable that behaves
|
||||
-- as if it has been built solely via calls to `named` and `freshIn`. The `===`
|
||||
-- is full equality, comparing any auxiliary info as well as qualified name.
|
||||
-- * `clear v == v`, according to Haskell equality. In other words, no auxiliary
|
||||
-- info attached to `v` values may participate in the `Eq` or `Ord` instances,
|
||||
-- it is 'just' metadata.
|
||||
--
|
||||
class (Eq v, Ord v) => Var v where
|
||||
named :: Text -> v
|
||||
name :: v -> Text
|
||||
clear :: v -> v
|
||||
qualifiedName :: v -> Text
|
||||
freshIn :: Set v -> v -> v
|
||||
|
||||
|
138
shared/src/Unison/View.hs
Normal file
138
shared/src/Unison/View.hs
Normal file
@ -0,0 +1,138 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
module Unison.View where
|
||||
|
||||
import Data.String (IsString(..))
|
||||
import Data.Text (Text)
|
||||
import Unison.Doc (Doc)
|
||||
import Unison.Path (Path)
|
||||
import qualified Data.Text as Text
|
||||
import qualified Unison.Doc as D
|
||||
import qualified Unison.Path as Path
|
||||
|
||||
newtype Precedence = Precedence Int deriving (Eq,Ord)
|
||||
|
||||
low :: Precedence
|
||||
low = Precedence 0
|
||||
|
||||
high :: Precedence
|
||||
high = Precedence 10
|
||||
|
||||
increase :: Precedence -> Precedence
|
||||
increase (Precedence p) = Precedence (p + 1)
|
||||
|
||||
-- | `Arg 0` references the name of the operator; `Arg 1`
|
||||
-- references the first argument it is applied to, `Arg 2`
|
||||
-- the second argument it is applied to, etc.
|
||||
newtype Var = Arg Int deriving (Eq,Ord)
|
||||
|
||||
data Segment = Slot Var Precedence | Text Text
|
||||
|
||||
instance IsString Segment where
|
||||
fromString s = Text (Text.pack s)
|
||||
|
||||
path :: Segment -> Maybe Var
|
||||
path (Slot v _) = Just v
|
||||
path _ = Nothing
|
||||
|
||||
text :: Text -> Doc Segment (Maybe Var)
|
||||
text t = D.embed (Text t)
|
||||
|
||||
toDoc :: Segment -> Doc Segment (Maybe Var)
|
||||
toDoc t@(Text _) = D.embed t
|
||||
toDoc s@(Slot var _) = D.embed' (Just var) s
|
||||
|
||||
arg0, arg1, arg2, arg3, arg4 :: Precedence -> Doc Segment (Maybe Var)
|
||||
arg0 p = toDoc $ Slot (Arg 0) p
|
||||
arg1 p = toDoc $ Slot (Arg 1) p
|
||||
arg2 p = toDoc $ Slot (Arg 2) p
|
||||
arg3 p = toDoc $ Slot (Arg 3) p
|
||||
arg4 p = toDoc $ Slot (Arg 4) p
|
||||
|
||||
name :: Doc Segment (Maybe Var)
|
||||
name = toDoc $ Slot (Arg 0) high
|
||||
|
||||
-- | The associativity of a binary operator, which controls how / whether
|
||||
-- parentheses or other indicators of grouping are displayed in chains
|
||||
-- of operators.
|
||||
--
|
||||
-- * `AssociateL` on an operator, `+`, indicates that `(a + b) + c`
|
||||
-- may be displayed without parens, as `a + b + c`. `a + (b + c)`
|
||||
-- should display with parentheses.
|
||||
-- * `AssociateR` on an operator, `::`, indicates that `a :: (b :: c)`
|
||||
-- may be displayed without parens, as `a :: b :: c`. `(a :: b) :: c`
|
||||
-- should display with parentheses.
|
||||
-- * `Associative` on an operator, `*`, indicates that chains of that
|
||||
-- operator should always display without parens. So a syntax tree of
|
||||
-- `a * (b * c)` and `(a * b) * c` would display as `a * b * c`.
|
||||
-- * `None` indicates that all grouping of the syntax tree should be
|
||||
-- indicated visually. So `a ++ (b ++ c)` and `(a ++ b) ++ c` would
|
||||
-- both display with parens if `++` had `None` as its associativity.
|
||||
--
|
||||
data Associativity = AssociateL | AssociateR | Associative | None deriving (Eq,Ord)
|
||||
|
||||
class View op where
|
||||
-- | A prefix operator, of arity 0. This is the only arity 0 operator.
|
||||
prefix :: op
|
||||
|
||||
-- | A postfix operator, of arity 1.
|
||||
postfix1 :: Precedence -> op
|
||||
|
||||
-- | A binary operator, of arity 2.
|
||||
binary :: Associativity -> Precedence -> op
|
||||
|
||||
-- | All operators have an arity, which is the number of subsequent
|
||||
-- applications they capture for insertion into their layout.
|
||||
-- `arity prefix == 0` and `arity (binary assoc prec) == 2`.
|
||||
arity :: op -> Int
|
||||
|
||||
-- | The layout is an arbitrary `Doc`, which can refer to both
|
||||
-- the operator's name, and any arguments captured by its arity.
|
||||
-- An unsaturated operator (applied to fewer than `arity` arguments)
|
||||
-- gets displayed as `prefix`.
|
||||
layout :: op -> Doc Segment (Maybe Var)
|
||||
|
||||
-- | The precedence of the operator
|
||||
precedence :: op -> Precedence
|
||||
|
||||
data DFO = DFO (Doc Segment (Maybe Var)) Precedence
|
||||
|
||||
mixfix :: Precedence -> [Doc Segment (Maybe Var)] -> DFO
|
||||
mixfix prec segs = DFO (D.docs segs) prec
|
||||
|
||||
instance View () where
|
||||
arity _ = 0
|
||||
precedence _ = high
|
||||
layout _ = name
|
||||
prefix = ()
|
||||
postfix1 _ = ()
|
||||
binary _ _ = ()
|
||||
|
||||
instance View DFO where
|
||||
arity (DFO l _) = maximum $ 0 : [ i | Slot (Arg i) _ <- D.elements l ]
|
||||
precedence (DFO _ p) = p
|
||||
layout (DFO l _) = l
|
||||
prefix = DFO name high
|
||||
postfix1 prec = DFO (D.docs [arg1 prec, text " ", name]) prec
|
||||
binary assoc prec =
|
||||
DFO layout prec
|
||||
where
|
||||
deltaL p | assoc == AssociateL || assoc == Associative = p
|
||||
deltaL p = increase p
|
||||
deltaR p | assoc == AssociateR || assoc == Associative = p
|
||||
deltaR p = increase p
|
||||
layout = D.docs
|
||||
[ arg1 (deltaL prec), D.breakable " ", name, text " "
|
||||
, arg2 (deltaR prec) ]
|
||||
|
||||
instantiate :: (Path p, View op) => op -> p -> Text -> [(Precedence -> Doc Text p, p)] -> Maybe (Doc Text p)
|
||||
instantiate op opP name args | arity op == length args =
|
||||
D.ebind f (fmap g (layout op))
|
||||
where
|
||||
f (Slot (Arg 0) prec) = D.embed name
|
||||
f (Slot (Arg i) prec) = let (a,_) = args !! (i - 1) in a prec
|
||||
f (Text t) = D.embed t
|
||||
g Nothing = Path.root
|
||||
g (Just (Arg 0)) = opP
|
||||
g (Just (Arg i)) = snd $ args !! (i - 1)
|
||||
instantiate _ _ _ _ = Nothing
|
@ -52,6 +52,7 @@ library
|
||||
Unison.Typechecker
|
||||
Unison.Typechecker.Context
|
||||
Unison.Var
|
||||
Unison.View
|
||||
|
||||
build-depends:
|
||||
aeson,
|
||||
|
Loading…
Reference in New Issue
Block a user