author | clasohm |
Fri, 08 Jul 1994 12:01:55 +0200 | |
changeset 91 | a94029edb01f |
parent 87 | b0ea0e55dfe8 |
child 92 | bcd0ee8d71aa |
permissions | -rw-r--r-- |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
1 |
(* Title: HOL/Datatype |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
2 |
ID: $Id$ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
3 |
Author: Max Breitling / Carsten Clasohm |
53 | 4 |
Copyright 1994 TU Muenchen |
5 |
*) |
|
6 |
||
7 |
||
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
8 |
(*choice between Ci_neg1 and Ci_neg2 axioms depends on number of constructors*) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
9 |
val dtK = 5; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
10 |
|
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
11 |
local open ThyParse in |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
12 |
val datatype_decls = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
13 |
let fun cat s1 s2 = s1 ^ " " ^ s2; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
14 |
|
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
15 |
val pars = parents "(" ")"; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
16 |
val brackets = parents "[" "]"; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
17 |
|
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
18 |
val mk_list = brackets o commas; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
19 |
|
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
20 |
val tvar = type_var >> cat "dtVar"; |
53 | 21 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
22 |
val type_var_list = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
23 |
tvar >> (fn s => [s]) || "(" $$-- list1 tvar --$$ ")"; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
24 |
|
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
25 |
val typ = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
26 |
ident >> (cat "dtId" o quote) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
27 |
|| |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
28 |
type_var_list -- ident >> (fn (ts, id) => "Comp (" ^ mk_list ts ^ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
29 |
", " ^ quote id ^ ")") |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
30 |
|| |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
31 |
tvar; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
32 |
|
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
33 |
val typ_list = "(" $$-- list1 typ --$$ ")" || empty; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
34 |
|
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
35 |
val cons = name -- typ_list -- opt_mixfix; |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
36 |
|
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
37 |
fun constructs ts = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
38 |
( cons --$$ "|" -- constructs >> op:: |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
39 |
|| |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
40 |
cons >> (fn c => [c])) ts; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
41 |
|
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
42 |
val mk_cons = map (fn ((s, ts), syn) => |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
43 |
pars (commas [s, mk_list ts, syn])); |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
44 |
|
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
45 |
(*remove all quotes from a string*) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
46 |
fun rem_quotes s = implode (filter (fn c => c <> "\"") (explode s)); |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
47 |
|
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
48 |
(*generate names of ineq axioms*) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
49 |
fun rules_ineq cs tname = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
50 |
let (*combine all constructor names with all others w/o duplicates*) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
51 |
fun negOne _ [] = [] |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
52 |
| negOne (c : (string * 'a) * 'b) ((c2 : (string * 'a) * 'b) |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
53 |
:: cs) = |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
54 |
quote ("ineq_" ^ rem_quotes (#1 (#1 c)) ^ "_" ^ |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
55 |
rem_quotes (#1 (#1 c2))) :: negOne c cs; |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
56 |
|
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
57 |
fun neg1 [] = [] |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
58 |
| neg1 (c1 :: cs) = (negOne c1 cs) @ (neg1 cs) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
59 |
in if length cs < dtK then neg1 cs |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
60 |
else map (fn n => quote (tname ^ "_ord" ^ string_of_int n)) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
61 |
(0 upto (length cs)) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
62 |
end; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
63 |
|
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
64 |
fun arg1 ((_, ts), _) = not (null ts); |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
65 |
|
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
66 |
(*generate string for calling 'add_datatype'*) |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
67 |
fun mk_params ((ts, tname), cons) = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
68 |
("|> add_datatype\n" ^ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
69 |
pars (commas [mk_list ts, quote tname, mk_list (mk_cons cons)]), |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
70 |
"structure " ^ tname ^ " =\n\ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
71 |
\struct\n\ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
72 |
\ val inject = map (get_axiom thy) " ^ |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
73 |
mk_list (map (fn ((s,_), _) => quote ("inject_" ^ rem_quotes s)) |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
74 |
(filter arg1 cons)) ^ ";\n\ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
75 |
\ val ineq = " ^ (if length cons < dtK then "let val ineq' = " else "") |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
76 |
^ "map (get_axiom thy) " ^ mk_list (rules_ineq cons tname) ^ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
77 |
(if length cons < dtK then |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
78 |
" in ineq' @ (map (fn t => sym COMP (t RS contrapos)) ineq') end" |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
79 |
else "") ^ ";\n\ |
87 | 80 |
\ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\ |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
81 |
\ val cases = map (get_axiom thy) " ^ |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
82 |
mk_list (map (fn ((s,_),_) => |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
83 |
quote(tname ^ "_case_" ^ rem_quotes s)) cons) ^ ";\n\ |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
84 |
\ val simps = inject @ ineq @ cases;\n\ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
85 |
\ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
86 |
\end;\n"); |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
87 |
in (type_var_list || empty) -- ident --$$ "=" -- constructs >> mk_params end |
53 | 88 |
end; |
89 |
||
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
90 |
(*used for constructor parameters*) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
91 |
datatype dt_type = dtVar of string | |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
92 |
dtId of string | |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
93 |
Comp of dt_type list * string | |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
94 |
Rek of dt_type list * string; |
53 | 95 |
|
96 |
exception Impossible; |
|
97 |
||
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
98 |
local open Syntax.Mixfix in |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
99 |
fun add_datatype (typevars, tname, cons_list') thy = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
100 |
let fun cat s1 s2 = s1 ^ " " ^ s2; |
53 | 101 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
102 |
val pars = parents "(" ")"; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
103 |
val brackets = parents "[" "]"; |
53 | 104 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
105 |
val mk_list = brackets o commas; |
53 | 106 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
107 |
(*check if constructor names are unique*) |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
108 |
fun check_cons (cs : (string * 'b * 'c) list) = |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
109 |
(case findrep (map #1 cs) of |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
110 |
[] => true |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
111 |
| c::_ => error("Constructor \"" ^ c ^ "\" occurs twice")); |
53 | 112 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
113 |
(*search for free type variables and convert recursive *) |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
114 |
fun analyse_types (cons, typlist, syn) = |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
115 |
let fun analyse ((dtVar v) :: typlist) = |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
116 |
if ((dtVar v) mem typevars) then |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
117 |
(dtVar v) :: analyse typlist |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
118 |
else error ("Variable " ^ v ^ " is free.") |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
119 |
| analyse ((dtId s) :: typlist) = |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
120 |
if tname<>s then (dtId s) :: analyse typlist |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
121 |
else if null typevars then |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
122 |
Rek ([], tname) :: analyse typlist |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
123 |
else error (s ^ " used in different ways") |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
124 |
| analyse (Comp (typl,s) :: typlist) = |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
125 |
if tname <> s then Comp (analyse typl, s) |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
126 |
:: analyse typlist |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
127 |
else if typevars = typl then |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
128 |
Rek (typl, s) :: analyse typlist |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
129 |
else |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
130 |
error (s ^ " used in different ways") |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
131 |
| analyse [] = [] |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
132 |
| analyse ((Rek _) :: _) = raise Impossible; |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
133 |
in (cons, analyse typlist, syn) end; |
53 | 134 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
135 |
(*test if there are elements that are not recursive, i.e. if the type is |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
136 |
not empty*) |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
137 |
fun one_not_rek (cs : ('a * dt_type list * 'c) list) = |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
138 |
let val contains_no_rek = forall (fn Rek _ => false | _ => true); |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
139 |
in exists (contains_no_rek o #2) cs orelse |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
140 |
error("Empty type not allowed!") end; |
53 | 141 |
|
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
142 |
val dummy = check_cons cons_list'; |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
143 |
val cons_list = map analyse_types cons_list'; |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
144 |
val dummy = one_not_rek cons_list; |
53 | 145 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
146 |
(*Pretty printers for type lists; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
147 |
pp_typlist1: parentheses, pp_typlist2: brackets*) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
148 |
fun pp_typ (dtVar s) = s |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
149 |
| pp_typ (dtId s) = s |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
150 |
| pp_typ (Comp (typvars, id)) = (pp_typlist1 typvars) ^ id |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
151 |
| pp_typ (Rek (typvars, id)) = (pp_typlist1 typvars) ^ id |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
152 |
and |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
153 |
pp_typlist' ts = commas (map pp_typ ts) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
154 |
and |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
155 |
pp_typlist1 ts = if null ts then "" else pars (pp_typlist' ts); |
53 | 156 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
157 |
fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts); |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
158 |
|
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
159 |
fun Args(var, delim, n, m) = if n = m then var ^ string_of_int(n) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
160 |
else var ^ string_of_int(n) ^ delim ^ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
161 |
Args(var, delim, n+1, m); |
53 | 162 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
163 |
(* Generate syntax translation for case rules *) |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
164 |
fun calc_xrules c_nr y_nr ((id, typlist, syn) :: cs) = |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
165 |
let val name = const_name id syn; |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
166 |
val arity = length typlist; |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
167 |
val body = "z" ^ string_of_int(c_nr); |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
168 |
val args1 = if arity=0 then "" |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
169 |
else pars (Args ("y", ",", y_nr, y_nr+arity-1)); |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
170 |
val args2 = if arity=0 then "" |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
171 |
else "% " ^ Args ("y", " ", y_nr, y_nr+arity-1) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
172 |
^ ". "; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
173 |
val (rest1,rest2) = |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
174 |
if null cs then ("","") |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
175 |
else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
176 |
in (" | " ^ h1, ", " ^ h2) end; |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
177 |
in (name ^ args1 ^ " => " ^ body ^ rest1, args2 ^ body ^ rest2) end |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
178 |
| calc_xrules _ _ [] = raise Impossible; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
179 |
|
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
180 |
val xrules = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
181 |
let val (first_part, scnd_part) = calc_xrules 1 1 cons_list |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
182 |
in [("logic", "case x of " ^ first_part) <-> |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
183 |
("logic", tname ^ "_case(x, " ^ scnd_part ^ ")" )] |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
184 |
end; |
53 | 185 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
186 |
(*type declarations for constructors*) |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
187 |
fun const_types ((id, typlist, syn) :: cs) = |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
188 |
(id, |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
189 |
(if null typlist then "" else pp_typlist2 typlist ^ " => ") ^ |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
190 |
pp_typlist1 typevars ^ tname, syn) |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
191 |
:: const_types cs |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
192 |
| const_types [] = []; |
53 | 193 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
194 |
fun create_typevar (dtVar s) typlist = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
195 |
if (dtVar s) mem typlist then |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
196 |
create_typevar (dtVar (s ^ "'")) typlist |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
197 |
else s |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
198 |
| create_typevar _ _ = raise Impossible; |
53 | 199 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
200 |
fun assumpt (Rek _ :: ts, v :: vs ,found) = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
201 |
let val h = if found then ";P(" ^ v ^ ")" |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
202 |
else "[| P(" ^ v ^ ")" |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
203 |
in h ^ (assumpt (ts, vs, true)) end |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
204 |
| assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
205 |
| assumpt ([], [], found) = if found then "|] ==>" else "" |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
206 |
| assumpt _ = raise Impossible; |
53 | 207 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
208 |
(*insert type with suggested name 'varname' into table*) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
209 |
fun insert typ varname ((t, s, n) :: xs) = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
210 |
if typ = t then (t, s, n+1) :: xs |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
211 |
else if varname = s then (t,s,n) :: (insert typ (varname ^ "'") xs) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
212 |
else (t,s,n) :: (insert typ varname xs) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
213 |
| insert typ varname [] = [(typ, varname, 1)]; |
53 | 214 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
215 |
fun insert_types (Rek (l,id) :: ts) tab = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
216 |
insert_types ts (insert (Rek(l,id)) id tab) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
217 |
| insert_types ((dtVar s) :: ts) tab = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
218 |
insert_types ts (insert (dtVar s) (implode (tl (explode s))) tab) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
219 |
| insert_types ((dtId s) :: ts) tab = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
220 |
insert_types ts (insert (dtId s) s tab) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
221 |
| insert_types (Comp (l,id) :: ts) tab = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
222 |
insert_types ts (insert (Comp(l,id)) id tab) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
223 |
| insert_types [] tab = tab; |
53 | 224 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
225 |
fun update(Rek _, s, v :: vs, (Rek _) :: ts) = s :: vs |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
226 |
| update(t, s, v :: vs, t1 :: ts) = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
227 |
if t=t1 then s :: vs |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
228 |
else v :: (update (t, s, vs, ts)) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
229 |
| update _ = raise Impossible; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
230 |
|
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
231 |
fun update_n (Rek r1, s, v :: vs, (Rek r2) :: ts, n) = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
232 |
if r1 = r2 then (s ^ string_of_int n) :: |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
233 |
(update_n (Rek r1, s, vs, ts, n+1)) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
234 |
else v :: (update_n (Rek r1, s, vs, ts, n)) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
235 |
| update_n (t, s, v :: vs, t1 :: ts, n) = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
236 |
if t = t1 then (s ^ string_of_int n) :: |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
237 |
(update_n (t, s, vs, ts, n+1)) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
238 |
else v :: (update_n (t, s, vs, ts, n)) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
239 |
| update_n (_,_,[],[],_) = [] |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
240 |
| update_n _ = raise Impossible; |
53 | 241 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
242 |
(*insert type variables into table*) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
243 |
fun convert ((t, s, n) :: ts) var_list typ_list = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
244 |
let val h = if n=1 then update (t, s, var_list, typ_list) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
245 |
else update_n (t, s, var_list, typ_list, 1) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
246 |
in convert ts h typ_list end |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
247 |
| convert [] var_list _ = var_list; |
53 | 248 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
249 |
fun empty_list n = replicate n ""; |
53 | 250 |
|
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
251 |
fun t_inducting ((id, typl, syn) :: cs) = |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
252 |
let val name = const_name id syn; |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
253 |
val tab = insert_types typl []; |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
254 |
val arity = length typl; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
255 |
val var_list = convert tab (empty_list arity) typl; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
256 |
val h = if arity = 0 then " P(" ^ name ^ ")" |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
257 |
else " !!" ^ (space_implode " " var_list) ^ "." ^ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
258 |
(assumpt (typl, var_list, false)) ^ "P(" ^ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
259 |
name ^ "(" ^ (commas var_list) ^ "))"; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
260 |
val rest = t_inducting cs; |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
261 |
in if rest = "" then h else h ^ "; " ^ rest end |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
262 |
| t_inducting [] = ""; |
53 | 263 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
264 |
fun t_induct cl typ_name= |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
265 |
"[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")"; |
53 | 266 |
|
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
267 |
fun case_typlist typevar ((_, typlist, _) :: cs) = |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
268 |
let val h = if (length typlist) > 0 then |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
269 |
(pp_typlist2 typlist) ^ "=>" |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
270 |
else "" |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
271 |
in "," ^ h ^ typevar ^ (case_typlist typevar cs) end |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
272 |
| case_typlist _ [] = ""; |
53 | 273 |
|
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
274 |
fun case_rules t_case arity n ((id, typlist, syn) :: cs) = |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
275 |
let val name = const_name id syn; |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
276 |
val args = if null typlist then "" |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
277 |
else "(" ^ Args ("x", ",", 1, length typlist) ^ ")" |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
278 |
in (t_case ^ "_" ^ id, |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
279 |
t_case ^ "(" ^ name ^ args ^ "," ^ Args ("f", ",", 1, arity) |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
280 |
^ ") = f" ^ string_of_int(n) ^ args) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
281 |
:: (case_rules t_case arity (n+1) cs) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
282 |
end |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
283 |
| case_rules _ _ _ [] = []; |
53 | 284 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
285 |
val datatype_arity = length typevars; |
53 | 286 |
|
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
287 |
val types = [(tname, datatype_arity, NoSyn)]; |
53 | 288 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
289 |
val arities = |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
290 |
let val term_list = replicate datatype_arity ["term"]; |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
291 |
in [(tname, term_list, ["term"])] end; |
53 | 292 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
293 |
val datatype_name = pp_typlist1 typevars ^ tname; |
53 | 294 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
295 |
val (case_const, rules_case) = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
296 |
let val typevar = create_typevar (dtVar "'beta") typevars; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
297 |
val t_case = tname ^ "_case"; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
298 |
val arity = length cons_list; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
299 |
val dekl = (t_case, "[" ^ pp_typlist1 typevars ^ tname ^ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
300 |
case_typlist typevar cons_list ^ "]=>" ^ typevar, NoSyn) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
301 |
:: nil; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
302 |
val rules = case_rules t_case arity 1 cons_list; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
303 |
in (dekl, rules) end; |
53 | 304 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
305 |
val consts = |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
306 |
const_types cons_list |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
307 |
@ (if length cons_list < dtK then [] |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
308 |
else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)]) |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
309 |
@ case_const; |
53 | 310 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
311 |
(*generate 'var_n, ..., var_m'*) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
312 |
fun Args(var, delim, n, m) = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
313 |
space_implode delim (map (fn n => var^string_of_int(n)) (n upto m)); |
53 | 314 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
315 |
(*generate 'name_1', ..., 'name_n'*) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
316 |
fun C_exp(name, n, var) = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
317 |
if n > 0 then name ^ "(" ^ Args (var, ",", 1, n) ^ ")" |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
318 |
else name; |
53 | 319 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
320 |
(*generate 'x_n = y_n, ..., x_m = y_m'*) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
321 |
fun Arg_eql(n,m) = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
322 |
if n=m then "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
323 |
else "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) ^ " & " ^ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
324 |
Arg_eql(n+1, m); |
53 | 325 |
|
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
326 |
fun Ci_ing ((id, typlist, syn) :: cs) = |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
327 |
let val name = const_name id syn; |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
328 |
val arity = length typlist; |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
329 |
in if arity > 0 |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
330 |
then ("inject_" ^ id, |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
331 |
"(" ^ C_exp(name,arity,"x") ^ "=" ^ C_exp(name,arity,"y") |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
332 |
^ ") = (" ^ Arg_eql (1, arity) ^ ")") :: (Ci_ing cs) |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
333 |
else (Ci_ing cs) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
334 |
end |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
335 |
| Ci_ing [] = []; |
53 | 336 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
337 |
fun Ci_negOne _ [] = [] |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
338 |
| Ci_negOne c (c1::cs) = |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
339 |
let val (id1, tl1, syn1) = c |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
340 |
val (id2, tl2, syn2) = c1 |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
341 |
val name1 = const_name id1 syn1; |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
342 |
val name2 = const_name id2 syn2; |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
343 |
val arit1 = length tl1 |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
344 |
val arit2 = length tl2 |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
345 |
val h = "(" ^ C_exp(name1, arit1, "x") ^ "~=" ^ |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
346 |
C_exp(name2, arit2, "y") ^ ")" |
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
347 |
in ("ineq_" ^ id1 ^ "_" ^ id2, h):: (Ci_negOne c cs) |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
348 |
end; |
53 | 349 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
350 |
fun Ci_neg1 [] = [] |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
351 |
| Ci_neg1 (c1::cs) = Ci_negOne c1 cs @ Ci_neg1 cs; |
53 | 352 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
353 |
fun suc_expr n = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
354 |
if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")"; |
53 | 355 |
|
91
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
356 |
fun Ci_neg2equals (ord_t, ((id, typlist, syn) :: cs), n) = |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
357 |
let val name = const_name id syn; |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
358 |
val h = ord_t ^ "(" ^ (C_exp(name, length typlist, "x")) |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
359 |
^ ") = " ^ (suc_expr n) |
a94029edb01f
added mixfix annotations to constructor declarations
clasohm
parents:
87
diff
changeset
|
360 |
in (ord_t ^ (string_of_int (n+1)), h) |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
361 |
:: (Ci_neg2equals (ord_t, cs , n+1)) |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
362 |
end |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
363 |
| Ci_neg2equals (_, [], _) = []; |
53 | 364 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
365 |
val Ci_neg2 = |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
366 |
let val ord_t = tname ^ "_ord"; |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
367 |
in (Ci_neg2equals (ord_t, cons_list, 0)) @ |
87 | 368 |
[(ord_t ^ "0", |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
369 |
"(" ^ ord_t ^ "(x) ~= " ^ ord_t ^ "(y)) ==> (x ~= y)")] |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
370 |
end; |
53 | 371 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
372 |
val rules_ineq = if length cons_list < dtK then Ci_neg1 cons_list |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
373 |
else Ci_neg2; |
53 | 374 |
|
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
375 |
val rules_inject = Ci_ing cons_list; |
53 | 376 |
|
87 | 377 |
val rule_induct = (tname ^ "_induct", t_induct cons_list tname); |
60 | 378 |
|
87 | 379 |
val rules = rule_induct :: (rules_inject @ rules_ineq @ rules_case); |
80
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
380 |
in thy |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
381 |
|> add_types types |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
382 |
|> add_arities arities |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
383 |
|> add_consts consts |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
384 |
|> add_trrules xrules |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
385 |
|> add_axioms rules |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
386 |
end |
d3d727449d7b
datatypes must now be defined using a thy file section
clasohm
parents:
60
diff
changeset
|
387 |
end; |