author | oheimb |
Mon, 27 Oct 1997 11:34:33 +0100 | |
changeset 4008 | 2444085532c6 |
parent 3793 | 6e807b50b6c1 |
child 4122 | f63c283cefaf |
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$ |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
3 |
Author : David von Oheimb |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
4 |
Copyright 1995, 1996 TU Muenchen |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
5 |
|
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
6 |
syntax generator for domain section |
1274 | 7 |
*) |
8 |
||
9 |
structure Domain_Syntax = struct |
|
10 |
||
11 |
local |
|
12 |
||
13 |
open Domain_Library; |
|
14 |
infixr 5 -->; infixr 6 ~>; |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
15 |
fun calc_syntax dtypeprod ((dname, typevars), (cons': |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
16 |
(string * ThyOps.cmixfix * (bool*string*typ) list) list)) = |
1274 | 17 |
let |
18 |
(* ----- constants concerning the isomorphism ------------------------------------- *) |
|
19 |
||
20 |
local |
|
21 |
fun opt_lazy (lazy,_,t) = if lazy then Type("u",[t]) else t |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
22 |
fun prod (_,_,args) = if args = [] then Type("one",[]) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
23 |
else foldr'(mk_typ "**") (map opt_lazy args); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
24 |
fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
25 |
fun when_type (_ ,_,args) = foldr (op ~>) (map third args,freetvar "t"); |
1274 | 26 |
in |
27 |
val dtype = Type(dname,typevars); |
|
28 |
val dtype2 = foldr' (mk_typ "++") (map prod cons'); |
|
4008 | 29 |
val dnam = Sign.base_name dname; |
30 |
val const_rep = (dnam^"_rep" , dtype ~> dtype2, NoSyn'); |
|
31 |
val const_abs = (dnam^"_abs" , dtype2 ~> dtype , NoSyn'); |
|
32 |
val const_when = (dnam^"_when", foldr (op ~>) ((map when_type cons'), |
|
33 |
dtype ~> freetvar "t"), NoSyn'); |
|
34 |
val const_copy = (dnam^"_copy", dtypeprod ~> dtype ~> dtype , NoSyn'); |
|
1274 | 35 |
end; |
36 |
||
37 |
(* ----- constants concerning the constructors, discriminators and selectors ------ *) |
|
38 |
||
39 |
fun is_infix (ThyOps.CInfixl _ ) = true |
|
40 |
| is_infix (ThyOps.CInfixr _ ) = true |
|
41 |
| is_infix (ThyOps.Mixfix(Infixl _)) = true |
|
42 |
| is_infix (ThyOps.Mixfix(Infixr _)) = true |
|
43 |
| is_infix _ = false; |
|
44 |
||
45 |
local |
|
46 |
val escape = let |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
47 |
fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
48 |
else c :: esc cs |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
49 |
| esc [] = [] |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
50 |
in implode o esc o explode end; |
1274 | 51 |
fun con (name,s,args) = (name,foldr (op ~>) (map third args,dtype),s); |
52 |
fun dis (con ,s,_ ) = (dis_name_ con, dtype~>Type("tr",[]), |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
53 |
ThyOps.Mixfix(Mixfix("is'_"^ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
54 |
(if is_infix s then Id else escape)con,[],max_pri))); |
1274 | 55 |
fun sel (_ ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ~> typ,NoSyn'))args; |
56 |
in |
|
57 |
val consts_con = map con cons'; |
|
58 |
val consts_dis = map dis cons'; |
|
59 |
val consts_sel = flat(map sel cons'); |
|
60 |
end; |
|
61 |
||
62 |
(* ----- constants concerning induction ------------------------------------------- *) |
|
63 |
||
4008 | 64 |
val const_take = (dnam^"_take" , Type("nat",[]) --> dtype ~> dtype, NoSyn'); |
65 |
val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT , NoSyn'); |
|
1274 | 66 |
|
67 |
(* ----- case translation --------------------------------------------------------- *) |
|
68 |
||
69 |
local open Syntax in |
|
70 |
val case_trans = let |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
71 |
fun c_ast con syn = Constant (ThyOps.const_name con syn); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
72 |
fun expvar n = Variable ("e"^(string_of_int n)); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
73 |
fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^(string_of_int m)); |
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]; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
75 |
fun case1 n (con,syn,args) = mk_appl (Constant "@case1") |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
76 |
[if is_infix syn |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
77 |
then mk_appl (c_ast con syn) (mapn (argvar n) 1 args) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
78 |
else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)), |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
79 |
expvar n]; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
80 |
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
|
81 |
else mk_appl (Constant "LAM ") |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
82 |
[foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n]; |
3534 | 83 |
in |
84 |
ParsePrintRule |
|
85 |
(mk_appl (Constant "@case") [Variable "x", foldr' |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
86 |
(fn (c,cs) => mk_appl (Constant "@case2") [c,cs]) |
3534 | 87 |
(mapn case1 1 cons')], |
88 |
mk_appl (Constant "@fapp") [foldl |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
89 |
(fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ]) |
4008 | 90 |
(Constant (dnam^"_when"),mapn arg1 1 cons'), |
3534 | 91 |
Variable "x"]) |
1274 | 92 |
end; |
93 |
end; |
|
94 |
||
95 |
in ([const_rep, const_abs, const_when, const_copy] @ |
|
96 |
consts_con @ consts_dis @ consts_sel @ |
|
97 |
[const_take, const_finite], |
|
98 |
[case_trans]) |
|
99 |
end; (* let *) |
|
100 |
||
101 |
(* ----- putting all the syntax stuff together ------------------------------------ *) |
|
102 |
||
103 |
in (* local *) |
|
104 |
||
4008 | 105 |
fun add_syntax (comp_dnam,eqs': ((string * typ list) * |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
106 |
(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' = |
1274 | 107 |
let |
4008 | 108 |
val dtypes = map (Type o fst) eqs'; |
1274 | 109 |
val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp )dtypes); |
110 |
val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes); |
|
4008 | 111 |
val const_copy = (comp_dnam^"_copy" ,funprod ~> funprod , NoSyn'); |
112 |
val const_bisim = (comp_dnam^"_bisim" ,relprod --> HOLogic.boolT, NoSyn'); |
|
1274 | 113 |
val ctt = map (calc_syntax funprod) eqs'; |
114 |
val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false}; |
|
4008 | 115 |
in thy'' |> add_cur_ops_i (flat(map fst ctt)) |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
116 |
|> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim]) |
3771 | 117 |
|> Theory.add_trrules_i (flat(map snd ctt)) |
1274 | 118 |
end; (* let *) |
119 |
||
120 |
end; (* local *) |
|
121 |
end; (* struct *) |