--- a/Datatype.ML Fri Jul 08 12:01:55 1994 +0200
+++ b/Datatype.ML Fri Jul 08 17:22:58 1994 +0200
@@ -6,7 +6,8 @@
(*choice between Ci_neg1 and Ci_neg2 axioms depends on number of constructors*)
-val dtK = 5;
+local val dtK = 5
+in
local open ThyParse in
val datatype_decls =
@@ -25,7 +26,7 @@
val typ =
ident >> (cat "dtId" o quote)
||
- type_var_list -- ident >> (fn (ts, id) => "Comp (" ^ mk_list ts ^
+ type_var_list -- ident >> (fn (ts, id) => "dtComp (" ^ mk_list ts ^
", " ^ quote id ^ ")")
||
tvar;
@@ -90,12 +91,12 @@
(*used for constructor parameters*)
datatype dt_type = dtVar of string |
dtId of string |
- Comp of dt_type list * string |
- Rek of dt_type list * string;
+ dtComp of dt_type list * string |
+ dtRek of dt_type list * string;
-exception Impossible;
-
-local open Syntax.Mixfix in
+local open Syntax.Mixfix
+ exception Impossible
+in
fun add_datatype (typevars, tname, cons_list') thy =
let fun cat s1 s2 = s1 ^ " " ^ s2;
@@ -119,23 +120,23 @@
| analyse ((dtId s) :: typlist) =
if tname<>s then (dtId s) :: analyse typlist
else if null typevars then
- Rek ([], tname) :: analyse typlist
+ dtRek ([], tname) :: analyse typlist
else error (s ^ " used in different ways")
- | analyse (Comp (typl,s) :: typlist) =
- if tname <> s then Comp (analyse typl, s)
+ | analyse (dtComp (typl,s) :: typlist) =
+ if tname <> s then dtComp (analyse typl, s)
:: analyse typlist
else if typevars = typl then
- Rek (typl, s) :: analyse typlist
+ dtRek (typl, s) :: analyse typlist
else
error (s ^ " used in different ways")
| analyse [] = []
- | analyse ((Rek _) :: _) = raise Impossible;
+ | analyse ((dtRek _) :: _) = raise Impossible;
in (cons, analyse typlist, syn) end;
(*test if there are elements that are not recursive, i.e. if the type is
not empty*)
fun one_not_rek (cs : ('a * dt_type list * 'c) list) =
- let val contains_no_rek = forall (fn Rek _ => false | _ => true);
+ let val contains_no_rek = forall (fn dtRek _ => false | _ => true);
in exists (contains_no_rek o #2) cs orelse
error("Empty type not allowed!") end;
@@ -147,8 +148,8 @@
pp_typlist1: parentheses, pp_typlist2: brackets*)
fun pp_typ (dtVar s) = s
| pp_typ (dtId s) = s
- | pp_typ (Comp (typvars, id)) = (pp_typlist1 typvars) ^ id
- | pp_typ (Rek (typvars, id)) = (pp_typlist1 typvars) ^ id
+ | pp_typ (dtComp (typvars, id)) = (pp_typlist1 typvars) ^ id
+ | pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id
and
pp_typlist' ts = commas (map pp_typ ts)
and
@@ -197,7 +198,7 @@
else s
| create_typevar _ _ = raise Impossible;
- fun assumpt (Rek _ :: ts, v :: vs ,found) =
+ fun assumpt (dtRek _ :: ts, v :: vs ,found) =
let val h = if found then ";P(" ^ v ^ ")"
else "[| P(" ^ v ^ ")"
in h ^ (assumpt (ts, vs, true)) end
@@ -212,26 +213,26 @@
else (t,s,n) :: (insert typ varname xs)
| insert typ varname [] = [(typ, varname, 1)];
- fun insert_types (Rek (l,id) :: ts) tab =
- insert_types ts (insert (Rek(l,id)) id tab)
+ fun insert_types (dtRek (l,id) :: ts) tab =
+ insert_types ts (insert (dtRek(l,id)) id tab)
| insert_types ((dtVar s) :: ts) tab =
insert_types ts (insert (dtVar s) (implode (tl (explode s))) tab)
| insert_types ((dtId s) :: ts) tab =
insert_types ts (insert (dtId s) s tab)
- | insert_types (Comp (l,id) :: ts) tab =
- insert_types ts (insert (Comp(l,id)) id tab)
+ | insert_types (dtComp (l,id) :: ts) tab =
+ insert_types ts (insert (dtComp(l,id)) id tab)
| insert_types [] tab = tab;
- fun update(Rek _, s, v :: vs, (Rek _) :: ts) = s :: vs
+ fun update(dtRek _, s, v :: vs, (dtRek _) :: ts) = s :: vs
| update(t, s, v :: vs, t1 :: ts) =
if t=t1 then s :: vs
else v :: (update (t, s, vs, ts))
| update _ = raise Impossible;
- fun update_n (Rek r1, s, v :: vs, (Rek r2) :: ts, n) =
+ fun update_n (dtRek r1, s, v :: vs, (dtRek r2) :: ts, n) =
if r1 = r2 then (s ^ string_of_int n) ::
- (update_n (Rek r1, s, vs, ts, n+1))
- else v :: (update_n (Rek r1, s, vs, ts, n))
+ (update_n (dtRek r1, s, vs, ts, n+1))
+ else v :: (update_n (dtRek r1, s, vs, ts, n))
| update_n (t, s, v :: vs, t1 :: ts, n) =
if t = t1 then (s ^ string_of_int n) ::
(update_n (t, s, vs, ts, n+1))
@@ -384,4 +385,5 @@
|> add_trrules xrules
|> add_axioms rules
end
-end;
\ No newline at end of file
+end
+end;