Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Marc Coiffier
BHR
Commits
92042b21
Commit
92042b21
authored
Apr 18, 2019
by
Marc Coiffier
Browse files
Start updating the CaPriCon interpreter to enable "automatic universes"
parent
6b457fd3
Changes
4
Hide whitespace changes
Inline
Side-by-side
capricon/exe/CaPriCon_Engine.hs
View file @
92042b21
...
...
@@ -177,7 +177,13 @@ main = do
1
->
do
(
_
,
out
)
<-
runWordsState
(
map
toString
$
stringWords
(
code
::
JS
.
JSString
))
st
postMessage
(
reqID
::
Int
,
fromString
out
::
JS
.
JSString
)
-- run a block of code, and return both its output, and the new state
2
->
do
(
st'
,
out
)
<-
runWordsState
(
map
toString
$
stringWords
(
code
::
JS
.
JSString
))
st
id
<-
appendState
capriconObject
st'
postMessage
(
reqID
::
Int
,
fromString
out
::
JS
.
JSString
,
id
)
_
->
error
"Unhandled request type"
appendState
::
MonadIO
m
=>
JS
.
JSAny
->
a
->
m
Int
...
...
@@ -188,71 +194,3 @@ postMessage msg = liftIO $ JS.ffi "(function (m) { postMessage(m); })" (JS.toAny
capriconObject
::
JS
.
JSAny
capriconObject
=
JS
.
constant
"CaPriCon"
-- maybe unit JS.focus =<< JS.elemById "content-scroll"
-- JS.wait 200
-- let withSubElem root cl = JS.withElemsQS root ('.':cl) . traverse_
-- withSubElems _ [] k = k []
-- withSubElems root (h:t) k = withSubElem root h $ \h' -> withSubElems root t $ \t' -> k (h':t')
-- prelude <- JS.withElem "capricon-prelude" (\e -> JS.getProp e "textContent")
-- (initState,_) <- runWordsState (map fromString $ stringWords prelude) (defaultState hasteDict (COCState False [] zero id))
-- roots <- JS.elemsByQS JS.documentBody ".capricon-steps, code.capricon"
-- Just console <- JS.elemById "capricon-console"
-- (\k -> foldr k (\_ _ -> unit) roots initState "") $ \root next state pref -> do
-- isCode <- JS.hasClass root "capricon"
-- if isCode
-- then do
-- p <- JS.getProp root "textContent"
-- next state (pref+p+" pop ")
-- 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"] $ \[inpCons] -> void $ do
-- let toggleActive = do
-- JS.toggleClass root' "active"
-- JS.focus inpCons
-- JS.onEvent closeBtn JS.Click (const toggleActive)
-- JS.onEvent trig JS.Click $ \_ -> toggleActive
-- withSubElems root ["capricon-input"] $ \[inpMain] -> do
-- 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
-- -- JS.alert ("Running "+fromString text)
-- (state',_) <- runWordsState (stringWords text) state
-- let onEnter x = \case
-- JS.KeyData 13 False False False False -> x
-- _ -> return ()
-- runCode inp = do
-- Just v <- JS.getValue inp
-- (_,x) <- runWordsState (stringWords v) state'
-- JS.setProp out "textContent" (toString x)
-- return v
-- JS.onEvent inp JS.KeyPress $ onEnter $ void $ runCode inp
-- JS.onEvent inpMain JS.KeyPress $ onEnter $ do
-- v <- runCode inpMain
-- JS.setClass root' "active" True
-- JS.focus inp
-- JS.setProp inp "value" v
-- JS.setClass inpMain "ready" True
-- next state' ""
-- cloneNode :: MonadIO m => JS.Elem -> m JS.Elem
-- cloneNode x = liftIO $ JS.ffi "(function (n) { return n.cloneNode(true); })" x
capricon/src/CaPriCon/Run.hs
View file @
92042b21
...
...
@@ -5,7 +5,7 @@ import Definitive
import
Language.Format
import
Algebra.Monad.Concatenative
import
Data.CaPriCon
import
Data.CaPriCon.Extraction
(
Algebraic
(
..
),
from
Node
)
import
Data.CaPriCon.Extraction
(
Algebraic
(
..
),
from
Term
)
import
GHC.Generics
(
Generic
)
class
Monad
m
=>
MonadSubIO
io
m
where
...
...
@@ -21,7 +21,7 @@ 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
))
data
COCValue
io
str
=
COCExpr
(
Context
Node
str
(
COCAxiom
str
))
data
COCValue
io
str
=
COCExpr
(
Context
Term
str
(
COCAxiom
str
))
|
COCNull
|
COCError
str
|
COCConvertible
(
Maybe
(
Int
,
Int
))
|
COCAlgebraic
(
Algebraic
str
)
...
...
@@ -49,10 +49,10 @@ pattern StackCOC v = StackExtra (Opaque v)
takeLast
n
l
=
drop
(
length
l
-
n
)
l
showStackVal
::
IsCapriconString
str
=>
(
NodeDoc
str
->
str
)
->
NodeDir
str
(
COCAxiom
str
)
([
str
],
StringPattern
str
)
->
[(
str
,
Node
str
(
COCAxiom
str
))]
->
StackVal
str
(
COCBuiltin
io
str
)
(
COCValue
io
str
)
->
str
showStackVal
::
IsCapriconString
str
=>
(
NodeDoc
str
->
str
)
->
NodeDir
str
(
COCAxiom
str
)
([
str
],
StringPattern
str
)
->
[(
str
,
Term
str
(
COCAxiom
str
))]
->
StackVal
str
(
COCBuiltin
io
str
)
(
COCValue
io
str
)
->
str
showStackVal
toRaw
dir
ctx
=
fix
$
\
go
_x
->
case
_x
of
StackCOC
_x
->
case
_x
of
COCExpr
(
Context
Node
d
e
)
->
-- "<"+show d+">:"+
COCExpr
(
Context
Term
d
e
)
->
-- "<"+show d+">:"+
toRaw
$
showNode'
dir
(
map
(
second
snd
)
$
takeLast
d
(
freshContext
ctx
))
e
COCNull
->
"(null)"
COCError
e
->
"<!"
+
e
+
"!>"
...
...
@@ -172,13 +172,13 @@ literate = liftA2 (\pref r -> pref + [Left (TextComment $ fromString r)])
data
COCState
str
=
COCState
{
_endState
::
Bool
,
_context
::
[(
str
,
Node
str
(
COCAxiom
str
))
]
,
_context
::
Env
str
(
ContextTerm
str
(
COCAxiom
str
)),
_showDir
::
NodeDir
str
(
COCAxiom
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
(
COCAxiom
str
))
]
context
::
Lens'
(
COCState
str
)
(
Env
str
(
ContextTerm
str
(
COCAxiom
str
))
)
context
=
lens
_context
(
\
x
y
->
x
{
_context
=
y
})
showDir
::
Lens'
(
COCState
str
)
(
NodeDir
str
(
COCAxiom
str
)
([
str
],
StringPattern
str
))
showDir
=
lens
_showDir
(
\
x
y
->
x
{
_showDir
=
y
})
...
...
@@ -188,11 +188,11 @@ outputText = lens _outputText (\x y -> x { _outputText = y })
pushError
::
MonadStack
(
COCState
str
)
str
(
COCBuiltin
io
str
)
(
COCValue
io
str
)
m
=>
str
->
m
()
pushError
s
=
runStackState
$
modify
$
(
StackCOC
(
COCError
s
)
:
)
runInContext
::
Env
str
ax
->
MaybeT
((
->
)
(
Env
str
ax
)
)
a
->
Maybe
a
runInContext
::
ax
->
MaybeT
((
->
)
ax
)
a
->
Maybe
a
runInContext
c
v
=
(
v
^..
maybeT
)
c
modifyAllExprs
::
MonadStack
(
COCState
str
)
str
(
COCBuiltin
io
str
)
(
COCValue
io
str
)
m
=>
(
Context
Node
str
(
COCAxiom
str
)
->
Context
Node
str
(
COCAxiom
str
))
->
m
()
=>
(
Context
Term
str
(
COCAxiom
str
)
->
Context
Term
str
(
COCAxiom
str
))
->
m
()
modifyAllExprs
f
=
do
let
modStack
(
StackCOC
(
COCExpr
e
))
=
StackCOC
(
COCExpr
(
f
e
))
modStack
(
StackDict
d
)
=
StackDict
(
map
modStack
d
)
...
...
@@ -201,7 +201,7 @@ modifyAllExprs f = do
runStackState
$
modify
$
map
modStack
runDictState
$
modify
$
map
modStack
modifyCOCEnv
::
MonadStack
(
COCState
str
)
str
(
COCBuiltin
io
str
)
(
COCValue
io
str
)
m
=>
Maybe
(
Context
Node
str
(
COCAxiom
str
)
->
Context
Node
str
(
COCAxiom
str
),
Env
str
(
COCAxiom
str
))
->
m
()
=>
Maybe
(
Context
Term
str
(
COCAxiom
str
)
->
Context
Term
str
(
COCAxiom
str
),
Env
str
(
ContextTerm
str
(
COCAxiom
str
))
)
->
m
()
modifyCOCEnv
Nothing
=
unit
modifyCOCEnv
(
Just
(
modE
,
ctx
))
=
do
runExtraState
(
context
=-
ctx
)
...
...
@@ -227,7 +227,7 @@ runCOCBuiltin COCB_Print = do
_
->
return
()
runCOCBuiltin
COCB_Axiom
=
runStackState
$
modify
$
\
case
StackCOC
(
COCExpr
(
Context
Node
0
e
))
:
StackSymbol
s
:
st
->
StackCOC
(
COCExpr
(
Context
Node
0
(
Cons
(
Ap
(
Axiom
e
s
)
[]
))))
:
st
StackCOC
(
COCExpr
(
Context
Term
0
e
))
:
StackSymbol
s
:
st
->
StackCOC
(
COCExpr
(
Context
Term
0
(
Cons
(
Ap
(
Axiom
e
s
)
[]
))))
:
st
st
->
st
runCOCBuiltin
COCB_Format
=
do
...
...
@@ -279,7 +279,7 @@ runCOCBuiltin COCB_Ap = do
runCOCBuiltin
(
COCB_Bind
close
bt
)
=
do
ctx
<-
runExtraState
(
getl
context
)
let
dctx
=
length
ctx
setVal
(
StackCOC
(
COCExpr
e
@
(
Context
Node
d
_
)))
setVal
(
StackCOC
(
COCExpr
e
@
(
Context
Term
d
_
)))
|
d
==
dctx
||
not
close
,
Just
e'
<-
runInContext
ctx
(
mkBind
bt
e
)
=
StackCOC
(
COCExpr
e'
)
setVal
(
StackDict
dict
)
=
StackDict
(
map
setVal
dict
)
...
...
@@ -307,13 +307,13 @@ runCOCBuiltin COCB_MatchTerm = do
case
e
of
Bind
Lambda
x
tx
e'
->
tailCall
onLambda
$
do
runExtraState
$
context
=~
((
x
,
tx
)
:
)
runStackState
$
put
(
StackCOC
(
COCExpr
(
Context
Node
(
d
+
1
)
(
Cons
(
Ap
(
Sym
0
)
[]
))))
:
StackCOC
(
COCExpr
(
Context
Node
(
d
+
1
)
e'
))
runStackState
$
put
(
StackCOC
(
COCExpr
(
Context
Term
(
d
+
1
)
(
Cons
(
Ap
(
Sym
0
)
[]
))))
:
StackCOC
(
COCExpr
(
Context
Term
(
d
+
1
)
e'
))
:
st'
)
Bind
Prod
x
tx
e'
->
tailCall
onProduct
$
do
runExtraState
$
context
=~
((
x
,
tx
)
:
)
runStackState
$
put
(
StackCOC
(
COCExpr
(
Context
Node
(
d
+
1
)
(
Cons
(
Ap
(
Sym
0
)
[]
))))
:
StackCOC
(
COCExpr
(
Context
Node
(
d
+
1
)
e'
))
runStackState
$
put
(
StackCOC
(
COCExpr
(
Context
Term
(
d
+
1
)
(
Cons
(
Ap
(
Sym
0
)
[]
))))
:
StackCOC
(
COCExpr
(
Context
Term
(
d
+
1
)
e'
))
:
st'
)
Cons
(
Ap
h
[]
)
->
do
case
h
of
...
...
@@ -321,21 +321,21 @@ runCOCBuiltin COCB_MatchTerm = do
|
otherwise
->
tailCall
onVar
$
runStackState
$
put
(
StackSymbol
(
"#"
+
fromString
(
show
i
))
:
st'
)
Mu
ctx
_
a
->
do
let
a'
=
foldl'
(
\
e'
(
x
,
tx
,
_
)
->
Bind
Lambda
x
tx
e'
)
(
Cons
a
)
ctx
tailCall
onMu
$
runStackState
$
put
(
StackCOC
(
COCExpr
(
Context
Node
d
a'
))
tailCall
onMu
$
runStackState
$
put
(
StackCOC
(
COCExpr
(
Context
Term
d
a'
))
:
st'
)
Axiom
t
a
->
tailCall
onAxiom
$
do
runStackState
$
put
(
StackSymbol
a
:
StackCOC
(
COCExpr
(
Context
Node
0
t
))
:
StackCOC
(
COCExpr
(
Context
Term
0
t
))
:
st'
)
Cons
(
Ap
h
args
)
->
tailCall
onApply
$
do
runStackState
$
put
(
StackList
(
map
(
StackCOC
.
COCExpr
.
Context
Node
d
)
args
)
:
StackCOC
(
COCExpr
(
Context
Node
d
(
Cons
(
Ap
h
[]
))))
runStackState
$
put
(
StackList
(
map
(
StackCOC
.
COCExpr
.
Context
Term
d
)
args
)
:
StackCOC
(
COCExpr
(
Context
Term
d
(
Cons
(
Ap
h
[]
))))
:
st'
)
Universe
n
->
tailCall
onUniverse
$
runStackState
$
put
(
StackInt
n
:
st'
)
case
st
of
StackList
[
onUniverse
,
onLambda
,
onProduct
,
onApply
,
onMu
,
onVar
,
onAxiom
]
:
StackCOC
(
COCExpr
(
Context
Node
d
e
))
:
st'
->
runMatch
onUniverse
onLambda
onProduct
onApply
onMu
onVar
onAxiom
d
e
st'
onUniverse
:
onLambda
:
onProduct
:
onApply
:
onMu
:
onVar
:
onAxiom
:
StackCOC
(
COCExpr
(
Context
Node
d
e
))
:
st'
->
runMatch
onUniverse
onLambda
onProduct
onApply
onMu
onVar
onAxiom
d
e
st'
StackList
[
onUniverse
,
onLambda
,
onProduct
,
onApply
,
onMu
,
onVar
,
onAxiom
]
:
StackCOC
(
COCExpr
(
Context
Term
d
e
))
:
st'
->
runMatch
onUniverse
onLambda
onProduct
onApply
onMu
onVar
onAxiom
d
e
st'
onUniverse
:
onLambda
:
onProduct
:
onApply
:
onMu
:
onVar
:
onAxiom
:
StackCOC
(
COCExpr
(
Context
Term
d
e
))
:
st'
->
runMatch
onUniverse
onLambda
onProduct
onApply
onMu
onVar
onAxiom
d
e
st'
_
->
unit
runCOCBuiltin
COCB_TypeOf
=
do
...
...
@@ -418,7 +418,7 @@ runCOCBuiltin COCB_ContextVars = do
runCOCBuiltin
COCB_Extract
=
do
ctx
<-
runExtraState
(
getl
context
)
runStackState
$
modify
$
\
case
StackCOC
(
COCExpr
(
Context
Node
d
e
))
:
t
->
StackCOC
(
COCAlgebraic
(
from
Node
e
(
[]
,
takeLast
d
ctx
)))
:
t
StackCOC
(
COCExpr
(
Context
Term
d
e
))
:
t
->
StackCOC
(
COCAlgebraic
(
from
Term
e
(
[]
,
takeLast
d
ctx
)))
:
t
st
->
st
runCOCBuiltin
COCB_GetShowDir
=
do
...
...
@@ -435,7 +435,7 @@ runCOCBuiltin COCB_SetShowDir = do
runCOCBuiltin
COCB_InsertNodeDir
=
do
ctx
<-
runExtraState
(
getl
context
)
runStackState
$
modify
$
\
case
x
:
StackCOC
(
COCExpr
(
Context
Node
d
e
))
:
StackCOC
(
COCDir
dir
)
:
t
->
x
:
StackCOC
(
COCExpr
(
Context
Term
d
e
))
:
StackCOC
(
COCDir
dir
)
:
t
->
StackCOC
(
COCDir
(
insert
e
(
map
fst
(
takeLast
d
ctx
),
x
)
dir
))
:
t
st
->
st
...
...
capricon/src/Data/CaPriCon.hs
View file @
92042b21
{-# LANGUAGE UndecidableInstances, OverloadedStrings, NoMonomorphismRestriction, DeriveGeneric, ConstraintKinds #-}
module
Data.CaPriCon
(
-- * Expression nodes
IsCapriconString
(
..
),
BindType
(
..
),
Node
(
..
),
ApHead
(
..
),
Application
(
..
),
Context
Node
(
..
),
Env
,
COCExpression
(
..
),
IsCapriconString
(
..
),
BindType
(
..
),
Term
(
..
),
ApHead
(
..
),
Application
(
..
),
Context
Term
(
..
),
Env
,
DependentLogic
(
..
),
-- ** Managing De Bruijin indices
adjust_depth
,
adjust_telescope_depth
,
inc_depth
,
free_vars
,
is_free_in
,
-- ** Expression directories
...
...
@@ -51,30 +51,31 @@ type UniverseSize = Int
type
SymbolRef
=
Int
data
BindType
=
Lambda
|
Prod
deriving
(
Show
,
Eq
,
Ord
,
Generic
)
data
Node
str
a
=
Bind
BindType
str
(
Node
Type
str
a
)
(
Node
str
a
)
data
Term
str
a
=
Bind
BindType
str
(
Type
Term
str
a
)
(
Term
str
a
)
|
Cons
(
Application
str
a
)
|
Universe
UniverseSize
deriving
(
Show
,
Generic
)
type
Node
Type
str
a
=
Node
str
a
data
ApHead
str
a
=
Sym
SymbolRef
|
Mu
[(
str
,
Node
str
a
,
Node
str
a
)]
[
Node
str
a
]
(
Application
str
a
)
|
Axiom
(
Node
str
a
)
a
type
Type
Term
str
a
=
Term
str
a
data
ApHead
str
a
=
Sym
SymbolRef
|
Mu
[(
str
,
TypeTerm
str
a
,
TypeTerm
str
a
)]
[
Term
str
a
]
(
Application
str
a
)
|
Axiom
(
Term
str
a
)
a
deriving
(
Show
,
Generic
)
data
Application
str
a
=
Ap
(
ApHead
str
a
)
[
Node
str
a
]
data
Application
str
a
=
Ap
(
ApHead
str
a
)
[
Term
str
a
]
deriving
(
Show
,
Generic
)
type
Env
str
a
=
[(
str
,
NodeType
str
a
)]
type
ListSerializable
a
=
(
Serializable
ListStream
a
)
type
ListFormat
a
=
(
Format
ListStream
a
)
instance
ListSerializable
BindType
instance
ListFormat
BindType
instance
(
ListSerializable
a
,
ListSerializable
str
)
=>
ListSerializable
(
Node
str
a
)
instance
(
ListFormat
a
,
ListFormat
str
)
=>
ListFormat
(
Node
str
a
)
instance
(
ListSerializable
a
,
ListSerializable
str
)
=>
ListSerializable
(
Term
str
a
)
instance
(
ListFormat
a
,
ListFormat
str
)
=>
ListFormat
(
Term
str
a
)
instance
(
ListSerializable
a
,
ListSerializable
str
)
=>
ListSerializable
(
ApHead
str
a
)
instance
(
ListFormat
a
,
ListFormat
str
)
=>
ListFormat
(
ApHead
str
a
)
instance
(
ListSerializable
a
,
ListSerializable
str
)
=>
ListSerializable
(
Application
str
a
)
instance
(
ListFormat
a
,
ListFormat
str
)
=>
ListFormat
(
Application
str
a
)
class
Monad
m
=>
COCExpression
str
m
e
|
e
->
str
where
type
Env
str
e
=
[(
str
,
Binding
e
)]
class
Monad
m
=>
DependentLogic
str
m
e
|
e
->
str
where
type
Axiom
e
::
*
type
Binding
e
::
*
mkUniverse
::
UniverseSize
->
m
e
mkVariable
::
str
->
m
e
...
...
@@ -84,11 +85,18 @@ class Monad m => COCExpression str m e | e -> str where
checkType
::
e
->
m
e
conversionDelta
::
e
->
e
->
m
(
UniverseSize
,
UniverseSize
)
substHyp
::
str
->
e
->
m
(
e
->
e
,
Env
str
(
Axiom
e
)
)
substHyp
::
str
->
e
->
m
(
e
->
e
,
Env
str
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
insertHypBefore
::
Maybe
str
->
str
->
e
->
m
(
e
->
e
,
Env
str
e
)
hypIndex
::
(
IsCapriconString
str
,
MonadReader
[(
str
,
a
)]
m
)
=>
str
->
MaybeT
m
Int
hypIndex
h
=
ask
>>=
\
l
->
case
[
i
|
(
i
,
x
)
<-
zip
[
0
..
]
l
,
fst
x
==
h
]
of
i
:
_
->
return
i
_
->
zero
instance
(
Show
a
,
IsCapriconString
str
,
Monad
m
,
MonadReader
(
Env
str
(
Term
str
a
))
m
)
=>
DependentLogic
str
(
MaybeT
m
)
(
Term
str
a
)
where
type
Axiom
(
Term
str
a
)
=
a
type
Binding
(
Term
str
a
)
=
TypeTerm
str
a
mkUniverse
=
pure
.
Universe
mkVariable
v
=
hypIndex
v
<&>
\
i
->
Cons
(
Ap
(
Sym
i
)
[]
)
...
...
@@ -103,7 +111,7 @@ instance (Show a,IsCapriconString str,Monad m,MonadReader (Env str a) m) => COCE
args
_
=
[]
return
(
subst
e
(
Cons
(
Ap
(
Mu
[]
(
args
mte
)
(
Ap
(
Sym
0
)
[]
))
[]
)))
checkType
e
=
type_of
e
^.
maybeT
conversionDelta
a
b
=
return
(
convert
ible
a
b
)
^.
maybeT
conversionDelta
a
b
=
return
(
convert
Delta
a
b
)
^.
maybeT
substHyp
h
x
=
do
i
<-
hypIndex
h
...
...
@@ -127,54 +135,51 @@ instance (Show a,IsCapriconString str,Monad m,MonadReader (Env str a) m) => COCE
GT
->
second
(
adjust_depth
(
adj
i
))
x
:
k
(
i
+
1
))
(
\
_
->
[]
)
ctx
0
)
hypIndex
::
(
IsCapriconString
str
,
MonadReader
(
Env
str
a
)
m
)
=>
str
->
MaybeT
m
Int
hypIndex
h
=
ask
>>=
\
l
->
case
[
i
|
(
i
,
x
)
<-
zip
[
0
..
]
l
,
fst
x
==
h
]
of
i
:
_
->
return
i
_
->
zero
data
ContextNode
str
a
=
ContextNode
SymbolRef
(
Node
str
a
)
data
ContextTerm
str
a
=
ContextTerm
SymbolRef
(
Term
str
a
)
deriving
(
Show
,
Generic
)
instance
(
ListSerializable
a
,
ListSerializable
str
)
=>
ListSerializable
(
Context
Node
str
a
)
instance
(
ListFormat
a
,
ListFormat
str
)
=>
ListFormat
(
Context
Node
str
a
)
restrictEnv
::
SymbolRef
->
Env
str
a
->
Env
str
a
instance
(
ListSerializable
a
,
ListSerializable
str
)
=>
ListSerializable
(
Context
Term
str
a
)
instance
(
ListFormat
a
,
ListFormat
str
)
=>
ListFormat
(
Context
Term
str
a
)
restrictEnv
::
SymbolRef
->
[
a
]
->
[
a
]
restrictEnv
n
e
=
drop
(
length
e
-
n
)
e
instance
(
Show
a
,
IsCapriconString
str
,
MonadReader
(
Env
str
a
)
m
,
Monad
m
)
=>
COCExpression
str
(
MaybeT
m
)
(
ContextNode
str
a
)
where
type
Axiom
(
ContextNode
str
a
)
=
a
instance
(
Show
a
,
IsCapriconString
str
,
MonadReader
(
Env
str
(
Term
str
a
))
m
,
Monad
m
)
=>
DependentLogic
str
(
MaybeT
m
)
(
ContextTerm
str
a
)
where
type
Axiom
(
ContextTerm
str
a
)
=
a
type
Binding
(
ContextTerm
str
a
)
=
Term
str
a
mkUniverse
u
=
ask
>>=
\
ctx
->
Context
Node
(
length
ctx
)
<$>
mkUniverse
u
mkVariable
i
=
local
(
dropWhile
((
/=
i
)
.
fst
))
(
ask
>>=
\
ctx
->
Context
Node
(
length
ctx
)
<$>
mkVariable
i
)
mkBind
t
ce
@
(
Context
Node
de
e
)
|
de
>
0
=
Context
Node
(
de
-
1
)
<$>
local
(
restrictEnv
de
)
(
mkBind
t
e
)
mkUniverse
u
=
ask
>>=
\
ctx
->
Context
Term
(
length
ctx
)
<$>
mkUniverse
u
mkVariable
i
=
local
(
dropWhile
((
/=
i
)
.
fst
))
(
ask
>>=
\
ctx
->
Context
Term
(
length
ctx
)
<$>
mkVariable
i
)
mkBind
t
ce
@
(
Context
Term
de
e
)
|
de
>
0
=
Context
Term
(
de
-
1
)
<$>
local
(
restrictEnv
de
)
(
mkBind
t
e
)
|
otherwise
=
return
ce
mkApply
(
Context
Node
df
f
)
(
Context
Node
dx
x
)
=
do
mkApply
(
Context
Term
df
f
)
(
Context
Term
dx
x
)
=
do
let
dm
=
max
df
dx
Context
Node
dm
<$>
mkApply
(
inc_depth
(
dm
-
df
)
f
)
(
inc_depth
(
dm
-
dx
)
x
)
mkMu
(
Context
Node
d
e
)
=
Context
Node
d
<$>
local
(
restrictEnv
d
)
(
mkMu
e
)
checkType
(
Context
Node
d
e
)
=
Context
Node
d
<$>
local
(
restrictEnv
d
)
(
checkType
e
)
conversionDelta
(
Context
Node
da
a
)
(
Context
Node
db
b
)
=
Context
Term
dm
<$>
mkApply
(
inc_depth
(
dm
-
df
)
f
)
(
inc_depth
(
dm
-
dx
)
x
)
mkMu
(
Context
Term
d
e
)
=
Context
Term
d
<$>
local
(
restrictEnv
d
)
(
mkMu
e
)
checkType
(
Context
Term
d
e
)
=
Context
Term
d
<$>
local
(
restrictEnv
d
)
(
checkType
e
)
conversionDelta
(
Context
Term
da
a
)
(
Context
Term
db
b
)
=
let
dm
=
max
da
db
in
local
(
restrictEnv
dm
)
$
conversionDelta
(
inc_depth
(
dm
-
da
)
a
)
(
inc_depth
(
dm
-
db
)
b
)
pullTerm
Nothing
(
Context
Node
d
e
)
=
ask
<&>
\
l
->
Context
Node
(
length
l
)
(
inc_depth
(
length
l
-
d
)
e
)
pullTerm
(
Just
v
)
(
Context
Node
d
e
)
=
do
pullTerm
Nothing
(
Context
Term
d
e
)
=
ask
<&>
\
l
->
Context
Term
(
length
l
)
(
inc_depth
(
length
l
-
d
)
e
)
pullTerm
(
Just
v
)
(
Context
Term
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
(
Context
Node
d'
$
inc_depth
(
d'
-
d
)
e
)
return
(
Context
Term
d'
$
inc_depth
(
d'
-
d
)
e
)
substHyp
h
vh
=
do
Context
Node
dm
vh'
<-
pullTerm
(
Just
h
)
vh
first
(
\
f
cv
@
(
Context
Node
d
v
)
->
Context
Term
dm
vh'
<-
pullTerm
(
Just
h
)
vh
first
(
\
f
cv
@
(
Context
Term
d
v
)
->
if
d
<=
dm
then
cv
else
Context
Node
(
d
-
1
)
(
inc_depth
(
d
-
dm
)
$
f
$
inc_depth
(
dm
-
d
)
v
))
<$>
else
Context
Term
(
d
-
1
)
(
inc_depth
(
d
-
dm
)
$
f
$
inc_depth
(
dm
-
d
)
v
))
<$>
substHyp
h
vh'
insertHypBefore
h
h'
cth'
=
do
Context
Node
dh
th'
<-
pullTerm
h
cth'
first
(
\
f
cx
@
(
Context
Node
d
x
)
->
Context
Term
dh
th'
<-
pullTerm
h
cth'
first
(
\
f
cx
@
(
Context
Term
d
x
)
->
if
d
<=
dh
then
cx
else
Context
Node
(
d
+
1
)
(
inc_depth
(
d
-
dh
)
$
f
$
inc_depth
(
dh
-
d
)
x
))
else
Context
Term
(
d
+
1
)
(
inc_depth
(
d
-
dh
)
$
f
$
inc_depth
(
dh
-
d
)
x
))
<$>
insertHypBefore
h
h'
th'
data
NodeDir
str
ax
a
=
NodeDir
...
...
@@ -227,7 +232,7 @@ i'Cofree = iso (uncurry Step) (\(Step x y) -> (x,y))
instance
Ord
ax
=>
Semigroup
(
NodeDir
str
ax
a
)
where
NodeDir
a
b
c
+
NodeDir
a'
b'
c'
=
NodeDir
(
a
+
a'
)
(
b
+
b'
)
(
c
+
c'
)
instance
Ord
ax
=>
Monoid
(
NodeDir
str
ax
a
)
where
zero
=
NodeDir
zero
zero
zero
instance
Ord
ax
=>
DataMap
(
NodeDir
str
ax
a
)
(
Node
str
ax
)
a
where
instance
Ord
ax
=>
DataMap
(
NodeDir
str
ax
a
)
(
Term
str
ax
)
a
where
at
(
Bind
t
_
tx
e
)
=
from
i'NodeDir
.
l'1
.
at
t
.
l'Just
zero
.
at
tx
.
l'Just
zero
.
at
e
at
(
Cons
a
)
=
from
i'NodeDir
.
l'2
.
atAp
a
at
(
Universe
u
)
=
from
i'NodeDir
.
l'3
.
at
u
...
...
@@ -250,11 +255,11 @@ mayChoose Nothing = zero
(
<++>
)
::
WriterT
w
[]
a
->
WriterT
w
[]
a
->
WriterT
w
[]
a
a
<++>
b
=
a
&
from
writerT
%~
(
+
b
^..
writerT
)
findPattern
::
Ord
ax
=>
NodeDir
str
ax
a
->
Node
str
ax
->
[([([(
str
,
Node
str
ax
)],
Int
,
Node
str
ax
)],
a
)]
findPattern
::
Ord
ax
=>
NodeDir
str
ax
a
->
Term
str
ax
->
[([([(
str
,
Term
str
ax
)],
Int
,
Term
str
ax
)],
a
)]
findPattern
=
\
x
y
->
go
[]
x
y
^..
writerT
where
go
::
Ord
ax
=>
[(
str
,
Node
str
ax
)]
->
NodeDir
str
ax
a
->
Node
str
ax
->
WriterT
[([(
str
,
Node
str
ax
)],
Int
,
Node
str
ax
)]
[]
a
go_a
::
Ord
ax
=>
[(
str
,
Node
str
ax
)]
->
ApDir
str
ax
a
->
Application
str
ax
->
WriterT
[([(
str
,
Node
str
ax
)],
Int
,
Node
str
ax
)]
[]
a
go_ah
::
Ord
ax
=>
[(
str
,
Node
str
ax
)]
->
AHDir
str
ax
a
->
ApHead
str
ax
->
WriterT
[([(
str
,
Node
str
ax
)],
Int
,
Node
str
ax
)]
[]
a
where
go
::
Ord
ax
=>
[(
str
,
Term
str
ax
)]
->
NodeDir
str
ax
a
->
Term
str
ax
->
WriterT
[([(
str
,
Term
str
ax
)],
Int
,
Term
str
ax
)]
[]
a
go_a
::
Ord
ax
=>
[(
str
,
Term
str
ax
)]
->
ApDir
str
ax
a
->
Application
str
ax
->
WriterT
[([(
str
,
Term
str
ax
)],
Int
,
Term
str
ax
)]
[]
a
go_ah
::
Ord
ax
=>
[(
str
,
Term
str
ax
)]
->
AHDir
str
ax
a
->
ApHead
str
ax
->
WriterT
[([(
str
,
Term
str
ax
)],
Int
,
Term
str
ax
)]
[]
a
withEnv
env
d
x
m
=
foldr
(
\
(
i
,
as
)
ma
->
ma
<++>
(
foldl'
.
foldl'
)
(
\
l
a
->
(
tell
[(
env
,
i
-
length
env
,
x
)]
>>
return
a
)
<++>
l
)
zero
as
)
m
(
d
^??
from
i'NodeDir
.
l'2
.
from
i'AHDir
.
l'1
.
ascList
.
each
.
sat
((
>=
length
env
)
.
fst
))
go
env
d
wh
@
(
Bind
t
x
tx
e
)
=
withEnv
env
d
wh
$
do
...
...
@@ -304,7 +309,7 @@ adjust_depth f = go 0
inc_depth
0
=
\
x
->
x
inc_depth
dx
=
adjust_depth
(
+
dx
)
adjust_telescope_depth
field
f
=
zipWith
(
field
.
adjust_depth
.
\
i
j
->
if
j
<
i
then
j
else
i
+
f
(
j
-
i
))
[
0
..
]
free_vars
::
Node
str
a
->
Set
Int
free_vars
::
Term
str
a
->
Set
Int
free_vars
(
Bind
_
_
tx
e
)
=
free_vars
tx
+
delete
(
-
1
)
(
map
(
subtract
1
)
(
free_vars
e
))
free_vars
(
Cons
a
)
=
freeA
a
where
freeA
(
Ap
(
Sym
i
)
xs
)
=
singleton'
i
+
foldMap
free_vars
xs
...
...
@@ -314,7 +319,7 @@ free_vars (Cons a) = freeA a
freeA
(
Ap
(
Axiom
_
_
)
xs
)
=
foldMap
free_vars
xs
free_vars
_
=
zero
is_free_in
::
Int
->
Node
str
a
->
Bool
is_free_in
::
Int
->
Term
str
a
->
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
...
...
@@ -323,9 +328,9 @@ is_free_in = map2 not go
go_a
v
(
Ap
(
Mu
env
_
a
)
subs
)
=
go_a
(
v
+
length
env
)
a
&&
all
(
go
v
)
subs
go_a
v
(
Ap
(
Axiom
_
_
)
subs
)
=
all
(
go
v
)
subs
subst
::
(
Show
str
,
Show
a
)
=>
Node
str
a
->
Node
str
a
->
Node
str
a
subst
::
(
Show
str
,
Show
a
)
=>
Term
str
a
->
Term
str
a
->
Term
str
a
subst
=
flip
substn
0
substn
::
(
Show
str
,
Show
a
)
=>
Node
str
a
->
Int
->
Node
str
a
->
Node
str
a
substn
::
(
Show
str
,
Show
a
)
=>
Term
str
a
->
Int
->
Term
str
a
->
Term
str
a
substn
val
n
|
n
>=
0
=
getId
.
go
n
|
otherwise
=
error
"'subst' should not be called with a negative index"
where
go
d
(
Bind
t
x
tx
e
)
=
do
...
...
@@ -462,7 +467,7 @@ latexName s = fromString $ go $ toString s
_
->
"_{"
+
n
+
"}"
showNode
=
showNode'
zero
showNode'
::
(
IsCapriconString
str
,
Show
ax
,
Ord
ax
)
=>
NodeDir
str
ax
([
str
],
StringPattern
str
)
->
[(
str
,
Node
str
ax
)]
->
Node
str
ax
->
NodeDoc
str
showNode'
::
(
IsCapriconString
str
,
Show
ax
,
Ord
ax
)
=>
NodeDir
str
ax
([
str
],
StringPattern
str
)
->
[(
str
,
Term
str
ax
)]
->
Term
str
ax
->
NodeDoc
str
showNode'
dir
=
go
0
where
go
d
env
x
|
Just
ret
<-
toPat
d
env
x
=
ret
go
_
_
(
Universe
u
)
=
DocSubscript
"Set"
(
fromString
(
show
u
))
...
...
@@ -508,7 +513,7 @@ showNode' dir = go 0
|
word
<-
k
]
|
otherwise
=
Nothing
type_of
::
(
Show
a
,
IsCapriconString
str
,
MonadReader
(
Env
str
a
)
m
)
=>
Node
str
a
->
m
(
Maybe
(
Node
str
a
))
type_of
::
(
Show
a
,
IsCapriconString
str
,
MonadReader
(
Env
str
(
Term
str
a
)
)
m
)
=>
Term
str
a
->
m
(
Maybe
(
Term
str
a
))
type_of
=
yb
maybeT
.
go
where
go
(
Bind
Lambda
x
tx
e
)
=
Bind
Prod
x
tx
<$>
local
((
x
,
tx
)
:
)
(
go
e
)
go
(
Bind
Prod
x
tx
e
)
=
do
...
...
@@ -532,12 +537,12 @@ type_of = yb maybeT . go
rec_subst
(
y
:
t
)
(
Bind
Prod
_
tx
e
)
=
do
ty
<-
go
y
_
<-
return
(
convert
ible
tx
ty
)
^.
maybeT
_
<-
return
(
convert
Delta
tx
ty
)
^.
maybeT
rec_subst
t
(
subst
y
e
)
rec_subst
[]
x
=
return
x
rec_subst
_
_
=
zero
mu_type
::
MonadReader
(
Env
str
a
)
m
=>
Node
str
a
->
m
(
Maybe
(
Node
str
a
))
mu_type
::
MonadReader
(
Env
str
(
Term
str
a
)
)
m
=>
Term
str
a
->
m
(
Maybe
(
Term
str
a
))
mu_type
(
inc_depth
1
->
root_type
)
=
yb
maybeT
$
go
0
root_type
where
root_args
=
go'
root_type
...
...
@@ -586,8 +591,8 @@ mu_type (inc_depth 1 -> root_type) = yb maybeT $ go 0 root_type
return
$
Bind
Prod
xn
tIH
(
Universe
(
u
+
1
))
go_col'
_
_
_
=
zero
convert
ible
::
Node
str
a
->
Node
str
a
->
Maybe
(
Int
,
Int
)
convert
ible
=
\
x
y
->
map
((
getMax
<#>
getMax
)
.
fst
)
((
tell
(
Max
0
,
Max
0
)
>>
go
False
x
y
)
^..
writerT
)
convert
Delta
::
Term
str
a
->
Term
str
a
->
Maybe
(
Int
,
Int
)
convert
Delta
=
\
x
y
->
map
((
getMax
<#>
getMax
)
.
fst
)
((
tell
(
Max
0
,
Max
0
)
>>
go
False
x
y
)
^..
writerT
)
where
go
inv
(
Bind
b
_
tx
e
)
(
Bind
b'
_
tx'
e'
)
=
guard
(
b
==
b'
)
>>
go
(
not
inv
)
tx
tx'
>>
go
inv
e
e'
go
inv
(
Cons
ax
)
(
Cons
ay
)
=
go_a
inv
ax
ay
go
inv
(
Universe
u
)
(
Universe
v
)
|
u
>
v
=
tellInv
inv
(
Max
(
u
-
v
),
zero
)
...
...
capricon/src/Data/CaPriCon/Extraction.hs
View file @
92042b21
...
...
@@ -32,37 +32,37 @@ instance Serializable bytes str => Serializable bytes (AType str)
instance
Format
bytes
str
=>
Format
bytes
(
Algebraic
str
)
instance
Format
bytes
str
=>
Format
bytes
(
AType
str
)
from
Node
::
(
Show
ax
,
IsCapriconString
str
,
MonadReader
([
Bool
],
Env
str
ax
)
m
)
=>
Node
str
ax
->
m
(
Algebraic
str
)
from
Node
(
Bind
Lambda
x
tx
e
)
=
do
from
Term
::
(
Show
ax
,
IsCapriconString
str
,
MonadReader
([
Bool
],
Env
str
(
Term
str
ax
)
)
m
)
=>
Term
str
ax
->
m
(
Algebraic
str
)
from
Term
(
Bind
Lambda
x
tx
e
)
=
do
let
isT
=
isTypeType
tx
e'
<-
local
((
not
isT
:
)
<#>
((
x
,
tx
)
:
))
(
from
Node
e
)
e'
<-
local
((
not
isT
:
)
<#>
((
x
,
tx
)
:
))
(
from
Term
e
)
if
isT
then
return
e'
else
AFun
x
<$>
fromType
Node
tx
<*>
pure
e'
from
Node
(
Cons
a
)
=
fromApplication
a
from
Node
_
=
error
"Cannot produce a type-term in a language without first-class types"
else
AFun
x
<$>
fromType
Term
tx
<*>
pure
e'
from
Term
(
Cons
a
)
=
fromApplication
a
from
Term
_
=
error
"Cannot produce a type-term in a language without first-class types"
fromApplication
::
(
Show
ax
,
IsCapriconString
str
,
MonadReader
([
Bool
],
Env
str
ax
)
m
)
=>
Application
str
ax
->
m
(
Algebraic
str
)
fromApplication
::
(
Show
ax
,
IsCapriconString
str
,
MonadReader
([
Bool
],
Env
str
(
Term
str
ax
)
)
m
)
=>
Application
str
ax
->
m
(
Algebraic
str
)
fromApplication
(
Ap
ah
args
)
=
do
(
varKinds
,
env
)
<-
ask
let
concreteArgs
=
[
arg
|
(
arg
,
Just
t
)
<-
map
(
\
x
->
(
x
,(
checkType
x
^..
maybeT
)
env
))
args
,
not
(
isTypeType
t
)]
case
ah
of
Sym
s
->
foldl'
(
liftA2
AApply
)
(
pure
$
AVar
$
sum
[
if
isV
then
1
else
0
|
isV
<-
take
s
varKinds
])
(
map
from
Node
concreteArgs
)
Mu
_
_
a
->
foldl'
(
liftA2
AApply
)
(
fromApplication
a
)
(
map
from
Node
concreteArgs
)
Sym
s
->
foldl'
(
liftA2
AApply
)
(
pure
$
AVar
$
sum
[
if
isV
then
1
else
0
|
isV
<-
take
s
varKinds
])
(
map
from
Term
concreteArgs
)
Mu
_
_
a
->
foldl'
(
liftA2
AApply
)
(
fromApplication
a
)
(
map
from
Term
concreteArgs
)
Axiom
_
_
->
undefined
fromType
Node
::
MonadReader
([
Bool
],
Env
str
ax
)
m
=>
Node
str
ax
->
m
(
AType
str
)
fromType
Node
(
Bind
Prod
x
tx
e
)
=
do
fromType
Term
::
MonadReader
([
Bool
],
Env
str
(
Term
str
ax
)
)
m
=>
Term
str
ax
->
m
(
AType
str
)
fromType
Term
(
Bind
Prod
x
tx
e
)
=
do
let
isT
=
isTypeType
tx
e'
<-
local
((
not
isT
:
)
<#>
((
x
,
tx
)
:
))
(
fromType
Node
e
)
e'
<-
local
((
not
isT
:
)
<#>
((
x
,
tx
)
:
))
(
fromType
Term
e
)
if
isT
then
return
AAny
else
AArr
<$>
fromType
Node
tx
<*>
pure
e'
fromType
Node
(
Cons
(
Ap
(
Sym
s
)
[]
))
=
do
else
AArr
<$>
fromType
Term
tx
<*>
pure
e'
fromType
Term
(
Cons
(
Ap
(
Sym
s
)
[]
))
=
do
(
varKinds
,
_
)
<-
ask
pure
$
ATVar
$
sum
[
if
isV
then
0
else
1
|
isV
<-
take
s
varKinds
]
fromType
Node
_
=
pure
AAny
fromType
Term
_
=
pure
AAny
isTypeType
::
Node
str
ax
->
Bool
isTypeType
::
Term
str
ax
->
Bool
isTypeType
(
Universe
_
)
=
True
isTypeType
(
Bind
Prod
_
_
e
)
=
isTypeType
e
isTypeType
_
=
False
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment