equal
deleted
inserted
replaced
3 |
3 |
4 Producing well-sorted systems of code equations in a graph |
4 Producing well-sorted systems of code equations in a graph |
5 with explicit dependencies -- the Waisenhaus algorithm. |
5 with explicit dependencies -- the Waisenhaus algorithm. |
6 *) |
6 *) |
7 |
7 |
8 signature CODE_FUNCGR = |
8 signature CODE_WELLSORTED = |
9 sig |
9 sig |
10 type T |
10 type T |
11 val eqns: T -> string -> (thm * bool) list |
11 val eqns: T -> string -> (thm * bool) list |
12 val typ: T -> string -> (string * sort) list * typ |
12 val typ: T -> string -> (string * sort) list * typ |
13 val all: T -> string list |
13 val all: T -> string list |
18 -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm |
18 -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm |
19 val eval_term: theory |
19 val eval_term: theory |
20 -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a |
20 -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a |
21 end |
21 end |
22 |
22 |
23 structure Code_Funcgr : CODE_FUNCGR = |
23 structure Code_Wellsorted : CODE_WELLSORTED = |
24 struct |
24 struct |
25 |
25 |
26 (** the equation graph type **) |
26 (** the equation graph type **) |
27 |
27 |
28 type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T; |
28 type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T; |