# HG changeset patch # User nipkow # Date 776956834 -7200 # Node ID c57ab3ce997e0a88f70077eb1fd0cc643085c186 # Parent 18d44ab74672eb0492ee516f93e3ddb7c9aa4f03 Cleaned up code. diff -r 18d44ab74672 -r c57ab3ce997e Datatype.ML --- a/Datatype.ML Sat Aug 13 16:34:30 1994 +0200 +++ b/Datatype.ML Mon Aug 15 15:20:34 1994 +0200 @@ -1,7 +1,7 @@ (* Title: HOL/Datatype ID: $Id$ - Author: Max Breitling / Carsten Clasohm / - Norbert Voelker / Tobias Nipkow + Author: Max Breitling, Carsten Clasohm, + Tobias Nipkow, Norbert Voelker Copyright 1994 TU Muenchen *) @@ -10,9 +10,6 @@ local val dtK = 5 -val pars = enclose "(" ")"; -val brackets = enclose "[" "]"; -val mk_list = brackets o commas; in @@ -40,9 +37,11 @@ || cons >> (fn c => [c])) ts; - val mk_cons = map (fn ((s, ts), syn) => - pars (commas [s, mk_list ts, syn])); - + fun mk_cons cs = + case findrep (map (fst o fst) cs) of + [] => map (fn ((s,ts),syn) => parens (commas [s,mk_list ts,syn])) cs + | c::_ => error("Constructor \"" ^ c ^ "\" occurs twice"); + (*remove all quotes from a string*) val rem_quotes = implode o filter (fn c => c <> "\"") o explode; @@ -57,17 +56,15 @@ else quote (tname ^ "_ord_distinct") :: map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs end; - - fun rule_names tname cons pre = + + fun rules tname cons pre = + " map (get_axiom thy) " ^ mk_list (map (fn ((s,_),_) => quote(tname ^ pre ^ rem_quotes s)) cons) - fun rules tname cons pre = - " map (get_axiom thy) " ^ rule_names tname cons pre - (*generate string for calling 'add_datatype'*) fun mk_params ((ts, tname), cons) = ("val (thy," ^ tname ^ "_add_primrec) = add_datatype\n" ^ - pars (commas [mk_list ts, quote tname, mk_list (mk_cons cons)]) ^ + parens (commas [mk_list ts, quote tname, mk_list (mk_cons cons)]) ^ " thy\n\ \val thy=thy", "structure " ^ tname ^ " =\n\ @@ -107,9 +104,10 @@ dtRek of dt_type list * string; local open Syntax.Mixfix + ThyParse exception Impossible -val is_rek = (fn dtRek _ => true | _ => false); +val is_Rek = (fn dtRek _ => true | _ => false); (* ------------------------------------------------------------------------- *) (* Die Funktionen fuer das Umsetzen von Gleichungen in eine Definition mit *) @@ -121,7 +119,7 @@ fun rek_args (args, targs) = let fun h (x :: xs, tx :: txs, res) - = h(xs,txs,if is_rek tx then x :: res else res ) + = h(xs,txs,if is_Rek tx then x :: res else res ) | h ([],[],res) = res in h (args,targs,[]) end; @@ -197,9 +195,9 @@ | h reqs (eq::eqs) (c::cs) res = let val (f,(Const(cname_eq,_),args),rhs) = dest_eq eq; - val (cname,targs,syn) = c; + val (_,cname,targs,_) = c; in - if (cname_eq <> const_name cname syn) then h reqs eqs (c::cs) res + if cname_eq <> cname then h reqs eqs (c::cs) res else if fst(dest_Const(f)) = fname andalso (duplicates (map (fst o dest_Free) args) = []) @@ -224,35 +222,27 @@ in fun add_datatype (typevars, tname, cons_list') thy = - let (*check if constructor names are unique*) - fun check_cons (cs : (string * 'b * 'c) list) = - (case findrep (map #1 cs) of - [] => true - | c::_ => error("Constructor \"" ^ c ^ "\" occurs twice")); - - (*search for free type variables and convert recursive *) + let (*search for free type variables and convert recursive *) fun analyse_types (cons, typlist, syn) = let fun analyse(t as dtVar v) = if t mem typevars then t - else error ("Variable " ^ v ^ " is free.") + 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") | analyse(dtRek _) = raise Impossible and analyses ts = map analyse ts; - in (cons, analyses typlist, syn) end; + in (cons, const_name cons syn, analyses 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 dtRek _ => false | _ => true); - in exists (contains_no_rek o #2) cs orelse - error("Empty type not allowed!") 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) = + not(forall (exists is_Rek o #3) cs) orelse + error("Empty datatype not allowed!"); - val dummy = check_cons cons_list'; val cons_list = map analyse_types cons_list'; - val dummy = one_not_rek cons_list; + val dummy = non_empty cons_list; + val num_of_cons = length cons_list; (*Pretty printers for type lists; pp_typlist1: parentheses, pp_typlist2: brackets*) @@ -263,7 +253,7 @@ and pp_typlist' ts = commas (map pp_typ ts) and - pp_typlist1 ts = if null ts then "" else pars (pp_typlist' ts); + 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); @@ -272,12 +262,11 @@ Args(var, delim, n+1, m); (* Generate syntax translation for case rules *) - fun calc_xrules c_nr y_nr ((id, typlist, syn) :: cs) = - let val name = const_name id syn; - val arity = length typlist; + fun calc_xrules c_nr y_nr ((_, name, typlist, _) :: cs) = + let val arity = length typlist; val body = "z" ^ string_of_int(c_nr); val args1 = if arity=0 then "" - else pars (Args ("y", ",", y_nr, y_nr+arity-1)); + 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) ^ ". "; @@ -295,16 +284,11 @@ 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); - fun create_typevar (dtVar s) typlist = - if (dtVar s) mem typlist then - create_typevar (dtVar (s ^ "'")) typlist - else s - | create_typevar _ _ = raise Impossible; fun assumpt (dtRek _ :: ts, v :: vs ,found) = let val h = if found then ";P(" ^ v ^ ")" else "[| P(" ^ v ^ ")" @@ -352,9 +336,8 @@ fun empty_list n = replicate n ""; - fun t_inducting ((id, typl, syn) :: cs) = - let val name = const_name id syn; - val tab = insert_types([],typl); + 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 ^ ")" @@ -365,28 +348,28 @@ in if rest = "" then h else h ^ "; " ^ rest end | t_inducting [] = ""; - fun t_induct cl typ_name= + fun t_induct cl typ_name = "[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")"; - fun case_typlist typevar ((_, typlist, _) :: cs) = - let val h = if (length typlist) > 0 then - (pp_typlist2 typlist) ^ "=>" + fun gen_typlist typevar f ((_, _, ts, _) :: cs) = + let val h = if (length ts) > 0 + then pp_typlist2(f ts) ^ "=>" else "" - in "," ^ h ^ typevar ^ (case_typlist typevar cs) end - | case_typlist _ [] = ""; + in "," ^ h ^ typevar ^ (gen_typlist typevar f cs) end + | gen_typlist _ _ [] = ""; val t_case = tname ^ "_case"; - fun case_rules arity n ((id, typlist, syn) :: cs) = - let val name = const_name id syn; - val args = if null typlist then "" - else pars(Args("x", ",", 1, length typlist)) + fun case_rules n ((id, name, typlist, _) :: cs) = + let val args = if null typlist then "" + else parens(Args("x", ",", 1, length typlist)) in (t_case ^ "_" ^ id, - t_case ^ "(" ^ name ^ args ^ "," ^ Args ("f", ",", 1, arity) - ^ ") = f" ^ string_of_int(n) ^ args) - :: (case_rules arity (n+1) cs) + t_case ^ "(" ^ name ^ args ^ "," ^ + Args("f", ",", 1, num_of_cons) + ^ ") = f" ^ string_of_int(n) ^ args) + :: (case_rules (n+1) cs) end - | case_rules _ _ [] = []; + | case_rules _ [] = []; val datatype_arity = length typevars; @@ -398,14 +381,15 @@ val datatype_name = pp_typlist1 typevars ^ tname; - val (case_const, rules_case) = - let val typevar = create_typevar (dtVar "'beta") typevars; - val arity = length cons_list; - val dekl = (t_case, "[" ^ pp_typlist1 typevars ^ tname ^ - case_typlist typevar cons_list ^ "]=>" ^ typevar, NoSyn) - val rules = case_rules arity 1 cons_list; - in (dekl, rules) end; + val new_tvar_name = variant (map (fn dtVar s => s) typevars) "'z"; + val case_const = + (t_case, + "[" ^ pp_typlist1 typevars ^ tname ^ + gen_typlist new_tvar_name I cons_list ^ "] =>" ^ new_tvar_name, + NoSyn); + + val rules_case = case_rules 1 cons_list; (* -------------------------------------------------------------------- *) @@ -414,62 +398,47 @@ val t_rec = tname ^ "_rec" -fun add_reks typevar ts = - let val tv = dtVar typevar; - fun h (t::ts) res = h ts (if is_rek(t) then tv::res else res) - | h [] res = res - in h ts ts - end; + fun add_reks ts = + let val tv = dtVar new_tvar_name; + fun h (t::ts) res = h ts (if is_Rek(t) then tv::res else res) + | h [] res = res + in h ts ts end; -fun rec_typlist typevar ((c,ts,_)::cs) = - let val h = if (length ts) > 0 - then (pp_typlist2 (add_reks typevar ts)) ^ "=>" - else "" - in "," ^ h ^ typevar ^ (rec_typlist typevar cs) - end - | rec_typlist _ [] = ""; - -fun arg_reks arity ts = +fun arg_reks ts = let fun arg_rek (t::ts) n res = let val h = t_rec ^"(" ^ "x" ^string_of_int(n) - ^"," ^Args("f",",",1,arity) ^")," - in arg_rek ts (n+1) (if is_rek(t) then res ^ h else res) + ^"," ^Args("f",",",1,num_of_cons) ^")," + in arg_rek ts (n+1) (if is_Rek(t) then res ^ h else res) end | arg_rek [] _ res = res - in arg_rek ts 1 "" - end; + in arg_rek ts 1 "" end; -fun rec_rules arity n ((id,ts,syn)::cs) = - let val name = const_name id syn; - val lts = length ts - val args = if (lts = 0) then "" - else "(" ^ Args("x",",",1,lts) ^ ")" +fun rec_rules n ((id,name,ts,_)::cs) = + let val lts = length ts + val args = if lts = 0 then "" + else parens(Args("x",",",1,lts)) val rargs = if (lts = 0) then "" - else "("^ arg_reks arity ts ^ Args("x",",",1,lts) ^")" + else "("^ arg_reks ts ^ Args("x",",",1,lts) ^")" in ( t_rec ^ "_" ^ id - , t_rec ^ "(" ^ name ^ args ^ "," ^ Args("f",",",1,arity) ^ ") = f" + , t_rec ^ "(" ^ name ^ args ^ "," ^ Args("f",",",1,num_of_cons) ^ ") = f" ^ string_of_int(n) ^ rargs) - :: (rec_rules arity (n+1) cs) + :: (rec_rules (n+1) cs) end - | rec_rules _ _ [] = []; + | rec_rules _ [] = []; -val (rec_const,rules_rec) = - let val typevar = create_typevar (dtVar "'beta") typevars - val arity = length cons_list - val dekl = (t_rec, - "[" ^ (pp_typlist1 typevars) ^ tname ^ - (rec_typlist typevar cons_list) ^ "]=>" ^ typevar, - NoSyn) - val rules = rec_rules arity 1 cons_list - in (dekl,rules) - end; + val rec_const = + (t_rec, + "[" ^ (pp_typlist1 typevars) ^ tname ^ + (gen_typlist new_tvar_name add_reks cons_list) ^ + "] =>" ^ new_tvar_name, + NoSyn); - + val rules_rec = rec_rules 1 cons_list val consts = map const_type cons_list - @ (if length cons_list < dtK then [] + @ (if num_of_cons < dtK then [] else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)]) @ [case_const,rec_const]; @@ -479,7 +448,7 @@ (*generate 'name_1', ..., 'name_n'*) fun C_exp(name, n, var) = - if n > 0 then name ^ pars(Args(var, ",", 1, n)) else name; + 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) = @@ -487,9 +456,8 @@ else "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) ^ " & " ^ Arg_eql(n+1, m); - fun Ci_ing ((id, typlist, syn) :: cs) = - let val name = const_name id syn; - val arity = length typlist; + 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") @@ -497,10 +465,8 @@ end | Ci_ing [] = []; - fun Ci_negOne (id1, tl1, syn1) (id2, tl2, syn2) = - let val name1 = const_name id1 syn1; - val name2 = const_name id2 syn2; - val ax = C_exp(name1, length tl1, "x") ^ "~=" ^ + 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; @@ -512,17 +478,16 @@ fun Ci_neg2() = let val ord_t = tname ^ "_ord"; - val cis = cons_list ~~ (0 upto (length cons_list - 1)) - fun Ci_neg2equals ((id, typlist, syn), n) = - let val name = const_name id syn; - val ax = ord_t ^ "(" ^ (C_exp(name, length typlist, "x")) + 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) in (ord_t ^ "_" ^ id, ax) end in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") :: (map Ci_neg2equals cis) end; - val rules_distinct = if length cons_list < dtK then Ci_neg1 cons_list + val rules_distinct = if num_of_cons < dtK then Ci_neg1 cons_list else Ci_neg2(); val rules_inject = Ci_ing cons_list;