foewhfuoewhow
parent
079cc4bc3c
commit
994212b3f3
Binary file not shown.
@ -0,0 +1,32 @@
|
|||||||
|
|
||||||
|
subprojects = $(patsubst examples/%, %, $(wildcard examples/*))
|
||||||
|
|
||||||
|
.PHONY: usage
|
||||||
|
usage:
|
||||||
|
@printf "Found the following subprojects:\n"
|
||||||
|
@for project in $(subprojects); do printf " - %s\n" $$project; done
|
||||||
|
@printf "\n"
|
||||||
|
@printf "Available rules\n"
|
||||||
|
@printf " - run-<name>: Will run the program\n"
|
||||||
|
@printf " - compile-<name>: Will compile the program\n"
|
||||||
|
@printf " - compile-noinline-<name>: Will compile the program without inlining\n"
|
||||||
|
@printf " - decomp-<name>: Will run lensm on the project\n"
|
||||||
|
@printf " - decomp-noinline-<name>: Will run lensm on the project without inlining\n"
|
||||||
|
@printf "\n"
|
||||||
|
|
||||||
|
run-%: FORCE
|
||||||
|
go run -v ./examples/$*
|
||||||
|
|
||||||
|
compile-%: FORCE
|
||||||
|
go build -v -o "./bin/$*" ./examples/$*
|
||||||
|
|
||||||
|
compile-noinline-%: FORCE
|
||||||
|
go build -v -o "./bin/$*@no-inline" -gcflags=-l ./examples/$*
|
||||||
|
|
||||||
|
decomp-%: compile-% FORCE
|
||||||
|
lensm -text-size 16 -filter main "./bin/$*"
|
||||||
|
|
||||||
|
decomp-noinline-%: compile-noinline-% FORCE
|
||||||
|
lensm -text-size 16 -filter main "./bin/$*@no-inline"
|
||||||
|
|
||||||
|
FORCE: ;
|
Binary file not shown.
@ -1,31 +0,0 @@
|
|||||||
package main
|
|
||||||
|
|
||||||
import (
|
|
||||||
"fmt"
|
|
||||||
|
|
||||||
"golang.org/x/exp/constraints"
|
|
||||||
)
|
|
||||||
|
|
||||||
func Min[T constraints.Ordered](x, y T) T {
|
|
||||||
if x < y {
|
|
||||||
return x
|
|
||||||
}
|
|
||||||
return y
|
|
||||||
}
|
|
||||||
|
|
||||||
type Liter int
|
|
||||||
|
|
||||||
func main() {
|
|
||||||
{
|
|
||||||
var a, b int = 1, 2
|
|
||||||
fmt.Println(Min(a, b))
|
|
||||||
}
|
|
||||||
{
|
|
||||||
var a, b float64 = 3.14, 2.71
|
|
||||||
fmt.Println(Min(a, b))
|
|
||||||
}
|
|
||||||
{
|
|
||||||
var a, b Liter = 1, 2
|
|
||||||
fmt.Println(Min(a, b))
|
|
||||||
}
|
|
||||||
}
|
|
@ -0,0 +1,83 @@
|
|||||||
|
package main
|
||||||
|
|
||||||
|
import (
|
||||||
|
"fmt"
|
||||||
|
|
||||||
|
"golang.org/x/exp/constraints"
|
||||||
|
)
|
||||||
|
|
||||||
|
// before go generics
|
||||||
|
|
||||||
|
func MinInt8(x, y int8) int8 {
|
||||||
|
if x < y {
|
||||||
|
return x
|
||||||
|
}
|
||||||
|
|
||||||
|
return y
|
||||||
|
}
|
||||||
|
|
||||||
|
func MinInt16(x, y int16) int16 {
|
||||||
|
if x < y {
|
||||||
|
return x
|
||||||
|
}
|
||||||
|
|
||||||
|
return y
|
||||||
|
}
|
||||||
|
|
||||||
|
func MinInt32(x, y int32) int32 {
|
||||||
|
if x < y {
|
||||||
|
return x
|
||||||
|
}
|
||||||
|
|
||||||
|
return y
|
||||||
|
}
|
||||||
|
|
||||||
|
func MinInt64(x, y int64) int64 {
|
||||||
|
if x < y {
|
||||||
|
return x
|
||||||
|
}
|
||||||
|
|
||||||
|
return y
|
||||||
|
}
|
||||||
|
|
||||||
|
func MinFloat32(x, y float32) float32 {
|
||||||
|
if x < y {
|
||||||
|
return x
|
||||||
|
}
|
||||||
|
|
||||||
|
return y
|
||||||
|
}
|
||||||
|
|
||||||
|
func MinFloat64(x, y float64) float64 {
|
||||||
|
if x < y {
|
||||||
|
return x
|
||||||
|
}
|
||||||
|
|
||||||
|
return y
|
||||||
|
}
|
||||||
|
|
||||||
|
// with go generics
|
||||||
|
|
||||||
|
func Min[T constraints.Ordered](x, y T) T {
|
||||||
|
if x < y {
|
||||||
|
return x
|
||||||
|
}
|
||||||
|
return y
|
||||||
|
}
|
||||||
|
|
||||||
|
type Liter int
|
||||||
|
|
||||||
|
func main() {
|
||||||
|
{
|
||||||
|
var a, b int = 1, 2
|
||||||
|
fmt.Println(Min(a, b))
|
||||||
|
}
|
||||||
|
{
|
||||||
|
var a, b float64 = 3.14, 2.71
|
||||||
|
fmt.Println(Min(a, b))
|
||||||
|
}
|
||||||
|
{
|
||||||
|
var a, b Liter = 1, 2
|
||||||
|
fmt.Println(Min(a, b))
|
||||||
|
}
|
||||||
|
}
|
@ -0,0 +1,87 @@
|
|||||||
|
package main
|
||||||
|
|
||||||
|
//
|
||||||
|
// Encoding the semantics
|
||||||
|
//
|
||||||
|
|
||||||
|
type Bool interface{ isBool() }
|
||||||
|
|
||||||
|
type Term interface{ isTerm() }
|
||||||
|
|
||||||
|
type Term2Term interface{ isTerm2Term() }
|
||||||
|
|
||||||
|
// trick to encode higher-kinded types
|
||||||
|
type V[H Term2Term, T Term] Term
|
||||||
|
|
||||||
|
//
|
||||||
|
// Naturals
|
||||||
|
//
|
||||||
|
|
||||||
|
type Zero Term
|
||||||
|
type Succ Term2Term
|
||||||
|
|
||||||
|
// Some aliases
|
||||||
|
|
||||||
|
type One = V[Succ, Zero]
|
||||||
|
type Two = V[Succ, V[Succ, Zero]]
|
||||||
|
type Three = V[Succ, V[Succ, V[Succ, Zero]]]
|
||||||
|
|
||||||
|
//
|
||||||
|
// Equality
|
||||||
|
//
|
||||||
|
|
||||||
|
type Eq[A, B any] Bool
|
||||||
|
|
||||||
|
// Eq_Refl ~> forall x : x = x
|
||||||
|
func Eq_Reflexive[T any]() Eq[T, T] { panic("axiom") }
|
||||||
|
|
||||||
|
// Eq_Symmetric ~> forall a, b: a = b => b = a
|
||||||
|
func Eq_Symmetric[A, B any](_ Eq[A, B]) Eq[B, A] { panic("axiom") }
|
||||||
|
|
||||||
|
// Eq_Transitive ~> forall a, b, c: a = b e b = c => a = c
|
||||||
|
func Eq_Transitive[A, B, C any](_ Eq[A, B], _ Eq[B, C]) Eq[A, C] { panic("axiom") }
|
||||||
|
|
||||||
|
// Function_Eq ~> forall f function, forall a, b terms: a = b => f(a) = f(b)
|
||||||
|
func Function_Eq[F Term2Term, A, B Term](_ Eq[A, B]) Eq[V[F, A], V[F, B]] {
|
||||||
|
panic("axiom")
|
||||||
|
}
|
||||||
|
|
||||||
|
//
|
||||||
|
// Plus Axioms
|
||||||
|
//
|
||||||
|
|
||||||
|
type Plus[L, R Term] Term
|
||||||
|
|
||||||
|
// "a + 0 = a"
|
||||||
|
|
||||||
|
// Plus_Zero ~> forall a, b: a + succ(b) = succ(a + b)
|
||||||
|
func Plus_Zero[N Term]() Eq[Plus[N, Zero], N] { panic("axiom") }
|
||||||
|
|
||||||
|
// "a + (b + 1) = (a + b) + 1"
|
||||||
|
|
||||||
|
// Plus_Sum ~> forall a, b: a + succ(b) = succ(a + b)
|
||||||
|
func Plus_Sum[N, M Term]() Eq[Plus[N, V[Succ, M]], V[Succ, Plus[N, M]]] { panic("axiom") }
|
||||||
|
|
||||||
|
//
|
||||||
|
// 1 + 1 = 2
|
||||||
|
//
|
||||||
|
|
||||||
|
// Theorem_OnePlusOneEqTwo
|
||||||
|
func Theorem_OnePlusOneEqTwo() Eq[Plus[One, One], Two] {
|
||||||
|
var en1 Eq[
|
||||||
|
Plus[One, Zero],
|
||||||
|
One,
|
||||||
|
] = Plus_Zero[One]()
|
||||||
|
|
||||||
|
var en2 Eq[
|
||||||
|
V[Succ, Plus[One, Zero]],
|
||||||
|
Two,
|
||||||
|
] = Function_Eq[Succ](en1)
|
||||||
|
|
||||||
|
var en3 Eq[
|
||||||
|
Plus[One, One],
|
||||||
|
V[Succ, Plus[One, Zero]],
|
||||||
|
] = Plus_Sum[One, Zero]()
|
||||||
|
|
||||||
|
return Eq_Transitive(en3, en2)
|
||||||
|
}
|
Loading…
Reference in New Issue