-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathSimpleSubs.sml
133 lines (131 loc) · 5.73 KB
/
SimpleSubs.sml
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
121
122
123
124
125
126
127
128
129
130
131
132
133
functor SimpleSubs
(val module_name : string
type repr
val map_name : string
structure Semantics : Semantics
where type repr = repr
structure Induction : Induction
where type repr = repr
) :> SubsConvention
where type repr = repr
and type exstate = Semantics.state =
struct
val map_name = map_name
type repr = repr
type exstate = Semantics.state
type str = Induction.str
type substate = {alpha : (str * str) list}
type state = substate * exstate
local
fun errmsg function part t s l =
let val params = t^","^s^","^(Induction.reprListToString l)
in module_name^"."^function^": "^part^": ("^params^")"
end
val rep_str = Induction.Repr.rep_str
val str = Induction.dec_repr_str Induction.Repr.prt_repr
val toMLString = Induction.Str.toMLString
fun rename v l =
let fun iter [] = v
| iter ((v',s)::ss) =
if v=v' then s else iter ss
in iter l
end
in
fun get_state ((_,exstate):state) = exstate
fun set_state ((substate,_):state) exstate = (substate,exstate)
val initstate = ({alpha = []},Semantics.initstate)
fun consavoid (state:state) (_:repr) = state
fun nullavoid (state:state) = state
fun consalpha ({alpha}:substate,exstate) s s' =
let val _ = () (*print("consalpha: renaming "^(toMLString (str s))^
"/"^(toMLString (str s'))^"\n") *)
in ({alpha = (str s,str s')::alpha},exstate) end
fun reference ({alpha},exstate) v = rep_str (rename (str v) alpha)
fun binder (substate:substate as {alpha},exstate) v =
let val v = str v
val v' = rename v alpha
(* val _ = print("binder: renamed "^(toMLString v')^
"/"^(toMLString v)^"\n") *)
in (rep_str v',(substate,exstate))
end
fun pattern corecur state p e =
let val (p',state') = corecur state p
val (e',_) = corecur state' e
in (p', e')
end
fun direct_binder corecur ({alpha}:substate,exstate) v e =
let val state' = ({alpha = alpha},exstate)
val (v',state') = binder state' v
val (exp,_) = corecur state' e
in (v', exp)
end
fun lifted function (state:state) = fn arg =>
let val exstate = get_state state
val (result,exstate') = function exstate arg
in (result,set_state state exstate')
end
fun reconstr deconstructor =
fn state => fn (arg as (t,c,l)) =>
let val corecur = deconstructor
fun constr state' = (* resync exstate after corecursion (FIXME) *)
lifted Semantics.reconstr (set_state state' (get_state state))
fun iter r state [] = (rev r,state)
| iter r state (arg::args) =
let val (e,state') = corecur state arg
in iter (e::r) state' args
end
fun default state t c l =
let val (l',state') = iter [] state l
in constr state' (t,c,l')
end
in if t = map_name
then case (c,l) of
("varref", [v]) =>
let val v' = reference state v
in constr state (t,c,[v'])
end
| ("patabsbind", [p,e]) =>
let val (p', e') = pattern corecur state p e
in constr state (t,c,[p',e'])
end
| ("patletbind", [p,e,e']) =>
let val (e'', state') = corecur state e
val (p, e''') = pattern corecur state' p e'
in constr state' (t,c,[p,e'',e'''])
end
| ("absbind", [v,e]) =>
let val (v', e') = direct_binder corecur state v e
in constr state (t,c,[v',e'])
end
| ("letbind", [v,e,e']) =>
let val (e'', state') = corecur state e
val (v', e''') = direct_binder corecur state' v e'
in constr state' (t,c,[v',e'',e'''])
end
| ("patvar", v::args) =>
let val (v',state') = binder state v
val (args',state'') = iter [] state' args
in constr state'' (t,c,v'::args')
end
| ("patalias", [v,p]) =>
let val (v',state') = binder state v
val (p',state'') = corecur state' p
in constr state'' (t,c,[v',p'])
end
| ("id", l) => constr state (t,c,l)
| _ => raise Fail (errmsg "reconstr" "no case" t c l) (* default state t c l *)
else default state t c l
end
local
fun loopback deconstruct reconstruct =
fn state => fn input =>
let val (output,state') = deconstruct state input
in reconstruct state' output
end
val deconstruct = loopback (lifted Semantics.deconstr)
val reconstruct = reconstr
in
val reconstr = Induction.induction deconstruct reconstruct
end
end
end