# HG changeset patch # User huffman # Date 1258674112 28800 # Node ID 46cbbcbd4e6825846292be0f0d3bbaaa0d7bf779 # Parent d3616f61c5c4a9ba2aa9d15b8d656a3fbdd24eb7 clean up indentation; add 'definitional' option flag diff -r d3616f61c5c4 -r 46cbbcbd4e68 src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Nov 19 15:31:19 2009 -0800 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Nov 19 15:41:52 2009 -0800 @@ -9,10 +9,12 @@ val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term val calc_axioms : + bool -> string -> Domain_Library.eq list -> int -> Domain_Library.eq -> string * (string * term) list * (string * term) list val add_axioms : + bool -> bstring -> Domain_Library.eq list -> theory -> theory end; @@ -43,110 +45,111 @@ | 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) + (definitional : bool) + (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 ------------------ *) + let - 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; +(* ----- axioms and definitions concerning the isomorphism ------------------ *) - 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 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 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 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 = proj (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; + val copy_def = + let fun r i = proj (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; + 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 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 /\# + 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; + in map ddef cons end; - val mat_defs = + val mat_defs = + let + fun mdef (con,_) = 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 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 = + val pat_defs = + let + fun pdef (con,args) = 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 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 map_filter I (maps (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 map_filter I (maps (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(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n - `%x_name === %:x_name)); - val take_def = - ("take_def", - %%:(dname^"_take") == - mk_lam("n",proj - (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(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n + `%x_name === %:x_name)); + val take_def = + ("take_def", + %%:(dname^"_take") == + mk_lam("n",proj + (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], - [when_def, copy_def] @ - con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @ - [take_def, finite_def]) - end; (* let (calc_axioms) *) + in (dnam, + if definitional then [reach_ax] else [abs_iso_ax, rep_iso_ax, reach_ax], + [when_def, copy_def] @ + con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @ + [take_def, finite_def]) + end; (* let (calc_axioms) *) (* legacy type inference *) @@ -173,16 +176,17 @@ val ms = map qualify con_names ~~ map qualify mat_names; in Fixrec.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))); +fun add_axioms definitional 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))); - fun one_con (con,args) = let + fun one_con (con,args) = + let val nonrec_args = filter_out is_rec args; val rec_args = filter is_rec args; val recs_cnt = length rec_args; @@ -199,37 +203,43 @@ 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 + 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 (dnam, axs, dfs) = - Sign.add_path dnam + 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 (dnam, axs, dfs) = + Sign.add_path dnam #> add_defs_infer dfs #> add_axioms_infer axs #> Sign.parent_path; - val thy = fold add_one (mapn (calc_axioms comp_dname eqs) 0 eqs) thy'; + val thy = thy' + |> fold add_one (mapn (calc_axioms definitional 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 [])) - |> Sign.parent_path - |> fold add_matchers eqs - end; (* let (add_axioms) *) + in + thy + |> Sign.add_path comp_dnam + |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) + |> Sign.parent_path + |> fold add_matchers eqs + end; (* let (add_axioms) *) end; (* struct *) diff -r d3616f61c5c4 -r 46cbbcbd4e68 src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Thu Nov 19 15:31:19 2009 -0800 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Thu Nov 19 15:41:52 2009 -0800 @@ -17,6 +17,18 @@ ((string * string option) list * binding * mixfix * (binding * (bool * binding option * typ) list * mixfix) list) list -> theory -> theory + + val add_new_domain_cmd: + string -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * string) list * mixfix) list) list + -> theory -> theory + + val add_new_domain: + string -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * typ) list * mixfix) list) list + -> theory -> theory end; structure Domain_Extender :> DOMAIN_EXTENDER = @@ -26,13 +38,14 @@ (* ----- general testing and preprocessing of constructor list -------------- *) fun check_and_sort_domain + (definitional : bool) (dtnvs : (string * typ list) list) (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list) - (sg : theory) + (thy : theory) : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list = let - val defaultS = Sign.defaultS sg; + val defaultS = Sign.defaultS thy; val test_dupl_typs = case duplicates (op =) (map fst dtnvs) of @@ -78,27 +91,27 @@ | analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of NONE => - if s mem indirect_ok + if definitional orelse 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)) + quote (string_of_typ thy 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) ^ + quote (string_of_typ thy 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 + in if ok thy T then T else error ("Constructor argument type is not of sort pcpo: " ^ - string_of_typ sg T) + string_of_typ thy T) end; fun analyse_arg (lazy, sel, T) = (lazy, sel, check_pcpo lazy (analyse false T)); @@ -126,7 +139,8 @@ 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''' + val thy'' = + thy''' |> Sign.add_types (map thy_type dtnvs) |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; val cons'' = @@ -135,8 +149,8 @@ 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'; + check_and_sort_domain false dtnvs' cons'' thy''; + val thy' = thy'' |> Domain_Syntax.add_syntax false 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 (fn s => s = "'") ss + 1, ss); @@ -154,7 +168,82 @@ ) : cons; val eqs : eq list = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; - val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs; + val thy = thy' |> Domain_Axioms.add_axioms false 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) + |> PureThy.add_thmss + [((Binding.name "rews", flat rewss @ take_rews), [])] + |> snd + |> Sign.parent_path + end; + +fun gen_add_new_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); + + 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, @{sort rep}); + + (* this theory is used just for parsing and error checking *) + val tmp_thy = thy''' + |> Theory.copy + |> Sign.add_types (map thy_type dtnvs) + |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; + + val cons'' : (binding * (bool * binding option * typ) list * mixfix) list list = + map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons'''; + val dtnvs' : (string * typ list) list = + 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 true dtnvs' cons'' tmp_thy; + + fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T; + fun mk_con_typ (bind, args, mx) = + if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args); + fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons); + + val thy'' = thy''' |> + Domain_Isomorphism.domain_isomorphism + (map (fn ((vs, dname, mx, _), eq) => + (map fst vs, dname, mx, mk_eq_typ eq)) + (eqs''' ~~ eqs')) + + val thy' = thy'' |> Domain_Syntax.add_syntax true 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 (fn s => s = "'") 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 : eq list = + map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; + val thy = thy' |> Domain_Axioms.add_axioms true comp_dnam eqs; val ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs @@ -171,6 +260,9 @@ val add_domain = gen_add_domain Sign.certify_typ; val add_domain_cmd = gen_add_domain Syntax.read_typ_global; +val add_new_domain = gen_add_new_domain Sign.certify_typ; +val add_new_domain_cmd = gen_add_new_domain Syntax.read_typ_global; + (** outer syntax **) @@ -205,6 +297,7 @@ P.and_list1 domain_decl; fun mk_domain + (definitional : bool) (opt_name : string option, doms : ((((string * string option) list * binding) * mixfix) * ((binding * (bool * binding option * string) list) * mixfix) list) list ) = @@ -216,11 +309,19 @@ (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; + in + if definitional + then add_new_domain_cmd comp_dnam specs + else 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)); + K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false)); + +val _ = + OuterSyntax.command "new_domain" "define recursive domains (HOLCF)" + K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true)); end; diff -r d3616f61c5c4 -r 46cbbcbd4e68 src/HOLCF/Tools/Domain/domain_syntax.ML --- a/src/HOLCF/Tools/Domain/domain_syntax.ML Thu Nov 19 15:31:19 2009 -0800 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Thu Nov 19 15:41:52 2009 -0800 @@ -7,12 +7,14 @@ signature DOMAIN_SYNTAX = sig val calc_syntax: + bool -> typ -> (string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list -> (binding * typ * mixfix) list * ast Syntax.trrule list val add_syntax: + bool -> string -> ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list -> @@ -27,155 +29,176 @@ infixr 5 -->; infixr 6 ->>; fun calc_syntax - (dtypeprod : typ) - ((dname : string, typevars : typ list), - (cons': (binding * (bool * binding option * typ) list * mixfix) list)) + (definitional : bool) + (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 ------------------------------- *) + let +(* ----- 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 --- *) + + 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; - (* ----- constants concerning constructors, discriminators, and selectors --- *) + 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; - 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 ->> List.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) = map_filter 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)); + fun mk_matT (a,bs,c) = + a ->> List.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) = map_filter 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 = maps sel cons'; + end; + +(* ----- constants concerning induction ------------------------------------- *) + + 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 (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 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 - 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 = maps sel cons'; - end; - - (* ----- constants concerning induction ------------------------------------- *) - - 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 (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"); + [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 = maps one_case_trans cons'; + end; + end; + val rep_abs_consts = + if definitional then [] else [const_rep, const_abs]; - 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 = maps 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 @ - [const_take, const_finite], - (case_trans::(abscon_trans @ Case_trans))) - end; (* let *) + in (rep_abs_consts @ [const_when, const_copy] @ + consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @ + [const_take, const_finite], + (case_trans::(abscon_trans @ Case_trans))) + end; (* let *) (* ----- 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) = - 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'; - in thy'' |> ContConsts.add_consts_i (maps fst ctt @ - (if length eqs'>1 then [const_copy] else[])@ - [const_bisim]) - |> Sign.add_trrules_i (maps snd ctt) - end; (* let *) + (definitional : bool) + (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 definitional funprod) eqs'; + in thy'' + |> ContConsts.add_consts_i + (maps fst ctt @ + (if length eqs'>1 then [const_copy] else[])@ + [const_bisim]) + |> Sign.add_trrules_i (maps snd ctt) + end; (* let *) end; (* struct *)