diff -r 1a3d3b5b5d15 -r 9b403e123c1b datatype.ML --- a/datatype.ML Wed Feb 08 11:34:11 1995 +0100 +++ b/datatype.ML Wed Feb 08 14:06:37 1995 +0100 @@ -1,7 +1,7 @@ (* Title: HOL/datatype.ML ID: $Id$ Author: Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker - Copyright 1994 TU Muenchen + Copyright 1995 TU Muenchen *) @@ -23,10 +23,10 @@ (* ----------------------------------------------------------------------- *) (* Derivation of the primrec combinator application from the equations *) -(* subst. applications fname(ls,xk,rs) by yk(ls,rs) for xk in rargs *) +(* substitute fname(ls,xk,rs) by yk(ls,rs) in t for (xk,yk) in pairs *) fun subst_apps (_,_) [] t = t - | subst_apps (fname,cpos) pairs t = + | subst_apps (fname,rpos) pairs t = let fun subst (Abs(a,T,t)) = Abs(a,T,subst t) | subst (funct $ body) = @@ -34,7 +34,7 @@ in if is_Const f andalso fst(dest_Const f) = fname then - let val (ls,rest) = (take(cpos,b), drop (cpos,b)); + 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" @@ -42,7 +42,7 @@ (case assoc (pairs,xk) of None => raise RecError ("illegal occurence of " ^ fname ^ " on rhs") - | Some(U) => list_comb(U,ls @ rs)) + | Some(U) => list_comb(U,map subst (ls @ rs))) end else list_comb(f, map subst b) end @@ -51,18 +51,15 @@ (* abstract rhs *) -fun abst_rec (fname,cpos,tc,ls,cargs,rs,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,cpos) + val subst_rhs = subst_apps (fname,rpos) (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 + in + list_abs_free (cargs @ subs @ ls @ rs, subst_rhs) end; (* parsing the prim rec equations *) @@ -76,7 +73,7 @@ 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 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' @@ -90,7 +87,7 @@ 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) + ,rpos,ls,fst( dest_Const c),cargs,rs,rhs) end; (* check function specified for all constructors and sort function terms *) @@ -106,7 +103,7 @@ fun trans_recs _ _ [] = error("No primrec equations.") | trans_recs thy cs' (eq1::eqs) = - let val (name1,cpos1,ls1,_,_,_,_) = dest_rec eq1 + 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); @@ -114,19 +111,19 @@ 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; + 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 cpos <> cpos1 then + 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,cpos,the tc,ls,cargs,rs,rhs)) + else (i,abst_rec (name,rpos,the tc,ls,cargs,rs,rhs)) :: trans_recs' (i::cis) eqs end handle RecError s => @@ -444,3 +441,76 @@ |> add_axioms rules,add_primrec) 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. +*)