diff -r f04b33ce250f -r a4dc62a46ee4 datatype.ML --- a/datatype.ML Tue Oct 24 14:59:17 1995 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,486 +0,0 @@ -(* Title: HOL/datatype.ML - ID: $Id$ - Author: Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker - Copyright 1995 TU Muenchen -*) - - -(*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; -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 *) - -(* substitute fname(ls,xk,rs) by yk(ls,rs) in t for (xk,yk) in pairs *) - -fun subst_apps (_,_) [] t = t - | subst_apps (fname,rpos) 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(rpos,b), drop(rpos,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,map subst (ls @ rs))) - end - else list_comb(f, map subst b) - end - | subst(t) = t - in subst t end; - -(* abstract rhs *) - -fun abst_rec (fname,rpos,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,rpos) - (map Free rargs ~~ map Free subs) rhs; - in - list_abs_free (cargs @ subs @ ls @ rs, subst_rhs) - 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 rpos = 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" - ,rpos,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 - 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,rpos,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 rpos <> rpos1 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,rpos,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 ; - -in - fun add_datatype (typevars, tname, cons_list') thy = - 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.") - | 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 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 *'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; - 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)); - - 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)) = - 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, _, 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) - ^ ". "; - 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; - - 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) = - 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, _, 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) - 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 termS; - in [(tname, term_list, termS)] - 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_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 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 - - 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, _, 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,_,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, _, 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; - - 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 neq => snd(read_axm (sign_of thy) neq)) 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 defpair = mk_defpair (Const(fname,dummyT),rhs) - val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair; - val varT = Type.varifyT T; - val ftyp = the (Sign.const_type sg fname); - in - if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT) - then add_defs_i [defpairT] 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 - -(* -Informal description of functions used in datatype.ML for the Isabelle/HOL -implementation of prim. rec. function definitions. (N. Voelker, Feb. 1995) - -* subst_apps (fname,rpos) pairs t: - substitute the term - fname(ls,xk,rs) - by - yk(ls,rs) - in t for (xk,yk) in pairs, where rpos = length ls. - Applied with : - fname = function name - rpos = position of recursive argument - pairs = list of pairs (xk,yk), where - xk are the rec. arguments of the constructor in the pattern, - yk is a variable with name derived from xk - t = rhs of equation - -* abst_rec (fname,rpos,tc,ls,cargs,rs,rhs) - - filter recursive arguments from constructor arguments cargs, - - perform substitutions on rhs, - - derive list subs of new variable names yk for use in subst_apps, - - abstract rhs with respect to cargs, subs, ls and rs. - -* dest_eq t - destruct a term denoting an equation into lhs and rhs. - -* dest_req eq - destruct an equation of the form - name (vl1..vlrpos, Ci(vi1..vin), vr1..vrn) = rhs - into - - function name (name) - - position of the first non-variable parameter (rpos) - - the list of first rpos parameters (ls = [vl1..vlrpos]) - - the constructor (fst( dest_Const c) = Ci) - - the arguments of the constructor (cargs = [vi1..vin]) - - the rest of the variables in the pattern (rs = [vr1..vrn]) - - the right hand side of the equation (rhs). - -* check_and_sort (n,its) - check that n = length its holds, and sort elements of its by - first component. - -* trans_recs thy cs' (eq1::eqs) - destruct eq1 into name1, rpos1, ls1, etc.. - get constructor list with and without type (tcs resp. cs) from cs', - for every equation: - destruct it into (name,rpos,ls,c,cargs,rs,rhs) - get typed constructor tc from c and tcs - determine the index i of the constructor - check function name and position of rec. argument by comparison - with first equation - check for repeated variable names in pattern - derive function term f_i which is used as argument of the rec. combinator - sort the terms f_i according to i and return them together - with the function name and the parameter of the definition (ls). - -* Application: - - The rec. combinator is applied to the function terms resulting from - trans_rec. This results in a function which takes the recursive arg. - as first parameter and then the arguments corresponding to ls. The - order of parameters is corrected by setting the rhs equal to - - list_abs_free - (ls @ [(tname,dummyT)] - ,list_comb(rec_comb - , fns @ map Bound (0 ::(length ls downto 1)))); - - Note the de-Bruijn indices counting the number of lambdas between the - variable and its binding. -*)