-
Notifications
You must be signed in to change notification settings - Fork 51
/
elpi-reduction.elpi
108 lines (89 loc) · 4.15 KB
/
elpi-reduction.elpi
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
/* Reduction (whd, hd-beta, ...) */
/* license: GNU Lesser General Public License Version 2.1 or later */
/* ------------------------------------------------------------------------- */
% Entry points
typeabbrev stack (list term).
pred hd-beta i:term, i:stack, o:term, o:stack.
pred hd-beta-zeta i:term, i:stack, o:term, o:stack.
pred hd-beta-zeta-reduce i:term, o:term.
pred whd i:term, i:stack, o:term, o:stack.
pred whd-indc i:term, o:constructor, o:stack.
pred unwind i:term, i:stack, o:term.
pred whd1 i:term, o:term.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
shorten std.{append, nth, drop}.
% indirection, to be used if we add to the stack "match" frames
unwind T A R :- if (var T) (coq.mk-app-uvar T A R) (coq.mk-app T A R).
pred nth-stack i:int, i:stack, o:stack, o:term, o:stack.
nth-stack 0 [X|XS] [] X XS :- !.
nth-stack N [X|XS] [X|Before] At After :-
M is N - 1, nth-stack M XS Before At After.
% whd beta-iota-delta-zeta, main code
whd (app [Hd|Args]) C X XC :- !, whd Hd {append Args C} X XC.
whd (fun _ _ _ as X) [] X [] :- !.
whd (fun N T F) [B|C] X XC :- !,
(pi x\ def x N T B => cache x BN_ => whd (F x) C (F1 x) (C1 x)), X = F1 B, XC = C1 B.
whd (let N T B F) C X XC :- !,
(pi x\ def x N T B => cache x BN_ => whd (F x) C (F1 x) (C1 x)), X = F1 B, XC = C1 B.
whd (global (const GR)) C X XC :- unfold GR none C D DC, !, whd D DC X XC.
whd (pglobal (const GR) I) C X XC :- unfold GR (some I) C D DC, !, whd D DC X XC.
whd (primitive (proj _ N)) [A|C] X XC :- whd-indc A _ KA, !,
whd {proj-red KA N C} X XC.
whd (global (const GR) as HD) C X XC :- coq.env.primitive? GR, !,
unwind HD C Orig,
coq.reduction.lazy.whd_all Orig R,
if (same_term Orig R) (X = HD, XC = C) (whd R [] X XC).
whd (match A _ L) C X XC :- whd-indc A GR KA, !,
whd {match-red GR KA L C} X XC.
whd (fix _ N _ F as Fix) C X XC :- nth-stack N C LA A RA, whd-indc A GR KA, !,
whd {fix-red F Fix LA GR KA RA} X XC.
whd N C X XC :- name N, def N _ _ V, !, cache-whd N VN V, whd VN C X XC.
whd X C X C.
% assert A reduces to a constructor
whd-indc A GR KA :- whd A [] VA C, !, not(var VA), VA = global (indc GR), KA = C.
% [whd1 T R] asserts progress was made in reducing T to R.
whd1 T R :-
whd T [] HD ARGS,
unwind HD ARGS R,
not(same_term T R).
% iota step
pred match-red i:constructor, i:list term, i:list term, i:stack, o:term, o:stack.
match-red GR KArgs BL C X XC :-
coq.env.indc GR Lno _ Ki _,
drop Lno KArgs Args,
nth Ki BL Bi,
hd-beta {coq.mk-app Bi Args} C X XC.
pred proj-red i:list term, i:int, i:stack, o:term, o:stack.
proj-red Args FieldNo C V C :-
nth FieldNo Args V.
% iota step
pred fix-red
i:(term -> term), i:term,
i:list term, i:constructor, i:list term, i:list term, o:term, o:stack.
fix-red F Fix LA GR KA RA X XC :-
append LA [{coq.mk-app (global (indc GR)) KA}|RA] ArgsWRedRecNo,
hd-beta {coq.mk-app (F Fix) ArgsWRedRecNo} [] X XC.
pred unfold % delta (global constants) + hd-beta
i:constant, % name
i:option univ-instance, % universe instance if the constant is universe polymorphic
i:stack, % args
o:term, % body
o:stack. % args after hd-beta
unfold GR none A BO BOC :- coq.env.const GR (some B) _, hd-beta B A BO BOC.
unfold GR (some I) A BO BOC :- @uinstance! I => coq.env.const GR (some B) _, hd-beta B A BO BOC.
% ensures its first argument is the whd of the second
pred cache i:term, o:term.
pred cache-whd i:term, i:term, i:term.
cache-whd N K V :- cache N VN, var VN, !, whd V [] X XC, unwind X XC VN, K = VN.
cache-whd N K _ :- cache N K, !.
cache-whd N _ _ :- coq.error "anomaly: def with no cache:" {coq.term->string N}.
hd-beta (app [Hd|Args]) S X C :- !, hd-beta Hd {append Args S} X C.
hd-beta (fun _ _ F) [A|AS] X C :- !, hd-beta (F A) AS X C.
:name "hd-beta:end"
hd-beta X C X C.
hd-beta-zeta (app [Hd|Args]) S X C :- !, hd-beta-zeta Hd {append Args S} X C.
hd-beta-zeta (fun _ _ F) [A|AS] X C :- !, hd-beta-zeta (F A) AS X C.
hd-beta-zeta (let _ _ B F) AS X C :- !, hd-beta-zeta (F B) AS X C.
:name "hd-beta-zeta:end"
hd-beta-zeta X C X C.
hd-beta-zeta-reduce T R :- hd-beta-zeta T [] H S, unwind H S R.