(* Title: HOLCF/cont_consts.ML ID: $Id: cont_consts.ML,v 1.13 2005/08/16 11:42:26 wenzelm Exp $ Author: Tobias Mayr, David von Oheimb, and Markus Wenzel HOLCF version of consts: handle continuous function types in mixfix syntax. *) signature CONT_CONSTS = sig val add_consts: (bstring * string * mixfix) list -> theory -> theory val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory end; structure ContConsts: CONT_CONSTS = struct (* misc utils *) open HOLCFLogic; 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 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 extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1); in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames), Library.foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun") [t,Variable arg])) (Constant name1,vnames))] @(case mx of InfixName _ => [extra_parse_rule] | InfixlName _ => [extra_parse_rule] | InfixrName _ => [extra_parse_rule] | _ => []) end; (* transforming infix/mixfix declarations of constants with type ...->... a declaration of such a constant is transformed to a normal declaration with an internal name, the same type, and nofix. Additionally, a purely syntactic declaration with the original name, type ...=>..., and the original mixfix is generated and connected to the other declaration via some translation. *) fun fix_mixfix (syn , T, mx as Infix p ) = (Syntax.const_name syn mx, T, InfixName (syn, p)) | fix_mixfix (syn , T, mx as Infixl p ) = (Syntax.const_name syn mx, T, InfixlName (syn, p)) | fix_mixfix (syn , T, mx as Infixr p ) = (Syntax.const_name syn mx, T, InfixrName (syn, p)) | fix_mixfix decl = decl; fun transform decl = let val (c, T, mx) = fix_mixfix decl; val c2 = "_cont_" ^ c; val n = Syntax.mixfix_args mx in ((c , T,NoSyn), (c2,change_arrow n T,mx ), trans_rules c2 c n mx) end; fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow 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 => error ("in mixfix annotation for " ^ quote (Syntax.const_name c mx)); (* add_consts(_i) *) fun gen_add_consts prep_typ raw_decls thy = let val decls = map (upd_second (Thm.typ_of o prep_typ thy)) raw_decls; val (contconst_decls, normal_decls) = List.partition is_contconst decls; val transformed_decls = map transform contconst_decls; in thy |> Theory.add_consts_i normal_decls |> Theory.add_consts_i (map first transformed_decls) |> Theory.add_syntax_i (map second transformed_decls) |> Theory.add_trrules_i (List.concat (map third transformed_decls)) end; val add_consts = gen_add_consts Thm.read_ctyp; val add_consts_i = gen_add_consts Thm.ctyp_of; (* outer syntax *) local structure P = OuterParse and K = OuterKeyword in val constsP = OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl (Scan.repeat1 P.const >> (Toplevel.theory o add_consts)); val _ = OuterSyntax.add_parsers [constsP]; end; (* old-style theory syntax *) val _ = ThySyn.add_syntax [] [ThyParse.section "consts" "|> ContConsts.add_consts" ThyParse.const_decls]; end;