nyuichi

#!/usr/local/Gambit-C/bin/gsi

; Copyright (C) 2004 by Marc Feeley, All Rights Reserved.

; This is the "90 minute Scheme to C compiler" presented at the
; Montreal Scheme/Lisp User Group on October 20, 2004.

; Usage with Gambit-C 4.0:
;
;    % ./90-min-scc.scm test.scm

nyuichi

;;; List Monad

(defmethod bind ((m list) f)
  (apply #'append (mapcar f m)))

(defmethod fmap ((m list) f)
  (mapcar f m))

nyuichi

// the characteristic of the diagonal mono δ : α → α × α
constant eq : α → α → Prop

infix = : 50 := eq

// This is definitionally equal to any term of the Unit type by the eta rule.
constant star : Unit

/-
This introduces a constant `top` and:

nyuichi

;;;; **deep binding**


;;; look up
(cdr (assq 'the-symbol *the-stack*))


;;; funcall
; wind...
(loop for arg  in args

nyuichi

The make command hangs up when it is run as init (PID=1) and its child processes are terminated with SIGINT

$ ls
loop.sh  Makefile  run-loop.sh
$ cat loop.sh 
#!/bin/bash
trap 'echo SIGTERM && exit 0' SIGTERM
trap 'echo SIGINT && exit 0' SIGINT
while true; do :; done

nyuichi

! [Type Error] at "bug.saty", line 11, character 0 to line 15, character 3:
    The implementation of value 'make' has type
      ('a phantom) M.t
    which is inconsistent with the type required by the signature
      ('#a phantom) M.t

nyuichi

; -*- mode: scheme;-*-
; Implementation of resolution principle for first-order logic in Egison

(define $unordered-pair
 (lambda [$m]
  (matcher
    {[<pair $ $> [m m] {[[$x $y] {[x y] [y x]}]}]
     [$ [something] {[$tgt {tgt}]}]})))

(define $positive?

nyuichi

(use r7rs)

(define uniq
  (let ((n 0))
    (lambda ()
      (set! n (+ n 1))
      (string->symbol (string-append "$" (number->string n))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; - Operational aspects of untyped normalization by evaluation, K. Aehlig et al, MSCS 2003.

nyuichi

import data.set
open function

universes u
variables {α β γ : Type u} 

noncomputable def bijective_inv (f : α → β) (h : bijective f) (b : β) : α :=
classical.some (h.right b)

lemma bijective_inv_spec (f : α → β) (h : bijective f) (b : β) : f (bijective_inv f h b) = b :=

nyuichi

open eq

section eckmann_hilton
  universe variables u
  parameter {α : Type u}
  parameters plus mult : α → α → α
  parameters one zero : α
  local notation a + b := plus a b
  local notation a * b := mult a b