MarcusVoelker

Require Import Ensembles.
Require Import Setoid.

Definition map {A B : Type} (f : A -> B) (S : Ensemble A) :=
  fun b => exists a, In A S a /\ f a = b.

Section lat.

Variable A : Type.
Variable leA : A -> A -> Prop.

MarcusVoelker

module W where

import qualified Data.Map.Strict as M
import Control.Monad.State.Lazy

data LExpr = Var String | App LExpr LExpr | Abs String LExpr | Let String LExpr LExpr

instance Show LExpr where
    show (Var s) = s
    show (App l r) = "(" ++ show l ++ ")(" ++ show r ++ show ")"

MarcusVoelker

module Main where

import Data.List

data CTL a = AG (CTL a) | AF (CTL a) | EG (CTL a) | EF (CTL a) | EU (CTL a) (CTL a) | AU (CTL a) (CTL a) | EX (CTL a) | AX (CTL a) | And (CTL a) (CTL a) | Or (CTL a) (CTL a) | Not (CTL a) | Atom a

data Kripke a = Kripke { t :: (Int -> [Int]), l :: (Int -> [a]) }

paths :: Kripke a -> Int -> [[Int]]
paths m s = paths' [] m s

MarcusVoelker

module ToDot where

import Data.Map

generateDot :: (Ord a, Show a) => Map a [a] -> IO ()
generateDot mp = do
	putStrLn "graph G {"
	foldrWithKey (\k v r ->
		putStrLn ("  v" ++ show k) >> Prelude.foldr (\e r' -> r' >> when (k < e) (putStrLn ("  v" ++ show k ++ " -- v" ++ show e))) 
			r v

MarcusVoelker

internal interface I
{
    int Foo(int i);
}

internal class B
{
    public int TestFunc(int i)
    {
        return 1;

MarcusVoelker

import java.util.Random;

public class Main
{
  private static void doThing(int[] param, int x, int y)
  {
    if (x >= y)
      return;
    
    int i = x;

MarcusVoelker

f :: [(a,a)] -> [[a]]
f [] = []
f (x:xs) = (snd x : fst (unzip xs)): map (fst x :) (f xs)

MarcusVoelker

#include <iostream>

const unsigned long long SEC = 1000L*1000L*1000L;

inline unsigned long long timespecTo64( const timespec &_time ) {
    return ( _time.tv_sec*SEC + _time.tv_nsec );
}

void runTest(clockid_t clkid, std::string const& name)
{

MarcusVoelker

module Main where

data SK = S | K | App SK SK deriving Eq

data CC = CCAtom Combinator | CCApp CC CC

data Combinator = Comb String SK deriving Eq

data BaseCombinator = BC String CC