# HG changeset patch # User wenzelm # Date 1010077024 -3600 # Node ID 425ca8613a1d1b9a38ac902a5872972b149a98fa # Parent 9ed65232429c4e5d79cebbc9ef8d3d1c9a28d9ab Isar version; support constdefs, too; diff -r 9ed65232429c -r 425ca8613a1d src/HOLCF/cont_consts.ML --- a/src/HOLCF/cont_consts.ML Thu Jan 03 17:56:15 2002 +0100 +++ b/src/HOLCF/cont_consts.ML Thu Jan 03 17:57:04 2002 +0100 @@ -1,21 +1,31 @@ (* Title: HOLCF/cont_consts.ML ID: $Id$ - Author: Tobias Mayr and David von Oheimb + Author: Tobias Mayr, David von Oheimb, and Markus Wenzel License: GPL (GNU GENERAL PUBLIC LICENSE) -Theory extender for consts section. +HOLCF version of consts/constdefs: handle continuous function types in +mixfix syntax. *) -structure ContConsts = +signature CONT_CONSTS = +sig + val add_consts: (bstring * string * mixfix) list -> theory -> theory + val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory + val add_constdefs: ((bstring * string * mixfix) * string) list -> theory -> theory + val add_constdefs_i: ((bstring * typ * mixfix) * term) list -> theory -> theory +end; + +structure ContConsts: CONT_CONSTS = struct -local + +(* misc utils *) open HOLCFLogic; -exception Impossible of string; -fun Imposs msg = raise Impossible ("ContConst:"^msg); -fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x; +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); @@ -23,12 +33,12 @@ fun filter2 (pred: 'a->bool) : 'a list -> 'a list * 'a list = let fun filt [] = ([],[]) | filt (x::xs) = let val (ys,zs) = filt xs in - if pred x then (x::ys,zs) else (ys,x::zs) end + if pred x then (x::ys,zs) else (ys,x::zs) end in filt end; fun change_arrow 0 T = T | change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T]) -| change_arrow _ _ = Imposs "change_arrow"; +| change_arrow _ _ = sys_error "cont_consts: change_arrow"; fun trans_rules name2 name1 n mx = let fun argnames _ 0 = [] @@ -36,34 +46,34 @@ 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), - foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun") - [t,Variable arg])) - (Constant name1,vnames))] + 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; + | 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 + 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)) +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 = "@"^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 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; @@ -71,33 +81,63 @@ 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)); + handle ERROR => error ("in mixfix annotation for " ^ + quote (Syntax.const_name c mx)); + -in (* local *) +(* add_consts(_i) *) -fun ext_consts prep_typ raw_decls thy = -let val decls = map (upd_second (typ_of o prep_typ (sign_of thy))) raw_decls; +fun gen_add_consts prep_typ raw_decls thy = + let + val decls = map (upd_second (Thm.typ_of o prep_typ (Theory.sign_of thy))) raw_decls; val (contconst_decls, normal_decls) = filter2 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 (flat (map third transformed_decls)) - handle ERROR => - error ("The error(s) above occurred in (cont)consts section") + 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 (flat (map third transformed_decls)) + end; + +val add_consts = gen_add_consts Thm.read_ctyp; +val add_consts_i = gen_add_consts Thm.ctyp_of; + + +(* add_constdefs(_i) *) + +fun gen_add_constdefs consts defs args thy = + thy + |> consts (map fst args) + |> defs (false, map (fn ((c, _, mx), s) => + (((Thm.def_name (Syntax.const_name c mx), s), []), Comment.none)) args); + +fun add_constdefs args = gen_add_constdefs add_consts IsarThy.add_defs args; +fun add_constdefs_i args = gen_add_constdefs add_consts_i IsarThy.add_defs_i args; + + +(* outer syntax *) + +local structure P = OuterParse and K = OuterSyntax.Keyword in + +val constsP = + OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl + (Scan.repeat1 (P.const --| P.marg_comment) >> (Toplevel.theory o add_consts)); + +val constdefsP = + OuterSyntax.command "constdefs" "declare and define constants (HOLCF)" K.thy_decl + (Scan.repeat1 ((P.const --| P.marg_comment) -- (P.term --| P.marg_comment)) + >> (Toplevel.theory o add_constdefs)); + + +val _ = OuterSyntax.add_parsers [constsP, constdefsP]; + end; -fun cert_typ sg typ = - ctyp_of sg typ handle TYPE (msg, _, _) => error msg; -val add_consts = ext_consts read_ctyp; -val add_consts_i = ext_consts cert_typ; - -end; (* local *) - -end; (* struct *) +(* old-style theory syntax *) val _ = ThySyn.add_syntax [] - [ThyParse.section "consts" "|> ContConsts.add_consts" ThyParse.const_decls]; + [ThyParse.section "consts" "|> ContConsts.add_consts" ThyParse.const_decls]; +end;