prozacchiwawa

<?xml version="1.0" standalone="no"?>
<!DOCTYPE chapter SYSTEM "minidocbook.dtd">

<chapter id="tdfc2-grammar-and-data-structure-notes">
    <title>TDFC2: Working with the grammars and data structures to support new C99 features</title>

    <section>
        <title>Tools involved in adding C99 features</title>

        <table>

prozacchiwawa

diff --git a/tdfc2/src/common/construct/initialise.c b/tdfc2/src/common/construct/initialise.c
index 4af7a0e0f..9a0c33ed8 100644
--- a/tdfc2/src/common/construct/initialise.c
+++ b/tdfc2/src/common/construct/initialise.c
@@ -6,9 +6,11 @@
  */
 
 #include <stdio.h>
+#include <string.h>
 

prozacchiwawa

module GLFW
-- https://gist.github.com/alrunner4/8a026f3bfea354b48d3294a20c9812e2

export data Monitor : Type where {}
export data Window  : Type where {}

%foreign "C:glfwInit,libglfw"
Init: PrimIO Int

%foreign "C:glfwCreateWindow,libglfw"

prozacchiwawa

data SignedNat : Bool -> Nat -> Type where
  Neg : (n:Nat) -> SignedNat True n
  Pos : (n:Nat) -> SignedNat False n

interface MagnitudeSN sn where
  magSN : sn -> Nat

implementation MagnitudeSN (SignedNat True Z) where
  magSN _ = Z

prozacchiwawa

data SignedNat : Bool -> Nat -> Type where
  Neg : (n:Nat) -> SignedNat True n
  Pos : (n:Nat) -> SignedNat False n

data Memory : sna -> mem -> Type where
  MWord : sna -> mem -> Memory sna mem
  MEnd : sna -> Memory sna Void

data MemoryAddress : Nat -> Type where
  MAddr : (n:Nat) -> MemoryAddress n

prozacchiwawa

import sys

def shiftout(fout, bs):
    for b in bs:
        bb = b
        for i in range(8):
            if (bb >> 7) % 2 == 0:
                fout.write(bytes([255]))
            else:
                fout.write(bytes([0]))

prozacchiwawa

;;; mood-dark-theme.el - Coding palette based on atari 2600 colors. based on the following
;; emacs theme:

;; spacemax-common.el --- Color theme with a dark and light versions.

;; Copyright (C) 2019 Michael Camilleri

;; Author: Michael Camilleri
;; URL: <https://github.com/pyrmont/spacemax-theme>
;;

prozacchiwawa

import xml.dom.minidom
import sys

def traverse(e,o):
    oldwhere = None
    useo = dict(o.items())

    if e.nodeType == e.TEXT_NODE:
        return

prozacchiwawa

module DecBool

-- Given a contra on bool equality (a = b) -> Void, produce a proof of the opposite (that (not a) = b)
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool a b contra = invertContraBool_ a b contra
  where
    fEf : False = False
    fEf = Refl

prozacchiwawa

module F1

import System
import Data.Bool
import Data.List
import Data.Vect
import Decidable.Equality

data Fruit = Apple | Banana