author | paulson |
Fri, 21 Nov 2003 11:15:40 +0100 | |
changeset 14265 | 95b42e69436c |
parent 12876 | a70df1e5bf10 |
child 14682 | a5072752114c |
permissions | -rw-r--r-- |
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOLCF/cont_consts.ML |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
12625 | 3 |
Author: Tobias Mayr, David von Oheimb, and Markus Wenzel |
12030 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
5 |
|
12625 | 6 |
HOLCF version of consts/constdefs: handle continuous function types in |
7 |
mixfix syntax. |
|
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
8 |
*) |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
9 |
|
12625 | 10 |
signature CONT_CONSTS = |
11 |
sig |
|
12 |
val add_consts: (bstring * string * mixfix) list -> theory -> theory |
|
13 |
val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory |
|
14 |
val add_constdefs: ((bstring * string * mixfix) * string) list -> theory -> theory |
|
15 |
val add_constdefs_i: ((bstring * typ * mixfix) * term) list -> theory -> theory |
|
16 |
end; |
|
17 |
||
18 |
structure ContConsts: CONT_CONSTS = |
|
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
19 |
struct |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
20 |
|
12625 | 21 |
|
22 |
(* misc utils *) |
|
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
23 |
|
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
24 |
open HOLCFLogic; |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
25 |
|
12625 | 26 |
fun first (x,_,_) = x; |
27 |
fun second (_,x,_) = x; |
|
28 |
fun third (_,_,x) = x; |
|
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
29 |
fun upd_first f (x,y,z) = (f x, y, z); |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
30 |
fun upd_second f (x,y,z) = ( x, f y, z); |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
31 |
fun upd_third f (x,y,z) = ( x, y, f z); |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
32 |
|
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
33 |
fun filter2 (pred: 'a->bool) : 'a list -> 'a list * 'a list = |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
34 |
let fun filt [] = ([],[]) |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
35 |
| filt (x::xs) = let val (ys,zs) = filt xs in |
12625 | 36 |
if pred x then (x::ys,zs) else (ys,x::zs) end |
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
37 |
in filt end; |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
38 |
|
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
39 |
fun change_arrow 0 T = T |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
40 |
| change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T]) |
12625 | 41 |
| change_arrow _ _ = sys_error "cont_consts: change_arrow"; |
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
42 |
|
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
43 |
fun trans_rules name2 name1 n mx = let |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
44 |
fun argnames _ 0 = [] |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
45 |
| argnames c n = chr c::argnames (c+1) (n-1); |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
46 |
val vnames = argnames (ord "A") n; |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
47 |
val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1); |
5700 | 48 |
in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames), |
12625 | 49 |
foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun") |
50 |
[t,Variable arg])) |
|
51 |
(Constant name1,vnames))] |
|
11651 | 52 |
@(case mx of InfixName _ => [extra_parse_rule] |
53 |
| InfixlName _ => [extra_parse_rule] |
|
12625 | 54 |
| InfixrName _ => [extra_parse_rule] | _ => []) end; |
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
55 |
|
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
56 |
|
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
57 |
(* transforming infix/mixfix declarations of constants with type ...->... |
12625 | 58 |
a declaration of such a constant is transformed to a normal declaration with |
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
59 |
an internal name, the same type, and nofix. Additionally, a purely syntactic |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
60 |
declaration with the original name, type ...=>..., and the original mixfix |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
61 |
is generated and connected to the other declaration via some translation. |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
62 |
*) |
12625 | 63 |
fun fix_mixfix (syn , T, mx as Infix p ) = |
64 |
(Syntax.const_name syn mx, T, InfixName (syn, p)) |
|
65 |
| fix_mixfix (syn , T, mx as Infixl p ) = |
|
66 |
(Syntax.const_name syn mx, T, InfixlName (syn, p)) |
|
67 |
| fix_mixfix (syn , T, mx as Infixr p ) = |
|
68 |
(Syntax.const_name syn mx, T, InfixrName (syn, p)) |
|
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
69 |
| fix_mixfix decl = decl; |
12625 | 70 |
fun transform decl = let |
71 |
val (c, T, mx) = fix_mixfix decl; |
|
72 |
val c2 = "_cont_" ^ c; |
|
73 |
val n = Syntax.mixfix_args mx |
|
74 |
in ((c , T,NoSyn), |
|
75 |
(c2,change_arrow n T,mx ), |
|
76 |
trans_rules c2 c n mx) end; |
|
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
77 |
|
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
78 |
fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0 |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
79 |
| cfun_arity _ = 0; |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
80 |
|
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
81 |
fun is_contconst (_,_,NoSyn ) = false |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
82 |
| is_contconst (_,_,Binder _) = false |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
83 |
| is_contconst (c,T,mx ) = cfun_arity T >= Syntax.mixfix_args mx |
12625 | 84 |
handle ERROR => error ("in mixfix annotation for " ^ |
85 |
quote (Syntax.const_name c mx)); |
|
86 |
||
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
87 |
|
12625 | 88 |
(* add_consts(_i) *) |
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
89 |
|
12625 | 90 |
fun gen_add_consts prep_typ raw_decls thy = |
91 |
let |
|
92 |
val decls = map (upd_second (Thm.typ_of o prep_typ (Theory.sign_of thy))) raw_decls; |
|
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
93 |
val (contconst_decls, normal_decls) = filter2 is_contconst decls; |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
94 |
val transformed_decls = map transform contconst_decls; |
12625 | 95 |
in |
96 |
thy |
|
97 |
|> Theory.add_consts_i normal_decls |
|
98 |
|> Theory.add_consts_i (map first transformed_decls) |
|
99 |
|> Theory.add_syntax_i (map second transformed_decls) |
|
100 |
|> Theory.add_trrules_i (flat (map third transformed_decls)) |
|
101 |
end; |
|
102 |
||
103 |
val add_consts = gen_add_consts Thm.read_ctyp; |
|
104 |
val add_consts_i = gen_add_consts Thm.ctyp_of; |
|
105 |
||
106 |
||
107 |
(* add_constdefs(_i) *) |
|
108 |
||
109 |
fun gen_add_constdefs consts defs args thy = |
|
110 |
thy |
|
111 |
|> consts (map fst args) |
|
112 |
|> defs (false, map (fn ((c, _, mx), s) => |
|
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12625
diff
changeset
|
113 |
((Thm.def_name (Syntax.const_name c mx), s), [])) args); |
12625 | 114 |
|
115 |
fun add_constdefs args = gen_add_constdefs add_consts IsarThy.add_defs args; |
|
116 |
fun add_constdefs_i args = gen_add_constdefs add_consts_i IsarThy.add_defs_i args; |
|
117 |
||
118 |
||
119 |
(* outer syntax *) |
|
120 |
||
121 |
local structure P = OuterParse and K = OuterSyntax.Keyword in |
|
122 |
||
123 |
val constsP = |
|
124 |
OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl |
|
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12625
diff
changeset
|
125 |
(Scan.repeat1 P.const >> (Toplevel.theory o add_consts)); |
12625 | 126 |
|
127 |
val constdefsP = |
|
128 |
OuterSyntax.command "constdefs" "declare and define constants (HOLCF)" K.thy_decl |
|
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12625
diff
changeset
|
129 |
(Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o add_constdefs)); |
12625 | 130 |
|
131 |
||
132 |
val _ = OuterSyntax.add_parsers [constsP, constdefsP]; |
|
133 |
||
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
134 |
end; |
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
135 |
|
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
136 |
|
12625 | 137 |
(* old-style theory syntax *) |
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
138 |
|
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
139 |
val _ = ThySyn.add_syntax [] |
12625 | 140 |
[ThyParse.section "consts" "|> ContConsts.add_consts" ThyParse.const_decls]; |
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset
|
141 |
|
12625 | 142 |
end; |