jfdm

#!/bin/env bash

test ! -z $1 && set -x # Show commands if first arg is non-zero

mkdir -p build/html

katla_run()
{
    KATLA_EXE=$(which katla)
    test -x KATLA_EXE && echo "Katla not installed"

jfdm

role Alice
role Bob

type foo = String

protocol pingpong = Alice ==> Bob   { ping(String)
                  . Bob   ==> Alice { pong(String)
                  . end }}

main()

jfdm

module Versioned

import Data.List.Elem
import Data.List.Quantifiers
import Data.Nat

%default total

data Ty
  = TyNat

jfdm

||| #+TITLE: Dependently Typed Functional Programming
||| #+AUTHOR: Jan de Muijnck-Hughes
||| #+DATE: FATA Seminar 22/23
||| #+STARTUP: noindent overview

module FATA

%default total

-- # Abstract

jfdm

module ConsNeg

import Data.Nat

%default total

namespace PosNeg

  public export
  data Truth : Type where

jfdm

module Example

import Ola

public export
example : Prog Nil Nil UNIT
example
  = DefType TyStr
  $ DefFunc (TyFunc TyUnit (TyVar Here))
            (Fun (Return (S "Hello World")

jfdm

Idris 0.5.1-8bd5ca949

1/1: Building Temp (Temp.idr)
λΠ> fst (snd example)
G [3, 2, 1, 1, 2, 1, 3] [(2, 1), (3, 1)]
λΠ> example
MkDPair 3 (MkDPair (G [3, 2, 1, 1, 2, 1, 3] [(2, 1),
                                             (3,
                                             1)]) (Port LOGIC OUT (Port LOGIC IN (Port LOGIC IN (GDecl (Gate (Var (There (There Here))) (Var (There Here)) (Var Here)) Stop)))))
λΠ> :t example

jfdm

λΠ> show EmployeeSchema
"(Employee (PersonInfo ((FullName ((Firstname : String is not restricted) <+> 
                                  ((Lastname : String is not restricted) <+> {}))) <+> 
                       (((Address : String is not restricted) 
                          <|> 
                        ((FirstLine : String is not restricted) <+> 
                        ((City : String is not restricted) <+> 
                        ((Country : String is restricted) <+> 
                        ((PostCode : String is not restricted) <+> {}))))) <+> 
                       {}))))"

jfdm

module a
(
  output logic clk,
  output logic rst
);
// TO ADD
endmodule;

module b
(

jfdm

module Examples

import Decidable.Equality

data Foo = F String Nat

namespace Beginner
  export
  decEq : (x,y : Foo) -> Dec (x = y)
  decEq (F xs xn) (F ys yn) with (decEq xs ys)