1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
let Bool = [T: <>, F: <>] in
let or (x : Bool) (y : Bool) : Bool = case x of {T u => T <>; F u => y} in
let SysT =
(\T =>
[ Var: Nat
, Zero: <>
, Suc: T
, Primrec: <Zero: T, Suc: T, Target: T>
, Abs: T
, App: <Fun: T, Arg: T>
])
in
let Stepped = <Term: SysT, Smaller: Bool> in
let lift (f : Nat -> Nat) (n : Nat) : Nat =
case !n of {Z u => 0; S k => suc (f k)}
in
let rename (t : SysT) : (Nat -> Nat) -> SysT =
foldcase t by
{ Var n => \f => ~(Var (f n))
; Zero u => \f => ~(Zero <>)
; Suc r => \f => ~(Suc (r f))
; Primrec p => \f =>
~(Primrec <Zero: p.Zero f, Suc: p.Suc (lift f), Target: p.Target f>)
; Abs r => \f => ~(Abs (r f))
; App p => \f => ~(App <Fun: p.Fun f, Arg: p.Arg f>)
}
in
let index (xs : List SysT) : Nat -> SysT =
foldcase xs by
{ N u => \k => ~(Var k)
; C p => \k => case !k of {Z u => p.H; S k => p.T k}
}
in
let shift = map (\X => List X) SysT SysT (\t => rename t (\x => suc x)) in
let sub (t : SysT) : List SysT -> SysT =
foldcase t by
{ Var n => \env => index env n
; Zero u => \env => ~(Zero <>)
; Suc f => \env => ~(Suc (f env))
; Primrec p => \env =>
~(Primrec
< Zero: p.Zero env
, Suc: p.Suc (cons ~(Var 0) (shift env))
, Target: p.Target env
>)
; Abs f => \env => ~(Abs (f (cons ~(Var 0) (shift env))))
; App p => \env => ~(App <Fun: p.Fun env, Arg: p.Arg env>)
}
in
let app (fun : SysT) (arg : SysT) (smaller : Bool) : Stepped =
let default : Stepped =
<Term: ~(App <Fun: fun, Arg: arg>), Smaller: smaller>
in
case !fun of
{ Var n => default
; Zero u => default
; Suc t => default
; Primrec p => default
; Abs t => <Term: sub t [arg], Smaller: T <>>
; App t => default
}
in
let rec (z : SysT) (s : SysT) (target : SysT) (smaller : Bool) : Stepped =
let default : Stepped =
<Term: ~(Primrec <Zero: z, Suc: s, Target: target>), Smaller: smaller>
in
case !target of
{ Var n => default
; Zero u => <Term: z, Smaller: T <>>
; Suc t =>
<Term: sub s [~(Primrec <Zero: z, Suc: s, Target: t>)], Smaller: T <>>
; Primrec p => default
; Abs t => default
; App t => default
}
in
let step (t : SysT) : Stepped =
foldcase t by
{ Var n => <Term: ~(Var n), Smaller: F <>>
; Zero u => <Term: ~(Zero <>), Smaller: F <>>
; Suc t => <Term: ~(Suc t.Term), Smaller: t.Smaller>
; Primrec t =>
case t.Target.Smaller of
{ F u =>
rec
t.Zero.Term
t.Suc.Term
t.Target.Term
(or t.Zero.Smaller t.Suc.Smaller)
; T u =>
< Term:
~(Primrec
(map
(\X => <Zero: X, Suc: X, Target: X>)
Stepped
SysT
(\p => p.Term)
t))
, Smaller: T <>
>
}
; Abs t => <Term: ~(Abs t.Term), Smaller: t.Smaller>
; App t =>
case t.Arg.Smaller of
{ F u => app t.Fun.Term t.Arg.Term t.Fun.Smaller
; T u =>
< Term:
~(App (map (\X => <Fun: X, Arg: X>) Stepped SysT (\p => p.Term) t))
, Smaller: T <>
>
}
}
in
\n =>
foldcase n by
{ Z u => \t => t
; S f => \t =>
let stepped = step t in
case stepped.Smaller of {F u => stepped.Term; T u => f stepped.Term}
}
|
