Some changes to allow mutually recursive, overloaded functions with same name.
authorberghofe
Fri Jul 08 11:57:15 2005 +0200 (2005-07-08)
changeset 16765b8b1f310877f
parent 16764 ca81a99c5bc1
child 16766 ea667a5426fe
Some changes to allow mutually recursive, overloaded functions with same name.
src/HOL/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Jul 08 11:39:59 2005 +0200
     1.2 +++ b/src/HOL/Tools/primrec_package.ML	Fri Jul 08 11:57:15 2005 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4  	else raise RecError "illegal schematic variable(s)";
     1.5  
     1.6      val (recfun, args) = strip_comb lhs;
     1.7 -    val (fname, _) = dest_Const recfun handle TERM _ => 
     1.8 +    val fnameT = dest_Const recfun handle TERM _ => 
     1.9        raise RecError "function is not declared as constant in theory";
    1.10  
    1.11      val (ls', rest)  = take_prefix is_Free args;
    1.12 @@ -72,9 +72,9 @@
    1.13       (check_vars "repeated variable names in pattern: " (duplicates lfrees);
    1.14        check_vars "extra variables on rhs: "
    1.15          (map dest_Free (term_frees rhs) \\ lfrees);
    1.16 -      case assoc (rec_fns, fname) of
    1.17 +      case assoc (rec_fns, fnameT) of
    1.18          NONE =>
    1.19 -          (fname, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
    1.20 +          (fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
    1.21        | SOME (_, rpos', eqns) =>
    1.22            if isSome (assoc (eqns, cname)) then
    1.23              raise RecError "constructor already occurred as pattern"
    1.24 @@ -82,13 +82,13 @@
    1.25              raise RecError "position of recursive argument inconsistent"
    1.26            else
    1.27              overwrite (rec_fns, 
    1.28 -		       (fname, 
    1.29 +		       (fnameT, 
    1.30  			(tname, rpos,
    1.31  			 (cname, (ls, cargs, rs, rhs, eq))::eqns))))
    1.32    end
    1.33    handle RecError s => primrec_eq_err sign s eq;
    1.34  
    1.35 -fun process_fun sign descr rec_eqns ((i, fname), (fnames, fnss)) =
    1.36 +fun process_fun sign descr rec_eqns ((i, fnameT as (fname, _)), (fnameTs, fnss)) =
    1.37    let
    1.38      val (_, (tname, _, constrs)) = List.nth (descr, i);
    1.39  
    1.40 @@ -101,10 +101,10 @@
    1.41        | subst subs (fs, t as (_ $ _)) =
    1.42            let val (f, ts) = strip_comb t;
    1.43            in
    1.44 -            if is_Const f andalso (fst (dest_Const f)) mem (map fst rec_eqns) then
    1.45 +            if is_Const f andalso dest_Const f mem map fst rec_eqns then
    1.46                let
    1.47 -                val (fname', _) = dest_Const f;
    1.48 -                val (_, rpos, _) = valOf (assoc (rec_eqns, fname'));
    1.49 +                val fnameT' as (fname', _) = dest_Const f;
    1.50 +                val (_, rpos, _) = valOf (assoc (rec_eqns, fnameT'));
    1.51                  val ls = Library.take (rpos, ts);
    1.52                  val rest = Library.drop (rpos, ts);
    1.53                  val (x', rs) = (hd rest, tl rest)
    1.54 @@ -120,7 +120,7 @@
    1.55                    | SOME (i', y) =>
    1.56                        let
    1.57                          val (fs', ts') = foldl_map (subst subs) (fs, xs @ ls @ rs);
    1.58 -                        val fs'' = process_fun sign descr rec_eqns ((i', fname'), fs')
    1.59 +                        val fs'' = process_fun sign descr rec_eqns ((i', fnameT'), fs')
    1.60                        in (fs'', list_comb (y, ts'))
    1.61                        end)
    1.62                end
    1.63 @@ -133,41 +133,41 @@
    1.64  
    1.65      (* translate rec equations into function arguments suitable for rec comb *)
    1.66  
    1.67 -    fun trans eqns ((cname, cargs), (fnames', fnss', fns)) =
    1.68 +    fun trans eqns ((cname, cargs), (fnameTs', fnss', fns)) =
    1.69        (case assoc (eqns, cname) of
    1.70            NONE => (warning ("No equation for constructor " ^ quote cname ^
    1.71              "\nin definition of function " ^ quote fname);
    1.72 -              (fnames', fnss', (Const ("arbitrary", dummyT))::fns))
    1.73 +              (fnameTs', fnss', (Const ("arbitrary", dummyT))::fns))
    1.74          | SOME (ls, cargs', rs, rhs, eq) =>
    1.75              let
    1.76                val recs = List.filter (is_rec_type o snd) (cargs' ~~ cargs);
    1.77                val rargs = map fst recs;
    1.78                val subs = map (rpair dummyT o fst) 
    1.79  		             (rev (rename_wrt_term rhs rargs));
    1.80 -              val ((fnames'', fnss''), rhs') = 
    1.81 +              val ((fnameTs'', fnss''), rhs') = 
    1.82  		  (subst (map (fn ((x, y), z) =>
    1.83  			       (Free x, (body_index y, Free z)))
    1.84  			  (recs ~~ subs))
    1.85 -		   ((fnames', fnss'), rhs))
    1.86 +		   ((fnameTs', fnss'), rhs))
    1.87                    handle RecError s => primrec_eq_err sign s eq
    1.88 -            in (fnames'', fnss'', 
    1.89 +            in (fnameTs'', fnss'', 
    1.90  		(list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns)
    1.91              end)
    1.92  
    1.93 -  in (case assoc (fnames, i) of
    1.94 +  in (case assoc (fnameTs, i) of
    1.95        NONE =>
    1.96 -        if exists (equal fname o snd) fnames then
    1.97 +        if exists (equal fnameT o snd) fnameTs then
    1.98            raise RecError ("inconsistent functions for datatype " ^ quote tname)
    1.99          else
   1.100            let
   1.101 -            val (_, _, eqns) = valOf (assoc (rec_eqns, fname));
   1.102 -            val (fnames', fnss', fns) = foldr (trans eqns)
   1.103 -              ((i, fname)::fnames, fnss, []) constrs
   1.104 +            val (_, _, eqns) = valOf (assoc (rec_eqns, fnameT));
   1.105 +            val (fnameTs', fnss', fns) = foldr (trans eqns)
   1.106 +              ((i, fnameT)::fnameTs, fnss, []) constrs
   1.107            in
   1.108 -            (fnames', (i, (fname, #1 (snd (hd eqns)), fns))::fnss')
   1.109 +            (fnameTs', (i, (fname, #1 (snd (hd eqns)), fns))::fnss')
   1.110            end
   1.111 -    | SOME fname' =>
   1.112 -        if fname = fname' then (fnames, fnss)
   1.113 +    | SOME fnameT' =>
   1.114 +        if fnameT = fnameT' then (fnameTs, fnss)
   1.115          else raise RecError ("inconsistent functions for datatype " ^ quote tname))
   1.116    end;
   1.117  
   1.118 @@ -241,20 +241,21 @@
   1.119  	    primrec_err ("datatypes " ^ commas_quote tnames ^ 
   1.120  			 "\nare not mutually recursive")
   1.121  	else snd (hd dts);
   1.122 -    val (fnames, fnss) = foldr (process_fun sg descr rec_eqns)
   1.123 +    val (fnameTs, fnss) = foldr (process_fun sg descr rec_eqns)
   1.124  	                       ([], []) main_fns;
   1.125      val (fs, defs) = foldr (get_fns fnss) ([], []) (descr ~~ rec_names);
   1.126      val defs' = map (make_def sg fs) defs;
   1.127 -    val names1 = map snd fnames;
   1.128 -    val names2 = map fst rec_eqns;
   1.129 +    val nameTs1 = map snd fnameTs;
   1.130 +    val nameTs2 = map fst rec_eqns;
   1.131      val primrec_name =
   1.132        if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
   1.133      val (thy', defs_thms') = thy |> Theory.add_path primrec_name |>
   1.134 -      (if eq_set (names1, names2) then (PureThy.add_defs_i false o map Thm.no_attributes) defs'
   1.135 -       else primrec_err ("functions " ^ commas_quote names2 ^
   1.136 +      (if eq_set (nameTs1, nameTs2) then (PureThy.add_defs_i false o map Thm.no_attributes) defs'
   1.137 +       else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
   1.138           "\nare not mutually recursive"));
   1.139      val rewrites = (map mk_meta_eq rec_rewrites) @ defs_thms';
   1.140 -    val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names1 ^ " ...");
   1.141 +    val _ = message ("Proving equations for primrec function(s) " ^
   1.142 +      commas_quote (map fst nameTs1) ^ " ...");
   1.143      val simps = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
   1.144          (fn _ => [rtac refl 1])) eqns;
   1.145      val (thy'', simps') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';