-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathReprEmbedding.sml
138 lines (124 loc) · 5.27 KB
/
ReprEmbedding.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
134
135
136
137
138
signature ReprEmbedding =
sig
val module_name : string
type repr
type reprrepr
eqtype str
val reprToString : repr -> string
val reprListToString : repr list -> string
structure Deconstructor : Deconstructor
where type repr = repr
structure Constructor : Constructor
where type repr = repr
end
functor ReprEmbedding
(val module_name : string
eqtype str
type repr
type reprrepr
structure Induction : Induction
where type str = str
and type repr = repr
and type reprrepr = reprrepr
) :> ReprEmbedding
where type str = str
and type repr = repr
and type reprrepr = reprrepr =
struct
val module_name = module_name
type str = str
type repr = repr
type reprrepr = reprrepr
local
val fromMLString = Induction.Str.fromMLString
val toMLString = Induction.Str.toMLString
val rep_str = Induction.Repr.rep_str
val str = Induction.dec_repr_str Induction.Repr.prt_repr
val r_rr = Induction.dec_repr_repr Induction.Repr.prt_repr
val prt_reprrepr = Induction.ReprRepr.prt_reprrepr
val reprnil = Induction.Repr.rep_reprrepr (Induction.ReprRepr.rep_nil ())
fun reprcons a l = Induction.Repr.rep_reprrepr (Induction.ReprRepr.rep_repr a l)
fun foldright f =
let val rec iter = fn r => Induction.ReprRepr.prt_reprrepr
(fn () => r)
(fn a => fn b => iter (f a r) (r_rr b))
in iter
end
fun foldleft f =
let val rec iter = fn r => Induction.ReprRepr.prt_reprrepr
(fn () => r)
(fn a => fn b => f a (iter r (r_rr b)))
in iter
end
val reverse = foldright reprcons reprnil
fun reprListToRepr [] = reprnil
| reprListToRepr (v::l) = reprcons v (reprListToRepr l)
fun reprToList rs =
rev (foldright (fn a => fn r => a::r)
[] (r_rr rs))
fun mk_reprrepr (t,c,l) = reprcons (reprcons (rep_str (fromMLString t))
(rep_str (fromMLString c)))
(reprListToRepr l)
fun dst_reprrepr r =
let val (tc,lr) =
Induction.ReprRepr.prt_reprrepr
(fn () => raise Fail (module_name^".extract_repr: nil pair"))
(fn a => fn b => (a,b)) (r_rr r)
val (t,c) =
Induction.ReprRepr.prt_reprrepr
(fn () => raise Fail (module_name^".extract_repr: nil pair"))
(fn a => fn b => (a,b)) (r_rr tc)
in (toMLString (str t),toMLString (str c),reprToList lr)
end
fun toString str deconstructor =
fn output => fn state => fn (t,cn,args) =>
let val corecur = deconstructor output
val state = output state (t^"."^cn)
fun iter state [] = state
| iter state (arg::args) =
let fun stringarg arg = output state (" '"^(str arg)^"'")
fun otherarg arg = output (corecur (output state " (") arg) ")"
(* val _ = print ("ReprEmbedding.toStr: "^t^"."^cn^" "^
(Induction.reprListToString (arg::args))^"\n") *)
val state = case (t,cn) of
("str","string") =>
(case dst_reprrepr arg of
("str","string",[arg]) => stringarg arg
| _ => raise Fail ("ReprEmbedding.reprToString: reprrepr"))
| ("bindvar","var") => stringarg arg
| ("atyvar","var") => stringarg arg
| ("exp","var") => stringarg arg
| ("bindvar","meta") => stringarg arg
| ("atyvar","meta") => stringarg arg
| ("exp","meta") => stringarg arg
| ("monomial","name") => stringarg arg
| _ => otherarg arg
in iter state args
end
in iter state args
end
fun stringPrinter state = fn s => state^s
val toStr = Induction.Str.toMLString o (Induction.dec_repr_str Induction.Repr.prt_repr)
in
structure Deconstructor :> Deconstructor where type repr = repr =
struct
type repr = repr
val deconstr = dst_reprrepr
end
structure Constructor :> Constructor where type repr = repr =
struct
type repr = repr
val constr = mk_reprrepr
end
val reprToString = Induction.induction (Induction.fromRep Deconstructor.deconstr)
(toString toStr) stringPrinter ""
fun reprListToString l =
let fun iter s [] = "["^s^"]"
| iter s (r::rs) =
let val sep = if s = "" then "" else ", "
in iter (s^sep^(reprToString r)) rs
end
in iter "" l
end
end
end