author | wenzelm |
Tue, 08 Nov 2005 10:43:08 +0100 | |
changeset 18117 | 61a430a67d7c |
parent 18065 | 16608ab6ed84 |
child 18146 | 47463b1825c6 |
permissions | -rw-r--r-- |
18060 | 1 |
(* Title: Pure/consts.ML |
2 |
ID: $Id$ |
|
3 |
Author: Makarius |
|
4 |
||
5 |
Polymorphic constants. |
|
6 |
*) |
|
7 |
||
8 |
signature CONSTS = |
|
9 |
sig |
|
10 |
type T |
|
11 |
val dest: T -> {declarations: typ NameSpace.table, constraints: typ NameSpace.table} |
|
12 |
val space: T -> NameSpace.T |
|
13 |
val declaration: T -> string -> typ (*exception TYPE*) |
|
14 |
val constraint: T -> string -> typ (*exception TYPE*) |
|
15 |
val monomorphic: T -> string -> bool |
|
16 |
val typargs: T -> string -> typ -> typ list |
|
17 |
val declare: NameSpace.naming -> bstring * typ -> T -> T |
|
18 |
val constrain: string * typ -> T -> T |
|
19 |
val hide: bool -> string -> T -> T |
|
20 |
val empty: T |
|
21 |
val merge: T * T -> T |
|
22 |
end |
|
23 |
||
24 |
structure Consts: CONSTS = |
|
25 |
struct |
|
26 |
||
27 |
||
28 |
(** datatype T **) |
|
29 |
||
30 |
datatype T = Consts of |
|
18117
61a430a67d7c
const args: do not store variable names (unused);
wenzelm
parents:
18065
diff
changeset
|
31 |
{declarations: ((typ * int list list) * serial) NameSpace.table, |
18060 | 32 |
constraints: typ Symtab.table}; |
33 |
||
34 |
fun make_consts (declarations, constraints) = |
|
35 |
Consts {declarations = declarations, constraints = constraints}; |
|
36 |
||
37 |
fun map_consts f (Consts {declarations, constraints}) = |
|
38 |
make_consts (f (declarations, constraints)); |
|
39 |
||
40 |
fun dest (Consts {declarations = (space, decls), constraints}) = |
|
41 |
{declarations = (space, Symtab.map (#1 o #1) decls), |
|
42 |
constraints = (space, constraints)}; |
|
43 |
||
44 |
fun space (Consts {declarations = (space, _), ...}) = space; |
|
45 |
||
46 |
||
47 |
(* lookup consts *) |
|
48 |
||
49 |
fun the_const (Consts {declarations = (_, decls), ...}) c = |
|
50 |
(case Symtab.lookup decls c of SOME (decl, _) => decl |
|
51 |
| NONE => raise TYPE ("Undeclared constant " ^ quote c, [], [])); |
|
52 |
||
53 |
fun declaration consts c = #1 (the_const consts c); |
|
54 |
||
55 |
fun constraint (consts as Consts {constraints, ...}) c = |
|
56 |
(case Symtab.lookup constraints c of |
|
57 |
SOME T => T |
|
58 |
| NONE => declaration consts c); |
|
59 |
||
60 |
fun monomorphic consts c = null (#2 (the_const consts c)); |
|
61 |
||
62 |
||
63 |
(* typargs -- view actual const type as instance of declaration *) |
|
64 |
||
65 |
fun sub (Type (_, Ts)) (i :: is) = sub (nth Ts i) is |
|
66 |
| sub T [] = T |
|
67 |
| sub T _ = raise Subscript; |
|
68 |
||
18117
61a430a67d7c
const args: do not store variable names (unused);
wenzelm
parents:
18065
diff
changeset
|
69 |
fun typargs consts c T = map (sub T) (#2 (the_const consts c)); |
18060 | 70 |
|
71 |
||
72 |
||
73 |
(** build consts **) |
|
74 |
||
75 |
fun err_dup_consts cs = |
|
76 |
error ("Duplicate declaration of constant(s) " ^ commas_quote cs); |
|
77 |
||
78 |
fun err_inconsistent_constraints cs = |
|
79 |
error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs); |
|
80 |
||
81 |
||
82 |
(* declarations etc. *) |
|
83 |
||
84 |
fun args_of declT = |
|
85 |
let |
|
86 |
fun args (Type (_, Ts)) pos = args_list Ts 0 pos |
|
87 |
| args (TVar v) pos = insert (eq_fst op =) (v, rev pos) |
|
88 |
| args (TFree _) _ = I |
|
89 |
and args_list (T :: Ts) i is = args T (i :: is) #> args_list Ts (i + 1) is |
|
90 |
| args_list [] _ _ = I; |
|
18117
61a430a67d7c
const args: do not store variable names (unused);
wenzelm
parents:
18065
diff
changeset
|
91 |
in map #2 (rev (args declT [] [])) end; |
18060 | 92 |
|
93 |
fun declare naming (c, T) = map_consts (apfst (fn declarations => |
|
94 |
let |
|
95 |
val decl = (c, ((T, args_of T), serial ())); |
|
96 |
val declarations' = NameSpace.extend_table naming (declarations, [decl]) |
|
97 |
handle Symtab.DUPS cs => err_dup_consts cs; |
|
98 |
in declarations' end)); |
|
99 |
||
100 |
val constrain = map_consts o apsnd o Symtab.update; |
|
101 |
||
102 |
fun hide fully c = map_consts (apfst (apfst (NameSpace.hide fully c))); |
|
103 |
||
104 |
||
105 |
(* empty and merge *) |
|
106 |
||
107 |
val empty = make_consts (NameSpace.empty_table, Symtab.empty); |
|
108 |
||
109 |
fun merge |
|
110 |
(Consts {declarations = declarations1, constraints = constraints1}, |
|
111 |
Consts {declarations = declarations2, constraints = constraints2}) = |
|
112 |
let |
|
113 |
val declarations = NameSpace.merge_tables (eq_snd (op =)) (declarations1, declarations2) |
|
114 |
handle Symtab.DUPS cs => err_dup_consts cs; |
|
115 |
val constraints = Symtab.merge (op =) (constraints1, constraints2) |
|
116 |
handle Symtab.DUPS cs => err_inconsistent_constraints cs; |
|
117 |
in make_consts (declarations, constraints) end; |
|
118 |
||
119 |
end; |