src/Pure/logic.ML
author wenzelm
Mon Apr 10 00:33:49 2006 +0200 (2006-04-10)
changeset 19391 4812d28c90a6
parent 19125 59b26248547b
child 19406 410b9d9bf9a1
permissions -rw-r--r--
Term.itselfT;
     1 (*  Title:      Pure/logic.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   Cambridge University 1992
     5 
     6 Abstract syntax operations of the Pure meta-logic.
     7 *)
     8 
     9 signature LOGIC =
    10 sig
    11   val is_all: term -> bool
    12   val dest_all: term -> typ * term
    13   val mk_equals: term * term -> term
    14   val dest_equals: term -> term * term
    15   val is_equals: term -> bool
    16   val mk_implies: term * term -> term
    17   val dest_implies: term -> term * term
    18   val is_implies: term -> bool
    19   val list_implies: term list * term -> term
    20   val strip_imp_prems: term -> term list
    21   val strip_imp_concl: term -> term
    22   val strip_prems: int * term list * term -> term list * term
    23   val count_prems: term * int -> int
    24   val nth_prem: int * term -> term
    25   val conjunction: term
    26   val mk_conjunction: term * term -> term
    27   val mk_conjunction_list: term list -> term
    28   val mk_conjunction_list2: term list list -> term
    29   val dest_conjunction: term -> term * term
    30   val dest_conjunctions: term -> term list
    31   val strip_horn: term -> term list * term
    32   val dest_type: term -> typ
    33   val const_of_class: class -> string
    34   val class_of_const: string -> class
    35   val mk_inclass: typ * class -> term
    36   val dest_inclass: term -> typ * class
    37   val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
    38     term -> (term * term) * term
    39   val abs_def: term -> term * term
    40   val mk_cond_defpair: term list -> term * term -> string * term
    41   val mk_defpair: term * term -> string * term
    42   val mk_type: typ -> term
    43   val protectC: term
    44   val protect: term -> term
    45   val unprotect: term -> term
    46   val occs: term * term -> bool
    47   val close_form: term -> term
    48   val combound: term * int * int -> term
    49   val rlist_abs: (string * typ) list * term -> term
    50   val incr_indexes: typ list * int -> term -> term
    51   val incr_tvar: int -> typ -> typ
    52   val lift_abs: int -> term -> term -> term
    53   val lift_all: int -> term -> term -> term
    54   val strip_assums_hyp: term -> term list
    55   val strip_assums_concl: term -> term
    56   val strip_params: term -> (string * typ) list
    57   val has_meta_prems: term -> int -> bool
    58   val flatten_params: int -> term -> term
    59   val auto_rename: bool ref
    60   val set_rename_prefix: string -> unit
    61   val list_rename_params: string list * term -> term
    62   val assum_pairs: int * term -> (term*term)list
    63   val varify: term -> term
    64   val unvarify: term -> term
    65   val get_goal: term -> int -> term
    66   val goal_params: term -> int -> term * term list
    67   val prems_of_goal: term -> int -> term list
    68   val concl_of_goal: term -> int -> term
    69 end;
    70 
    71 structure Logic : LOGIC =
    72 struct
    73 
    74 
    75 (*** Abstract syntax operations on the meta-connectives ***)
    76 
    77 (** all **)
    78 
    79 fun is_all (Const ("all", _) $ _) = true
    80   | is_all _ = false;
    81 
    82 fun dest_all (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ A) = (T, A)
    83   | dest_all t = raise TERM ("dest_all", [t]);
    84 
    85 
    86 
    87 (** equality **)
    88 
    89 (*Make an equality.  DOES NOT CHECK TYPE OF u*)
    90 fun mk_equals(t,u) = equals(fastype_of t) $ t $ u;
    91 
    92 fun dest_equals (Const("==",_) $ t $ u)  =  (t,u)
    93   | dest_equals t = raise TERM("dest_equals", [t]);
    94 
    95 fun is_equals (Const ("==", _) $ _ $ _) = true
    96   | is_equals _ = false;
    97 
    98 
    99 (** implies **)
   100 
   101 fun mk_implies(A,B) = implies $ A $ B;
   102 
   103 fun dest_implies (Const("==>",_) $ A $ B)  =  (A,B)
   104   | dest_implies A = raise TERM("dest_implies", [A]);
   105 
   106 fun is_implies (Const ("==>", _) $ _ $ _) = true
   107   | is_implies _ = false;
   108 
   109 
   110 (** nested implications **)
   111 
   112 (* [A1,...,An], B  goes to  A1==>...An==>B  *)
   113 fun list_implies ([], B) = B
   114   | list_implies (A::As, B) = implies $ A $ list_implies(As,B);
   115 
   116 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   117 fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
   118   | strip_imp_prems _ = [];
   119 
   120 (* A1==>...An==>B  goes to B, where B is not an implication *)
   121 fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
   122   | strip_imp_concl A = A : term;
   123 
   124 (*Strip and return premises: (i, [], A1==>...Ai==>B)
   125     goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
   126   if  i<0 or else i too big then raises  TERM*)
   127 fun strip_prems (0, As, B) = (As, B)
   128   | strip_prems (i, As, Const("==>", _) $ A $ B) =
   129         strip_prems (i-1, A::As, B)
   130   | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
   131 
   132 (*Count premises -- quicker than (length o strip_prems) *)
   133 fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1)
   134   | count_prems (_,n) = n;
   135 
   136 (*Select Ai from A1 ==>...Ai==>B*)
   137 fun nth_prem (1, Const ("==>", _) $ A $ _) = A
   138   | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
   139   | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
   140 
   141 (*strip a proof state (Horn clause):
   142   B1 ==> ... Bn ==> C   goes to   ([B1, ..., Bn], C)    *)
   143 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
   144 
   145 
   146 (** conjunction **)
   147 
   148 val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
   149 
   150 (*A && B*)
   151 fun mk_conjunction (A, B) = conjunction $ A $ B;
   152 
   153 (*A && B && C -- improper*)
   154 fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
   155   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
   156 
   157 (*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
   158 fun mk_conjunction_list2 tss =
   159   mk_conjunction_list (map mk_conjunction_list (filter_out null tss));
   160 
   161 (*A && B*)
   162 fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
   163   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
   164 
   165 (*((A && B) && C) && D && E -- flat*)
   166 fun dest_conjunctions t =
   167   (case try dest_conjunction t of
   168     NONE => [t]
   169   | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
   170 
   171 
   172 
   173 (** types as terms **)
   174 
   175 fun mk_type ty = Const ("TYPE", Term.itselfT ty);
   176 
   177 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   178   | dest_type t = raise TERM ("dest_type", [t]);
   179 
   180 
   181 (** class constraints **)
   182 
   183 val classN = "_class";
   184 
   185 val const_of_class = suffix classN;
   186 fun class_of_const c = unsuffix classN c
   187   handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
   188 
   189 fun mk_inclass (ty, c) =
   190   Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
   191 
   192 fun dest_inclass (t as Const (c_class, _) $ ty) =
   193       ((dest_type ty, class_of_const c_class)
   194         handle TERM _ => raise TERM ("dest_inclass", [t]))
   195   | dest_inclass t = raise TERM ("dest_inclass", [t]);
   196 
   197 
   198 
   199 (** definitions **)
   200 
   201 fun term_kind (Const _) = "existing constant "
   202   | term_kind (Free _) = "free variable "
   203   | term_kind (Bound _) = "bound variable "
   204   | term_kind _ = "";
   205 
   206 (*c x == t[x] to !!x. c x == t[x]*)
   207 fun dest_def pp check_head is_fixed is_fixedT eq =
   208   let
   209     fun err msg = raise TERM (msg, [eq]);
   210     val eq_vars = Term.strip_all_vars eq;
   211     val eq_body = Term.strip_all_body eq;
   212 
   213     val display_terms = commas_quote o map (Pretty.string_of_term pp o Syntax.bound_vars eq_vars);
   214     val display_types = commas_quote o map (Pretty.string_of_typ pp);
   215 
   216     val (raw_lhs, rhs) = dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
   217     val lhs = Envir.beta_eta_contract raw_lhs;
   218     val (head, args) = Term.strip_comb lhs;
   219     val head_tfrees = Term.add_tfrees head [];
   220 
   221     fun check_arg (Bound _) = true
   222       | check_arg (Free (x, _)) = not (is_fixed x)
   223       | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
   224       | check_arg _ = false;
   225     fun close_arg (Bound _) t = t
   226       | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
   227 
   228     val lhs_bads = filter_out check_arg args;
   229     val lhs_dups = duplicates (op aconv) args;
   230     val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
   231       if is_fixed x orelse member (op aconv) args v then I
   232       else insert (op aconv) v | _ => I) rhs [];
   233     val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
   234       if is_fixedT a orelse member (op =) head_tfrees (a, S) then I
   235       else insert (op =) v | _ => I)) rhs [];
   236   in
   237     if not (check_head head) then
   238       err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])
   239     else if not (null lhs_bads) then
   240       err ("Bad arguments on lhs: " ^ display_terms lhs_bads)
   241     else if not (null lhs_dups) then
   242       err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups)
   243     else if not (null rhs_extras) then
   244       err ("Extra variables on rhs: " ^ display_terms rhs_extras)
   245     else if not (null rhs_extrasT) then
   246       err ("Extra type variables on rhs: " ^ display_types rhs_extrasT)
   247     else if exists_subterm (fn t => t aconv head) rhs then
   248       err "Entity to be defined occurs on rhs"
   249     else ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (mk_equals (lhs, rhs)))))
   250   end;
   251 
   252 (*!!x. c x == t[x] to c == %x. t[x]*)
   253 fun abs_def eq =
   254   let
   255     val body = Term.strip_all_body eq;
   256     val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
   257     val (lhs, rhs) = dest_equals (Term.subst_bounds (vars, body));
   258     val (lhs', args) = Term.strip_comb lhs;
   259     val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
   260   in (lhs', rhs') end;
   261 
   262 fun mk_cond_defpair As (lhs, rhs) =
   263   (case Term.head_of lhs of
   264     Const (name, _) =>
   265       (NameSpace.base name ^ "_def", list_implies (As, mk_equals (lhs, rhs)))
   266   | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
   267 
   268 fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs;
   269 
   270 
   271 (** protected propositions **)
   272 
   273 val protectC = Const ("prop", propT --> propT);
   274 fun protect t = protectC $ t;
   275 
   276 fun unprotect (Const ("prop", _) $ t) = t
   277   | unprotect t = raise TERM ("unprotect", [t]);
   278 
   279 
   280 
   281 (*** Low-level term operations ***)
   282 
   283 (*Does t occur in u?  Or is alpha-convertible to u?
   284   The term t must contain no loose bound variables*)
   285 fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
   286 
   287 (*Close up a formula over all free variables by quantification*)
   288 fun close_form A =
   289   list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A);
   290 
   291 
   292 
   293 (*** Specialized operations for resolution... ***)
   294 
   295 (*computes t(Bound(n+k-1),...,Bound(n))  *)
   296 fun combound (t, n, k) =
   297     if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   298 
   299 (* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   300 fun rlist_abs ([], body) = body
   301   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   302 
   303 
   304 local exception SAME in
   305 
   306 fun incrT k =
   307   let
   308     fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
   309       | incr (Type (a, Ts)) = Type (a, incrs Ts)
   310       | incr _ = raise SAME
   311     and incrs (T :: Ts) =
   312         (incr T :: (incrs Ts handle SAME => Ts)
   313           handle SAME => T :: incrs Ts)
   314       | incrs [] = raise SAME;
   315   in incr end;
   316 
   317 (*For all variables in the term, increment indexnames and lift over the Us
   318     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   319 fun incr_indexes ([], 0) t = t
   320   | incr_indexes (Ts, k) t =
   321   let
   322     val n = length Ts;
   323     val incrT = if k = 0 then I else incrT k;
   324 
   325     fun incr lev (Var ((x, i), T)) =
   326           combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
   327       | incr lev (Abs (x, T, body)) =
   328           (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
   329             handle SAME => Abs (x, T, incr (lev + 1) body))
   330       | incr lev (t $ u) =
   331           (incr lev t $ (incr lev u handle SAME => u)
   332             handle SAME => t $ incr lev u)
   333       | incr _ (Const (c, T)) = Const (c, incrT T)
   334       | incr _ (Free (x, T)) = Free (x, incrT T)
   335       | incr _ (t as Bound _) = t;
   336   in incr 0 t handle SAME => t end;
   337 
   338 fun incr_tvar 0 T = T
   339   | incr_tvar k T = incrT k T handle SAME => T;
   340 
   341 end;
   342 
   343 
   344 (* Lifting functions from subgoal and increment:
   345     lift_abs operates on terms
   346     lift_all operates on propositions *)
   347 
   348 fun lift_abs inc =
   349   let
   350     fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
   351       | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
   352       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   353   in lift [] end;
   354 
   355 fun lift_all inc =
   356   let
   357     fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
   358       | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
   359       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   360   in lift [] end;
   361 
   362 (*Strips assumptions in goal, yielding list of hypotheses.   *)
   363 fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B
   364   | strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t
   365   | strip_assums_hyp B = [];
   366 
   367 (*Strips assumptions in goal, yielding conclusion.   *)
   368 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   369   | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   370   | strip_assums_concl B = B;
   371 
   372 (*Make a list of all the parameters in a subgoal, even if nested*)
   373 fun strip_params (Const("==>", _) $ H $ B) = strip_params B
   374   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   375   | strip_params B = [];
   376 
   377 (*test for meta connectives in prems of a 'subgoal'*)
   378 fun has_meta_prems prop i =
   379   let
   380     fun is_meta (Const ("==>", _) $ _ $ _) = true
   381       | is_meta (Const ("==", _) $ _ $ _) = true
   382       | is_meta (Const ("all", _) $ _) = true
   383       | is_meta _ = false;
   384   in
   385     (case strip_prems (i, [], prop) of
   386       (B :: _, _) => exists is_meta (strip_assums_hyp B)
   387     | _ => false) handle TERM _ => false
   388   end;
   389 
   390 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
   391     where j is the total number of parameters (precomputed)
   392   If n>0 then deletes assumption n. *)
   393 fun remove_params j n A =
   394     if j=0 andalso n<=0 then A  (*nothing left to do...*)
   395     else case A of
   396         Const("==>", _) $ H $ B =>
   397           if n=1 then                           (remove_params j (n-1) B)
   398           else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   399       | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   400       | _ => if n>0 then raise TERM("remove_params", [A])
   401              else A;
   402 
   403 (** Auto-renaming of parameters in subgoals **)
   404 
   405 val auto_rename = ref false
   406 and rename_prefix = ref "ka";
   407 
   408 (*rename_prefix is not exported; it is set by this function.*)
   409 fun set_rename_prefix a =
   410     if a<>"" andalso forall Symbol.is_letter (Symbol.explode a)
   411     then  (rename_prefix := a;  auto_rename := true)
   412     else  error"rename prefix must be nonempty and consist of letters";
   413 
   414 (*Makes parameters in a goal have distinctive names (not guaranteed unique!)
   415   A name clash could cause the printer to rename bound vars;
   416     then res_inst_tac would not work properly.*)
   417 fun rename_vars (a, []) = []
   418   | rename_vars (a, (_,T)::vars) =
   419         (a,T) :: rename_vars (Symbol.bump_string a, vars);
   420 
   421 (*Move all parameters to the front of the subgoal, renaming them apart;
   422   if n>0 then deletes assumption n. *)
   423 fun flatten_params n A =
   424     let val params = strip_params A;
   425         val vars = if !auto_rename
   426                    then rename_vars (!rename_prefix, params)
   427                    else ListPair.zip (variantlist(map #1 params,[]),
   428                                       map #2 params)
   429     in  list_all (vars, remove_params (length vars) n A)
   430     end;
   431 
   432 (*Makes parameters in a goal have the names supplied by the list cs.*)
   433 fun list_rename_params (cs, Const("==>", _) $ A $ B) =
   434       implies $ A $ list_rename_params (cs, B)
   435   | list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) =
   436       all T $ Abs(c, T, list_rename_params (cs, t))
   437   | list_rename_params (cs, B) = B;
   438 
   439 (*** Treatmsent of "assume", "erule", etc. ***)
   440 
   441 (*Strips assumptions in goal yielding
   442    HS = [Hn,...,H1],   params = [xm,...,x1], and B,
   443   where x1...xm are the parameters. This version (21.1.2005) REQUIRES
   444   the the parameters to be flattened, but it allows erule to work on
   445   assumptions of the form !!x. phi. Any !! after the outermost string
   446   will be regarded as belonging to the conclusion, and left untouched.
   447   Used ONLY by assum_pairs.
   448       Unless nasms<0, it can terminate the recursion early; that allows
   449   erule to work on assumptions of the form P==>Q.*)
   450 fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
   451   | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
   452       strip_assums_imp (nasms-1, H::Hs, B)
   453   | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
   454 
   455 
   456 (*Strips OUTER parameters only, unlike similar legacy versions.*)
   457 fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
   458       strip_assums_all ((a,T)::params, t)
   459   | strip_assums_all (params, B) = (params, B);
   460 
   461 (*Produces disagreement pairs, one for each assumption proof, in order.
   462   A is the first premise of the lifted rule, and thus has the form
   463     H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B).
   464   nasms is the number of assumptions in the original subgoal, needed when B
   465     has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
   466 fun assum_pairs(nasms,A) =
   467   let val (params, A') = strip_assums_all ([],A)
   468       val (Hs,B) = strip_assums_imp (nasms,[],A')
   469       fun abspar t = rlist_abs(params, t)
   470       val D = abspar B
   471       fun pairrev ([], pairs) = pairs
   472         | pairrev (H::Hs, pairs) = pairrev(Hs,  (abspar H, D) :: pairs)
   473   in  pairrev (Hs,[])
   474   end;
   475 
   476 (*Converts Frees to Vars and TFrees to TVars*)
   477 fun varify (Const(a, T)) = Const (a, Type.varifyT T)
   478   | varify (Free (a, T)) = Var ((a, 0), Type.varifyT T)
   479   | varify (Var (ixn, T)) = Var (ixn, Type.varifyT T)
   480   | varify (t as Bound _) = t
   481   | varify (Abs (a, T, body)) = Abs (a, Type.varifyT T, varify body)
   482   | varify (f $ t) = varify f $ varify t;
   483 
   484 (*Inverse of varify.*)
   485 fun unvarify (Const (a, T)) = Const (a, Type.unvarifyT T)
   486   | unvarify (Free (a, T)) = Free (a, Type.unvarifyT T)
   487   | unvarify (Var ((a, 0), T)) = Free (a, Type.unvarifyT T)
   488   | unvarify (Var (ixn, T)) = Var (ixn, Type.unvarifyT T)  (*non-0 index!*)
   489   | unvarify (t as Bound _) = t
   490   | unvarify (Abs (a, T, body)) = Abs (a, Type.unvarifyT T, unvarify body)
   491   | unvarify (f $ t) = unvarify f $ unvarify t;
   492 
   493 
   494 (* goal states *)
   495 
   496 fun get_goal st i = nth_prem (i, st)
   497   handle TERM _ => error "Goal number out of range";
   498 
   499 (*reverses parameters for substitution*)
   500 fun goal_params st i =
   501   let val gi = get_goal st i
   502       val rfrees = map Free (rename_wrt_term gi (strip_params gi))
   503   in (gi, rfrees) end;
   504 
   505 fun concl_of_goal st i =
   506   let val (gi, rfrees) = goal_params st i
   507       val B = strip_assums_concl gi
   508   in subst_bounds (rfrees, B) end;
   509 
   510 fun prems_of_goal st i =
   511   let val (gi, rfrees) = goal_params st i
   512       val As = strip_assums_hyp gi
   513   in map (fn A => subst_bounds (rfrees, A)) As end;
   514 
   515 end;