# HG changeset patch # User wenzelm # Date 1266783024 -3600 # Node ID 3e5980f612d99e1d76997fcb393c4ccc3fade4ae # Parent b73ae1a8fe7eeefdb53740793fb069840c0f323d adapted to authentic syntax; misc cleanup and modernization; diff -r b73ae1a8fe7e -r 3e5980f612d9 src/HOLCF/Tools/cont_consts.ML --- a/src/HOLCF/Tools/cont_consts.ML Sun Feb 21 21:10:01 2010 +0100 +++ b/src/HOLCF/Tools/cont_consts.ML Sun Feb 21 21:10:24 2010 +0100 @@ -7,37 +7,28 @@ signature CONT_CONSTS = sig - val add_consts: (binding * string * mixfix) list -> theory -> theory - val add_consts_i: (binding * typ * mixfix) list -> theory -> theory + val add_consts: (binding * typ * mixfix) list -> theory -> theory + val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory end; -structure ContConsts: CONT_CONSTS = +structure Cont_Consts: CONT_CONSTS = struct (* misc utils *) -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 change_arrow 0 T = T -| change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T]) -| change_arrow _ _ = sys_error "cont_consts: change_arrow"; +fun change_arrow 0 T = T + | change_arrow n (Type (_, [S, T])) = Type ("fun", [S, change_arrow (n - 1) T]) + | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], []); fun trans_rules name2 name1 n mx = let - fun argnames _ 0 = [] - | argnames c n = chr c::argnames (c+1) (n-1); - val vnames = argnames (ord "A") n; + val vnames = Name.invents Name.context "a" n; val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1); in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames), - fold (fn arg => fn t => Syntax.mk_appl (Constant "Rep_CFun") [t, Variable arg]) + fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_CFun}) [t, Variable a]) vnames (Constant name1))] @ (case mx of Infix _ => [extra_parse_rule] @@ -53,42 +44,51 @@ declaration with the original name, type ...=>..., and the original mixfix is generated and connected to the other declaration via some translation. *) -fun transform (c, T, mx) = - let - val c1 = Binding.name_of c; - val c2 = "_cont_" ^ c1; - val n = Syntax.mixfix_args mx - in ((c, T, NoSyn), - (Binding.name c2, change_arrow n T, mx), - trans_rules c2 c1 n mx) end; +fun transform thy (c, T, mx) = + let + fun syntax b = Syntax.constN ^ Sign.full_bname thy b; + val c1 = Binding.name_of c; + val c2 = c1 ^ "_cont_syntax"; + val n = Syntax.mixfix_args mx; + in + ((c, T, NoSyn), + (Binding.name c2, change_arrow n T, mx), + trans_rules (syntax c2) (syntax c1) n mx) + end; -fun cfun_arity (Type(n,[_,T])) = if n = @{type_name "->"} then 1+cfun_arity T else 0 -| cfun_arity _ = 0; +fun cfun_arity (Type (n, [_, T])) = if n = @{type_name "->"} then 1 + cfun_arity T else 0 + | cfun_arity _ = 0; -fun is_contconst (_,_,NoSyn ) = false -| is_contconst (_,_,Binder _) = false -| is_contconst (c,T,mx ) = - cfun_arity T >= Syntax.mixfix_args mx - handle ERROR msg => cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c)); +fun is_contconst (_, _, NoSyn) = false + | is_contconst (_, _, Binder _) = false (* FIXME ? *) + | is_contconst (c, T, mx) = + let + val n = Syntax.mixfix_args mx handle ERROR msg => + cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c)); + in cfun_arity T >= n end; -(* add_consts(_i) *) +(* add_consts *) + +local fun gen_add_consts prep_typ raw_decls thy = let - val decls = map (upd_second (prep_typ thy)) raw_decls; + val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls; val (contconst_decls, normal_decls) = List.partition is_contconst decls; - val transformed_decls = map transform contconst_decls; + val transformed_decls = map (transform thy) contconst_decls; in thy - |> Sign.add_consts_i - (normal_decls @ map first transformed_decls @ map second transformed_decls) - (* FIXME authentic syntax *) - |> Sign.add_trrules_i (maps third transformed_decls) + |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls) + |> Sign.add_trrules_i (maps #3 transformed_decls) end; -val add_consts = gen_add_consts Syntax.read_typ_global; -val add_consts_i = gen_add_consts Sign.certify_typ; +in + +val add_consts = gen_add_consts Sign.certify_typ; +val add_consts_cmd = gen_add_consts Syntax.read_typ_global; + +end; (* outer syntax *) @@ -97,7 +97,7 @@ val _ = OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl - (Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts)); + (Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts_cmd)); end;