src/HOLCF/Tools/domain/domain_extender.ML
author huffman
Thu, 21 May 2009 18:23:19 -0700
changeset 31228 bcacfd816d28
parent 31163 19c2f68ae23d
child 31229 8a890890d143
permissions -rw-r--r--
make type Domain_Library.arg abstract
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
    Author:     David von Oheimb
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     3
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     4
Theory extender for domain command, including theory syntax.
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     5
*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     6
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     7
signature DOMAIN_EXTENDER =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     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
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    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
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    16
    -> theory -> theory
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    17
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    18
31023
d027411c9a38 use opaque ascription for all HOLCF code
huffman
parents: 30919
diff changeset
    19
structure Domain_Extender :> DOMAIN_EXTENDER =
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    20
struct
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    21
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    22
open Domain_Library;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    23
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    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)
31163
19c2f68ae23d allow lazy domain arguments to have class cpo
huffman
parents: 31161
diff changeset
    27
  (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
30919
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
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    31
  let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    32
    val defaultS = Sign.defaultS sg;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    33
    val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    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
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    36
	[] => false | dups => error ("Duplicate constructors: " 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    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
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    40
        [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    41
    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
    42
	[] => false | dups => error("Duplicate type arguments: " 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    43
		   ^commas_quote dups)) (map snd dtnvs);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    44
    (* test for free type variables, illegal sort constraints on rhs,
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    45
	       non-pcpo-types and invalid use of recursive type;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    46
       replace sorts in type variables on rhs *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    47
    fun analyse_equation ((dname,typevars),cons') = 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    48
      let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    49
	val tvars = map dest_TFree typevars;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    50
	val distinct_typevars = map TFree tvars;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    51
	fun rm_sorts (TFree(s,_)) = TFree(s,[])
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    52
	|   rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    53
	|   rm_sorts (TVar(s,_))  = TVar(s,[])
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    54
	and remove_sorts l = map rm_sorts l;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    55
	val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    56
	fun analyse indirect (TFree(v,s))  = (case AList.lookup (op =) tvars v of 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    57
		    NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    58
	          | SOME sort => if eq_set_string (s,defaultS) orelse
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    59
				    eq_set_string (s,sort    )
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    60
				 then TFree(v,sort)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    61
				 else error ("Inconsistent sort constraint" ^
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    62
				             " for type variable " ^ quote v))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    63
        |   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
    64
		NONE          => if s mem indirect_ok
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    65
				 then Type(s,map (analyse false) typl)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    66
				 else Type(s,map (analyse true) typl)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    67
	      | SOME typevars => if indirect 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    68
                           then error ("Indirect recursion of type " ^ 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    69
				        quote (string_of_typ sg t))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    70
                           else if dname <> s orelse (** BUG OR FEATURE?: 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    71
                                mutual recursion may use different arguments **)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    72
				   remove_sorts typevars = remove_sorts typl 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    73
				then Type(s,map (analyse true) typl)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    74
				else error ("Direct recursion of type " ^ 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    75
					     quote (string_of_typ sg t) ^ 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    76
					    " with different arguments"))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    77
        |   analyse indirect (TVar _) = Imposs "extender:analyse";
31163
19c2f68ae23d allow lazy domain arguments to have class cpo
huffman
parents: 31161
diff changeset
    78
        fun check_pcpo lazy T =
19c2f68ae23d allow lazy domain arguments to have class cpo
huffman
parents: 31161
diff changeset
    79
          let val ok = if lazy then cpo_type else pcpo_type
19c2f68ae23d allow lazy domain arguments to have class cpo
huffman
parents: 31161
diff changeset
    80
          in if ok sg T then T else error
19c2f68ae23d allow lazy domain arguments to have class cpo
huffman
parents: 31161
diff changeset
    81
            ("Constructor argument type is not of sort pcpo: " ^
19c2f68ae23d allow lazy domain arguments to have class cpo
huffman
parents: 31161
diff changeset
    82
              string_of_typ sg T)
19c2f68ae23d allow lazy domain arguments to have class cpo
huffman
parents: 31161
diff changeset
    83
          end;
19c2f68ae23d allow lazy domain arguments to have class cpo
huffman
parents: 31161
diff changeset
    84
        fun analyse_arg (lazy, sel, T) =
19c2f68ae23d allow lazy domain arguments to have class cpo
huffman
parents: 31161
diff changeset
    85
          (lazy, sel, check_pcpo lazy (analyse false T));
19c2f68ae23d allow lazy domain arguments to have class cpo
huffman
parents: 31161
diff changeset
    86
        fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    87
      in ((dname,distinct_typevars), map analyse_con cons') end; 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    88
  in ListPair.map analyse_equation (dtnvs,cons'')
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    89
  end; (* let *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    90
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    91
(* ----- calls for building new thy and thms -------------------------------- *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    92
30919
dcf8a7a66bd1 make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents: 30916
diff changeset
    93
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
    94
  (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
    95
  (comp_dnam : string)
31161
a27d4254ff4c fix domain package parsing of lhs sort constraints
huffman
parents: 31023
diff changeset
    96
  (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
    97
              (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
    98
  (thy''' : theory) =
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    99
  let
31161
a27d4254ff4c fix domain package parsing of lhs sort constraints
huffman
parents: 31023
diff changeset
   100
    fun readS (SOME s) = Syntax.read_sort_global thy''' s
a27d4254ff4c fix domain package parsing of lhs sort constraints
huffman
parents: 31023
diff changeset
   101
      | readS NONE = Sign.defaultS thy''';
a27d4254ff4c fix domain package parsing of lhs sort constraints
huffman
parents: 31023
diff changeset
   102
    fun readTFree (a, s) = TFree (a, readS s);
a27d4254ff4c fix domain package parsing of lhs sort constraints
huffman
parents: 31023
diff changeset
   103
30919
dcf8a7a66bd1 make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents: 30916
diff changeset
   104
    val dtnvs = map (fn (vs,dname:binding,mx,_) => 
31161
a27d4254ff4c fix domain package parsing of lhs sort constraints
huffman
parents: 31023
diff changeset
   105
                  (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
   106
    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
   107
    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
   108
    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
   109
    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
   110
		       |> 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
   111
    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
   112
    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
   113
    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
   114
    val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   115
    val dts  = map (Type o fst) eqs';
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   116
    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
   117
    fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   118
    fun typid (Type  (id,_)) =
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   119
          let val c = hd (Symbol.explode (Long_Name.base_name id))
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   120
          in if Symbol.is_letter c then c else "t" end
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   121
      | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   122
      | 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
   123
    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
   124
	((Syntax.const_name mx (Binding.name_of con)),
31228
bcacfd816d28 make type Domain_Library.arg abstract
huffman
parents: 31163
diff changeset
   125
	 ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy,
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   126
					find_index_eq tp dts,
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   127
					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
   128
					Option.map Binding.name_of sel,vn))
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   129
	     (args,(mk_var_names(map (typid o third) args)))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   130
	 ) : cons;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   131
    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
   132
    val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs;
28536
8dccb6035d0f established canonical argument order
haftmann
parents: 27353
diff changeset
   133
    val ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn eq =>
8dccb6035d0f established canonical argument order
haftmann
parents: 27353
diff changeset
   134
      Domain_Theorems.theorems (eq, eqs)) eqs
8dccb6035d0f established canonical argument order
haftmann
parents: 27353
diff changeset
   135
      ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   136
  in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   137
    theorems_thy
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   138
    |> Sign.add_path (Long_Name.base_name comp_dnam)
29585
c23295521af5 binding replaces bstring
haftmann
parents: 28965
diff changeset
   139
    |> (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
   140
    |> Sign.parent_path
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   141
  end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   142
30919
dcf8a7a66bd1 make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents: 30916
diff changeset
   143
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
   144
val add_domain_cmd = gen_add_domain Syntax.read_typ_global;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   145
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   146
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   147
(** outer syntax **)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   148
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   149
local structure P = OuterParse and K = OuterKeyword in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   150
27353
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 24926
diff changeset
   151
val _ = OuterKeyword.keyword "lazy";
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24712
diff changeset
   152
30919
dcf8a7a66bd1 make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents: 30916
diff changeset
   153
val dest_decl : (bool * binding option * string) parser =
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   154
  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
   155
    (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   156
  || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   157
       >> (fn t => (true,NONE,t))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   158
  || P.typ >> (fn t => (false,NONE,t));
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 cons_decl =
30919
dcf8a7a66bd1 make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents: 30916
diff changeset
   161
  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
   162
31161
a27d4254ff4c fix domain package parsing of lhs sort constraints
huffman
parents: 31023
diff changeset
   163
val type_var' : (string * string option) parser =
a27d4254ff4c fix domain package parsing of lhs sort constraints
huffman
parents: 31023
diff changeset
   164
  (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
   165
31161
a27d4254ff4c fix domain package parsing of lhs sort constraints
huffman
parents: 31023
diff changeset
   166
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
   167
  type_var' >> single ||
a3d2128cac92 allow infix declarations for type constructors defined with domain package
huffman
parents: 30915
diff changeset
   168
  P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
a3d2128cac92 allow infix declarations for type constructors defined with domain package
huffman
parents: 30915
diff changeset
   169
  Scan.succeed [];
a3d2128cac92 allow infix declarations for type constructors defined with domain package
huffman
parents: 30915
diff changeset
   170
a3d2128cac92 allow infix declarations for type constructors defined with domain package
huffman
parents: 30915
diff changeset
   171
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
   172
  (type_args' -- P.binding -- P.opt_infix) --
30916
a3d2128cac92 allow infix declarations for type constructors defined with domain package
huffman
parents: 30915
diff changeset
   173
  (P.$$$ "=" |-- P.enum1 "|" cons_decl);
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   174
30916
a3d2128cac92 allow infix declarations for type constructors defined with domain package
huffman
parents: 30915
diff changeset
   175
val domains_decl =
a3d2128cac92 allow infix declarations for type constructors defined with domain package
huffman
parents: 30915
diff changeset
   176
  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
a3d2128cac92 allow infix declarations for type constructors defined with domain package
huffman
parents: 30915
diff changeset
   177
  P.and_list1 domain_decl;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   178
31161
a27d4254ff4c fix domain package parsing of lhs sort constraints
huffman
parents: 31023
diff changeset
   179
fun mk_domain (opt_name : string option,
a27d4254ff4c fix domain package parsing of lhs sort constraints
huffman
parents: 31023
diff changeset
   180
  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
   181
    ((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
   182
  let
30919
dcf8a7a66bd1 make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents: 30916
diff changeset
   183
    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
   184
    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
   185
      (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
   186
        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
   187
          (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
   188
    val comp_dnam =
30916
a3d2128cac92 allow infix declarations for type constructors defined with domain package
huffman
parents: 30915
diff changeset
   189
      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
   190
  in add_domain_cmd comp_dnam specs end;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   191
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24712
diff changeset
   192
val _ =
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   193
  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
   194
    (domains_decl >> (Toplevel.theory o mk_domain));
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   195
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24712
diff changeset
   196
end;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   197
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   198
end;