From 2731302c40b0f1e1c0227a4591cde9361ef35eef Mon Sep 17 00:00:00 2001 From: Marc Coiffier Date: Wed, 17 Oct 2018 20:23:32 +0200 Subject: [PATCH] Improve the showNode function to only show minimal patterns (using eta-equivalence); add support for inline code snippets in the WiQEE consoles --- capricon/capricon.cabal | 2 +- capricon/exe/WiQEE.hs | 72 +++++++++++++++++++---------------- capricon/src/CaPriCon/Run.hs | 6 +-- capricon/src/Data/CaPriCon.hs | 47 +++++++++++++++++------ 4 files changed, 79 insertions(+), 48 deletions(-) diff --git a/capricon/capricon.cabal b/capricon/capricon.cabal index 7ac85e7..b41afb8 100644 --- a/capricon/capricon.cabal +++ b/capricon/capricon.cabal @@ -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 diff --git a/capricon/exe/WiQEE.hs b/capricon/exe/WiQEE.hs index 57d17b0..121742e 100644 --- a/capricon/exe/WiQEE.hs +++ b/capricon/exe/WiQEE.hs @@ -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 diff --git a/capricon/src/CaPriCon/Run.hs b/capricon/src/CaPriCon/Run.hs index 1843ebe..27cc03c 100644 --- a/capricon/src/CaPriCon/Run.hs +++ b/capricon/src/CaPriCon/Run.hs @@ -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 ), diff --git a/capricon/src/Data/CaPriCon.hs b/capricon/src/Data/CaPriCon.hs index 48212a0..02cd539 100644 --- a/capricon/src/Data/CaPriCon.hs +++ b/capricon/src/Data/CaPriCon.hs @@ -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')