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