--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/datatype.ML Tue Aug 30 10:04:49 1994 +0200
@@ -0,0 +1,556 @@
+(* Title: HOL/Datatype
+ ID: $Id$
+ Author: Max Breitling, Carsten Clasohm,
+ Tobias Nipkow, Norbert Voelker
+ Copyright 1994 TU Muenchen
+*)
+
+
+(*choice between Ci_neg1 and Ci_neg2 axioms depends on number of constructors*)
+local
+
+ val dtK = 5
+
+in
+
+local open ThyParse in
+ val datatype_decls =
+ let
+ val tvar = type_var >> (fn s => "dtVar" ^ s);
+
+ val type_var_list =
+ tvar >> (fn s => [s]) || "(" $$-- list1 tvar --$$ ")";
+
+ val typ =
+ ident >> (fn s => "dtTyp([]," ^ quote s ^")")
+ ||
+ type_var_list -- ident >> (fn (ts, id) => "dtTyp(" ^ mk_list ts ^
+ "," ^ quote id ^ ")")
+ ||
+ tvar;
+
+ val typ_list = "(" $$-- list1 typ --$$ ")" || empty;
+
+ val cons = name -- typ_list -- opt_mixfix;
+
+ fun constructs ts =
+ ( cons --$$ "|" -- constructs >> op::
+ ||
+ cons >> (fn c => [c])) ts;
+
+ 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;
+
+ (*generate names of distinct axioms*)
+ fun rules_distinct cs tname =
+ let val uqcs = map (fn ((s,_),_) => rem_quotes s) cs;
+ (*combine all constructor names with all others w/o duplicates*)
+ fun negOne c = map (fn c2 => quote (c ^ "_not_" ^ c2));
+ fun neg1 [] = []
+ | neg1 (c1 :: cs) = (negOne c1 cs) @ (neg1 cs)
+ in if length uqcs < dtK then neg1 uqcs
+ else quote (tname ^ "_ord_distinct") ::
+ map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
+ end;
+
+ fun rules tname cons pre =
+ " map (get_axiom thy) " ^
+ mk_list (map (fn ((s,_),_) => quote(tname ^ pre ^ rem_quotes s))
+ cons)
+
+ (*generate string for calling 'add_datatype'*)
+ fun mk_params ((ts, tname), cons) =
+ ("val (thy," ^ tname ^ "_add_primrec) = add_datatype\n" ^
+ parens (commas [mk_list ts, quote tname, mk_list (mk_cons cons)]) ^
+ " thy\n\
+ \val thy=thy",
+ "structure " ^ tname ^ " =\n\
+ \struct\n\
+ \ val inject = map (get_axiom thy) " ^
+ mk_list (map (fn ((s,_), _) => quote ("inject_" ^ rem_quotes s))
+ (filter_out (null o snd o fst) cons)) ^ ";\n\
+ \ val distinct = " ^
+ (if length cons < dtK then "let val distinct' = " else "") ^
+ "map (get_axiom thy) " ^ mk_list (rules_distinct cons tname) ^
+ (if length cons < dtK then
+ " in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
+ \ distinct') end"
+ else "") ^ ";\n\
+ \ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
+ \ val cases =" ^ rules tname cons "_case_" ^ ";\n\
+ \ val recs =" ^ rules tname cons "_rec_" ^ ";\n\
+ \ val simps = inject @ distinct @ cases @ recs;\n\
+ \ fun induct_tac a =\
+ \res_inst_tac[(" ^ quote tname ^ ", a)]induct;\n\
+ \end;\n")
+ in
+ (type_var_list || empty) -- ident --$$ "=" -- constructs >> mk_params
+end
+
+val primrec_decl =
+ let fun mkstrings((fname,tname),axms) =
+ let fun prove (name,eqn) =
+ "val "^name^"= prove_goalw thy [get_def thy \""^fname^"\"] "
+ ^ eqn ^"\n\
+ \(fn _ => [simp_tac (HOL_ss addsimps " ^ tname^".recs) 1])"
+ in ("|> " ^ tname^"_add_primrec " ^ mk_list (map snd axms)
+ , cat_lines(map prove axms))
+ end
+ in ident -- long_id -- repeat1 (ident -- string) >> mkstrings end
+end;
+
+(*used for constructor parameters*)
+datatype dt_type = dtVar of string |
+ dtTyp of dt_type list * string |
+ dtRek of dt_type list * string;
+
+local
+
+val mysort = sort;
+open ThyParse
+exception Impossible;
+exception RecError of string;
+
+val is_dtRek = (fn dtRek _ => true | _ => false);
+fun opt_parens s = if s = "" then "" else enclose "(" ")" s;
+
+(* ----------------------------------------------------------------------- *)
+(* Derivation of the primrec combinator application from the equations *)
+
+(* subst. applications fname(ls,xk,rs) by yk(ls,rs) for xk in rargs *)
+
+fun subst_apps (_,_) [] t = t
+ | subst_apps (fname,cpos) pairs t =
+ let
+ fun subst (Abs(a,T,t)) = Abs(a,T,subst t)
+ | subst (funct $ body) =
+ let val (f,b) = strip_comb (funct$body)
+ in
+ if is_Const f andalso fst(dest_Const f) = fname
+ then
+ let val (ls,rest) = (take(cpos,b), drop (cpos,b));
+ val (xk,rs) = (hd rest,tl rest)
+ handle LIST _ => raise RecError "not enough arguments \
+ \ in recursive application on rhs"
+ in
+ (case assoc (pairs,xk) of
+ None => raise RecError
+ ("illegal occurence of " ^ fname ^ " on rhs")
+ | Some(U) => list_comb(U,ls @ rs))
+ end
+ else list_comb(f, map subst b)
+ end
+ | subst(t) = t
+ in subst t end;
+
+(* abstract rhs *)
+
+fun abst_rec (fname,cpos,tc,ls,cargs,rs,rhs) =
+ let val rargs = (map fst o
+ (filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc);
+ val subs = map (fn (s,T) => (s,dummyT))
+ (rev(rename_wrt_term rhs rargs));
+ val subst_rhs = subst_apps (fname,cpos)
+ (map Free rargs ~~ map Free subs) rhs;
+ val res = list_abs_free (cargs @ subs @ ls @ rs, subst_rhs);
+ in
+ if fname mem add_term_names (res,[])
+ then raise RecError ("illegal occurence of " ^ fname ^ " on rhs")
+ else res
+ end;
+
+(* parsing the prim rec equations *)
+
+fun dest_eq ( Const("Trueprop",_) $ (Const ("op =",_) $ lhs $ rhs))
+ = (lhs, rhs)
+ | dest_eq _ = raise RecError "not a proper equation";
+
+fun dest_rec eq =
+ let val (lhs,rhs) = dest_eq eq;
+ val (name,args) = strip_comb lhs;
+ val (ls',rest) = take_prefix is_Free args;
+ val (middle,rs') = take_suffix is_Free rest;
+ val cpos = length ls';
+ val (c,cargs') = strip_comb (hd middle)
+ handle LIST "hd" => raise RecError "constructor missing";
+ val (ls,cargs,rs) = (map dest_Free ls', map dest_Free cargs'
+ , map dest_Free rs')
+ handle TERM ("dest_Free",_) =>
+ raise RecError "constructor has illegal argument in pattern";
+ in
+ if length middle > 1 then
+ raise RecError "more than one non-variable in pattern"
+ else if not(null(findrep (map fst (ls @ rs @ cargs)))) then
+ raise RecError "repeated variable name in pattern"
+ else (fst(dest_Const name) handle TERM _ =>
+ raise RecError "function is not declared as constant in theory"
+ ,cpos,ls,fst( dest_Const c),cargs,rs,rhs)
+ end;
+
+(* check function specified for all constructors and sort function terms *)
+
+fun check_and_sort (n,its) =
+ if length its = n
+ then map snd (mysort (fn ((i : int,_),(j,_)) => i<j) its)
+ else raise error "Primrec definition error:\n\
+ \Please give an equation for every constructor";
+
+(* translate rec equations into function arguments suitable for rec comb *)
+(* theory parameter needed for printing error messages *)
+
+fun trans_recs _ _ [] = error("No primrec equations.")
+ | trans_recs thy cs' (eq1::eqs) =
+ let val (name1,cpos1,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 cs = map fst tcs;
+ fun trans_recs' _ [] = []
+ | trans_recs' cis (eq::eqs) =
+ let val (name,cpos,ls,c,cargs,rs,rhs) = dest_rec eq;
+ val tc = assoc(tcs,c);
+ val i = (1 + find (c,cs)) handle LIST "find" => 0;
+ in
+ if name <> name1 then
+ raise RecError "function names inconsistent"
+ else if cpos <> cpos1 then
+ raise RecError "position of rec. argument inconsistent"
+ else if i = 0 then
+ raise RecError "illegal argument in pattern"
+ else if i mem cis then
+ raise RecError "constructor already occured as pattern "
+ else (i,abst_rec (name,cpos,the tc,ls,cargs,rs,rhs))
+ :: trans_recs' (i::cis) eqs
+ end
+ handle RecError s =>
+ error("Primrec definition error\n" ^ s ^ "\n"
+ ^ " " ^ Sign.string_of_term (sign_of thy) eq);
+ in ( name1, ls1
+ , check_and_sort (length cs, trans_recs' [] (eq1::eqs)))
+ end ;
+
+
+fun instantiate_types thy t =
+ let val sg = sign_of thy
+ val rsg = Sign.rep_sg sg
+ in fst(Type.infer_types(#tsig rsg, lookup_const sg, K None, K None,
+ TVar(("",0),[]), t))
+ 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 analyse(t as dtVar v) =
+ 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")
+ | analyse(dtRek _) = raise Impossible
+ and analyses ts = map analyse ts;
+ in (cons, Syntax.const_name cons syn, analyses typlist, 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) =
+ 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;
+ val num_of_cons = length cons_list;
+
+ (* Auxiliary functions to construct argument and equation lists *)
+
+ (*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);
+
+ (*Pretty printers for type lists;
+ pp_typlist1: parentheses, pp_typlist2: brackets*)
+ fun pp_typ (dtVar s) = s
+ | pp_typ (dtTyp (typvars, id)) =
+ if null typvars then id else (pp_typlist1 typvars) ^ id
+ | pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id
+ and
+ pp_typlist' ts = commas (map pp_typ ts)
+ and
+ 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;
+ 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)
+ ^ ". ";
+ val (rest1,rest2) =
+ if null cs then ("","")
+ else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs
+ in (" | " ^ h1, ", " ^ h2) end;
+ in (name ^ args1 ^ " => " ^ body ^ rest1, args2 ^ body ^ rest2) end
+ | calc_xrules _ _ [] = raise Impossible;
+
+ val xrules =
+ let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
+ in [("logic", "case x of " ^ first_part) <->
+ ("logic", tname ^ "_case(" ^ scnd_part ^ ", x)" )]
+ end;
+
+ (*type declarations for constructors*)
+ fun const_type (id, _, typlist, syn) =
+ (id,
+ (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^
+ pp_typlist1 typevars ^ tname, syn);
+
+
+ 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
+ | 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) ^ "))";
+ 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) =
+ 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))
+ in (t_case ^ "_" ^ id,
+ t_case ^ "(" ^ Args("f", ",", 1, num_of_cons)
+ ^ "," ^ 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 _ [] = [];
+
+ val datatype_arity = length typevars;
+
+ val types = [(tname, datatype_arity, NoSyn)];
+
+ val arities =
+ let val term_list = replicate datatype_arity ["term"];
+ in [(tname, term_list, ["term"])]
+ end;
+
+ val datatype_name = pp_typlist1 typevars ^ tname;
+
+ val new_tvar_name = variant (map (fn dtVar s => s) typevars) "'z";
+
+ val case_const =
+ (t_case,
+ "[" ^ gen_typlist new_tvar_name I cons_list
+ ^ pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name,
+ NoSyn);
+
+ val rules_case = case_rules 1 cons_list;
+
+(* -------------------------------------------------------------------- *)
+(* The prim-rec combinator *)
+
+ val t_rec = tname ^ "_rec"
+
+(* adding type variables for dtRek types to end of list of dt_types *)
+
+ 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)
+ 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
+ ( t_rec ^ "_" ^ id
+ , t_rec ^ parens(fargs ^ "," ^ name ^ (opt_parens args)) ^ " = f"
+ ^ string_of_int(n) ^ opt_parens (args ^ rargs))
+ end
+
+ fun rec_rules n (c::cs) = rec_rule n c :: rec_rules (n+1) cs
+ | rec_rules _ [] = [];
+
+ val rec_const =
+ (t_rec,
+ "[" ^ (gen_typlist new_tvar_name add_reks cons_list)
+ ^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name,
+ NoSyn);
+
+ val rules_rec = rec_rules 1 cons_list
+
+(* -------------------------------------------------------------------- *)
+ val consts =
+ map const_type cons_list
+ @ (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
+ | 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_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)
+ 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 num_of_cons < dtK then Ci_neg1 cons_list
+ else Ci_neg2();
+
+ val rules_inject = Ci_ing cons_list;
+
+ val rule_induct = (tname ^ "_induct", t_induct cons_list tname);
+
+ val rules = rule_induct ::
+ (rules_inject @ rules_distinct @ rules_case @ rules_rec);
+
+ fun add_primrec eqns thy =
+ let val rec_comb = Const(t_rec,dummyT)
+ val teqns = map (fn eq => snd(read_axm (sign_of thy)
+ ("",eq))) eqns
+ val (fname,ls,fns) = trans_recs thy cons_list teqns
+ val rhs =
+ list_abs_free
+ (ls @ [(tname,dummyT)]
+ ,list_comb(rec_comb
+ , fns @ map Bound (0 ::(length ls downto 1))));
+ val sg = sign_of thy;
+ val (defname,def) = mk_defpair (Const(fname,dummyT),rhs)
+ val tdef as ( _ $ Const(_,T) $ _ ) = instantiate_types thy def;
+ val varT = Type.varifyT T;
+ val Some(ftyp) = lookup_const sg fname;
+ in
+ if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT)
+ then add_defs_i [(defname,tdef)] thy
+ else error("Primrec definition error: \ntype of " ^ fname
+ ^ " is not instance of type deduced from equations")
+ end;
+
+ in
+ (thy
+ |> add_types types
+ |> add_arities arities
+ |> add_consts consts
+ |> add_trrules xrules
+ |> add_axioms rules,add_primrec)
+ end
+end
+end;
+