make domain package ML interface more consistent with datatype package; use binding instead of bstring
--- a/src/HOLCF/Tools/cont_consts.ML Tue Apr 21 11:11:04 2009 -0700
+++ b/src/HOLCF/Tools/cont_consts.ML Tue Apr 21 15:57:08 2009 -0700
@@ -8,8 +8,8 @@
signature CONT_CONSTS =
sig
- val add_consts: (bstring * string * mixfix) list -> theory -> theory
- val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
+ val add_consts: (binding * string * mixfix) list -> theory -> theory
+ val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
end;
structure ContConsts: CONT_CONSTS =
@@ -49,20 +49,24 @@
declaration with the original name, type ...=>..., and the original mixfix
is generated and connected to the other declaration via some translation.
*)
-fun fix_mixfix (syn , T, mx as Infix p ) =
- (Syntax.const_name mx syn, T, InfixName (syn, p))
- | fix_mixfix (syn , T, mx as Infixl p ) =
- (Syntax.const_name mx syn, T, InfixlName (syn, p))
- | fix_mixfix (syn , T, mx as Infixr p ) =
- (Syntax.const_name mx syn, T, InfixrName (syn, p))
+fun const_binding mx = Binding.name o Syntax.const_name mx o Binding.name_of;
+
+fun fix_mixfix (syn , T, mx as Infix p ) =
+ (const_binding mx syn, T, InfixName (Binding.name_of syn, p))
+ | fix_mixfix (syn , T, mx as Infixl p ) =
+ (const_binding mx syn, T, InfixlName (Binding.name_of syn, p))
+ | fix_mixfix (syn , T, mx as Infixr p ) =
+ (const_binding mx syn, T, InfixrName (Binding.name_of syn, p))
| fix_mixfix decl = decl;
+
fun transform decl = let
val (c, T, mx) = fix_mixfix decl;
- val c2 = "_cont_" ^ c;
+ val c1 = Binding.name_of c;
+ val c2 = "_cont_" ^ c1;
val n = Syntax.mixfix_args mx
- in ((c , T,NoSyn),
- (c2,change_arrow n T,mx ),
- trans_rules c2 c n mx) end;
+ in ((c, T, NoSyn),
+ (Binding.name c2, change_arrow n T, mx),
+ trans_rules c2 c1 n mx) end;
fun cfun_arity (Type(n,[_,T])) = if n = @{type_name "->"} then 1+cfun_arity T else 0
| cfun_arity _ = 0;
@@ -71,7 +75,7 @@
| is_contconst (_,_,Binder _) = false
| is_contconst (c,T,mx ) = cfun_arity T >= Syntax.mixfix_args mx
handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
- quote (Syntax.const_name mx c));
+ quote (Syntax.const_name mx (Binding.name_of c)));
(* add_consts(_i) *)
@@ -83,7 +87,7 @@
val transformed_decls = map transform contconst_decls;
in
thy
- |> (Sign.add_consts_i o map (upd_first Binding.name))
+ |> Sign.add_consts_i
(normal_decls @ map first transformed_decls @ map second transformed_decls)
|> Sign.add_trrules_i (maps third transformed_decls)
end;
@@ -98,7 +102,7 @@
val _ =
OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
- (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
+ (Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts));
end;
--- a/src/HOLCF/Tools/domain/domain_axioms.ML Tue Apr 21 11:11:04 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML Tue Apr 21 15:57:08 2009 -0700
@@ -4,7 +4,14 @@
Syntax generator for domain command.
*)
-structure Domain_Axioms = struct
+signature DOMAIN_AXIOMS =
+sig
+ val add_axioms : bstring -> Domain_Library.eq list -> theory -> theory
+end;
+
+
+structure Domain_Axioms : DOMAIN_AXIOMS =
+struct
local
@@ -139,7 +146,7 @@
in (* local *)
-fun add_axioms (comp_dnam, eqs : eq list) thy' = let
+fun add_axioms comp_dnam (eqs : eq list) thy' = let
val comp_dname = Sign.full_bname thy' comp_dnam;
val dnames = map (fst o fst) eqs;
val x_name = idx_name dnames "x";
--- a/src/HOLCF/Tools/domain/domain_extender.ML Tue Apr 21 11:11:04 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Tue Apr 21 15:57:08 2009 -0700
@@ -6,11 +6,11 @@
signature DOMAIN_EXTENDER =
sig
- val add_domain: string * ((bstring * string list * mixfix) *
- (string * mixfix * (bool * string option * string) list) list) list
+ val add_domain_cmd: string -> (string list * binding * mixfix *
+ (binding * (bool * binding option * string) list * mixfix) list) list
-> theory -> theory
- val add_domain_i: string * ((bstring * string list * mixfix) *
- (string * mixfix * (bool * string option * typ) list) list) list
+ val add_domain: string -> (string list * binding * mixfix *
+ (binding * (bool * binding option * typ) list * mixfix) list) list
-> theory -> theory
end;
@@ -20,17 +20,21 @@
open Domain_Library;
(* ----- general testing and preprocessing of constructor list -------------- *)
-fun check_and_sort_domain (dtnvs: (string * typ list) list,
- cons'' : ((string * mixfix * (bool * string option * typ) list) list) list) sg =
+fun check_and_sort_domain
+ (dtnvs : (string * typ list) list)
+ (cons'' : ((binding * (bool * binding option * typ) list * mixfix) list) list)
+ (sg : theory)
+ : ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list =
let
val defaultS = Sign.defaultS sg;
val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of
[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
- val test_dupl_cons = (case duplicates (op =) (map first (List.concat cons'')) of
+ val test_dupl_cons = (case duplicates (op =) (map (Binding.name_of o first) (List.concat cons'')) of
[] => false | dups => error ("Duplicate constructors: "
^ commas_quote dups));
- val test_dupl_sels = (case duplicates (op =) (List.mapPartial second
- (List.concat (map third (List.concat cons'')))) of
+ val test_dupl_sels = (case duplicates (op =) (map Binding.name_of (List.mapPartial second
+ (List.concat (map second (List.concat cons''))))) of
[] => false | dups => error("Duplicate selectors: "^commas_quote dups));
val test_dupl_tvars = exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
[] => false | dups => error("Duplicate type arguments: "
@@ -71,27 +75,31 @@
| analyse indirect (TVar _) = Imposs "extender:analyse";
fun check_pcpo T = if pcpo_type sg T then T
else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T);
- val analyse_con = upd_third (map (upd_third (check_pcpo o analyse false)));
+ val analyse_con = upd_second (map (upd_third (check_pcpo o analyse false)));
in ((dname,distinct_typevars), map analyse_con cons') end;
in ListPair.map analyse_equation (dtnvs,cons'')
end; (* let *)
(* ----- calls for building new thy and thms -------------------------------- *)
-fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
+fun gen_add_domain
+ (prep_typ : theory -> 'a -> typ)
+ (comp_dnam : string)
+ (eqs''' : (string list * binding * mixfix *
+ (binding * (bool * binding option * 'a) list * mixfix) list) list)
+ (thy''' : theory) =
let
- val dtnvs = map ((fn (dname,vs,mx) =>
- (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs, mx))
- o fst) eqs''';
- val cons''' = map snd eqs''';
- fun thy_type (dname,tvars,mx) = (Binding.name (Long_Name.base_name dname), length tvars, mx);
- fun thy_arity (dname,tvars,mx) = (dname, map (snd o dest_TFree) tvars, pcpoS);
+ val dtnvs = map (fn (vs,dname:binding,mx,_) =>
+ (dname, map (Syntax.read_typ_global thy''') vs, mx)) eqs''';
+ val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
+ fun thy_type (dname,tvars,mx) = (dname, length tvars, mx);
+ fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
|> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
- val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
- val dtnvs' = map (fn (dname,vs,mx) => (dname,vs)) dtnvs;
- val eqs' = check_and_sort_domain (dtnvs',cons'') thy'';
- val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
+ val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
+ val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
+ val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list = check_and_sort_domain dtnvs' cons'' thy'';
+ val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
val dts = map (Type o fst) eqs';
val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
@@ -100,16 +108,16 @@
in if Symbol.is_letter c then c else "t" end
| typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
| typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
- fun one_con (con,mx,args) =
- ((Syntax.const_name mx con),
+ fun one_con (con,args,mx) =
+ ((Syntax.const_name mx (Binding.name_of con)),
ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
find_index_eq tp dts,
DatatypeAux.dtyp_of_typ new_dts tp),
- sel,vn))
+ Option.map Binding.name_of sel,vn))
(args,(mk_var_names(map (typid o third) args)))
) : cons;
val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
- val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
+ val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs;
val ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn eq =>
Domain_Theorems.theorems (eq, eqs)) eqs
||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
@@ -120,8 +128,8 @@
|> Sign.parent_path
end;
-val add_domain_i = gen_add_domain Sign.certify_typ;
-val add_domain = gen_add_domain Syntax.read_typ_global;
+val add_domain = gen_add_domain Sign.certify_typ;
+val add_domain_cmd = gen_add_domain Syntax.read_typ_global;
(** outer syntax **)
@@ -130,15 +138,15 @@
val _ = OuterKeyword.keyword "lazy";
-val dest_decl : (bool * string option * string) parser =
+val dest_decl : (bool * binding option * string) parser =
P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
- (P.name >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
+ (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
|| P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
>> (fn t => (true,NONE,t))
|| P.typ >> (fn t => (false,NONE,t));
val cons_decl =
- P.name -- Scan.repeat dest_decl -- P.opt_mixfix;
+ P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
val type_var' =
(P.type_ident ^^ Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
@@ -149,22 +157,24 @@
Scan.succeed [];
val domain_decl =
- (type_args' -- P.name -- P.opt_infix) --
+ (type_args' -- P.binding -- P.opt_infix) --
(P.$$$ "=" |-- P.enum1 "|" cons_decl);
val domains_decl =
Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
P.and_list1 domain_decl;
-fun mk_domain (opt_name : string option, doms : (((string list * bstring) * mixfix) *
- ((string * (bool * string option * string) list) * mixfix) list) list ) =
+fun mk_domain (opt_name : string option, doms : (((string list * binding) * mixfix) *
+ ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
let
- val names = map (fn (((_, t), _), _) => t) doms;
- val specs = map (fn (((vs, t), mx), cons) =>
- ((t, vs, mx), map (fn ((c, ds), mx) => (c, mx, ds)) cons)) doms;
- val big_name =
+ val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
+ val specs : (string list * binding * mixfix *
+ (binding * (bool * binding option * string) list * mixfix) list) list =
+ map (fn (((vs, t), mx), cons) =>
+ (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
+ val comp_dnam =
case opt_name of NONE => space_implode "_" names | SOME s => s;
- in add_domain (big_name, specs) end;
+ in add_domain_cmd comp_dnam specs end;
val _ =
OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
--- a/src/HOLCF/Tools/domain/domain_syntax.ML Tue Apr 21 11:11:04 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML Tue Apr 21 15:57:08 2009 -0700
@@ -4,32 +4,42 @@
Syntax generator for domain command.
*)
-structure Domain_Syntax = struct
+signature DOMAIN_SYNTAX =
+sig
+ val add_syntax: string -> ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list
+ -> theory -> theory
+end;
+
+
+structure Domain_Syntax : DOMAIN_SYNTAX =
+struct
local
open Domain_Library;
infixr 5 -->; infixr 6 ->>;
fun calc_syntax dtypeprod ((dname, typevars),
- (cons': (string * mixfix * (bool * string option * typ) list) list)) =
+ (cons': (binding * (bool * binding option * typ) list * mixfix) list)) : ((binding * typ * mixfix) list * ast Syntax.trrule list) =
let
(* ----- constants concerning the isomorphism ------------------------------- *)
local
fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
- fun prod (_,_,args) = if args = [] then oneT
- else foldr1 mk_sprodT (map opt_lazy args);
+ fun prod (_,args,_) = case args of [] => oneT
+ | _ => foldr1 mk_sprodT (map opt_lazy args);
fun freetvar s = let val tvar = mk_TFree s in
if tvar mem typevars then freetvar ("t"^s) else tvar end;
- fun when_type (_ ,_,args) = List.foldr (op ->>) (freetvar "t") (map third args);
+ fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args);
in
val dtype = Type(dname,typevars);
val dtype2 = foldr1 mk_ssumT (map prod cons');
val dnam = Long_Name.base_name dname;
- val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn);
- val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn);
- val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
- val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
+ fun dbind s = Binding.name (dnam ^ s);
+ val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn);
+ val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn);
+ val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
+ val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
end;
(* ----- constants concerning constructors, discriminators, and selectors --- *)
@@ -40,25 +50,28 @@
else c::esc cs
| esc [] = []
in implode o esc o Symbol.explode end;
- fun con (name,s,args) = (name, List.foldr (op ->>) dtype (map third args),s);
- fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT,
- Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
+ fun dis_name_ con = Binding.name ("is_" ^ strip_esc (Binding.name_of con));
+ fun mat_name_ con = Binding.name ("match_" ^ strip_esc (Binding.name_of con));
+ fun pat_name_ con = Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
+ fun con (name,args,mx) = (name, List.foldr (op ->>) dtype (map third args), mx);
+ fun dis (con,args,mx) = (dis_name_ con, dtype->>trT,
+ Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri));
(* strictly speaking, these constants have one argument,
but the mixfix (without arguments) is introduced only
to generate parse rules for non-alphanumeric names*)
fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in
if tvar mem typevars then freetvar ("t"^s) n else tvar end;
fun mk_matT (a,bs,c) = a ->> foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
- fun mat (con,s,args) = (mat_name_ con,
+ fun mat (con,args,mx) = (mat_name_ con,
mk_matT(dtype, map third args, freetvar "t" 1),
- Mixfix(escape ("match_" ^ con), [], Syntax.max_pri));
+ Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
- fun sel (_ ,_,args) = List.mapPartial sel1 args;
+ fun sel (con,args,mx) = List.mapPartial sel1 args;
fun mk_patT (a,b) = a ->> mk_maybeT b;
fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
- fun pat (con ,s,args) = (pat_name_ con, (mapn pat_arg_typ 1 args) --->
+ fun pat (con,args,mx) = (pat_name_ con, (mapn pat_arg_typ 1 args) --->
mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
- Mixfix(escape (con ^ "_pat"), [], Syntax.max_pri));
+ Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
in
val consts_con = map con cons';
@@ -70,14 +83,14 @@
(* ----- constants concerning induction ------------------------------------- *)
- val const_take = (dnam^"_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
- val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT , NoSyn);
+ val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
+ val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn);
(* ----- case translation --------------------------------------------------- *)
local open Syntax in
local
- fun c_ast con mx = Constant (Syntax.const_name mx con);
+ fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con));
fun expvar n = Variable ("e"^(string_of_int n));
fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
(string_of_int m));
@@ -85,9 +98,9 @@
fun app s (l,r) = mk_appl (Constant s) [l,r];
val cabs = app "_cabs";
val capp = app "Rep_CFun";
- fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args);
- fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n);
- fun arg1 n (con,_,args) = List.foldr cabs (expvar n) (argvars n args);
+ fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args);
+ fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n);
+ fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args);
fun when1 n m = if n = m then arg1 n else K (Constant "UU");
fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
@@ -103,10 +116,10 @@
(cabs (con1 n (con,mx,args), expvar n),
Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'))) 1 cons';
- val Case_trans = List.concat (map (fn (con,mx,args) =>
+ val Case_trans = List.concat (map (fn (con,args,mx) =>
let
val cname = c_ast con mx;
- val pname = Constant (pat_name_ con);
+ val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat");
val ns = 1 upto length args;
val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
@@ -132,16 +145,19 @@
in (* local *)
-fun add_syntax (comp_dnam,eqs': ((string * typ list) *
- (string * mixfix * (bool * string option * typ) list) list) list) thy'' =
+fun add_syntax
+ (comp_dnam : string)
+ (eqs' : ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list)
+ (thy'' : theory) =
let
val dtypes = map (Type o fst) eqs';
val boolT = HOLogic.boolT;
val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes);
val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
- val const_copy = (comp_dnam^"_copy" ,funprod ->> funprod, NoSyn);
- val const_bisim = (comp_dnam^"_bisim" ,relprod --> boolT , NoSyn);
- val ctt = map (calc_syntax funprod) eqs';
+ val const_copy = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
+ val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
+ val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs';
in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @
(if length eqs'>1 then [const_copy] else[])@
[const_bisim])