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