author | huffman |
Tue, 12 May 2009 11:37:40 -0700 | |
changeset 31161 | a27d4254ff4c |
parent 31023 | d027411c9a38 |
child 31163 | 19c2f68ae23d |
permissions | -rw-r--r-- |
23152 | 1 |
(* Title: HOLCF/Tools/domain/domain_extender.ML |
2 |
Author: David von Oheimb |
|
3 |
||
4 |
Theory extender for domain command, including theory syntax. |
|
5 |
*) |
|
6 |
||
7 |
signature DOMAIN_EXTENDER = |
|
8 |
sig |
|
31161
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
9 |
val add_domain_cmd: string -> |
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
10 |
((string * string option) list * binding * mixfix * |
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
11 |
(binding * (bool * binding option * string) list * mixfix) list) list |
23152 | 12 |
-> theory -> theory |
31161
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
13 |
val add_domain: string -> |
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
14 |
((string * string option) list * binding * mixfix * |
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
15 |
(binding * (bool * binding option * typ) list * mixfix) list) list |
23152 | 16 |
-> theory -> theory |
17 |
end; |
|
18 |
||
31023 | 19 |
structure Domain_Extender :> DOMAIN_EXTENDER = |
23152 | 20 |
struct |
21 |
||
22 |
open Domain_Library; |
|
23 |
||
24 |
(* ----- general testing and preprocessing of constructor list -------------- *) |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
25 |
fun check_and_sort_domain |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
26 |
(dtnvs : (string * typ list) list) |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
27 |
(cons'' : ((binding * (bool * binding option * typ) list * mixfix) list) list) |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
28 |
(sg : theory) |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
29 |
: ((string * typ list) * |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
30 |
(binding * (bool * binding option * typ) list * mixfix) list) list = |
23152 | 31 |
let |
32 |
val defaultS = Sign.defaultS sg; |
|
33 |
val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of |
|
34 |
[] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
35 |
val test_dupl_cons = (case duplicates (op =) (map (Binding.name_of o first) (List.concat cons'')) of |
23152 | 36 |
[] => false | dups => error ("Duplicate constructors: " |
37 |
^ commas_quote dups)); |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
38 |
val test_dupl_sels = (case duplicates (op =) (map Binding.name_of (List.mapPartial second |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
39 |
(List.concat (map second (List.concat cons''))))) of |
23152 | 40 |
[] => false | dups => error("Duplicate selectors: "^commas_quote dups)); |
41 |
val test_dupl_tvars = exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of |
|
42 |
[] => false | dups => error("Duplicate type arguments: " |
|
43 |
^commas_quote dups)) (map snd dtnvs); |
|
44 |
(* test for free type variables, illegal sort constraints on rhs, |
|
45 |
non-pcpo-types and invalid use of recursive type; |
|
46 |
replace sorts in type variables on rhs *) |
|
47 |
fun analyse_equation ((dname,typevars),cons') = |
|
48 |
let |
|
49 |
val tvars = map dest_TFree typevars; |
|
50 |
val distinct_typevars = map TFree tvars; |
|
51 |
fun rm_sorts (TFree(s,_)) = TFree(s,[]) |
|
52 |
| rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) |
|
53 |
| rm_sorts (TVar(s,_)) = TVar(s,[]) |
|
54 |
and remove_sorts l = map rm_sorts l; |
|
55 |
val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"] |
|
56 |
fun analyse indirect (TFree(v,s)) = (case AList.lookup (op =) tvars v of |
|
57 |
NONE => error ("Free type variable " ^ quote v ^ " on rhs.") |
|
58 |
| SOME sort => if eq_set_string (s,defaultS) orelse |
|
59 |
eq_set_string (s,sort ) |
|
60 |
then TFree(v,sort) |
|
61 |
else error ("Inconsistent sort constraint" ^ |
|
62 |
" for type variable " ^ quote v)) |
|
63 |
| analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of |
|
64 |
NONE => if s mem indirect_ok |
|
65 |
then Type(s,map (analyse false) typl) |
|
66 |
else Type(s,map (analyse true) typl) |
|
67 |
| SOME typevars => if indirect |
|
68 |
then error ("Indirect recursion of type " ^ |
|
69 |
quote (string_of_typ sg t)) |
|
70 |
else if dname <> s orelse (** BUG OR FEATURE?: |
|
71 |
mutual recursion may use different arguments **) |
|
72 |
remove_sorts typevars = remove_sorts typl |
|
73 |
then Type(s,map (analyse true) typl) |
|
74 |
else error ("Direct recursion of type " ^ |
|
75 |
quote (string_of_typ sg t) ^ |
|
76 |
" with different arguments")) |
|
77 |
| analyse indirect (TVar _) = Imposs "extender:analyse"; |
|
78 |
fun check_pcpo T = if pcpo_type sg T then T |
|
79 |
else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T); |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
80 |
val analyse_con = upd_second (map (upd_third (check_pcpo o analyse false))); |
23152 | 81 |
in ((dname,distinct_typevars), map analyse_con cons') end; |
82 |
in ListPair.map analyse_equation (dtnvs,cons'') |
|
83 |
end; (* let *) |
|
84 |
||
85 |
(* ----- calls for building new thy and thms -------------------------------- *) |
|
86 |
||
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
87 |
fun gen_add_domain |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
88 |
(prep_typ : theory -> 'a -> typ) |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
89 |
(comp_dnam : string) |
31161
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
90 |
(eqs''' : ((string * string option) list * binding * mixfix * |
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
91 |
(binding * (bool * binding option * 'a) list * mixfix) list) list) |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
92 |
(thy''' : theory) = |
23152 | 93 |
let |
31161
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
94 |
fun readS (SOME s) = Syntax.read_sort_global thy''' s |
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
95 |
| readS NONE = Sign.defaultS thy'''; |
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
96 |
fun readTFree (a, s) = TFree (a, readS s); |
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
97 |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
98 |
val dtnvs = map (fn (vs,dname:binding,mx,_) => |
31161
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
99 |
(dname, map readTFree vs, mx)) eqs'''; |
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
100 |
val cons''' = map (fn (_,_,_,cons) => cons) eqs'''; |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
101 |
fun thy_type (dname,tvars,mx) = (dname, length tvars, mx); |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
102 |
fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS); |
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
103 |
val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs) |
24926
bcb6b098df11
AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24867
diff
changeset
|
104 |
|> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; |
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
105 |
val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons'''; |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
106 |
val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs; |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
107 |
val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list = check_and_sort_domain dtnvs' cons'' thy''; |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
108 |
val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs'; |
23152 | 109 |
val dts = map (Type o fst) eqs'; |
110 |
val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; |
|
111 |
fun strip ss = Library.drop (find_index_eq "'" ss +1, ss); |
|
112 |
fun typid (Type (id,_)) = |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
113 |
let val c = hd (Symbol.explode (Long_Name.base_name id)) |
23152 | 114 |
in if Symbol.is_letter c then c else "t" end |
115 |
| typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id))) |
|
116 |
| typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
117 |
fun one_con (con,args,mx) = |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
118 |
((Syntax.const_name mx (Binding.name_of con)), |
23152 | 119 |
ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy, |
120 |
find_index_eq tp dts, |
|
121 |
DatatypeAux.dtyp_of_typ new_dts tp), |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
122 |
Option.map Binding.name_of sel,vn)) |
23152 | 123 |
(args,(mk_var_names(map (typid o third) args))) |
124 |
) : cons; |
|
125 |
val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list; |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
126 |
val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs; |
28536 | 127 |
val ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn eq => |
128 |
Domain_Theorems.theorems (eq, eqs)) eqs |
|
129 |
||>> Domain_Theorems.comp_theorems (comp_dnam, eqs); |
|
23152 | 130 |
in |
131 |
theorems_thy |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
132 |
|> Sign.add_path (Long_Name.base_name comp_dnam) |
29585 | 133 |
|> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])])) |
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24707
diff
changeset
|
134 |
|> Sign.parent_path |
23152 | 135 |
end; |
136 |
||
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
137 |
val add_domain = gen_add_domain Sign.certify_typ; |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
138 |
val add_domain_cmd = gen_add_domain Syntax.read_typ_global; |
23152 | 139 |
|
140 |
||
141 |
(** outer syntax **) |
|
142 |
||
143 |
local structure P = OuterParse and K = OuterKeyword in |
|
144 |
||
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
24926
diff
changeset
|
145 |
val _ = OuterKeyword.keyword "lazy"; |
24867 | 146 |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
147 |
val dest_decl : (bool * binding option * string) parser = |
23152 | 148 |
P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false -- |
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
149 |
(P.binding >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1 |
23152 | 150 |
|| P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")" |
151 |
>> (fn t => (true,NONE,t)) |
|
152 |
|| P.typ >> (fn t => (false,NONE,t)); |
|
153 |
||
154 |
val cons_decl = |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
155 |
P.binding -- Scan.repeat dest_decl -- P.opt_mixfix; |
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
156 |
|
31161
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
157 |
val type_var' : (string * string option) parser = |
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
158 |
(P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort)); |
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
159 |
|
31161
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
160 |
val type_args' : (string * string option) list parser = |
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
161 |
type_var' >> single || |
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
162 |
P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") || |
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
163 |
Scan.succeed []; |
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
164 |
|
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
165 |
val domain_decl = |
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
166 |
(type_args' -- P.binding -- P.opt_infix) -- |
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
167 |
(P.$$$ "=" |-- P.enum1 "|" cons_decl); |
23152 | 168 |
|
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
169 |
val domains_decl = |
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
170 |
Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- |
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
171 |
P.and_list1 domain_decl; |
23152 | 172 |
|
31161
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
173 |
fun mk_domain (opt_name : string option, |
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
174 |
doms : ((((string * string option) list * binding) * mixfix) * |
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
175 |
((binding * (bool * binding option * string) list) * mixfix) list) list ) = |
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
176 |
let |
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
177 |
val names = map (fn (((_, t), _), _) => Binding.name_of t) doms; |
31161
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
178 |
val specs : ((string * string option) list * binding * mixfix * |
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
179 |
(binding * (bool * binding option * string) list * mixfix) list) list = |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
180 |
map (fn (((vs, t), mx), cons) => |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
181 |
(vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms; |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
182 |
val comp_dnam = |
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
183 |
case opt_name of NONE => space_implode "_" names | SOME s => s; |
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
184 |
in add_domain_cmd comp_dnam specs end; |
23152 | 185 |
|
24867 | 186 |
val _ = |
23152 | 187 |
OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl |
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
188 |
(domains_decl >> (Toplevel.theory o mk_domain)); |
23152 | 189 |
|
24867 | 190 |
end; |
23152 | 191 |
|
192 |
end; |