Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@132 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 172 insertions, 98 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index f6c27a8be..6dd6c2177 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -143,7 +143,7 @@ let const_value_cache info c =
   try  
     Some (Hashtbl.find info.i_tab c)
   with Not_found ->
-    match const_abst_opt_value info.i_env c with
+    match const_abst_opt_value info.i_env info.i_evc c with
       | Some body ->
           let v = info.i_repr info body in
           Hashtbl.add info.i_tab c v;
@@ -349,7 +349,7 @@ let rec norm_head info env t stack =
                     reduce_const_body
                       (cbv_norm_more info) (shift_value n v) stack
                 | Inr n -> (VAL(0, Rel n), stack))
-  | DOPN ((Const _ | Abst _) as op, vars)
+  | DOPN ((Const _ | Evar _ | Abst _) as op, vars)
                   when red_allowed info.i_flags stack (DELTA op) ->
       let normt = DOPN(op, Array.map (cbv_norm_term info env) vars) in
       (match const_value_cache info normt with
@@ -751,7 +751,7 @@ and whnf_frterm info ft =
           { norm = uf.norm; term = FLIFT(k, uf) }
       | FOP2 (Cast,f,_) -> whnf_frterm info f  (* remove outer casts *)
       | FOPN (AppL,appl) -> whnf_apply info appl.(0) (array_tl appl)
-      | FOPN ((Const _ | Abst _) as op,vars) ->
+      | FOPN ((Const _ | Evar _ | Abst _) as op,vars) ->
 	  if red_under info.i_flags (DELTA op) then
             let cst = DOPN(op, Array.map term_of_freeze vars) in
             (match const_value_cache info cst with
@@ -818,7 +818,7 @@ and whnf_term info env t =
     | DOP2 (Cast,ct,c) -> whnf_term info env ct    (* remove outer casts *)
     | DOP2 (op,a,b) -> (* Lambda Prod *)
       	{ norm = false; term = FOP2 (op, freeze env a, freeze env b) }
-    | DOPN ((AppL | Const _ | Abst _ | MutCase _) as op, ve) ->
+    | DOPN ((AppL | Const _ | Evar _ | Abst _ | MutCase _) as op, ve) ->
       	whnf_frterm info { norm = false; term = FOPN (op, freeze_vect env ve) }
     | DOPN ((MutInd _ | MutConstruct _) as op,v) ->
       	{ norm = (v=[||]); term = FOPN (op, freeze_vect env v) }
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a983a6759..f715e985a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -199,9 +199,6 @@ let defined_constant env = function
       Constant.is_defined (lookup_constant sp env)
   | _ -> invalid_arg "defined_constant"
 
-(* A const is opaque if it is a non-defined existential or
-   a non-existential opaque constant *)
-
 let opaque_constant env = function
   | DOPN (Const sp, _) -> 
       Constant.is_opaque (lookup_constant sp env)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 0154aa7a9..60139def2 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -49,6 +49,7 @@ let mis_recargs mis =
   Array.map (fun mip -> mip.mind_listrec) mis.mis_mib.mind_packets
 let mis_recarg mis = mis.mis_mip.mind_listrec
 let mis_typename mis = mis.mis_mip.mind_typename
+let mis_consnames mis = mis.mis_mip.mind_consnames
 
 let is_recursive listind = 
   let rec one_is_rec rvec = 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index ceb8fa0de..8140d949d 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -58,6 +58,7 @@ val mis_recarg : mind_specif -> (recarg list) array
 val mis_typename : mind_specif -> identifier
 val is_recursive : int list -> recarg list array -> bool
 val mis_is_recursive : mind_specif -> bool
+val mis_consnames : mind_specif -> identifier array
 
 val mind_nth_type_packet : 
   mutual_inductive_body -> int -> mutual_inductive_packet
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 07c552526..819dfcf84 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -52,14 +52,6 @@ let constant_value env k =
   else 
     failwith "opaque"
 
-let const_abst_opt_value env c =
-  match c with
-    | DOPN(Const sp,_) ->
-	if evaluable_constant env c then Some (constant_value env c) else None
-    | DOPN(Abst sp,_) ->
-	if evaluable_abst env c then Some (abst_value env c) else None
-    | _ -> invalid_arg "const_abst_opt_value"
-
 let mis_lc mis =
   instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps) mis.mis_mip.mind_lc
     (Array.to_list mis.mis_args)
@@ -102,6 +94,19 @@ let existential_value sigma c =
     | Evar_empty ->
 	anomaly "a defined existential with no body"
 
+let const_abst_opt_value env sigma c =
+  match c with
+    | DOPN(Const sp,_) ->
+	if evaluable_constant env c then Some (constant_value env c) else None
+    | DOPN(Evar ev,_) ->
+	if Evd.is_defined sigma ev then 
+	  Some (existential_value sigma c) 
+	else 
+	  None
+    | DOPN(Abst sp,_) ->
+	if evaluable_abst env c then Some (abst_value env c) else None
+    | _ -> invalid_arg "const_abst_opt_value"
+
 let mis_arity' mis =
   let idhyps = ids_of_sign mis.mis_mib.mind_hyps 
   and largs = Array.to_list mis.mis_args in 
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index ba5a072a1..376494884 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -22,7 +22,7 @@ val constant_type : unsafe_env -> constr -> typed_type
 val existential_value : 'a evar_map -> constr -> constr
 val existential_type : 'a evar_map -> constr -> constr
 
-val const_abst_opt_value : unsafe_env -> constr -> constr option
+val const_abst_opt_value : unsafe_env -> 'a evar_map -> constr -> constr option
 
 val mis_arity : mind_specif -> constr
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 0d4557efc..bc4021fbf 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -100,93 +100,31 @@ let red_product env sigma c =
     match x with
       | DOPN(AppL,cl) -> 
 	  DOPN(AppL,Array.append [|redrec (array_hd cl)|] (array_tl cl))
-      | DOPN(Const _,_) when evaluable_constant env x -> constant_value env x
-      | DOPN(Abst _,_) when evaluable_abst env x -> abst_value env x 
+      | DOPN(Const _,_) when evaluable_constant env x -> 
+	  constant_value env x
+      | DOPN(Evar ev,_) when Evd.is_defined sigma ev -> 
+	  existential_value sigma x
+      | DOPN(Abst _,_) when evaluable_abst env x -> 
+	  abst_value env x 
       | DOP2(Cast,c,_) -> redrec c
       | DOP2(Prod,a,DLAM(x,b)) -> DOP2(Prod, a, DLAM(x, redrec b))  
       | _ -> error "Term not reducible"
   in 
   nf_betaiota env sigma (redrec c)
 
-
-(* Substitute only a list of locations locs, the empty list is interpreted
-   as substitute all, if 0 is in the list then no substitution is done 
-   the list may contain only negative occurrences that will not be substituted *)
-(* Aurait sa place dans term.ml mais term.ml ne connait pas printer.ml *)
-let subst_term_occ locs c t = 
-  let rec substcheck except k occ c t =
-    if except or List.exists (function u -> u>=occ) locs then
-      substrec except k occ c t
-    else 
-      (occ,t)
-  and substrec except k occ c t =
-    if eq_constr t c then
-      if except then 
-	if List.mem (-occ) locs then (occ+1,t) else (occ+1,Rel(k))
-      else 
-	if List.mem occ locs then (occ+1,Rel(k)) else  (occ+1,t)
-    else 
-      match t with
-	| DOPN(Const sp,tl) -> occ,t
-	|  DOPN(MutConstruct _,tl) -> occ,t
-	|  DOPN(MutInd _,tl) -> occ,t
-	|  DOPN(i,cl) -> 
-	     let (occ',cl') =   
-               Array.fold_left 
-		 (fun (nocc',lfd) f ->
-		    let (nocc'',f') = substcheck except k nocc' c f in
-                    (nocc'',f'::lfd)) 
-		 (occ,[]) cl
-             in 
-	     (occ',DOPN(i,Array.of_list (List.rev cl')))
-	|  DOP2(i,t1,t2) -> 
-	     let (nocc1,t1')=substrec except k occ c t1 in
-             let (nocc2,t2')=substcheck except k nocc1 c t2 in
-             nocc2,DOP2(i,t1',t2')
-	|  DOP1(i,t) -> 
-	     let (nocc,t')= substrec except k occ c t in
-	     nocc,DOP1(i,t')
-	|  DLAM(n,t) -> 
-	     let (occ',t') = substcheck except (k+1) occ (lift 1 c) t in
-             (occ',DLAM(n,t'))
-	|  DLAMV(n,cl) -> 
-	     let (occ',cl') =   
-               Array.fold_left 
-		 (fun (nocc',lfd) f ->
-		    let (nocc'',f') = 
-		      substcheck except (k+1) nocc' (lift 1 c) f
-                    in (nocc'',f'::lfd)) 
-		 (occ,[]) cl
-             in 
-	     (occ',DLAMV(n,Array.of_list (List.rev cl') ))
-	|  _ -> occ,t
-  in 
-  if locs = [] then 
-    subst_term c t
-  else if List.mem 0 locs then 
-    t
-  else 
-    let except = List.for_all (fun n -> n<0) locs in
-    let (nbocc,t') = substcheck except 1 1 c t in
-    if List.exists (fun o -> o >= nbocc or o <= -nbocc) locs then
-      failwith "subst_term_occ: too few occurences" 
-    else 
-      t'
-
 (* linear substitution (following pretty-printer) of the value of name in c.
  * n is the number of the next occurence of name.
  * ol is the occurence list to find. *)
 let rec substlin env name n ol c =
   match c with
     | DOPN(Const sp,_) ->
-        if path_of_const c = name then
+        if sp = name then
           if List.hd ol = n then
             if evaluable_constant env c then 
-	      ((n+1),(List.tl ol), constant_value env c)
+	      (n+1, List.tl ol, constant_value env c)
             else
               errorlabstrm "substlin"
-                [< 'sTR(string_of_path sp);
-                   'sTR " is not a defined constant" >]
+                [< print_sp sp; 'sTR " is not a defined constant" >]
           else 
 	    ((n+1),ol,c)
         else 
@@ -195,13 +133,13 @@ let rec substlin env name n ol c =
     | DOPN(Abst _,_) ->
         if path_of_abst c = name then
           if List.hd ol = n then 
-	    ((n+1),(List.tl ol), abst_value env c)
+	    (n+1, List.tl ol, abst_value env c)
           else 
-	    ((n+1),ol,c)
+	    (n+1,ol,c)
         else 
 	  (n,ol,c)
 
-(* INEFFICIENT: OPTIMIZE *)
+    (* INEFFICIENT: OPTIMIZE *)
     | DOPN(AppL,tl) ->
         let c1 = array_hd tl and cl = array_tl tl in
         Array.fold_left 
@@ -394,6 +332,11 @@ let whd_delta_stack env sigma =
             whrec (constant_value env c) l
 	  else 
 	    x,l
+      | DOPN(Evar ev,_) as c ->
+	  if Evd.is_defined sigma ev then
+            whrec (existential_value sigma c) l
+	  else 
+	    x,l
       | (DOPN(Abst _,_)) as c ->
 	  if evaluable_abst env c then
             whrec (abst_value env c) l
@@ -416,6 +359,11 @@ let whd_betadelta_stack env sigma =
 	    whrec (constant_value env x) l
           else 
 	    (x,l)
+      | DOPN(Evar ev,_) ->
+          if Evd.is_defined sigma ev then 
+	    whrec (existential_value sigma x) l
+          else 
+	    (x,l)
       | DOPN(Abst _,_) ->
           if evaluable_abst env x then 
 	    whrec (abst_value env x) l
@@ -442,6 +390,11 @@ let whd_betadeltat_stack env sigma =
 	    whrec (constant_value env x) l
           else 
 	    (x,l)
+      | DOPN(Evar ev,_) ->
+          if Evd.is_defined sigma ev then 
+	    whrec (existential_value sigma x) l
+          else 
+	    (x,l)
       | DOPN(Abst _,_) ->
           if translucent_abst env x then 
 	    whrec (abst_value env x) l
@@ -467,6 +420,11 @@ let whd_betadeltaeta_stack env sigma =
 	    whrec (constant_value env x) stack
           else 
 	    (x,stack)
+      | DOPN(Evar ev,_) ->
+          if Evd.is_defined sigma ev then 
+	    whrec (existential_value sigma x) stack
+          else 
+	    (x,stack)
       | DOPN(Abst _,_) ->
           if evaluable_abst env x then
 	    whrec (abst_value env x) stack
@@ -611,6 +569,11 @@ let whd_betadeltatiota_stack env sigma =
             whrec (constant_value env x) stack
           else 
 	    (x,stack)
+      | DOPN(Evar ev,_) ->
+          if Evd.is_defined sigma ev then 
+	    whrec (existential_value sigma x) stack
+          else 
+	    (x,stack)
       | DOPN(Abst _,_) ->
           if translucent_abst env x then
 	    whrec (abst_value env x) stack
@@ -648,6 +611,11 @@ let whd_betadeltaiota_stack env sigma =
 	    bdi_rec (constant_value env x) stack
           else 
 	    (x,stack)
+      | DOPN(Evar ev,_) ->
+          if Evd.is_defined sigma ev then 
+	    bdi_rec (existential_value sigma x) stack
+          else 
+	    (x,stack)
       | DOPN(Abst _,_) ->
           if evaluable_abst env x then 
 	    bdi_rec (abst_value env x) stack 
@@ -686,6 +654,11 @@ let whd_betadeltaiotaeta_stack env sigma =
 	    whrec (constant_value env x) stack
           else 
 	    (x,stack)
+      | DOPN(Evar ev,_) ->
+          if Evd.is_defined sigma ev then 
+	    whrec (existential_value sigma x) stack
+          else 
+	    (x,stack)
       | DOPN(Abst _,_) ->
           if evaluable_abst env x then
 	    whrec (abst_value env x) stack
@@ -815,18 +788,19 @@ and eqappr cv_pb infos appr1 appr2 =
 	  (reloc_rel n el1 = reloc_rel m el2)
           (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
 
-    | (FOP0(Meta(n)), FOP0(Meta(m))) ->
+    | (FOP0(Meta n), FOP0(Meta m)) ->
         bool_and_convert (n=m) 
 	  (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
 
-    (* 2 constants or 2 abstractions *)
+    (* 2 constants, 2 existentials or 2 abstractions *)
     | (FOPN(Const sp1,al1), FOPN(Const sp2,al2)) ->
 	convert_or
 	  (* try first intensional equality *)
 	  (bool_and_convert (sp1 == sp2 or sp1 = sp2)
 	     (convert_and
 		(convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2)
-		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)))
+		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
+		   v1 v2)))
           (* else expand the second occurrence (arbitrary heuristic) *)
           (match search_frozen_cst infos (Const sp2) al2 with
              | Some def2 -> 
@@ -836,13 +810,31 @@ and eqappr cv_pb infos appr1 appr2 =
 				(lft1, fhnf_apply infos n1 def1 v1) appr2
 			  | None -> fun _ -> raise NotConvertible))
 
+    | (FOPN(Evar ev1,al1), FOPN(Evar ev2,al2)) ->
+	convert_or
+	  (* try first intensional equality *)
+	  (bool_and_convert (ev1 == ev2)
+	     (convert_and
+		(convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2)
+		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
+		   v1 v2)))
+          (* else expand the second occurrence (arbitrary heuristic) *)
+          (match search_frozen_cst infos (Evar ev2) al2 with
+             | Some def2 -> 
+		 eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2)
+             | None -> (match search_frozen_cst infos (Evar ev1) al1 with
+                          | Some def1 -> eqappr cv_pb infos
+				(lft1, fhnf_apply infos n1 def1 v1) appr2
+			  | None -> fun _ -> raise NotConvertible))
+
     | (FOPN(Abst sp1,al1), FOPN(Abst sp2,al2)) ->
 	convert_or
 	  (* try first intensional equality *)
           (bool_and_convert  (sp1 = sp2)
 	     (convert_and
 		(convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2)
-		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)))
+		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
+		   v1 v2)))
           (* else expand the second occurrence (arbitrary heuristic) *)
           (match search_frozen_cst infos (Abst sp2) al2 with
              | Some def2 -> 
@@ -852,14 +844,14 @@ and eqappr cv_pb infos appr1 appr2 =
 				(lft1, fhnf_apply infos n1 def1 v1) appr2
 			  | None -> fun _ -> raise NotConvertible))
 
-    (* only one constant or abstraction *)
-    | (FOPN((Const _ | Abst _) as op,al1), _)      ->
+    (* only one constant, existential or abstraction *)
+    | (FOPN((Const _ | Evar _ | Abst _) as op,al1), _)      ->
         (match search_frozen_cst infos op al1 with
            | Some def1 -> 
 	       eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2
            | None -> fun _ -> raise NotConvertible)
 
-    | (_, FOPN((Const _ | Abst _) as op,al2))      ->
+    | (_, FOPN((Const _ | Evar _ | Abst _) as op,al2))      ->
         (match search_frozen_cst infos op al2 with
            | Some def2 -> 
 	       eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 1ff259e01..67ad99f55 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -122,7 +122,6 @@ val unfoldn :
   (int list * section_path) list -> 'a reduction_function
 val fold_one_com : constr -> 'a reduction_function
 val fold_commands : constr list -> 'a reduction_function
-val subst_term_occ : int list -> constr -> constr -> constr
 val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
 val compute : 'a reduction_function
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 543c41baa..72d6cfbd2 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1139,6 +1139,71 @@ let rec subst_meta bl c =
     | DOP2(op,c'1, c'2) -> DOP2(op, subst_meta bl c'1, subst_meta bl c'2)
     | DOPN(op, c') -> DOPN(op, Array.map (subst_meta bl) c')
     | _ -> c
+
+(* Substitute only a list of locations locs, the empty list is
+   interpreted as substitute all, if 0 is in the list then no
+   substitution is done the list may contain only negative occurrences
+   that will not be substituted. *)
+
+let subst_term_occ locs c t = 
+  let rec substcheck except k occ c t =
+    if except or List.exists (function u -> u>=occ) locs then
+      substrec except k occ c t
+    else 
+      (occ,t)
+  and substrec except k occ c t =
+    if eq_constr t c then
+      if except then 
+	if List.mem (-occ) locs then (occ+1,t) else (occ+1,Rel(k))
+      else 
+	if List.mem occ locs then (occ+1,Rel(k)) else  (occ+1,t)
+    else 
+      match t with
+	| DOPN(Const sp,tl) -> occ,t
+	|  DOPN(MutConstruct _,tl) -> occ,t
+	|  DOPN(MutInd _,tl) -> occ,t
+	|  DOPN(i,cl) -> 
+	     let (occ',cl') =   
+               Array.fold_left 
+		 (fun (nocc',lfd) f ->
+		    let (nocc'',f') = substcheck except k nocc' c f in
+                    (nocc'',f'::lfd)) 
+		 (occ,[]) cl
+             in 
+	     (occ',DOPN(i,Array.of_list (List.rev cl')))
+	|  DOP2(i,t1,t2) -> 
+	     let (nocc1,t1')=substrec except k occ c t1 in
+             let (nocc2,t2')=substcheck except k nocc1 c t2 in
+             nocc2,DOP2(i,t1',t2')
+	|  DOP1(i,t) -> 
+	     let (nocc,t')= substrec except k occ c t in
+	     nocc,DOP1(i,t')
+	|  DLAM(n,t) -> 
+	     let (occ',t') = substcheck except (k+1) occ (lift 1 c) t in
+             (occ',DLAM(n,t'))
+	|  DLAMV(n,cl) -> 
+	     let (occ',cl') =   
+               Array.fold_left 
+		 (fun (nocc',lfd) f ->
+		    let (nocc'',f') = 
+		      substcheck except (k+1) nocc' (lift 1 c) f
+                    in (nocc'',f'::lfd)) 
+		 (occ,[]) cl
+             in 
+	     (occ',DLAMV(n,Array.of_list (List.rev cl') ))
+	|  _ -> occ,t
+  in 
+  if locs = [] then 
+    subst_term c t
+  else if List.mem 0 locs then 
+    t
+  else 
+    let except = List.for_all (fun n -> n<0) locs in
+    let (nbocc,t') = substcheck except 1 1 c t in
+    if List.exists (fun o -> o >= nbocc or o <= -nbocc) locs then
+      failwith "subst_term_occ: too few occurences";
+    t'
+
   
 (***************************)
 (* occurs check functions  *)                         
@@ -1154,6 +1219,18 @@ let rec occur_meta = function
 
 let rel_vect = (Generic.rel_vect : int -> int -> constr array)
 		 
+let occur_existential = 
+  let rec occrec = function
+    | DOPN(Evar _,_) -> true
+    | DOPN(_,cl) -> array_exists occrec cl
+    | DOPL(_,cl) -> List.exists occrec cl
+    | DOP2(_,c1,c2) -> occrec c1 or occrec c2
+    | DOP1(_,c) -> occrec c
+    | DLAM(_,c) -> occrec c
+    | DLAMV(_,cl) -> array_exists occrec cl
+    | _ -> false
+  in 
+  occrec
 
 (***************************)
 (* hash-consing functions  *)                         
diff --git a/kernel/term.mli b/kernel/term.mli
index 823917ea5..5118d39c5 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -474,6 +474,7 @@ val sort_hdchar : sorts -> string
 (*s Occur check functions. *)                         
 
 val occur_meta : constr -> bool
+val occur_existential : constr -> bool
 val rel_vect : int -> int -> constr array
 
 (* [(occur_const (s:section_path) c)] returns [true] if constant [s] occurs 
@@ -492,6 +493,7 @@ val subst_term : constr -> constr -> constr
 val subst_term_eta_eq : constr -> constr -> constr
 val replace_consts :
   (section_path * (identifier list * constr) option) list -> constr -> constr
+val subst_term_occ : int list -> constr -> constr -> constr
 
 (* [subst_meta bl c] substitutes the metavar $i$ by $c_i$ in [c] 
    for each binding $(i,c_i)$ in [bl],