Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
System modules
[go: Go Back, main page]

System modules

There are a number of system modules containing commonly used types and functions. Some of these modules written entirely in Cayenne, some (like the Int module) are not.

All the signatures below should be read as if in the context 

let String = System$String.String
    Char = System$Char.Char
    Int = System$Int.Int
    Bool = System$Bool.Bool
    List = System$List.List
    Unit = System$Unit.Unit
    Pair = System$Tuples.Pair
in

Bool

System$Bool ::
sig {
  data Bool = False | True;
  if :: (a :: #) |-> Bool -> a -> a -> a;
  (&&) :: Bool -> Bool -> Bool;
  (||) :: Bool -> Bool -> Bool;
  not :: Bool -> Bool;
  show :: Bool -> String;
};

Char

System$Char ::
sig {
  type Char = System$CharType.Char;
  native (/=) :: Char ->
		 Char ->
		 Bool = "\\x -> \\y -> x /= (y::Char)";
  native (<) :: Char ->
		Char ->
		Bool = "\\x -> \\y -> x < (y::Char)";
  native (<=) :: Char ->
		 Char ->
		 Bool = "\\x -> \\y -> x <= (y::Char)";
  native (==) :: Char ->
		 Char ->
		 Bool = "\\x -> \\y -> x == (y::Char)";
  native (>) :: Char ->
		Char ->
		Bool = "\\x -> \\y -> x > (y::Char)";
  native (>=) :: Char ->
		 Char ->
		 Bool = "\\x -> \\y -> x >= (y::Char)";
  native chr :: Int ->
		Char = "\\x -> (toEnum x)::Char";
  native ord :: Char ->
		Int = "\\x -> fromEnum (x::Char)";
  isAlpha :: Char -> Bool;
  isAlphaNum :: Char -> Bool;
  isDigit :: Char -> Bool;
  isLower :: Char -> Bool;
  isSpace :: Char -> Bool;
  isSymbol :: Char -> Bool;
  isUpper :: Char -> Bool;
  show :: Char -> String;
};

CharType

System$CharType ::
sig { type Char; };

Double

System$Double ::
sig {
  native (*) :: Double ->
		Double ->
		Double = "\\x -> \\y -> x*(y::Double)";
  native (+) :: Double ->
		Double ->
		Double = "\\x -> \\y -> x+(y::Double)";
  native (-) :: Double ->
		Double ->
		Double = "\\x -> \\y -> x-(y::Double)";
  native (/) :: Double ->
		Double ->
		Double = "\\x -> \\y -> x/(y::Double)";
  native (/=) :: Double ->
		 Double ->
		 Bool = "\\x -> \\y -> x/=(y::Double)";
  native (<) :: Double ->
		Double ->
		Bool = "\\x -> \\y -> x<(y::Double)";
  native (<=) :: Double ->
		 Double ->
		 Bool = "\\x -> \\y -> x<=(y::Double)";
  native (==) :: Double ->
		 Double ->
		 Bool = "\\x -> \\y -> x==(y::Double)";
  native (>) :: Double ->
		Double ->
		Bool = "\\x -> \\y -> x>(y::Double)";
  native (>=) :: Double ->
		 Double ->
		 Bool = "\\x -> \\y -> x>=(y::Double)";
  negate :: Double -> Double;
  type Double;
  read :: String -> Double;
  show :: Double -> String;
};

Either

System$Either ::
sig {
  data Either a b = Left a | Right b;
  either ::
    (a :: #) |->
    (b :: #) |->
    (c :: #) |->
    (a -> c) ->
    (b -> c) ->
    Either a b ->
    c;
  show ::
    (a :: #) |->
    (b :: #) |->
    (a -> String) ->
    (b -> String) ->
    Either a b ->
    String;
};

Error

System$Error ::
sig {
  type Error (_ :: String);
  ErrorT :: String -> #1;
  type Undefined;
  UndefinedT :: #1;
  error :: (a :: #) |-> String -> a;
  undefined :: (a :: #) |-> a;
};

HO

System$HO ::
sig {
  const :: (a :: #) |-> (b :: #) |-> a -> b -> a;
  curry ::
    (a :: #) |->
    (b :: #) |->
    (c :: #) |->
    (Char a b -> c) ->
    a ->
    b ->
    c;
  flip ::
    (a :: #) |->
    (b :: #) |->
    (c :: #) |->
    (a -> b -> c) ->
    b ->
    a ->
    c;
  id :: (a :: #) |-> a -> a;
  uncurry ::
    (a :: #) |->
    (b :: #) |->
    (c :: #) |->
    (a -> b -> c) ->
    Char a b ->
    c;
  (·) ::
    (a :: #) |->
    (b :: #) |->
    (c :: #) |->
    (b -> c) ->
    (a -> b) ->
    a ->
    c;
};

IO

System$IO ::
sig {
  type FilePath = String;
  data IOMode =
  ReadMode | WriteMode | AppendMode | ReadWriteMode;
  type Handle;
  type IO _;
  type IOError;
  Monad_IO :: System$Monad IO;
  catch :: (a :: #) |-> IO a -> (IOError -> IO a) -> IO a;
  exitWith :: Int -> IO Unit;
  getArgs :: IO (List String);
  getLine :: IO String;
  hClose :: Handle -> IO Unit;
  hGetChar :: Handle -> IO Char;
  hGetContents :: Handle -> IO String;
  hPutChar ::
    Handle -> Char -> IO Unit;
  hPutStr ::
    Handle -> String -> IO Unit;
  interact ::
    (String -> String) ->
    IO Unit;
  ioError :: (a :: #) |-> IOError -> IO a;
  openFile :: FilePath -> IOMode -> IO Handle;
  putStr :: String -> IO Unit;
  putStrLn :: String -> IO Unit;
  readFile :: FilePath -> IO String;
  stderr :: Handle;
  stdin :: Handle;
  stdout :: Handle;
  userError :: String -> IOError;
  writeFile ::
    FilePath -> String -> IO Unit;
};

Id

System$Id ::
let concrete (===) :: (a :: #) |-> a -> a -> # =
	       \ (a :: #) |-> \ (_ :: a) -> \ (_ :: a) -> data refl;
    concrete reflE :: (a :: #) |-> (x :: a) -> (===) |a x x =
	       \ (a :: #) |-> \ (_ :: a) -> refl@(data refl);
sig {
  (===) :: (a :: #) |-> a -> a -> #;
  congr ::
	(a :: #) |->
	(P :: (a -> #)) ->
	(x :: a) ->
	(y :: a) ->
	(===) |a x y ->
	P x ->
	P y;
  ext ::
	(a :: #) |->
	(b :: #) |->
	(f :: (a -> b)) |->
	(g :: (a -> b)) |->
	((x :: a) -> (===) |b (f x) (g x)) ->
	(===) |(a -> b) f g;
  idPeel ::
	(a :: #) |->
	(C :: ((x :: a) -> (y :: a) -> (===) |a x y -> #)) ->
	((x :: a) -> C x x (reflE |a x)) ->
	(x :: a) ->
	(y :: a) ->
	(p :: (===) |a x y) ->
	C x y p;
  refl :: (a :: #) |-> (x :: a) |-> (===) |a x x;
  subst ::
	(a :: #) |->
	(b :: #) |->
	(x :: a) |->
	(y :: a) |->
	(f :: (a -> b)) ->
	(===) |a x y ->
	(===) |b (f x) (f y);
  symm ::
	(a :: #) |->
	(x :: a) |->
	(y :: a) |->
	(===) |a x y ->
	(===) |a y x;
  trans ::
	(a :: #) |->
	(x :: a) |->
	(y :: a) |->
	(z :: a) |->
	(===) |a x y ->
	(===) |a y z ->
	(===) |a x z;
};

Int

System$Int ::
sig {
  native (*) :: Int ->
		Int ->
		Int = "\\x -> \\y -> x * y :: Int";
  native (+) :: Int ->
		Int ->
		Int = "\\x -> \\y -> x + y :: Int";
  native (-) :: Int ->
		Int ->
		Int = "\\x -> \\y -> x - y :: Int";
  native (/=) :: Int ->
		 Int ->
		 Bool = "\\x -> \\y -> x /= (y :: Int)";
  native (<) :: Int ->
		Int ->
		Bool = "\\x -> \\y -> x < (y :: Int)";
  native (<=) :: Int ->
		 Int ->
		 Bool = "\\x -> \\y -> x <= (y :: Int)";
  native (==) :: Int ->
		 Int ->
		 Bool = "\\x -> \\y -> x == (y :: Int)";
  native (>) :: Int ->
		Int ->
		Bool = "\\x -> \\y -> x > (y :: Int)";
  native (>=) :: Int ->
		 Int ->
		 Bool = "\\x -> \\y -> x >= (y :: Int)";
  native even :: Int ->
		 Bool = "\\x -> (x :: Int) `rem` 2 == 0";
  negate :: Int -> Int;
  native odd :: Int ->
		Bool = "\\x -> (x :: Int) `rem` 2 == 1";
  native quot :: Int ->
		 Int ->
		 Int = "\\x -> \\y -> x `quot` y :: Int";
  native rem :: Int ->
		Int ->
		Int = "\\x -> \\y -> x `rem` y :: Int";
  type Int;
  read :: String -> Int;
  show :: Int -> String;
};

Integer

System$Integer ::
sig {
  type Integer;
  (*) :: Integer -> Integer -> Integer;
  (+) :: Integer -> Integer -> Integer;
  (-) :: Integer -> Integer -> Integer;
  (/=) :: Integer -> Integer -> Bool;
  (<) :: Integer -> Integer -> Bool;
  (<=) :: Integer -> Integer -> Bool;
  (==) :: Integer -> Integer -> Bool;
  (>) :: Integer -> Integer -> Bool;
  (>=) :: Integer -> Integer -> Bool;
  even :: Integer -> Bool;
  negate :: Integer -> Integer;
  odd :: Integer -> Bool;
  quot :: Integer -> Integer -> Integer;
  read :: String -> Integer;
  rem :: Integer -> Integer -> Integer;
  show :: Integer -> String;
};

List

System$List ::
sig {
  data List a = Nil | (:) a (List a);
  (++) :: (a :: #) |-> List a -> List a -> List a;
  Monad_List :: System$Monad List;
  concat :: (a :: #) |-> List (List a) -> List a;
  drop :: (a :: #) |-> Int -> List a -> List a;
  elem ::
	(a :: #) |->
	(a -> a -> Bool) ->
	a ->
	List a ->
	Bool;
  equal ::
	(a :: #) |->
	(a -> a -> Bool) ->
	List a ->
	List a ->
	Bool;
  filter ::
	(a :: #) |-> (a -> Bool) -> List a -> List a;
  foldr ::
	(a :: #) |-> (b :: #) |-> (a -> b -> b) -> b -> List a -> b;
  head :: (a :: #) |-> List a -> a;
  intersperse :: (a :: #) |-> a -> List a -> List a;
  length :: (a :: #) |-> List a -> Int;
  map ::
	(a :: #) |-> (b :: #) |-> (a -> b) -> List a -> List b;
  null :: (a :: #) |-> List a -> Bool;
  reverse :: (a :: #) |-> List a -> List a;
  show ::
	(a :: #) |->
	(a -> String) ->
	List a ->
	String;
  tail :: (a :: #) |-> List a -> List a;
  take :: (a :: #) |-> Int -> List a -> List a;
  zip ::
	(a :: #) |->
	(b :: #) |->
	List a ->
	List b ->
	List (Pair a b);
  zipWith ::
	(a :: #) |->
	(b :: #) |->
	(c :: #) |->
	(a -> b -> c) ->
	List a ->
	List b ->
	List c;
};

Logic

System$Logic ::
sig {
  data (/\) a b = (&) a b;
  type (<=>) a b = sig { impL :: b -> a; impR :: a -> b; };
  data Absurd = ;
  type Lift (_10112 :: Bool) =
    case _10112 of {
    (False) ->  Absurd; (True) ->  Truth;
};
  LiftBin ::
    (a :: #) |-> (a -> a -> Bool) -> a -> a -> # =
    \ (a :: #) |->
    \ (op :: (a -> a -> Bool)) ->
    \ (x :: a) -> \ (y :: a) -> Lift (op x y);
  data Truth = truth;
  data (\/) a b = Inl a | Inr b;
  absurd :: (a :: #) |-> Absurd -> a;
};

Maybe

System$Maybe ::
sig {
  data Maybe a = Nothing | Just a;
  Monad_Maybe :: System$Monad Maybe;
  fromJust :: (a :: #) |-> Maybe a -> a;
  maybe ::
    (a :: #) |-> (b :: #) |-> b -> (a -> b) -> Maybe a -> b;
  show ::
    (a :: #) |->
    (a -> String) ->
    Maybe a ->
    String;
};

Monad

System$Monad (m :: (# -> #)) :: #1.0 =
  sig {
    (>>) :: (a :: #) |-> (b :: #) |-> m a -> m b -> m b;
    (>>=) :: (a :: #) |-> (b :: #) |-> m a -> (a -> m b) -> m b;
    return :: (a :: #) |-> a -> m a;
  };

MonadUtil

System$MonadUtil ::
sig {
  Monad :: #1.0 = sig { type m _; o :: System$Monad m; };
  join :: (M :: Monad) -> (a :: #) |-> M.m (M.m a) -> M.m a;
};

Nat

System$Nat ::
let concrete False :: Bool = System$Bool.False;
    concrete True :: Bool = System$Bool.True;
sig {
  data Nat = Zero | Succ Nat;
  (+) (_10097 :: Nat) (m :: Nat) :: Nat =
	case _10097 of {
	(Succ n) ->  Succ ((+) n m); (Zero) ->  m;
	};
  (==) (_10103 :: Nat) (_10104 :: Nat) :: Bool =
	case _10103 of {
	(Succ n) -> 
	  case _10104 of {
	  (Succ m) ->  (==) n m; _ ->  False;
	  };
	(Zero) -> 
	  case _10104 of {
	  (Zero) ->  True; _ ->  False;
	  };
	};
  fromInteger :: System$Integer.Integer -> Nat;
  toInt :: Nat -> Int;
  toInteger :: Nat -> System$Integer.Integer;
};

Num

System$Num ::
let concrete Zero :: System$Nat.Nat = System$Nat.Zero;
    concrete Succ :: System$Nat.Nat -> System$Nat.Nat =
	       System$Nat.Succ;
sig {
  data Num = NonNeg System$Nat.Nat | Neg System$Nat.Nat;
  minusone ::
	data NonNeg System$Nat.Nat | Neg System$Nat.Nat =
	neg one;
  minustwo ::
	data NonNeg System$Nat.Nat | Neg System$Nat.Nat =
	neg two;
  one :: data NonNeg System$Nat.Nat | Neg System$Nat.Nat =
	succ zero;
  two :: data NonNeg System$Nat.Nat | Neg System$Nat.Nat =
	succ one;
  zero :: data NonNeg System$Nat.Nat | Neg System$Nat.Nat =
	NonNeg Zero;
  (+) (_11370 :: Num) (_11371 :: Num) :: Num =
	case _11370 of {
	(Neg n) -> 
	  case _11371 of {
	  (Neg m) ->  Neg (System$Nat.(+) (Succ n) (Succ m));
	  (NonNeg m) ->  sub m (Succ n);
	  };
	(NonNeg n) -> 
	  case _11371 of {
	  (Neg m) ->  sub n (Succ m);
	  (NonNeg m) ->  NonNeg (System$Nat.(+) n m);
	  };
	};
  (-) (_12823 :: Num) (_12824 :: Num) :: Num =
	case _12823 of {
	(Neg n) -> 
	  case _12824 of {
	  (Neg m) ->  sub (Succ m) (Succ n);
	  (NonNeg m) ->  Neg (System$Nat.(+) (Succ n) m);
	  };
	(NonNeg n) -> 
	  case _12824 of {
	  (Neg m) ->  NonNeg (System$Nat.(+) n (Succ m));
	  (NonNeg m) ->  sub n m;
	  };
	};
  neg (n :: Num) :: Num =
	case n of {
	(Neg n) ->  NonNeg (Succ n);
	(NonNeg _14478) -> 
	  case _14478 of {
	  (Succ n) ->  Neg n; _ ->  n;
	  };
	};
  sub (_10640 :: System$Nat.Nat) (_10641 :: System$Nat.Nat) ::
	Num =
	case _10640 of {
	(Succ n) -> 
	  case _10641 of {
	  (Succ m) ->  sub n m; (Zero) ->  NonNeg (Succ n);
	  };
	(Zero) -> 
	  case _10641 of {
	  (Succ n) ->  Neg n; (Zero) ->  NonNeg Zero;
	  };
	};
  succ :: Num -> Num = (+) (NonNeg (Succ Zero));
  toInt :: Num -> Int;
};

String

System$String ::
let type List a = data Nil | (:) a (List a);
sig { type String = List System$CharType.Char; };

StringUtil

System$StringUtil ::
sig {
  (==) ::
    String ->
    String ->
    Bool;
};

Trace

The System$Trace module contains a side effecting function that prints its first argument and returns the second. It is intended for debugging. 
System$Trace ::
sig {
  trace :: (a :: #) |-> String -> a -> a;
};

Tuples

System$Tuples ::
sig {
  data Pair a b = (,) a b;
  fst :: (a :: #) |-> (b :: #) |-> Pair a b -> a;
  show ::
    (a :: #) |->
    (b :: #) |->
    (a -> String) ->
    (b -> String) ->
    Pair a b ->
    String;
  snd :: (a :: #) |-> (b :: #) |-> Pair a b -> b;
};

Unit

System$Unit ::
sig {
  data Unit = unit; show :: Unit -> String;
};

Void

System$Void ::
sig { type Void; void :: (a :: #) |-> Void -> a; };

Back

Lennart Augustsson
Last modified: Thu Aug 25 23:11:51 CEST 2005