mirror of
https://github.com/anoma/juvix.git
synced 2024-09-11 16:26:33 +03:00
parent
6d49c9c9f1
commit
d8ba7ca36f
8
Makefile
8
Makefile
@ -200,8 +200,8 @@ STACKFLAGS?=--jobs $(THREADS)
|
||||
STACKTESTFLAGS?=--ta --hide-successes --ta --ansi-tricks=false
|
||||
SMOKEFLAGS?=--color --diff=git
|
||||
|
||||
.PHONY: check
|
||||
check: clean
|
||||
.PHONY: check-only
|
||||
check-only:
|
||||
@${MAKE} build
|
||||
@${MAKE} install
|
||||
@${MAKE} test
|
||||
@ -210,6 +210,10 @@ check: clean
|
||||
@${MAKE} format
|
||||
@${MAKE} pre-commit
|
||||
|
||||
.PHONY: check
|
||||
check: clean
|
||||
@${MAKE} check-only
|
||||
|
||||
# -- Build requirements
|
||||
|
||||
.PHONY: submodules
|
||||
|
@ -5,11 +5,11 @@ module Logic.GameState;
|
||||
|
||||
type Error :=
|
||||
| --- no error occurred
|
||||
noError : Error
|
||||
noError : Error
|
||||
| --- a non-fatal error occurred
|
||||
continue : String → Error
|
||||
continue : String → Error
|
||||
| --- a fatal occurred
|
||||
terminate : String → Error;
|
||||
terminate : String → Error;
|
||||
|
||||
type GameState :=
|
||||
| state : Board → Symbol → Error → GameState;
|
||||
|
@ -7,10 +7,9 @@ module Logic.Square;
|
||||
--- A square is each of the holes in a board
|
||||
type Square :=
|
||||
| --- An empty square has a ;Nat; that uniquely identifies it
|
||||
empty : Nat → Square
|
||||
| -- TODO: Check the line below using Judoc
|
||||
-- - An occupied square has a ;Symbol; in it
|
||||
occupied : Symbol → Square;
|
||||
empty : Nat → Square
|
||||
| --- An occupied square has a ;Symbol; in it
|
||||
occupied : Symbol → Square;
|
||||
|
||||
--- Equality for ;Square;s
|
||||
==Square : Square → Square → Bool;
|
||||
|
@ -5,9 +5,9 @@ module Logic.Symbol;
|
||||
--- A symbol represents a token that can be placed in a square
|
||||
type Symbol :=
|
||||
| --- The circle token
|
||||
O : Symbol
|
||||
O : Symbol
|
||||
| --- The cross token
|
||||
X : Symbol;
|
||||
X : Symbol;
|
||||
|
||||
--- Equality for ;Symbol;s
|
||||
==Symbol : Symbol → Symbol → Bool;
|
||||
|
@ -150,7 +150,7 @@ instance HasAtomicity Lambda where
|
||||
atomicity = const Atom
|
||||
|
||||
newtype Lambda = Lambda
|
||||
{_lambdaClauses :: [LambdaClause]}
|
||||
{_lambdaClauses :: NonEmpty LambdaClause}
|
||||
deriving stock (Eq, Show)
|
||||
|
||||
data LambdaClause = LambdaClause
|
||||
|
@ -111,9 +111,12 @@ instance PrettyCode LambdaClause where
|
||||
|
||||
instance PrettyCode Lambda where
|
||||
ppCode Lambda {..} = do
|
||||
lambdaClauses' <- ppBlock _lambdaClauses
|
||||
lambdaClauses' <- ppPipeBlock _lambdaClauses
|
||||
return $ kwLambda <+> lambdaClauses'
|
||||
|
||||
ppPipeBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann)
|
||||
ppPipeBlock items = vsep <$> mapM (fmap (kwPipe <+>) . ppCode) items
|
||||
|
||||
ppBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann)
|
||||
ppBlock items = bracesIndent . vsep . toList <$> mapM (fmap endSemicolon . ppCode) items
|
||||
|
||||
|
@ -402,9 +402,9 @@ goLambda :: forall r. (Members '[Error ScoperError, InfoTableBuilder] r) => Lamb
|
||||
goLambda l = Abstract.Lambda <$> mapM goClause (l ^. lambdaClauses)
|
||||
where
|
||||
goClause :: LambdaClause 'Scoped -> Sem r Abstract.LambdaClause
|
||||
goClause (LambdaClause ps b) = do
|
||||
ps' <- mapM goPatternArg ps
|
||||
b' <- goExpression b
|
||||
goClause lc = do
|
||||
ps' <- mapM goPatternArg (lc ^. lambdaParameters)
|
||||
b' <- goExpression (lc ^. lambdaBody)
|
||||
return (Abstract.LambdaClause ps' b')
|
||||
|
||||
goUniverse :: Universe -> Universe
|
||||
|
@ -222,7 +222,8 @@ type InductiveConstructorName s = SymbolType s
|
||||
type InductiveName s = SymbolType s
|
||||
|
||||
data InductiveConstructorDef (s :: Stage) = InductiveConstructorDef
|
||||
{ _constructorName :: InductiveConstructorName s,
|
||||
{ _constructorPipe :: Irrelevant (Maybe KeywordRef),
|
||||
_constructorName :: InductiveConstructorName s,
|
||||
_constructorDoc :: Maybe (Judoc s),
|
||||
_constructorType :: ExpressionType s
|
||||
}
|
||||
@ -631,7 +632,7 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Fun
|
||||
|
||||
data Lambda (s :: Stage) = Lambda
|
||||
{ _lambdaKw :: KeywordRef,
|
||||
_lambdaClauses :: [LambdaClause s]
|
||||
_lambdaClauses :: NonEmpty (LambdaClause s)
|
||||
}
|
||||
|
||||
deriving stock instance
|
||||
@ -653,7 +654,8 @@ deriving stock instance
|
||||
Ord (Lambda s)
|
||||
|
||||
data LambdaClause (s :: Stage) = LambdaClause
|
||||
{ _lambdaParameters :: NonEmpty (PatternType s),
|
||||
{ _lambdaPipe :: Irrelevant (Maybe KeywordRef),
|
||||
_lambdaParameters :: NonEmpty (PatternType s),
|
||||
_lambdaBody :: ExpressionType s
|
||||
}
|
||||
|
||||
@ -1020,7 +1022,7 @@ instance HasLoc (LambdaClause 'Scoped) where
|
||||
getLoc c = getLocSpan (c ^. lambdaParameters) <> getLoc (c ^. lambdaBody)
|
||||
|
||||
instance HasLoc (Lambda 'Scoped) where
|
||||
getLoc l = getLoc (l ^. lambdaKw) <>? (getLocSpan <$> nonEmpty (l ^. lambdaClauses))
|
||||
getLoc l = getLoc (l ^. lambdaKw) <> getLocSpan (l ^. lambdaClauses)
|
||||
|
||||
instance HasLoc (FunctionParameter 'Scoped) where
|
||||
getLoc p = (getLoc <$> p ^. paramName) ?<> getLoc (p ^. paramType)
|
||||
|
@ -292,17 +292,12 @@ instance (SingI s) => PrettyCode (InductiveDef s) where
|
||||
ppCode d@InductiveDef {..} = do
|
||||
doc' <- mapM ppCode _inductiveDoc
|
||||
sig' <- ppInductiveSignature d
|
||||
inductiveConstructors' <- ppConstructorBlock _inductiveConstructors
|
||||
inductiveConstructors' <- ppPipeBlock _inductiveConstructors
|
||||
return $
|
||||
doc' ?<> sig'
|
||||
<+> kwAssign
|
||||
<> line
|
||||
<> (indent' . align) inductiveConstructors'
|
||||
where
|
||||
ppConstructorBlock ::
|
||||
NonEmpty (InductiveConstructorDef s) -> Sem r (Doc Ann)
|
||||
ppConstructorBlock cs =
|
||||
vsep <$> mapM (fmap (kwPipe <+>) . ppCode) (toList cs)
|
||||
|
||||
dotted :: (Foldable f) => f (Doc Ann) -> Doc Ann
|
||||
dotted = concatWith (surround kwDot)
|
||||
@ -494,6 +489,9 @@ instance (SingI s) => PrettyCode (LetClause s) where
|
||||
ppBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann)
|
||||
ppBlock items = bracesIndent . vsep <$> mapM (fmap endSemicolon . ppCode) items
|
||||
|
||||
ppPipeBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann)
|
||||
ppPipeBlock items = vsep <$> mapM (fmap (kwPipe <+>) . ppCode) items
|
||||
|
||||
instance (SingI s) => PrettyCode (LambdaClause s) where
|
||||
ppCode LambdaClause {..} = do
|
||||
lambdaParameters' <- hsep <$> mapM ppPatternAtom _lambdaParameters
|
||||
@ -502,7 +500,7 @@ instance (SingI s) => PrettyCode (LambdaClause s) where
|
||||
|
||||
instance (SingI s) => PrettyCode (Lambda s) where
|
||||
ppCode Lambda {..} = do
|
||||
lambdaClauses' <- ppBlock _lambdaClauses
|
||||
lambdaClauses' <- bracesIndent <$> ppPipeBlock _lambdaClauses
|
||||
return $ kwLambda <+> lambdaClauses'
|
||||
|
||||
instance (SingI s) => PrettyCode (FunctionClause s) where
|
||||
|
@ -76,7 +76,7 @@ instance SingI t => PrettyPrint (Module 'Scoped t) where
|
||||
lastSemicolon :: Sem r ()
|
||||
lastSemicolon = case sing :: SModuleIsTop t of
|
||||
SModuleLocal -> return ()
|
||||
SModuleTop -> semicolon >> end
|
||||
SModuleTop -> semicolon >> line <> end
|
||||
|
||||
instance PrettyPrint [Statement 'Scoped] where
|
||||
ppCode :: forall r. Members '[ExactPrint, Reader Options] r => [Statement 'Scoped] -> Sem r ()
|
||||
@ -287,12 +287,22 @@ instance PrettyPrint (InductiveParameter 'Scoped) where
|
||||
instance PrettyPrint (NonEmpty (InductiveParameter 'Scoped)) where
|
||||
ppCode = hsep . fmap ppCode
|
||||
|
||||
instance (PrettyPrint a) => PrettyPrint (Irrelevant a) where
|
||||
ppCode (Irrelevant a) = ppCode a
|
||||
|
||||
instance PrettyPrint (InductiveConstructorDef 'Scoped) where
|
||||
ppCode :: forall r. Members '[ExactPrint, Reader Options] r => InductiveConstructorDef 'Scoped -> Sem r ()
|
||||
ppCode InductiveConstructorDef {..} = do
|
||||
let constructorName' = region (P.annDef _constructorName) (ppCode _constructorName)
|
||||
constructorType' = ppCode _constructorType
|
||||
doc' = ppCode <$> _constructorDoc
|
||||
doc' ?<> hang (constructorName' <+> noLoc P.kwColon <+> constructorType')
|
||||
hang (pipeHelper <+> doc' ?<> constructorName' <+> noLoc P.kwColon <+> constructorType')
|
||||
where
|
||||
-- we use this helper so that comments appear before the first optional pipe if the pipe was omitted
|
||||
pipeHelper :: Sem r ()
|
||||
pipeHelper = case _constructorPipe ^. unIrrelevant of
|
||||
Just p -> ppCode p
|
||||
Nothing -> P.ppCode kwPipe >>= morpheme (getLoc _constructorName)
|
||||
|
||||
ppInductiveSignature :: forall r. Members '[ExactPrint, Reader Options] r => InductiveDef 'Scoped -> Sem r ()
|
||||
ppInductiveSignature InductiveDef {..} = do
|
||||
@ -321,8 +331,7 @@ instance PrettyPrint (InductiveDef 'Scoped) where
|
||||
<> (indent . align) constrs'
|
||||
where
|
||||
ppConstructorBlock :: NonEmpty (InductiveConstructorDef 'Scoped) -> Sem r ()
|
||||
ppConstructorBlock cs =
|
||||
vsep (map ((noLoc P.kwPipe <+>) . ppCode) (toList cs))
|
||||
ppConstructorBlock cs = vsep (ppCode <$> cs)
|
||||
|
||||
instance PrettyPrint (WithLoc Backend) where
|
||||
ppCode = ppMorpheme
|
||||
|
@ -435,7 +435,8 @@ checkConstructorDef InductiveConstructorDef {..} = do
|
||||
InductiveConstructorDef
|
||||
{ _constructorName = constructorName',
|
||||
_constructorType = constructorType',
|
||||
_constructorDoc = doc'
|
||||
_constructorDoc = doc',
|
||||
_constructorPipe
|
||||
}
|
||||
|
||||
withParams ::
|
||||
@ -1005,7 +1006,8 @@ checkLambdaClause LambdaClause {..} = do
|
||||
return
|
||||
LambdaClause
|
||||
{ _lambdaParameters = lambdaParameters',
|
||||
_lambdaBody = lambdaBody'
|
||||
_lambdaBody = lambdaBody',
|
||||
_lambdaPipe
|
||||
}
|
||||
|
||||
scopedVar ::
|
||||
|
@ -85,6 +85,13 @@ runExpressionParser fileName input = do
|
||||
(_, Left err) -> return (Left (ErrMegaparsec (MegaparsecError err)))
|
||||
(_, Right r) -> return (Right r)
|
||||
|
||||
-- | The first pipe is optional, and thus we need a `Maybe`. The rest of the elements are guaranted to be given a `Just`.
|
||||
pipeSep1 :: Member InfoTableBuilder r => (Irrelevant (Maybe KeywordRef) -> ParsecS r a) -> ParsecS r (NonEmpty a)
|
||||
pipeSep1 e = do
|
||||
p <- Irrelevant <$> optional (kw kwPipe)
|
||||
h <- e p
|
||||
(h :|) <$> many (kw kwPipe >>= e . Irrelevant . Just)
|
||||
|
||||
top ::
|
||||
(Member InfoTableBuilder r) =>
|
||||
ParsecS r a ->
|
||||
@ -511,8 +518,8 @@ function = do
|
||||
-- Lambda expression
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
lambdaClause :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (LambdaClause 'Parsed)
|
||||
lambdaClause = do
|
||||
lambdaClause :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (LambdaClause 'Parsed)
|
||||
lambdaClause _lambdaPipe = do
|
||||
_lambdaParameters <- P.some patternAtom
|
||||
kw kwAssign
|
||||
_lambdaBody <- parseExpressionAtoms
|
||||
@ -521,7 +528,7 @@ lambdaClause = do
|
||||
lambda :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (Lambda 'Parsed)
|
||||
lambda = do
|
||||
_lambdaKw <- kw kwLambda
|
||||
_lambdaClauses <- braces (P.sepEndBy lambdaClause (kw kwSemicolon))
|
||||
_lambdaClauses <- braces (pipeSep1 lambdaClause)
|
||||
return Lambda {..}
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
@ -542,8 +549,7 @@ inductiveDef _inductiveBuiltin = do
|
||||
P.<?> "<type annotation e.g. ': Type'>"
|
||||
kw kwAssign P.<?> "<assignment symbol ':='>"
|
||||
_inductiveConstructors <-
|
||||
optional (kw kwPipe)
|
||||
>> P.sepBy1 constructorDef (kw kwPipe)
|
||||
pipeSep1 constructorDef
|
||||
P.<?> "<constructor definition>"
|
||||
return InductiveDef {..}
|
||||
|
||||
@ -554,8 +560,8 @@ inductiveParam = parens $ do
|
||||
_inductiveParameterType <- parseExpressionAtoms
|
||||
return InductiveParameter {..}
|
||||
|
||||
constructorDef :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (InductiveConstructorDef 'Parsed)
|
||||
constructorDef = do
|
||||
constructorDef :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (InductiveConstructorDef 'Parsed)
|
||||
constructorDef _constructorPipe = do
|
||||
_constructorDoc <- optional stashJudoc >> getJudoc
|
||||
_constructorName <- symbol P.<?> "<constructor name>"
|
||||
_constructorType <-
|
||||
|
@ -82,6 +82,9 @@ instance PrettyCode LetClause where
|
||||
ppCode = \case
|
||||
LetFunDef f -> ppCode f
|
||||
|
||||
ppPipeBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann)
|
||||
ppPipeBlock items = vsep <$> mapM (fmap (kwPipe <+>) . ppCode) items
|
||||
|
||||
instance PrettyCode LambdaClause where
|
||||
ppCode LambdaClause {..} = do
|
||||
lambdaParameters' <- hsep <$> mapM ppCodeAtom _lambdaPatterns
|
||||
@ -90,7 +93,7 @@ instance PrettyCode LambdaClause where
|
||||
|
||||
instance PrettyCode Lambda where
|
||||
ppCode Lambda {..} = do
|
||||
lambdaClauses' <- ppBlock _lambdaClauses
|
||||
lambdaClauses' <- ppPipeBlock _lambdaClauses
|
||||
return $ kwLambda <+> lambdaClauses'
|
||||
|
||||
instance PrettyCode a => PrettyCode (WithLoc a) where
|
||||
|
@ -281,9 +281,7 @@ goType e = case e of
|
||||
Abstract.ExpressionLet {} -> unsupported "let in types"
|
||||
|
||||
goLambda :: forall r. (Members '[NameIdGen] r) => Abstract.Lambda -> Sem r Lambda
|
||||
goLambda (Abstract.Lambda cl) = case nonEmpty cl of
|
||||
Nothing -> unsupported "empty lambda"
|
||||
Just cl' -> Lambda <$> mapM goClause cl'
|
||||
goLambda (Abstract.Lambda cl') = Lambda <$> mapM goClause cl'
|
||||
where
|
||||
goClause :: Abstract.LambdaClause -> Sem r LambdaClause
|
||||
goClause (Abstract.LambdaClause ps b) = do
|
||||
|
@ -9,6 +9,7 @@ module Juvix.Data
|
||||
module Juvix.Data.Loc,
|
||||
module Juvix.Data.NameId,
|
||||
module Juvix.Data.Comment,
|
||||
module Juvix.Data.Irrelevant,
|
||||
module Juvix.Data.Processed,
|
||||
module Juvix.Data.Uid,
|
||||
module Juvix.Data.Universe,
|
||||
@ -27,6 +28,7 @@ import Juvix.Data.Error
|
||||
import Juvix.Data.Fixity
|
||||
import Juvix.Data.ForeignBlock
|
||||
import Juvix.Data.Hole
|
||||
import Juvix.Data.Irrelevant
|
||||
import Juvix.Data.IsImplicit
|
||||
import Juvix.Data.Loc
|
||||
import Juvix.Data.NameId qualified
|
||||
|
@ -80,7 +80,6 @@ line' = append' P.line
|
||||
end' :: forall r. Members '[State Builder] r => Sem r ()
|
||||
end' = do
|
||||
cs <- gets (^. builderComments)
|
||||
unless (null cs) line'
|
||||
mapM_ printComment cs
|
||||
modify' (set builderComments [])
|
||||
|
||||
|
32
src/Juvix/Data/Irrelevant.hs
Normal file
32
src/Juvix/Data/Irrelevant.hs
Normal file
@ -0,0 +1,32 @@
|
||||
-- | Used when you annotate some AST with some information that you want to be
|
||||
-- ignored when checking for equality/ordering
|
||||
module Juvix.Data.Irrelevant where
|
||||
|
||||
import Juvix.Prelude.Base
|
||||
import Juvix.Prelude.Pretty
|
||||
|
||||
newtype Irrelevant a = Irrelevant
|
||||
{ _unIrrelevant :: a
|
||||
}
|
||||
deriving stock (Show)
|
||||
|
||||
instance Eq (Irrelevant a) where
|
||||
_ == _ = True
|
||||
|
||||
instance Ord (Irrelevant a) where
|
||||
compare _ _ = EQ
|
||||
|
||||
instance (Pretty a) => Pretty (Irrelevant a) where
|
||||
pretty (Irrelevant a) = pretty a
|
||||
|
||||
instance Functor Irrelevant where
|
||||
fmap f (Irrelevant a) = Irrelevant (f a)
|
||||
|
||||
instance Applicative Irrelevant where
|
||||
pure :: a -> Irrelevant a
|
||||
pure = Irrelevant
|
||||
|
||||
(<*>) :: Irrelevant (a -> b) -> Irrelevant a -> Irrelevant b
|
||||
Irrelevant f <*> Irrelevant a = Irrelevant (f a)
|
||||
|
||||
makeLenses ''Irrelevant
|
@ -4,7 +4,7 @@ module test007;
|
||||
open import Stdlib.Prelude;
|
||||
|
||||
map' : {A : Type} → {B : Type} → (A → B) → List A → List B;
|
||||
map' f := \{ nil := nil; (h :: t) := f h :: map' f t};
|
||||
map' f := \{ nil := nil | (h :: t) := f h :: map' f t};
|
||||
|
||||
terminating
|
||||
map'' : {A : Type} → {B : Type} → (A → B) → List A → List B;
|
||||
|
@ -18,10 +18,10 @@ f leaf := 1;
|
||||
f (node l r) :=
|
||||
let {l : Tree; l := g l} in
|
||||
let {r : Tree; r := g r} in
|
||||
let {terminating a : Nat; a := λ{leaf := 1; (node l r) := f l + f r} l} in
|
||||
let {terminating a : Nat; a := λ{leaf := 1 | (node l r) := f l + f r} l} in
|
||||
let {terminating b : Nat;
|
||||
b := λ {(node l r) := f l + f r;
|
||||
_ := 2} r} in
|
||||
b := λ {(node l r) := f l + f r
|
||||
| _ := 2} r} in
|
||||
a * b;
|
||||
|
||||
isNode : Tree → Bool;
|
||||
|
@ -18,20 +18,20 @@ pop_front : {A : Type} → Queue A → Queue A;
|
||||
pop_front {A} q :=
|
||||
let {q' : Queue A; q' := queue (tail (qfst q)) (qsnd q)} in
|
||||
case (qfst q') λ{
|
||||
nil := queue (reverse (qsnd q')) nil;
|
||||
_ := q'
|
||||
nil := queue (reverse (qsnd q')) nil
|
||||
| _ := q'
|
||||
};
|
||||
|
||||
push_back : {A : Type} → Queue A → A → Queue A;
|
||||
push_back q x := case (qfst q) λ{
|
||||
nil := queue (x :: nil) (qsnd q);
|
||||
q' := queue q' (x :: qsnd q)
|
||||
nil := queue (x :: nil) (qsnd q)
|
||||
| q' := queue q' (x :: qsnd q)
|
||||
};
|
||||
|
||||
is_empty : {A : Type} → Queue A → Bool;
|
||||
is_empty q := case (qfst q) λ{
|
||||
nil := case (qsnd q) λ{nil := true; _ := false};
|
||||
_ := false;
|
||||
nil := case (qsnd q) λ{nil := true | _ := false}
|
||||
| _ := false
|
||||
};
|
||||
|
||||
empty : {A : Type} → Queue A;
|
||||
|
@ -7,8 +7,8 @@ module test034;
|
||||
sum := let {
|
||||
sum' : Nat → Nat;
|
||||
sum' := λ {
|
||||
zero := zero;
|
||||
(suc n) := suc n + sum' n;
|
||||
zero := zero
|
||||
| (suc n) := suc n + sum' n
|
||||
};
|
||||
} in sum';
|
||||
|
||||
|
@ -27,10 +27,10 @@ f : Tree → Nat;
|
||||
f leaf := 1;
|
||||
f (node l r) :=
|
||||
case (g l, g r) λ{
|
||||
(leaf, leaf) := 3;
|
||||
(node l r, leaf) := (f l + f r) * 2;
|
||||
(node l1 r1, node l2 r2) := (f l1 + f r1) * (f l2 + f r2);
|
||||
(_, node l r) := f l + f r;
|
||||
(leaf, leaf) := 3
|
||||
| (node l r, leaf) := (f l + f r) * 2
|
||||
| (node l1 r1, node l2 r2) := (f l1 + f r1) * (f l2 + f r2)
|
||||
| (_, node l r) := f l + f r
|
||||
};
|
||||
|
||||
g leaf := leaf;
|
||||
|
@ -5,8 +5,8 @@ module test037;
|
||||
f l := case
|
||||
l
|
||||
λ {
|
||||
(x :: _) := x;
|
||||
nil := id;
|
||||
(x :: _) := x
|
||||
| nil := id
|
||||
}
|
||||
(let {
|
||||
y : Nat → Nat;
|
||||
@ -14,10 +14,10 @@ module test037;
|
||||
} in (let {
|
||||
z : (Nat → Nat) → Nat → Nat;
|
||||
z := id;
|
||||
} in case l λ { (_ :: _) := id; } z)
|
||||
} in case l λ { (_ :: _) := id } z)
|
||||
y)
|
||||
7;
|
||||
|
||||
main : IO;
|
||||
main := printNatLn (f (λ { x y := x y + 2; } :: nil));
|
||||
main := printNatLn (f (λ { x y := x y + 2 } :: nil));
|
||||
end;
|
||||
|
@ -3,7 +3,7 @@ module HigherOrderLambda;
|
||||
open import Stdlib.Prelude;
|
||||
|
||||
map' : {A : Type} → {B : Type} → (A → B) → List A → List B;
|
||||
map' f := \{ nil := nil; (h :: t) := f h :: map' f t};
|
||||
map' f := \{ nil := nil | (h :: t) := f h :: map' f t};
|
||||
|
||||
lst : List Nat;
|
||||
lst := zero :: suc zero :: nil;
|
||||
|
@ -1,28 +1,39 @@
|
||||
module Lambda;
|
||||
open import Stdlib.Prelude public;
|
||||
|
||||
open import Stdlib.Prelude public;
|
||||
id' : {A : Type} → A → A;
|
||||
id' := λ {
|
||||
| a := a
|
||||
};
|
||||
|
||||
id' : {A : Type} → A → A;
|
||||
id' := λ { a := a };
|
||||
uncurry' : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → A
|
||||
× B → C;
|
||||
uncurry' := λ {
|
||||
| f (a , b) := f a b
|
||||
};
|
||||
|
||||
uncurry' : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → A × B → C;
|
||||
uncurry' := λ {f (a, b) := f a b};
|
||||
fst' : {A : Type} → {B : Type} → A × B → A;
|
||||
fst' {_} := λ {
|
||||
| (a , _) := a
|
||||
};
|
||||
|
||||
fst' : {A : Type} → {B : Type} → A × B → A;
|
||||
fst' {_} := λ {(a, _) := a};
|
||||
first' : {A : Type} → {B : Type} → {A' : Type} → (A → A') → A
|
||||
× B → A' × B;
|
||||
first' := λ {
|
||||
| f (a , b) := f a , b
|
||||
};
|
||||
|
||||
first' : {A : Type} → {B : Type} → {A' : Type} → (A → A') → A × B → A' × B;
|
||||
first' := λ {f (a, b) := f a, b};
|
||||
|
||||
foldr' : {A : Type} → {B : Type} → (A → B → B) → B → List A → B;
|
||||
foldr' := λ {_ z nil := z;
|
||||
f z (h :: hs) := f h (foldr' f z hs)};
|
||||
|
||||
main : IO;
|
||||
main := printNatLn (id' zero)
|
||||
>> printNatLn (uncurry' (+) (1, 1))
|
||||
>> printNatLn (fst' (zero, 1))
|
||||
>> printNatLn (fst (first' ((+) 1) (1, zero)))
|
||||
>> printNatLn (foldr' (+) zero (1 :: 2 :: 3 :: nil));
|
||||
foldr' : {A : Type} → {B : Type} → (A → B → B) → B → List
|
||||
A → B;
|
||||
foldr' := λ {
|
||||
| _ z nil := z
|
||||
| f z (h :: hs) := f h (foldr' f z hs)
|
||||
};
|
||||
|
||||
main : IO;
|
||||
main := printNatLn (id' zero)
|
||||
>> printNatLn (uncurry' (+) (1 , 1))
|
||||
>> printNatLn (fst' (zero , 1))
|
||||
>> printNatLn (fst (first' ((+) 1) (1 , zero)))
|
||||
>> printNatLn (foldr' (+) zero (1 :: 2 :: 3 :: nil));
|
||||
end;
|
||||
|
@ -35,7 +35,7 @@ mapB : {A : Type} → (A → A) → A → A;
|
||||
mapB := λ { f a := f a};
|
||||
|
||||
add : Nat → Nat → Nat;
|
||||
add := λ {zero n := n; (suc n) := λ {m := suc (add n m) }};
|
||||
add := λ {zero n := n | (suc n) := λ {m := suc (add n m) }};
|
||||
|
||||
fst : {A : Type} → {B : Type} → A × B → A;
|
||||
fst {_} := λ {(a, _) := a};
|
||||
@ -58,42 +58,42 @@ type List (a : Type) :=
|
||||
| :: : a → List a → List a;
|
||||
|
||||
map : {A : Type} → {B : Type} → (A → B) → List A → List B;
|
||||
map {_} := λ {f nil := nil;
|
||||
f (x :: xs) := f x :: map f xs};
|
||||
map {_} := λ {f nil := nil
|
||||
| f (x :: xs) := f x :: map f xs};
|
||||
|
||||
pairEval : {A : Type} → {B : Type} → (A → B) × A → B;
|
||||
pairEval := λ {(f, x) := f x};
|
||||
|
||||
foldr : {A : Type} → {B : Type} → (A → B → B) → B → List A → B;
|
||||
foldr := λ {_ z nil := z;
|
||||
f z (h :: hs) := f h (foldr f z hs)};
|
||||
foldr := λ {_ z nil := z
|
||||
| f z (h :: hs) := f h (foldr f z hs)};
|
||||
|
||||
foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B;
|
||||
foldl := λ {f z nil := z;
|
||||
f z (h :: hs) := foldl f (f z h) hs};
|
||||
foldl := λ {f z nil := z
|
||||
| f z (h :: hs) := foldl f (f z h) hs};
|
||||
|
||||
type Bool :=
|
||||
true : Bool
|
||||
| false : Bool;
|
||||
|
||||
if : {A : Type} → Bool → A → A → A;
|
||||
if := λ {true a _ := a;
|
||||
false _ b := b};
|
||||
if := λ {true a _ := a
|
||||
| false _ b := b};
|
||||
|
||||
filter : {A : Type} → (A → Bool) → List A → List A;
|
||||
filter := λ {_ nil := nil;
|
||||
f (h :: hs) := if (f h)
|
||||
filter := λ {_ nil := nil
|
||||
| f (h :: hs) := if (f h)
|
||||
(h :: filter f hs)
|
||||
(filter f hs)};
|
||||
|
||||
partition : {A : Type} → (A → Bool) → List A → List A × List A;
|
||||
partition := λ {_ nil := nil, nil;
|
||||
f (x :: xs) := (if (f x) first second) ((::) x) (partition f xs)};
|
||||
partition := λ {_ nil := nil, nil
|
||||
| f (x :: xs) := (if (f x) first second) ((::) x) (partition f xs)};
|
||||
|
||||
zipWith : {A : Type} → {B : Type} → {C : Type} → (_ → _ → _) → List A → List B → List C;
|
||||
zipWith := λ {_ nil _ := nil;
|
||||
_ _ nil := nil;
|
||||
f (x :: xs) (y :: ys) := f x y :: zipWith f xs ys
|
||||
zipWith := λ {_ nil _ := nil
|
||||
| _ _ nil := nil
|
||||
| f (x :: xs) (y :: ys) := f x y :: zipWith f xs ys
|
||||
};
|
||||
|
||||
t : {A : Type} → {B : Type} → ({X : Type} → List X) → List A × List B;
|
||||
|
@ -25,9 +25,9 @@ map a b f (:: _ h hs) := :: a (f h) (map a b f hs);
|
||||
|
||||
filter : (a : Type) → (a → Bool) → List a → List a;
|
||||
filter a f (nil _) := nil a;
|
||||
filter a f (:: _ h hs) := match (f h) λ{
|
||||
true := :: a h (filter a f hs);
|
||||
false := filter a f hs;
|
||||
filter a f (:: _ h hs) := match (f h) λ {
|
||||
| true := :: a h (filter a f hs)
|
||||
| false := filter a f hs
|
||||
};
|
||||
|
||||
import Data.Nat;
|
||||
@ -64,13 +64,13 @@ splitAt a _ (nil _) := nil a, nil a;
|
||||
splitAt a zero xs := , (List a) (List a) (nil a) xs;
|
||||
splitAt a (suc zero) (:: _ x xs) := , (List a) (List a) (:: a x (nil a)) xs;
|
||||
splitAt a (suc (suc m)) (:: _ x xs) := match (splitAt a m xs) λ {
|
||||
(, la _ xs' xs'') := , la la (:: a x xs') xs'';
|
||||
(, la _ xs' xs'') := , la la (:: a x xs') xs''
|
||||
};
|
||||
|
||||
merge : (a : Type) → (a → a → Ordering) → List a → List a → List a;
|
||||
merge a cmp (:: _ x xs) (:: _ y ys) := match (cmp x y) λ{
|
||||
LT := :: a x (merge a cmp xs (:: a y ys));
|
||||
_ := :: a y (merge a cmp (:: a x xs) ys);
|
||||
merge a cmp (:: _ x xs) (:: _ y ys) := match (cmp x y) λ {
|
||||
| LT := :: a x (merge a cmp xs (:: a y ys))
|
||||
| _ := :: a y (merge a cmp (:: a x xs) ys)
|
||||
};
|
||||
merge _ _ (nil _) ys := ys;
|
||||
merge _ _ xs (nil _) := xs;
|
||||
@ -87,8 +87,8 @@ quickSort a cmp (:: _ x ys) :=
|
||||
let {
|
||||
ltx : a → Bool;
|
||||
ltx y := match (cmp y x) λ{
|
||||
LT := true;
|
||||
_ := false;
|
||||
| LT := true
|
||||
| _ := false
|
||||
};
|
||||
gex : a → Bool;
|
||||
gex y := not (ltx y)
|
||||
|
Loading…
Reference in New Issue
Block a user