|
1 signature IML_PACKAGE = |
|
2 sig |
|
3 end; |
|
4 |
|
5 structure ImlPackage : IML_PACKAGE = |
|
6 struct |
|
7 |
|
8 type nsidf = string |
|
9 type idf = string |
|
10 type qidf = nsidf * idf |
|
11 type iclass = qidf |
|
12 type isort = iclass list |
|
13 type ityco = qidf |
|
14 type iconst = qidf |
|
15 type 'a vidf = string * 'a |
|
16 type tvname = isort vidf |
|
17 |
|
18 fun qidf_ord ((a, c), (b, d)) = |
|
19 (case string_ord (a, b) of EQUAL => string_ord (c, d) | ord => ord); |
|
20 |
|
21 structure Idfgraph = GraphFun(type key = qidf val ord = qidf_ord); |
|
22 |
|
23 datatype ityp = |
|
24 IType of ityco * ityp list |
|
25 | IFree of tvname * isort |
|
26 |
|
27 type vname = ityp vidf |
|
28 |
|
29 datatype iexpr = |
|
30 IConst of iconst * ityp |
|
31 | IVar of vname * ityp |
|
32 | IAbs of vname * iexpr |
|
33 | IApp of iexpr * iexpr |
|
34 |
|
35 datatype pat = |
|
36 PConst of iconst |
|
37 | PVar of vname |
|
38 |
|
39 type 'a defn = 'a * (pat list * iexpr) list |
|
40 |
|
41 datatype stmt = |
|
42 Def of ityp defn |
|
43 | Typdecl of vname list * ityp |
|
44 | Datadef of (iconst * vname list) list |
|
45 | Classdecl of string list * (string * ityp) list |
|
46 | Instdef of iclass * ityco * isort list * (string defn) list |
|
47 |
|
48 type module = stmt Idfgraph.T |
|
49 |
|
50 type universe = module Graph.T |
|
51 |
|
52 fun isort_of_sort nsp sort = |
|
53 map (pair nsp) sort |
|
54 |
|
55 (* fun ityp_of_typ nsp ty = |
|
56 * let |
|
57 * fun ityp_of_typ' (Type (tycon, tys)) = IType ((nsp, tycon), map ityp_of_typ' tys) |
|
58 * | ityp_of_typ' (TFree (varname, sort)) = IFree ((nsp, varname), isort_of_sort nsp sort) |
|
59 * in (ityp_of_typ' o unvarifyT) ty end; |
|
60 *) |
|
61 |
|
62 (* fun iexpr_of_term nsp t = |
|
63 * let |
|
64 * fun iexpr_of_term' (Const (const, ty)) = IConst ((nsp, const), ityp_of_typ nsp ty) |
|
65 * | iexpr_of_term' (Free (varname, ty)) = IVar ((nsp, varname), ityp_of_typ nsp ty) |
|
66 * | iexpr_of_term' (Free (varname, ty)) = IVar ((nsp, varname), ityp_of_typ nsp ty) |
|
67 * in (iexpr_of_term' o map_term_types (unvarifyT)) t |
|
68 * |
|
69 * datatype term = |
|
70 * Const of string * typ | |
|
71 * Free of string * typ | |
|
72 * Var of indexname * typ | |
|
73 * Bound of int | |
|
74 * Abs of string * typ * term | |
|
75 * op $ of term * term |
|
76 * |
|
77 * |
|
78 * fun iexpr_of |
|
79 *) |
|
80 |
|
81 val empty_universe = Graph.empty |
|
82 |
|
83 val empty_module = Idfgraph.empty |
|
84 |
|
85 datatype deps = |
|
86 Check |
|
87 | Nocheck |
|
88 | Dep of qidf list |
|
89 |
|
90 fun add_stmt modname idf deps stmt univ = |
|
91 let |
|
92 fun check_deps Nocheck = I |
|
93 | check_deps (Dep idfs) = Graph.add_deps_acyclic (modname, map #2 idfs) |
|
94 | check_deps _ = error "'Nocheck' not implemented yet" |
|
95 in |
|
96 univ |
|
97 |> Graph.default_node modname empty_module |
|
98 |> Graph.map_node modname (Idfgraph.new_node (idf, stmt)) |
|
99 |> fold check_deps deps |
|
100 end |
|
101 |
|
102 (* WICHTIG: resolve_qidf, resolve_midf *) |
|
103 |
|
104 (* IDEAS: Transaktionspuffer, Errormessage-Stack *) |
|
105 |
|
106 end; |
|
107 |