author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 14097 | f4d2ff3cad09 |
child 15187 | 8b74a39dba89 |
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. |
1274 | 6 |
*) |
7 |
||
12037 | 8 |
signature DOMAIN_EXTENDER = |
9 |
sig |
|
10 |
val add_domain: string * |
|
11 |
((bstring * string list) * (string * mixfix * (bool * string * string) list) list) list |
|
12 |
-> theory -> theory |
|
13 |
end; |
|
2446
c2a9bf6c0948
The previous log message was wrong. The correct one is:
oheimb
parents:
2445
diff
changeset
|
14 |
|
12037 | 15 |
structure Domain_Extender: DOMAIN_EXTENDER = |
1274 | 16 |
struct |
17 |
||
18 |
open Domain_Library; |
|
19 |
||
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
20 |
(* ----- general testing and preprocessing of constructor list -------------- *) |
1274 | 21 |
|
4008 | 22 |
fun check_and_sort_domain (dtnvs: (string * typ list) list, cons'' : |
4122 | 23 |
((string * mixfix * (bool*string*typ) list) list) list) sg = |
4008 | 24 |
let |
7653 | 25 |
val defaultS = Sign.defaultS sg; |
1274 | 26 |
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
|
27 |
[] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); |
4008 | 28 |
val test_dupl_cons = (case duplicates (map first (flat cons'')) of |
29 |
[] => false | dups => error ("Duplicate constructors: " |
|
30 |
^ commas_quote dups)); |
|
31 |
val test_dupl_sels = (case duplicates |
|
32 |
(map second (flat (map third (flat cons'')))) of |
|
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
33 |
[] => 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
|
34 |
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
|
35 |
[] => false | dups => error("Duplicate type arguments: " |
4008 | 36 |
^commas_quote dups)) (map snd dtnvs); |
37 |
(* test for free type variables, illegal sort constraints on rhs, |
|
38 |
non-pcpo-types and invalid use of recursive type; |
|
39 |
replace sorts in type variables on rhs *) |
|
40 |
fun analyse_equation ((dname,typevars),cons') = |
|
41 |
let |
|
42 |
val tvars = map rep_TFree typevars; |
|
4030 | 43 |
fun distinct_name s = "'"^Sign.base_name dname^"_"^s; |
44 |
val distinct_typevars = map (fn (n,sort) => |
|
45 |
TFree (distinct_name n,sort)) tvars; |
|
4008 | 46 |
fun rm_sorts (TFree(s,_)) = TFree(s,[]) |
47 |
| rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) |
|
48 |
| rm_sorts (TVar(s,_)) = TVar(s,[]) |
|
49 |
and remove_sorts l = map rm_sorts l; |
|
50 |
fun analyse(TFree(v,s)) = (case assoc_string(tvars,v) of |
|
14097 | 51 |
None => error ("Free type variable " ^ quote v ^ " on rhs.") |
4008 | 52 |
| Some sort => if eq_set_string (s,defaultS) orelse |
4030 | 53 |
eq_set_string (s,sort ) |
54 |
then TFree(distinct_name v,sort) |
|
14097 | 55 |
else error ("Inconsistent sort constraint" ^ |
56 |
" for type variable " ^ quote v)) |
|
4753 | 57 |
(** BUG OR FEATURE?: mutual recursion may use different arguments **) |
58 |
| analyse(Type(s,typl)) = (case assoc_string((*dtnvs*) |
|
59 |
[(dname,typevars)],s) of |
|
60 |
None => Type(s,map analyse typl) |
|
61 |
| Some typevars => if remove_sorts typevars = remove_sorts typl |
|
62 |
then Type(s,map analyse typl) |
|
14097 | 63 |
else error ("Recursion of type " ^ quote s ^ |
4753 | 64 |
" with different arguments")) |
65 |
| analyse(TVar _) = Imposs "extender:analyse"; |
|
66 |
fun check_pcpo t = (pcpo_type sg t orelse error( |
|
14097 | 67 |
"Constructor argument type is not of sort pcpo: "^string_of_typ sg t); t); |
4008 | 68 |
val analyse_con = upd_third (map (upd_third (check_pcpo o analyse))); |
4030 | 69 |
in ((dname,distinct_typevars), map analyse_con cons') end; |
4008 | 70 |
in ListPair.map analyse_equation (dtnvs,cons'') |
71 |
end; (* let *) |
|
72 |
||
4030 | 73 |
(* ----- calls for building new thy and thms -------------------------------- *) |
1274 | 74 |
|
4008 | 75 |
fun add_domain (comp_dnam,eqs''') thy''' = let |
76 |
val sg''' = sign_of thy'''; |
|
77 |
val dtnvs = map ((fn (dname,vs) => |
|
78 |
(Sign.full_name sg''' dname,map (str2typ sg''') vs)) |
|
79 |
o fst) eqs'''; |
|
80 |
val cons''' = map snd eqs'''; |
|
81 |
fun thy_type (dname,tvars) = (Sign.base_name dname, length tvars, NoSyn); |
|
82 |
fun thy_arity (dname,tvars) = (dname, map (snd o rep_TFree) tvars, pcpoS); |
|
83 |
val thy'' = thy''' |> Theory.add_types (map thy_type dtnvs) |
|
84 |
|> Theory.add_arities_i (map thy_arity dtnvs); |
|
85 |
val sg'' = sign_of thy''; |
|
86 |
val cons''=map (map (upd_third (map (upd_third (str2typ sg''))))) cons'''; |
|
87 |
val eqs' = check_and_sort_domain (dtnvs,cons'') sg''; |
|
88 |
val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs'); |
|
1274 | 89 |
val dts = map (Type o fst) eqs'; |
4188
1025a27b08f9
changed libraray function find to find_index_eq, currying it
oheimb
parents:
4122
diff
changeset
|
90 |
fun strip ss = drop (find_index_eq "'" ss +1, ss); |
11728 | 91 |
fun typid (Type (id,_)) = |
92 |
let val c = hd (Symbol.explode (Sign.base_name id)) |
|
93 |
in if Symbol.is_letter c then c else "t" end |
|
94 |
| typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id))) |
|
95 |
| typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); |
|
1274 | 96 |
fun cons cons' = (map (fn (con,syn,args) => |
4122 | 97 |
((Syntax.const_name con syn), |
4008 | 98 |
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
|
99 |
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
|
100 |
sel,vn)) |
4122 | 101 |
(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
|
102 |
)) cons') : cons list; |
1274 | 103 |
val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list; |
4122 | 104 |
val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs); |
12037 | 105 |
val (theorems_thy, (rewss, take_rews)) = (foldl_map (fn (thy0,eq) => |
106 |
Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs)) |
|
107 |
|>>> Domain_Theorems.comp_theorems (comp_dnam, eqs); |
|
108 |
in |
|
109 |
theorems_thy |
|
110 |
|> Theory.add_path (Sign.base_name comp_dnam) |
|
111 |
|> (#1 o (PureThy.add_thmss [(("rews", flat rewss @ take_rews), [])])) |
|
112 |
|> Theory.parent_path |
|
113 |
end; |
|
114 |
||
115 |
||
116 |
||
117 |
(** outer syntax **) |
|
118 |
||
119 |
local structure P = OuterParse and K = OuterSyntax.Keyword in |
|
120 |
||
121 |
val dest_decl = |
|
122 |
P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false -- |
|
123 |
P.name -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1; |
|
1274 | 124 |
|
12037 | 125 |
val cons_decl = |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12037
diff
changeset
|
126 |
P.name -- Scan.repeat dest_decl -- P.opt_mixfix |
12037 | 127 |
>> (fn ((c, ds), mx) => (c, mx, ds)); |
128 |
||
14097 | 129 |
val type_var' = (P.type_ident ^^ |
130 |
Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) ""); |
|
131 |
val type_args' = type_var' >> single || |
|
132 |
P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") || |
|
133 |
Scan.succeed []; |
|
134 |
||
135 |
val domain_decl = (type_args' -- P.name >> Library.swap) -- |
|
136 |
(P.$$$ "=" |-- P.enum1 "|" cons_decl); |
|
12037 | 137 |
val domains_decl = |
138 |
Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl |
|
139 |
>> (fn (opt_name, doms) => |
|
140 |
(case opt_name of None => space_implode "_" (map (#1 o #1) doms) | Some s => s, doms)); |
|
141 |
||
142 |
val domainP = |
|
143 |
OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl |
|
144 |
(domains_decl >> (Toplevel.theory o add_domain)); |
|
145 |
||
146 |
||
147 |
val _ = OuterSyntax.add_keywords ["lazy"]; |
|
148 |
val _ = OuterSyntax.add_parsers [domainP]; |
|
149 |
||
150 |
end; |
|
151 |
||
152 |
end; |