CPL (empty) → 0.0.5
raw patch · 33 files changed
+2842/−0 lines, 33 filesdep +arraydep +basedep +containerssetup-changed
Dependencies added: array, base, containers, mtl, parsec
Files
- COPYING +27/−0
- CPL.cabal +32/−0
- NEWS +17/−0
- README +60/−0
- Setup.hs +3/−0
- samples/ack.cpl +55/−0
- samples/ack_3_4.cpl +23/−0
- samples/automata.cdt +12/−0
- samples/benchmark.cpl +36/−0
- samples/ccc.cdt +17/−0
- samples/examples.cpl +81/−0
- samples/examples.txt +102/−0
- samples/function.cpl +84/−0
- samples/misc.cdt +28/−0
- samples/obscure.cdt +12/−0
- samples/rec.cdt +19/−0
- src/AExp.hs +157/−0
- src/CDT.hs +274/−0
- src/CDT.hs-boot +9/−0
- src/CDTParser.hs +102/−0
- src/CPLSystem.hs +162/−0
- src/Exp.hs +64/−0
- src/ExpParser.hs +90/−0
- src/FE.hs +81/−0
- src/Funct.hs +8/−0
- src/Main.hs +418/−0
- src/ParserUtils.hs +26/−0
- src/Simp.hs +352/−0
- src/Statement.hs +97/−0
- src/Subst.hs +99/−0
- src/Type.hs +44/−0
- src/Typing.hs +176/−0
- src/Variance.hs +75/−0
+ COPYING view
@@ -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 view
@@ -0,0 +1,32 @@+Name: CPL+Version: 0.0.5+License: BSD3+License-File: COPYING+Author: Masahiro Sakai (masahiro.sakai@gmail.com)+Maintainer: masahiro.sakai@gmail.com+Category: Compilers/Interpreters+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++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
+ NEWS view
@@ -0,0 +1,17 @@+= 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 view
@@ -0,0 +1,60 @@+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++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 <masahiro.sakai@gmail.com>++Author+----------+ Masahiro Sakai <masahiro.sakai@gmail.com>++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 view
@@ -0,0 +1,3 @@+#!/usr/bin/env runghc+import Distribution.Simple+main = defaultMain
+ samples/ack.cpl view
@@ -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 view
@@ -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 view
@@ -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 view
@@ -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 view
@@ -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 view
@@ -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;
+ samples/examples.txt view
@@ -0,0 +1,102 @@+% cpl.rb +cpl.rb (An Implementation of Categorical Programming Language)+version 0.0.1+cpl> edit+| right object 1 with !+| end object;+right object 1 defined+cpl> edit+| right object prod(a,b) with pair is+| pi1: prod -> a+| pi2: prod -> b+| end object;+right object prod(+,+) defined+cpl> edit+| right object exp(a,b) with curry is+| eval: prod(exp,a) -> b+| end object;+right object exp(-,+) defined+cpl> edit+| left object nat with pr is+| 0: 1 -> nat+| s: nat -> nat+| end object;+left object nat defined+cpl> edit+| left object coprod(a,b) with case is+| in1: a -> coprod+| in2: b -> coprod+| end object;+left object coprod(+,+) defined+cpl> show pair(pi2,eval)+pair(pi2,eval)+ : prod(exp(*a,*b),*a) -> prod(*a,*b)+cpl> let add=eval.prod(pr(curry(pi2), curry(s.eval)), I)+add : prod(nat,nat) -> nat defined+cpl> simp add.pair(s.s.0, s.0)+s.s.s.0+ : 1 -> nat+cpl> let mult=eval.prod(pr(curry(0.!), curry(add.pair(eval, pi2))), I)+mult : prod(nat,nat) -> nat+cpl> let fact=pi1.pr(pair(s.0,0), pair(mult.pair(s.pi2,pi1), s.pi2))+fact : nat -> nat defined+cpl> simp fact.s.s.s.s.0+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+ : 1 -> nat+cpl> edit+| left object list(p) with prl is+| nil: 1 -> list+| cons: prod(p,list) -> list+| end object;+left object list(+) defined+cpl> let append = eval.prod(prl(curry(pi2), curry(cons.pair(pi1.pi1, eval.pair(pi2.pi1, pi2)))), I)+append : prod(list(*a),list(*a)) -> list(*a) defined+cpl> let reverse=prl(nil, append.pair(pi2, cons.pair(pi1, nil.!)))+reverse : list(*a) -> list(*a) defined+cpl> let hd = prl(in2, in1.pi1)+hd : list(*a) -> coprod(*a,1) defined+cpl> let hdp=case(hd,in2)+hdp : coprod(list(*a),1) -> coprod(*a,1) defined+cpl> let tl = coprod(pi2,I).prl(in2, in1.prod(I, case(cons,nil)))+tl : list(*a) -> coprod(list(*a),1) defined+cpl> let tlp = case(tl, in2)+tlp : coprod(list(*a),1) -> coprod(list(*a),1) defined+cpl> let seq = pi2.pr(pair(0,nil), pair(s.pi1, cons))+seq : nat -> list(nat) defined+cpl> simp seq.s.s.s.0+cons.pair(s.pi1,cons).pair(s.pi1,cons).pair(0,nil)+ : 1 -> list(nat)+cpl> simp full seq.s.s.s.0+cons.pair(s.s.0,cons.pair(s.0,cons.pair(0,nil)))+ : 1 -> list(nat)+cpl> simp hdp.tl.seq.s.s.s.0+in1.s.0+ : 1 -> coprod(nat,*a)+cpl> simp full append.pair(seq.s.s.0, seq.s.s.s.0)+cons.pair(s.0,cons.pair(0,cons.pair(s.s.0,cons.pair(s.0,cons.pair(0,nil)))))+ : 1 -> list(nat)+cpl> simp full reverse.it+cons.pair(0,cons.pair(s.0,cons.pair(s.s.0,cons.pair(0,cons.pair(s.0,nil.!)))))+ : 1 -> list(nat)+cpl> edit+| right object inflist(a) with fold is+| head: inflist -> a+| tail: inflist -> inflist+| end object;+right object inflist(+) defined+cpl> let incseq=fold(I,s).0+incseq : 1 -> inflist(nat) defined+cpl> simp head.incseq+0+ : 1 -> nat+cpl> simp head.tail.tail.tail.incseq+s.s.s.0+ : 1 -> nat+cpl> let alt=fold(head.pi1, pair(pi2, tail.pi1))+alt : prod(inflist(*a),inflist(*a)) -> inflist(*a) defined+cpl> let infseq=fold(I,I).0+infseq : 1 -> inflist(nat) defined+cpl> simp head.tail.tail.alt.pair(incseq, infseq)+s.0+ : 1 -> nat+cpl> exit
+ samples/function.cpl view
@@ -0,0 +1,84 @@+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;++let uncurry(f) = eval . prod(f, I);++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 primrec(f,g) = pi2.pr(pair(0,f), pair(s.pi1, g));+let fact = primrec(s.0, mult.prod(s,I));++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;
+ samples/misc.cdt view
@@ -0,0 +1,28 @@+# initial object+left object 0 with !! is+end object;++# coproduct functor+left object coprod(X,Y) with case is+ in1: X -> coprod+ in2: Y -> coprod+end object;++# co-"natural number object"+right object conat with copr is+ pred: conat -> coprod(1,conat)+end object;++right object colist(X) with coprl is+ delist: colist -> coprod(1,prod(X,colist))+end object;++# let list2colist = coprl(prl(in1, in2.prod(I, case(nil, cons))));+# let inflist2colist = coprl(in2.pair(head,tail));+# let colist-length = copr(coprod(I, pi2).delist);++# ordinals+left object ord with pro is+ ozero: 1 -> ord+ sup: exp(nat, ord) -> ord+end object;
+ samples/obscure.cdt view
@@ -0,0 +1,12 @@+# Examples of obscure categorical data type+# which are not computable in the sense of CPL.++# the left adjoint functor of the list functor+left object ladjlist(X) with psi is+ a: X -> list(ladjlist)+end object;++# the right adjoint functor of the list functor+right object radjlist(X) with psi' is+ a': list(radjlist) -> X+end object;
+ samples/rec.cdt view
@@ -0,0 +1,19 @@+# Some of the recursively defined object++# natural number object+left object nat with pr is+ 0: 1 -> nat+ s: nat -> nat+end object;++# list+left object list(X) with prl is+ nil: 1 -> list+ cons: prod(X,list) -> list+end object;++# infinite list (a.k.a stream)+right object inflist(X) with fold is+ head: inflist -> X+ tail: inflist -> inflist+end object;
+ src/AExp.hs view
@@ -0,0 +1,157 @@+-----------------------------------------------------------------------------+-- |+-- Module : AExp+-- Copyright : (c) Masahiro Sakai 2004,2009+-- License : BSD-style+-- +-- Maintainer : masahiro.sakai@gmail.com+-- Stability : provisional+-- Portability : portable+--+-- Annotated Expression.+--+-----------------------------------------------------------------------------++module AExp+ ( AExp(..)+ , aexpType+ , isElement++ , TypeScheme+ , AExpScheme+ , quantify++ , skelton+ ) where++import Variance+import Funct+import qualified FE+import qualified CDT+import Type (GenType(..), Type)+import Subst+import qualified Exp as E+import Exp (Id)++import Data.List (nub, intercalate)++----------------------------------------------------------------------------++-- Annotated expression with type information+data AExp+ = Identity FE.FE+ | Comp AExp AExp+ | Nat !CDT.Nat [FE.FE]+ | Fact !CDT.CDT [AExp] [FE.FE]+ | Funct !CDT.CDT [AExp]+ | Var !Id [FE.FE] [AExp] Type++instance FEs AExp where+ apply s (Identity annotation) = Identity (apply s annotation)+ apply s (Comp a b) = Comp (apply s a) (apply s b)+ apply s (Nat sym annotation) = Nat sym (apply s annotation)+ apply s (Fact obj args annotations) =+ Fact obj (apply s args) (apply s annotations)+ apply s (Funct obj args) =+ Funct obj (apply s args)+ apply s (Var v annotations args typ) =+ Var v (apply s annotations) (apply s args) (apply s typ)+ tv (Identity x) = tv x+ tv (Comp a b) = nub (tv a ++ tv b)+ tv (Nat _ annotations) = tv annotations+ tv (Fact _ args _) = tv args+ tv (Funct _ args) = tv args+ tv (Var _ annotations args _) = nub (tv annotations ++ tv args)++instance Show AExp where+ show (Identity fe) = "I" ++ showAnnotations [fe]+ show (Comp a b) = show a ++ "." ++ show b+ show (Nat sym annotations) =+ CDT.natName sym ++ showAnnotations annotations+ show (Fact obj args annotations) =+ CDT.factName obj ++ showAnnotations annotations ++ showAExpArgs args+ show (Funct obj args) =+ CDT.factName obj ++ showAExpArgs args+ show (Var v annotations args _) = v ++ showAnnotations annotations ++ showAExpArgs args++showAnnotations :: [FE.FE] -> String+showAnnotations [] = ""+showAnnotations xs = "[" ++ intercalate "," (map show xs) ++ "]"++showAExpArgs :: [AExp] -> String+showAExpArgs [] = ""+showAExpArgs xs = "(" ++ intercalate "," (map show xs) ++ ")"++skelton :: AExp -> E.Exp+skelton = f+ where+ f (Identity _) = E.Identity+ f (Comp a b) = f a `E.Comp` f b+ f (Nat sym _) = E.Nat sym+ f (Fact sym args _) = E.Fact sym (map f args)+ f (Funct sym args) = E.Funct sym (map f args)+ f (Var name _ args _) = E.Var name (map f args)++-- XXX+aexpType :: AExp -> Type+aexpType = f+ where + f (Identity a) = a :-> a+ f (Comp g h) = dom (f h) :-> cod (f g)+ f (Nat nat annotation) =+ apply (zip [0..] annotation) (CDT.natType nat)+ f (Fact obj _ annotation) =+ apply (zip [0..] annotation) (CDT.factDestType obj)+ f (Funct obj args) = FE.Ap obj xs :-> FE.Ap obj ys+ where+ (xs,ys) = foldr phi ([],[]) (zip (variance obj) (map aexpType args))+ phi (v, (x:->y)) (xs,ys) =+ case v of+ Contravariance -> (y:xs, x:ys)+ _ -> (x:xs, y:ys)+ f (Var _ _ args typ) = typ -- FIXME?++isElement :: AExp -> Bool+isElement x =+ case dom (AExp.aexpType x) of+ FE.Var _ -> True+ FE.Ap obj _ -> CDT.isTerminalObject obj++----------------------------------------------------------------------------++-- data Scheme t = Forall !Int t+type Scheme t = (Int, t)+type TypeScheme = Scheme Type+type AExpScheme = Scheme AExp++quantify :: FEs t => t -> Scheme t+quantify x = (length vars, apply s x)+ where+ vars = tv x+ s = zip vars [FE.Var i | i<-[0..]]++----------------------------------------------------------------------------++simp :: AExp -> AExp+simp (Comp a b) =+ case (simp a, simp b) of+ (Identity _, b') -> b'+ (a', Identity _) -> a'+ (a', b') -> Comp a' b'+simp orig@(Fact obj args _) =+ if a==b && all f (zip (CDT.nats obj) (map simp args))+ then Identity a+ else orig+ where+ (a :-> b) = aexpType orig+ f (nat, Nat sym _) = nat==sym+ f _ = False+simp orig@(Funct _ args) =+ if a==b && all f (map simp args)+ then Identity a+ else orig+ where+ (a :-> b) = aexpType orig+ f (Identity _) = True+ f _ = False+simp x = x
+ src/CDT.hs view
@@ -0,0 +1,274 @@+-----------------------------------------------------------------------------+-- |+-- Module : CDT+-- Copyright : (c) Masahiro Sakai 2004,2009+-- License : BSD-style+-- +-- Maintainer : masahiro.sakai@gmail.com+-- Stability : provisional+-- Portability : portable+--+-- Categorical Data Type+--+-----------------------------------------------------------------------------++module CDT+ ( ObjectType (..)+ , CDT+ , mkCDT+ , objectType+ , nats+ , nNats+ , isUnconditioned++ , functName+ , functVariance+ , functArity++ , Nat+ , natName+ , natNTypeParams+ , natType+ , natCDT+ , natIndex+ , natDeclType+ , natDeclDom+ , natDeclCod+ {- for optimization -}+ , natProjectionSequence+ , natIsUnconditioned++ , factName+ , factParams+ , factDestType+ , factNTypeParams++ , _eqCDT -- XXX++ , isComputable+ , isProductiveIn+ , showFunctNameWithVariance++ , isTerminalObject+ ) where++import Variance+import Funct+import FE+import Type+import Subst (tv, apply)++import Data.List (findIndices, transpose, find, findIndex, intercalate)+++data ObjectType+ = LeftObject+ | RightObject+ deriving (Show, Read, Eq)++data CDT+ = CDT+ { objectType :: !ObjectType+ , nats :: ![Nat]+ , nNats :: !Int -- = length of nats+ , isUnconditioned :: !Bool++ , functName :: !String+ , functVariance :: ![Variance]+ , functArity :: !Int -- = length of functVariance++ , factName :: !String+ , factParams :: ![Type]+ , factDestType :: Type -- $B%k!<%W$rHr$1$k$?$a$K@53J%U%i%0$rIU$1$J$$(B+ }++instance Funct CDT where+ variance CDT{ functVariance = vs } = vs++instance Eq CDT where+ a==b = objectType a == objectType b &&+ nNats a == nNats b &&+ functName a == functName b &&+ functArity a == functArity b &&+ all (\(n1,n2) -> natName n1 == natName n2 &&+ natDeclType n1 == natDeclType n2)+ (zip (nats a) (nats b))++_eqCDT :: CDT -> CDT -> Bool+_eqCDT a b = a==b++data Nat+ = Nat+ { natName :: !String+ , natType :: !Type+ , natCDT :: !CDT+ , natIndex :: !Int+ , natDeclType :: !Type++ {- for optimization -}++ -- right object $B$G$7$+0UL#$,L5$$$N$G(B!$B$rIU$1$J$$(B+ , natProjectionSequence :: [Int]++ , natIsUnconditioned :: !Bool+ {- LeftObject$B$J$i(BnatDecl$B$N(Bdom$B$K!"(B+ - RightObject$B$J$i(BnatDecl$B$N(Bcod$B$K(B+ - $B$=$N%*%V%8%'%/%H(B(Var 0)$B$,8=$o$l$F$$$J$$>l9g$K??!#(B+ -}+ }++instance Eq Nat where+ a==b = natCDT a == natCDT b && natIndex a == natIndex b++{-# INLINE natNTypeParams #-}+natNTypeParams :: Nat -> Int+natNTypeParams = functArity . natCDT++{-# INLINE natDeclDom #-}+natDeclDom :: Nat -> FE+natDeclDom = dom . natDeclType++{-# INLINE natDeclCod #-}+natDeclCod :: Nat -> FE+natDeclCod = cod . natDeclType++{-# INLINE factNTypeParams #-}+factNTypeParams :: CDT -> Int+factNTypeParams factObj = functArity factObj + 1+++mkCDT :: ObjectType -> String -> Int -> String -> [(String,Type)] -> CDT+mkCDT t functName functArity factName natDecls = object+ where+ object =+ CDT+ { objectType = t+ , nats = nats+ , nNats = length (natDecls)+ , isUnconditioned = isUnconditioned++ , functName = functName+ , functVariance = vs+ , functArity = functArity++ , factName = factName+ , factParams = map snd natDecls+ , factDestType = factDestType+ }++ vs = map joinL . transpose . map f $ natDecls+ where+ f (_,dom:->cod) =+ zipWith g (tail (variance (CFE (1+functArity) dom)))+ (tail (variance (CFE (1+functArity) cod)))+ g = case t of+ LeftObject ->+ \a b -> a `join` (Contravariance `mult` b)+ RightObject ->+ \a b -> (Contravariance `mult` a) `join` b++ factDestType =+ case t of+ LeftObject -> a :-> b+ RightObject -> b :-> a+ where a = Ap object [Var x | x <- [1..functArity]]+ b = Var 0++ nats = zipWith f natDecls [0..]+ where+ f (name, declType@(dom :-> cod)) idx = nat+ where+ nat = Nat{ natName = name+ , natType = apply s declType+ , natCDT = object+ , natIndex = idx+ , natDeclType = declType+ , natProjectionSequence =+ case t of+ LeftObject -> error "not a right object"+ RightObject -> makeProjectionSequence dom+ , natIsUnconditioned =+ case t of+ LeftObject -> not (0 `elem` tv dom)+ RightObject -> not (0 `elem` tv cod)+ }+ s = [(x, h x) | x <- [0..functArity]]+ where+ h 0 = Ap object [Var x | x <- [0..(functArity-1)]]+ h n = Var (n-1)++ isUnconditioned = all f natDecls+ where+ f (_, dom :-> cod) =+ case t of+ LeftObject -> 0 `notElem` tv dom+ RightObject -> 0 `notElem` tv cod++----------------------------------------------------------------------------++isComputable :: CDT -> Bool+isComputable obj =+ case objectType obj of+ LeftObject -> all f (nats obj)+ where+ f nat = case natDeclCod nat of+ Var 0 -> True+ _ -> False+ RightObject -> all f (nats obj)+ where+ f nat = feIsProductiveIn (natDeclDom nat) 0++isProductiveIn :: CDT -> Int -> Bool+isProductiveIn obj i =+ objectType obj == RightObject &&+ isUnconditioned obj &&+ all (\(dom :-> _) -> i+1 `notElem` tv dom) natDecls &&+ case filter (\(_ :-> cod) -> i+1 `elem` tv cod) natDecls of+ [Var 0 :-> cod] -> feIsProductiveIn cod (i+1)+ _ -> False+ where natDecls = map natDeclType (nats obj)++feIsProductiveIn :: FE -> Int -> Bool+feIsProductiveIn (Var m) n = m==n+feIsProductiveIn (Ap functObj args) n =+ case findIndices (\arg -> n `elem` tv arg) args of+ [i] -> isProductiveIn functObj i+ _ -> False++----------------------------------------------------------------------------++makeProjectionSequence :: FE -> [Int]+makeProjectionSequence fe = + case fe of+ FE.Var 0 -> []+ FE.Var _ ->+ error "BUG: not a natural transformation of a computable right object"+ FE.Ap functObj args ->+ case findIndex (\arg -> 0 `elem` tv arg) args of+ Just i -> getProjection functObj i+ _ -> error "BUG"++getProjection :: CDT -> Int -> [Int]+getProjection obj i =+ case find f (nats obj) of+ Just nat -> natIndex nat : makeProjectionSequence (natDeclDom nat)+ _ -> error "BUG"+ where+ f nat = i+1 `elem` tv (natDeclCod nat) && + case natDeclDom nat of+ FE.Var 0 -> True+ _ -> False++----------------------------------------------------------------------------++showFunctNameWithVariance :: CDT -> String+showFunctNameWithVariance funct =+ functName funct +++ case variance funct of+ [] -> ""+ vs -> "(" ++ intercalate "," (map Variance.mnemonic vs) ++ ")"++----------------------------------------------------------------------------++isTerminalObject :: CDT -> Bool+isTerminalObject obj = objectType obj == RightObject && null (nats obj)
+ src/CDT.hs-boot view
@@ -0,0 +1,9 @@+module CDT where++import Variance++data CDT++functName :: CDT -> String+functVariance :: CDT -> [Variance]+_eqCDT :: CDT -> CDT -> Bool
+ src/CDTParser.hs view
@@ -0,0 +1,102 @@+-----------------------------------------------------------------------------+-- |+-- Module : CDTParser+-- Copyright : (c) Masahiro Sakai 2006,2009+-- License : BSD-style+-- +-- Maintainer : masahiro.sakai@gmail.com+-- Stability : provisional+-- Portability : portable+--+-----------------------------------------------------------------------------++module CDTParser+ ( FE+ , Type+ , CDTDecl+ , cdtDecl+ , evalCDTDecl+ ) where++import qualified FE+import qualified Type as T+import Type (GenType(..))+import CDT+import ParserUtils++import Text.ParserCombinators.Parsec+import Control.Monad+import Data.List++type FE = FE.GenFE String+type Type = T.GenType String+data CDTDecl = CDTDecl !ObjectType String !Int String [(String, Type)]++cdtDecl :: Parser CDTDecl+cdtDecl = + do t <- mplus (string' "left" >> return LeftObject)+ (string' "right" >> return RightObject)+ string' "object"+ name <- ident+ params <- option [] $ between (char' '(') (char' ')')+ $ sepBy ident (char' ',')+ spaces+ string' "with"+ fact_name <- ident+ let endObject = string' "end" >> string' "object"+ normalDecl = do string' "is"+ manyTill (try (nat_decl (name : params)))+ (try endObject)+ emptyDecl = endObject >> return []+ nat_decls <- normalDecl <|> emptyDecl+ return $ CDTDecl t name (length params) fact_name nat_decls++nat_decl :: [String] -> Parser (String, Type)+nat_decl params = + do name <- ident+ char' ':'+ let f x = x `elemIndex` params+ a <- fe f+ string' "->"+ b <- fe f+ return (name, a :-> b)++fe :: (String -> Maybe Int) -> Parser FE+fe lookupVar = fe'+ where fe' = + do name <- ident+ params <- option [] $ between (char' '(') (char' ')')+ $ sepBy fe' (char' ',')+ spaces+ return $ case lookupVar name of+ Just n -> FE.Var n+ Nothing -> FE.Ap name params++-----------------------------------------------------------------------------++type CDTEnv = [CDT]++evalCDTDecl :: Monad m => CDTEnv -> CDTDecl -> m CDT+evalCDTDecl cenv (CDTDecl lr name arity fact_name nat_decls) =+ do nat_decls' <- mapM (evalNatDecl cenv) nat_decls+ return $ mkCDT lr name arity fact_name nat_decls'++evalNatDecl :: Monad m => CDTEnv -> (String, Type) -> m (String, T.Type)+evalNatDecl cenv (name, a :-> b) =+ do a' <- evalFE cenv a+ b' <- evalFE cenv b+ return (name, a' :-> b')++evalFE :: Monad m => CDTEnv -> FE -> m FE.FE+evalFE _ (FE.Var n) = return (FE.Var n)+evalFE cenv (FE.Ap sym xs) =+ do ys <- mapM (evalFE cenv) xs+ case find (\cdt -> sym == CDT.functName cdt) cenv of+ Just f ->+ if CDT.functArity f == length xs+ then return (FE.Ap f ys)+ else fail "wrong number of arguments"+ Nothing ->+ fail $ "no such functor or variable: " ++ sym++-----------------------------------------------------------------------------
+ src/CPLSystem.hs view
@@ -0,0 +1,162 @@+-----------------------------------------------------------------------------+-- |+-- Module : CPLSystem+-- Copyright : (c) Masahiro Sakai 2004,2009++-- License : BSD-style+-- +-- Maintainer : masahiro.sakai@gmail.com+-- Stability : provisional+-- Portability : portable+--+-----------------------------------------------------------------------------++module CPLSystem+ ( VarTable+ , System (..)+ , emptySystem+ , parseExp+ , checkName+ , parseCDT+ , parseDef+ , addCDT+ , letExp+ , simp+ ) where++import CDT+import qualified CDTParser+import qualified ExpParser+import Exp+import qualified AExp+import qualified Simp+import Type+import qualified Typing+import Typing (Typing(..))++-- FIXME+import qualified FE+import qualified Subst++import Control.Monad+import Data.Maybe+import Data.List+import Text.ParserCombinators.Parsec+import qualified Data.Map as Map++type CDTEnv = [CDT]++type VarTable = Map.Map Id ([Id], Exp, FType)++data System+ = System+ { objects :: !CDTEnv+ , varTable :: !VarTable+ , trace :: !Bool+ , lastExp :: !(Maybe Exp)+ }++emptySystem :: System+emptySystem =+ System{ objects = []+ , varTable = Map.empty+ , trace = False+ , lastExp = Nothing+ }++parseExp :: System -> String -> Either String (Int, Typing)+parseExp sys str =+ case parse ExpParser.exp "" str of+ Left err -> fail (show err)+ Right e ->+ case ExpParser.evalExp (objects sys) (arityEnv sys) e of+ Nothing -> Left "invalid expression" -- FIXME+ Just e ->+ Typing.runTI (tiEnv sys) $ do+ t <- Typing.inferType (substIt sys e)+ t <- Typing.appSubst t+ return $ AExp.quantify t++type Def = (Id, [Id], AExp.AExp, FType)++parseDef :: System -> String -> Either String Def+parseDef sys str =+ case parse ExpParser.def "" str of+ Left err -> fail (show err)+ Right (name,ps,e) ->+ case ExpParser.evalExp (objects sys) (Map.union (Map.fromList (zip ps (repeat 0))) (arityEnv sys)) e of+ Nothing -> Left "invalid definition" -- FIXME+ Just e1 ->+ Typing.runTI (tiEnv sys) $ do+ (ts, t) <- Typing.inferType2 ps e1+ ts <- Typing.appSubst ts+ t@(ae :! t') <- Typing.appSubst t+ let vars = Subst.tv (t' : ts)+ s = zip vars [FE.Var i | i<-[0..]]+ return (name, ps, Subst.apply s ae, FType (length vars) (Subst.apply s ts) (Subst.apply s t'))++arityEnv :: System -> Map.Map Id Int+arityEnv sys = if isJust (lastExp sys) then Map.insert "it" 0 env0 else env0+ where env0 = Map.map (\(ps,_,_) -> length ps) (varTable sys)++tiEnv :: System -> Map.Map Id (Either FType Type)+tiEnv sys = Map.map (\(ps, body, t) -> Left t) (varTable sys)++substIt :: System -> Exp -> Exp+substIt sys e = + case lastExp sys of+ Just it -> f it e+ Nothing -> e+ where+ f it Identity = Identity+ f it (Comp a b) = Comp (f it a) (f it b)+ f it e@(Nat _) = e+ f it (Fact obj args) = Fact obj $ map (f it) args+ f it (Funct obj args) = Funct obj $ map (f it) args+ f it (Var "it" []) = it+ f it (Var v args) = Var v $ map (f it) args++checkName :: Monad m => System -> String -> m ()+checkName sys name =+ if name `elem` names+ then fail ("\"" ++ name ++ "\" is already used")+ else return ()+ where+ vt = varTable sys+ objs = objects sys+ names = Map.keys vt +++ map CDT.functName objs +++ map CDT.factName objs +++ concatMap (map CDT.natName . CDT.nats) objs++parseCDT :: Monad m => System -> String -> m CDT.CDT+parseCDT sys src = case parse CDTParser.cdtDecl "" src of+ Left err -> fail (show err)+ Right decl -> CDTParser.evalCDTDecl (objects sys) decl++addCDT :: Monad m => System -> CDT.CDT -> m System+addCDT sys obj =+ if CDT.isComputable obj+ then do checkName sys (CDT.functName obj)+ checkName sys (CDT.factName obj)+ mapM_ (checkName sys . CDT.natName) (CDT.nats obj)+ return sys{ objects = obj : objects sys }+ else fail "not a computable object"++compile :: System -> Exp -> Simp.CompiledExp+compile sys e = Simp.compile env e+ where env = Map.map (\(ps,body,_) -> (ps, body)) (varTable sys)++letExp :: Monad m => System -> Def -> m System+letExp sys (name,ps,e,ftype) = do+ checkName sys name+ return sys{ varTable = Map.insert name (ps, AExp.skelton e, ftype) (varTable sys) }++simp :: System -> Bool -> Exp -> [(Int, Simp.CompiledExp, Simp.CompiledExp)]+simp sys full exp =+ let exp' = compile sys exp+ traces =+ if trace sys+ then Simp.simpWithTrace full exp'+ else [(0, compile sys Identity, Simp.simp full exp')]+ in traces
+ src/Exp.hs view
@@ -0,0 +1,64 @@+-----------------------------------------------------------------------------+-- |+-- Module : Exp+-- Copyright : (c) Masahiro Sakai 2009+-- License : BSD-style+-- +-- Maintainer : masahiro.sakai@gmail.com+-- Stability : provisional+-- Portability : portable+--+-- Expression of CPL.+--+-----------------------------------------------------------------------------++module Exp+ ( Id+ , Exp (..)+ , comp+ , expandFunct+ ) where++import qualified CDT+import qualified FE+import Type (GenType(..))+import Data.List (intercalate)++----------------------------------------------------------------------------++type Id = String++data Exp+ = Identity+ | Comp Exp Exp+ | Nat !CDT.Nat+ | Fact !CDT.CDT ![Exp]+ | Funct !CDT.CDT ![Exp]+ | Var !Id ![Exp]++instance Show Exp where+ show Identity = "I"+ show (Comp a b) = show a ++ "." ++ show b+ show (Nat nat) = CDT.natName nat+ show (Fact fact args) = CDT.factName fact ++ showArgs args+ show (Funct funct args) = CDT.functName funct ++ showArgs args+ show (Var name args) = name ++ showArgs args++showArgs :: [Exp] -> String+showArgs [] = ""+showArgs args = "(" ++ intercalate "," (map show args) ++ ")"++{-# INLINE comp #-}+comp :: Exp -> Exp -> Exp+comp a Identity = a+comp Identity b = b+comp a b = Comp a b++expandFunct :: CDT.CDT -> [Exp] -> Exp+expandFunct _ [] = Identity+expandFunct obj args = Fact obj (map g (CDT.nats obj))+ where g nat = FE.fold h expandFunct cod `comp`+ (Nat nat `comp` FE.fold h expandFunct dom)+ where h 0 = Identity+ h i = args !! (i-1)+ dom:->cod = CDT.natDeclType nat
+ src/ExpParser.hs view
@@ -0,0 +1,90 @@+-----------------------------------------------------------------------------+-- |+-- Module : ExpParser+-- Copyright : (c) Masahiro Sakai 2009+-- License : BSD-style+-- +-- Maintainer : masahiro.sakai@gmail.com+-- Stability : provisional+-- Portability : portable+--+-----------------------------------------------------------------------------++module ExpParser+ ( Exp (..)+ , exp+ , def+ , evalExp+ ) where++import qualified CDT+import qualified Exp as E+import ParserUtils++import Prelude hiding (exp)+import Control.Monad+import Text.ParserCombinators.Parsec+import Data.Maybe+import qualified Data.Map as Map++----------------------------------------------------------------------------++data Exp+ = Comp Exp Exp+ | Ident String [Exp]+ deriving (Show, Read)++exp :: Parser Exp+exp =+ do xs <- sepBy1 pident (tok (char '.' `mplus` char '\x2218'))+ return (foldr1 Comp xs)+ where pident = + do s <- ident+ xs <- option [] $ between (char' '(') (char' ')')+ $ exp `sepBy` char' ','+ spaces+ return (Ident s xs)++def :: Parser (E.Id, [E.Id], Exp)+def = do+ spaces+ s <- ident+ ps <- option [] $ between (char' '(') (char' ')') $ ident `sepBy` char' ','+ spaces+ char' '='+ body <- exp+ spaces+ return (s, ps, body)++----------------------------------------------------------------------------++type CDTEnv = [CDT.CDT]++evalExp :: CDTEnv -> (Map.Map String Int) -> Exp -> Maybe E.Exp+evalExp cenv env = listToMaybe . f+ where f (Comp a b) =+ do a' <- f a+ b' <- f b+ return (E.Comp a' b')+ f (Ident "I" args) =+ do guard (length args == 0)+ return E.Identity+ f (Ident s args) =+ do let arity = length args+ args' <- mapM f args+ o <- cenv+ msum [ do guard $ CDT.functName o == s &&+ CDT.functArity o == arity+ return (E.Funct o args')+ , do guard $ CDT.factName o == s &&+ CDT.nNats o == arity+ return (E.Fact o args')+ , do guard $ arity == 0+ n <- CDT.nats o+ guard $ CDT.natName n == s+ return (E.Nat n)+ , do guard $ Just arity == Map.lookup s env+ return (E.Var s args')+ ]++----------------------------------------------------------------------------
+ src/FE.hs view
@@ -0,0 +1,81 @@+{-# OPTIONS -fglasgow-exts #-}+-----------------------------------------------------------------------------+-- |+-- Module : FE+-- Copyright : (c) Masahiro Sakai 2004,2009+-- License : BSD-style+-- +-- Maintainer : masahiro.sakai@gmail.com+-- Stability : provisional+-- Portability : portable+--+-- Functorial expression and functorial calculus.+--+-----------------------------------------------------------------------------++module FE+ ( VarId+ , GenFE (..)+ , FE+ , fold+ , GenCFE (..)+ , CFE+ ) where++import Variance+import Funct+import {-# SOURCE #-} CDT (CDT, functName, functVariance, _eqCDT)++import Data.List (transpose, intercalate)++----------------------------------------------------------------------------++type VarId = Int++showVarId :: VarId -> String+showVarId v = seq m $ seq n $+ '*' : (table !! n) : (if m /= 0 then show m else "")+ where table = ['a'..'z']+ tableSize = length table+ (m,n) = v `divMod` tableSize++----------------------------------------------------------------------------+-- Functorial Expression++data GenFE f = Var !VarId | Ap !f [GenFE f] --deriving Eq+type FE = GenFE CDT++instance Eq FE where+ Var i == Var j = i==j+ Ap f xs == Ap g ys = _eqCDT f g && xs==ys+ _ == _ = False++instance Show FE where+ show = fold showVarId f+ where f funct args =+ case functVariance funct of+ [] -> functName funct+ _ -> functName funct ++ "(" ++ intercalate "," args ++ ")"++{-# INLINE fold #-}+fold :: (VarId -> a) -> (f -> [a] -> a) -> GenFE f -> a+fold f g = func+ where func (Var v) = f v+ func (Ap funct l) = g funct (map func l)++----------------------------------------------------------------------------+-- Closed Functorial Expression++data GenCFE f = CFE !Int !(GenFE f)+type CFE = GenCFE CDT++instance Funct f => Funct (GenCFE f) where+ variance (CFE n fe) = fold f g fe+ where f v = [if x==v then Covariance else FreeVariance | x <- [0..(n-1)] ]+ g obj args = case variance obj of+ [] -> nFree+ xs -> [ joinL [x `mult` y | (x,y) <- zip xs col]+ | col <- transpose args ]+ nFree = replicate n FreeVariance++----------------------------------------------------------------------------
+ src/Funct.hs view
@@ -0,0 +1,8 @@+module Funct+ ( Funct(..)+ ) where++import Variance++class Funct f where+ variance :: f -> [Variance]
+ src/Main.hs view
@@ -0,0 +1,418 @@+{-# LANGUAGE CPP #-}++-----------------------------------------------------------------------------+-- |+-- Module : Main+-- Copyright : (c) Masahiro Sakai 2004,2009+-- License : BSD-style+-- +-- Maintainer : masahiro.sakai@gmail.com+-- Stability : provisional+-- Portability : portable+--+-----------------------------------------------------------------------------++module Main where++import CDT+import Exp+import qualified Statement+import qualified CPLSystem as Sys+import qualified AExp+import Type+import Typing (Typing(..))+import qualified Simp++import Data.Maybe+import Data.List+import Data.Char (isSpace)+import System.Environment+import System.Exit+import System.IO+import Control.Monad.State+import Control.Monad.Error+import System.Console.GetOpt+#ifdef HAVE_READLINE_PACKAGE+import qualified System.Console.SimpleLineEditor as SLE+#endif+import Control.Exception++----------------------------------------------------------------------------++type UIState = Sys.System++getSystem :: (Monad m) => StateT UIState m Sys.System+getSystem = get++putSystem :: (Monad m) => Sys.System -> StateT UIState m ()+putSystem = put++initialState :: UIState+initialState = Sys.emptySystem++----------------------------------------------------------------------------+--- Utility++shift :: String -> (String, String)+shift = break isSpace . dropWhile isSpace++strip :: String -> String+strip = reverse . f . reverse . f+ where f = dropWhile isSpace++indent :: Int -> String -> String+indent n = unlines . map (prefix++) . lines+ where prefix = replicate n ' '++showObjectInfo :: CDT.CDT -> String+showObjectInfo obj =+ t ++ showFunctNameWithVariance obj ++ "\n" +++ "- natural transformations:\n" +++ natsStr +++ "- factorizer:\n" ++ factorizerInfoStr +++ "- equations:\n" ++ indent 4 equations +++ "- unconditioned: " ++ (if CDT.isUnconditioned obj then "yes" else "no") +++ "\n" +++ "- productive: (" ++ productiveStr ++ ")\n"+ where t = case CDT.objectType obj of+ LeftObject -> "left object "+ RightObject -> "right object "+ natsStr = indent 4 $ concatMap f (CDT.nats obj)+ where f nat = CDT.natName nat ++ ": " +++ show (CDT.natType nat) ++ "\n"+ productiveStr = intercalate "," (map f [0 .. CDT.functArity obj - 1])+ where f n = if CDT.isProductiveIn obj n+ then "yes"+ else "no"+ factorizerInfoStr =+ indent 4 $+ upper ++ "\n" +++ replicate (max (length upper) (length lower)) '-' ++ "\n" +++ lower ++ "\n"+ where upper = intercalate " " $ zipWith f factArgs $ factParams obj+ where f fact typ = show fact ++ ": " ++ show typ+ lower =+ show (Fact obj factArgs) ++ ": " +++ show (factDestType obj)+ factArgs = map f (CDT.nats obj)+ where f nat = Var ("f" ++ show (CDT.natIndex nat)) []+ equations = concat (map (++"\n") (eqs ++ [feq, ceq]))+ where eqs = zipWith g [(1::Int)..] (Statement.eqs obj)+ where g n eq = "("++lr++"EQ" ++ show n ++ "): " +++ show eq+ feq = "("++lr++"FEQ): " ++ show (Statement.feq obj)+ ceq = "("++lr++"CEQ): " ++ show (Statement.ceq obj)+ lr = case CDT.objectType obj of+ LeftObject -> "L"+ RightObject -> "R"++readLine :: String -> IO String+#ifdef HAVE_READLINE_PACKAGE+readLine prompt = fmap (fromMaybe "") (SLE.getLineEdited prompt)+#else+readLine prompt =+ do putStr prompt+ getLine+#endif++----------------------------------------------------------------------------++type Command = String -> StateT UIState IO ()++commandTable :: [(String, Command)]+commandTable =+ [ ("show", cmdShow)+ , ("edit", cmdEdit)+ , ("simp", cmdSimp)+ , ("let", cmdLet)+ , ("load", cmdLoad)+ , ("quit", cmdQuit)+ , ("exit", cmdQuit)+ , ("bye", cmdQuit)+ , ("help", cmdHelp)+ , ("set", cmdSet)+ , ("reset", cmdReset)++ , ("left", cmdLeft)+ , ("right", cmdRight)+ ]++dispatchCommand :: String -> StateT UIState IO ()+dispatchCommand l =+ case shift l of+ ([], _) -> return ()+ (cmdStr, arg) ->+ case lookup cmdStr commandTable of+ Just cmd -> cmd arg+ Nothing -> throwError (userError ("unknown command: " ++ l))++----------------------------------------------------------------------------++defineObject :: Command+defineObject src =+ do sys <- getSystem+ obj <- Sys.parseCDT sys src+ sys' <- Sys.addCDT sys obj+ putSystem sys'+ let lr = case CDT.objectType obj of+ LeftObject -> "left"+ RightObject -> "right"+ msg = concat [lr, " object ", showFunctNameWithVariance obj, " is defined"]+ lift $ putStrLn $ msg++cmdLeft, cmdRight :: Command+cmdLeft s = defineObject ("left " ++ s)+cmdRight s = defineObject ("right " ++ s)++cmdShow :: Command+cmdShow arg =+ case shift arg of+ ("object", arg') ->+ do sys <- getSystem+ let name = strip arg'+ objects = Sys.objects sys+ lift $ putStrLn $+ case find (\x -> CDT.functName x == name) objects of+ Just obj -> showObjectInfo obj+ Nothing -> "unknown object: " ++ name+ ("aexp", arg') -> do -- XXX+ sys <- getSystem+ case Sys.parseExp sys (strip arg') of+ Left err -> fail err+ Right (_, e :! t) -> lift $ do+ putStrLn $ show e+ putStrLn $ " : " ++ show t+ _ -> do+ sys <- getSystem+ case Sys.parseExp sys (strip arg) of+ Left err -> fail err+ Right (_, e :! t) -> lift $ do+ putStrLn $ show $ AExp.skelton e+ putStrLn $ " : " ++ show t++cmdLet :: Command+cmdLet arg = do+ sys <- getSystem+ case Sys.parseDef sys (strip arg) of+ Left err -> fail err+ Right def@(name, args, e, FType _ args' t) -> do+ sys' <- Sys.letExp sys def+ putSystem sys'+ if null args+ then lift $ do+ putStrLn $ name ++ " = " ++ show (AExp.skelton e)+ putStrLn $ " : " ++ show t+ else lift $ do+ let lhs = name ++ "(" ++ intercalate "," args ++ ")"+ putStrLn $ lhs ++ " = " ++ show (AExp.skelton e)+ let upper = intercalate " " $ [p ++ ": " ++ show t | (p,t) <- zip args args']+ lower = lhs ++ ": " ++ show t+ s = upper ++ "\n" +++ replicate (max (length upper) (length lower)) '-' ++ "\n" +++ lower+ putStrLn $ s+ -- putStrLn $ " : " ++ intercalate ", " (map show args') ++ " => " ++ show t++cmdSimp :: Command+cmdSimp arg =+ case shift arg of+ ("full", arg') ->+ doSimp True (strip arg')+ _ ->+ doSimp False (strip arg)+ where+ doSimp full str = do+ sys <- getSystem+ unless (any isTerminalObject (Sys.objects sys))+ (fail "No terminal object is defined.")+ case Sys.parseExp sys str of+ Left err -> fail err+ Right (_, e :! t) -> do+ unless (AExp.isElement e) (fail "not a element")+ let traces = Sys.simp sys full (AExp.skelton e)+ loop ((step,(depth,exp,cexp)) : xs) = do+ let line = show step+ ++ (if depth==0 then "" else "[" ++ show depth ++ "]")+ ++ ":" ++ show (Simp.decompile exp) ++ "*" ++ show (Simp.decompile cexp)+ when (Sys.trace sys) $ lift $ putStrLn line+ if null xs+ then do+ let it = Simp.decompile cexp+ lift $ putStrLn (show it)+ lift $ putStrLn (" : " ++ show t)+ putSystem sys{ Sys.lastExp = Just it }+ else+ loop xs+ loop (zip [(0::Int)..] traces)++cmdLoad :: Command+cmdLoad s =+ do h <- lift $ openFile filename ReadMode+ contents <- lift $ hGetContents h+ let src = unlines (map removeComment (lines contents))+ cmds = split src+ mapM_ (\x -> do lift $ (putStr . unlines . map ("> "++) . lines $ x)+ dispatchCommand x)+ cmds+ where filename = -- FIXME+ let s' = strip s in+ case s' of+ '"':_ -> read s'+ _ -> s'+ removeComment [] = []+ removeComment ('#':_) = []+ removeComment (x:xs) = x : removeComment xs+ split :: String -> [String]+ split s = map (strip . reverse) (f s [])+ where f (';':xs) tmp = tmp : (f xs [])+ f (x:xs) tmp = f xs (x:tmp)+ f [] tmp = [tmp]++cmdEdit :: Command+cmdEdit _ =+ do s <- lift editLoop+ dispatchCommand s+ where editLoop =+ do l <- readLine "| "+ case dropWhile isSpace (reverse l) of+ ';':s -> return (reverse s)+ _ -> do s <- editLoop+ return $ l ++ "\n" ++ s++cmdQuit :: Command+cmdQuit _ = lift $ exitWith ExitSuccess++cmdHelp :: Command+cmdHelp _ = lift $ mapM_ putStrLn l+ where l = [ " exit exit the interpreter"+ , " quit ditto"+ , " bye ditto"+ , " edit enter editing mode"+ , " simp [full] <exp> evaluate expression"+ , " show <exp> print type of expression"+ , " show object <functor> print information of functor"+ , " load <filename> load from file"+ , " set trace [on|off] enable/disable trace"+ , " reset remove all definitions"+ ]++cmdSet :: Command+cmdSet arg =+ case shift arg of+ (flag, a) ->+ case shift a of+ ([], _) ->+ case flag of+ "trace" ->+ do sys <- getSystem+ lift $ putStrLn $+ "trace=" ++ (if Sys.trace sys then "on" else "off")+ _ ->+ lift $ putStrLn $ "unknown flag:" ++ flag+ (value, _) ->+ case flag of+ "trace" ->+ case value of+ "on" ->+ do sys <- getSystem+ putSystem (sys{ Sys.trace = True })+ "off" ->+ do sys <- getSystem+ putSystem (sys{ Sys.trace = False })+ _ ->+ lift $ putStrLn ("unknown value:" ++ value)+ _ ->+ lift $ putStrLn ("unknown flag:" ++ flag)++cmdReset :: Command+cmdReset _ = put initialState++----------------------------------------------------------------------------++data Flag+ = Help+ | Version+ | Interactive+ -- | Load String+ | Trace String+ deriving Eq++options :: [OptDescr Flag]+options =+ [ Option ['h'] ["help"] (NoArg Help) "show help"+ , Option ['v'] ["version"] (NoArg Version) "show version number"+ , Option ['i'] ["interactive"] (NoArg Interactive) "force interactive mode"+ -- , Option ['l'] ["load"] (ReqArg Load "FILE") "load FILE"+ , Option ['t'] ["trace"] (OptArg (Trace . fromMaybe "on") "[on|off]")+ "enable/disable trace"+ ]++main :: IO ()+main =+#ifndef HAVE_READLINE_PACKAGE+ do bracket (do x <- hGetBuffering stdout+ hSetBuffering stdout NoBuffering+ return x)+ (hSetBuffering stdout)+ (const main_)+#else+ do bracket SLE.initialise+ (const SLE.restore)+ (const main_)+#endif++main_ :: IO ()+main_ =+ do args <- getArgs+ case getOpt Permute options args of+ (o,_,[]) | Help `elem` o ->+ putStrLn (usageInfo header options)+ (o,_,[]) | Version `elem` o ->+ putStrLn versionStr+ (o,n,[]) ->+ do putStr banner+ evalStateT (do mapM_ processOpt o+ mapM_ cmdLoad n+ if null n || Interactive `elem` o+ then mainLoop+ else return ())+ initialState+ (_,_,errs) ->+ ioError $ userError $ concat errs ++ usageInfo header options++version :: [Int]+version = [0,0,2]++versionStr :: String+versionStr = intercalate "." $ map show $ version++header :: String+header = "Usage: cpl [OPTION...] files..."++banner :: String+banner =+ "Categorical Programming Language (Haskell version)\n" +++ "version " ++ versionStr ++ "\n" +++ "\n" +++ "Type help for help\n" +++ "\n"++processOpt :: Flag -> StateT UIState IO ()+processOpt (Trace s) =+ do sys <- getSystem+ val <- case s of+ "on" -> return True+ "off" -> return False+ _ -> fail "invalid option"+ putSystem sys{ Sys.trace = val }+ return ()+processOpt _ = return ()++mainLoop :: StateT UIState IO ()+mainLoop =+ do l <- lift $ readLine "cpl> "+ catchError (dispatchCommand l)+ (lift . putStrLn . show)+ mainLoop++----------------------------------------------------------------------------
+ src/ParserUtils.hs view
@@ -0,0 +1,26 @@+module ParserUtils+ ( tok+ , char'+ , string'+ , Ident+ , ident+ ) where++import Text.ParserCombinators.Parsec+import Data.Char++type Ident = String++tok :: Parser a -> Parser a+tok p = do x <- p+ spaces+ return x++char' :: Char -> Parser Char+char' = tok . char++string' :: String -> Parser String+string' = tok . string++ident :: Parser Ident+ident = tok $ many1 $ satisfy $ \c -> isAlphaNum c || (c `elem` "'!_")
+ src/Simp.hs view
@@ -0,0 +1,352 @@+{- # OPTIONS -ddump-simpl -ddump-stg # -}+-----------------------------------------------------------------------------+-- |+-- Module : Simp+-- Copyright : (c) Masahiro Sakai 2004-2009+-- License : BSD-style+-- +-- Maintainer : masahiro.sakai@gmail.com+-- Stability : provisional+-- Portability : portable+--+-- Simplifier+--+-----------------------------------------------------------------------------++module Simp+ ( CompiledExp+ , compile+ , decompile+ , simp+ , simpWithTrace+ ) where++import qualified Exp as E+import qualified CDT+import qualified FE+import Exp (Id)+import Type+import Control.Monad.RWS+import Data.Array+import qualified Data.Map as Map++----------------------------------------------------------------------------++data CompiledExp+ = Identity+ | Comp CompiledExp CompiledExp+ | LNat !CDT.Nat+ | RNat !CDT.Nat+ | LFact !CDT.CDT [CompiledExp] !(Array Int CompiledExp)+ | RFact !CDT.CDT [CompiledExp]+ | Var E.Exp CompiledExp++compile :: (Map.Map E.Id ([E.Id], E.Exp)) -> E.Exp -> CompiledExp+compile env = f+ where+ f E.Identity = Identity+ f (E.Comp a b) = f a `comp` f b+ f (E.Funct sym args) = expandFunct sym (map f args)+ f (E.Fact sym args) = mkFact sym (map f args)+ f (E.Nat sym) = mkNat sym+ f src@(E.Var v args) = Var src (compile env' body)+ where+ (ps, body) = env Map.! v+ -- Note that Map.union is left biased+ env' = Map.union (Map.fromList [(p, ([], arg)) | (p,arg) <- zip ps args]) env++{-# INLINE mkFact #-}+mkFact :: CDT.CDT -> [CompiledExp] -> CompiledExp+mkFact obj args =+ case CDT.objectType obj of+ CDT.LeftObject -> lfact+ where+ lfact = LFact obj args (listArray (0, CDT.nNats obj - 1) l)+ l = zipWith f args (CDT.nats obj)+ f arg nat =+ case CDT.natIsUnconditioned nat of --- optimize+ True -> arg+ False -> arg `comp` (subst1 lfact (CDT.natDeclDom nat))+ CDT.RightObject -> RFact obj args++{-# INLINE mkNat #-}+mkNat :: CDT.Nat -> CompiledExp+mkNat sym =+ case CDT.objectType (CDT.natCDT sym) of+ CDT.LeftObject -> LNat sym+ CDT.RightObject -> RNat sym++decompile :: CompiledExp -> E.Exp+decompile Identity = E.Identity+decompile (Comp e1 e2) = E.Comp (decompile e1) (decompile e2)+decompile (LNat nat) = E.Nat nat+decompile (RNat nat) = E.Nat nat+decompile (LFact sym args _) = E.Fact sym (map decompile args)+decompile (RFact sym args) = E.Fact sym (map decompile args)+decompile (Var src _) = src++----------------------------------------------------------------------------++simp :: Bool -> CompiledExp -> CompiledExp+simp full startExp =+ if full+ then simpFull startExp+ else simpLazy startExp++{-# NOINLINE simpFull #-}+{-# NOINLINE simpLazy #-}+simpFull, simpLazy :: CompiledExp -> CompiledExp+simpFull = simpImpl True+simpLazy = simpImpl False++{-# INLINE simpImpl #-}+simpImpl :: Bool -> CompiledExp -> CompiledExp+simpImpl full startExp = seq full $ simp1 startExp Identity+ where+ simp1 :: CompiledExp -> CompiledExp -> CompiledExp++ simp1 Identity c = c --- IDENT+ + simp1 (Comp a b) c = simp1 a (simp1 b c) --- COMP+ + simp1 e@(LNat _) c = e `comp` c -- L-NAT+ simp1 (RNat sym) c+ | full = simp1_FULL_R_NAT sym c --- FULL-R-NAT+ | otherwise = simp1_R_NAT sym c --- R-NAT+ + simp1 (LFact _ _ table) c = --- L-FACT+ case split c of+ (LNat sym, c') -> simp1 (table ! (CDT.natIndex sym)) c'+ _ -> impossible+ + simp1 e@(RFact obj args) c+ | full && CDT.isUnconditioned obj = simp1_FULL_C_FACT obj args c+ | otherwise = e `comp` c -- R-FACT+ + simp1 (Var _ e) c = simp1 e c+ + ----------------------------------+ + simp1_R_NAT :: CDT.Nat -> CompiledExp -> CompiledExp+ simp1_R_NAT sym c =+ case simp2 c sym of+ (factR@(RFact _ args), c'') ->+ if CDT.natIsUnconditioned sym --- optimize+ then simp1 (args !! CDT.natIndex sym) c''+ else simp1 (subst1 factR (CDT.natDeclCod sym))+ (simp1 (args !! CDT.natIndex sym) c'')+ _ -> impossible+ + simp1_FULL_R_NAT :: CDT.Nat -> CompiledExp -> CompiledExp+ simp1_FULL_R_NAT sym factP =+ case pickupFactR sym factP of+ (factR@(RFact _ args), factP') ->+ if CDT.natIsUnconditioned sym+ then simp1 (args !! CDT.natIndex sym) factP'+ else simp1 (subst1 factR (CDT.natDeclCod sym))+ (simp1 (args !! CDT.natIndex sym) factP')+ _ -> impossible+ + simp1_FULL_C_FACT :: CDT.CDT -> [CompiledExp] -> CompiledExp -> CompiledExp+ simp1_FULL_C_FACT obj args p = RFact obj (zipWith f args (CDT.nats obj))+ {- 並列処理出来るのって、ここのzipWithくらいだろうか -}+ where+ f e nat =+ case CDT.natDeclDom nat of+ FE.Var 0 -> simp1 e p+ fe -> e `comp` subst1 p fe -- ack(3,3)で16000回くらい+ + ----------------------------------+ + simp2 :: CompiledExp -> CDT.Nat -> (CompiledExp, CompiledExp)+ simp2 c sym = f (CDT.natProjectionSequence sym) c+ where+ f :: [Int] -> CompiledExp -> (CompiledExp, CompiledExp)+ f [] c = split c --- R-NAT-V+ f (j:js) c_ = --- R-NAT-F+ case split c_ of+ (RFact p args, c) ->+ case g 0 args (CDT.nats p) of+ (factR, args') -> (factR, (RFact p args'))+ where+ g i (arg:args) (nat:nats)+ | i==j =+ case f js (simp1 arg c) of+ (factR', arg') -> (factR',arg':args')+ | otherwise =+ let arg' = arg `comp` subst1 c (CDT.natDeclDom nat)+ in (factR, arg':args')+ where (factR, args') = g (i+1) args nats+ g _ [] [] = (undefined, [])+ g _ _ _ = impossible+ _ -> impossible++{-# INLINE pickupFactR #-}+pickupFactR :: CDT.Nat -> CompiledExp -> (CompiledExp,CompiledExp)+pickupFactR sym = f (CDT.natProjectionSequence sym)+ where+ f :: [Int] -> CompiledExp -> (CompiledExp, CompiledExp)+ f [] e = split e+ f (j:js) (RFact p args) =+ case processArgs 0 args of+ (factR, args') -> (factR, RFact p args')+ where+ processArgs :: Int -> [CompiledExp] -> (CompiledExp, [CompiledExp])+ processArgs i (arg:args)+ | i==j =+ case f js arg of+ (factR, arg') -> (factR, arg':args)+ | otherwise =+ case processArgs (i+1) args of+ (factR, args') -> (factR, arg:args')+ processArgs _ _ = impossible+ f _ _ = impossible++----------------------------------------------------------------------------++type Trace = [(Int,CompiledExp,CompiledExp)]+type M = RWS Int Trace ()++runM :: M x -> Trace+runM x =+ case runRWS x 0 () of+ (_,_,c) -> c++trace :: CompiledExp -> CompiledExp -> M ()+trace e c = do+ depth <- ask+ seq depth $ seq e $ seq c $ tell [(depth,e,c)]++deepen :: M a -> M a+deepen = local (+1)++simpWithTrace :: Bool -> CompiledExp -> Trace+simpWithTrace full startExp = seq full $ runM $ do+ c <- simp1 startExp Identity+ trace Identity c+ return ()+ where+ simp1 :: CompiledExp -> CompiledExp -> M CompiledExp++ simp1 a c = trace a c >> simp1' a c++ simp1' Identity c = return c++ simp1' (Comp a b) c = do+ c' <- deepen (simp1 b c)+ simp1 a c'++ simp1' e@(LNat _) c = return (e `comp` c) --- L-NAT+ simp1' (RNat sym) c+ | full = simp1_FULL_R_NAT sym c --- FULL-R-NAT+ | otherwise = simp1_R_NAT sym c --- R-NAT++ simp1' (LFact _ _ table) c = --- L-FACT+ case split c of+ (LNat sym, c') -> simp1 (table ! (CDT.natIndex sym)) c'+ _ -> impossible++ simp1' e@(RFact obj args) c+ | full && CDT.isUnconditioned obj = simp1_FULL_C_FACT obj args c --- FULL-C-FACT+ | otherwise = return (e `comp` c) -- R-FACT++ simp1' (Var _ e) c = simp1 e c++ ----------------------------------++ simp1_R_NAT :: CDT.Nat -> CompiledExp -> M CompiledExp+ simp1_R_NAT sym c = do+ tmp <- simp2 c sym+ case tmp of+ (factR@(RFact _ args), c'') ->+ if CDT.natIsUnconditioned sym+ then simp1 (args !! CDT.natIndex sym) c''+ else simp1 (subst1 factR (CDT.natDeclCod sym) `comp` (args !! CDT.natIndex sym)) c''+ _ -> impossible++ simp1_FULL_R_NAT :: CDT.Nat -> CompiledExp -> M CompiledExp+ simp1_FULL_R_NAT sym factP =+ case pickupFactR sym factP of+ (factR@(RFact _ args), factP') ->+ if CDT.natIsUnconditioned sym+ then simp1 (args !! CDT.natIndex sym) factP'+ else simp1 (subst1 factR (CDT.natDeclCod sym) `comp` (args !! CDT.natIndex sym)) factP'+ _ -> impossible++ simp1_FULL_C_FACT :: CDT.CDT -> [CompiledExp] -> CompiledExp -> M CompiledExp+ simp1_FULL_C_FACT obj args p = do+ args' <- zipWithM f args (CDT.nats obj)+ return (RFact obj args')+ where+ f e nat =+ case CDT.natDeclDom nat of+ FE.Var 0 -> simp1 e p+ fe -> return (e `comp` subst1 p fe) -- ack(3,3)で16000回くらい++ ----------------------------------++ simp2 :: CompiledExp -> CDT.Nat -> M (CompiledExp, CompiledExp)+ simp2 c sym = f (CDT.natProjectionSequence sym) c+ where+ f :: [Int] -> CompiledExp -> M (CompiledExp, CompiledExp)+ f [] c = return (split c) --- R-NAT-V+ f (j:js) c_ = --- R-NAT-F+ case split c_ of+ (RFact p args, c) -> do+ (factR, args') <- g 0 args (CDT.nats p)+ return (factR, (RFact p args'))+ where+ g _ [] [] = return (undefined, [])+ g i (arg:args) (nat:nats)+ | i==j = do+ (_, args') <- g (i+1) args nats+ tmp <- simp1 arg c+ (factR', arg') <- f js tmp+ return (factR',arg':args')+ | otherwise = do+ (factR, args') <- g (i+1) args nats+ let arg' = arg `comp` subst1 c (CDT.natDeclDom nat)+ return (factR, arg':args')+ g _ _ _ = impossible+ _ -> impossible++----------------------------------------------------------------------------++{-# INLINE comp #-}+comp :: CompiledExp -> CompiledExp -> CompiledExp+comp a Identity = a+comp Identity b = b+comp a b = Comp a b++split :: CompiledExp -> (CompiledExp, CompiledExp)+split (Comp a b) =+ case split a of+ (c, d) -> (c, d `comp` b)+split a = (a,Identity)+{-+split :: CompiledExp -> (CompiledExp, CompiledExp)+split (Comp a b) = go a b+ where+ go (Comp a b) r = go a (Comp b r)+ go e r = (e, r)+split e = (e, Identity)+-}++subst1 :: CompiledExp -> FE.FE -> CompiledExp+subst1 x e = FE.fold f expandFunct e+ where+ f 0 = x+ f _ = Identity++expandFunct :: CDT.CDT -> [CompiledExp] -> CompiledExp+expandFunct _ [] = Identity+expandFunct obj args = mkFact obj (map g (CDT.nats obj))+ where+ g nat = FE.fold h expandFunct cod `comp` (mkNat nat `comp` FE.fold h expandFunct dom)+ where+ h 0 = Identity+ h i = args !! (i-1)+ dom:->cod = CDT.natDeclType nat++impossible :: a+impossible = error "impossible happens"
+ src/Statement.hs view
@@ -0,0 +1,97 @@+-----------------------------------------------------------------------------+-- |+-- Module : Statement+-- Copyright : (c) Masahiro Sakai 2004,2009+-- License : BSD-style+-- +-- Maintainer : masahiro.sakai@gmail.com+-- Stability : provisional+-- Portability : portable+--+-----------------------------------------------------------------------------++module Statement+ ( ConditionalEquation (..)+ , Equation (..)+ , eqs+ , ceq+ , feq+ , statements+ ) where++import CDT+import Exp+import qualified FE+import Data.List++infix 4 :=:+infixr 3 :=>++data ConditionalEquation = [Equation] :=> Equation+data Equation = Exp :=: Exp++instance Show ConditionalEquation where+ show (premisses :=> body) =+ case premisses of+ [] -> show body+ _ -> intercalate " & " (map show premisses) ++ " => " ++ show body++instance Show Equation where+ show (a :=: b) = show a ++ "=" ++ show b++eqs :: CDT.CDT -> [ConditionalEquation]+eqs obj = map f (CDT.nats obj)+ where f nat =+ case CDT.objectType obj of+ LeftObject ->+ [] :=>+ FE.fold g mkFunct (CDT.natDeclCod nat) `comp` Nat nat+ :=: (factArgs !! CDT.natIndex nat) `comp`+ FE.fold g mkFunct (CDT.natDeclDom nat)+ RightObject ->+ [] :=>+ Nat nat `comp` FE.fold g mkFunct (CDT.natDeclDom nat)+ :=: FE.fold g mkFunct (CDT.natDeclCod nat) `comp`+ (factArgs !! CDT.natIndex nat)+ factArgs = map (\i -> Var ("f" ++ show i) []) [0 .. CDT.nNats obj - 1]+ g 0 = Fact obj factArgs+ g _ = Identity++ceq :: CDT -> ConditionalEquation+ceq obj = map f (CDT.nats obj) :=> (u :=: Fact obj args)+ where f nat =+ case CDT.objectType obj of+ LeftObject ->+ FE.fold g mkFunct (CDT.natDeclCod nat) `comp` Nat nat+ :=:+ (args !! CDT.natIndex nat) `comp`+ FE.fold g mkFunct (CDT.natDeclDom nat)+ RightObject ->+ Nat nat `comp` FE.fold g mkFunct (CDT.natDeclDom nat)+ :=:+ FE.fold g mkFunct (CDT.natDeclCod nat) `comp`+ (args !! CDT.natIndex nat)+ args = map (\i -> Var ("f" ++ show i) []) [0 .. CDT.nNats obj - 1]+ u = Var "g" []+ g 0 = u+ g _ = Identity++feq :: CDT -> ConditionalEquation+feq obj = [] :=> Funct obj functArgs :=: Fact obj factArgs+ where functArgs = map f [0 .. CDT.functArity obj - 1]+ where f i = Var ("f" ++ show i) []+ factArgs = map f (CDT.nats obj)+ where f nat = FE.fold g mkFunct (CDT.natDeclCod nat) `comp`+ Nat nat `comp`+ FE.fold g mkFunct (CDT.natDeclDom nat)+ g 0 = Identity+ g n = functArgs !! (n-1)++statements :: CDT -> [ConditionalEquation]+statements obj = eqs obj ++ [feq obj, ceq obj]++-----------------------------------------------------------------------------++mkFunct :: CDT -> [Exp] -> Exp+mkFunct _ [] = Identity+mkFunct obj args = Funct obj args
+ src/Subst.hs view
@@ -0,0 +1,99 @@+{-# OPTIONS -fglasgow-exts #-}+-----------------------------------------------------------------------------+-- |+-- Module : Subst+-- Copyright : (c) Masahiro Sakai 2006,2009+-- License : BSD-style+-- +-- Maintainer : masahiro.sakai@gmail.com+-- Stability : provisional+-- Portability : +--+-- Based on "Typing Haskell in Haskell".+-- http://www.cse.ogi.edu/~mpj/thih/+-----------------------------------------------------------------------------++module Subst+ ( Subst+ , nullSubst+ , (+->)+ , FEs (..)+ , (@@)+ , merge+ , mgu+ , match+ , varBind+ ) where++import FE+import {-# SOURCE #-} CDT (_eqCDT)++import Data.List (nub, intersect)+import Data.Maybe (fromMaybe)+++type Subst = [(VarId,FE)]++nullSubst :: Subst+nullSubst = []++(+->) :: VarId -> FE -> Subst+u+->t = [(u,t)]++class FEs t where+ apply :: Subst -> t -> t+ tv :: t -> [VarId]++instance FEs FE where+ apply s = fold (\v -> fromMaybe (Var v) (lookup v s)) Ap+ tv = nub . fold return (const concat)++instance FEs a => FEs [a] where+ apply s = map (apply s)+ tv = nub . concat . map tv++infixr 4 @@+(@@) :: Subst -> Subst -> Subst+s1 @@ s2 = [(u, apply s1 t) | (u,t) <- s2] ++ s1++merge :: Monad m => Subst -> Subst -> m Subst+merge s1 s2 = if agree then return (s1 ++ s2) else fail "merge fails"+ where agree = all (\v -> apply s1 (Var v :: FE) == apply s2 (Var v))+ (map fst s1 `intersect` map fst s2)++mgu :: Monad m => FE -> FE -> m Subst+mgu (Ap obj1 args1) (Ap obj2 args2) =+ if obj1 `_eqCDT` obj2+ then mguList args1 args2+ else fail "types do not unify"+mgu (Var u) t = varBind u t+mgu t (Var u) = varBind u t++mguList :: Monad m => [FE] -> [FE] -> m Subst+mguList (a:as) (b:bs) =+ do s1 <- mgu a b+ s2 <- mguList (apply s1 as) (apply s1 bs)+ return (s2 @@ s1)+mguList [] [] = return nullSubst+mguList _ _ = fail "types do not unify"++match :: Monad m => FE -> FE -> m Subst+match (Ap obj1 args1) (Ap obj2 args2) =+ if obj1 `_eqCDT` obj2+ then matchList args1 args2+ else fail "types do not unify"+match (Var u) t = varBind u t+match _ _ = fail "types do not unify"++matchList :: Monad m => [FE] -> [FE] -> m Subst+matchList (a:as) (b:bs) =+ do s1 <- match a b+ s2 <- matchList (apply s1 as) (apply s1 bs)+ return (s2 @@ s1)+matchList [] [] = return nullSubst+matchList _ _ = fail "types do not unify" ++varBind :: Monad m => VarId -> FE -> m Subst+varBind u t | t == Var u = return nullSubst+ | u `elem` tv t = fail "occurs check fails"+ | otherwise = return (u +-> t)
+ src/Type.hs view
@@ -0,0 +1,44 @@+{-# OPTIONS -fglasgow-exts #-}+-----------------------------------------------------------------------------+-- |+-- Module : Type+-- Copyright : (c) Masahiro Sakai 2006,2009+-- License : BSD-style+-- +-- Maintainer : masahiro.sakai@gmail.com+-- Stability : provisional+-- Portability : portable+--+-----------------------------------------------------------------------------++module Type+ ( GenType (..)+ , Type+ , FType (..)+ ) where++import FE+import Subst+import {-# SOURCE #-} CDT (CDT)++import Data.List (nub)++data GenType f+ = (:->)+ { dom :: !(GenFE f)+ , cod :: !(GenFE f)+ }++type Type = GenType CDT++instance Eq Type where+ (a :-> b) == (c :-> d) = a==c && b==d++instance FEs Type where+ apply s (a :-> b) = apply s a :-> apply s b+ tv (a :-> b) = nub (tv a ++ tv b)++instance Show Type where+ show (a :-> b) = show a ++ " -> " ++ show b++data FType = FType !Int [Type] Type
+ src/Typing.hs view
@@ -0,0 +1,176 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+module Typing+ ( Typing (..)+ , inferType+ , inferType2++ , TI+ , Env+ , runTI+ , getSubst+ , extSubst+ , appSubst+ , unify+ , newFEVar+ ) where++import Variance+import Funct+import qualified FE+import qualified CDT+import Type (GenType (..), Type, FType (..))+import Subst+import AExp+import qualified Exp as E++import Data.List (nub)+import Control.Monad.Error+import Control.Monad.RWS+import qualified Data.Map as Map++----------------------------------------------------------------------------++infix 6 :!+data Typing = AExp :! Type++tm :: Typing -> AExp+tm (e :! _) = e++ty :: Typing -> Type+ty (_ :! t) = t++instance FEs Typing where+ tv (e :! t) = nub (tv e ++ tv t)+ apply s (e :! t) = apply s e :! apply s t++----------------------------------------------------------------------------++-- Type inference monad+newtype TI a = TI (RWST Env () TIState (Either String) a)+ deriving (Monad, MonadState TIState, MonadReader Env, MonadError String)++type Env = Map.Map E.Id (Either FType Type)+type TIState = (Int, Subst)++runTI :: Env -> TI a -> Either String a+runTI env (TI m) = liftM fst (evalRWST m env initialState)+ where initialState = (0, nullSubst)++getSubst :: TI Subst+getSubst = do+ (_,s) <- get+ return s++extSubst :: Subst -> TI ()+extSubst s2 = do+ (i,s1) <- get+ put (i, s2@@s1)+ return ()++appSubst :: (FEs a) => a -> TI a+appSubst x = do+ s <- getSubst+ return (apply s x)++unify :: FE.FE -> FE.FE -> TI ()+unify a b = do+ s1 <- getSubst+ s2 <- mgu (apply s1 a) (apply s1 b)+ extSubst s2++newFEVar :: TI FE.FE+newFEVar = do+ (i,s) <- get+ put (i+1,s)+ return $ FE.Var i++----------------------------------------------------------------------------++inferType :: E.Exp -> TI Typing+inferType E.Identity = iIdentity+inferType (E.Comp a b) = do+ a' <- inferType a+ b' <- inferType b+ iComp a' b'+inferType (E.Nat nat) = iNat nat+inferType (E.Fact obj args) = iFact obj =<< mapM inferType args+inferType (E.Funct obj args) = iFunct obj =<< mapM inferType args+inferType (E.Var v args) = iVar v =<< mapM inferType args++inferType2 :: [E.Id] -> E.Exp -> TI ([Type], Typing)+inferType2 ps e = do+ ps <- liftM Map.fromList $ forM ps $ \p -> do+ dom <- newFEVar+ cod <- newFEVar+ return (p, dom :-> cod)+ local (Map.union (Map.map Right ps)) $ do+ t <- inferType e+ return (map snd (Map.toList ps), t)++----------------------------------------------------------------------------+-- introduction rules++iIdentity :: TI Typing+iIdentity = do+ v <- newFEVar+ return $ Identity v :! v :-> v++iComp :: Typing -> Typing -> TI Typing+iComp (f :! domf :-> codf) (g :! domg :-> codg) = do+ unify domf codg+ return $ Comp f g :! domg :-> codf++iNat :: CDT.Nat -> TI Typing+iNat nat = do+ annotation <- sequence $ replicate (CDT.natNTypeParams nat) newFEVar+ return $ Nat nat annotation :! apply (zip [0..] annotation) (CDT.natType nat)++iFact :: CDT.CDT -> [Typing] -> TI Typing+iFact obj args = do+ annotation <- sequence $ replicate (CDT.factNTypeParams obj) newFEVar+ let s = zip [0..] annotation+ unifyParams (apply s (CDT.factParams obj)) args+ return $ Fact obj (map tm args) annotation :! apply s (CDT.factDestType obj)++iFunct :: CDT.CDT -> [Typing] -> TI Typing+iFunct obj args = do+ (doml,codl) <- unifyParams (variance obj) args+ return $ Funct obj (map tm args) :! FE.Ap obj doml :-> FE.Ap obj codl+ where+ unifyParams [] [] = return ([],[])+ unifyParams (v:vs) ((_ :! d:->c) : as) = do+ (doms,cods) <- unifyParams vs as+ case v of+ Covariance -> return (d:doms, c:cods)+ Contravariance -> return (c:doms, d:cods)+ FixedVariance -> unify d c >> return (d:doms, d:cods)+ FreeVariance -> do+ x <- newFEVar+ y <- newFEVar+ return (x:doms, y:cods)+ unifyParams _ _ = throwError "wrong number of arguments"++iVar :: E.Id -> [Typing] -> TI Typing+iVar v args = do+ env <- ask+ case Map.lookup v env of+ Just (Right t) ->+ return $ Var v [] [] t :! t+ Just (Left (FType n typs typ)) -> do+ annotation <- sequence (replicate n newFEVar)+ let s = zip [0..] annotation+ unifyParams (apply s typs) args+ let t = apply s typ+ return $ Var v annotation (map tm args) t :! t+ Nothing -> throwError $ "no such variable: " ++ v++unifyParams :: [Type] -> [Typing] -> TI ()+unifyParams [] [] = return ()+unifyParams ((pdom :-> pcod):ps) ((_ :! adom:->acod):as) = do+ unify pdom adom+ unify pcod acod+ unifyParams ps as+ return ()+unifyParams _ _ = throwError "wrong number of arguments"++----------------------------------------------------------------------------
+ src/Variance.hs view
@@ -0,0 +1,75 @@+-----------------------------------------------------------------------------+-- |+-- Module : Variance+-- Copyright : (c) Masahiro Sakai 2009+-- License : BSD-style+-- +-- Maintainer : masahiro.sakai@gmail.com+-- Stability : provisional+-- Portability : portable+--+-- Variance calculation.+--+-----------------------------------------------------------------------------++module Variance+ ( Variance(..)+ , top+ , bottom+ , join+ , meet+ , joinL+ , meetL+ , mult+ , mnemonic+ ) where++data Variance+ = Covariance --- ++ | Contravariance --- -+ | FixedVariance --- T+ | FreeVariance --- ⊥+ deriving (Show,Read,Eq)++mnemonic :: Variance -> String+mnemonic Covariance = "+"+mnemonic Contravariance = "-"+mnemonic FixedVariance = "T"+mnemonic FreeVariance = "_|_"++bottom, top :: Variance+bottom = FreeVariance+top = FixedVariance++join,meet :: Variance -> Variance -> Variance+join a b | a==b = a+ | a==FreeVariance = b+ | b==FreeVariance = a+ | otherwise = FixedVariance+meet a b | a==b = a+ | a==FixedVariance = b+ | b==FixedVariance = a+ | otherwise = FreeVariance++joinL,meetL :: [Variance] -> Variance+joinL = foldl join bottom+meetL = foldl meet top++{-++・|⊥|+ |- |T+--+--+--+--+--+⊥|⊥|⊥|⊥|⊥++ |⊥|+ |- |T+- |⊥|- |+ |T+T |⊥|T |T |T++-}+mult :: Variance -> Variance -> Variance+mult _ FreeVariance = FreeVariance+mult FreeVariance _ = FreeVariance+mult _ FixedVariance = FixedVariance+mult FixedVariance _ = FixedVariance+mult a Covariance = a+mult Covariance a = a+mult Contravariance Contravariance = Covariance