datatype.ML

 (*used for constructor parameters*)
 datatype dt_type = dtVar of string |
   dtTyp of dt_type list * string |
   dtRek of dt_type list * string;
 
+structure Datatype =
+struct
 local 
 
 val mysort = sort;
 open ThyParse HOLogic;
 exception Impossible;

   | trans_recs thy cs' (eq1::eqs) = 
     let val (name1,rpos1,ls1,_,_,_,_) = dest_rec eq1
       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) = 
 	  let val (name,rpos,ls,c,cargs,rs,rhs) = dest_rec eq; 
 	    val tc = assoc(tcs,c);

 	, check_and_sort (length cs, trans_recs' [] (eq1::eqs)))
     end ;
 
 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!");
 
       val cons_list = map analyse_types cons_list';
       val dummy = non_empty cons_list;

 
      (*generate 'var_n, ..., var_m'*)
       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;
-
-     (*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);
+      fun C_exp name vns = name ^ opt_parens(commas vns);
+
+     (*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*)
       fun pp_typ (dtVar s) = s
         | pp_typ (dtTyp (typvars, id)) =

 	pp_typlist1 ts = if null ts then "" else parens (pp_typlist' ts);
 
       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));
 	  val args2 = if arity=0 then ""
 		      else "% " ^ Args ("y", " ", y_nr, y_nr+arity-1) 

 	in  [("logic", "case x of " ^ first_part) <->
 	     ("logic", tname ^ "_case(" ^ scnd_part ^ ", x)" )]
 	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);
 
 

 	in h ^ (assumpt (ts, vs, true)) end
         | assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found)
       | 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 [] = "";
 
       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 ""
 	in h ^ typevar ^  "," ^ (gen_typlist typevar f cs) end
         | gen_typlist _ _ [] = "";

 (* -------------------------------------------------------------------- *)
 (* The case constant and rules 	        				*)
  		
       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
         | case_rules _ [] = [];
 

 
       fun add_reks ts = 
 	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 rec_rule n (id,name,ts,_) = 
-	let val args = Args("x",",",1,length ts)
+      fun rek_vars ts vns = map snd (filter (is_dtRek o fst) (ts ~~ vns))
+
+      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)) 
 	end
 

 	@ (if num_of_cons < dtK then []
 	   else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)])
 	@ [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;
 
       fun suc_expr n = 
 	if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")";
 
       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)
 	end;
 

       |> add_consts consts
       |> add_trrules xrules
       |> add_axioms rules,add_primrec)
     end
 end
+end
 
 (*
 Informal description of functions used in datatype.ML for the Isabelle/HOL
 implementation of prim. rec. function definitions. (N. Voelker, Feb. 1995)