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