view cbc/variable-tuple.agda @ 24:0fcb7b35ba81

Add data version CodeSegment
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2016 01:57:13 +0000
parents 84e3fbc662db
children da78bb99d654
line wrap: on
line source

module variable-tuple where

open import Data.Nat hiding (_<_ ; _>_)
open import Data.String
open import Data.List
open import Data.Unit
open import Data.Product
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
open import Level hiding (zero)

data Format : Set₁ where
  FEnd : Format
  FSet : Set -> Format -> Format

<> : Format
<> = FEnd

infix  51 _>
_> : (Format -> Format) -> Format
_> f = f FEnd

infixl 52 _||_
_||_ : (Format -> Format) -> Set -> (Format -> Format)
_||_ f1 s = f1 ∘ (FSet s)

infix 53 <_
<_ : Set -> Format -> Format
<_ s = FSet s


unit : Format
unit = <>

single : Format
single = < ℕ  >

double : Format
double = < String || ℕ  >

triple : Format
triple = < String || ℕ  || (List ℕ) >

data CodeSegment (A B : Set₁) : Set₁ where
--  cs : A -> B -> (A -> B) -> CodeSegment A B
  cs : A -> B  -> CodeSegment A B

id : {l : Level} {A : Set l} -> A -> A
id a = a

CommonCodeSegment : Set₁
CommonCodeSegment = CodeSegment Format Format

csDouble : CommonCodeSegment
csDouble = cs double double


ods : CommonCodeSegment -> Set
ods (cs i FEnd)       = ⊤
ods (cs i (FSet s o)) = s × (ods (cs i o))


ods-double : ods csDouble
ods-double = "hoge" , zero , tt


ids : {A : Set} -> CommonCodeSegment -> Set
ids {A} (cs FEnd o)       = A
ids {A} (cs (FSet s i) o) = s -> (ids {A} (cs i o))


ids-double : {A : Set} {a : A} -> ids {A} csDouble
ids-double {_} {a}  =  \(s : String) -> \(n : ℕ) -> a



executeCS : (cs : CommonCodeSegment) -> Set
executeCS c = ids {ods c} c


infixr 30  _◎_
_◎_ : {A B C : Set₁} -> CodeSegment A B -> CodeSegment B C -> CodeSegment A C
(cs i _) ◎ (cs _ o) = cs i o


◎-double : CommonCodeSegment 
◎-double = csDouble ◎ (cs (< String || ℕ >) <>) ◎ (cs <> triple)
-- ◎-double = csDouble ◎ (cs (< String || ℕ >) <>) ◎ (cs double triple) -- ...