author  huffman 
Sat, 04 Jun 2005 00:22:08 +0200  
changeset 16221  879400e029bf 
parent 15570  8d8c70b41bab 
child 16621  78b32293a8b1 
permissions  rwrr 
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 
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

4 

14682
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
12876
diff
changeset

5 
HOLCF version of consts: handle continuous function types in mixfix 
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
12876
diff
changeset

6 
syntax. 
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

7 
*) 
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

8 

12625  9 
signature CONT_CONSTS = 
10 
sig 

11 
val add_consts: (bstring * string * mixfix) list > theory > theory 

12 
val add_consts_i: (bstring * typ * mixfix) list > theory > theory 

13 
end; 

14 

15 
structure ContConsts: CONT_CONSTS = 

4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

16 
struct 
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

17 

12625  18 

19 
(* misc utils *) 

4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

20 

2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

21 
open HOLCFLogic; 
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

22 

12625  23 
fun first (x,_,_) = x; 
24 
fun second (_,x,_) = x; 

25 
fun third (_,_,x) = x; 

4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

26 
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

27 
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

28 
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

29 

2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

30 
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

31 
let fun filt [] = ([],[]) 
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

32 
 filt (x::xs) = let val (ys,zs) = filt xs in 
12625  33 
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

34 
in filt end; 
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

35 

2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

36 
fun change_arrow 0 T = T 
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

37 
 change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n1) T]) 
12625  38 
 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

39 

2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

40 
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

41 
fun argnames _ 0 = [] 
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

42 
 argnames c n = chr c::argnames (c+1) (n1); 
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

43 
val vnames = argnames (ord "A") n; 
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

44 
val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1); 
5700  45 
in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames), 
15570  46 
Library.foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun") 
12625  47 
[t,Variable arg])) 
48 
(Constant name1,vnames))] 

11651  49 
@(case mx of InfixName _ => [extra_parse_rule] 
50 
 InfixlName _ => [extra_parse_rule] 

12625  51 
 InfixrName _ => [extra_parse_rule]  _ => []) end; 
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

52 

2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

53 

2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

54 
(* transforming infix/mixfix declarations of constants with type ...>... 
12625  55 
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

56 
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

57 
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

58 
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

59 
*) 
12625  60 
fun fix_mixfix (syn , T, mx as Infix p ) = 
61 
(Syntax.const_name syn mx, T, InfixName (syn, p)) 

62 
 fix_mixfix (syn , T, mx as Infixl p ) = 

63 
(Syntax.const_name syn mx, T, InfixlName (syn, p)) 

64 
 fix_mixfix (syn , T, mx as Infixr p ) = 

65 
(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

66 
 fix_mixfix decl = decl; 
12625  67 
fun transform decl = let 
68 
val (c, T, mx) = fix_mixfix decl; 

69 
val c2 = "_cont_" ^ c; 

70 
val n = Syntax.mixfix_args mx 

71 
in ((c , T,NoSyn), 

72 
(c2,change_arrow n T,mx ), 

73 
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

74 

2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

75 
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

76 
 cfun_arity _ = 0; 
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 is_contconst (_,_,NoSyn ) = false 
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

79 
 is_contconst (_,_,Binder _) = false 
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

80 
 is_contconst (c,T,mx ) = cfun_arity T >= Syntax.mixfix_args mx 
12625  81 
handle ERROR => error ("in mixfix annotation for " ^ 
82 
quote (Syntax.const_name c mx)); 

83 

4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

84 

12625  85 
(* add_consts(_i) *) 
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

86 

12625  87 
fun gen_add_consts prep_typ raw_decls thy = 
88 
let 

89 
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

90 
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

91 
val transformed_decls = map transform contconst_decls; 
12625  92 
in 
93 
thy 

94 
> Theory.add_consts_i normal_decls 

95 
> Theory.add_consts_i (map first transformed_decls) 

96 
> Theory.add_syntax_i (map second transformed_decls) 

15570  97 
> Theory.add_trrules_i (List.concat (map third transformed_decls)) 
12625  98 
end; 
99 

100 
val add_consts = gen_add_consts Thm.read_ctyp; 

101 
val add_consts_i = gen_add_consts Thm.ctyp_of; 

102 

103 

104 
(* outer syntax *) 

105 

106 
local structure P = OuterParse and K = OuterSyntax.Keyword in 

107 

108 
val constsP = 

109 
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

110 
(Scan.repeat1 P.const >> (Toplevel.theory o add_consts)); 
12625  111 

14682
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
12876
diff
changeset

112 
val _ = OuterSyntax.add_parsers [constsP]; 
12625  113 

4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

114 
end; 
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

115 

2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

116 

12625  117 
(* oldstyle theory syntax *) 
4129
2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

118 

2fd816aa6206
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff
changeset

119 
val _ = ThySyn.add_syntax [] 
12625  120 
[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

121 

12625  122 
end; 