# HG changeset patch # User huffman # Date 1243546581 25200 # Node ID 67dff9c5b2bdd2b671aff15c548dbefe2b0dc365 # Parent 6c593b431f04318dcc82832167b6eb4a9d925381 remove hard tabs, fix indentation diff -r 6c593b431f04 -r 67dff9c5b2bd src/HOLCF/Tools/domain/domain_axioms.ML --- a/src/HOLCF/Tools/domain/domain_axioms.ML Thu May 28 13:52:13 2009 -0700 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Thu May 28 14:36:21 2009 -0700 @@ -6,14 +6,14 @@ signature DOMAIN_AXIOMS = sig - val copy_of_dtyp : (int -> term) -> DatatypeAux.dtyp -> term + val copy_of_dtyp : (int -> term) -> DatatypeAux.dtyp -> term - val calc_axioms : - string -> Domain_Library.eq list -> int -> Domain_Library.eq -> - string * (string * term) list * (string * term) list + val calc_axioms : + string -> Domain_Library.eq list -> int -> Domain_Library.eq -> + string * (string * term) list * (string * term) list - val add_axioms : - bstring -> Domain_Library.eq list -> theory -> theory + val add_axioms : + bstring -> Domain_Library.eq list -> theory -> theory end; @@ -39,101 +39,107 @@ | copy r (DatatypeAux.DtTFree a) = ID | copy r (DatatypeAux.DtType (c, ds)) = case Symtab.lookup copy_tab c of - SOME f => list_ccomb (%%:f, map (copy_of_dtyp r) ds) - | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID); + SOME f => list_ccomb (%%:f, map (copy_of_dtyp r) ds) + | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID); fun calc_axioms - (comp_dname : string) - (eqs : eq list) - (n : int) - (eqn as ((dname,_),cons) : eq) + (comp_dname : string) + (eqs : eq list) + (n : int) + (eqn as ((dname,_),cons) : eq) : string * (string * term) list * (string * term) list = let - (* ----- axioms and definitions concerning the isomorphism ------------------ *) + (* ----- axioms and definitions concerning the isomorphism ------------------ *) - val dc_abs = %%:(dname^"_abs"); - val dc_rep = %%:(dname^"_rep"); - val x_name'= "x"; - val x_name = idx_name eqs x_name' (n+1); - val dnam = Long_Name.base_name dname; + val dc_abs = %%:(dname^"_abs"); + val dc_rep = %%:(dname^"_rep"); + val x_name'= "x"; + val x_name = idx_name eqs x_name' (n+1); + val dnam = Long_Name.base_name dname; - val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); - val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); + val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); + val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); - val when_def = ("when_def",%%:(dname^"_when") == - List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) => - Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons)); - - val copy_def = + val when_def = ("when_def",%%:(dname^"_when") == + List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) => + Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons)); + + val copy_def = let fun r i = cproj (Bound 0) eqs i; in ("copy_def", %%:(dname^"_copy") == /\ "f" (dc_abs oo (copy_of_dtyp r (dtyp_of_eq eqn)) oo dc_rep)) end; - (* -- definitions concerning the constructors, discriminators and selectors - *) + (* -- definitions concerning the constructors, discriminators and selectors - *) - fun con_def m n (_,args) = let - fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x)); - fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs); - fun inj y 1 _ = y - | inj y _ 0 = mk_sinl y - | inj y i j = mk_sinr (inj y (i-1) (j-1)); - in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end; - - val con_defs = mapn (fn n => fn (con,args) => - (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons; - - val dis_defs = let - fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == - list_ccomb(%%:(dname^"_when"),map - (fn (con',args) => (List.foldr /\# - (if con'=con then TT else FF) args)) cons)) - in map ddef cons end; + fun con_def m n (_,args) = let + fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x)); + fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs); + fun inj y 1 _ = y + | inj y _ 0 = mk_sinl y + | inj y i j = mk_sinr (inj y (i-1) (j-1)); + in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end; + + val con_defs = mapn (fn n => fn (con,args) => + (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons; + + val dis_defs = let + fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == + list_ccomb(%%:(dname^"_when"),map + (fn (con',args) => (List.foldr /\# + (if con'=con then TT else FF) args)) cons)) + in map ddef cons end; - val mat_defs = - let - fun mdef (con,_) = - let - val k = Bound 0 - val x = Bound 1 - fun one_con (con', args') = - if con'=con then k else List.foldr /\# mk_fail args' - val w = list_ccomb(%%:(dname^"_when"), map one_con cons) - val rhs = /\ "x" (/\ "k" (w ` x)) - in (mat_name con ^"_def", %%:(mat_name con) == rhs) end - in map mdef cons end; + val mat_defs = + let + fun mdef (con,_) = + let + val k = Bound 0 + val x = Bound 1 + fun one_con (con', args') = + if con'=con then k else List.foldr /\# mk_fail args' + val w = list_ccomb(%%:(dname^"_when"), map one_con cons) + val rhs = /\ "x" (/\ "k" (w ` x)) + in (mat_name con ^"_def", %%:(mat_name con) == rhs) end + in map mdef cons end; - val pat_defs = - let - fun pdef (con,args) = - let - val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; - val xs = map (bound_arg args) args; - val r = Bound (length args); - val rhs = case args of [] => mk_return HOLogic.unit - | _ => mk_ctuple_pat ps ` mk_ctuple xs; - fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args'; - in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == - list_ccomb(%%:(dname^"_when"), map one_con cons)) - end - in map pdef cons end; + val pat_defs = + let + fun pdef (con,args) = + let + val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; + val xs = map (bound_arg args) args; + val r = Bound (length args); + val rhs = case args of [] => mk_return HOLogic.unit + | _ => mk_ctuple_pat ps ` mk_ctuple xs; + fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args'; + in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == + list_ccomb(%%:(dname^"_when"), map one_con cons)) + end + in map pdef cons end; - val sel_defs = let - fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == - list_ccomb(%%:(dname^"_when"),map - (fn (con',args) => if con'<>con then UU else - List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); - in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end; + val sel_defs = let + fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == + list_ccomb(%%:(dname^"_when"),map + (fn (con',args) => if con'<>con then UU else + List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); + in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end; - (* ----- axiom and definitions concerning induction ------------------------- *) + (* ----- axiom and definitions concerning induction ------------------------- *) - val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n - `%x_name === %:x_name)); - val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj - (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n)); - val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name, - mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); + val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n + `%x_name === %:x_name)); + val take_def = + ("take_def", + %%:(dname^"_take") == + mk_lam("n",cproj + (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n)); + val finite_def = + ("finite_def", + %%:(dname^"_finite") == + mk_lam(x_name, + mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); in (dnam, [abs_iso_ax, rep_iso_ax, reach_ax], @@ -161,64 +167,64 @@ fun add_matchers (((dname,_),cons) : eq) thy = let - val con_names = map fst cons; - val mat_names = map mat_name con_names; - fun qualify n = Sign.full_name thy (Binding.name n); - val ms = map qualify con_names ~~ map qualify mat_names; + val con_names = map fst cons; + val mat_names = map mat_name con_names; + fun qualify n = Sign.full_name thy (Binding.name n); + val ms = map qualify con_names ~~ map qualify mat_names; in FixrecPackage.add_matchers ms thy end; 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"; - fun copy_app dname = %%:(dname^"_copy")`Bound 0; - val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == - /\ "f"(mk_ctuple (map copy_app dnames))); + val comp_dname = Sign.full_bname thy' comp_dnam; + val dnames = map (fst o fst) eqs; + val x_name = idx_name dnames "x"; + fun copy_app dname = %%:(dname^"_copy")`Bound 0; + val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == + /\ "f"(mk_ctuple (map copy_app dnames))); - fun one_con (con,args) = let - val nonrec_args = filter_out is_rec args; - val rec_args = List.filter is_rec args; - val recs_cnt = length rec_args; - val allargs = nonrec_args @ rec_args - @ map (upd_vname (fn s=> s^"'")) rec_args; - val allvns = map vname allargs; - fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; - val vns1 = map (vname_arg "" ) args; - val vns2 = map (vname_arg "'") args; - val allargs_cnt = length nonrec_args + 2*recs_cnt; - val rec_idxs = (recs_cnt-1) downto 0; - val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) - (allargs~~((allargs_cnt-1) downto 0))); - fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ - Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); - val capps = - List.foldr mk_conj - (mk_conj( - Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), - Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) - (mapn rel_app 1 rec_args); - in List.foldr mk_ex - (Library.foldr mk_conj - (map (defined o Bound) nonlazy_idxs,capps)) allvns - end; - fun one_comp n (_,cons) = - mk_all(x_name(n+1), - mk_all(x_name(n+1)^"'", - mk_imp(proj (Bound 2) eqs n $ Bound 1 $ Bound 0, - foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) - ::map one_con cons)))); - val bisim_def = - ("bisim_def", - %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs))); - - fun add_one (thy,(dnam,axs,dfs)) = - thy |> Sign.add_path dnam - |> add_defs_infer dfs - |> add_axioms_infer axs - |> Sign.parent_path; + fun one_con (con,args) = let + val nonrec_args = filter_out is_rec args; + val rec_args = List.filter is_rec args; + val recs_cnt = length rec_args; + val allargs = nonrec_args @ rec_args + @ map (upd_vname (fn s=> s^"'")) rec_args; + val allvns = map vname allargs; + fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; + val vns1 = map (vname_arg "" ) args; + val vns2 = map (vname_arg "'") args; + val allargs_cnt = length nonrec_args + 2*recs_cnt; + val rec_idxs = (recs_cnt-1) downto 0; + val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) + (allargs~~((allargs_cnt-1) downto 0))); + fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ + Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); + val capps = + List.foldr mk_conj + (mk_conj( + Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), + Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) + (mapn rel_app 1 rec_args); + in List.foldr mk_ex + (Library.foldr mk_conj + (map (defined o Bound) nonlazy_idxs,capps)) allvns + end; + fun one_comp n (_,cons) = + mk_all(x_name(n+1), + mk_all(x_name(n+1)^"'", + mk_imp(proj (Bound 2) eqs n $ Bound 1 $ Bound 0, + foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) + ::map one_con cons)))); + val bisim_def = + ("bisim_def", + %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs))); + + fun add_one (thy,(dnam,axs,dfs)) = + thy |> Sign.add_path dnam + |> add_defs_infer dfs + |> add_axioms_infer axs + |> Sign.parent_path; - val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); + val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); in thy |> Sign.add_path comp_dnam |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) diff -r 6c593b431f04 -r 67dff9c5b2bd src/HOLCF/Tools/domain/domain_extender.ML --- a/src/HOLCF/Tools/domain/domain_extender.ML Thu May 28 13:52:13 2009 -0700 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Thu May 28 14:36:21 2009 -0700 @@ -7,13 +7,13 @@ signature DOMAIN_EXTENDER = sig val add_domain_cmd: string -> - ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * string) list * mixfix) list) list - -> theory -> theory + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * string) list * mixfix) list) list + -> theory -> theory val add_domain: string -> - ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * typ) list * mixfix) list) list - -> theory -> theory + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * typ) list * mixfix) list) list + -> theory -> theory end; structure Domain_Extender :> DOMAIN_EXTENDER = @@ -23,121 +23,128 @@ (* ----- general testing and preprocessing of constructor list -------------- *) 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 (Binding.name_of o first) (List.concat cons'')) of - [] => false | dups => error ("Duplicate constructors: " - ^ commas_quote dups)); - 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: " - ^commas_quote dups)) (map snd dtnvs); - (* test for free type variables, illegal sort constraints on rhs, - non-pcpo-types and invalid use of recursive type; - replace sorts in type variables on rhs *) - fun analyse_equation ((dname,typevars),cons') = - let - val tvars = map dest_TFree typevars; - val distinct_typevars = map TFree tvars; - fun rm_sorts (TFree(s,_)) = TFree(s,[]) - | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) - | rm_sorts (TVar(s,_)) = TVar(s,[]) - and remove_sorts l = map rm_sorts l; - val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"] - fun analyse indirect (TFree(v,s)) = (case AList.lookup (op =) tvars v of - NONE => error ("Free type variable " ^ quote v ^ " on rhs.") - | SOME sort => if eq_set_string (s,defaultS) orelse - eq_set_string (s,sort ) - then TFree(v,sort) - else error ("Inconsistent sort constraint" ^ - " for type variable " ^ quote v)) - | analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of - NONE => if s mem indirect_ok - then Type(s,map (analyse false) typl) - else Type(s,map (analyse true) typl) - | SOME typevars => if indirect - then error ("Indirect recursion of type " ^ - quote (string_of_typ sg t)) - else if dname <> s orelse (** BUG OR FEATURE?: - mutual recursion may use different arguments **) - remove_sorts typevars = remove_sorts typl - then Type(s,map (analyse true) typl) - else error ("Direct recursion of type " ^ - quote (string_of_typ sg t) ^ - " with different arguments")) - | analyse indirect (TVar _) = Imposs "extender:analyse"; - fun check_pcpo lazy T = - let val ok = if lazy then cpo_type else pcpo_type - in if ok sg T then T else error - ("Constructor argument type is not of sort pcpo: " ^ - string_of_typ sg T) - end; - fun analyse_arg (lazy, sel, T) = - (lazy, sel, check_pcpo lazy (analyse false T)); - fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx); - in ((dname,distinct_typevars), map analyse_con cons') end; - in ListPair.map analyse_equation (dtnvs,cons'') - end; (* let *) + (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 (Binding.name_of o first) (List.concat cons'')) of + [] => false | dups => error ("Duplicate constructors: " + ^ commas_quote dups)); + 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: " + ^commas_quote dups)) (map snd dtnvs); + (* test for free type variables, illegal sort constraints on rhs, + non-pcpo-types and invalid use of recursive type; + replace sorts in type variables on rhs *) + fun analyse_equation ((dname,typevars),cons') = + let + val tvars = map dest_TFree typevars; + val distinct_typevars = map TFree tvars; + fun rm_sorts (TFree(s,_)) = TFree(s,[]) + | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) + | rm_sorts (TVar(s,_)) = TVar(s,[]) + and remove_sorts l = map rm_sorts l; + val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"] + fun analyse indirect (TFree(v,s)) = + (case AList.lookup (op =) tvars v of + NONE => error ("Free type variable " ^ quote v ^ " on rhs.") + | SOME sort => if eq_set_string (s,defaultS) orelse + eq_set_string (s,sort ) + then TFree(v,sort) + else error ("Inconsistent sort constraint" ^ + " for type variable " ^ quote v)) + | analyse indirect (t as Type(s,typl)) = + (case AList.lookup (op =) dtnvs s of + NONE => if s mem indirect_ok + then Type(s,map (analyse false) typl) + else Type(s,map (analyse true) typl) + | SOME typevars => if indirect + then error ("Indirect recursion of type " ^ + quote (string_of_typ sg t)) + else if dname <> s orelse + (** BUG OR FEATURE?: + mutual recursion may use different arguments **) + remove_sorts typevars = remove_sorts typl + then Type(s,map (analyse true) typl) + else error ("Direct recursion of type " ^ + quote (string_of_typ sg t) ^ + " with different arguments")) + | analyse indirect (TVar _) = Imposs "extender:analyse"; + fun check_pcpo lazy T = + let val ok = if lazy then cpo_type else pcpo_type + in if ok sg T then T else error + ("Constructor argument type is not of sort pcpo: " ^ + string_of_typ sg T) + end; + fun analyse_arg (lazy, sel, T) = + (lazy, sel, check_pcpo lazy (analyse false T)); + fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx); + 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 : theory -> 'a -> typ) - (comp_dnam : string) - (eqs''' : ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * 'a) list * mixfix) list) list) - (thy''' : theory) = - let - fun readS (SOME s) = Syntax.read_sort_global thy''' s - | readS NONE = Sign.defaultS thy'''; - fun readTFree (a, s) = TFree (a, readS s); + (prep_typ : theory -> 'a -> typ) + (comp_dnam : string) + (eqs''' : ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * 'a) list * mixfix) list) list) + (thy''' : theory) = + let + fun readS (SOME s) = Syntax.read_sort_global thy''' s + | readS NONE = Sign.defaultS thy'''; + fun readTFree (a, s) = TFree (a, readS s); - val dtnvs = map (fn (vs,dname:binding,mx,_) => - (dname, map readTFree 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_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); - fun typid (Type (id,_)) = + val dtnvs = map (fn (vs,dname:binding,mx,_) => + (dname, map readTFree 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_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); + fun typid (Type (id,_)) = let val c = hd (Symbol.explode (Long_Name.base_name id)) 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,args,mx) = - ((Syntax.const_name mx (Binding.name_of con)), - ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy, - DatatypeAux.dtyp_of_typ new_dts tp), - 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 ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn eq => - Domain_Theorems.theorems (eq, eqs)) eqs - ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs); - in - theorems_thy - |> Sign.add_path (Long_Name.base_name comp_dnam) - |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])])) - |> Sign.parent_path - end; + | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id))) + | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); + fun one_con (con,args,mx) = + ((Syntax.const_name mx (Binding.name_of con)), + ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy, + DatatypeAux.dtyp_of_typ new_dts tp), + 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 ((rewss, take_rews), theorems_thy) = + thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs + ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs); + in + theorems_thy + |> Sign.add_path (Long_Name.base_name comp_dnam) + |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])])) + |> Sign.parent_path + end; val add_domain = gen_add_domain Sign.certify_typ; val add_domain_cmd = gen_add_domain Syntax.read_typ_global; @@ -150,47 +157,47 @@ val _ = OuterKeyword.keyword "lazy"; val dest_decl : (bool * binding option * string) parser = - P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false -- - (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)); + P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false -- + (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.binding -- Scan.repeat dest_decl -- P.opt_mixfix; + P.binding -- Scan.repeat dest_decl -- P.opt_mixfix; val type_var' : (string * string option) parser = - (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort)); + (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort)); val type_args' : (string * string option) list parser = - type_var' >> single || - P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") || - Scan.succeed []; + type_var' >> single || + P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") || + Scan.succeed []; val domain_decl = - (type_args' -- P.binding -- P.opt_infix) -- - (P.$$$ "=" |-- P.enum1 "|" cons_decl); + (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; + Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- + P.and_list1 domain_decl; fun mk_domain (opt_name : string option, - doms : ((((string * string option) list * binding) * mixfix) * - ((binding * (bool * binding option * string) list) * mixfix) list) list ) = - let - val names = map (fn (((_, t), _), _) => Binding.name_of t) doms; - val specs : ((string * string option) 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_cmd comp_dnam specs end; + doms : ((((string * string option) list * binding) * mixfix) * + ((binding * (bool * binding option * string) list) * mixfix) list) list ) = + let + val names = map (fn (((_, t), _), _) => Binding.name_of t) doms; + val specs : ((string * string option) 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_cmd comp_dnam specs end; val _ = - OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl - (domains_decl >> (Toplevel.theory o mk_domain)); + OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl + (domains_decl >> (Toplevel.theory o mk_domain)); end; diff -r 6c593b431f04 -r 67dff9c5b2bd src/HOLCF/Tools/domain/domain_library.ML --- a/src/HOLCF/Tools/domain/domain_library.ML Thu May 28 13:52:13 2009 -0700 +++ b/src/HOLCF/Tools/domain/domain_library.ML Thu May 28 14:36:21 2009 -0700 @@ -8,27 +8,32 @@ (* ----- general support ---------------------------------------------------- *) fun mapn f n [] = [] -| mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs; + | mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs; -fun foldr'' f (l,f2) = let fun itr [] = raise Fail "foldr''" - | itr [a] = f2 a - | itr (a::l) = f(a, itr l) -in itr l end; -fun map_cumulr f start xs = List.foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) => - (y::ys,res2)) ([],start) xs; +fun foldr'' f (l,f2) = + let fun itr [] = raise Fail "foldr''" + | itr [a] = f2 a + | itr (a::l) = f(a, itr l) + in itr l end; +fun map_cumulr f start xs = + List.foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) => + (y::ys,res2)) ([],start) xs; fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x; fun upd_first f (x,y,z) = (f x, y, z); fun upd_second f (x,y,z) = ( x, f y, z); fun upd_third f (x,y,z) = ( x, y, f z); -fun atomize ctxt thm = let val r_inst = read_instantiate ctxt; - fun at thm = case concl_of thm of - _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) - | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec)) - | _ => [thm]; -in map zero_var_indexes (at thm) end; +fun atomize ctxt thm = + let + val r_inst = read_instantiate ctxt; + fun at thm = + case concl_of thm of + _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) + | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec)) + | _ => [thm]; + in map zero_var_indexes (at thm) end; (* infix syntax *) @@ -91,9 +96,9 @@ val mk_return : term -> term; val cproj : term -> 'a list -> int -> term; val list_ccomb : term * term list -> term; -(* - val con_app : string -> ('a * 'b * string) list -> term; -*) + (* + val con_app : string -> ('a * 'b * string) list -> term; + *) val con_app2 : string -> ('a -> term) -> 'a list -> term; val proj : term -> 'a list -> int -> term; val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a; @@ -126,8 +131,8 @@ val ==> : term * term -> term; val mk_All : string * term -> term; - (* Domain specifications *) - eqtype arg; + (* Domain specifications *) + eqtype arg; type cons = string * arg list; type eq = (string * typ list) * cons list; val mk_arg : (bool * DatatypeAux.dtyp) * string option * string -> arg; @@ -169,15 +174,17 @@ (* ----- name handling ----- *) -val strip_esc = let fun strip ("'" :: c :: cs) = c :: strip cs - | strip ["'"] = [] - | strip (c :: cs) = c :: strip cs - | strip [] = []; -in implode o strip o Symbol.explode end; +val strip_esc = + let fun strip ("'" :: c :: cs) = c :: strip cs + | strip ["'"] = [] + | strip (c :: cs) = c :: strip cs + | strip [] = []; + in implode o strip o Symbol.explode end; -fun extern_name con = case Symbol.explode con of - ("o"::"p"::" "::rest) => implode rest - | _ => con; +fun extern_name con = + case Symbol.explode con of + ("o"::"p"::" "::rest) => implode rest + | _ => con; fun dis_name con = "is_"^ (extern_name con); fun dis_name_ con = "is_"^ (strip_esc con); fun mat_name con = "match_"^ (extern_name con); @@ -186,19 +193,20 @@ fun pat_name_ con = (strip_esc con) ^ "_pat"; (* make distinct names out of the type list, - forbidding "o","n..","x..","f..","P.." as names *) + forbidding "o","n..","x..","f..","P.." as names *) (* a number string is added if necessary *) -fun mk_var_names ids : string list = let - fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s; - fun index_vnames(vn::vns,occupied) = +fun mk_var_names ids : string list = + let + fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s; + fun index_vnames(vn::vns,occupied) = (case AList.lookup (op =) occupied vn of NONE => if vn mem vns then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied) else vn :: index_vnames(vns, occupied) | SOME(i) => (vn^(string_of_int (i+1))) - :: index_vnames(vns,(vn,i+1)::occupied)) - | index_vnames([],occupied) = []; -in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end; + :: index_vnames(vns,(vn,i+1)::occupied)) + | index_vnames([],occupied) = []; + in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end; fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo}); fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo}); @@ -207,23 +215,23 @@ (* ----- constructor list handling ----- *) type arg = - (bool * DatatypeAux.dtyp) * (* (lazy, recursive element) *) - string option * (* selector name *) - string; (* argument name *) + (bool * DatatypeAux.dtyp) * (* (lazy, recursive element) *) + string option * (* selector name *) + string; (* argument name *) type cons = - string * (* operator name of constr *) - arg list; (* argument list *) + string * (* operator name of constr *) + arg list; (* argument list *) type eq = - (string * (* name of abstracted type *) - typ list) * (* arguments of abstracted type *) - cons list; (* represented type, as a constructor list *) + (string * (* name of abstracted type *) + typ list) * (* arguments of abstracted type *) + cons list; (* represented type, as a constructor list *) val mk_arg = I; fun rec_of ((_,dtyp),_,_) = - case dtyp of DatatypeAux.DtRec i => i | _ => ~1; + case dtyp of DatatypeAux.DtRec i => i | _ => ~1; (* FIXME: what about indirect recursion? *) fun is_lazy arg = fst (first arg); @@ -333,8 +341,8 @@ fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y; fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg); fun prj _ _ x ( _::[]) _ = x -| prj f1 _ x (_::y::ys) 0 = f1 x y -| prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1); + | prj f1 _ x (_::y::ys) 0 = f1 x y + | prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1); fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x; fun cproj x = prj (fn S => K(mk_cfst S)) (fn S => K(mk_csnd S)) x; fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); @@ -348,11 +356,11 @@ fun cpair (t,u) = %%: @{const_name cpair}`t`u; fun spair (t,u) = %%: @{const_name spair}`t`u; fun mk_ctuple [] = HOLogic.unit (* used in match_defs *) -| mk_ctuple ts = foldr1 cpair ts; + | mk_ctuple ts = foldr1 cpair ts; fun mk_stuple [] = ONE -| mk_stuple ts = foldr1 spair ts; + | mk_stuple ts = foldr1 spair ts; fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *) -| mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; + | mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; fun mk_maybeT T = Type ("Fixrec.maybe",[T]); fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2; val mk_ctuple_pat = foldr1 cpair_pat; @@ -360,29 +368,32 @@ fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1); fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = - (case cont_eta_contract body of - body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => - if not (0 mem loose_bnos f) then incr_boundvars ~1 f - else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body') - | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')) -| cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t -| cont_eta_contract t = t; + (case cont_eta_contract body of + body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => + if not (0 mem loose_bnos f) then incr_boundvars ~1 f + else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body') + | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')) + | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t + | cont_eta_contract t = t; fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n); fun when_funs cons = if length cons = 1 then ["f"] else mapn (fn n => K("f"^(string_of_int n))) 1 cons; -fun when_body cons funarg = let - fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n)) - | one_fun n (_,args) = let - val l2 = length args; - fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t)) - else I) (Bound(l2-m)); - in cont_eta_contract (foldr'' - (fn (a,t) => mk_ssplit (/\# (a,t))) - (args, - fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args)))) - ) end; -in (if length cons = 1 andalso length(snd(hd cons)) <= 1 - then mk_strictify else I) - (foldr1 mk_sscase (mapn one_fun 1 cons)) end; +fun when_body cons funarg = + let + fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n)) + | one_fun n (_,args) = let + val l2 = length args; + fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t)) + else I) (Bound(l2-m)); + in cont_eta_contract + (foldr'' + (fn (a,t) => mk_ssplit (/\# (a,t))) + (args, + fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args)))) + ) end; + in (if length cons = 1 andalso length(snd(hd cons)) <= 1 + then mk_strictify else I) + (foldr1 mk_sscase (mapn one_fun 1 cons)) end; + end; (* struct *) diff -r 6c593b431f04 -r 67dff9c5b2bd src/HOLCF/Tools/domain/domain_syntax.ML --- a/src/HOLCF/Tools/domain/domain_syntax.ML Thu May 28 13:52:13 2009 -0700 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML Thu May 28 14:36:21 2009 -0700 @@ -6,17 +6,17 @@ signature DOMAIN_SYNTAX = sig - val calc_syntax: - typ -> - (string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list -> - (binding * typ * mixfix) list * ast Syntax.trrule list + val calc_syntax: + typ -> + (string * typ list) * + (binding * (bool * binding option * typ) list * mixfix) list -> + (binding * typ * mixfix) list * ast Syntax.trrule list - val add_syntax: - string -> - ((string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list) list -> - theory -> theory + val add_syntax: + string -> + ((string * typ list) * + (binding * (bool * binding option * typ) list * mixfix) list) list -> + theory -> theory end; @@ -27,127 +27,129 @@ infixr 5 -->; infixr 6 ->>; fun calc_syntax - (dtypeprod : typ) - ((dname : string, typevars : typ list), - (cons': (binding * (bool * binding option * typ) list * mixfix) list)) + (dtypeprod : typ) + ((dname : string, typevars : typ list), + (cons': (binding * (bool * binding option * typ) list * mixfix) list)) : (binding * typ * mixfix) list * ast Syntax.trrule list = let - (* ----- constants concerning the isomorphism ------------------------------- *) + (* ----- constants concerning the isomorphism ------------------------------- *) - local - fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t - 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); - in - val dtype = Type(dname,typevars); - val dtype2 = foldr1 mk_ssumT (map prod cons'); - val dnam = Long_Name.base_name dname; - 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; + local + fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t + 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); + in + val dtype = Type(dname,typevars); + val dtype2 = foldr1 mk_ssumT (map prod cons'); + val dnam = Long_Name.base_name dname; + 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 --- *) + (* ----- constants concerning constructors, discriminators, and selectors --- *) - local - val escape = let - fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs - else c::esc cs - | esc [] = [] - in implode o esc o Symbol.explode end; - 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,args,mx) = (mat_name_ con, - mk_matT(dtype, map third args, freetvar "t" 1), - 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 (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,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 (Binding.name_of con ^ "_pat"), [], Syntax.max_pri)); + local + val escape = let + fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs + else c::esc cs + | esc [] = [] + in implode o esc o Symbol.explode end; + 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,args,mx) = (mat_name_ con, + mk_matT(dtype, map third args, freetvar "t" 1), + 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 (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,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 (Binding.name_of con ^ "_pat"), [], Syntax.max_pri)); - in - val consts_con = map con cons'; - val consts_dis = map dis cons'; - val consts_mat = map mat cons'; - val consts_pat = map pat cons'; - val consts_sel = List.concat(map sel cons'); - end; + in + val consts_con = map con cons'; + val consts_dis = map dis cons'; + val consts_mat = map mat cons'; + val consts_pat = map pat cons'; + val consts_sel = List.concat(map sel cons'); + end; - (* ----- constants concerning induction ------------------------------------- *) + (* ----- constants concerning induction ------------------------------------- *) - val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn); - val const_finite = (dbind "_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 --------------------------------------------------- *) + (* ----- case translation --------------------------------------------------- *) - local open Syntax in - local - 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)); - fun argvars n args = mapn (argvar n) 1 args; - fun app s (l,r) = mk_appl (Constant s) [l,r]; - val cabs = app "_cabs"; - val capp = app "Rep_CFun"; - 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"); + local open Syntax in + local + 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)); + fun argvars n args = mapn (argvar n) 1 args; + fun app s (l,r) = mk_appl (Constant s) [l,r]; + val cabs = app "_cabs"; + val capp = app "Rep_CFun"; + 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"]; - fun app_pat x = mk_appl (Constant "_pat") [x]; - fun args_list [] = Constant "_noargs" - | args_list xs = foldr1 (app "_args") xs; - in - val case_trans = - ParsePrintRule - (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')), - capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x")); + fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"]; + fun app_pat x = mk_appl (Constant "_pat") [x]; + fun args_list [] = Constant "_noargs" + | args_list xs = foldr1 (app "_args") xs; + in + val case_trans = + ParsePrintRule + (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')), + capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x")); - fun one_abscon_trans n (con,mx,args) = - ParsePrintRule - (cabs (con1 n (con,mx,args), expvar n), - Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons')); - val abscon_trans = mapn one_abscon_trans 1 cons'; - - fun one_case_trans (con,args,mx) = - let - val cname = c_ast con mx; - 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; - val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; - in - [ParseRule (app_pat (Library.foldl capp (cname, xs)), - mk_appl pname (map app_pat xs)), - ParseRule (app_var (Library.foldl capp (cname, xs)), - app_var (args_list xs)), - PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)), - app "_match" (mk_appl pname ps, args_list vs))] - end; - val Case_trans = List.concat (map one_case_trans cons'); - end; - end; + fun one_abscon_trans n (con,mx,args) = + ParsePrintRule + (cabs (con1 n (con,mx,args), expvar n), + Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons')); + val abscon_trans = mapn one_abscon_trans 1 cons'; + + fun one_case_trans (con,args,mx) = + let + val cname = c_ast con mx; + 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; + val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; + in + [ParseRule (app_pat (Library.foldl capp (cname, xs)), + mk_appl pname (map app_pat xs)), + ParseRule (app_var (Library.foldl capp (cname, xs)), + app_var (args_list xs)), + PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)), + app "_match" (mk_appl pname ps, args_list vs))] + end; + val Case_trans = List.concat (map one_case_trans cons'); + end; + end; in ([const_rep, const_abs, const_when, const_copy] @ consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @ @@ -158,22 +160,22 @@ (* ----- putting all the syntax stuff together ------------------------------ *) fun add_syntax - (comp_dnam : string) - (eqs' : ((string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list) list) - (thy'' : theory) = + (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 = (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'; + 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 = (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]) - |> Sign.add_trrules_i (List.concat(map snd ctt)) + (if length eqs'>1 then [const_copy] else[])@ + [const_bisim]) + |> Sign.add_trrules_i (List.concat(map snd ctt)) end; (* let *) end; (* struct *) diff -r 6c593b431f04 -r 67dff9c5b2bd src/HOLCF/Tools/domain/domain_theorems.ML --- a/src/HOLCF/Tools/domain/domain_theorems.ML Thu May 28 13:52:13 2009 -0700 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Thu May 28 14:36:21 2009 -0700 @@ -539,9 +539,10 @@ [eq1, eq2] end; fun distincts [] = [] - | distincts ((c,leqs)::cs) = flat - (ListPair.map (distinct c) ((map #1 cs),leqs)) @ - distincts cs; + | distincts ((c,leqs)::cs) = + flat + (ListPair.map (distinct c) ((map #1 cs),leqs)) @ + distincts cs; in map standard (distincts (cons ~~ distincts_le)) end; local