This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 ")" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
internal interface I | |
{ | |
int Foo(int i); | |
} | |
internal class B | |
{ | |
public int TestFunc(int i) | |
{ | |
return 1; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import java.util.Random; | |
public class Main | |
{ | |
private static void doThing(int[] param, int x, int y) | |
{ | |
if (x >= y) | |
return; | |
int i = x; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
f :: [(a,a)] -> [[a]] | |
f [] = [] | |
f (x:xs) = (snd x : fst (unzip xs)): map (fst x :) (f xs) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#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) | |
{ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |