# HG changeset patch # User huffman # Date 1240354628 25200 # Node ID dcf8a7a66bd1d8b358bd8c67aa1f57657bc9d326 # Parent 21ce52733a4d9c9d5264c4b40ca58ef5b4d3d9f9 make domain package ML interface more consistent with datatype package; use binding instead of bstring diff -r 21ce52733a4d -r dcf8a7a66bd1 src/HOLCF/Tools/cont_consts.ML --- 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; diff -r 21ce52733a4d -r dcf8a7a66bd1 src/HOLCF/Tools/domain/domain_axioms.ML --- 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"; diff -r 21ce52733a4d -r dcf8a7a66bd1 src/HOLCF/Tools/domain/domain_extender.ML --- 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 diff -r 21ce52733a4d -r dcf8a7a66bd1 src/HOLCF/Tools/domain/domain_syntax.ML --- 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])