--- a/datatype.ML Thu Feb 16 08:56:44 1995 +0100
+++ b/datatype.ML Sun Feb 19 15:04:39 1995 +0100
@@ -10,6 +10,8 @@
dtTyp of dt_type list * string |
dtRek of dt_type list * string;
+structure Datatype =
+struct
local
val mysort = sort;
@@ -107,7 +109,7 @@
handle RecError s =>
error("Primrec definition error: " ^ s ^ ":\n"
^ " " ^ Sign.string_of_term (sign_of thy) eq1);
- val tcs = map (fn (_,c,T,_) => (c,T)) cs';
+ val tcs = map (fn (_,c,T,_,_) => (c,T)) cs';
val cs = map fst tcs;
fun trans_recs' _ [] = []
| trans_recs' cis (eq::eqs) =
@@ -135,23 +137,40 @@
in
fun add_datatype (typevars, tname, cons_list') thy =
- let (*search for free type variables and convert recursive *)
- fun analyse_types (cons, typlist, syn) =
+ let
+ fun typid(dtRek(_,id)) = id
+ | typid(dtVar s) = implode (tl (explode s))
+ | typid(dtTyp(_,id)) = id;
+
+ fun index_vnames(vn::vns,tab) =
+ (case assoc(tab,vn) of
+ None => if vn mem vns
+ then (vn^"1") :: index_vnames(vns,(vn,2)::tab)
+ else vn :: index_vnames(vns,tab)
+ | Some(i) => (vn^(string_of_int i)) ::
+ index_vnames(vns,(vn,i+1)::tab))
+ | index_vnames([],tab) = [];
+
+ fun mk_var_names types = index_vnames(map typid types,[]);
+
+ (*search for free type variables and convert recursive *)
+ fun analyse_types (cons, types, syn) =
let fun analyse(t as dtVar v) =
- if t mem typevars then t
- else error ("Free type variable " ^ v ^ " on rhs.")
+ if t mem typevars then t
+ else error ("Free type variable " ^ v ^ " on rhs.")
| analyse(dtTyp(typl,s)) =
- if tname <> s then dtTyp(analyses typl, s)
- else if typevars = typl then dtRek(typl, s)
- else error (s ^ " used in different ways")
+ if tname <> s then dtTyp(analyses typl, s)
+ else if typevars = typl then dtRek(typl, s)
+ else error (s ^ " used in different ways")
| analyse(dtRek _) = raise Impossible
and analyses ts = map analyse ts;
- in (cons, Syntax.const_name cons syn, analyses typlist, syn)
- end;
+ in (cons, Syntax.const_name cons syn, analyses types,
+ mk_var_names types, syn)
+ end;
(*test if all elements are recursive, i.e. if the type is empty*)
- fun non_empty (cs : ('a * 'b * dt_type list * 'c) list) =
+ fun non_empty (cs : ('a * 'b * dt_type list * 'c *'d) list) =
not(forall (exists is_dtRek o #3) cs) orelse
error("Empty datatype not allowed!");
@@ -165,15 +184,12 @@
fun Args(var, delim, n, m) =
space_implode delim (map (fn n => var^string_of_int(n)) (n upto m));
- (*generate 'name_1', ..., 'name_n'*)
- fun C_exp(name, n, var) =
- if n > 0 then name ^ parens(Args(var, ",", 1, n)) else name;
+ fun C_exp name vns = name ^ opt_parens(commas vns);
- (*generate 'x_n = y_n, ..., x_m = y_m'*)
- fun Arg_eql(n,m) =
- if n=m then "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n)
- else "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) ^ " & " ^
- Arg_eql(n+1, m);
+ (*Arg_eqs([x1,...,xn],[y1,...,yn]) = "x1 = y1 & ... & xn = yn" *)
+ fun arg_eqs vns vns' =
+ let fun mkeq(x,x') = x ^ "=" ^ x'
+ in space_implode " & " (map mkeq (vns~~vns')) end
(*Pretty printers for type lists;
pp_typlist1: parentheses, pp_typlist2: brackets*)
@@ -189,8 +205,8 @@
fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts);
(* Generate syntax translation for case rules *)
- fun calc_xrules c_nr y_nr ((_, name, typlist, _) :: cs) =
- let val arity = length typlist;
+ fun calc_xrules c_nr y_nr ((_, name, _, vns, _) :: cs) =
+ let val arity = length vns;
val body = "z" ^ string_of_int(c_nr);
val args1 = if arity=0 then ""
else parens (Args ("y", ",", y_nr, y_nr+arity-1));
@@ -211,7 +227,7 @@
end;
(*type declarations for constructors*)
- fun const_type (id, _, typlist, syn) =
+ fun const_type (id, _, typlist, _, syn) =
(id,
(if null typlist then "" else pp_typlist2 typlist ^ " => ") ^
pp_typlist1 typevars ^ tname, syn);
@@ -224,53 +240,12 @@
| assumpt ([], [], found) = if found then "|] ==>" else ""
| assumpt _ = raise Impossible;
- (*insert type with suggested name 'varname' into table*)
- fun insert typ varname ((tri as (t, s, n)) :: xs) =
- if typ = t then (t, s, n+1) :: xs
- else tri :: (if varname = s then insert typ (varname ^ "'") xs
- else insert typ varname xs)
- | insert typ varname [] = [(typ, varname, 1)];
-
- fun typid(dtRek(_,id)) = id
- | typid(dtVar s) = implode (tl (explode s))
- | typid(dtTyp(_,id)) = id;
-
- val insert_types = foldl (fn (tab,typ) => insert typ (typid typ) tab);
-
- 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 (dtRek r1, s, v :: vs, (dtRek r2) :: ts, n) =
- if r1 = r2 then (s ^ string_of_int 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))
- else v :: (update_n (t, s, vs, ts, n))
- | update_n (_,_,[],[],_) = []
- | update_n _ = raise Impossible;
-
- (*insert type variables into table*)
- fun convert typs =
- let fun conv(vars, (t, s, n)) =
- if n=1 then update (t, s, vars, typs)
- else update_n (t, s, vars, typs, 1)
- in foldl conv
- end;
-
- fun empty_list n = replicate n "";
-
- fun t_inducting ((_, name, typl, _) :: cs) =
- let val tab = insert_types([],typl);
- val arity = length typl;
- val var_list = convert typl (empty_list arity,tab);
- val h = if arity = 0 then " P(" ^ name ^ ")"
- else " !!" ^ (space_implode " " var_list) ^ "." ^
- (assumpt (typl, var_list, false)) ^ "P(" ^
- name ^ "(" ^ (commas var_list) ^ "))";
+ fun t_inducting ((_, name, types, vns, _) :: cs) =
+ let
+ val h = if null types then " P(" ^ name ^ ")"
+ else " !!" ^ (space_implode " " vns) ^ "." ^
+ (assumpt (types, vns, false)) ^
+ "P(" ^ C_exp name vns ^ ")";
val rest = t_inducting cs;
in if rest = "" then h else h ^ "; " ^ rest end
| t_inducting [] = "";
@@ -278,7 +253,7 @@
fun t_induct cl typ_name =
"[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")";
- fun gen_typlist typevar f ((_, _, ts, _) :: cs) =
+ fun gen_typlist typevar f ((_, _, ts, _, _) :: cs) =
let val h = if (length ts) > 0
then pp_typlist2(f ts) ^ "=>"
else ""
@@ -291,12 +266,11 @@
val t_case = tname ^ "_case";
- fun case_rule n (id, name, ts, _) =
- let val args = opt_parens(Args("x", ",", 1, length ts))
+ fun case_rule n (id, name, _, vns, _) =
+ let val args = opt_parens(commas vns)
in (t_case ^ "_" ^ id,
t_case ^ "(" ^ Args("f", ",", 1, num_of_cons)
- ^ "," ^ name ^ args
- ^ ") = f" ^ string_of_int(n) ^ args)
+ ^ "," ^ name ^ args ^ ") = f"^string_of_int(n) ^ args)
end
fun case_rules n (c :: cs) = case_rule n c :: case_rules(n+1) cs
@@ -334,17 +308,14 @@
ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts);
(* positions of the dtRek types in a list of dt_types, starting from 1 *)
-
- fun rek_pos ts =
- map snd (filter (is_dtRek o fst) (ts ~~ (1 upto length ts)))
+ fun rek_vars ts vns = map snd (filter (is_dtRek o fst) (ts ~~ vns))
- fun rec_rule n (id,name,ts,_) =
- let val args = Args("x",",",1,length ts)
+ fun rec_rule n (id,name,ts,vns,_) =
+ let val args = commas vns
val fargs = Args("f",",",1,num_of_cons)
- fun rarg i = "," ^ t_rec ^ parens(fargs ^ "," ^ "x" ^
- string_of_int(i))
- val rargs = implode (map rarg (rek_pos ts))
- in
+ fun rarg vn = "," ^ t_rec ^ parens(fargs ^ "," ^ vn)
+ val rargs = implode (map rarg (rek_vars ts vns))
+ in
( t_rec ^ "_" ^ id
, t_rec ^ parens(fargs ^ "," ^ name ^ (opt_parens args)) ^ " = f"
^ string_of_int(n) ^ opt_parens (args ^ rargs))
@@ -369,20 +340,19 @@
@ [case_const,rec_const];
- fun Ci_ing ((id, name, typlist, _) :: cs) =
- let val arity = length typlist;
- in if arity = 0 then Ci_ing cs
- else ("inject_" ^ id,
- "(" ^ C_exp(name,arity,"x") ^ "=" ^ C_exp(name,arity,"y")
- ^ ") = (" ^ Arg_eql (1, arity) ^ ")") :: (Ci_ing cs)
- end
+ fun Ci_ing ((id, name, _, vns, _) :: cs) =
+ if null vns then Ci_ing cs
+ else let val vns' = variantlist(vns,vns)
+ in ("inject_" ^ id,
+ "(" ^ (C_exp name vns) ^ "=" ^ (C_exp name vns')
+ ^ ") = (" ^ (arg_eqs vns vns') ^ ")") :: (Ci_ing cs)
+ end
| Ci_ing [] = [];
- fun Ci_negOne (id1, name1, tl1, _) (id2, name2, tl2, _) =
- let val ax = C_exp(name1, length tl1, "x") ^ "~=" ^
- C_exp(name2, length tl2, "y")
- in (id1 ^ "_not_" ^ id2, ax)
- end;
+ fun Ci_negOne (id1,name1,_,vns1,_) (id2,name2,_,vns2,_) =
+ let val vns2' = variantlist(vns2,vns1)
+ val ax = C_exp name1 vns1 ^ "~=" ^ C_exp name2 vns2'
+ in (id1 ^ "_not_" ^ id2, ax) end;
fun Ci_neg1 [] = []
| Ci_neg1 (c1::cs) = (map (Ci_negOne c1) cs) @ Ci_neg1 cs;
@@ -393,9 +363,8 @@
fun Ci_neg2() =
let val ord_t = tname ^ "_ord";
val cis = cons_list ~~ (0 upto (num_of_cons - 1))
- fun Ci_neg2equals ((id, name, typlist, _), n) =
- let val ax = ord_t ^ "(" ^ (C_exp(name, length typlist, "x"))
- ^ ") = " ^ (suc_expr n)
+ fun Ci_neg2equals ((id, name, _, vns, _), n) =
+ let val ax = ord_t ^ "(" ^ (C_exp name vns) ^ ") = " ^ (suc_expr n)
in (ord_t ^ "_" ^ id, ax) end
in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") ::
(map Ci_neg2equals cis)
@@ -441,6 +410,7 @@
|> add_axioms rules,add_primrec)
end
end
+end
(*
Informal description of functions used in datatype.ML for the Isabelle/HOL