importing from CPL 0.0.6

COPYING

@@ -0,0 +1,27 @@
+Copyright 2004-2008 Masahiro Sakai. All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+   1. Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+   2. Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+   3. The name of the author may not be used to endorse or promote
+      products derived from this software without specific prior
+      written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,
+INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING
+IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.

CPL.cabal

@@ -0,0 +1,48 @@
+Name:		CPL
+Version:	0.0.6
+License:	BSD3
+License-File:	COPYING
+Author:		Masahiro Sakai ([email protected])
+Maintainer:	[email protected]
+Category:	Compilers/Interpreters
+Cabal-Version:	>= 1.2
+Synopsis:	An interpreter of Hagino's Categorical Programming Language (CPL).
+Description:	An interpreter of Hagino's Categorical Programming Language (CPL).
+Extra-Source-Files:
+   README,
+   NEWS,
+   samples/ack.cpl,
+   samples/automata.cdt,
+   samples/ccc.cdt,
+   samples/examples.cpl,
+   samples/examples.txt,
+   samples/misc.cdt,
+   samples/obscure.cdt,
+   samples/rec.cdt,
+   samples/benchmark.cpl,
+   samples/ack_3_4.cpl,
+   samples/function.cpl,
+   src/CDT.hs-boot
+Build-Type: Simple
+
+Flag Readline
+  Description: Use Readline
+  Default: False
+
+Flag Haskeline
+  Description: Use Haskeline
+  Default: False
+
+Executable cpl
+  Main-is: Main.hs
+  HS-Source-Dirs: src
+  Other-Modules: AExp CDT CDTParser CPLSystem Exp ExpParser FE Funct ParserUtils Simp Statement Subst Type Typing Variance 
+  Build-Depends: base >=4 && <5, mtl, containers, array, parsec
+  Extensions: CPP, GeneralizedNewtypeDeriving
+  if flag(Readline)
+    CPP-Options: "-DUSE_READLINE_PACKAGE"
+    Build-Depends: readline
+  else
+    if flag(Haskeline)
+      CPP-Options: "-DUSE_HASKELINE_PACKAGE"
+      Build-Depends: haskeline

NEWS

@@ -0,0 +1,22 @@
+
+= Changes since the 0.0.5 release
+
+Readline/Haskeline support.
+
+= Changes since the 0.0.3 release
+
+Function defintions are added.
+
+Examples:
+
+  > let uncurry(f) = eval . prod(f, I)
+  uncurry(f) = eval.prod(f,I)
+  f: *a -> exp(*b,*c)
+  -----------------------------
+  uncurry(f): prod(*a,*b) -> *c
+
+  > let primrec(f,g) = pi2.pr(pair(0,f), pair(s.pi1, g))
+  primrec(f,g) = pi2.pr(pair(0,f),pair(s.pi1,g))
+  f: 1 -> *a  g: prod(nat,*a) -> *a
+  ---------------------------------
+  primrec(f,g): nat -> *a

README

@@ -0,0 +1,63 @@
+An implementation of "A Categorical Programing Language".
+version 0.0.5
+====================
+
+  This package is an implementation of "A Categorical Programing Language"
+  (CPL for short)[1][2] written in Haskell.
+
+  CPL is a functional programming language based on category
+  theory[3]. Data types are declared in a categorical manner by
+  adjunctions. Data types that can be handled include the terminal
+  object, the initial object, the binary product functor, the binary
+  coproduct functor, the exponential functor, the natural number object,
+  the functor for finite lists, and the functor for infinite lists.
+  Each data type is declared with its basic operations or
+  morphisms. Programs consist of these morphisms, and execution of
+  programs is the reduction of elements (i.e. special morphisms) to
+  their canonical form.
+
+Requirements
+------------
+
+  * GHC-6.10
+
+Install
+-------
+
+  De-Compress archive and enter its top directory.
+  Then type:
+
+    $ runhaskell Setup.hs configure
+    $ runhaskell Setup.hs build
+    $ runhaskell Setup.hs install
+
+  If you want to compile with readline or haskeline, add -fReadline or
+  -fHaskeline respectively to configure command.
+
+Usage
+-----
+
+  See chapter 5 of [1]
+
+License
+-------
+  This program is licenced under the BSD-style license.
+  (See the file 'COPYING'.)
+
+  Copyright (C) 2004-2009 Masahiro Sakai <[email protected]>
+
+Author
+----------
+  Masahiro Sakai <[email protected]>
+
+Bibliography
+------------
+
+[1]  Tatsuya Hagino, ``A Categorical Programming Languge''.
+     Ph.D. Thesis, University of Edinburgh, 1987
+     available at <http://www.tom.sfc.keio.ac.jp/~hagino/index.html.en>
+
+[2]  Tatsuya Hagino, ``Categorical Functional Programming Language''
+     Computer Software, Vol 7, No.1.
+     Advances in Software Science and Technology 4, 1992
+     ISBN 0-12-037104-9

Setup.hs

@@ -0,0 +1,3 @@
+#!/usr/bin/env runghc
+import Distribution.Simple
+main = defaultMain

samples/ack.cpl

@@ -0,0 +1,55 @@
+
+right object 1 with ! is
+end object;
+
+right object prod(a,b) with pair is
+  pi1: prod -> a
+  pi2: prod -> b
+end object;
+
+right object exp(a,b) with curry is
+  eval: prod(exp,a) -> b
+end object;
+
+left object nat with pr is
+  0: 1 -> nat
+  s: nat -> nat
+end object;
+
+let times=eval.prod(pr(curry(curry(pi2)), curry(curry(eval.pair(eval.pi1,eval.pair(pi2.pi1,pi2))))),I);
+let ack_0=curry(s.pi2);
+let ack_s=curry(eval.pair(times.pair(s.pi2,pi1),s.0.!));
+let ack=eval.prod(pr(ack_0,ack_s),I);
+
+#show aexp eval.prod(pr(curry(curry(pi2)), curry(curry(eval.pair(eval.pi1,eval.pair(pi2.pi1,pi2))))),I);
+#show aexp curry(s.pi2);
+#show aexp curry(eval.pair(times.pair(s.pi2,pi1),s.0.!));
+#show aexp eval.prod(pr(ack_0,ack_s),I);
+
+simp full ack.pair(s.s.s.0,s.s.s.0);
+
+# time ~/cpl/cpl/bin/cpl.rb ack.cpl
+# cpl.rb (An implementation of Categorical Programming Language)
+# version 0.0.4
+# Type help for help
+# right object 1 defined
+# right object prod(+,+) defined
+# right object exp(-,+) defined
+# left object nat defined
+# times : prod(nat,exp(*a,*a)) -> exp(*a,*a)  defined
+# ack_0 : *a -> exp(nat,nat)  defined
+# ack_s : exp(nat,nat) -> exp(nat,nat)  defined
+# ack : prod(nat,nat) -> nat  defined
+# s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.0.!
+#     : *a -> nat
+# 
+# real	21m17.567s
+# user	20m43.233s
+# sys	0m0.296s
+
+
+# Haskell��
+# real	0m9.230s
+# user	0m0.031s
+# sys	0m0.000s
+

samples/ack_3_4.cpl

@@ -0,0 +1,23 @@
+right object 1 with ! is
+end object;
+
+right object prod(a,b) with pair is
+  pi1: prod -> a
+  pi2: prod -> b
+end object;
+
+right object exp(a,b) with curry is
+  eval: prod(exp,a) -> b
+end object;
+
+left object nat with pr is
+  0: 1 -> nat
+  s: nat -> nat
+end object;
+
+let times=eval.prod(pr(curry(curry(pi2)), curry(curry(eval.pair(eval.pi1,eval.pair(pi2.pi1,pi2))))),I);
+let ack_0=curry(s.pi2);
+let ack_s=curry(eval.pair(times.pair(s.pi2,pi1),s.0.!));
+let ack=eval.prod(pr(ack_0,ack_s),I);
+
+simp full ack.pair(s.s.s.0, s.s.s.s.0);

samples/automata.cdt

@@ -0,0 +1,12 @@
+# categorical data type of automata
+
+# Moore automata
+right object dyn'(I,O) with univ' is
+  next': prod(dyn',I) -> dyn'
+  output': dyn' -> O
+end object;
+
+# Mealy automata
+right object dyn''(I,O) with univ'' is
+  next'': prod(dyn'',I) -> prod(dyn'',O)
+end object;

samples/benchmark.cpl

@@ -0,0 +1,36 @@
+right object 1 with ! is
+end object;
+
+right object prod(a,b) with pair is
+  pi1: prod -> a
+  pi2: prod -> b
+end object;
+
+right object exp(a,b) with curry is
+  eval: prod(exp,a) -> b
+end object;
+
+left object nat with pr is
+  0: 1 -> nat
+  s: nat -> nat
+end object;
+
+let times=eval.prod(pr(curry(curry(pi2)), curry(curry(eval.pair(eval.pi1,eval.pair(pi2.pi1,pi2))))),I);
+let ack_0=curry(s.pi2);
+let ack_s=curry(eval.pair(times.pair(s.pi2,pi1),s.0.!));
+let ack=eval.prod(pr(ack_0,ack_s),I);
+
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+
+# src/cpl.exe samples/test.cpl  0.00s user 0.03s system 0% cpu 5.864 total
+
+# src/cpl.exe samples/test.cpl  0.00s user 0.00s system 0% cpu 5.348 total

samples/ccc.cdt

@@ -0,0 +1,17 @@
+# Cartesian Closed Category
+
+# terminal object
+right object 1 with !
+end object;
+
+# product functor 
+right object prod(X,Y) with pair is
+  pi1: prod -> X
+  pi2: prod -> Y
+end object;
+
+# exponential functor
+right object exp(X,Y) with curry is
+  eval: prod(exp,X) -> Y
+end object;
+

samples/examples.cpl

@@ -0,0 +1,81 @@
+right object 1 with !
+end object;
+
+right object prod(a,b) with pair is
+  pi1: prod -> a
+  pi2: prod -> b
+end object;
+
+right object exp(a,b) with curry is
+  eval: prod(exp,a) -> b
+end object;
+
+left object nat with pr is
+  0: 1 -> nat
+  s: nat -> nat
+end object;
+
+left object coprod(a,b) with case is
+  in1: a -> coprod
+  in2: b -> coprod
+end object;
+
+show pair(pi2,eval);
+
+let add=eval.prod(pr(curry(pi2), curry(s.eval)), I);
+
+simp add.pair(s.s.0, s.0);
+
+let mult=eval.prod(pr(curry(0.!), curry(add.pair(eval, pi2))), I);
+
+let fact=pi1.pr(pair(s.0,0), pair(mult.pair(s.pi2,pi1), s.pi2));
+
+simp fact.s.s.s.s.0;
+
+left object list(p) with prl is
+  nil: 1 -> list
+  cons: prod(p,list) -> list
+end object;
+
+let append = eval.prod(prl(curry(pi2), curry(cons.pair(pi1.pi1, eval.pair(pi2.pi1, pi2)))), I);
+
+let reverse=prl(nil, append.pair(pi2, cons.pair(pi1, nil.!)));
+
+let hd = prl(in2, in1.pi1);
+
+let hdp=case(hd,in2);
+
+let tl = coprod(pi2,I).prl(in2, in1.prod(I, case(cons,nil)));
+
+let tlp = case(tl, in2);
+
+let seq = pi2.pr(pair(0,nil), pair(s.pi1, cons));
+
+simp seq.s.s.s.0;
+
+simp full seq.s.s.s.0;
+
+simp hdp.tl.seq.s.s.s.0;
+
+simp full append.pair(seq.s.s.0, seq.s.s.s.0);
+
+simp full reverse.it;
+
+right object inflist(a) with fold is
+  head: inflist -> a
+  tail: inflist -> inflist
+end object;
+
+let incseq=fold(I,s).0;
+
+simp head.incseq;
+
+simp head.tail.tail.tail.incseq;
+
+let alt=fold(head.pi1, pair(pi2, tail.pi1));
+
+let infseq=fold(I,I).0;
+
+simp head.tail.tail.alt.pair(incseq, infseq);
+
+#exit;