Implement a 'pull' builtin to precisely manage the scope of terms on the...

Implement a 'pull' builtin to precisely manage the scope of terms on the stack; merge the 'intro' and 'intro-before' builtins

capricon/capricon.cabal

@@ -2,7 +2,7 @@
 -- see http://haskell.org/cabal/users-guide/
 
 name:                capricon
-version:             0.9.2
+version:             0.10
 -- synopsis:            
 -- description:         
 license:             GPL-3
@@ -35,7 +35,7 @@ executable capricon
   default-extensions: RebindableSyntax, ViewPatterns, TupleSections, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies, LambdaCase, TypeOperators, RankNTypes, GeneralizedNewtypeDeriving, TypeFamilies
   -- other-modules:       
   -- other-extensions:    
-  build-depends: base >=4.8 && <4.10,capricon >=0.9 && <0.10,definitive-base >=2.6 && <2.7,definitive-parser >=3.1 && <3.2
+  build-depends: base >=4.8 && <4.10,capricon >=0.10 && <0.11,definitive-base >=2.6 && <2.7,definitive-parser >=3.1 && <3.2
   ghc-options: -Wincomplete-patterns -Wname-shadowing -W -Werror
   hs-source-dirs:      exe
   default-language:    Haskell2010
@@ -47,7 +47,7 @@ executable WiQEE.js
   -- other-modules:       
   -- other-extensions:    
   haste-options: --opt-all
-  build-depends: array >=0.5 && <0.6,base >=4.8 && <4.10,capricon >=0.9 && <0.10,definitive-base >=2.6 && <2.7,definitive-parser >=3.1 && <3.2,filepath >=1.4 && <1.5,haste-lib
+  build-depends: array >=0.5 && <0.6,base >=4.8 && <4.10,capricon >=0.10 && <0.11,definitive-base >=2.6 && <2.7,definitive-parser >=3.1 && <3.2,filepath >=1.4 && <1.5,haste-lib
   hs-source-dirs:      exe
   default-language:    Haskell2010
 -- executable coinche
@@ -55,7 +55,7 @@ executable WiQEE.js
 --   default-extensions:  RebindableSyntax
 --   -- other-modules:       
 --   -- other-extensions:    
---  build-depends: base >=4.8 && <4.10,definitive-base >=2.6 && <2.7,definitive-parser >=3.1 && <3.2,random >=1.1 && <1.2,random-shuffle
+--  build-depends: base >=4.9 && <4.10,definitive-base >=2.6 && <2.7,definitive-parser >=3.1 && <3.2,random >=1.1 && <1.2,random-shuffle
 --   ghc-options: -Wincomplete-patterns -Wname-shadowing -Werror
 --   hs-source-dirs:      exe
 --   default-language:    Haskell2010

capricon/data/prelude

@@ -35,7 +35,7 @@
 
 'vis { show-context "-------\n" printf show-stack } def
 
-'-> { dup 1 swapn swap intro dup [ swap "'%s" format 'variable ] quote def } def
+'-> { dup 1 swapn swap intro { {@ dup @} variable } def } def
 '! 'extro-lambda $ def
 '? 'extro-forall $ def
 
@@ -50,3 +50,9 @@
 ') { ] applyl } def
 
 'defconstr { 1 dupn swap showdef def } def
+
+'mustache. { show } def
+'tex { 'mustache. { "$%l$\n" printf 'mustache. {@ dup $ @} def } def } def
+'raw { 'mustache. { "%s\n" printf 'mustache. {@ dup $ @} def } def } def
+
+'recursor { dup 2 shaft -> variable mu ! } def

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.9.2-js" :: String) getString getBytes setString setBytes
+hasteDict = cocDict ("0.10-js" :: String) getString getBytes setString setBytes
 
 main :: IO ()
 main = JS.concurrent $ void $ do

capricon/src/CaPriCon/Run.hs

@@ -69,17 +69,26 @@ showStackVal toRaw dir ctx = fix $ \go _x -> case _x of
         showClosure (StackClosure cs c) = "{ "+intercalate " " (map (\(i,c') -> showSteps i+" "+showClosure c') cs + map showStep c)+" }"
     in "{ "+showSteps p+" }"
   _ -> fromString $ show _x
-data COCBuiltin io str = COCB_Print
+data COCBuiltin io str = COCB_Print | COCB_Quit
                        | COCB_Open (ReadImpl io str str) | COCB_ExecModule (WriteImpl io str str)
                        | COCB_Cache (ReadImpl io str [Word8]) (WriteImpl io str [Word8])
-                       | COCB_ToInt | COCB_Concat | COCB_Uni | COCB_Hyp
-                       | COCB_Quit | COCB_Var
-                       | COCB_Ap | COCB_Bind Bool BindType
-                       | COCB_TypeOf | COCB_Mu | COCB_Convertible
-                       | COCB_HypBefore | COCB_Subst | COCB_Rename
-                       | COCB_ContextVars | COCB_Axiom
+
+                       | COCB_ToInt | COCB_Concat
+
+                       | COCB_Bind Bool BindType
+                       | COCB_Uni | COCB_Var | COCB_Mu | COCB_Ap | COCB_Axiom
+
+                       | COCB_TypeOf | COCB_Convertible
+                       | COCB_Extract | COCB_MatchTerm
+                       
+                       | COCB_Intro | COCB_Subst | COCB_Rename
+                       | COCB_Pull
+
+                       | COCB_ContextVars
                        | COCB_GetShowDir | COCB_SetShowDir | COCB_InsertNodeDir
-                       | COCB_Format | COCB_Extract | COCB_MatchTerm
+
+                       | COCB_Format
+                       
                        deriving (Show,Generic)
 data ReadImpl io str bytes = ReadImpl (str -> io (Maybe bytes))
 data WriteImpl io str bytes = WriteImpl (str -> bytes -> io ())
@@ -222,7 +231,7 @@ runCOCBuiltin COCB_Uni = do
 runCOCBuiltin COCB_Var = do
   ctx <- runExtraState (getl context)
   runStackState $ modify $ \case
-    StackSymbol name:t | Just e <- runInContext ctx (pullTerm =<< mkVariable name) -> StackCOC (COCExpr e):t
+    StackSymbol name:t | Just e <- runInContext (map (\(x,(_,v)) -> (x,v)) $ freshContext ctx) (mkVariable name) -> StackCOC (COCExpr e):t
     st -> st
 runCOCBuiltin COCB_Ap = do
   ctx <- runExtraState (getl context)
@@ -252,6 +261,7 @@ runCOCBuiltin COCB_Mu = do
                            | otherwise -> StackCOC COCNull:t
     st -> st
 
+
 runCOCBuiltin COCB_MatchTerm = do
   st <- runStackState get
   cctx <- runExtraState (getl context)
@@ -303,6 +313,16 @@ runCOCBuiltin COCB_Convertible = do
       StackCOC (COCConvertible (runInContext ctx $ conversionDelta e e')):t
     st -> st
 
+runCOCBuiltin COCB_Pull = do
+  ctx <- runExtraState (getl context)
+  runStackState $ modify $ \case
+    StackCOC (COCExpr e):st | Just e' <- runInContext ctx (pullTerm Nothing e) -> StackCOC (COCExpr e'):st
+                            | otherwise -> StackCOC COCNull:st
+    StackSymbol s:StackCOC (COCExpr e):st
+      | Just e' <- runInContext ctx (pullTerm (Just s) e) -> StackCOC (COCExpr e'):st
+      | otherwise -> StackCOC COCNull:st
+    st -> st
+
 runCOCBuiltin (COCB_ExecModule (WriteImpl writeResource)) = do
   st <- runStackState get
   case st of
@@ -331,21 +351,17 @@ runCOCBuiltin (COCB_Cache (ReadImpl getResource) (WriteImpl writeResource)) = do
             _ -> unit
     _ -> pushError "Invalid argument types for builtin 'cache'. Usage: <prog> <string> cache."
 
-runCOCBuiltin COCB_Hyp = do
+runCOCBuiltin COCB_Intro = do
   ctx <- runExtraState (getl context)
   s <- runStackState $ id <~ \case
+    StackCOC (COCExpr e):t -> (t,runInContext ctx (insertHypBefore Nothing "_" e))
     StackSymbol name:StackCOC (COCExpr e):t
       -> (t,runInContext ctx (insertHypBefore Nothing name e))
+    StackSymbol limit:StackSymbol name:StackCOC (COCExpr e):t
+      -> (t,runInContext ctx (insertHypBefore (Just limit) name e))
     st -> (st,Nothing)
   modifyCOCEnv s
   
-runCOCBuiltin COCB_HypBefore = do
-  ctx <- runExtraState (getl context)
-  s <- runStackState $ id <~ \case
-    StackSymbol h:StackSymbol h':StackCOC (COCExpr e):t
-      -> (t,runInContext ctx (insertHypBefore (Just h) h' e))
-    st -> (st,Nothing)
-  modifyCOCEnv s
 runCOCBuiltin COCB_Subst = do
   ctx <- runExtraState (getl context)
   s <- runStackState $ id <~ \case
@@ -441,24 +457,25 @@ cocDict version getResource getBResource writeResource writeBResource =
                ("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                 ),
-               ("term/convertible"         , Builtin_Extra COCB_Convertible        ),
-               ("term/axiom"               , Builtin_Extra COCB_Axiom              ),
-               ("term/extract"             , Builtin_Extra COCB_Extract            ),
-               ("term/match"               , Builtin_Extra COCB_MatchTerm          ),
-
-               ("context/intro"           , Builtin_Extra COCB_Hyp                ),
-               ("context/intro-before"    , Builtin_Extra COCB_HypBefore          ),
+               ("construction/universe"            , Builtin_Extra COCB_Uni                ),
+               ("construction/variable"            , Builtin_Extra COCB_Var                ),
+               ("construction/apply"               , Builtin_Extra COCB_Ap                 ),
+               ("construction/lambda"              , Builtin_Extra (COCB_Bind False Lambda)),
+               ("construction/forall"              , Builtin_Extra (COCB_Bind False Prod  )),
+               ("construction/mu"                  , Builtin_Extra COCB_Mu                 ),
+               ("construction/axiom"               , Builtin_Extra COCB_Axiom              ),
+               ("construction/pull"                , Builtin_Extra COCB_Pull               ),
+               
+               ("query/convertible"         , Builtin_Extra COCB_Convertible        ),
+               ("query/extract"             , Builtin_Extra COCB_Extract            ),
+               ("query/match"               , Builtin_Extra COCB_MatchTerm          ),
+               ("query/type"                , Builtin_Extra COCB_TypeOf             ),
+               
+               ("context/intro"           , Builtin_Extra COCB_Intro                ),
                ("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        )
                ]])
   where mkDict :: [(str,StackVal str (COCBuiltin io str) (COCValue io str))] -> Map str (StackVal str (COCBuiltin io str) (COCValue io str))

capricon/src/Data/CaPriCon.hs

@@ -85,7 +85,7 @@ class Monad m => COCExpression str m e | e -> str where
   conversionDelta :: e -> e -> m (UniverseSize,UniverseSize)
 
   substHyp :: str -> e -> m (e -> e,Env str (Axiom e))
-  pullTerm :: e -> m e
+  pullTerm :: Maybe str -> e -> m e
   insertHypBefore :: Maybe str -> str -> e -> m (e -> e,Env str (Axiom e))
 instance (Show a,IsCapriconString str,Monad m,MonadReader (Env str a) m) => COCExpression str (MaybeT m) (Node str a) where
   type Axiom (Node str a) = a
@@ -110,7 +110,7 @@ instance (Show a,IsCapriconString str,Monad m,MonadReader (Env str a) m) => COCE
     lift $ do
       ctx <- ask
       return (substn x i,let (ch,ct) = splitAt i ctx in zipWith (\j -> second $ substn (inc_depth (negate (1+j)) x) (i-j-1)) [0..] ch+drop 1 ct)
-  pullTerm = return
+  pullTerm _ = return
   insertHypBefore Nothing h th = lift $ do
     ctx <- ask
     return (inc_depth 1,(h,th):ctx)
@@ -156,19 +156,24 @@ instance (Show a,IsCapriconString str,MonadReader (Env str a) m,Monad m) => COCE
       local (restrictEnv dm)
       $ conversionDelta (inc_depth (dm-da) a) (inc_depth (dm-db) b)
   
-  pullTerm (ContextNode d e) = ask <&> \l -> ContextNode (length l) (inc_depth (length l-d) e)
+  pullTerm Nothing (ContextNode d e) = ask <&> \l -> ContextNode (length l) (inc_depth (length l-d) e)
+  pullTerm (Just v) (ContextNode d e) = do
+    nctx <- length <$> ask
+    i <- hypIndex v
+    let d' = nctx-(i+1)
+    guard (d'>=d || all (\j -> d'+j >= d) (free_vars e))
+    return (ContextNode d' $ inc_depth (d'-d) e)
+
   substHyp h vh = do
-    hi <- hypIndex h
-    ContextNode dm vh' <- pullTerm vh
+    ContextNode dm vh' <- pullTerm (Just h) vh
     first (\f cv@(ContextNode d v) ->
-             if d+hi <= dm then cv
+             if d <= dm then cv
              else ContextNode (d-1) (inc_depth (d-dm) $ f $ inc_depth (dm-d) v)) <$>
       substHyp h vh'
   insertHypBefore h h' cth' = do
-    ContextNode dh th' <- pullTerm cth'
-    hi <- maybe (return (-1)) hypIndex h
+    ContextNode dh th' <- pullTerm h cth'
     first (\f cx@(ContextNode d x) ->
-             if d+hi < dh then cx
+             if d <= dh then cx
              else ContextNode (d+1) (inc_depth (d-dh) $ f $ inc_depth (dh-d) x))
             <$> insertHypBefore h h' th'
 

logos/logos.cabal

@@ -19,7 +19,7 @@ library
   default-language:    Haskell2010
 
 executable logos
-  build-depends: base >=4.9 && <4.10,capricon >=0.9 && <0.10,definitive-base >=2.6 && <2.7,definitive-parser >=3.1 && <3.2,GLFW >=0.5 && <0.6,hreadline >=0.2 && <0.3,JuicyPixels >=3.2 && <3.3,logos >=0.1 && <0.2,OpenGL >=3.0 && <3.1,StateVar >=1.1 && <1.2,vector >=0.12 && <0.13
+  build-depends: base >=4.9 && <4.10,capricon >=0.10 && <0.11,definitive-base >=2.6 && <2.7,definitive-parser >=3.1 && <3.2,GLFW >=0.5 && <0.6,hreadline >=0.2 && <0.3,JuicyPixels >=3.2 && <3.3,logos >=0.1 && <0.2,OpenGL >=3.0 && <3.1,StateVar >=1.1 && <1.2,vector >=0.12 && <0.13
   default-extensions: TypeSynonymInstances, NoMonomorphismRestriction, StandaloneDeriving, GeneralizedNewtypeDeriving, TypeOperators, RebindableSyntax, FlexibleInstances, FlexibleContexts, FunctionalDependencies, TupleSections, MultiParamTypeClasses, Rank2Types, AllowAmbiguousTypes, RoleAnnotations, ViewPatterns, LambdaCase
   hs-source-dirs:      exe
   ghc-options: -threaded