Commit 2731302c authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Improve the showNode function to only show minimal patterns (using...

Improve the showNode function to only show minimal patterns (using eta-equivalence); add support for inline code snippets in the WiQEE consoles
parent ffa15775
......@@ -2,7 +2,7 @@
-- see http://haskell.org/cabal/users-guide/
name: capricon
version: 0.8
version: 0.8.1
-- synopsis:
-- description:
license: GPL-3
......
......@@ -90,7 +90,7 @@ setBytes :: String -> [Word8] -> JS.CIO ()
setBytes f v = setString f (map (toEnum . fromIntegral) v)
hasteDict :: COCDict JS.CIO String
hasteDict = cocDict ("0.8-js" :: String) getString getBytes setString setBytes
hasteDict = cocDict ("0.8.1-js" :: String) getString getBytes setString setBytes
main :: IO ()
main = JS.concurrent $ void $ do
......@@ -107,40 +107,48 @@ main = JS.concurrent $ void $ do
prelude <- JS.withElem "capricon-prelude" (\e -> JS.getProp e "textContent")
(initState,_) <- runWordsState (map fromString $ stringWords prelude) (defaultState hasteDict (COCState False [] zero id))
roots <- JS.elemsByClass "capricon-steps"
roots <- JS.elemsByQS JS.documentBody ".capricon-steps, code.capricon"
Just console <- JS.elemById "capricon-console"
(\k -> foldr k (const unit) roots initState) $ \root next state -> do
JS.wait 10
(\k -> foldr k (\_ _ -> unit) roots initState "") $ \root next state pref -> do
isCode <- JS.hasClass root "capricon"
root' <- cloneNode root
JS.toggleClass root' "capricon-frame"
rootChildren <- JS.getChildren root'
rootTitle <- JS.newElem "h3" <*= \head -> JS.appendChild head =<< JS.newTextElem "CaPriCon Console"
closeBtn <- JS.newElem "button" <*= \but -> JS.appendChild but =<< JS.newTextElem "Close"
JS.appendChild rootTitle closeBtn
JS.appendChild console root'
JS.setChildren root' (rootTitle:rootChildren)
withSubElems root ["capricon-trigger"] $ \[trig] -> void $ do
withSubElems root' ["capricon-input"] $ \[inp] -> void $ do
let toggleActive = do
JS.toggleClass root' "active"
JS.focus inp
JS.onEvent closeBtn JS.Click (const toggleActive)
JS.onEvent trig JS.Click $ \_ -> toggleActive
withSubElems root' ["capricon-input","capricon-output"] $ \[inp,out] -> do
JS.withElemsQS root' ".capricon-context" $ \case
[con] -> do
context <- JS.getProp con "textContent"
(state',_) <- runWordsState (stringWords (fromString context)) state
JS.onEvent inp JS.KeyPress $ \case
JS.KeyData 13 False False False False -> do
Just v <- JS.getValue inp
(_,x) <- runWordsState (stringWords v) state'
JS.setProp out "textContent" (toString x)
_ -> unit
next state'
if isCode
then do
p <- JS.getProp root "textContent"
next state (pref+" "+p)
else do
JS.wait 10
root' <- cloneNode root
JS.toggleClass root' "capricon-frame"
rootChildren <- JS.getChildren root'
rootTitle <- JS.newElem "h3" <*= \head -> JS.appendChild head =<< JS.newTextElem "CaPriCon Console"
closeBtn <- JS.newElem "button" <*= \but -> JS.appendChild but =<< JS.newTextElem "Close"
JS.appendChild rootTitle closeBtn
JS.appendChild console root'
JS.setChildren root' (rootTitle:rootChildren)
withSubElems root ["capricon-trigger"] $ \[trig] -> void $ do
withSubElems root' ["capricon-input"] $ \[inp] -> void $ do
let toggleActive = do
JS.toggleClass root' "active"
JS.focus inp
JS.onEvent closeBtn JS.Click (const toggleActive)
JS.onEvent trig JS.Click $ \_ -> toggleActive
withSubElems root' ["capricon-input","capricon-output"] $ \[inp,out] -> do
JS.withElemsQS root' ".capricon-context" $ \case
[con] -> do
context <- JS.getProp con "textContent"
let text = pref+" "+context
(state',_) <- runWordsState (stringWords text) state
JS.onEvent inp JS.KeyPress $ \case
JS.KeyData 13 False False False False -> do
Just v <- JS.getValue inp
(_,x) <- runWordsState (stringWords v) state'
JS.setProp out "textContent" (toString x)
_ -> unit
next state' ""
cloneNode :: MonadIO m => JS.Elem -> m JS.Elem
cloneNode x = liftIO $ JS.ffi "(function (n) { return n.cloneNode(true); })" x
......@@ -82,13 +82,13 @@ literate = intercalate [":s\n"] <$> sepBy' (cmdline "> " <+? cmdline "$> " <+? c
cmdline pre = map (\x -> [":cp"+intercalate "\n" (map fst x)]
+ wrapResult True (foldMap snd x))
(sepBy1' go (single '\n'))
where go = do pre; many' (noneOf ['\n']) <&> \x -> (fromString x,map fromString (stringWords x))
where go = do pre; many' (noneOf ['\n']) <&> \x -> (fromString x,map fromString (stringWords x+["steps."]))
commentline = map (foldMap (pure . (":s"+) <|> \(x,t) -> t+[":cs"+x])) $ (<* lookingAt eol)
$ many' (map (Left . fromString) (many1' (noneOf ['{','\n'] <+?
(fill '{' $ single '{' <* lookingAt (noneOf ['{']))))
<+? map Right (between "{{" "}}"
(many1' (noneOf ['}'] <+? fill '}' (single '}' <* lookingAt (noneOf ['}'])))
<&> \x -> (fromString x,wrapResult False (stringWords (fromString x))))))
<&> \x -> (fromString x,wrapResult False (stringWords (fromString x)+["mustache."])))))
data COCState str = COCState {
_endState :: Bool,
......@@ -322,7 +322,7 @@ type COCDict io str = Map str (StackVal str (COCBuiltin io str) (COCValue io str
cocDict :: forall io str. IsCapriconString str => str -> (str -> io (Maybe str)) -> (str -> io (Maybe [Word8])) -> (str -> str -> io ()) -> (str -> [Word8] -> io ()) -> COCDict io str
cocDict version getResource getBResource writeResource writeBResource =
mkDict ((".",StackProg []):("version",StackSymbol version):
mkDict ((".",StackProg []):("steps.",StackProg []):("mustache.",StackProg []):("version",StackSymbol version):
[(x,StackBuiltin b) | (x,b) <- [
("def" , Builtin_Def ),
("$" , Builtin_DeRef ),
......
......@@ -3,7 +3,7 @@ module Data.CaPriCon(
-- * Expression nodes
IsCapriconString(..),BindType(..),Node(..),ApHead(..),Application(..),
-- ** Managing De Bruijin indices
adjust_depth,adjust_telescope_depth,inc_depth,free_vars,
adjust_depth,adjust_telescope_depth,inc_depth,free_vars,is_free_in,
-- ** General term substitution and type inference
subst,substn,type_of,mu_type,
-- ** Expression directories
......@@ -196,6 +196,14 @@ free_vars (Cons a) = freeA a
where envS = length env
free_vars _ = zero
is_free_in :: Int -> Node str -> Bool
is_free_in = map2 not go
where go v (Bind _ _ t e) = go v t && go (v+1) e
go v (Cons a) = go_a v a
go _ (Universe _) = True
go_a v (Ap (Sym v') subs) = v/=v' && all (go v) subs
go_a v (Ap (Mu env _ a) subs) = go_a (v+length env) a && all (go v) subs
subst :: (IsCapriconString str, MonadReader (Env str) m) => Node str -> Node str -> m (Node str)
subst = flip substn 0
substn :: (IsCapriconString str, MonadReader (Env str) m) => Node str -> Int -> Node str -> m (Node str)
......@@ -252,20 +260,14 @@ freshContext = go []
showNode = showNode' zero
showNode' :: IsCapriconString str => NodeDir str ([str],StringPattern str) -> [(str,Node str)] -> Node str -> str
showNode' dir = go 0
where go d env x | (pats,(_,k)):_ <- findPattern dir x =
let holes = c'map $ fromAList [(i,(env',hole)) | (env',i,hole) <- pats] in
par (if empty pats then 1000 else 1 :: Int) d $ intercalate (fromString " ") [
case word of
Left w -> w
Right i | Just (env',hole) <- lookup i holes -> go 2 (env'+env) hole
| otherwise -> zero
| word <- k]
where go d env x | Just ret <- toPat d env x = ret
go _ _ (Universe u) = "Set"+fromString (show u)
go d env whole@(Bind t aname atype body) | t == Lambda || 0`isKeyIn`free_vars body = par 0 d $ bind_head t + drop 1 (bind_tail env whole)
go d env whole@(Bind t aname atype body) | t == Lambda || 0`is_free_in`body = par 0 d $ bind_head t + drop 1 (bind_tail env whole)
| otherwise = par 0 d $ go 1 env atype + fromString " -> " + go 0 ((aname,atype):env) body
where bind_head Lambda = "λ"
bind_head Prod = "∀"
bind_tail env' (Bind t' x tx e) | t==t' && (t==Lambda || 0`isKeyIn`free_vars e) = fromString " ("+x'+fromString ":"+go 0 env' tx+fromString ")"+bind_tail ((x',tx):env') e
bind_tail env' x | Just ret <- toPat 0 (env'+env) x = ", "+ret
bind_tail env' (Bind t' x tx e) | t==t' && (t==Lambda || 0`is_free_in`e) = fromString " ("+x'+fromString ":"+go 0 env' tx+fromString ")"+bind_tail ((x',tx):env') e
where x' = fresh (map fst env') x
bind_tail env' x = ", "+go 0 env' x
go d env (Cons a) = showA d a
......@@ -278,6 +280,27 @@ showNode' dir = go 0
lvl = if empty xs then 1000 else 1
in par lvl d $ ni+foldMap ((" "+) . go 2 env) xs
toPat d env x
| (pats,(_,k)):_ <- findPattern dir x =
let holes = c'map $ fromAList [(i,(env',hole)) | (env',i,hole) <- pats] in
Just $ par (if empty pats then 1000 else 1 :: Int) d $ intercalate (fromString " ")
[case word of
Left w -> w
Right i | Just (env',hole) <- lookup i holes ->
go 2 env $
let (hole',env'') =
fix (\kj -> \case
(Cons (Ap h t@(_:_)),_:env0)
| Cons (Ap (Sym 0) []) <- debug $ last t
, not (is_free_in 0 (Cons (Ap h (init t))))
-> kj (inc_depth (-1) (Cons (Ap h (init t))),env0)
(Cons (Ap (Sym j') []),_:env0) | j'>0 -> kj (Cons (Ap (Sym (j'-1)) []),env0)
e -> e) (hole,env')
in foldl' (\e (n,t) -> Bind Lambda n t e) hole' env''
| otherwise -> zero
| word <- k]
| otherwise = Nothing
type_of :: (IsCapriconString str,MonadReader (Env str) m) => Node str -> m (Maybe (Node str))
type_of = yb maybeT . go
where go (Bind Lambda x tx e) = Bind Prod x tx <$> local (tx:) (go e)
......@@ -332,7 +355,7 @@ mu_type (inc_depth 1 -> root_type) = yb maybeT $ go 0 root_type
go_col' d' recs (Bind Prod x tx e) = Bind Prod x tx <$> local (tx:) (go_col' (d'+1) (map (+1) recs) e)
go_col' d' recs (Cons (Ap (Sym i) xs))
| constr_ind d d' i = do
let args = select (not . (`isKeyIn`recs)) [0..d'-1]
let args = reverse $ select (not . (`isKeyIn`recs)) [0..d'-1]
lastE = bind Lambda (adjust_telescope_depth second (+(d+d')) root_args)
(Cons (Ap (Sym (nargs-d-1))
[Cons (Ap (Sym (j'+nargs)) args')
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment