projects
/
lambda.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
consistent vars, some paren spacing
[lambda.git]
/
code
/
ski_evaluator.ml
diff --git
a/code/ski_evaluator.ml
b/code/ski_evaluator.ml
index
7837880
..
727a84a
100644
(file)
--- a/
code/ski_evaluator.ml
+++ b/
code/ski_evaluator.ml
@@
-42,7
+42,7
@@
let rec reduce_try3 (t:term):term = match t with
type to emphasize the parallels with the untyped interpreter. *)
type reduceOutcome = AlreadyReduced | ReducedTo of term
type to emphasize the parallels with the untyped interpreter. *)
type reduceOutcome = AlreadyReduced | ReducedTo of term
- let reduce_if_redex (t : term) :
term
= match t with
+ let reduce_if_redex (t : term) :
reduceOutcome
= match t with
| App(I,a) -> ReducedTo a
| App(App(K,a),b) -> ReducedTo a
| App(App(App(S,a),b),c) -> ReducedTo (App(App(a,c),App(b,c)))
| App(I,a) -> ReducedTo a
| App(App(K,a),b) -> ReducedTo a
| App(App(App(S,a),b),c) -> ReducedTo (App(App(a,c),App(b,c)))
@@
-53,7
+53,7
@@
let rec reduce_try3 (t:term):term = match t with
| K -> K
| S -> S
| App(a, b) ->
| K -> K
| S -> S
| App(a, b) ->
- let t' = App(reduce_try
3 a, reduce_try
b) in
+ let t' = App(reduce_try
4 a, reduce_try4
b) in
(match reduce_if_redex t' with
| ReducedTo t'' -> reduce_try4 t''
| AlreadyReduced -> t')
(match reduce_if_redex t' with
| ReducedTo t'' -> reduce_try4 t''
| AlreadyReduced -> t')
@@
-64,7
+64,7
@@
let rec reduce_try3 (t:term):term = match t with
type reduceOutcome = AlreadyReduced | ReducedTo of term
type reduceOutcome = AlreadyReduced | ReducedTo of term
- let rec reduce_once (t : term) :
term
= match t with
+ let rec reduce_once (t : term) :
reduceOutcome
= match t with
| App(a, b) -> (match reduce_once a with
| ReducedTo a' -> ReducedTo (App(a',b))
| AlreadyReduced -> (match reduce_once b with
| App(a, b) -> (match reduce_once a with
| ReducedTo a' -> ReducedTo (App(a',b))
| AlreadyReduced -> (match reduce_once b with
@@
-96,7
+96,7
@@
let rec reduce_try3 (t:term):term = match t with
| App(App(App(S,_),_),_) -> true
| _ -> false
| App(App(App(S,_),_),_) -> true
| _ -> false
- let rec reduce_head_once (t : term) :
term
= match t with
+ let rec reduce_head_once (t : term) :
reduceOutcome
= match t with
| App(a, b) -> (match reduce_head_once a with
| ReducedTo a' -> ReducedTo (App(a',b))
(* now we only try to reduce b when App(a,b) is a redex *)
| App(a, b) -> (match reduce_head_once a with
| ReducedTo a' -> ReducedTo (App(a',b))
(* now we only try to reduce b when App(a,b) is a redex *)