Mesabloo Mesabloo

## #Typechecker for QTT
This gist contains an implementation for a typechecker for Quantitative Type Theory (QTT), in Isabelle/HOL.

## #Closure Conversion and monomorphisation for QDTLC
Closure conversion and monomorphisation by type erasure implemented on a Quantitative Dependently Typed Lambda Calculus.

## #Typechecker for QDTLC
A small typechecker using normalization by evaluation (NbE) for a Quantitative Dependently Typed Lambda Calculus (QDTLC).

## README.md

      
              2 files
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                Mesabloo
                / README.md
            
            
              Last active
              June 2, 2022 15:00
            
              
                A very simple VM (as a stack script) for a small concatenative programming language which aims to be as performant as possible.
              
          
    Yes, this is very ugly.
However, I managed to squeeze so much out of the original code, and make it really fast (though this could be even better).
I think I might have gotten to the point where I cannot really make it go faster, but for a basic VM, I think this is bloody good as it is.

  
## Makefile
.DEFAULT: main.ice
ifdef tool
		silice-make.py -s main.ice -b $@ -p basic,pmod -o BUILD_$(subst :,_,$@) -t $(tool)
else
		silice-make.py -s main.ice -b $@ -p basic,pmod -o BUILD_$(subst :,_,$@)
endif

clean:
	rm -rf BUILD_*

## micro-interpreter.js
/**
----------------------------------------------------------------
// Interpreter callstack
type CallStack = { vars: { name: string, value: Value }[] }[]
----------------------------------------------------------------
// A runtime value
type Value = Integer | Function | PrimFunction
type Integer = { type: 'Integer', value: int }
type Function = { type: 'Function', args: string[], block: ASTBlock }
type PrimFunction = { type: 'PrimFunction', val: (Value...) => Value }

## Variadic.hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeOperators #-}

## Test.hs
{-| Exercise:

- Step 1:

Write a program simulating an iterating machine: we for example feed a range
  @[0..4]@ and an action @print@ and it must execute this action on all the
  elements of the range.

Writing @iterate1 [4..9] print@ must output:
  > 4

## main.py
from discord.ext import commands
import discord
import sqlite3

prefix = '#!'
client = commands.Bot(command_prefix=prefix)

print('Connecting to database...')
conn = sqlite3.connect('categories.db')
c = conn.cursor()

## LAM.hs
-- The linear abstract machine
-- as described in the "The Linear Abstract Machine"

-- Environment is a representation of a canonical combinator
-- the canonical combinator u ⊗ v is represented by Ja, and 1 by Nil
-- the canonical combinator y ∘ v represented by Comb: y is piece of code.
--
-- Code is list of primitive instructions.
--
-- Sequential composition becomes concatenation (in opposite order),
	.DEFAULT: main.ice
	ifdef tool
	silice-make.py -s main.ice -b $@ -p basic,pmod -o BUILD_$(subst :,_,$@) -t $(tool)
	else
	silice-make.py -s main.ice -b $@ -p basic,pmod -o BUILD_$(subst :,_,$@)
	endif

	clean:
	rm -rf BUILD_*
	/**
	----------------------------------------------------------------
	// Interpreter callstack
	type CallStack = { vars: { name: string, value: Value }[] }[]
	----------------------------------------------------------------
	// A runtime value
	type Value = Integer \| Function \| PrimFunction
	type Integer = { type: 'Integer', value: int }
	type Function = { type: 'Function', args: string[], block: ASTBlock }
	type PrimFunction = { type: 'PrimFunction', val: (Value...) => Value }
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE ConstraintKinds #-}
	{-# LANGUAGE KindSignatures #-}
	{-# LANGUAGE NoStarIsType #-}
	{-# LANGUAGE TypeApplications #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE RecordWildCards #-}
	{-# LANGUAGE TypeOperators #-}
	{-\| Exercise:

	- Step 1:

	Write a program simulating an iterating machine: we for example feed a range
	@[0..4]@ and an action @print@ and it must execute this action on all the
	elements of the range.

	Writing @iterate1 [4..9] print@ must output:
	> 4
	from discord.ext import commands
	import discord
	import sqlite3

	prefix = '#!'
	client = commands.Bot(command_prefix=prefix)

	print('Connecting to database...')
	conn = sqlite3.connect('categories.db')
	c = conn.cursor()
	-- The linear abstract machine
	-- as described in the "The Linear Abstract Machine"

	-- Environment is a representation of a canonical combinator
	-- the canonical combinator u ⊗ v is represented by Ja, and 1 by Nil
	-- the canonical combinator y ∘ v represented by Comb: y is piece of code.
	--
	-- Code is list of primitive instructions.
	--
	-- Sequential composition becomes concatenation (in opposite order),