11 domain empty = silly empty |
11 domain empty = silly empty |
12 yields |
12 yields |
13 Exception- |
13 Exception- |
14 TERM |
14 TERM |
15 ("typ_of_term: bad encoding of type", |
15 ("typ_of_term: bad encoding of type", |
16 [Abs ("uu", "_", Const ("None", "_"))]) raised |
16 [Abs ("uu", "_", Const ("NONE", "_"))]) raised |
17 but this works fine: |
17 but this works fine: |
18 domain Empty = silly Empty |
18 domain Empty = silly Empty |
19 |
19 |
20 strange syntax errors are produced for: |
20 strange syntax errors are produced for: |
21 domain xx = xx ("x yy") |
21 domain xx = xx ("x yy") |
65 fun rm_sorts (TFree(s,_)) = TFree(s,[]) |
65 fun rm_sorts (TFree(s,_)) = TFree(s,[]) |
66 | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) |
66 | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) |
67 | rm_sorts (TVar(s,_)) = TVar(s,[]) |
67 | rm_sorts (TVar(s,_)) = TVar(s,[]) |
68 and remove_sorts l = map rm_sorts l; |
68 and remove_sorts l = map rm_sorts l; |
69 fun analyse indirect (TFree(v,s)) = (case assoc_string(tvars,v) of |
69 fun analyse indirect (TFree(v,s)) = (case assoc_string(tvars,v) of |
70 None => error ("Free type variable " ^ quote v ^ " on rhs.") |
70 NONE => error ("Free type variable " ^ quote v ^ " on rhs.") |
71 | Some sort => if eq_set_string (s,defaultS) orelse |
71 | SOME sort => if eq_set_string (s,defaultS) orelse |
72 eq_set_string (s,sort ) |
72 eq_set_string (s,sort ) |
73 then TFree(distinct_name v,sort) |
73 then TFree(distinct_name v,sort) |
74 else error ("Inconsistent sort constraint" ^ |
74 else error ("Inconsistent sort constraint" ^ |
75 " for type variable " ^ quote v)) |
75 " for type variable " ^ quote v)) |
76 | analyse indirect (t as Type(s,typl)) = (case assoc_string(dtnvs,s)of |
76 | analyse indirect (t as Type(s,typl)) = (case assoc_string(dtnvs,s)of |
77 None => Type(s,map (analyse true) typl) |
77 NONE => Type(s,map (analyse true) typl) |
78 | Some typevars => if indirect |
78 | SOME typevars => if indirect |
79 then error ("Indirect recursion of type " ^ |
79 then error ("Indirect recursion of type " ^ |
80 quote (string_of_typ sg t)) |
80 quote (string_of_typ sg t)) |
81 else if dname <> s orelse (** BUG OR FEATURE?: |
81 else if dname <> s orelse (** BUG OR FEATURE?: |
82 mutual recursion may use different arguments **) |
82 mutual recursion may use different arguments **) |
83 remove_sorts typevars = remove_sorts typl |
83 remove_sorts typevars = remove_sorts typl |
158 val domain_decl = (type_args' -- P.name >> Library.swap) -- |
158 val domain_decl = (type_args' -- P.name >> Library.swap) -- |
159 (P.$$$ "=" |-- P.enum1 "|" cons_decl); |
159 (P.$$$ "=" |-- P.enum1 "|" cons_decl); |
160 val domains_decl = |
160 val domains_decl = |
161 Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl |
161 Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl |
162 >> (fn (opt_name, doms) => |
162 >> (fn (opt_name, doms) => |
163 (case opt_name of None => space_implode "_" (map (#1 o #1) doms) | Some s => s, doms)); |
163 (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms)); |
164 |
164 |
165 val domainP = |
165 val domainP = |
166 OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl |
166 OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl |
167 (domains_decl >> (Toplevel.theory o add_domain)); |
167 (domains_decl >> (Toplevel.theory o add_domain)); |
168 |
168 |