# HG changeset patch # User nipkow # Date 793202679 -3600 # Node ID 5f9d7ed4ea0c0ac45ad9962dac0c436d4178abf2 # Parent 8c1afdbea4734d93b237309c7b6f760d82fec0cc Reorganized/optimized datatype definitions. diff -r 8c1afdbea473 -r 5f9d7ed4ea0c datatype.ML --- 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 diff -r 8c1afdbea473 -r 5f9d7ed4ea0c thy_syntax.ML --- a/thy_syntax.ML Thu Feb 16 08:56:44 1995 +0100 +++ b/thy_syntax.ML Sun Feb 19 15:04:39 1995 +0100 @@ -114,7 +114,7 @@ (*generate string for calling add_datatype*) fun mk_params ((ts, tname), cons) = - ("val (thy, " ^ tname ^ "_add_primrec) = add_datatype\n" + ("val (thy, " ^ tname ^ "_add_primrec) = Datatype.add_datatype\n" ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\ \val thy = thy", "structure " ^ tname ^ " =\n\