--- 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.
+*)