author | wenzelm |
Wed, 25 May 2005 09:44:34 +0200 | |
changeset 16070 | 4a83dd540b88 |
parent 15601 | 2de79f493856 |
child 16394 | 495dbcd4f4c9 |
permissions | -rw-r--r-- |
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
1 |
(* Title: HOLCF/domain/extender.ML |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
2 |
ID: $Id$ |
14097 | 3 |
Author: David von Oheimb |
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
4 |
|
12037 | 5 |
Theory extender for domain section, including new-style theory syntax. |
15187 | 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", |
|
15531 | 15 |
[Abs ("uu", "_", Const ("NONE", "_"))]) raised |
15187 | 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 |
||
1274 | 24 |
*) |
25 |
||
12037 | 26 |
signature DOMAIN_EXTENDER = |
27 |
sig |
|
28 |
val add_domain: string * |
|
29 |
((bstring * string list) * (string * mixfix * (bool * string * string) list) list) list |
|
30 |
-> theory -> theory |
|
31 |
end; |
|
2446
c2a9bf6c0948
The previous log message was wrong. The correct one is:
oheimb
parents:
2445
diff
changeset
|
32 |
|
12037 | 33 |
structure Domain_Extender: DOMAIN_EXTENDER = |
1274 | 34 |
struct |
35 |
||
36 |
open Domain_Library; |
|
37 |
||
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
38 |
(* ----- general testing and preprocessing of constructor list -------------- *) |
1274 | 39 |
|
15187 | 40 |
fun check_and_sort_domain (dtnvs: (string * typ list) list, |
41 |
cons'' : ((string * mixfix * (bool*string*typ) list) list) list) sg = |
|
4008 | 42 |
let |
7653 | 43 |
val defaultS = Sign.defaultS sg; |
1274 | 44 |
val test_dupl_typs = (case duplicates (map fst dtnvs) of |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
45 |
[] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); |
15570 | 46 |
val test_dupl_cons = (case duplicates (map first (List.concat cons'')) of |
4008 | 47 |
[] => false | dups => error ("Duplicate constructors: " |
48 |
^ commas_quote dups)); |
|
49 |
val test_dupl_sels = (case duplicates |
|
15570 | 50 |
(map second (List.concat (map third (List.concat cons'')))) of |
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
51 |
[] => false | dups => error("Duplicate selectors: "^commas_quote dups)); |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
52 |
val test_dupl_tvars = exists(fn s=>case duplicates(map(fst o rep_TFree)s)of |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
53 |
[] => false | dups => error("Duplicate type arguments: " |
4008 | 54 |
^commas_quote dups)) (map snd dtnvs); |
55 |
(* test for free type variables, illegal sort constraints on rhs, |
|
56 |
non-pcpo-types and invalid use of recursive type; |
|
57 |
replace sorts in type variables on rhs *) |
|
58 |
fun analyse_equation ((dname,typevars),cons') = |
|
59 |
let |
|
60 |
val tvars = map rep_TFree typevars; |
|
4030 | 61 |
fun distinct_name s = "'"^Sign.base_name dname^"_"^s; |
62 |
val distinct_typevars = map (fn (n,sort) => |
|
63 |
TFree (distinct_name n,sort)) tvars; |
|
4008 | 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; |
|
15601
2de79f493856
domain package now permits indirect recursion with these type constructors: *, ->, ++, **, u
huffman
parents:
15570
diff
changeset
|
68 |
val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"] |
15187 | 69 |
fun analyse indirect (TFree(v,s)) = (case assoc_string(tvars,v) of |
15531 | 70 |
NONE => error ("Free type variable " ^ quote v ^ " on rhs.") |
71 |
| SOME sort => if eq_set_string (s,defaultS) orelse |
|
4030 | 72 |
eq_set_string (s,sort ) |
73 |
then TFree(distinct_name v,sort) |
|
14097 | 74 |
else error ("Inconsistent sort constraint" ^ |
75 |
" for type variable " ^ quote v)) |
|
15187 | 76 |
| analyse indirect (t as Type(s,typl)) = (case assoc_string(dtnvs,s)of |
15601
2de79f493856
domain package now permits indirect recursion with these type constructors: *, ->, ++, **, u
huffman
parents:
15570
diff
changeset
|
77 |
NONE => if exists (fn x => x = s) indirect_ok |
2de79f493856
domain package now permits indirect recursion with these type constructors: *, ->, ++, **, u
huffman
parents:
15570
diff
changeset
|
78 |
then Type(s,map (analyse false) typl) |
2de79f493856
domain package now permits indirect recursion with these type constructors: *, ->, ++, **, u
huffman
parents:
15570
diff
changeset
|
79 |
else Type(s,map (analyse true) typl) |
15531 | 80 |
| SOME typevars => if indirect |
15187 | 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) ^ |
|
4753 | 89 |
" with different arguments")) |
15187 | 90 |
| analyse indirect (TVar _) = Imposs "extender:analyse"; |
4753 | 91 |
fun check_pcpo t = (pcpo_type sg t orelse error( |
14097 | 92 |
"Constructor argument type is not of sort pcpo: "^string_of_typ sg t); t); |
15187 | 93 |
val analyse_con = upd_third (map (upd_third (check_pcpo o analyse false))); |
4030 | 94 |
in ((dname,distinct_typevars), map analyse_con cons') end; |
4008 | 95 |
in ListPair.map analyse_equation (dtnvs,cons'') |
96 |
end; (* let *) |
|
97 |
||
4030 | 98 |
(* ----- calls for building new thy and thms -------------------------------- *) |
1274 | 99 |
|
4008 | 100 |
fun add_domain (comp_dnam,eqs''') thy''' = let |
101 |
val sg''' = sign_of thy'''; |
|
102 |
val dtnvs = map ((fn (dname,vs) => |
|
103 |
(Sign.full_name sg''' dname,map (str2typ sg''') vs)) |
|
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 rep_TFree) tvars, pcpoS); |
|
108 |
val thy'' = thy''' |> Theory.add_types (map thy_type dtnvs) |
|
109 |
|> Theory.add_arities_i (map thy_arity dtnvs); |
|
110 |
val sg'' = sign_of thy''; |
|
111 |
val cons''=map (map (upd_third (map (upd_third (str2typ sg''))))) cons'''; |
|
112 |
val eqs' = check_and_sort_domain (dtnvs,cons'') sg''; |
|
113 |
val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs'); |
|
1274 | 114 |
val dts = map (Type o fst) eqs'; |
15570 | 115 |
fun strip ss = Library.drop (find_index_eq "'" ss +1, ss); |
11728 | 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)); |
|
1274 | 121 |
fun cons cons' = (map (fn (con,syn,args) => |
4122 | 122 |
((Syntax.const_name con syn), |
4008 | 123 |
ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy, |
4188
1025a27b08f9
changed libraray function find to find_index_eq, currying it
oheimb
parents:
4122
diff
changeset
|
124 |
find_index_eq tp dts), |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
125 |
sel,vn)) |
4122 | 126 |
(args,(mk_var_names(map (typid o third) args))) |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
127 |
)) cons') : cons list; |
1274 | 128 |
val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list; |
4122 | 129 |
val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs); |
12037 | 130 |
val (theorems_thy, (rewss, take_rews)) = (foldl_map (fn (thy0,eq) => |
131 |
Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs)) |
|
132 |
|>>> Domain_Theorems.comp_theorems (comp_dnam, eqs); |
|
133 |
in |
|
134 |
theorems_thy |
|
135 |
|> Theory.add_path (Sign.base_name comp_dnam) |
|
15570 | 136 |
|> (#1 o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])])) |
12037 | 137 |
|> Theory.parent_path |
138 |
end; |
|
139 |
||
140 |
||
141 |
||
142 |
(** outer syntax **) |
|
143 |
||
144 |
local structure P = OuterParse and K = OuterSyntax.Keyword in |
|
145 |
||
146 |
val dest_decl = |
|
147 |
P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false -- |
|
148 |
P.name -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1; |
|
1274 | 149 |
|
12037 | 150 |
val cons_decl = |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12037
diff
changeset
|
151 |
P.name -- Scan.repeat dest_decl -- P.opt_mixfix |
12037 | 152 |
>> (fn ((c, ds), mx) => (c, mx, ds)); |
153 |
||
14097 | 154 |
val type_var' = (P.type_ident ^^ |
155 |
Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) ""); |
|
156 |
val type_args' = type_var' >> single || |
|
157 |
P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") || |
|
158 |
Scan.succeed []; |
|
159 |
||
160 |
val domain_decl = (type_args' -- P.name >> Library.swap) -- |
|
161 |
(P.$$$ "=" |-- P.enum1 "|" cons_decl); |
|
12037 | 162 |
val domains_decl = |
163 |
Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl |
|
164 |
>> (fn (opt_name, doms) => |
|
15531 | 165 |
(case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms)); |
12037 | 166 |
|
167 |
val domainP = |
|
168 |
OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl |
|
169 |
(domains_decl >> (Toplevel.theory o add_domain)); |
|
170 |
||
171 |
||
172 |
val _ = OuterSyntax.add_keywords ["lazy"]; |
|
173 |
val _ = OuterSyntax.add_parsers [domainP]; |
|
174 |
||
175 |
end; |
|
176 |
||
177 |
end; |