fetburner

(* 命題論理式 *)
datatype prop = PTOP
              | PBOT
              | PVAR of string
              | ~~ of prop
              | /\ of prop * prop
              | \/ of prop * prop
              | --> of prop * prop

infix 5 /\

fetburner

type term =
  | Var of int
  | Abs of term
  | App of term * term

let rec rename r = function
  | Var x -> Var (r x)
  | Abs t -> Abs (rename (function 0 -> 0 | x -> succ @@ r @@ x - 1) t)
  | App (t1, t2) -> App (rename r t1, rename r t2)

fetburner

(fun x y z->Printf.printf y(string_of_format y)z x)"(fun x y z->Printf.printf y(string_of_format y)z x)""int main(){char*x=%S,*y=%S,*z=%S;printf(y,34,y,34,34,z,34,34,x,34);}""(fn q=>fn x=>fn y=>fn z=>print(y^q^y^q^q^z^q^q^x^q))(str(chr 34))%c%s%c%c%s%c%c%s%c"

fetburner

(fun q x y->print_string@@y^q^y^q^q^x^q)(String.make 1(Char.chr 34))"(fun q x y->print_string@@y^q^y^q^q^x^q)(String.make 1(Char.chr 34))""(fn q=>fn x=>fn y=>print(y^q^y^q^q^x^q))(str(chr 34))"

fetburner

Require Import Autosubst.Autosubst.
Require Import Program Omega Relations Sorted.

Hint Constructors clos_refl_trans.

Lemma rt_impl A (R R' : relation A) x y :
  (forall x y, R x y -> R' x y) ->
  clos_refl_trans A R x y ->
  clos_refl_trans _ R' x y.
Proof. induction 2; eauto. Qed.

fetburner

Require Import Autosubst.Autosubst.
Require Import Program Omega Relations Sorted.

Inductive term :=
  | tvar (x : var)
  | tapp (s t : term)
  | tabs (s : {bind term}).

Instance Ids_term : Ids term. derive. Defined.
Instance Rename_term : Rename term. derive. Defined.

fetburner

(fn s=>print(s^str(chr 34)^s^str(chr 34)))"(fn s=>print(s^str(chr 34)^s^str(chr 34)))"

fetburner

(fun s->print_string s;print_char@@Char.chr 34;print_string s;print_char@@Char.chr 34)"(fun s->print_string s;print_char@@Char.chr 34;print_string s;print_char@@Char.chr 34)"

fetburner

module type OrderedType = sig
  type t
  val compare: t -> t -> int
end

type z = Z_
type 'n s = S_ : 'n -> 'n s
type _ nat =
  | Z : z nat
  | S : 'n nat -> 'n s nat

fetburner

datatype 'a thunk = VALUE of 'a
                  | SUSPEND of unit -> 'a

fun memoize (n, f) =
  let
    val dp = Array.array (n, SUSPEND (fn () => raise Domain))
    fun get i =
      case Array.sub (dp, i) of
           VALUE v => v
         | SUSPEND f =>