author | wenzelm |
Thu, 14 Jul 2005 19:28:24 +0200 | |
changeset 16842 | 5979c46853d1 |
parent 16394 | 495dbcd4f4c9 |
child 17811 | 10ebcd7032c1 |
permissions | -rw-r--r-- |
2453 | 1 |
(* Title: HOLCF/domain/syntax.ML |
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
2 |
ID: $Id$ |
12030 | 3 |
Author: David von Oheimb |
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
4 |
|
12030 | 5 |
Syntax generator for domain section. |
1274 | 6 |
*) |
7 |
||
8 |
structure Domain_Syntax = struct |
|
9 |
||
10 |
local |
|
11 |
||
12 |
open Domain_Library; |
|
4122 | 13 |
infixr 5 -->; infixr 6 ->>; |
14 |
fun calc_syntax dtypeprod ((dname, typevars), |
|
16394
495dbcd4f4c9
in domain declarations, selector names are now optional
huffman
parents:
16224
diff
changeset
|
15 |
(cons': (string * mixfix * (bool*string option*typ) list) list)) = |
1274 | 16 |
let |
4122 | 17 |
(* ----- constants concerning the isomorphism ------------------------------- *) |
1274 | 18 |
|
19 |
local |
|
4122 | 20 |
fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t |
21 |
fun prod (_,_,args) = if args = [] then oneT |
|
22 |
else foldr' mk_sprodT (map opt_lazy args); |
|
23 |
fun freetvar s = let val tvar = mk_TFree s in |
|
24 |
if tvar mem typevars then freetvar ("t"^s) else tvar end; |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
25 |
fun when_type (_ ,_,args) = foldr (op ->>) (freetvar "t") (map third args); |
1274 | 26 |
in |
27 |
val dtype = Type(dname,typevars); |
|
4122 | 28 |
val dtype2 = foldr' mk_ssumT (map prod cons'); |
4008 | 29 |
val dnam = Sign.base_name dname; |
4122 | 30 |
val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn); |
31 |
val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn); |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
32 |
val const_when = (dnam^"_when",foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); |
4122 | 33 |
val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn); |
1274 | 34 |
end; |
35 |
||
4122 | 36 |
(* ----- constants concerning constructors, discriminators, and selectors --- *) |
1274 | 37 |
|
38 |
local |
|
39 |
val escape = let |
|
4122 | 40 |
fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs |
41 |
else c::esc cs |
|
42 |
| esc [] = [] |
|
4709 | 43 |
in implode o esc o Symbol.explode end; |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
44 |
fun con (name,s,args) = (name,foldr (op ->>) dtype (map third args),s); |
4122 | 45 |
fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT, |
5700 | 46 |
Mixfix(escape ("is_" ^ con), [], Syntax.max_pri)); |
4122 | 47 |
(* stricly speaking, these constants have one argument, |
48 |
but the mixfix (without arguments) is introduced only |
|
49 |
to generate parse rules for non-alphanumeric names*) |
|
16224
57094b83774e
Domain package generates match functions for new datatypes, for use with the fixrec package
huffman
parents:
15574
diff
changeset
|
50 |
fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_ssumT(oneT,mk_uT(mk_ctupleT(map third args))), |
57094b83774e
Domain package generates match functions for new datatypes, for use with the fixrec package
huffman
parents:
15574
diff
changeset
|
51 |
Mixfix(escape ("match_" ^ con), [], Syntax.max_pri)); |
16394
495dbcd4f4c9
in domain declarations, selector names are now optional
huffman
parents:
16224
diff
changeset
|
52 |
fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel; |
495dbcd4f4c9
in domain declarations, selector names are now optional
huffman
parents:
16224
diff
changeset
|
53 |
fun sel (_ ,_,args) = List.mapPartial sel1 args; |
1274 | 54 |
in |
55 |
val consts_con = map con cons'; |
|
56 |
val consts_dis = map dis cons'; |
|
16224
57094b83774e
Domain package generates match functions for new datatypes, for use with the fixrec package
huffman
parents:
15574
diff
changeset
|
57 |
val consts_mat = map mat cons'; |
15570 | 58 |
val consts_sel = List.concat(map sel cons'); |
1274 | 59 |
end; |
60 |
||
4122 | 61 |
(* ----- constants concerning induction ------------------------------------- *) |
1274 | 62 |
|
4122 | 63 |
val const_take = (dnam^"_take" , HOLogic.natT-->dtype->>dtype, NoSyn); |
64 |
val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT , NoSyn); |
|
1274 | 65 |
|
4122 | 66 |
(* ----- case translation --------------------------------------------------- *) |
1274 | 67 |
|
68 |
local open Syntax in |
|
69 |
val case_trans = let |
|
4122 | 70 |
fun c_ast con mx = Constant (const_name con mx); |
71 |
fun expvar n = Variable ("e"^(string_of_int n)); |
|
72 |
fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^ |
|
73 |
(string_of_int m)); |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
74 |
fun app s (l,r) = mk_appl (Constant s) [l,r]; |
9060
b0dd884b1848
rename @case to _case_syntax (improves on low-level errors);
wenzelm
parents:
5700
diff
changeset
|
75 |
fun case1 n (con,mx,args) = mk_appl (Constant "_case1") |
15570 | 76 |
[Library.foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)), |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
77 |
expvar n]; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
78 |
fun arg1 n (con,_,args) = if args = [] then expvar n |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
79 |
else mk_appl (Constant "LAM ") |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
80 |
[foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n]; |
3534 | 81 |
in |
82 |
ParsePrintRule |
|
9060
b0dd884b1848
rename @case to _case_syntax (improves on low-level errors);
wenzelm
parents:
5700
diff
changeset
|
83 |
(mk_appl (Constant "_case_syntax") [Variable "x", foldr' |
b0dd884b1848
rename @case to _case_syntax (improves on low-level errors);
wenzelm
parents:
5700
diff
changeset
|
84 |
(fn (c,cs) => mk_appl (Constant"_case2") [c,cs]) |
3534 | 85 |
(mapn case1 1 cons')], |
15570 | 86 |
mk_appl (Constant "Rep_CFun") [Library.foldl |
5291 | 87 |
(fn (w,a ) => mk_appl (Constant"Rep_CFun" ) [w,a ]) |
4008 | 88 |
(Constant (dnam^"_when"),mapn arg1 1 cons'), |
3534 | 89 |
Variable "x"]) |
1274 | 90 |
end; |
91 |
end; |
|
92 |
||
93 |
in ([const_rep, const_abs, const_when, const_copy] @ |
|
16224
57094b83774e
Domain package generates match functions for new datatypes, for use with the fixrec package
huffman
parents:
15574
diff
changeset
|
94 |
consts_con @ consts_dis @ consts_mat @ consts_sel @ |
1274 | 95 |
[const_take, const_finite], |
96 |
[case_trans]) |
|
97 |
end; (* let *) |
|
98 |
||
4122 | 99 |
(* ----- putting all the syntax stuff together ------------------------------ *) |
1274 | 100 |
|
101 |
in (* local *) |
|
102 |
||
4008 | 103 |
fun add_syntax (comp_dnam,eqs': ((string * typ list) * |
16394
495dbcd4f4c9
in domain declarations, selector names are now optional
huffman
parents:
16224
diff
changeset
|
104 |
(string * mixfix * (bool*string option*typ) list) list) list) thy'' = |
1274 | 105 |
let |
4122 | 106 |
val dtypes = map (Type o fst) eqs'; |
107 |
val boolT = HOLogic.boolT; |
|
16842 | 108 |
val funprod = foldr' HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes); |
109 |
val relprod = foldr' HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes); |
|
4122 | 110 |
val const_copy = (comp_dnam^"_copy" ,funprod ->> funprod, NoSyn); |
111 |
val const_bisim = (comp_dnam^"_bisim" ,relprod --> boolT , NoSyn); |
|
1274 | 112 |
val ctt = map (calc_syntax funprod) eqs'; |
15570 | 113 |
in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ |
4122 | 114 |
(if length eqs'>1 then [const_copy] else[])@ |
115 |
[const_bisim]) |
|
15570 | 116 |
|> Theory.add_trrules_i (List.concat(map snd ctt)) |
1274 | 117 |
end; (* let *) |
118 |
||
119 |
end; (* local *) |
|
120 |
end; (* struct *) |