# HG changeset patch # User huffman # Date 1266866261 28800 # Node ID aa7da51ae1ef56ec2b749e3a4ce5c4aca6d91472 # Parent 978a936faace2d3cc5081ce629df40faa53e1f08 add mixfix field to type Domain_Library.cons diff -r 978a936faace -r aa7da51ae1ef src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Feb 22 09:43:36 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Feb 22 11:17:41 2010 -0800 @@ -88,23 +88,23 @@ | 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) => + 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) == + fun ddef (con,_,_) = (dis_name con ^"_def",%%:(dis_name con) == list_ccomb(%%:(dname^"_when"),map - (fn (con',args) => (List.foldr /\# + (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,_) = + fun mdef (con, _, _) = let val k = Bound 0 val x = Bound 1 - fun one_con (con', args') = + 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)) @@ -113,14 +113,14 @@ val pat_defs = let - fun pdef (con,args) = + 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'; + 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 @@ -129,9 +129,9 @@ 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 + (fn (con', _, args) => if con'<>con then UU else List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); - in map_filter I (maps (fn (con,args) => mapn (sdef con) 1 args) cons) end; + in map_filter I (maps (fn (con, _, args) => mapn (sdef con) 1 args) cons) end; (* ----- axiom and definitions concerning induction ------------------------- *) @@ -175,7 +175,7 @@ fun add_matchers (((dname,_),cons) : eq) thy = let - val con_names = map fst cons; + val con_names = map first 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; @@ -190,7 +190,7 @@ val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == /\ "f"(mk_ctuple (map copy_app dnames))); - fun one_con (con,args) = + fun one_con (con, _, args) = let val nonrec_args = filter_out is_rec args; val rec_args = filter is_rec args; diff -r 978a936faace -r aa7da51ae1ef src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Mon Feb 22 09:43:36 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Mon Feb 22 11:17:41 2010 -0800 @@ -161,6 +161,7 @@ | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); fun one_con (con,args,mx) = (Binding.name_of con, (* FIXME preverse binding (!?) *) + mx, ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), Option.map Binding.name_of sel,vn)) @@ -236,6 +237,7 @@ | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); fun one_con (con,args,mx) = (Binding.name_of con, (* FIXME preverse binding (!?) *) + mx, ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), Option.map Binding.name_of sel,vn)) diff -r 978a936faace -r aa7da51ae1ef src/HOLCF/Tools/Domain/domain_library.ML --- a/src/HOLCF/Tools/Domain/domain_library.ML Mon Feb 22 09:43:36 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_library.ML Mon Feb 22 11:17:41 2010 -0800 @@ -132,7 +132,7 @@ (* Domain specifications *) eqtype arg; - type cons = string * arg list; + type cons = string * mixfix * arg list; type eq = (string * typ list) * cons list; val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg; val is_lazy : arg -> bool; @@ -220,6 +220,7 @@ type cons = string * (* operator name of constr *) + mixfix * (* mixfix syntax of constructor *) arg list; (* argument list *) type eq = @@ -258,7 +259,7 @@ fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds; fun dtyp_of_arg ((lazy, D), _, _) = if lazy then mk_uD D else D; -fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args); +fun dtyp_of_cons (_, _, args) = big_sprodD (map dtyp_of_arg args); fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons); @@ -377,8 +378,8 @@ 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 + 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)); @@ -388,7 +389,7 @@ (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 + in (if length cons = 1 andalso length(third(hd cons)) <= 1 then mk_strictify else I) (foldr1 mk_sscase (mapn one_fun 1 cons)) end; diff -r 978a936faace -r aa7da51ae1ef src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Feb 22 09:43:36 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Feb 22 11:17:41 2010 -0800 @@ -148,7 +148,7 @@ val ax_abs_iso = ga "abs_iso" dname; val ax_rep_iso = ga "rep_iso" dname; val ax_when_def = ga "when_def" dname; - fun get_def mk_name (con,_) = ga (mk_name con^"_def") dname; + fun get_def mk_name (con, _, _) = ga (mk_name con^"_def") dname; val axs_con_def = map (get_def extern_name) cons; val axs_dis_def = map (get_def dis_name) cons; val axs_mat_def = map (get_def mat_name) cons; @@ -157,7 +157,7 @@ let fun def_of_sel sel = ga (sel^"_def") dname; fun def_of_arg arg = Option.map def_of_sel (sel_of arg); - fun defs_of_con (_, args) = map_filter def_of_arg args; + fun defs_of_con (_, _, args) = map_filter def_of_arg args; in maps defs_of_con cons end; @@ -222,10 +222,10 @@ in (n2, mk_sprodT (t1, t2)) end; fun cons2typ n [] = (n,oneT) - | cons2typ n [con] = args2typ n (snd con) + | cons2typ n [con] = args2typ n (third con) | cons2typ n (con::cons) = let - val (n1, t1) = args2typ n (snd con); + val (n1, t1) = args2typ n (third con); val (n2, t2) = cons2typ n1 cons in (n2, mk_ssumT (t1, t2)) end; in @@ -234,7 +234,7 @@ local val iso_swap = iso_locale RS iso_iso_swap; - fun one_con (con, args) = + fun one_con (con, _, args) = let val vns = map vname args; val eqn = %:x_name === con_app2 con %: vns; @@ -278,7 +278,7 @@ val _ = trace " Proving when_apps..."; val when_apps = let - fun one_when n (con,args) = + fun one_when n (con, _, args) = let val axs = when_appl :: con_appls; val goal = bind_fun (lift_defined %: (nonlazy args, @@ -293,12 +293,12 @@ (* ----- theorems concerning the constructors, discriminators and selectors - *) local - fun dis_strict (con, _) = + fun dis_strict (con, _, _) = let val goal = mk_trp (strict (%%:(dis_name con))); in pg axs_dis_def goal (K [rtac when_strict 1]) end; - fun dis_app c (con, args) = + fun dis_app c (con, _, args) = let val lhs = %%:(dis_name c) ` con_app con args; val rhs = if con = c then TT else FF; @@ -307,9 +307,9 @@ in pg axs_dis_def goal (K tacs) end; val _ = trace " Proving dis_apps..."; - val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons; + val dis_apps = maps (fn (c,_,_) => map (dis_app c) cons) cons; - fun dis_defin (con, args) = + fun dis_defin (con, _, args) = let val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name); val tacs = @@ -328,7 +328,7 @@ end; local - fun mat_strict (con, _) = + fun mat_strict (con, _, _) = let val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU); val tacs = [asm_simp_tac (HOLCF_ss addsimps [when_strict]) 1]; @@ -337,7 +337,7 @@ val _ = trace " Proving mat_stricts..."; val mat_stricts = map mat_strict cons; - fun one_mat c (con, args) = + fun one_mat c (con, _, args) = let val lhs = %%:(mat_name c) ` con_app con args ` %:"rhs"; val rhs = @@ -350,7 +350,7 @@ val _ = trace " Proving mat_apps..."; val mat_apps = - maps (fn (c,_) => map (one_mat c) cons) cons; + maps (fn (c,_,_) => map (one_mat c) cons) cons; in val mat_rews = mat_stricts @ mat_apps; end; @@ -358,10 +358,10 @@ local fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; - fun pat_lhs (con,args) = mk_branch (list_comb (%%:(pat_name con), ps args)); + fun pat_lhs (con,_,args) = mk_branch (list_comb (%%:(pat_name con), ps args)); - fun pat_rhs (con,[]) = mk_return ((%:"rhs") ` HOLogic.unit) - | pat_rhs (con,args) = + fun pat_rhs (con,_,[]) = mk_return ((%:"rhs") ` HOLogic.unit) + | pat_rhs (con,_,args) = (mk_branch (mk_ctuple_pat (ps args))) `(%:"rhs")`(mk_ctuple (map %# args)); @@ -372,11 +372,11 @@ val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1]; in pg axs goal (K tacs) end; - fun pat_app c (con, args) = + fun pat_app c (con, _, args) = let val axs = @{thm branch_def} :: axs_pat_def; val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args); - val rhs = if con = fst c then pat_rhs c else mk_fail; + val rhs = if con = first c then pat_rhs c else mk_fail; val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; in pg axs goal (K tacs) end; @@ -390,7 +390,7 @@ end; local - fun con_strict (con, args) = + fun con_strict (con, _, args) = let val rules = abs_strict :: @{thms con_strict_rules}; fun one_strict vn = @@ -401,7 +401,7 @@ in pg con_appls goal (K tacs) end; in map one_strict (nonlazy args) end; - fun con_defin (con, args) = + fun con_defin (con, _, args) = let fun iff_disj (t, []) = HOLogic.mk_not t | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts; @@ -423,7 +423,7 @@ local val rules = [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE]; - fun con_compact (con, args) = + fun con_compact (con, _, args) = let val concl = mk_trp (mk_compact (con_app con args)); val goal = lift (fn x => mk_compact (%#x)) (args, concl); @@ -441,7 +441,7 @@ pg axs_sel_def (mk_trp (strict (%%:sel))) (K [simp_tac (HOLCF_ss addsimps when_rews) 1]); - fun sel_strict (_, args) = + fun sel_strict (_, _, args) = map_filter (Option.map one_sel o sel_of) args; in val _ = trace " Proving sel_stricts..."; @@ -472,14 +472,14 @@ val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; - fun sel_app c n sel (con, args) = + fun sel_app c n sel (con, _, args) = if con = c then sel_app_same c n sel (con, args) else sel_app_diff c n sel (con, args); fun one_sel c n sel = map (sel_app c n sel) cons; fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg); - fun one_con (c, args) = + fun one_con (c, _, args) = flat (map_filter I (mapn (one_sel' c) 0 args)); in val _ = trace " Proving sel_apps..."; @@ -501,7 +501,7 @@ val sel_defins = if length cons = 1 then map_filter (fn arg => Option.map sel_defin (sel_of arg)) - (filter_out is_lazy (snd (hd cons))) + (filter_out is_lazy (third (hd cons))) else []; end; @@ -522,7 +522,7 @@ val tacs = [simp_tac (HOL_ss addsimps rules) 1]; in pg con_appls goal (K tacs) end; - fun distinct (con1, args1) (con2, args2) = + fun distinct (con1, _, args1) (con2, _, args2) = let val arg1 = (con1, args1); val arg2 = @@ -554,7 +554,7 @@ val tacs = [simp_tac (HOL_ss addsimps rules) 1]; in pg con_appls goal (K tacs) end; - fun distinct (con1, args1) (con2, args2) = + fun distinct (con1, _, args1) (con2, _, args2) = let val arg1 = (con1, args1); val arg2 = @@ -576,7 +576,7 @@ val sargs = case largs of [_] => [] | _ => nonlazy args; val prop = lift_defined %: (sargs, mk_trp (prem === concl)); in pg con_appls prop end; - val cons' = filter (fn (_,args) => args<>[]) cons; + val cons' = filter (fn (_, _, args) => args<>[]) cons; in val _ = trace " Proving inverts..."; val inverts = @@ -584,14 +584,14 @@ val abs_less = ax_abs_iso RS (allI RS injection_less); val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1]; - in map (fn (con, args) => pgterm (op <<) con args (K tacs)) cons' end; + in map (fn (con, _, args) => pgterm (op <<) con args (K tacs)) cons' end; val _ = trace " Proving injects..."; val injects = let val abs_eq = ax_abs_iso RS (allI RS injection_eq); val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1]; - in map (fn (con, args) => pgterm (op ===) con args (K tacs)) cons' end; + in map (fn (con, _, args) => pgterm (op ===) con args (K tacs)) cons' end; end; (* ----- theorems concerning one induction step ----------------------------- *) @@ -610,7 +610,7 @@ end; local - fun copy_app (con, args) = + fun copy_app (con, _, args) = let val lhs = dc_copy`%"f"`(con_app con args); fun one_rhs arg = @@ -635,7 +635,7 @@ end; local - fun one_strict (con, args) = + fun one_strict (con, _, args) = let val goal = mk_trp (dc_copy`UU`(con_app con args) === UU); val rews = the_list copy_strict @ copy_apps @ con_rews; @@ -648,7 +648,7 @@ | ERROR s => (trace s; NONE) end; - fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args; + fun has_nonlazy_rec (_, _, args) = exists is_nonlazy_rec args; in val _ = trace " Proving copy_stricts..."; val copy_stricts = map_filter one_strict (filter has_nonlazy_rec cons); @@ -749,7 +749,7 @@ in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end; val take_0s = mapn take_0 1 dnames; val _ = trace " Proving take_apps..."; - fun one_take_app dn (con, args) = + fun one_take_app dn (con, _, args) = let fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; fun one_rhs arg = @@ -773,7 +773,7 @@ end; (* local *) local - fun one_con p (con,args) = + fun one_con p (con, _, args) = let fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg; val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args); @@ -794,7 +794,7 @@ fun ind_prems_tac prems = EVERY (maps (fn cons => (resolve_tac prems 1 :: - maps (fn (_,args) => + maps (fn (_,_,args) => resolve_tac prems 1 :: map (K(atac 1)) (nonlazy args) @ map (K(atac 1)) (filter is_rec args)) @@ -809,7 +809,7 @@ ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) - ) o snd) cons; + ) o third) cons; fun all_rec_to ns = rec_to forall not all_rec_to ns; fun warn (n,cons) = if all_rec_to [] false (n,cons) @@ -840,7 +840,7 @@ fun arg_tac arg = case_UU_tac context (prems @ con_rews) 1 (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg); - fun con_tacs (con, args) = + fun con_tacs (con, _, args) = asm_simp_tac take_ss 1 :: map arg_tac (filter is_nonlazy_rec args) @ [resolve_tac prems 1] @ @@ -927,7 +927,7 @@ etac disjE 1, asm_simp_tac (HOL_ss addsimps con_rews) 1, asm_simp_tac take_ss 1]; - fun con_tacs ctxt (con, args) = + fun con_tacs ctxt (con, _, args) = asm_simp_tac take_ss 1 :: maps (arg_tacs ctxt) (nonlazy_rec args); fun foo_tacs ctxt n (cons, cases) =