useronym

open import Size

mutual
  data Delay (A : Set) (i : Size) : Set where
    now   : A → Delay A i
    later : ∞Delay A i → Delay A i

  record ∞Delay (A : Set) (i : Size) : Set where
    coinductive
    field

useronym

data Path {A : Set} (R : A → A → Set) : A → A → Set where
  ∅    : ∀ {a} → Path R a a
  _>>_ : ∀ {a b c} → R a b → Path R b c → Path R a c
infixr 5 _>>_

_>|_ : ∀ {R a b c} → R a b → R b c → Path R a c
a >| b = a >> b >> ∅

useronym

open import Data.List using (List; _∷_; []; [_]; reverse)
open import Data.String using (String; toList; fromList)
open import Category.Monad.State


data _∈_ {A : Set} : A → List A → Set where
  here  : ∀ {a xs} → a ∈ (a ∷ xs)
  there : ∀ {a b xs} → a ∈ xs → a ∈ (b ∷ xs)
infix 7 _∈_

useronym

open import Data.String


record Print (A : Set) : Set where
  field
    print : A → String
open Print {{…}} public

mutual
  data α : Set where

useronym

module Erlang.Print where
open import Erlang.Syntax
open import Function
open import Data.Nat renaming (ℕ to Nat)
open import Data.Integer renaming (ℤ to Int)
open import Data.Float
open import Data.Char
open import Data.String
open import Data.List

useronym

(defmacro tupleize-record (rec-name)
  `(lambda (rec)
     ,(lists:map (lambda (field-name)
                   (tuple field-name (rec-get rec-name field-name)))
                 (rec-fields rec-name))))

(defmacro rec-fields (name)
  `(,(ltoa (++ "fields-" (atol name)))))

(defmacro rec-get (name field)

useronym

(defmacro make-record (name)
  `(lambda (rec)
     (lists:zip ,(rec-fields name)
                (lists:map (lambda (rec-field) (funcall ,(rec-get name rec-field) rec
                                                        ,(rec-fields name)))))))

(defmacro rec-fields (name)
  `(,(ltoa (++ "fields-" (atol name)))))

(defmacro rec-get (name field)

useronym

(defun handle_ssh_msg
  (((tuple 'ssh_cm conn-ref
           (tuple 'pty chan-id want-reply
                  (tuple term width height _ _ modes)))
    state)
   (progn (if want-reply
            (ssh_connection:reply_request conn-ref 'false 'success chan-id))
          (tuple 'ok state)))
  (((tuple 'ssh_cm conn-ref
           (tuple 'shell chan-id want-reply)))

useronym

(defmodule rec 
  (export-macro make-myrec myrec-a myrec-b))

(defrecord myrec
  a
  b)

useronym

open import Data.Empty

-- Intuition: We have objects (Struct) which consist of a bunch of fields (Atomic)
-- which can be in different states (state).

record Struct : Set₁ where
  field
    Atomic : Set
    State  : Atomic → Set
open Struct