mirror of
https://github.com/anoma/juvix.git
synced 2024-11-30 14:13:27 +03:00
Update Geb backend (#2436)
Changes in the printing of Lambda terms necessary for the use of the Juvix Geb backend, changing the names of binary operations, adding a constructor for natural numbers. Appropriately changes tests when necessary. --------- Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
This commit is contained in:
Artem Gureev
GitHub
parent
9bed4bbadb
commit
e7f5a83da3
@ -73,7 +73,7 @@ eval morph =
|
||||
MorphismBinop op -> evalBinop op
|
||||
MorphismCase c -> evalCase c
|
||||
MorphismFirst f -> evalFirst f
|
||||
MorphismInteger i -> return $ GebValueMorphismInteger i
|
||||
MorphismInteger i -> evalBitChoice i
|
||||
MorphismLambda l -> evalLambda l
|
||||
MorphismLeft m -> evalLeftInj m
|
||||
MorphismPair p -> evalPair p
|
||||
@ -83,6 +83,10 @@ eval morph =
|
||||
MorphismVar x -> evalVar x
|
||||
MorphismFail x -> evalFail x
|
||||
|
||||
evalBitChoice :: BitChoice -> Sem r GebValue
|
||||
evalBitChoice n = do
|
||||
return (GebValueMorphismInteger (n ^. bitChoice))
|
||||
|
||||
evalVar :: (EvalEffects r) => Var -> Sem r GebValue
|
||||
evalVar var = do
|
||||
ctx <- asks (^. envContext)
|
||||
@ -303,12 +307,15 @@ valueFalse =
|
||||
quote :: GebValue -> Morphism
|
||||
quote = \case
|
||||
GebValueClosure cls -> quoteClosure cls
|
||||
GebValueMorphismInteger i -> MorphismInteger i
|
||||
GebValueMorphismInteger i -> quoteBitChoice i
|
||||
GebValueMorphismLeft m -> quoteValueMorphismLeft m
|
||||
GebValueMorphismPair m -> quoteValueMorphismPair m
|
||||
GebValueMorphismRight m -> quoteValueMorphismRight m
|
||||
GebValueMorphismUnit -> MorphismUnit
|
||||
|
||||
quoteBitChoice :: Integer -> Morphism
|
||||
quoteBitChoice n = MorphismInteger (BitChoice {_bitChoice = n})
|
||||
|
||||
quoteClosure :: ValueClosure -> Morphism
|
||||
quoteClosure cls =
|
||||
let env = map quote (toList (cls ^. valueClosureEnv))
|
||||
|
||||
@ -33,6 +33,7 @@ allKeywords =
|
||||
kwGebBinopMod,
|
||||
kwGebBinopEq,
|
||||
kwGebBinopLt,
|
||||
kwGebBitChoice,
|
||||
kwGebObjectInitial,
|
||||
kwGebObjectTerminal,
|
||||
kwGebObjectProduct,
|
||||
@ -98,6 +99,9 @@ kwGebObjectInteger = asciiKw Str.gebInteger
|
||||
kwGebVar :: Keyword
|
||||
kwGebVar = asciiKw Str.gebVar
|
||||
|
||||
kwGebBitChoice :: Keyword
|
||||
kwGebBitChoice = asciiKw Str.gebBitChoice
|
||||
|
||||
kwGebObjectInitial :: Keyword
|
||||
kwGebObjectInitial = asciiKw Str.gebInitial
|
||||
|
||||
|
||||
@ -103,6 +103,11 @@ data Failure = Failure
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
newtype BitChoice = BitChoice
|
||||
{ _bitChoice :: Integer
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
-- | Corresponds to the GEB type for terms (morphisms of the category): `stlc`
|
||||
-- (https://github.com/anoma/geb/blob/main/src/specs/lambda.lisp).
|
||||
data Morphism
|
||||
@ -117,7 +122,7 @@ data Morphism
|
||||
| MorphismLambda Lambda
|
||||
| MorphismApplication Application
|
||||
| MorphismVar Var
|
||||
| MorphismInteger Integer
|
||||
| MorphismInteger BitChoice
|
||||
| MorphismBinop Binop
|
||||
| MorphismFail Failure
|
||||
deriving stock (Show, Eq, Generic)
|
||||
@ -189,7 +194,7 @@ instance HasAtomicity Morphism where
|
||||
MorphismLambda {} -> Aggregate appFixity
|
||||
MorphismApplication {} -> Aggregate appFixity
|
||||
MorphismVar {} -> Aggregate appFixity
|
||||
MorphismInteger {} -> Atom
|
||||
MorphismInteger {} -> Aggregate appFixity
|
||||
MorphismBinop {} -> Aggregate appFixity
|
||||
MorphismFail {} -> Aggregate appFixity
|
||||
|
||||
@ -231,3 +236,4 @@ makeLenses ''RightInj'
|
||||
makeLenses ''Second
|
||||
makeLenses ''TypedMorphism
|
||||
makeLenses ''Var
|
||||
makeLenses ''BitChoice
|
||||
|
||||
@ -146,10 +146,15 @@ instance PrettyCode Morphism where
|
||||
MorphismLambda x -> ppCode x
|
||||
MorphismApplication x -> ppCode x
|
||||
MorphismVar idx -> ppCode idx
|
||||
MorphismInteger n -> return $ annotate AnnLiteralInteger (pretty n)
|
||||
MorphismInteger n -> ppCode n
|
||||
MorphismBinop x -> ppCode x
|
||||
MorphismFail x -> ppCode x
|
||||
|
||||
instance PrettyCode BitChoice where
|
||||
ppCode BitChoice {..} = do
|
||||
let pnumb = (annotate AnnLiteralInteger (pretty _bitChoice))
|
||||
return $ kwBitChoice <+> pnumb
|
||||
|
||||
instance PrettyCode Product where
|
||||
ppCode Product {..} = do
|
||||
left <- ppArg _productLeft
|
||||
|
||||
@ -67,6 +67,9 @@ kwEq = keyword Str.gebEq
|
||||
kwLt :: Doc Ann
|
||||
kwLt = keyword Str.gebLt
|
||||
|
||||
kwBitChoice :: Doc Ann
|
||||
kwBitChoice = keyword Str.gebBitChoice
|
||||
|
||||
kwInitial :: Doc Ann
|
||||
kwInitial = keyword Str.gebInitial
|
||||
|
||||
|
||||
@ -157,7 +157,7 @@ fromCore tab = case tab ^. Core.infoMain of
|
||||
|
||||
convertConstant :: Core.Constant -> Trans Morphism
|
||||
convertConstant Core.Constant {..} = case _constantValue of
|
||||
Core.ConstInteger n -> return $ MorphismInteger n
|
||||
Core.ConstInteger n -> return $ MorphismInteger (BitChoice {_bitChoice = n})
|
||||
Core.ConstString {} -> unsupported
|
||||
|
||||
convertApp :: Core.App -> Trans Morphism
|
||||
|
||||
@ -115,7 +115,6 @@ morphism :: ParsecS r Geb.Morphism
|
||||
morphism =
|
||||
P.label "<geb morphism>" $ do
|
||||
morphismUnit
|
||||
<|> Geb.MorphismInteger <$> morphismInteger
|
||||
<|> parens
|
||||
( morphismUnit
|
||||
<|> Geb.MorphismAbsurd <$> morphismAbsurd
|
||||
@ -130,6 +129,7 @@ morphism =
|
||||
<|> Geb.MorphismVar <$> morphismVar
|
||||
<|> Geb.MorphismBinop <$> morphismBinop
|
||||
<|> Geb.MorphismFail <$> morphismFail
|
||||
<|> Geb.MorphismInteger <$> morphismBitChoice
|
||||
)
|
||||
|
||||
morphismList :: ParsecS r Geb.Morphism
|
||||
@ -140,8 +140,12 @@ morphismList = parens $ do
|
||||
parseNatural :: ParsecS r Integer
|
||||
parseNatural = lexeme P.decimal
|
||||
|
||||
morphismInteger :: ParsecS r Integer
|
||||
morphismInteger = parseNatural
|
||||
morphismBitChoice :: ParsecS r Geb.BitChoice
|
||||
morphismBitChoice = do
|
||||
P.label "<geb MorphismBitChoice>" $ do
|
||||
kw kwGebBitChoice <* space
|
||||
_bitChoice <- parseNatural
|
||||
return Geb.BitChoice {..}
|
||||
|
||||
opcode :: ParsecS r Geb.Opcode
|
||||
opcode =
|
||||
|
||||
@ -638,29 +638,32 @@ gebApp = "app"
|
||||
gebVar :: (IsString s) => s
|
||||
gebVar = "index"
|
||||
|
||||
gebBitChoice :: (IsString s) => s
|
||||
gebBitChoice = "bit-choice"
|
||||
|
||||
gebAdd :: (IsString s) => s
|
||||
gebAdd = "add"
|
||||
gebAdd = "plus"
|
||||
|
||||
gebSub :: (IsString s) => s
|
||||
gebSub = "sub"
|
||||
gebSub = "minus"
|
||||
|
||||
gebMul :: (IsString s) => s
|
||||
gebMul = "mul"
|
||||
gebMul = "times"
|
||||
|
||||
gebDiv :: (IsString s) => s
|
||||
gebDiv = "div"
|
||||
gebDiv = "divide"
|
||||
|
||||
gebMod :: (IsString s) => s
|
||||
gebMod = "mod"
|
||||
gebMod = "modulo"
|
||||
|
||||
gebFail :: (IsString s) => s
|
||||
gebFail = "err"
|
||||
|
||||
gebEq :: (IsString s) => s
|
||||
gebEq = "eq"
|
||||
gebEq = "lamb-eq"
|
||||
|
||||
gebLt :: (IsString s) => s
|
||||
gebLt = "lt"
|
||||
gebLt = "lamb-lt"
|
||||
|
||||
gebInitial :: (IsString s) => s
|
||||
gebInitial = "so0"
|
||||
@ -675,7 +678,7 @@ gebCoprod :: (IsString s) => s
|
||||
gebCoprod = "coprod"
|
||||
|
||||
gebHom :: (IsString s) => s
|
||||
gebHom = "so-hom-obj"
|
||||
gebHom = "fun-type"
|
||||
|
||||
gebInteger :: (IsString s) => s
|
||||
gebInteger = "int"
|
||||
|
||||
@ -1 +1 @@
|
||||
11
|
||||
(bit-choice 11)
|
||||
|
||||
@ -1 +1,2 @@
|
||||
32
|
||||
(bit-choice 32)
|
||||
|
||||
|
||||
@ -1 +1 @@
|
||||
8
|
||||
(bit-choice 8)
|
||||
|
||||
@ -1 +1 @@
|
||||
32
|
||||
(bit-choice 32)
|
||||
|
||||
@ -1 +1 @@
|
||||
8
|
||||
(bit-choice 8)
|
||||
|
||||
@ -1 +1 @@
|
||||
9
|
||||
(bit-choice 9)
|
||||
|
||||
@ -1 +1 @@
|
||||
3
|
||||
(bit-choice 3)
|
||||
|
||||
@ -1 +1 @@
|
||||
5050
|
||||
(bit-choice 5050)
|
||||
|
||||
@ -1 +1 @@
|
||||
5050
|
||||
(bit-choice 5050)
|
||||
|
||||
@ -1 +1 @@
|
||||
55
|
||||
(bit-choice 55)
|
||||
|
||||
@ -1 +1 @@
|
||||
771
|
||||
(bit-choice 771)
|
||||
|
||||
@ -1 +1 @@
|
||||
55
|
||||
(bit-choice 55)
|
||||
|
||||
@ -1 +1 @@
|
||||
5050
|
||||
(bit-choice 5050)
|
||||
|
||||
@ -1 +1 @@
|
||||
11
|
||||
(bit-choice 11)
|
||||
|
||||
@ -1 +1 @@
|
||||
364
|
||||
(bit-choice 364)
|
||||
|
||||
@ -1 +1 @@
|
||||
48830320
|
||||
(bit-choice 48830320)
|
||||
|
||||
@ -1 +1 @@
|
||||
6386010
|
||||
(bit-choice 6386010)
|
||||
|
||||
@ -1 +1 @@
|
||||
87
|
||||
(bit-choice 87)
|
||||
|
||||
@ -1 +1 @@
|
||||
203
|
||||
(bit-choice 203)
|
||||
|
||||
@ -1 +1 @@
|
||||
3
|
||||
(bit-choice 3)
|
||||
|
||||
@ -1 +1 @@
|
||||
6077
|
||||
(bit-choice 6077)
|
||||
|
||||
@ -1 +1 @@
|
||||
1
|
||||
(bit-choice 1)
|
||||
|
||||
@ -1 +1 @@
|
||||
1
|
||||
(bit-choice 1)
|
||||
|
||||
@ -1 +1 @@
|
||||
55
|
||||
(bit-choice 55)
|
||||
|
||||
@ -1 +1 @@
|
||||
11
|
||||
(bit-choice 11)
|
||||
|
||||
@ -1 +1 @@
|
||||
32
|
||||
(bit-choice 32)
|
||||
|
||||
@ -1 +1 @@
|
||||
8
|
||||
(bit-choice 8)
|
||||
|
||||
@ -1 +1 @@
|
||||
1
|
||||
(bit-choice 1)
|
||||
|
||||
@ -1 +1 @@
|
||||
40
|
||||
(bit-choice 40)
|
||||
|
||||
@ -1 +1 @@
|
||||
8
|
||||
(bit-choice 8)
|
||||
|
||||
@ -1 +1 @@
|
||||
5
|
||||
(bit-choice 5)
|
||||
|
||||
@ -1 +1 @@
|
||||
3
|
||||
(bit-choice 3)
|
||||
|
||||
@ -1 +1 @@
|
||||
5050
|
||||
(bit-choice 5050)
|
||||
|
||||
@ -1 +1 @@
|
||||
5050
|
||||
(bit-choice 5050)
|
||||
|
||||
@ -1 +1 @@
|
||||
55
|
||||
(bit-choice 55)
|
||||
|
||||
@ -1 +1 @@
|
||||
55
|
||||
(bit-choice 55)
|
||||
|
||||
@ -1 +1 @@
|
||||
5050
|
||||
(bit-choice 5050)
|
||||
|
||||
@ -1 +1 @@
|
||||
11
|
||||
(bit-choice 11)
|
||||
|
||||
@ -1 +1 @@
|
||||
364
|
||||
(bit-choice 364)
|
||||
|
||||
@ -1 +1 @@
|
||||
48830320
|
||||
(bit-choice 48830320)
|
||||
|
||||
@ -1 +1 @@
|
||||
901
|
||||
(bit-choice 901)
|
||||
|
||||
@ -1 +1 @@
|
||||
87
|
||||
(bit-choice 87)
|
||||
|
||||
@ -1 +1 @@
|
||||
203
|
||||
(bit-choice 203)
|
||||
|
||||
@ -1 +1 @@
|
||||
3
|
||||
(bit-choice 3)
|
||||
|
||||
@ -1 +1 @@
|
||||
6295
|
||||
(bit-choice 6295)
|
||||
|
||||
@ -1 +1 @@
|
||||
9
|
||||
(bit-choice 9)
|
||||
|
||||
@ -1,23 +1,21 @@
|
||||
(typed
|
||||
(app
|
||||
(app
|
||||
(app
|
||||
(app
|
||||
(lamb
|
||||
(list
|
||||
(fun-type
|
||||
so1
|
||||
so1))
|
||||
(lamb
|
||||
(list
|
||||
(so-hom-obj
|
||||
so1
|
||||
so1))
|
||||
(lamb
|
||||
(list
|
||||
int)
|
||||
(index 1)))
|
||||
(list
|
||||
(lamb
|
||||
(list
|
||||
so1)
|
||||
(index 0))))
|
||||
int)
|
||||
(index 1)))
|
||||
(list
|
||||
12345))
|
||||
(lamb
|
||||
(list
|
||||
so1)
|
||||
(index 0))))
|
||||
(list
|
||||
(unit)))
|
||||
so1)
|
||||
(bit-choice 12345)))
|
||||
(list
|
||||
(unit)))
|
||||
|
||||
@ -1,22 +1,18 @@
|
||||
(typed
|
||||
(app
|
||||
(lamb
|
||||
(list
|
||||
(coprod
|
||||
int
|
||||
int))
|
||||
(case-on
|
||||
(index 0)
|
||||
(right
|
||||
int
|
||||
1)
|
||||
(left
|
||||
int
|
||||
2)))
|
||||
(app
|
||||
(lamb
|
||||
(list
|
||||
(coprod
|
||||
int
|
||||
int))
|
||||
(case-on
|
||||
(index 0)
|
||||
(right
|
||||
int
|
||||
(bit-choice 1))
|
||||
(left
|
||||
int
|
||||
3)))
|
||||
(coprod
|
||||
int
|
||||
int))
|
||||
(bit-choice 2))))
|
||||
(list
|
||||
(left
|
||||
int
|
||||
(bit-choice 3))))
|
||||
|
||||
@ -1,14 +1,12 @@
|
||||
(typed
|
||||
(app
|
||||
(lamb
|
||||
(list
|
||||
(prod
|
||||
int
|
||||
int))
|
||||
(fst
|
||||
(index 0)))
|
||||
(app
|
||||
(lamb
|
||||
(list
|
||||
(pair
|
||||
10
|
||||
20)))
|
||||
int)
|
||||
(prod
|
||||
int
|
||||
int))
|
||||
(fst
|
||||
(index 0)))
|
||||
(list
|
||||
(pair
|
||||
(bit-choice 10)
|
||||
(bit-choice 20))))
|
||||
|
||||
@ -1,21 +1,15 @@
|
||||
(typed
|
||||
(app
|
||||
(app
|
||||
(lamb
|
||||
(list
|
||||
(fun-type
|
||||
so1
|
||||
so1))
|
||||
(lamb
|
||||
(list
|
||||
(so-hom-obj
|
||||
so1
|
||||
so1))
|
||||
(lamb
|
||||
(list
|
||||
int)
|
||||
(index 1)))
|
||||
(list
|
||||
(lamb
|
||||
(list
|
||||
so1)
|
||||
(index 0))))
|
||||
(so-hom-obj
|
||||
int
|
||||
(so-hom-obj
|
||||
so1
|
||||
so1)))
|
||||
int)
|
||||
(index 1)))
|
||||
(list
|
||||
(lamb
|
||||
(list
|
||||
so1)
|
||||
(index 0))))
|
||||
|
||||
@ -1,11 +1,9 @@
|
||||
(typed
|
||||
(app
|
||||
(lamb
|
||||
(list
|
||||
int)
|
||||
(index 0))
|
||||
(app
|
||||
(lamb
|
||||
(list
|
||||
(add
|
||||
1000
|
||||
2000)))
|
||||
int)
|
||||
int)
|
||||
(index 0))
|
||||
(list
|
||||
(plus
|
||||
(bit-choice 1000)
|
||||
(bit-choice 2000))))
|
||||
|
||||
@ -1,14 +1,10 @@
|
||||
(typed
|
||||
(case-on
|
||||
(right
|
||||
so1
|
||||
(unit))
|
||||
(right
|
||||
so1
|
||||
(unit))
|
||||
(left
|
||||
so1
|
||||
(unit)))
|
||||
(coprod
|
||||
(case-on
|
||||
(right
|
||||
so1
|
||||
so1))
|
||||
(unit))
|
||||
(right
|
||||
so1
|
||||
(unit))
|
||||
(left
|
||||
so1
|
||||
(unit)))
|
||||
|
||||
@ -1,13 +1,7 @@
|
||||
(typed
|
||||
(lamb
|
||||
(list
|
||||
so1)
|
||||
(lamb
|
||||
(list
|
||||
so1)
|
||||
(lamb
|
||||
(list
|
||||
so1)
|
||||
(index 1)))
|
||||
(so-hom-obj
|
||||
so1
|
||||
(so-hom-obj
|
||||
so1
|
||||
so1)))
|
||||
(index 1)))
|
||||
|
||||
@ -1,12 +1,6 @@
|
||||
(typed
|
||||
(lamb
|
||||
(list
|
||||
so1)
|
||||
(left
|
||||
so1
|
||||
(unit)))
|
||||
(so-hom-obj
|
||||
(lamb
|
||||
(list
|
||||
so1)
|
||||
(left
|
||||
so1
|
||||
(coprod
|
||||
so1
|
||||
so1)))
|
||||
(unit)))
|
||||
|
||||
@ -55,7 +55,7 @@ tests:
|
||||
- dev
|
||||
- geb
|
||||
- repl
|
||||
stdin: ':t (mul 2 3)'
|
||||
stdin: ':t (times (bit-choice 2) (bit-choice 3))'
|
||||
stdout:
|
||||
contains: 'int'
|
||||
exit-status: 0
|
||||
@ -78,7 +78,7 @@ tests:
|
||||
- dev
|
||||
- geb
|
||||
- repl
|
||||
stdin: '(add 2 (mul 3 4))'
|
||||
stdin: '(plus (bit-choice 2) (times (bit-choice 3) (bit-choice 4)))'
|
||||
stdout:
|
||||
contains: |
|
||||
14
|
||||
@ -133,25 +133,19 @@ tests:
|
||||
args:
|
||||
- Geb/positive/app-lambda.geb
|
||||
stdout: |
|
||||
(typed
|
||||
(app
|
||||
(app
|
||||
(lamb
|
||||
(list
|
||||
(fun-type
|
||||
so1
|
||||
so1))
|
||||
(lamb
|
||||
(list
|
||||
(so-hom-obj
|
||||
so1
|
||||
so1))
|
||||
(lamb
|
||||
(list
|
||||
int)
|
||||
(index 1)))
|
||||
(list
|
||||
(lamb
|
||||
(list
|
||||
so1)
|
||||
(index 0))))
|
||||
(so-hom-obj
|
||||
int
|
||||
(so-hom-obj
|
||||
so1
|
||||
so1)))
|
||||
int)
|
||||
(index 1)))
|
||||
(list
|
||||
(lamb
|
||||
(list
|
||||
so1)
|
||||
(index 0))))
|
||||
exit-status: 0
|
||||
|
||||
Loading…
Reference in New Issue
Block a user