blob: 3abbc974477702d4cb60a49f8ccadc328fc1e3ef (
plain)
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}
}
|
