Abhiroop

import Data.List (group)

type TimedWord v = [(Int, v)]


ex1 :: TimedWord Float
ex1 = [(1,3.4),(3,2.1),(3,1.9),(5,6.3)]

-- 1
reps :: Int -> [(Int, v)] -> Int

Abhiroop

_++_ : ∀ {A : Set} → List A → List A → List A
[]       ++ ys  =  ys
(x ∷ xs) ++ ys  =  x ∷ (xs ++ ys)

length : ∀ {A : Set} → List A → ℕ
length [] = 0
length (x ∷ xs) = 1 + length xs

length-lemma : ∀ {A : Set} → (xs ys : List A) →
  length (xs ++ ys) ≡ length xs + length ys  -- the theorem to be proven

Abhiroop

import Prelude hiding (last, (!!), map, id)

{-@ Induction examples from slide @-}

data Foo a = Nil | Cons  a (Foo a)
--    ^       ^    ^
--    |       |    |
--   type    data constructor
--  constructor

Abhiroop

module Ex3 where

import Prelude hiding (last, (!!), map, id)

{-@ Induction examples from slide @-}

data Foo a = Nil | Cons  a (Foo a)
--    ^       ^    ^
--    |       |    |
--   type    data constructor

Abhiroop

-- A.hs

module A where

class Foo a where
  foo :: a -> Bool

data X = X Int

-- B.hs

Abhiroop

CFLAGS = -Wall -Wextra

ifeq ($(DEBUG),1)
GRAMINE_LOG_LEVEL = debug
CFLAGS += -g
else
GRAMINE_LOG_LEVEL = error
CFLAGS += -O3
endif

Abhiroop

# Hello World manifest file example

loader.entrypoint = "file:{{ gramine.libos }}"
libos.entrypoint = "/helloworld"
loader.log_level = "{{ log_level }}"

loader.env.LD_LIBRARY_PATH = "/lib:/lib/x86_64-linux-gnu"

fs.mounts = [
  { path = "/lib", uri = "file:{{ gramine.runtimedir() }}" },

Abhiroop

#include<HsFFI.h>
.
.
static void my_enter(void) __attribute__((constructor));
static void my_enter(void)
{
  static char *argv[] = { "libFoo.so", 0 }, **argv_ = argv;
  static int argc = 1;
  hs_init(&argc, &argv_);
}

Abhiroop

aaaa

Abhiroop

#include <zephyr.h>
#include <device.h>
#include <drivers/gpio.h>
#include <sys/util.h>
#include <sys/printk.h>
#include <inttypes.h>

#define SLEEP_TIME_MS	1