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