|
1 (* Title: HOLCF/Tools/Domain/domain_syntax.ML |
|
2 Author: David von Oheimb |
|
3 |
|
4 Syntax generator for domain command. |
|
5 *) |
|
6 |
|
7 signature DOMAIN_SYNTAX = |
|
8 sig |
|
9 val calc_syntax: |
|
10 typ -> |
|
11 (string * typ list) * |
|
12 (binding * (bool * binding option * typ) list * mixfix) list -> |
|
13 (binding * typ * mixfix) list * ast Syntax.trrule list |
|
14 |
|
15 val add_syntax: |
|
16 string -> |
|
17 ((string * typ list) * |
|
18 (binding * (bool * binding option * typ) list * mixfix) list) list -> |
|
19 theory -> theory |
|
20 end; |
|
21 |
|
22 |
|
23 structure Domain_Syntax :> DOMAIN_SYNTAX = |
|
24 struct |
|
25 |
|
26 open Domain_Library; |
|
27 infixr 5 -->; infixr 6 ->>; |
|
28 |
|
29 fun calc_syntax |
|
30 (dtypeprod : typ) |
|
31 ((dname : string, typevars : typ list), |
|
32 (cons': (binding * (bool * binding option * typ) list * mixfix) list)) |
|
33 : (binding * typ * mixfix) list * ast Syntax.trrule list = |
|
34 let |
|
35 (* ----- constants concerning the isomorphism ------------------------------- *) |
|
36 |
|
37 local |
|
38 fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t |
|
39 fun prod (_,args,_) = case args of [] => oneT |
|
40 | _ => foldr1 mk_sprodT (map opt_lazy args); |
|
41 fun freetvar s = let val tvar = mk_TFree s in |
|
42 if tvar mem typevars then freetvar ("t"^s) else tvar end; |
|
43 fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args); |
|
44 in |
|
45 val dtype = Type(dname,typevars); |
|
46 val dtype2 = foldr1 mk_ssumT (map prod cons'); |
|
47 val dnam = Long_Name.base_name dname; |
|
48 fun dbind s = Binding.name (dnam ^ s); |
|
49 val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn); |
|
50 val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn); |
|
51 val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); |
|
52 val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn); |
|
53 end; |
|
54 |
|
55 (* ----- constants concerning constructors, discriminators, and selectors --- *) |
|
56 |
|
57 local |
|
58 val escape = let |
|
59 fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs |
|
60 else c::esc cs |
|
61 | esc [] = [] |
|
62 in implode o esc o Symbol.explode end; |
|
63 fun dis_name_ con = Binding.name ("is_" ^ strip_esc (Binding.name_of con)); |
|
64 fun mat_name_ con = Binding.name ("match_" ^ strip_esc (Binding.name_of con)); |
|
65 fun pat_name_ con = Binding.name (strip_esc (Binding.name_of con) ^ "_pat"); |
|
66 fun con (name,args,mx) = (name, List.foldr (op ->>) dtype (map third args), mx); |
|
67 fun dis (con,args,mx) = (dis_name_ con, dtype->>trT, |
|
68 Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri)); |
|
69 (* strictly speaking, these constants have one argument, |
|
70 but the mixfix (without arguments) is introduced only |
|
71 to generate parse rules for non-alphanumeric names*) |
|
72 fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in |
|
73 if tvar mem typevars then freetvar ("t"^s) n else tvar end; |
|
74 fun mk_matT (a,bs,c) = a ->> foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c; |
|
75 fun mat (con,args,mx) = (mat_name_ con, |
|
76 mk_matT(dtype, map third args, freetvar "t" 1), |
|
77 Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri)); |
|
78 fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel; |
|
79 fun sel (con,args,mx) = List.mapPartial sel1 args; |
|
80 fun mk_patT (a,b) = a ->> mk_maybeT b; |
|
81 fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n); |
|
82 fun pat (con,args,mx) = (pat_name_ con, |
|
83 (mapn pat_arg_typ 1 args) |
|
84 ---> |
|
85 mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))), |
|
86 Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri)); |
|
87 |
|
88 in |
|
89 val consts_con = map con cons'; |
|
90 val consts_dis = map dis cons'; |
|
91 val consts_mat = map mat cons'; |
|
92 val consts_pat = map pat cons'; |
|
93 val consts_sel = List.concat(map sel cons'); |
|
94 end; |
|
95 |
|
96 (* ----- constants concerning induction ------------------------------------- *) |
|
97 |
|
98 val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn); |
|
99 val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn); |
|
100 |
|
101 (* ----- case translation --------------------------------------------------- *) |
|
102 |
|
103 local open Syntax in |
|
104 local |
|
105 fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con)); |
|
106 fun expvar n = Variable ("e"^(string_of_int n)); |
|
107 fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^ |
|
108 (string_of_int m)); |
|
109 fun argvars n args = mapn (argvar n) 1 args; |
|
110 fun app s (l,r) = mk_appl (Constant s) [l,r]; |
|
111 val cabs = app "_cabs"; |
|
112 val capp = app "Rep_CFun"; |
|
113 fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args); |
|
114 fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n); |
|
115 fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args); |
|
116 fun when1 n m = if n = m then arg1 n else K (Constant "UU"); |
|
117 |
|
118 fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"]; |
|
119 fun app_pat x = mk_appl (Constant "_pat") [x]; |
|
120 fun args_list [] = Constant "_noargs" |
|
121 | args_list xs = foldr1 (app "_args") xs; |
|
122 in |
|
123 val case_trans = |
|
124 ParsePrintRule |
|
125 (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')), |
|
126 capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x")); |
|
127 |
|
128 fun one_abscon_trans n (con,mx,args) = |
|
129 ParsePrintRule |
|
130 (cabs (con1 n (con,mx,args), expvar n), |
|
131 Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons')); |
|
132 val abscon_trans = mapn one_abscon_trans 1 cons'; |
|
133 |
|
134 fun one_case_trans (con,args,mx) = |
|
135 let |
|
136 val cname = c_ast con mx; |
|
137 val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat"); |
|
138 val ns = 1 upto length args; |
|
139 val xs = map (fn n => Variable ("x"^(string_of_int n))) ns; |
|
140 val ps = map (fn n => Variable ("p"^(string_of_int n))) ns; |
|
141 val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; |
|
142 in |
|
143 [ParseRule (app_pat (Library.foldl capp (cname, xs)), |
|
144 mk_appl pname (map app_pat xs)), |
|
145 ParseRule (app_var (Library.foldl capp (cname, xs)), |
|
146 app_var (args_list xs)), |
|
147 PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)), |
|
148 app "_match" (mk_appl pname ps, args_list vs))] |
|
149 end; |
|
150 val Case_trans = List.concat (map one_case_trans cons'); |
|
151 end; |
|
152 end; |
|
153 |
|
154 in ([const_rep, const_abs, const_when, const_copy] @ |
|
155 consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @ |
|
156 [const_take, const_finite], |
|
157 (case_trans::(abscon_trans @ Case_trans))) |
|
158 end; (* let *) |
|
159 |
|
160 (* ----- putting all the syntax stuff together ------------------------------ *) |
|
161 |
|
162 fun add_syntax |
|
163 (comp_dnam : string) |
|
164 (eqs' : ((string * typ list) * |
|
165 (binding * (bool * binding option * typ) list * mixfix) list) list) |
|
166 (thy'' : theory) = |
|
167 let |
|
168 val dtypes = map (Type o fst) eqs'; |
|
169 val boolT = HOLogic.boolT; |
|
170 val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes); |
|
171 val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes); |
|
172 val const_copy = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn); |
|
173 val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn); |
|
174 val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs'; |
|
175 in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ |
|
176 (if length eqs'>1 then [const_copy] else[])@ |
|
177 [const_bisim]) |
|
178 |> Sign.add_trrules_i (List.concat(map snd ctt)) |
|
179 end; (* let *) |
|
180 |
|
181 end; (* struct *) |