datatype.ML

 (* Title:       HOL/datatype.ML
    ID:          $Id$
    Author:      Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker
-   Copyright 1994 TU Muenchen
+   Copyright 1995 TU Muenchen
 *)
 
 
 (*used for constructor parameters*)
 datatype dt_type = dtVar of string |

 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 *)
+(* 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) = 
 	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));
+	      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,ls @ rs))
+		 | 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,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 *)
 
 fun dest_eq ( Const("Trueprop",_) $ (Const ("op =",_) $ lhs $ rhs))

 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 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 "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)
+		 ,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) = 

 (* 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
+    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);
       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; 
+	  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 =>
 	        error("Primrec definition error\n" ^ s ^ "\n" 
 		      ^ "   " ^ Sign.string_of_term (sign_of thy) eq);

       |> add_consts consts
       |> add_trrules xrules
       |> 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. 
+*)