Skip to content

Instantly share code, notes, and snippets.

@einblicker
Created August 20, 2011 12:18
Show Gist options
  • Save einblicker/1159025 to your computer and use it in GitHub Desktop.
Save einblicker/1159025 to your computer and use it in GitHub Desktop.
CoPL problem 77
|- let rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x) in
apply ((fun x -> x * x) :: (fun y -> y + 3) :: []) 4
evalto 19
by E-LetRec {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)] |-
apply ((fun x -> x * x) :: (fun y -> y + 3) :: []) 4
evalto 19
by E-App {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)] |-
apply ((fun x -> x * x) :: (fun y -> y + 3) :: [])
evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [])[
fun x ->
match l with [] -> x | f :: l -> apply l (f x)]
by E-AppRec {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)] |-
apply evalto ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)]
by E-Var {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)] |-
((fun x -> x * x) :: (fun y -> y + 3) :: [])
evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: []
by E-Cons {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)] |-
fun x -> x * x
evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x]
by E-Fun {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)] |-
(fun y -> y + 3) :: []
evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: []
by E-Cons {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)] |-
fun y -> y + 3
evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3]
by E-Fun {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)] |-
[] evalto [] by E-Nil {}
}
};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [] |-
fun x ->
match l with [] -> x | f :: l -> apply l (f x)
evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [])[
fun x ->
match l with [] -> x | f :: l -> apply l (f x)]
by E-Fun {}
};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)] |-
4 evalto 4 by E-Int {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 4 |-
match l with [] -> x | f :: l -> apply l (f x)
evalto 19
by E-MatchCons {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 4 |-
l evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: []
by E-Var {};
// ?
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 4,
f = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [] |-
apply l (f x) evalto 19
by E-App {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 4,
f = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [] |-
apply l
evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [] )[
fun x ->
match l with [] -> x | f :: l -> apply l (f x) ]
by E-AppRec {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 4,
f = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [] |-
apply evalto ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)]
by E-Var {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 4,
f = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [] |-
l evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: []
by E-Var {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [] |-
fun x ->
match l with [] -> x | f :: l -> apply l (f x)
evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [] )[
fun x ->
match l with [] -> x | f :: l -> apply l (f x) ]
by E-Fun {}
};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 4,
f = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [] |-
f x evalto 16
by E-App {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 4,
f = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [] |-
f evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x]
by E-Var {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 4,
f = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun x -> x * x],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [] |-
x evalto 4 by E-Var {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
x = 4 |-
x * x evalto 16
by E-Times {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
x = 4 |-
x evalto 4 by E-Var {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
x = 4 |-
x evalto 4 by E-Var {};
4 times 4 is 16 by B-Times {}
}
};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 16 |-
match l with [] -> x | f :: l -> apply l (f x)
evalto 19
by E-MatchCons {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 16 |-
l evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: []
by E-Var {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 16,
f = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3],
l = [] |-
((apply l) (f x))
evalto 19
by E-App {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 16,
f = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3],
l = [] |-
apply l
evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = [])[
fun x ->
match l with [] -> x | f :: l -> apply l (f x)]
by E-AppRec {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 16,
f = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3],
l = [] |-
apply evalto ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)]
by E-Var {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 16,
f = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3],
l = [] |-
l evalto []
by E-Var {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = [] |-
fun x ->
match l with [] -> x | f :: l -> apply l (f x)
evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = [])[
fun x ->
match l with [] -> x | f :: l -> apply l (f x)]
by E-Fun {}
};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 16,
f = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3],
l = [] |-
f x evalto 19
by E-App {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 16,
f = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3],
l = [] |-
f evalto (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3]
by E-Var {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3] :: [],
x = 16,
f = (apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)])[
fun y -> y + 3],
l = [] |-
x evalto 16
by E-Var {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
y = 16 |-
y + 3 evalto 19
by E-Plus {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
y = 16 |-
y evalto 16
by E-Var {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
y = 16 |-
3 evalto 3
by E-Int {};
16 plus 3 is 19 by B-Plus {}
}
};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = [],
x = 19 |-
match l with [] -> x | f :: l -> apply l (f x)
evalto 19
by E-MatchNil {
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = [],
x = 19 |-
l evalto []
by E-Var {};
apply = ()[rec apply = fun l -> fun x ->
match l with [] -> x | f :: l -> apply l (f x)],
l = [],
x = 19 |-
x evalto 19
by E-Var {}
}
}
}
}
}
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment