khibino

{-# LANGUAGE DataKinds, KindSignatures, MultiParamTypeClasses,
             FunctionalDependencies, FlexibleInstances, FlexibleContexts,
             OverloadedLabels, ScopedTypeVariables #-}

import GHC.OverloadedLabels (IsLabel(..))
import GHC.TypeLits (Symbol)

data Label (l :: Symbol) = Put

class Belongs a l b | l b -> a where

khibino

-- printf like function, formatting package method

newtype Format r a = Format ((ShowS -> r) -> a)

string :: Format r (String -> r)
string = Format $ \k s -> k (s ++)

int :: Format r (Int -> r)
int = Format $ \k i -> k (show i ++)

khibino

open import Function.Base using (_∘_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)

----------
-- List の定義

infixr 50 _∷_

data List (A : Set) : Set where
  [] : List A

khibino

open import Agda.Primitive using (lsuc)
open import Data.Bool using (Bool)

Fix : ∀{l} -> (Set l → Set l) → Set (lsuc l)
Fix f = ∀ k → (f k → k) → k

T : ∀{l} → Set l → Set l
T a = (a → Bool) → Bool

X : Set1

khibino

Theorem plus_0_r : forall n:nat, n + 0 = n.
Proof.
  intros n. induction n as [| n'].
  (* Case "n = 0". *)    +  reflexivity.
  (* Case "n = S n'". *) +  simpl. rewrite -> IHn'. reflexivity.  Qed.

(** 練習問題: ★★★★, recommended (binary) *)

(* (a) *)
Inductive bin : Type :=

khibino

Theorem plus_0_r : forall n:nat, n + 0 = n.
Proof.
  intros n. induction n as [| n'].
  (* Case "n = 0". *)    +  reflexivity.
  (* Case "n = S n'". *) +  simpl. rewrite -> IHn'. reflexivity.  Qed.

(** **** 練習問題: ★★★★, recommended (binary) *)
(** これまでとは異なる、通常表記の自然数ではなく2進のシステムで、自然数のより効率的な表現を考えなさい。それは自然数をゼロとゼロに1を加える加算器からなるものを定義する代わりに、以下のような2進の形で表すものです。2進数とは、
      - ゼロであるか,
      - 2進数を2倍したものか,

khibino

{--# OPTIONS_GHC -Wno-name-shadowing #-}

import Control.Concurrent (forkIO)
import Control.Concurrent (threadDelay)
import Control.Concurrent.Chan (Chan, newChan, readChan, writeChan)
import Control.Monad (void, replicateM, replicateM_)
import System.IO (BufferMode (LineBuffering), hSetBuffering, stdout)

-----

khibino

module Language where
import Utils

import Prelude hiding (seq)

data Expr a
   = EVar Name               -- ^ Variables
   | ENum Int                -- ^ Numbers
   | EConstr Int Int         -- ^ Constructor tag arity
   | EAp (Expr a) (Expr a)   -- ^ Applications

khibino

-- Example implementation for Meta-Theory à la Carte

-- data Fix (f : Set -> Set) : Set where
--   inF : f (Fix f) -> Fix f

open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; _+_)
import Data.Nat as Nat

khibino

f1029 = [7, 123229502148636]

f1030 = [2, 7]

f1031 = [4, 21855]

f1032 = [7, 560803991675135]

f1034 = [5, 33554431]