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)

jfdm

def xs : (List Nat) :=
  (extend 1
          (extend 2
                  empty[Nat]))

def myAdd : (Nat -> (Nat -> Nat))
  := (fun x : Nat, y : Nat => (add x y))


def rec foldr : ((Nat -> (Nat -> Nat)) -> (Nat -> ((List Nat) -> Nat)))