author | oheimb |
Wed, 18 Dec 1996 15:16:13 +0100 | |
changeset 2445 | 51993fea433f |
parent 1637 | b8a8ae2e5de1 |
child 2446 | c2a9bf6c0948 |
permissions | -rw-r--r-- |
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
1 |
(* Title: HOLCF/domain/syntaxd.ML |
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'); |
|
29 |
val const_rep = (dname^"_rep" , dtype ~> dtype2, NoSyn'); |
|
30 |
val const_abs = (dname^"_abs" , dtype2 ~> dtype , NoSyn'); |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
31 |
val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'), |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
32 |
dtype ~> freetvar "t"), NoSyn'); |
1274 | 33 |
val const_copy = (dname^"_copy", dtypeprod ~> dtype ~> dtype , NoSyn'); |
34 |
end; |
|
35 |
||
36 |
(* ----- constants concerning the constructors, discriminators and selectors ------ *) |
|
37 |
||
38 |
fun is_infix (ThyOps.CInfixl _ ) = true |
|
39 |
| is_infix (ThyOps.CInfixr _ ) = true |
|
40 |
| is_infix (ThyOps.Mixfix(Infixl _)) = true |
|
41 |
| is_infix (ThyOps.Mixfix(Infixr _)) = true |
|
42 |
| is_infix _ = false; |
|
43 |
||
44 |
local |
|
45 |
val escape = let |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
46 |
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
|
47 |
else c :: esc cs |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
48 |
| esc [] = [] |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
49 |
in implode o esc o explode end; |
1274 | 50 |
fun con (name,s,args) = (name,foldr (op ~>) (map third args,dtype),s); |
51 |
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
|
52 |
ThyOps.Mixfix(Mixfix("is'_"^ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
53 |
(if is_infix s then Id else escape)con,[],max_pri))); |
1274 | 54 |
fun sel (_ ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ~> typ,NoSyn'))args; |
55 |
in |
|
56 |
val consts_con = map con cons'; |
|
57 |
val consts_dis = map dis cons'; |
|
58 |
val consts_sel = flat(map sel cons'); |
|
59 |
end; |
|
60 |
||
61 |
(* ----- constants concerning induction ------------------------------------------- *) |
|
62 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
63 |
val const_take = (dname^"_take" , Type("nat",[]) --> dtype ~> dtype, NoSyn'); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
64 |
val const_finite = (dname^"_finite", dtype-->HOLogic.boolT , NoSyn'); |
1274 | 65 |
|
66 |
(* ----- case translation --------------------------------------------------------- *) |
|
67 |
||
68 |
local open Syntax in |
|
69 |
val case_trans = let |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
70 |
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
|
71 |
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
|
72 |
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
|
73 |
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
|
74 |
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
|
75 |
[if is_infix syn |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
76 |
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
|
77 |
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
|
78 |
expvar n]; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
79 |
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
|
80 |
else mk_appl (Constant "LAM ") |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
81 |
[foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n]; |
1274 | 82 |
in 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
|
83 |
(fn (c,cs) => mk_appl (Constant "@case2") [c,cs]) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
84 |
(mapn case1 1 cons')] <-> |
1274 | 85 |
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
|
86 |
(fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ]) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
87 |
(Constant (dname^"_when"),mapn arg1 1 cons'), |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
88 |
Variable "x"] |
1274 | 89 |
end; |
90 |
end; |
|
91 |
||
92 |
in ([const_rep, const_abs, const_when, const_copy] @ |
|
93 |
consts_con @ consts_dis @ consts_sel @ |
|
94 |
[const_take, const_finite], |
|
95 |
[case_trans]) |
|
96 |
end; (* let *) |
|
97 |
||
98 |
(* ----- putting all the syntax stuff together ------------------------------------ *) |
|
99 |
||
100 |
in (* local *) |
|
101 |
||
102 |
fun add_syntax (comp_dname,eqs': ((string * typ list) * |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
103 |
(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' = |
1274 | 104 |
let |
2445
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
105 |
fun thy_type (dname,tvars) = (dname, length tvars, NoSyn); |
51993fea433f
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
oheimb
parents:
1637
diff
changeset
|
106 |
fun thy_arity (dname,tvars) = (dname, map (snd o rep_TFree) tvars, ["pcpo"]); |
1274 | 107 |
val thy_types = map (thy_type o fst) eqs'; |
108 |
val thy_arities = map (thy_arity o fst) eqs'; |
|
109 |
val dtypes = map (Type o fst) eqs'; |
|
110 |
val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp )dtypes); |
|
111 |
val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes); |
|
112 |
val const_copy = (comp_dname^"_copy" ,funprod ~> funprod , NoSyn'); |
|
113 |
val const_bisim = (comp_dname^"_bisim" ,relprod --> HOLogic.boolT, NoSyn'); |
|
114 |
val ctt = map (calc_syntax funprod) eqs'; |
|
115 |
val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false}; |
|
116 |
in thy'' |> add_types thy_types |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
117 |
|> add_arities thy_arities |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
118 |
|> add_cur_ops_i (flat(map fst ctt)) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
119 |
|> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim]) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
120 |
|> add_trrules_i (flat(map snd ctt)) |
1274 | 121 |
end; (* let *) |
122 |
||
123 |
end; (* local *) |
|
124 |
end; (* struct *) |