23152
|
1 |
(* Title: HOLCF/Tools/domain/domain_extender.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb
|
|
4 |
|
|
5 |
Theory extender for domain command, including theory syntax.
|
|
6 |
|
|
7 |
###TODO:
|
|
8 |
|
|
9 |
this definition
|
|
10 |
domain empty = silly empty
|
|
11 |
yields
|
|
12 |
Exception-
|
|
13 |
TERM
|
|
14 |
("typ_of_term: bad encoding of type",
|
|
15 |
[Abs ("uu", "_", Const ("NONE", "_"))]) raised
|
|
16 |
but this works fine:
|
|
17 |
domain Empty = silly Empty
|
|
18 |
|
|
19 |
strange syntax errors are produced for:
|
|
20 |
domain xx = xx ("x yy")
|
|
21 |
domain 'a foo = foo (sel::"'a")
|
|
22 |
and bar = bar ("'a dummy")
|
|
23 |
|
|
24 |
*)
|
|
25 |
|
|
26 |
signature DOMAIN_EXTENDER =
|
|
27 |
sig
|
|
28 |
val add_domain: string * ((bstring * string list) *
|
|
29 |
(string * mixfix * (bool * string option * string) list) list) list
|
|
30 |
-> theory -> theory
|
|
31 |
val add_domain_i: string * ((bstring * string list) *
|
|
32 |
(string * mixfix * (bool * string option * typ) list) list) list
|
|
33 |
-> theory -> theory
|
|
34 |
end;
|
|
35 |
|
|
36 |
structure Domain_Extender: DOMAIN_EXTENDER =
|
|
37 |
struct
|
|
38 |
|
|
39 |
open Domain_Library;
|
|
40 |
|
|
41 |
(* ----- general testing and preprocessing of constructor list -------------- *)
|
|
42 |
fun check_and_sort_domain (dtnvs: (string * typ list) list,
|
|
43 |
cons'' : ((string * mixfix * (bool * string option * typ) list) list) list) sg =
|
|
44 |
let
|
|
45 |
val defaultS = Sign.defaultS sg;
|
|
46 |
val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of
|
|
47 |
[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
|
|
48 |
val test_dupl_cons = (case duplicates (op =) (map first (List.concat cons'')) of
|
|
49 |
[] => false | dups => error ("Duplicate constructors: "
|
|
50 |
^ commas_quote dups));
|
|
51 |
val test_dupl_sels = (case duplicates (op =) (List.mapPartial second
|
|
52 |
(List.concat (map third (List.concat cons'')))) of
|
|
53 |
[] => false | dups => error("Duplicate selectors: "^commas_quote dups));
|
|
54 |
val test_dupl_tvars = exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
|
|
55 |
[] => false | dups => error("Duplicate type arguments: "
|
|
56 |
^commas_quote dups)) (map snd dtnvs);
|
|
57 |
(* test for free type variables, illegal sort constraints on rhs,
|
|
58 |
non-pcpo-types and invalid use of recursive type;
|
|
59 |
replace sorts in type variables on rhs *)
|
|
60 |
fun analyse_equation ((dname,typevars),cons') =
|
|
61 |
let
|
|
62 |
val tvars = map dest_TFree typevars;
|
|
63 |
val distinct_typevars = map TFree tvars;
|
|
64 |
fun rm_sorts (TFree(s,_)) = TFree(s,[])
|
|
65 |
| rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
|
|
66 |
| rm_sorts (TVar(s,_)) = TVar(s,[])
|
|
67 |
and remove_sorts l = map rm_sorts l;
|
|
68 |
val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
|
|
69 |
fun analyse indirect (TFree(v,s)) = (case AList.lookup (op =) tvars v of
|
|
70 |
NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
|
|
71 |
| SOME sort => if eq_set_string (s,defaultS) orelse
|
|
72 |
eq_set_string (s,sort )
|
|
73 |
then TFree(v,sort)
|
|
74 |
else error ("Inconsistent sort constraint" ^
|
|
75 |
" for type variable " ^ quote v))
|
|
76 |
| analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of
|
|
77 |
NONE => if s mem indirect_ok
|
|
78 |
then Type(s,map (analyse false) typl)
|
|
79 |
else Type(s,map (analyse true) typl)
|
|
80 |
| SOME typevars => if indirect
|
|
81 |
then error ("Indirect recursion of type " ^
|
|
82 |
quote (string_of_typ sg t))
|
|
83 |
else if dname <> s orelse (** BUG OR FEATURE?:
|
|
84 |
mutual recursion may use different arguments **)
|
|
85 |
remove_sorts typevars = remove_sorts typl
|
|
86 |
then Type(s,map (analyse true) typl)
|
|
87 |
else error ("Direct recursion of type " ^
|
|
88 |
quote (string_of_typ sg t) ^
|
|
89 |
" with different arguments"))
|
|
90 |
| analyse indirect (TVar _) = Imposs "extender:analyse";
|
|
91 |
fun check_pcpo T = if pcpo_type sg T then T
|
|
92 |
else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T);
|
|
93 |
val analyse_con = upd_third (map (upd_third (check_pcpo o analyse false)));
|
|
94 |
in ((dname,distinct_typevars), map analyse_con cons') end;
|
|
95 |
in ListPair.map analyse_equation (dtnvs,cons'')
|
|
96 |
end; (* let *)
|
|
97 |
|
|
98 |
(* ----- calls for building new thy and thms -------------------------------- *)
|
|
99 |
|
|
100 |
fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
|
|
101 |
let
|
|
102 |
val dtnvs = map ((fn (dname,vs) =>
|
24707
|
103 |
(Sign.full_name thy''' dname, map (Syntax.read_typ_global thy''') vs))
|
23152
|
104 |
o fst) eqs''';
|
|
105 |
val cons''' = map snd eqs''';
|
|
106 |
fun thy_type (dname,tvars) = (Sign.base_name dname, length tvars, NoSyn);
|
|
107 |
fun thy_arity (dname,tvars) = (dname, map (snd o dest_TFree) tvars, pcpoS);
|
|
108 |
val thy'' = thy''' |> Theory.add_types (map thy_type dtnvs)
|
|
109 |
|> fold (AxClass.axiomatize_arity_i o thy_arity) dtnvs;
|
|
110 |
val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
|
|
111 |
val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';
|
|
112 |
val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
|
|
113 |
val dts = map (Type o fst) eqs';
|
|
114 |
val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
|
|
115 |
fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
|
|
116 |
fun typid (Type (id,_)) =
|
|
117 |
let val c = hd (Symbol.explode (Sign.base_name id))
|
|
118 |
in if Symbol.is_letter c then c else "t" end
|
|
119 |
| typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
|
|
120 |
| typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
|
|
121 |
fun one_con (con,mx,args) =
|
|
122 |
((Syntax.const_name con mx),
|
|
123 |
ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
|
|
124 |
find_index_eq tp dts,
|
|
125 |
DatatypeAux.dtyp_of_typ new_dts tp),
|
|
126 |
sel,vn))
|
|
127 |
(args,(mk_var_names(map (typid o third) args)))
|
|
128 |
) : cons;
|
|
129 |
val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
|
|
130 |
val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
|
|
131 |
val (theorems_thy, (rewss, take_rews)) = (foldl_map (fn (thy0,eq) =>
|
|
132 |
Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs))
|
|
133 |
|>>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
|
|
134 |
in
|
|
135 |
theorems_thy
|
|
136 |
|> Theory.add_path (Sign.base_name comp_dnam)
|
|
137 |
|> (snd o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
|
|
138 |
|> Theory.parent_path
|
|
139 |
end;
|
|
140 |
|
|
141 |
val add_domain_i = gen_add_domain Sign.certify_typ;
|
24707
|
142 |
val add_domain = gen_add_domain Syntax.read_typ_global;
|
23152
|
143 |
|
|
144 |
|
|
145 |
(** outer syntax **)
|
|
146 |
|
|
147 |
local structure P = OuterParse and K = OuterKeyword in
|
|
148 |
|
|
149 |
val dest_decl =
|
|
150 |
P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
|
|
151 |
(P.name >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
|
|
152 |
|| P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
|
|
153 |
>> (fn t => (true,NONE,t))
|
|
154 |
|| P.typ >> (fn t => (false,NONE,t));
|
|
155 |
|
|
156 |
val cons_decl =
|
|
157 |
P.name -- Scan.repeat dest_decl -- P.opt_mixfix
|
|
158 |
>> (fn ((c, ds), mx) => (c, mx, ds));
|
|
159 |
|
|
160 |
val type_var' = (P.type_ident ^^
|
|
161 |
Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
|
|
162 |
val type_args' = type_var' >> single ||
|
|
163 |
P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
|
|
164 |
Scan.succeed [];
|
|
165 |
|
|
166 |
val domain_decl = (type_args' -- P.name >> Library.swap) --
|
|
167 |
(P.$$$ "=" |-- P.enum1 "|" cons_decl);
|
|
168 |
val domains_decl =
|
|
169 |
Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl
|
|
170 |
>> (fn (opt_name, doms) =>
|
|
171 |
(case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms));
|
|
172 |
|
|
173 |
val domainP =
|
|
174 |
OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
|
|
175 |
(domains_decl >> (Toplevel.theory o add_domain));
|
|
176 |
|
|
177 |
|
|
178 |
val _ = OuterSyntax.add_keywords ["lazy"];
|
|
179 |
val _ = OuterSyntax.add_parsers [domainP];
|
|
180 |
|
|
181 |
end; (* local structure *)
|
|
182 |
|
|
183 |
end;
|