Run.hs 23.2 KB
Newer Older
1
{-# LANGUAGE CPP, NoMonomorphismRestriction, OverloadedStrings, ScopedTypeVariables, DeriveGeneric, ConstraintKinds, UndecidableInstances #-}
2
3
4
module CaPriCon.Run where

import Definitive
5
import Language.Format
6
7
import Algebra.Monad.Concatenative
import Data.CaPriCon
8
9
10
11
12
13
14
import GHC.Generics (Generic)

class Monad m => MonadSubIO io m where
  liftSubIO :: io a -> m a
instance MonadSubIO IO IO where liftSubIO = id
instance MonadSubIO io m => MonadSubIO io (ConcatT st b o s m) where
  liftSubIO ma = lift $ liftSubIO ma
15
16
17

takeLast n l = drop (length l-n) l

18
showStackVal :: IsCapriconString str => (NodeDoc str -> str) -> NodeDir str ([str],StringPattern str) -> [(str,Node str)] -> StackVal str (COCBuiltin io str) (COCValue io str) -> str
19
showStackVal toRaw dir ctx = fix $ \go _x -> case _x of
20
21
  StackExtra (Opaque _x) -> case _x of
    COCExpr d e -> -- "<"+show d+">:"+
22
      toRaw $ showNode' dir (map (second snd) $ takeLast d (freshContext ctx)) e
23
    COCNull -> "(null)"
24
    COCError e -> "<!"+e+"!>"
25
26
27
    COCDir d -> fromString $ show d
  StackSymbol s -> fromString $ show s
  StackInt n -> fromString $ show n
28
29
30
  StackList l -> "["+intercalate "," (map go l)+"]"
  StackDict d -> "[<"+intercalate "," (map (\(k,v) -> k+": "+go v) (d^.ascList))+">]"
  StackProg p -> "{ "+intercalate " " p+" }"
31
  _ -> fromString $ show _x
32
33
34
data COCBuiltin io str = COCB_Print
                       | COCB_Open (ReadImpl io str str) | COCB_ExecModule (WriteImpl io str str)
                       | COCB_Cache (ReadImpl io str [Word8]) (WriteImpl io str [Word8])
35
36
37
38
39
40
41
42
43
                       | COCB_ToInt | COCB_Concat | COCB_Uni | COCB_Hyp
                       | COCB_Quit | COCB_Var
                       | COCB_Ap | COCB_Bind Bool BindType
                       | COCB_TypeOf | COCB_Mu
                       | COCB_HypBefore | COCB_Subst | COCB_Rename
                       | COCB_ContextVars
                       | COCB_GetShowDir | COCB_SetShowDir | COCB_InsertNodeDir
                       | COCB_Format
                       deriving (Show,Generic)
44
45
46
47
data ReadImpl io str bytes = ReadImpl (str -> io (Maybe bytes))
data WriteImpl io str bytes = WriteImpl (str -> bytes -> io ())
instance Show (ReadImpl io str bytes) where show _ = "#<open>"
instance Show (WriteImpl io str bytes) where show _ = "#<write>"
48

49
50
type ListSerializable a = (Serializable Word8 ([Word8] -> [Word8]) [Word8] a)
type ListFormat a = (Format Word8 ([Word8] -> [Word8]) [Word8] a)
51
52
53
54
type IOListFormat io str = (ListFormat (ReadImpl io str str), ListFormat (WriteImpl io str str),
                            ListFormat (ReadImpl io str [Word8]), ListFormat (WriteImpl io str [Word8]))
instance Serializable Word8 ([Word8] -> [Word8]) [Word8] (ReadImpl io str bytes) where encode _ _ = id
instance Serializable Word8 ([Word8] -> [Word8]) [Word8] (WriteImpl io str bytes) where encode _ _ = id
55
instance ListSerializable str => ListSerializable (COCBuiltin io str)
56
instance (ListFormat str,IOListFormat io str) => ListFormat (COCBuiltin io str)
57

58
59
htmlQuote :: IsCapriconString str => str -> str
htmlQuote = fromString . foldMap qChar . toString
60
61
62
63
  where qChar '<' = "&lt;"
        qChar '>' = "&gt;"
        qChar '&' = "&amp;"
        qChar c = [c]
64
65
66
stringWords :: IsCapriconString str => str -> [str]
stringWords = map fromString . fromBlank . toString
  where fromBlank (c:t) | c `elem` [' ', '\t', '\r', '\n'] = fromBlank t
67
68
69
70
71
72
73
74
                        | c == '"' = fromQuote id t
                        | otherwise = fromWChar (c:) t
        fromBlank "" = []
        fromQuote k ('"':t) = ('"':k "\""):fromBlank t
        fromQuote k ('\\':c:t) = fromQuote (k.(qChar c:)) t
          where qChar 'n' = '\n' ; qChar 't' = '\t' ; qChar x = x
        fromQuote k (c:t) = fromQuote (k.(c:)) t
        fromQuote k "" = ['"':k "\""]
75
        fromWChar k (c:t) | c `elem` [' ', '\t', '\r', '\n'] = k "":fromBlank t
76
77
78
                          | otherwise = fromWChar (k.(c:)) t
        fromWChar k "" = [k ""]

79
80
81
82
83
84
85
86
87
literate :: forall str. IsCapriconString str => Parser String [str]
literate = intercalate [":s\n"] <$> sepBy' (cmdline "> " <+? cmdline "$> " <+? commentline) (single '\n')
  where
    wrapResult :: Bool -> [str] -> [str]
    wrapResult isParagraph l = (if isParagraph then ":rbp" else ":rbs") : l + [if isParagraph then ":rep" else ":res"]
    cmdline :: Parser String () -> Parser String [str]
    cmdline pre = map (\x -> [":cp"+intercalate "\n" (map fst x)]
                             + wrapResult True (foldMap snd x))
                  (sepBy1' go (single '\n'))
88
      where go = do pre; many' (noneOf ['\n']) <&> \x -> (fromString x,map fromString (stringWords x+["steps."]))
89
90
91
92
93
    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 ['}'])))
94
                                 <&> \x -> (fromString x,wrapResult False (stringWords (fromString x)+["mustache."])))))
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110

data COCState str = COCState {
  _endState :: Bool,
  _context :: [(str,Node str)],
  _showDir :: NodeDir str ([str],StringPattern str),
  _outputText :: str -> str
  }
endState :: Lens' (COCState str) Bool
endState = lens _endState (\x y -> x { _endState = y })
context :: Lens' (COCState str) [(str,Node str)]
context = lens _context (\x y -> x { _context = y })
showDir :: Lens' (COCState str) (NodeDir str ([str],StringPattern str))
showDir = lens _showDir (\x y -> x { _showDir = y })
outputText :: Lens' (COCState str) (str -> str)
outputText = lens _outputText (\x y -> x { _outputText = y })

111
112
113
114
pushError :: MonadStack (COCState str) str (COCBuiltin io str) (COCValue io str) m => str -> m ()
pushError s = runStackState $ modify $ (StackExtra (Opaque (COCError s)):)

runCOCBuiltin :: (MonadSubIO io m,IsCapriconString str, MonadStack (COCState str) str (COCBuiltin io str) (COCValue io str) m,IOListFormat io str,ListFormat str) => COCBuiltin io str -> m ()
115
116
117
118
119
120
121
122
123
124
runCOCBuiltin COCB_Quit = runExtraState (endState =- True)
runCOCBuiltin COCB_Print = do
  s <- runStackState get
  for_ (take 1 s) $ \case
    StackSymbol s' -> runExtraState (outputText =~ \o t -> o (s'+t))
    _ -> return ()

runCOCBuiltin COCB_Format = do
  ex <- runExtraState get
  let format ('%':'s':s) (StackSymbol h:t) = first (h+) (format s t)
125
126
      format ('%':'v':s) (x:t) = first (showStackVal doc2raw (ex^.showDir) (ex^.context) x+) (format s t)
      format ('%':'l':s) (x:t) = first (showStackVal doc2latex (ex^.showDir) (ex^.context) x+) (format s t)
127
      format (c:s) t = first (fromString [c]+) (format s t)
128
129
      format "" t = ("",t)
  runStackState $ modify $ \case
130
    StackSymbol s:t -> uncurry ((:) . StackSymbol) (format (toString s) t)
131
132
    st -> st

133
runCOCBuiltin (COCB_Open (ReadImpl getResource)) = do
134
135
136
  s <- runStackState get
  case s of
    StackSymbol f:t -> do
137
      xs <- liftSubIO (getResource (f+".md")) >>= maybe undefined return . matches Just literate . maybe "" toString
138
139
      runStackState (put (StackProg xs:t))
    _ -> return ()
140
                     
141
runCOCBuiltin COCB_ToInt = runStackState $ modify $ \case
142
  StackSymbol s:t -> StackInt (read (toString s)):t
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
  st -> st
runCOCBuiltin COCB_Concat = runStackState $ modify $ \case
  StackSymbol s:StackSymbol s':t -> StackSymbol (s'+s):t
  st -> st

runCOCBuiltin COCB_Uni = do
  ctx <- runExtraState (getl context)
  runStackState $ modify $ \case
    StackInt n:t -> StackExtra (Opaque (COCExpr (length ctx) (Universe n))):t
    st -> st
runCOCBuiltin COCB_Var = do
  ctx <- runExtraState (getl context)
  runStackState $ modify $ \case
    StackSymbol name:t | Just i <- lookup name (zipWith (second . const) [0..] (freshContext ctx)) ->
                         StackExtra (Opaque (COCExpr (length ctx) (Cons (Ap (Sym i) [])))):t
    st -> st
runCOCBuiltin COCB_Ap = do
  ctx <- runExtraState (getl context)
  let adj d dd x = inc_depth (dd+nctx-d) x
      nctx = length ctx
      env = map snd ctx
  runStackState $ modify $ \case
    (StackExtra (Opaque (COCExpr df f)):StackExtra (Opaque (COCExpr dx x)):t) ->
      let x' = adj dx 1 x ; f' = adj df 0 f in
        StackExtra (Opaque (COCExpr nctx (subst f' (Cons (Ap (Sym 0) [x'])) env))):t
    x -> x
runCOCBuiltin (COCB_Bind close bt) = do
  ctx <- runExtraState (getl context) 
  let d = length ctx
      setVal (StackExtra (Opaque (COCExpr d' e')))
        | i <- d-d'
        , d==d' || not close
        , (_,(x,tx):_) <- splitAt i ctx
        = StackExtra (Opaque (COCExpr (d'-1) (Bind bt x tx e')))
      setVal (StackDict dict) = StackDict (map setVal dict)
      setVal (StackList l) = StackList (map setVal l)
      setVal x = x
      setStack (x:t) = setVal x:if close then setStack t else t
      setStack [] = []
                                                         
  ctx' <- runStackState $ id <~ map (,if close && nonempty ctx then tail ctx else ctx) setStack
  runDictState $ modify $ map setVal
  runExtraState (context =- ctx')
runCOCBuiltin COCB_Mu = do
  ctx <- runExtraState (getl context)
  let locEnv d = map snd (takeLast d ctx)
  runStackState $ modify $ \case
    StackExtra (Opaque (COCExpr d e)):t -> 
      case type_of e (locEnv d) >>= \te -> mu_type te (locEnv d) of
        Just mte -> let args (Bind Prod _ tx e') = tx:args e'
                        args _ = []
                    in (:t) $ StackExtra $ Opaque $ COCExpr d $
                       subst e (Cons (Ap (Mu [] (args mte) (Ap (Sym 0) [])) [])) (locEnv d)
        Nothing -> StackExtra (Opaque COCNull):t
    st -> st
runCOCBuiltin COCB_TypeOf = do
  ctx <- runExtraState (getl context)
  runStackState $ modify $ \case
    StackExtra (Opaque (COCExpr d (Cons (Ap (Sym i) [])))):t
      | (_,ti):_ <- drop i ctx ->
          StackExtra (Opaque (COCExpr (d-i-1) ti)):t
    StackExtra (Opaque (COCExpr d e)):t -> (:t) $ StackExtra $ Opaque $ case type_of e (takeLast d (map snd ctx)) of
      Just te -> COCExpr d te
      Nothing -> COCNull
    st -> st

209
runCOCBuiltin (COCB_ExecModule (WriteImpl writeResource)) = do
210
211
212
213
214
215
216
217
  st <- runStackState get
  case st of
    StackSymbol f:StackProg p:t -> do
      old <- runDictState get
      oldH <- runExtraState (outputText <~ \x -> (id,x))
      traverse_ (execSymbol runCOCBuiltin outputComment) p
      new <- runDictState (id <~ (old,))
      newH <- runExtraState (outputText <~ \x -> (oldH,x))
218
      liftSubIO $ writeResource f (newH "")
219
220
221
      runStackState $ put $ StackDict new:t
    _ -> return ()

222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
runCOCBuiltin (COCB_Cache (ReadImpl getResource) (WriteImpl writeResource)) = do
  st <- runStackState get
  case st of
    StackSymbol f:StackProg p:t -> do
      runStackState (put t)
      liftSubIO (getResource (f+".blob")) >>= \case
        Just res | Just v <- matches Just datum res -> runStackState $ modify $ (v:)
        _ -> do
          traverse_ (execSymbol runCOCBuiltin outputComment) p
          st' <- runStackState get
          case st' of
            v:_ -> liftSubIO $ writeResource (f+".blob") (serialize v)
            _ -> unit
    _ -> pushError "Invalid argument types for builtin 'cache'. Usage: <prog> <string> cache."

237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
runCOCBuiltin COCB_Hyp = do
  ass <- runStackState $ id <~ \case
    StackSymbol name:StackExtra (Opaque (COCExpr d typ)):t -> (t,Just (d,(name,typ)))
    st -> (st,Nothing)
  case ass of
    Just (d,x) -> runExtraState $ context =~ \ctx -> (second (inc_depth (length ctx-d)) x:ctx)
    Nothing -> return ()
runCOCBuiltin COCB_HypBefore = do
  ctx <- runExtraState (getl context)
  let csz = length ctx
      adj hi i j = if i+j>=hi then j+1 else j
  ctx' <- runStackState $ id <~ \case
    StackSymbol h:StackSymbol h':StackExtra (Opaque (COCExpr d e)):t
      | (hi,_):_ <- select ((==h) . fst . snd) (zip [0..] ctx)
      , all (>hi+d-csz) (free_vars e) ->
        let ctx' = foldr (\x k i -> case compare hi i of
                             LT -> x:k (i+1)
                             EQ -> second (adjust_depth (adj hi i)) x:(h',inc_depth (csz-(d+hi+1)) e):k (i+1)
                             GT -> second (adjust_depth (adj hi i)) x:k (i+1))
                   (\_ -> []) ctx 0
            adjE x@(StackExtra (Opaque (COCExpr d' e'))) =
              let i = csz-d'
              in if i<=hi then StackExtra (Opaque (COCExpr (d+1) (adjust_depth (adj (hi+1) i) e')))
                 else x
            adjE x = x
        in (map adjE t,ctx')
    st -> (st,ctx)
  runExtraState (context =- ctx')
runCOCBuiltin COCB_Subst = do
  ctx <- runExtraState (getl context)
  let csz = length ctx
  ctx' <- runStackState $ id <~ \case
    StackSymbol h:StackExtra (Opaque (COCExpr d e)):t
      | (hi,_):_ <- select ((==h) . fst . snd) (zip [0..] ctx)
      , all (>hi+d-csz) (free_vars e) ->
        let ctx' = foldr (\x k i env -> case compare i hi of
                             LT -> second (\xv -> substn e (hi-i) xv env) x:k (i+1) (tail env)
                             EQ -> k (i+1) (tail env)
                             GT -> x:k (i+1) (tail env)) (\_ _ -> []) ctx 0 (map snd ctx)
            adjE x@(StackExtra (Opaque (COCExpr d' e'))) =
              let i = csz - d'
              in if i<=hi then StackExtra (Opaque (COCExpr (d-1) ((substn e (hi-i) e' (map snd (drop i ctx))))))
                 else x
            adjE x = x
        in (map adjE t,ctx')
    st -> (st,ctx)
  runExtraState (context =- ctx')
runCOCBuiltin COCB_Rename = do
  ctx <- runExtraState (getl context)
  ctx' <- runStackState $ id <~ \case
287
    StackSymbol s:StackSymbol s':t -> (t,map (\(n',(n,v)) -> (if n'==s then s' else n, v)) (freshContext ctx))
288
289
290
291
292
293
294
295
296
297
298
299
300
301
    st -> (st,ctx)
  runExtraState (context =- ctx')
runCOCBuiltin COCB_ContextVars = do
  ctx <- runExtraState (getl context)
  runStackState $ modify (StackList (map (StackSymbol . fst) (freshContext ctx)):)

runCOCBuiltin COCB_GetShowDir = do
  dir <- runExtraState (getl showDir)
  runStackState $ modify $ (StackExtra (Opaque (COCDir (map (\(c,l) -> (c,StackSymbol (intercalate " " $ map (id <|> head . flip drop c) l))) dir))):)
runCOCBuiltin COCB_SetShowDir = do
  mod' <- runStackState $ id <~ \case
    StackExtra (Opaque (COCDir d)):t -> (t,showDir =- map (\(c,StackSymbol ws) -> (c,[case select ((==w) . fst) (zip c [0..]) of
                                                                                        (_,i):_ -> Right i
                                                                                        _ -> Left w
302
                                                                                     | w <- map fromString $ words (toString ws)])) d)
303
304
305
306
307
308
309
310
311
    st -> (st,return ())
  runExtraState mod'
runCOCBuiltin COCB_InsertNodeDir = do
  ctx <- runExtraState (getl context)
  runStackState $ modify $ \case
    x:StackExtra (Opaque (COCExpr d e)):StackExtra (Opaque (COCDir dir)):t ->
      StackExtra (Opaque (COCDir (insert e (map fst (takeLast d ctx),x) dir))):t
    st -> st

312
type MaxDelta = Int
313
314
315
316
317
type UniverseConstraint = [Maybe MaxDelta]
data UniverseConstraints = UniverseConstraints [UniverseConstraint]
instance Semigroup UniverseConstraints where
  UniverseConstraints x + UniverseConstraints y = UniverseConstraints $ zipWith (zipWith (\_x _y -> zipWith max _x _y + _x + _y)) x y
instance Monoid UniverseConstraints where zero = UniverseConstraints (repeat (repeat Nothing))
318
319
320
data COCValue io str = COCExpr Int (Node str)
                     | COCNull | COCError str
                     | COCDir (NodeDir str ([str],StackVal str (COCBuiltin io str) (COCValue io str)))
321
322
323
324
325
326
327
328
329
                     deriving Generic
instance (ListSerializable s,ListSerializable b,ListSerializable a) => ListSerializable (StackVal s b a)
instance (IsCapriconString s,ListFormat s,ListFormat b,ListFormat a) => ListFormat (StackVal s b a)
instance (ListSerializable b) => ListSerializable (StackBuiltin b)
instance (ListFormat b) => ListFormat (StackBuiltin b)
instance (ListSerializable a) => ListSerializable (Opaque a)
instance (ListFormat a) => ListFormat (Opaque a)

instance ListSerializable str => ListSerializable (COCValue io str)
330
instance (IsCapriconString str,ListFormat str,IOListFormat io str) => ListFormat (COCValue io str)
331
type COCDict io str = Map str (StackVal str (COCBuiltin io str) (COCValue io str))
332

333
334
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 =
335
  mkDict ((".",StackProg []):("steps.",StackProg []):("mustache.",StackProg []):("version",StackSymbol version):
336
337
338
339
340
341
342
343
344
           [(x,StackBuiltin b) | (x,b) <- [
               ("def"                     , Builtin_Def                           ),
               ("$"                       , Builtin_DeRef                         ),
               ("lookup"                  , Builtin_Lookup                        ),
               ("exec"                    , Builtin_Exec                          ),
               ("quote"                   , Builtin_Quote                         ),

               ("stack"                   , Builtin_Stack                         ),
               ("clear"                   , Builtin_Clear                         ),
345
346
               ("shift"                   , Builtin_Shift                         ),
               ("shaft"                   , Builtin_Shaft                         ),
347
348
349
350
351
352
353
354
355
356
357
358
359
               ("pop"                     , Builtin_Pop                           ),
               ("popn"                    , Builtin_PopN                          ),
               ("dup"                     , Builtin_Dup                           ),
               ("dupn"                    , Builtin_DupN                          ),
               ("swap"                    , Builtin_Swap                          ),
               ("swapn"                   , Builtin_SwapN                         ),
               ("pick"                    , Builtin_Pick                          ),

               ("["                       , Builtin_ListBegin                     ),
               ("]"                       , Builtin_ListEnd                       ),
               
               ("io/exit"                 , Builtin_Extra COCB_Quit               ),
               ("io/print"                , Builtin_Extra COCB_Print              ),
360
361
362
               ("io/source"               , Builtin_Extra (COCB_Open (ReadImpl getResource))), 
               ("io/cache"                , Builtin_Extra (COCB_Cache (ReadImpl getBResource) (WriteImpl writeBResource))),
                 
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
               ("string/format"           , Builtin_Extra COCB_Format             ),
               ("string/to-int"           , Builtin_Extra COCB_ToInt              ),
               
               ("arith/+"                 , Builtin_Add                           ),
               ("arith/-"                 , Builtin_Sub                           ),
               ("arith/*"                 , Builtin_Mul                           ),
               ("arith/div"               , Builtin_Div                           ),
               ("arith/mod"               , Builtin_Mod                           ),
               ("arith/sign"              , Builtin_Sign                          ),
               
               ("list/each"               , Builtin_Each                          ),
               ("list/range"              , Builtin_Range                         ),

               ("dict/vocabulary"         , Builtin_CurrentDict                   ),
               ("dict/empty"              , Builtin_Empty                         ),
               ("dict/insert"             , Builtin_Insert                        ),
               ("dict/delete"             , Builtin_Delete                        ),
               ("dict/keys"               , Builtin_Keys                          ),
381
               ("dict/module"             , Builtin_Extra (COCB_ExecModule (WriteImpl writeResource))),
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402

               ("term-index/pattern-index"     , Builtin_Extra COCB_GetShowDir         ),
               ("term-index/set-pattern-index" , Builtin_Extra COCB_SetShowDir         ),
               ("term-index/index-insert"      , Builtin_Extra COCB_InsertNodeDir      ),
               
               ("term/universe"            , Builtin_Extra COCB_Uni                ),
               ("term/variable"            , Builtin_Extra COCB_Var                ),
               ("term/apply"               , Builtin_Extra COCB_Ap                 ),
               ("term/lambda"              , Builtin_Extra (COCB_Bind False Lambda )),
               ("term/forall"              , Builtin_Extra (COCB_Bind False Prod   )  ),
               ("term/mu"                  , Builtin_Extra COCB_Mu                 ),

               ("context/intro"           , Builtin_Extra COCB_Hyp                ),
               ("context/intro-before"    , Builtin_Extra COCB_HypBefore          ),
               ("context/extro-lambda"    , Builtin_Extra (COCB_Bind True Lambda  ) ),
               ("context/extro-forall"    , Builtin_Extra (COCB_Bind True Prod    )   ),
               ("context/rename"          , Builtin_Extra COCB_Rename             ),
               ("context/substitute"      , Builtin_Extra COCB_Subst              ),
               ("context/type"            , Builtin_Extra COCB_TypeOf             ),
               ("context/hypotheses"      , Builtin_Extra COCB_ContextVars        )
               ]])
403
404
405
406
  where mkDict :: [(str,StackVal str (COCBuiltin io str) (COCValue io str))] -> Map str (StackVal str (COCBuiltin io str) (COCValue io str))
        mkDict = foldr addElt (c'map zero)
        addElt (x,v) = atP (first fromString $ splitPath $ toString x) %- Just v
        splitPath ('/':x) = ("",uncurry (:) (first fromString $ splitPath x))
407
408
409
410
411
        splitPath (h:t) = let ~(w,l) = splitPath t in (h:w,l)
        splitPath [] = ("",[])
        atP (h,[]) = at h
        atP (h,x:t) = at h.l'Just (StackDict zero).t'StackDict.atP (x,t)

412
413
414
415
416
417
418
419
420
421
422
423
outputComment c = (runExtraState $ do outputText =~ (\o t -> o (commentText+t)))
  where commentText = case toString c of
          'r':'b':p:[] -> let x = if p=='p' then "paragraph" else ""
                              tag = if p=='p' then "div" else "span"
                          in "<"+tag+" class=\"capricon-"+x+"result\">"
          'r':'e':p:[] -> "</"+(if p=='p' then "div" else "span")+">"
          'c':'p':_ -> let nlines = length (lines (toString c))
                       in wrapStart True nlines+"<div class=\"capricon-steps\"><pre class=\"capricon capricon-paragraph capricon-context\">"
                          +htmlQuote (drop 2 c)+"</pre>"+userInput+"</div>"+wrapEnd
          'c':'s':_ -> wrapStart False 1+"<code class=\"capricon\">"+htmlQuote (drop 2 c)+"</code>"+wrapEnd
          's':_ -> drop 1 c
          _ -> ""
424

425
426
427
428
429
430
        wrapStart isP nlines =
          let hide = if isP then "hideparagraph" else "hidestache"
          in "<label class=\"hide-label\"><input type=\"checkbox\" class=\"capricon-hide\" checked=\"checked\"/><span class=\"capricon-"
             + hide +"\"></span><span class=\"capricon-reveal\" data-linecount=\""
             + fromString (show nlines)+"\">"
        wrapEnd = "</span></label>"
431
        userInput = "<div class=\"user-input\"><button class=\"capricon-trigger\">Open/Close console</button><span class=\"capricon-input-prefix\">Evaluate in this context (press Enter to run):</span><input type=\"text\" class=\"capricon-input\" /><pre class=\"capricon-output\"></pre></div>"
432