src/HOL/BNF/Tools/bnf_fp_util.ML
author blanchet
Mon May 06 21:20:54 2013 +0200 (2013-05-06)
changeset 51884 2928fda12661
parent 51869 d58cd7673b04
child 51893 596baae88a88
permissions -rw-r--r--
factor out construction of iterator
     1 (*  Title:      HOL/BNF/Tools/bnf_fp_util.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Copyright   2012, 2013
     5 
     6 Shared library for the datatype and codatatype constructions.
     7 *)
     8 
     9 signature BNF_FP_UTIL =
    10 sig
    11   type fp_result =
    12     {Ts: typ list,
    13      bnfs: BNF_Def.bnf list,
    14      ctors: term list,
    15      dtors: term list,
    16      un_folds: term list,
    17      co_recs: term list,
    18      co_induct: thm,
    19      strong_co_induct: thm,
    20      dtor_ctors: thm list,
    21      ctor_dtors: thm list,
    22      ctor_injects: thm list,
    23      map_thms: thm list,
    24      set_thmss: thm list list,
    25      rel_thms: thm list,
    26      un_fold_thms: thm list,
    27      co_rec_thms: thm list}
    28 
    29   val morph_fp_result: morphism -> fp_result -> fp_result
    30   val eq_fp_result: fp_result * fp_result -> bool
    31 
    32   val time: Timer.real_timer -> string -> Timer.real_timer
    33 
    34   val IITN: string
    35   val LevN: string
    36   val algN: string
    37   val behN: string
    38   val bisN: string
    39   val carTN: string
    40   val caseN: string
    41   val coN: string
    42   val coinductN: string
    43   val corecN: string
    44   val ctorN: string
    45   val ctor_dtorN: string
    46   val ctor_dtor_corecN: string
    47   val ctor_dtor_unfoldN: string
    48   val ctor_exhaustN: string
    49   val ctor_induct2N: string
    50   val ctor_inductN: string
    51   val ctor_injectN: string
    52   val ctor_foldN: string
    53   val ctor_fold_uniqueN: string
    54   val ctor_mapN: string
    55   val ctor_map_uniqueN: string
    56   val ctor_recN: string
    57   val ctor_rec_uniqueN: string
    58   val ctor_relN: string
    59   val ctor_set_inclN: string
    60   val ctor_set_set_inclN: string
    61   val ctor_srelN: string
    62   val disc_unfoldN: string
    63   val disc_unfold_iffN: string
    64   val disc_corecN: string
    65   val disc_corec_iffN: string
    66   val dtorN: string
    67   val dtor_coinductN: string
    68   val dtor_corecN: string
    69   val dtor_corec_uniqueN: string
    70   val dtor_ctorN: string
    71   val dtor_exhaustN: string
    72   val dtor_injectN: string
    73   val dtor_mapN: string
    74   val dtor_map_coinductN: string
    75   val dtor_map_strong_coinductN: string
    76   val dtor_map_uniqueN: string
    77   val dtor_relN: string
    78   val dtor_set_inclN: string
    79   val dtor_set_set_inclN: string
    80   val dtor_srelN: string
    81   val dtor_srel_coinductN: string
    82   val dtor_srel_strong_coinductN: string
    83   val dtor_strong_coinductN: string
    84   val dtor_unfoldN: string
    85   val dtor_unfold_uniqueN: string
    86   val exhaustN: string
    87   val foldN: string
    88   val hsetN: string
    89   val hset_recN: string
    90   val inductN: string
    91   val injectN: string
    92   val isNodeN: string
    93   val lsbisN: string
    94   val mapN: string
    95   val map_uniqueN: string
    96   val min_algN: string
    97   val morN: string
    98   val nchotomyN: string
    99   val recN: string
   100   val rel_injectN: string
   101   val rel_distinctN: string
   102   val rvN: string
   103   val sel_corecN: string
   104   val set_inclN: string
   105   val set_set_inclN: string
   106   val sel_unfoldN: string
   107   val setsN: string
   108   val simpsN: string
   109   val strTN: string
   110   val str_initN: string
   111   val strong_coinductN: string
   112   val sum_bdN: string
   113   val sum_bdTN: string
   114   val unfoldN: string
   115   val uniqueN: string
   116 
   117   (* TODO: Don't index set facts. Isabelle packages traditionally generate uniform names. *)
   118   val mk_ctor_setN: int -> string
   119   val mk_dtor_setN: int -> string
   120   val mk_dtor_set_inductN: int -> string
   121   val mk_set_inductN: int -> string
   122 
   123   val datatype_word: bool -> string
   124 
   125   val base_name_of_typ: typ -> string
   126   val mk_common_name: string list -> string
   127 
   128   val variant_types: string list -> sort list -> Proof.context ->
   129     (string * sort) list * Proof.context
   130   val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
   131 
   132   val split_conj_thm: thm -> thm list
   133   val split_conj_prems: int -> thm -> thm
   134 
   135   val mk_sumTN: typ list -> typ
   136   val mk_sumTN_balanced: typ list -> typ
   137 
   138   val id_const: typ -> term
   139 
   140   val Inl_const: typ -> typ -> term
   141   val Inr_const: typ -> typ -> term
   142 
   143   val mk_Inl: typ -> term -> term
   144   val mk_Inr: typ -> term -> term
   145   val mk_InN: typ list -> term -> int -> term
   146   val mk_InN_balanced: typ -> int -> term -> int -> term
   147   val mk_sum_case: term * term -> term
   148   val mk_sum_caseN: term list -> term
   149   val mk_sum_caseN_balanced: term list -> term
   150 
   151   val dest_sumT: typ -> typ * typ
   152   val dest_sumTN: int -> typ -> typ list
   153   val dest_sumTN_balanced: int -> typ -> typ list
   154   val dest_tupleT: int -> typ -> typ list
   155 
   156   val mk_Field: term -> term
   157   val mk_If: term -> term -> term -> term
   158   val mk_union: term * term -> term
   159 
   160   val mk_sumEN: int -> thm
   161   val mk_sumEN_balanced: int -> thm
   162   val mk_sumEN_tupled_balanced: int list -> thm
   163   val mk_sum_casesN: int -> int -> thm
   164   val mk_sum_casesN_balanced: int -> int -> thm
   165 
   166   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
   167 
   168   val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
   169       BNF_Def.bnf list -> local_theory -> 'a) ->
   170     binding list -> (string * sort) list -> ((string * sort) * typ) list -> local_theory ->
   171     BNF_Def.bnf list * 'a
   172 end;
   173 
   174 structure BNF_FP_Util : BNF_FP_UTIL =
   175 struct
   176 
   177 open BNF_Comp
   178 open BNF_Def
   179 open BNF_Util
   180 
   181 type fp_result =
   182   {Ts: typ list,
   183    bnfs: BNF_Def.bnf list,
   184    ctors: term list,
   185    dtors: term list,
   186    un_folds: term list,
   187    co_recs: term list,
   188    co_induct: thm,
   189    strong_co_induct: thm,
   190    dtor_ctors: thm list,
   191    ctor_dtors: thm list,
   192    ctor_injects: thm list,
   193    map_thms: thm list,
   194    set_thmss: thm list list,
   195    rel_thms: thm list,
   196    un_fold_thms: thm list,
   197    co_rec_thms: thm list};
   198 
   199 fun morph_fp_result phi {Ts, bnfs, ctors, dtors, un_folds, co_recs, co_induct, strong_co_induct,
   200     dtor_ctors, ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, un_fold_thms,
   201     co_rec_thms} =
   202   {Ts = map (Morphism.typ phi) Ts,
   203    bnfs = map (morph_bnf phi) bnfs,
   204    ctors = map (Morphism.term phi) ctors,
   205    dtors = map (Morphism.term phi) dtors,
   206    un_folds = map (Morphism.term phi) un_folds,
   207    co_recs = map (Morphism.term phi) co_recs,
   208    co_induct = Morphism.thm phi co_induct,
   209    strong_co_induct = Morphism.thm phi strong_co_induct,
   210    dtor_ctors = map (Morphism.thm phi) dtor_ctors,
   211    ctor_dtors = map (Morphism.thm phi) ctor_dtors,
   212    ctor_injects = map (Morphism.thm phi) ctor_injects,
   213    map_thms = map (Morphism.thm phi) map_thms,
   214    set_thmss = map (map (Morphism.thm phi)) set_thmss,
   215    rel_thms = map (Morphism.thm phi) rel_thms,
   216    un_fold_thms = map (Morphism.thm phi) un_fold_thms,
   217    co_rec_thms = map (Morphism.thm phi) co_rec_thms};
   218 
   219 fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
   220   eq_list eq_bnf (bnfs1, bnfs2);
   221 
   222 val timing = true;
   223 fun time timer msg = (if timing
   224   then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer))
   225   else (); Timer.startRealTimer ());
   226 
   227 val preN = "pre_"
   228 val rawN = "raw_"
   229 
   230 val coN = "co"
   231 val unN = "un"
   232 val algN = "alg"
   233 val IITN = "IITN"
   234 val foldN = "fold"
   235 val unfoldN = unN ^ foldN
   236 val uniqueN = "_unique"
   237 val simpsN = "simps"
   238 val ctorN = "ctor"
   239 val dtorN = "dtor"
   240 val ctor_foldN = ctorN ^ "_" ^ foldN
   241 val dtor_unfoldN = dtorN ^ "_" ^ unfoldN
   242 val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
   243 val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
   244 val ctor_dtor_unfoldN = ctorN ^ "_" ^ dtor_unfoldN
   245 val ctor_mapN = ctorN ^ "_" ^ mapN
   246 val dtor_mapN = dtorN ^ "_" ^ mapN
   247 val map_uniqueN = mapN ^ uniqueN
   248 val ctor_map_uniqueN = ctorN ^ "_" ^ map_uniqueN
   249 val dtor_map_uniqueN = dtorN ^ "_" ^ map_uniqueN
   250 val min_algN = "min_alg"
   251 val morN = "mor"
   252 val bisN = "bis"
   253 val lsbisN = "lsbis"
   254 val sum_bdTN = "sbdT"
   255 val sum_bdN = "sbd"
   256 val carTN = "carT"
   257 val strTN = "strT"
   258 val isNodeN = "isNode"
   259 val LevN = "Lev"
   260 val rvN = "recover"
   261 val behN = "beh"
   262 val setsN = "sets"
   263 val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN
   264 val mk_dtor_setN = prefix (dtorN ^ "_") o mk_setN
   265 fun mk_set_inductN i = mk_setN i ^ "_induct"
   266 val mk_dtor_set_inductN = prefix (dtorN ^ "_") o mk_set_inductN
   267 
   268 val str_initN = "str_init"
   269 val recN = "rec"
   270 val corecN = coN ^ recN
   271 val ctor_recN = ctorN ^ "_" ^ recN
   272 val ctor_rec_uniqueN = ctor_recN ^ uniqueN
   273 val dtor_corecN = dtorN ^ "_" ^ corecN
   274 val dtor_corec_uniqueN = dtor_corecN ^ uniqueN
   275 val ctor_dtor_corecN = ctorN ^ "_" ^ dtor_corecN
   276 
   277 val ctor_dtorN = ctorN ^ "_" ^ dtorN
   278 val dtor_ctorN = dtorN ^ "_" ^ ctorN
   279 val nchotomyN = "nchotomy"
   280 val injectN = "inject"
   281 val exhaustN = "exhaust"
   282 val ctor_injectN = ctorN ^ "_" ^ injectN
   283 val ctor_exhaustN = ctorN ^ "_" ^ exhaustN
   284 val dtor_injectN = dtorN ^ "_" ^ injectN
   285 val dtor_exhaustN = dtorN ^ "_" ^ exhaustN
   286 val ctor_relN = ctorN ^ "_" ^ relN
   287 val dtor_relN = dtorN ^ "_" ^ relN
   288 val ctor_srelN = ctorN ^ "_" ^ srelN
   289 val dtor_srelN = dtorN ^ "_" ^ srelN
   290 val inductN = "induct"
   291 val coinductN = coN ^ inductN
   292 val ctor_inductN = ctorN ^ "_" ^ inductN
   293 val ctor_induct2N = ctor_inductN ^ "2"
   294 val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN
   295 val dtor_coinductN = dtorN ^ "_" ^ coinductN
   296 val dtor_srel_coinductN = dtor_srelN ^ "_" ^ coinductN
   297 val strong_coinductN = "strong_" ^ coinductN
   298 val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strong_coinductN
   299 val dtor_strong_coinductN = dtorN ^ "_" ^ strong_coinductN
   300 val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strong_coinductN
   301 val hsetN = "Hset"
   302 val hset_recN = hsetN ^ "_rec"
   303 val set_inclN = "set_incl"
   304 val ctor_set_inclN = ctorN ^ "_" ^ set_inclN
   305 val dtor_set_inclN = dtorN ^ "_" ^ set_inclN
   306 val set_set_inclN = "set_set_incl"
   307 val ctor_set_set_inclN = ctorN ^ "_" ^ set_set_inclN
   308 val dtor_set_set_inclN = dtorN ^ "_" ^ set_set_inclN
   309 
   310 val caseN = "case"
   311 val discN = "disc"
   312 val disc_unfoldN = discN ^ "_" ^ unfoldN
   313 val disc_corecN = discN ^ "_" ^ corecN
   314 val iffN = "_iff"
   315 val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN
   316 val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
   317 val distinctN = "distinct"
   318 val rel_distinctN = relN ^ "_" ^ distinctN
   319 val injectN = "inject"
   320 val rel_injectN = relN ^ "_" ^ injectN
   321 val selN = "sel"
   322 val sel_unfoldN = selN ^ "_" ^ unfoldN
   323 val sel_corecN = selN ^ "_" ^ corecN
   324 
   325 fun datatype_word lfp = (if lfp then "" else "co") ^ "datatype";
   326 
   327 fun add_components_of_typ (Type (s, Ts)) =
   328     fold add_components_of_typ Ts #> cons (Long_Name.base_name s)
   329   | add_components_of_typ _ = I;
   330 
   331 fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []);
   332 
   333 val mk_common_name = space_implode "_";
   334 
   335 fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
   336 
   337 fun dest_sumTN 1 T = [T]
   338   | dest_sumTN n (Type (@{type_name sum}, [T, T'])) = T :: dest_sumTN (n - 1) T';
   339 
   340 val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT;
   341 
   342 (* TODO: move something like this to "HOLogic"? *)
   343 fun dest_tupleT 0 @{typ unit} = []
   344   | dest_tupleT 1 T = [T]
   345   | dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T';
   346 
   347 val mk_sumTN = Library.foldr1 mk_sumT;
   348 val mk_sumTN_balanced = Balanced_Tree.make mk_sumT;
   349 
   350 fun id_const T = Const (@{const_name id}, T --> T);
   351 
   352 fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
   353 fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
   354 
   355 fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
   356 fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;
   357 
   358 fun mk_InN [_] t 1 = t
   359   | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t
   360   | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1))
   361   | mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t]));
   362 
   363 fun mk_InN_balanced sum_T n t k =
   364   let
   365     fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t
   366       | repair_types T (Const (s as @{const_name Inr}, _) $ t) = repair_inj_types T s snd t
   367       | repair_types _ t = t
   368     and repair_inj_types T s get t =
   369       let val T' = get (dest_sumT T) in
   370         Const (s, T' --> T) $ repair_types T' t
   371       end;
   372   in
   373     Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} n k
   374     |> repair_types sum_T
   375   end;
   376 
   377 fun mk_sum_case (f, g) =
   378   let
   379     val fT = fastype_of f;
   380     val gT = fastype_of g;
   381   in
   382     Const (@{const_name sum_case},
   383       fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g
   384   end;
   385 
   386 val mk_sum_caseN = Library.foldr1 mk_sum_case;
   387 val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case;
   388 
   389 fun mk_If p t f =
   390   let val T = fastype_of t;
   391   in Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ p $ t $ f end;
   392 
   393 fun mk_Field r =
   394   let val T = fst (dest_relT (fastype_of r));
   395   in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end;
   396 
   397 val mk_union = HOLogic.mk_binop @{const_name sup};
   398 
   399 (*dangerous; use with monotonic, converging functions only!*)
   400 fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X);
   401 
   402 fun variant_types ss Ss ctxt =
   403   let
   404     val (tfrees, _) =
   405       fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
   406     val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
   407   in (tfrees, ctxt') end;
   408 
   409 fun variant_tfrees ss =
   410   apfst (map TFree) o variant_types (map (prefix "'") ss) (replicate (length ss) HOLogic.typeS);
   411 
   412 (* stolen from "~~/src/HOL/Tools/Datatype/datatype_aux.ML" *)
   413 fun split_conj_thm th =
   414   ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];
   415 
   416 fun split_conj_prems limit th =
   417   let
   418     fun split n i th =
   419       if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th;
   420   in split limit 1 th end;
   421 
   422 fun mk_sumEN 1 = @{thm one_pointE}
   423   | mk_sumEN 2 = @{thm sumE}
   424   | mk_sumEN n =
   425     (fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
   426       replicate n (impI RS allI);
   427 
   428 fun mk_obj_sumEN_balanced n =
   429   Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
   430     (replicate n asm_rl);
   431 
   432 fun mk_sumEN_balanced' n all_impIs = mk_obj_sumEN_balanced n OF all_impIs RS @{thm obj_one_pointE};
   433 
   434 fun mk_sumEN_balanced 1 = @{thm one_pointE} (*optimization*)
   435   | mk_sumEN_balanced 2 = @{thm sumE} (*optimization*)
   436   | mk_sumEN_balanced n = mk_sumEN_balanced' n (replicate n (impI RS allI));
   437 
   438 fun mk_tupled_allIN 0 = @{thm unit_all_impI}
   439   | mk_tupled_allIN 1 = @{thm impI[THEN allI]}
   440   | mk_tupled_allIN 2 = @{thm prod_all_impI} (*optimization*)
   441   | mk_tupled_allIN n = mk_tupled_allIN (n - 1) RS @{thm prod_all_impI_step};
   442 
   443 fun mk_sumEN_tupled_balanced ms =
   444   let val n = length ms in
   445     if forall (curry (op =) 1) ms then mk_sumEN_balanced n
   446     else mk_sumEN_balanced' n (map mk_tupled_allIN ms)
   447   end;
   448 
   449 fun mk_sum_casesN 1 1 = refl
   450   | mk_sum_casesN _ 1 = @{thm sum.cases(1)}
   451   | mk_sum_casesN 2 2 = @{thm sum.cases(2)}
   452   | mk_sum_casesN n k = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (k - 1)];
   453 
   454 fun mk_sum_step base step thm =
   455   if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm];
   456 
   457 fun mk_sum_casesN_balanced 1 1 = refl
   458   | mk_sum_casesN_balanced n k =
   459     Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)},
   460       right = mk_sum_step @{thm sum.cases(2)} @{thm sum_case_step(2)}, init = refl} n k;
   461 
   462 fun fp_bnf construct_fp bs resBs eqs lthy =
   463   let
   464     val timer = time (Timer.startRealTimer ());
   465     val (lhss, rhss) = split_list eqs;
   466 
   467     (* FIXME: because of "@ lhss", the output could contain type variables that are not in the
   468        input; also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
   469     fun fp_sort Ass =
   470       subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ lhss;
   471 
   472     fun raw_qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
   473 
   474     val ((bnfs, (deadss, livess)), (unfold_set, lthy)) = apfst (apsnd split_list o split_list)
   475       (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort) bs rhss
   476         (empty_unfolds, lthy));
   477 
   478     val name = mk_common_name (map Binding.name_of bs);
   479     fun qualify i =
   480       let val namei = name ^ nonzero_string_of_int i;
   481       in Binding.qualify true namei end;
   482 
   483     val Ass = map (map dest_TFree) livess;
   484     val resDs = fold (subtract (op =)) Ass resBs;
   485     val Ds = fold (fold Term.add_tfreesT) deadss [];
   486 
   487     val _ = (case Library.inter (op =) Ds lhss of [] => ()
   488       | A :: _ => error ("Inadmissible type recursion (cannot take fixed point of dead type \
   489         \variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")"));
   490 
   491     val timer = time (timer "Construction of BNFs");
   492 
   493     val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) =
   494       normalize_bnfs qualify Ass Ds fp_sort bnfs unfold_set lthy;
   495 
   496     val Dss = map3 (append oo map o nth) livess kill_poss deadss;
   497 
   498     val ((pre_bnfs, deadss), lthy'') =
   499       fold_map3 (seal_bnf unfold_set') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy'
   500       |>> split_list;
   501 
   502     val timer = time (timer "Normalization & sealing of BNFs");
   503 
   504     val res = construct_fp bs resBs (map TFree resDs, deadss) pre_bnfs lthy'';
   505 
   506     val timer = time (timer "FP construction in total");
   507   in
   508     timer; (pre_bnfs, res)
   509   end;
   510 
   511 end;