From 08b29bb79ce23db1ddf70894d6d353769c9884b1 Mon Sep 17 00:00:00 2001 From: pingu Date: Mon, 17 Nov 2025 14:25:48 +0100 Subject: [PATCH] Initial --- .gitignore | 13 + 1.org | 60 ++++ 2.org | 59 ++++ 3/.envrc | 1 + 3/.gitignore | 20 ++ 3/Chi.cf | 27 ++ 3/Chi.hs | 787 ++++++++++++++++++++++++++++++++++++++++++++++++ 3/assig.org | 119 ++++++++ 3/cabal.project | 2 + 3/chi.cabal | 28 ++ 3/flake.lock | 61 ++++ 3/flake.nix | 89 ++++++ two.agda | 124 ++++++++ 13 files changed, 1390 insertions(+) create mode 100644 .gitignore create mode 100644 1.org create mode 100644 2.org create mode 100644 3/.envrc create mode 100644 3/.gitignore create mode 100644 3/Chi.cf create mode 100644 3/Chi.hs create mode 100644 3/assig.org create mode 100644 3/cabal.project create mode 100644 3/chi.cabal create mode 100644 3/flake.lock create mode 100644 3/flake.nix create mode 100644 two.agda diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..b1ced1a --- /dev/null +++ b/.gitignore @@ -0,0 +1,13 @@ +.DS_Store +.idea +*.log +tmp/ + +.direnv/ +dist-newstyle/ + +*.bbl +*.pdf +*.tex + +*.agdai diff --git a/1.org b/1.org new file mode 100644 index 0000000..e5b7b91 --- /dev/null +++ b/1.org @@ -0,0 +1,60 @@ +#+title: Assignment 1 +#+options: toc:nil +#+latex_header: \usepackage{parskip} + +In order to pass this assignment you have to get at least two points. + +(Exercises marked with [BN] are based on exercises from a previous version of this course, given by Bengt Nordström.) + +* (1 point) +State and give a brief explanation of the Church-Turing thesis. + +** Answer +The Church-Turing thesis states that "effective" computation can be carried out by several methods. +In this case, effective means a set of structured finite instructions, that requires no knowledge except for the instructions themselves. +Further, given that the instructions, given that no error occurs, then the result should be completed in finite time. +* (1 point) +Give an example of a function on the natural numbers (from $\mathbb{N}$ to $\mathbb{N}$) that is: +- Injective but not surjective. +- Bijective. + +** Answer +$\lambda x. x + 1$ is injective and not surjective. This comes from that each natural number has a successor (injective), but $0$ is not the image of any value (not surjective). + +$\lambda x. x$ is bijective, which is trivial, since each input is their own image. + +* (1 point) +Is $\mathbb{N} \times \text{Bool}$ countable? Provide a proof. (Bool is a set with two elements, true and false.) + +** Answer +$\mathbb{N} \times \text{Bool}$ is countable. +One way to prove this is by isomorphism between $\mathbb{N} \times \text{Bool}$ and $\mathbb{N} + \mathbb{N}$. +To show this isomorphism, we need two functions $f \in \mathbb{N} \times \text{Bool} \rightarrow \mathbb{N} + \mathbb{N}$ and $g \in \mathbb{N} + \mathbb{N} \rightarrow \mathbb{N} \times \text{Bool}$, such that $f \circ g = \text{Id}_{\mathbb{N} + \mathbb{N}}$ and that $g \circ f = \text{Id}_{\mathbb{N} \times \text{Bool}}$. +So, let $f = \lambda (n,b).\ \text{if}\ b\ \text{then}\ \text{Inr}\ n\ \text{else}\ \text{Inl}\ n$ and $g = \lambda (x).\ \text{case}\ x\ \text{of}\ \text{Inl}\ n \rightarrow (n,\text{False});\ \text{Inr}\ n \rightarrow (n,True)$ +Now, these are trivially isomorphic, and thus will not be shown. + +Since this these functions are isomorphic, they are also injective, which means that if $\mathbb{N} + \mathbb{N}$ is countable, then $\mathbb{N} \times \text{Bool}$ will also be so. +In the literature for this week (namely Enumerable sets and Hilbert's hotel), it is shown that $\mathbb{N} + \mathbb{N}$ is countable, and therefore $\mathbb{N} \times \text{Bool}$. + +*** Alternative solution + +This can be answered by creating a function $f \in \mathbb{N} \times \text{Bool} \rightarrow \mathbb{N}$ that is injective. +I define it as $f = \lambda (x,b). if b then 2 \cdot x + 1 else 2 \cdot x$. +To show that it is injective, let's do a proof by contradiction. +Assume that $(n_1, b_1) \ne (n_2, b_2)$ and $f (n_1, b_1) = f (n_2, b_2) = c$. +If $c$ is odd, then $b_1$ and $b_2$ have be $\text{True}$, further, then $n_1$ and $n_2$ have to $\frac{c - 1}{2}$, thus creating a contradiction. +If $c$ is even, then $b_1$ and $b_2$ have be $\text{False}$, further, then $n_1$ and $n_2$ have to $\frac{c}{2}$, thus creating a contradiction. +In both cases a contradiction is raised, meaning that the function is injective, and thus $\mathbb{N} \times \text{Bool}$ is countable. + +* (1 Point) [BN] +Is $\mathbb{N} \rightarrow \text{Bool}$ countable? Provide a proof. + +** Answer +No. + +Assume that it is countable. +Then one could enumerate them as $f_0, f_1, \dots$. +Then lets create a function $d = \lambda i. \neg (f_i i)$. +Assume that $d$ is in the set of functions, that is to say that $d = f_k$ for some k. +If that was the case, then $d\ k = \neg (f_k\ k) = \neg (d\ k)$ which is a contradition. +Thus $d$ cannot be in the set of functions, which in of it self creates a contradiction that it is enumerable. diff --git a/2.org b/2.org new file mode 100644 index 0000000..329c119 --- /dev/null +++ b/2.org @@ -0,0 +1,59 @@ +#+title: Assignment 2 +#+options: toc:nil +#+latex_header: \usepackage{parskip} + +In order to pass this assignment you have to get at least three points. (Minor mistakes may be accepted.) + +Please provide your source code in a form that is easy to test, not, say, a PDF file. + +(Exercises marked with [BN] are based on exercises from a previous version of this course, given by Bengt Nordström.) + +* (1p) +Give a brief explanation of the relationship between inductively defined sets, primitive recursion, and proofs by structural induction. + +Here “primitive recursion” refers to the general concept, not the model of computation called PRF that is discussed in the course. + +** Answer +Each inductively defined set has a number of constructors. +To prove something about these sets, the proposition needs to hold for the individual constructors, and the information that they hold. +In particular, if this definition is recursive in nature, one can depend that the recursion itself holds the proposition. +For natural numbers defined as $\mathbb{N} := \text{zero} | \text{succ}\ n$, that would look like $\text{P}\ \text{zero}\ \land (\forall n \in \mathbb{N}. \text{P}\ n \rightarrow \text{P}\ (\text{succ}\ n)) \rightarrow \forall n \in \mathbb{N}. \text{P}\ n$. +This proof on the structure is a generalized version of primitive recursion, which would have that $\text{P}$ be a function. +For natural numbers, that would be $A \land (\mathbb{N} \rightarrow A \rightarrow A) \rightarrow \mathbb{N} \rightarrow A$. + +* (1p) [BN] +Define the integers inductively, implement this definition as a data type in a functional programming language (for instance Agda or Haskell), and show how the numbers -1, 0, 1 and 3 are represented using your definition. It should be easy to implement simple functions like addition and multiplication using your representation (but you don’t have to do this). + +Do not use the incorrect definition from [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/reading/Some_mathematical_preliminaries.pdf][Some mathematical preliminaries: sets, relations and functions]]. Be careful so that you avoid off-by-one errors. Make sure that every integer can be constructed using your definition, that every object that can be constructed corresponds to an integer, and that no two distinct objects correspond to the same integer. + +/Hint/: Define the integers in terms of the natural numbers. + +** Answer +See file attached. +* (1p) [BN] +[[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/reading/Some_mathematical_preliminaries.pdf][Some mathematical preliminaries: sets, relations and functions]] mentions a higher-order function rec. Give the type of and implement an analogous function zrec for your definition of integers. Use this function to implement a function that adds one to an integer, without using pattern matching or recursion. + +If your inductive definition of the integers is not recursive (i.e. if the integers are not defined in terms of the integers), then zrec should not be recursive. Furthermore, if your inductive definition of the integers has n constructors, then there should be n cases in the implementation of zrec, one for each constructor. + +Test that your function works. If it doesn’t, then you will not get full credit. + +Note that if you define the integers in terms of another inductively defined set (like the natural numbers), then you can also use the higher-order recursion function for that set (like rec) when defining the successor function for the integers. + +** Answer +See file attached. +* (2p) [BN] +The [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/lectures/L3.pdf][slides]] for the third lecture contain an (indexed) inductive definition of the abstract syntax of the primitive recursive functions. Represent this definition as a data type in a functional programming language, show how one can encode addition of two natural numbers as a value in this type, and implement the denotational semantics of PRF as a function from your data type and a vector of natural numbers to a natural number. + +Depending on what language you use it may be hard to handle the natural number indices /(n in PRF n)/, so you are allowed to omit them. If you do, implement the following inductive definition: + +- $\text{zero} \in PRF$. +- $\text{suc} \in PRF$. +- $\text{proj}\ i \in PRF$ if $i \in \mathbb{N}$. +- $\text{comp}\ f\ gs \in PRF$ if $f \in PRF$ and $gs \in \text{List}\ PRF$. +- $\text{rec}\ f\ g \in PRF$ if $f, g \in PRF$. + +You are also allowed to represent fixed-length vectors by arbitrary-length vectors/lists, and to represent natural numbers using some kind of integer type. If you detect malformed input, then you can give an error message. + +Test that addition works for some inputs. If it doesn’t, then you will not get full credit. +** Answer +See file attached. diff --git a/3/.envrc b/3/.envrc new file mode 100644 index 0000000..3550a30 --- /dev/null +++ b/3/.envrc @@ -0,0 +1 @@ +use flake diff --git a/3/.gitignore b/3/.gitignore new file mode 100644 index 0000000..81f9a80 --- /dev/null +++ b/3/.gitignore @@ -0,0 +1,20 @@ +.DS_Store +.idea +*.log +tmp/ + +AbsChi.hs +DocChi.txt +ErrM.hs +LexChi.x +ParChi.y +PrintChi.hs +SkelChi.hs +TestChi.hs + +.direnv/ +dist-newstyle/ + +*.bbl +*.pdf +*.tex diff --git a/3/Chi.cf b/3/Chi.cf new file mode 100644 index 0000000..e376adb --- /dev/null +++ b/3/Chi.cf @@ -0,0 +1,27 @@ +token Constructor (["ABCDEFGHIJKLMNOPQRSTUVWXYZ"] + (["abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ_-'"] + | digit + )*); +token Variable (["abcdefghijklmnopqrstuvwxyz_"] + (["abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ_-'"] + | digit + )*); + +Apply . Exp1 ::= Exp1 Exp2; +Lambda . Exp ::= "\\" Variable "." Exp; +Case . Exp1 ::= "case" Exp "of" "{" [Br] "}"; +Rec . Exp ::= "rec" Variable "=" Exp; +Var . Exp2 ::= Variable; +Const . Exp2 ::= Constructor "(" [Exp] ")"; +_ . Exp ::= Exp1; +_ . Exp1 ::= Exp2; +_ . Exp2 ::= "(" Exp ")"; + +Branch . Br ::= Constructor "(" [Variable] ")" "->" Exp; + +separator Br ";"; +separator Exp ","; +separator Variable ","; + +comment "--"; +comment "{-" "-}"; diff --git a/3/Chi.hs b/3/Chi.hs new file mode 100644 index 0000000..d73186b --- /dev/null +++ b/3/Chi.hs @@ -0,0 +1,787 @@ +-- | A wrapper module that exports the generated abstract syntax of χ +-- as well as some definitions that may be useful when testing χ code +-- or interpreters. + +{-# LANGUAGE DeriveGeneric, + GeneralizedNewtypeDeriving, + PatternSynonyms, + StandaloneDeriving, + TemplateHaskell #-} + +module Chi + ( -- * The abstract syntax of χ + module AbsChi + -- * Parsing and pretty-printing + , parse + , pretty + -- * An example + , add + -- * Conversions + , fromNatural + , toNatural + , Code + , Decode + , runCode + , runDecode + , asDecoder + , code + , decode + , codeVar + , codeCon + , decodeVar + , decodeCon + , internalCode + -- * Free and bound variables + , free + , bound + , closed + -- * Functions that can be used to run internal substitution functions and self-interpreters + , runInternalSubstitution + , runSelfInterpreter + -- * Some testing procedures + , testEvaluation + , testMultiplication + , testSubstitution + , testInternalSubstitutionWith + , testInternalSubstitution + , testSelfInterpreterWith + , testSelfInterpreter + , testTuringMachineInterpreter + ) + where + +import AbsChi +import Control.Applicative + (Applicative, Alternative, (<$>), (<*>), empty) +import Control.Monad.State.Strict (State, evalState, put, get) +import Control.Monad.Trans (lift) +import Control.Monad.Trans.Maybe (MaybeT(MaybeT), runMaybeT) +import Data.Hashable (Hashable) +import Data.HashMap.Strict (HashMap) +import qualified Data.HashMap.Strict as Map +import Data.HashSet (HashSet) +import qualified Data.HashSet as Set +import Data.List (genericReplicate) +import Data.Typeable (Typeable) +import GHC.Generics (Generic) +import Numeric.Natural (Natural) +import ParChi (pExp, myLexer) +import PrintChi (printTree) +import Text.PrettyPrint.HughesPJ (fsep, nest, render, text, vcat, (<+>)) +import Test.QuickCheck + (Arbitrary(arbitrary, shrink), Gen, NonNegative(NonNegative), + Property, Testable, arbitrarySizedNatural, choose, counterexample, + elements, forAll, forAllShrink, genericShrink, maxSuccess, oneof, + quickCheckAll, quickCheckResult, quickCheckWithResult, + shrinkIntegral, sized, stdArgs, vectorOf, (.&&.), (==>)) +import Test.QuickCheck.Test (isSuccess) + +------------------------------------------------------------------------ +-- Some orphan instances for types defined in AbsChi + +deriving instance Generic Constructor +deriving instance Generic Variable +deriving instance Generic Exp +deriving instance Generic Br + +instance Hashable Constructor +instance Hashable Variable + +------------------------------------------------------------------------ +-- Orphan Arbitrary instances and related definitions + +-- | A combinator that can be used to construct properties involving +-- universal quantification over natural numbers. + +forAllNatural :: Testable p => (Natural -> p) -> Property +forAllNatural = forAllShrink arbitrarySizedNatural shrinkIntegral + +-- | A QuickCheck generator for (a small number of) constructors. + +instance Arbitrary Constructor where + arbitrary = elements $ map Constructor ["Zero", "Suc"] + + shrink (Constructor "Suc") = [Constructor "Zero"] + shrink _ = [] + +-- | A QuickCheck generator for (a small number of) variables. + +instance Arbitrary Variable where + arbitrary = elements $ map Variable ["x", "y"] + + shrink (Variable "y") = [Variable "x"] + shrink _ = [] + +-- | A QuickCheck generator for branches. + +instance Arbitrary Br where + arbitrary = Branch <$> arbitrary <*> arbitrary <*> arbitrary + + shrink = genericShrink + +-- | A QuickCheck generator for terms. + +instance Arbitrary Exp where + arbitrary = sized gen + where + gen n = oneof $ + [ Var <$> arbitrary ] ++ + if n <= 0 then [] else + [ Apply <$> g <*> g + , Lambda <$> arbitrary <*> g + , Case <$> g <*> do + i <- choose (0, n `div` 3) + es <- vectorOf i g + mapM (\e -> Branch <$> arbitrary + <*> do i <- choose (0, n `div` 3) + vectorOf i arbitrary + <*> return e) es + , Rec <$> arbitrary <*> g + , Const <$> arbitrary <*> do + n <- choose (0, n `div` 3) + vectorOf n g + ] + where + g = gen (n `div` 2) + + shrink = genericShrink + +------------------------------------------------------------------------ +-- Parsing and pretty-printing + +-- | Tries to parse a χ program. If parsing fails, then an exception +-- is raised. + +parse :: String -> Exp +parse s = case pExp (myLexer s) of + Right e -> e + Left s -> error ("Parse failed: " ++ s) + +-- | Pretty-prints a χ program. + +pretty :: Exp -> String +pretty = printTree + +prop_parse_pretty e = + parse (pretty e) == e + +------------------------------------------------------------------------ +-- An example + +-- | A χ program for addition of natural numbers. + +add :: Exp +add = parse + "rec add = \\x. \\y. case x of\ + \ { Zero() -> y\ + \ ; Suc(n) -> Suc(add n y)\ + \ }" + +------------------------------------------------------------------------ +-- Free and bound variables + +-- | Helper function used to implement 'free' and 'bound'. + +freeAndBound :: Exp -> (HashSet Variable, HashSet Variable) +freeAndBound e = case e of + Var x -> (Set.singleton x, Set.empty) + Lambda x e -> let (f, b) = freeAndBound e in + (Set.delete x f, if Set.member x f + then Set.insert x b + else b) + Rec x e -> freeAndBound (Lambda x e) + Case e bs -> freeAndBoundL (e : map (\(Branch _ xs e) -> + foldr Lambda e xs) + bs) + Apply e1 e2 -> freeAndBoundL [e1, e2] + Const _ es -> freeAndBoundL es + where + freeAndBoundL :: [Exp] -> (HashSet Variable, HashSet Variable) + freeAndBoundL es = (Set.unions fs, Set.unions bs) + where (fs, bs) = unzip $ map freeAndBound es + +-- | The term's free variables. + +free :: Exp -> HashSet Variable +free e = fst (freeAndBound e) + +-- | Bound variables that actually occur bound in the term (not in a +-- binder). For @λx.x@ a singleton set containing @x@ is returned, but +-- for @λx.Nil()@ the empty set is returned. + +bound :: Exp -> HashSet Variable +bound e = snd (freeAndBound e) + +-- | A QuickCheck generator for closed terms. + +closed :: Gen Exp +closed = do + e <- arbitrary + let xs = free e + bs <- mapM binder (Set.toList xs) + return $ foldr ($) e bs + where + binder x = elements [Rec x, Lambda x] + +prop_closed = + forAll closed $ \e -> + free e == Set.empty + +------------------------------------------------------------------------ +-- Conversions + +-- | Converts a Haskell natural number to its χ representation. + +fromNatural :: Natural -> Exp +fromNatural n + | n == 0 = Const (Constructor "Zero") [] + | otherwise = Const (Constructor "Suc") [fromNatural (n - 1)] + +-- | Tries to convert the given χ expression to a natural number. + +toNatural :: Exp -> Maybe Natural +toNatural e = case e of + Const (Constructor "Zero") [] -> Just 0 + Const (Constructor "Suc") [n] -> succ <$> toNatural n + _ -> Nothing + +prop_toNatural_fromNatural = + forAllNatural $ \n -> + toNatural (fromNatural n) == Just n + +-- | Partial bijections between strings and natural numbers. + +data PartialBijection = + Maps (HashMap String Natural) + (HashMap Natural String) + +-- | Encoding monad. + +newtype Code a = Code (State PartialBijection a) + deriving (Functor, Applicative, Monad) + +-- | Decoding monad. + +newtype Decode a = Decode (MaybeT Code a) + deriving (Functor, Applicative, Alternative, Monad) + +-- | Runs a coder. +-- +-- Note that coding might not give consistent results if you invoke +-- 'runCode' multiple times. For instance, the following code will +-- return 'False': +-- +-- @ +-- runCode (code (parse "Suc(Zero())")) +-- == +-- runCode (do +-- code (parse "Zero()") +-- code (parse "Suc(Zero())")) +-- @ + +runCode :: Code a -> a +runCode (Code m) = evalState m (Maps Map.empty Map.empty) + +prop_runCode_inconsistent = not $ + runCode (code (parse "Suc(Zero())")) + == + runCode (do + code (parse "Zero()") + code (parse "Suc(Zero())")) + +-- | Runs a decoder. Note that decoders can fail. + +runDecode :: Decode a -> Maybe a +runDecode (Decode m) = runCode (runMaybeT m) + +-- | Turns a coder into a decoder. +-- +-- Example usage: +-- +-- @ +-- do e <- 'asDecoder' ('code' e) +-- 'decode' (eval ('Apply' selfInterpreter e)) +-- @ + +asDecoder :: Code a -> Decode a +asDecoder = Decode . lift + +-- | Converts a string to a natural number. + +fromString :: String -> Code Natural +fromString s = do + Maps strMap natMap <- Code get + case Map.lookup s strMap of + Just n -> return n + Nothing -> do + let n = fromIntegral $ Map.size strMap + Code (put (Maps (Map.insert s n strMap) + (Map.insert n s natMap))) + return n + +-- | Tries to convert a natural number to a string. + +toString :: Natural -> Decode String +toString n = Decode $ MaybeT $ Code $ do + Maps _ natMap <- get + return (Map.lookup n natMap) + +-- | Encodes strings. + +codeString :: String -> Code Exp +codeString s = fromNatural <$> fromString s + +-- | Decodes strings. + +decodeString :: Exp -> Decode String +decodeString e = do + n <- Decode (MaybeT (return (toNatural e))) + toString n + +-- | Encodes variables. + +codeVar :: Variable -> Code Exp +codeVar (Variable s) = codeString s + +-- | Decodes variables. + +decodeVar :: Exp -> Decode Variable +decodeVar e = Variable <$> decodeString e + +-- | Encodes constructors. + +codeCon :: Constructor -> Code Exp +codeCon (Constructor s) = codeString s + +-- | Decodes constructors. + +decodeCon :: Exp -> Decode Constructor +decodeCon e = Constructor <$> decodeString e + +-- | Encodes expressions. + +code :: Exp -> Code Exp +code e = case e of + Apply e1 e2 -> constr "Apply" [code e1, code e2] + Lambda x e -> constr "Lambda" [codeVar x, code e] + Case e bs -> constr "Case" [code e, codeList codeBr bs] + Rec x e -> constr "Rec" [codeVar x, code e] + Var x -> constr "Var" [codeVar x] + Const c es -> constr "Const" [codeCon c, codeList code es] + where + constr c args = Const (Constructor c) <$> sequence args + + codeBr :: Br -> Code Exp + codeBr (Branch c xs e) = + constr "Branch" [codeCon c, codeList codeVar xs, code e] + + codeList :: (a -> Code Exp) -> [a] -> Code Exp + codeList r [] = constr "Nil" [] + codeList r (x : xs) = constr "Cons" [r x, codeList r xs] + +-- | Decodes expressions. + +decode :: Exp -> Decode Exp +decode e = case e of + Const (Constructor c) args -> case (c, args) of + ("Apply", [e1, e2]) -> Apply <$> decode e1 <*> decode e2 + ("Lambda", [x, e]) -> Lambda <$> decodeVar x <*> decode e + ("Case", [e, bs]) -> Case <$> decode e <*> decodeList decodeBr bs + ("Rec", [x, e]) -> Rec <$> decodeVar x <*> decode e + ("Var", [x]) -> Var <$> decodeVar x + ("Const", [c, es]) -> Const <$> decodeCon c + <*> decodeList decode es + _ -> empty + _ -> empty + where + decodeBr :: Exp -> Decode Br + decodeBr (Const (Constructor "Branch") [c, xs, e]) = + Branch <$> decodeCon c <*> decodeList decodeVar xs <*> decode e + decodeBr _ = empty + + decodeList :: (Exp -> Decode a) -> Exp -> Decode [a] + decodeList decode e = case e of + Const (Constructor c) args -> case (c, args) of + ("Nil", []) -> return [] + ("Cons", [x, xs]) -> (:) <$> decode x <*> decodeList decode xs + +prop_decode_code e = + runDecode (decode =<< asDecoder (code e)) == Just e + +-- | An internal implementation of coding. +-- +-- Example usage: +-- +-- @ +-- 'runCode' $ do +-- ic <- 'internalCode' +-- ce <- 'code' e +-- return (eval ('Apply' ic ce)) +-- @ + +internalCode :: Code Exp +internalCode = do + bs <- sequence + [ branch 0 "Zero" + , branch 1 "Suc" + , branch 0 "Nil" + , branch 2 "Cons" + , branch 2 "Apply" + , branch 2 "Lambda" + , branch 2 "Case" + , branch 2 "Rec" + , branch 1 "Var" + , branch 2 "Const" + , branch 3 "Branch" + ] + return $ + Rec (Variable "code") $ + Lambda (Variable "p") $ + Case (Var (Variable "p")) bs + where + args = map (Variable . ("x" ++) . show) [(1 :: Integer)..] + + branch n c = do + cc <- codeCon (Constructor c) + return $ + Branch (Constructor c) (take n args) $ + Const (Constructor "Const") $ + [ cc + , foldr (\arg rest -> + Const (Constructor "Cons") + [ Apply (Var (Variable "code")) (Var arg) + , rest + ]) + (Const (Constructor "Nil") []) + (take n args) + ] + +-- The following test case depends on an implementation of evaluation +-- (eval), and is therefore commented out. + +-- prop_internalCode :: Exp -> Bool +-- prop_internalCode e = runCode $ do +-- internalCode <- internalCode +-- ce <- code e +-- cce <- code ce +-- return $ eval (Apply internalCode ce) == cce + +------------------------------------------------------------------------ +-- Functions that can be used to run internal substitution functions +-- and self-interpreters + +-- | Tries to compute the value of the given internal substitution +-- function applied to the given arguments. +-- +-- If the application terminates, and the result can be decoded, then +-- this result is returned. +-- +-- Example usage: +-- +-- @ +-- 'runInternalSubstitution' eval internalSubst +-- (Variable "plus") 'add' ('parse' "plus") +-- @ + +runInternalSubstitution + :: (Exp -> Exp) -- ^ Evaluation. + -> Exp -- ^ Internal substitution. + -> Variable -- ^ The variable. + -> Exp -- ^ The closed expression that should be + -- substituted for the variable (not in coded + -- form). + -> Exp -- ^ The possibly open expression in which the + -- closed expression should be substituted for + -- the variable (not in coded form). + -> Maybe Exp +runInternalSubstitution eval internalSubst x e e' = runDecode $ do + x <- asDecoder $ codeVar x + e <- asDecoder $ code e + e' <- asDecoder $ code e' + decode (eval (foldl1 Apply [internalSubst, x, e, e'])) + +-- | Uses a self-interpreter to evaluate a program applied to some +-- arguments. +-- +-- If the self-interpreter terminates, and the result can be decoded, +-- then this result is returned. +-- +-- Example usage: +-- +-- @ +-- do n <- 'runSelfInterpreter' eval selfInterpreter 'add' +-- ['fromNatural' 2, 'fromNatural' 2] +-- 'toNatural' n +-- @ + +runSelfInterpreter + :: (Exp -> Exp) -- ^ An implementation of evaluation. + -> Exp -- ^ The self-interpreter. + -> Exp -- ^ The program to be evaluated (not in coded form). + -> [Exp] -- ^ The program's arguments (not in coded form). + -> Maybe Exp +runSelfInterpreter eval selfInterpreter p args = runDecode $ do + term <- asDecoder (code (foldl1 Apply (p : args))) + decode (eval (Apply selfInterpreter term)) + +------------------------------------------------------------------------ +-- Some testing procedures + +-- | Tests whether a purported implementation of evaluation can +-- evaluate addition of two natural numbers ('add') correctly. +-- +-- The test is, of course, incomplete. + +testEvaluation :: (Exp -> Exp) -> IO Bool +testEvaluation eval = + isSuccess <$> + quickCheckResult + (forAllNatural $ \m -> + forAllNatural $ \n -> + eval (Apply (Apply add (fromNatural m)) (fromNatural n)) == + fromNatural (m + n)) + +-- | Tests whether a purported implementation of evaluation and a +-- purported implementation of multiplication of two natural numbers +-- are correct. +-- +-- The test is, of course, incomplete. + +testMultiplication + :: (Exp -> Exp) -- ^ Evaluation. + -> Exp -- ^ Multiplication. The program should take two + -- natural numbers as input and produce a natural + -- number as its result. + -> IO Bool +testMultiplication eval mul = + isSuccess <$> + quickCheckResult + (forAllNatural $ \m' -> + forAllNatural $ \n' -> + let m = m' `div` 2; n = n' `div` 2 in + eval (Apply (Apply mul (fromNatural m)) (fromNatural n)) == + fromNatural (m * n)) + +-- | Tests a purported implementation of substitution. +-- +-- The substitution operation takes three arguments, @x@, @e@ and +-- @e'@, where @e@ is closed, and should substitute @e@ for every free +-- occurrence of @x@ in @e'@. +-- +-- The test is designed for substitution operations that are +-- implemented exactly like in the χ specification. In particular, the +-- substitution operation should not rename any bound variables. +-- +-- The test is, of course, incomplete. + +testSubstitution :: (Variable -> Exp -> Exp -> Exp) -> IO Bool +testSubstitution subst = + isSuccess <$> + quickCheckResult + (\e' -> + forAll closed $ \e -> + let fs = free e' + fbs = fs `Set.intersection` bound e' + var ys = elements (Set.toList ys) + in + (forAll (var (Set.insert (Variable "x") fs)) $ \x -> + counterexample' x e e' + (\x -> "However, FV e'' /= FV e' - {" ++ x ++ "}.") $ + free (subst x e e') == Set.delete x fs) + .&&. + (not (Set.null fs) && not (isVar e) ==> + forAll (var fs) $ \x -> + counterexample' x e e' + (\x -> + "However, e'' = e' (which should not hold, because " ++ + x ++ " is free in e' and e is not a variable).") $ + subst x e e' /= e') + .&&. + (not (Set.null fbs) ==> + forAll (var fbs) $ \x -> + counterexample' x e e' + (\x -> + "However, bound e'' /= union (bound e) (bound e') " ++ + "(the two sides should be equal, because " ++ x ++ + " is free in e' and bound in e).") $ + bound (subst x e e') + == + bound e `Set.union` bound e')) + where + isVar Var{} = True + isVar _ = False + + para = fsep . map text . words + + def s e = + nest 2 $ vcat $ + [text s <+> text "="] ++ + map (nest (length s + 3) . text) (lines (pretty e)) + + counterexample' x e e' s = + counterexample $ + render $ vcat $ + [ para "This counterexample uses the following values:" + , def "e " e + , def "e'" e' + , para $ + "Note that e is closed. " ++ + "Your implementation gives the following value " ++ + "for e'[" ++ px ++ " <- e]:" + , def "e''" (subst x e e') + , para (s px) + ] + where + px = pretty (Var x) + +-- | Tests if the result of the given internal substitution function +-- matches that of the given substitution function for given inputs. +-- +-- Note that no result is returned if some program crashes or fails to +-- terminate. +-- +-- Example usage: +-- +-- @ +-- 'testInternalSubstitutionWith' eval subst internalSubst +-- ('Variable' "plus") 'add' ('parse' "plus") +-- @ + +testInternalSubstitutionWith + :: (Exp -> Exp) -- ^ Evaluation. + -> (Variable -> Exp -> Exp -> Exp) -- ^ Substitution. + -> Exp -- ^ Internal substitution. + -> Variable -- ^ The variable. + -> Exp -- ^ The closed expression that + -- should be substituted for + -- the variable (not in coded + -- form). + -> Exp -- ^ The possibly open + -- expression in which the + -- closed expression should be + -- substituted for the + -- variable (not in coded + -- form). + -> Bool +testInternalSubstitutionWith eval subst internalSubst x e e' = + runInternalSubstitution eval internalSubst x e e' + == + Just (subst x e e') + +-- | Tests whether an implementation of internal substitution matches +-- an implementation of substitution. +-- +-- The test is, of course, incomplete. + +testInternalSubstitution + :: (Exp -> Exp) -- ^ Evaluation. + -> (Variable -> Exp -> Exp -> Exp) -- ^ Substitution. + -> Exp -- ^ Internal substitution. + -> IO Bool +testInternalSubstitution eval subst internalSubst = + isSuccess <$> + quickCheckResult (\e' -> + forAll closed $ \e -> + forAll (elements $ Set.toList $ + Set.insert (Variable "x") $ free e') $ \x -> + testInternalSubstitutionWith eval subst internalSubst x e e') + +-- | Tests if the result of the given self-interpreter matches that of +-- the given evaluator for a program applied to some arguments. +-- +-- Note that no result is returned if some program crashes or fails to +-- terminate. +-- +-- Example usage: +-- +-- @ +-- 'testSelfInterpreterWith' eval selfInterpreter 'add' +-- ['fromNatural' 2, 'fromNatural' 2] +-- @ + +testSelfInterpreterWith + :: (Exp -> Exp) -- ^ Evaluation. + -> Exp -- ^ The self-interpreter. + -> Exp -- ^ The program to be evaluated (not in coded form). + -> [Exp] -- ^ The arguments (not in coded form). + -> Bool +testSelfInterpreterWith eval selfInterpreter p args = + runSelfInterpreter eval selfInterpreter p args + == + Just (eval (foldl1 Apply (p : args))) + +-- | Tests whether a purported implementation of evaluation and a +-- purported self-interpreter are correctly implemented. +-- +-- The test is, of course, incomplete. + +testSelfInterpreter + :: (Exp -> Exp) -- ^ Evaluation. + -> Exp -- ^ The self-interpreter. + -> IO Bool +testSelfInterpreter eval selfInterpreter = + isSuccess <$> + quickCheckResult + (forAllNatural $ \m -> + (forAllNatural $ \n -> + testSelfInterpreterWith eval selfInterpreter + add [fromNatural (m `min` 5), fromNatural (n `min` 5)]) + .&&. + testSelfInterpreterWith eval selfInterpreter + add' [fromNatural m]) + where + add' :: Exp + add' = parse $ unlines + [ "rec add = \\m. case m of" + , " { Zero() -> \\n. n" + , " ; Suc(m) -> \\n. add m Suc(n)" + , " }" + ] + +-- | Tests whether a purported implementation of evaluation and a +-- purported Turing machine interpreter are correctly implemented. The +-- Turing machine interpreter should satisfy the specification given +-- in Assignment 6. +-- +-- The test is, of course, incomplete. + +testTuringMachineInterpreter + :: (Exp -> Exp) -- ^ Evaluation. + -> Exp -- ^ The Turing machine interpreter. + -> IO Bool +testTuringMachineInterpreter eval tmInterpreter = + isSuccess <$> + quickCheckWithResult + (stdArgs { maxSuccess = 36 }) + (forAll smallNumber $ \m -> + forAll smallNumber $ \n -> + eval (foldl1 Apply [ tmInterpreter + , add + , fromList (ones m ++ [0] ++ ones n) + ]) + == + fromList (ones (m + n))) + where + smallNumber :: Gen Natural + smallNumber = fromInteger <$> choose (0, 5) + + ones :: Natural -> [Natural] + ones n = genericReplicate n 1 + + fromList :: [Natural] -> Exp + fromList [] = Const (Constructor "Nil") [] + fromList (n : ns) = + Const (Constructor "Cons") [fromNatural n, fromList ns] + + add :: Exp + add = Const (Constructor "TM") [Const (Constructor "Zero") [],Const (Constructor "Cons") [Const (Constructor "Rule") [Const (Constructor "Zero") [],Const (Constructor "Zero") [],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "R") []],Const (Constructor "Cons") [Const (Constructor "Rule") [Const (Constructor "Zero") [],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "Zero") [],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "R") []],Const (Constructor "Cons") [Const (Constructor "Rule") [Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "Blank") [],Const (Constructor "Suc") [Const (Constructor "Suc") [Const (Constructor "Zero") []]],Const (Constructor "Blank") [],Const (Constructor "L") []],Const (Constructor "Cons") [Const (Constructor "Rule") [Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "R") []],Const (Constructor "Cons") [Const (Constructor "Rule") [Const (Constructor "Suc") [Const (Constructor "Suc") [Const (Constructor "Zero") []]],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "Suc") [Const (Constructor "Suc") [Const (Constructor "Suc") [Const (Constructor "Zero") []]]],Const (Constructor "Blank") [],Const (Constructor "L") []],Const (Constructor "Nil") []]]]]]] + +------------------------------------------------------------------------ +-- Internal tests + +return [] + +-- | Runs all the internal tests. + +tests :: IO Bool +tests = $quickCheckAll diff --git a/3/assig.org b/3/assig.org new file mode 100644 index 0000000..290684c --- /dev/null +++ b/3/assig.org @@ -0,0 +1,119 @@ +#+title: Assignment 3 +#+options: toc:nil +#+latex_header: \usepackage{parskip} + +* Supporting files + +~This~ time you can make use of a [[http://bnfc.digitalgrammars.com/][BNFC]] specification ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.cf][~Chi.cf~]]) of a variant of the concrete syntax of $\chi$. This grammar gives specific rules for variable and constructor names, and differs from the concrete syntax presented in the lectures in some ways: +# TODO: Fix ' +- Variables and constructors are sequences of letters (~a~ to ~z~ and ~A~ to ~Z~), digits (~0~ to ~9~), underscores (~_~), dashes (~-~) and primes ('), and variables have to start with lower-case letters or underscores, whereas constructors have to start with upper-case letters. +- Lambdas are written using backslash characters (~\~) and arrows are written using the string ~->~. +- End-of-line comments of the form ~-- ...~ are allowed, as are (non-nested) comments of the form ~{- ... -}~. +- There can be a final comma after a non-empty list of constructor arguments, and there can be a final semicolon after a non-empty list of branches. +- Parentheses are treated differently. Superfluous parentheses are allowed around expressions. Some parentheses can be omitted; application is treated as a left-associative operation. Note that some grammatically correct expressions actually parse differently with this variant of the grammar, for instance ~(rec x = x y)~ which is interpreted as ~rec x = (x y)~ rather than ~(rec x = x) y~ (which was previously grammatically incorrect). See the [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.cf][grammar]] for details. + +If you want to use Haskell then there is also a wrapper module ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.cf][~Chi.cf~]]) that exports the generated abstract syntax and some definitions that may be useful for testing your code ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.html][documentation]]). The wrapper module comes with a Cabal file ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/chi.cabal][~chi.cabal~]]) and a [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/cabal.project][~cabal.project~]] file that might make installation a little easier. Here is one way to (hopefully) get started: + +- Install all dependencies properly, including suitable versions of GHC and cabal-install ([[https://www.haskell.org/downloads/][installation instructions]]), as well as [[http://bnfc.digitalgrammars.com/][BNFC]]. +- Put [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.cf][~Chi.cf~]], [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.hs][~Chi.hs~]], [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/chi.cabal][~chi.cabal~]] and [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/cabal.project][~cabal.project~]] in an otherwise empty directory. +- Run ~bnfc --haskell Chi.cf~ in that directory. + - Now it is hopefully possible to use standard ~cabal~ commands. You could for instance try the following (still in the same directory): + - First use cabal repl to start GHCi. + - Then issue the following commands at the GHCi command prompt: + #+begin_src haskell + import Chi + import Prelude + pretty <$> (runDecode (decode =<< + asDecoder (code =<< code (parse "\\x. x")))) + #+end_src + +* Exercises +In order to pass this assignment you have to get at least four points. + +Please provide your source code in a form which is easy to test, not, say, a PDF file. Do not submit the files provided on this page or the generated code, only the code that you write. + +(Exercises marked with [BN] are based on exercises from a previous version of this course, given by Bengt Nordström.) + +** (1p) +Consider the following $\chi$ program: +#+begin_src chi +rec foo = \m. \n. case m of + { Zero() → case n of + { Zero() → True() + ; Suc(n) → False() + } + ; Suc(m) → case n of + { Zero() → False() + ; Suc(n) → foo m n + } + } +#+end_src +Give a high-level explanation of the mathematical function in $\mathbb{N} \rightarrow \mathbb{N} \rightarrow \text{Bool}$ that is implemented by this code. + +*** Answer +The function will check for equality of the two natural numbers. If they are both $Zero()$, then it returns true, and if both are the successor of a some values, it checks if they are equal. In the other cases, it returns false. + +** (2p) +Consider the $\chi$ term /t/ with concrete syntax $C (\lambda z.z)$: +- Give the abstract syntax corresponding to /t/. Use the abstract syntax presented in the lectures. The answer should be a value in the set /Exp/. +- Give the concrete syntax of the (standard) $\chi$ representation of /t/. +- Give the abstract syntax of the (standard) $\chi$ representation of /t/. + +In the abstract syntax the constructor ~C~ should be represented by $\underline{C} \in \text{Const}$, and the variable ~z~ by $\underline{z} \in \text{Var}$. When giving the $\chi$ representation of the term you should use (the representation of) the number 0 to represent $\underline{C}$, and 1 to represent $\underline{z}$. +*** Answer +The abstract syntax is the following: $\text{const}\ \underline{C}\ (\text{cons}\ (\text{lambda}\ \underline{z}\ (\text{var}\ \underline{z}))\ \text{nil})$. + +The concrete syntax of the standard representation is the following: $Const(\ulcorner \underline{C} \urcorner, Cons(Lambda(\ulcorner \underline{z} \urcorner, Cons (Var(\ulcorner \underline{z} \urcorner), Nil())), Nil())$ +# TODO: check paranthesis above + +** (2p) [BN] + +Implement substitution for $\chi$. The function should take three arguments, a variable, a closed term, and another term, and substitute the first term for every free occurrence of the variable in the second term. + +If you use the BNFC specification above and Haskell, then the substitution function should have the following type: +#+begin_src haskell + Variable -> Exp -> Exp -> Exp +#+end_src +Test your implementation. Here are some test cases that must work: +| Variable | Substituted term | Term | Result | +|----------+------------------+---------------------------------------------+---------------------------------------------| +| ~x~ | ~Z()~ | ~rec x = x~ | ~rec x = x~ | +| ~y~ | $\lambda x.x$ | $\lambda x. (x y)$ | $\lambda x . (x (\lambda x . x))$ | +| ~z~ | $C(\lambda z . z)$ | $\text{case}\ z\ \text{of}\ \{ C(z) \rightarrow z \}$ | $\text{case}\ C(\lambda z. z) \ \text{of}\ \{ C(z) \rightarrow z \}$ | + +*** Answer + +** (1p) +Implement multiplication of natural numbers in $\chi$, using the representation of natural numbers given in the $\chi$ specification. + +Hint: If you want to make use of addition in the implementation of multiplication, then you can define multiplication using a free variable ~add~, and use the substitution operation from the previous exercise to substitute a complete (closed) implementation of addition for this variable. + +*** Answer + +** (2p) [BN] +Implement an interpreter for $\chi$. The interpreter should be a partial function from closed terms to values, and should implement the operational semantics of $\chi$. + +If you use the BNFC specification above and Haskell, then the interpreter should have the following type: +#+begin_src haskell + Exp -> Exp +#+end_src + +Test your implementation, for instance by testing that addition (defined in the [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.hs][wrapper module]]) works for some inputs. If addition doesn’t work when your code is tested, then your solution will not be accepted. Also make sure that the following examples are implemented correctly: + +- The following programs should fail to terminate: + + $C() C()$ + + $case \lambda x.x of {}$ + + $case C() of { C(x) \rightarrow C() }$ + + $case C(C()) of { C() \rightarrow C() }$ + + $case C(C()) of { C() \rightarrow C(); C(x) \rightarrow x }$ + + $case C() of { D() \rightarrow D() }$ + + $(\lambda x.\lambda y.x) (rec x = x)$ +- The following programs should terminate with specific results: + + The program $case C(D(),E()) of { C(x, x) \rightarrow x }$ should terminate with the value $E()$. + + The program $case C(\lambda x.x, Zero()) of { C(f, x) \rightarrow f x }$ should terminate with the value $Zero()$. + + The program $case (\lambda x.x) C() of { C() \rightarrow C() }$ should terminate with the value $C()$. + + The program $((\lambda x.x)(\lambda x.x))(\lambda x.x)$ should terminate with the value $\lambda x.x$. + +Note that implementing a call-by-value semantics properly in a language like Haskell, which is by default non-strict, can be tricky. However, you will not fail if the only problem with your implementation is that some programs that should fail to terminate instead terminate with a “reasonable” result. + +*** Answer diff --git a/3/cabal.project b/3/cabal.project new file mode 100644 index 0000000..54aa83d --- /dev/null +++ b/3/cabal.project @@ -0,0 +1,2 @@ +packages: + chi.cabal diff --git a/3/chi.cabal b/3/chi.cabal new file mode 100644 index 0000000..cfd37a4 --- /dev/null +++ b/3/chi.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.0 +name: chi +version: 0.1.0 +build-type: Simple + +library + default-language: + Haskell2010 + build-depends: + array ^>= 0.5.4.0, + base >= 4.15 && < 4.22, + hashable >= 1.4.7.0 && < 1.6, + mtl >= 2.2.2 && < 2.4, + pretty ^>= 1.1.3.6, + QuickCheck ^>= 2.15.0.0, + transformers >= 0.5.6.2 && < 0.7, + unordered-containers ^>= 0.2.20 + build-tool-depends: + alex:alex ^>= 3.5.2.0, + happy:happy ^>= 2.1.5 + exposed-modules: + AbsChi + Chi + LexChi + ParChi + PrintChi + hs-source-dirs: + . diff --git a/3/flake.lock b/3/flake.lock new file mode 100644 index 0000000..e27180f --- /dev/null +++ b/3/flake.lock @@ -0,0 +1,61 @@ +{ + "nodes": { + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1763283776, + "narHash": "sha256-Y7TDFPK4GlqrKrivOcsHG8xSGqQx3A6c+i7novT85Uk=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "50a96edd8d0db6cc8db57dab6bb6d6ee1f3dc49a", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/3/flake.nix b/3/flake.nix new file mode 100644 index 0000000..b3da1db --- /dev/null +++ b/3/flake.nix @@ -0,0 +1,89 @@ +{ + description = "χ ^^"; + + inputs = { + nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; + flake-utils.url = "github:numtide/flake-utils"; + }; + + nixConfig.allow-import-from-derivation = true; # cabal2nix uses IFD + + outputs = { self, nixpkgs, flake-utils }: + let + ghcVer = "ghc910"; + makeHaskellOverlay = overlay: final: prev: { + haskell = prev.haskell // { + packages = prev.haskell.packages // { + ${ghcVer} = prev.haskell.packages."${ghcVer}".override (oldArgs: { + overrides = + prev.lib.composeExtensions (oldArgs.overrides or (_: _: { })) + (overlay prev); + }); + }; + }; + }; + + out = system: + let + pkgs = import nixpkgs { + inherit system; + overlays = [ self.overlays.default ]; + config.allowBroken = true; + }; + + in + { + packages = rec { + default = chi; + chi = pkgs.haskell.packages.${ghcVer}.chi; + }; + + checks = { + inherit (self.packages.${system}) chi; + }; + + # for debugging + # inherit pkgs; + + devShells.default = + let haskellPackages = pkgs.haskell.packages.${ghcVer}; + in + haskellPackages.shellFor { + packages = p: [ self.packages.${system}.chi ]; + withHoogle = true; + buildInputs = + (with pkgs; [ + gnumake + jasmin + jre_minimal + ]) ++ + (with haskellPackages; [ + haskell-language-server + cabal-install + alex + happy + BNFC + ]); + # Change the prompt to show that you are in a devShell + # shellHook = "export PS1='\\e[1;34mdev > \\e[0m'"; + }; + }; + in + flake-utils.lib.eachDefaultSystem out // { + # this stuff is *not* per-system + overlays = { + default = makeHaskellOverlay (prev: hfinal: hprev: + let hlib = prev.haskell.lib; in + { + chi = hprev.callCabal2nix "chi" ./. { }; + + # here's how to do hacks to the package set + # don't run the test suite + # fast-tags = hlib.dontCheck hprev.fast-tags; + # + # don't check version bounds + # friendly = hlib.doJailbreak hprev.friendly; + }); + }; + }; +} diff --git a/two.agda b/two.agda new file mode 100644 index 0000000..a1149c9 --- /dev/null +++ b/two.agda @@ -0,0 +1,124 @@ +data _≡_ {A : Set} : A → A → Set where + refl : {a : A} → a ≡ a + +context : {A B : Set} → {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b +context f refl = refl + +trans : {A : Set} → {a b c : A} → a ≡ b → b ≡ c → a ≡ c +trans refl refl = refl + +data ⊥ : Set where + +¬ : Set → Set +¬ A = A → ⊥ + +_≢_ : {A : Set} → A -> A -> Set +_≢_ a b = ¬ (a ≡ b) + +data _∧_ (A B : Set) : Set where + _∧ᵢ_ : A → B → A ∧ B + +infixr 19 _∧_ +infixr 19 _∧ᵢ_ + +data ℕ : Set where + zero : ℕ + succ : ℕ → ℕ +{-# BUILTIN NATURAL ℕ #-} + +_+_ : ℕ → ℕ → ℕ +n + 0 = n +n + succ m = succ (n + m) + +data _<_ : ℕ → ℕ → Set where + z 0 ≤ n + s≤s : ∀ (n m : ℕ) -> n ≤ m -> succ n ≤ succ m + +-- Task 2 +data ℤ : Set where + pos : ℕ → ℤ + negsucc : ℕ → ℤ -- -n - 1 alternatively - (n + 1) + +recN : {A : Set} → ℕ → A → (ℕ → A → A) → A +recN 0 d e = d +recN (succ x) d e = e x (recN x d e) + +addℕ : ℕ → ℕ → ℕ +addℕ n m = recN m n (λ _ x → succ x) + +prfadd : (n m : ℕ) → (n + m) ≡ (addℕ n m) +prfadd n 0 = refl +prfadd n (succ m) = context succ (prfadd n m) + +-- Task 3 +zrec : {A : Set} → ℤ → (ℕ → A) → (ℕ → A) → A +zrec (pos n) f _ = f n +zrec (negsucc n) _ g = g n + +addOne : ℤ → ℤ +addOne a = zrec a (λ x → pos (succ x)) (λ x → recN x (pos x) (λ n _ → negsucc n)) + +subOne : ℤ → ℤ +subOne a = zrec a (λ x → recN x (negsucc x) (λ n _ → pos n)) (λ x → negsucc (succ x)) + +prfℤ₁ : (z : ℤ) → subOne (addOne z) ≡ z +prfℤ₁ (pos x) = refl +prfℤ₁ (negsucc 0) = refl +prfℤ₁ (negsucc (succ x)) = refl + +prfℤ₂ : (z : ℤ) → addOne (subOne z) ≡ z +prfℤ₂ (pos 0) = refl +prfℤ₂ (pos (succ x)) = refl +prfℤ₂ (negsucc x) = refl + +-- Task 4 + +data Vec (A : Set) : ℕ → Set where + nil : Vec A 0 + _,_ : {n : ℕ} → Vec A n → (a : A) → Vec A (succ n) + +infixl 20 _,_ + +index : {A : Set} {n : ℕ} → Vec A n → (i : ℕ) → (0 ≤ i ∧ i < n) → A +index (xs , a) 0 (z≤n n ∧ᵢ z