-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathConstructor.sml
More file actions
65 lines (63 loc) · 1.9 KB
/
Constructor.sml
File metadata and controls
65 lines (63 loc) · 1.9 KB
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
signature Constructor =
sig
type repr
val constr : string * string * repr list -> repr
end
functor Constructor
(val module_name : string
type exp
type infixop
type bind
type pat
type atype
eqtype str
type repr
type reprrepr
val construct_exp : ('a -> exp) -> ('a -> infixop) -> ('a -> bind) ->
('a -> atype) -> ('a -> str) ->
(exp -> 'b) -> string * 'a list -> 'b
val construct_infixop : ('a -> infixop) -> ('a -> exp) ->
(infixop -> 'b) ->
string * 'a list -> 'b
val construct_bind : ('a -> exp) -> ('a -> pat) -> ('a -> str) -> (bind -> 'b) ->
string * 'a list -> 'b
val construct_pat : ('a -> pat) -> ('a -> atype) ->
('a -> str) -> (pat -> 'b) -> string * 'a list -> 'b
val construct_atype : ('a -> atype) -> ('a -> str) ->
(atype -> 'b) -> string * 'a list -> 'b
val construct_str : ('a -> str) ->
(str -> 'b) -> string * 'a list -> 'b
val construct_reprrepr : (reprrepr -> 'a) -> string * repr list -> 'a
structure Induction : Induction
where type exp = exp
and type infixop = infixop
and type bind = bind
and type pat = pat
and type atype = atype
and type str = str
and type repr = repr
and type reprrepr = reprrepr
) :> Constructor
where type repr = repr =
struct
type exp = exp
type infixop = infixop
type bind = bind
type pat = pat
type atype = atype
type str = str
type repr = repr
type reprrepr = reprrepr
local
open Induction
in
val constr = constructor
construct_exp
construct_infixop
construct_bind
construct_pat
construct_atype
construct_str
construct_reprrepr
end
end