<commit_before>open Printer
open Pp
open Names
open Term
open Vars
open Glob_term
open Glob_ops
open Globnames
open Indfun_common
open Errors
open Util
open Glob_termops
open Misctypes

let observe strm =
  if do_observe ()
  then Pp.msg_debug strm
  else ()
(*let observennl strm =
  if do_observe ()
  then Pp.msg strm
  else ()*)


type binder_type =
  | Lambda of Name.t
  | Prod of Name.t
  | LetIn of Name.t

type glob_context = (binder_type*glob_constr) list

(*
   compose_glob_context [(bt_1,n_1,t_1);......] rt returns
   b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the
   binders corresponding to the bt_i's
*)
let compose_glob_context =
  let compose_binder  (bt,t) acc =
    match bt with
      | Lambda n -> mkGLambda(n,t,acc)
      | Prod n -> mkGProd(n,t,acc)
      | LetIn n -> mkGLetIn(n,t,acc)
  in
  List.fold_right compose_binder


(*
   The main part deals with building a list of globalized constructor expressions
   from the rhs of a fixpoint equation.
*)

type 'a build_entry_pre_return =
    {
      context : glob_context;  (* the binding context of the result *)
      value : 'a; (* The value *)
    }

type 'a build_entry_return =
    {
      result : 'a build_entry_pre_return list;
      to_avoid : Id.t list
    }

(*
  [combine_results combine_fun res1 res2] combine two results [res1] and [res2]
  w.r.t. [combine_fun].

  Informally, both [res1] and [res2] are lists of "constructors"  [res1_1;...]
  and [res2_1,....] and we need to produce
  [combine_fun res1_1 res2_1;combine_fun res1_1 res2_2;........]
*)

let combine_results
    (combine_fun : 'a build_entry_pre_return -> 'b build_entry_pre_return ->
      'c build_entry_pre_return
    )
    (res1: 'a build_entry_return)
    (res2 : 'b build_entry_return)
    : 'c build_entry_return
    =
  let pre_result =     List.map
    ( fun res1 ->  (* for each result in arg_res *)
	  List.map (* we add it in each args_res *)
	    (fun res2 ->
	       combine_fun res1 res2
	    )
	    res2.result
      )
      res1.result
  in (* and then we flatten the map *)
  {
    result = List.concat pre_result;
    to_avoid = List.union Id.equal res1.to_avoid res2.to_avoid
  }


(*
   The combination function for an argument with a list of argument
*)

let combine_args arg args =
  {
    context = arg.context@args.context;
    (* Note that the binding context of [arg] MUST be placed before the one of
       [args] in order to preserve possible type dependencies
    *)
    value = arg.value::args.value;
  }


let ids_of_binder =  function
  | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> []
  | LetIn (Name id)  | Prod (Name id) | Lambda (Name id) -> [id]

let rec change_vars_in_binder mapping = function
    [] -> []
  | (bt,t)::l ->
      let new_mapping = List.fold_right Id.Map.remove (ids_of_binder bt) mapping in
      (bt,change_vars mapping t)::
	(if Id.Map.is_empty new_mapping
	 then l
	 else change_vars_in_binder new_mapping l
	)

let rec replace_var_by_term_in_binder x_id term = function
  | [] -> []
  | (bt,t)::l ->
      (bt,replace_var_by_term x_id term t)::
	if Id.List.mem x_id (ids_of_binder bt)
	then l
	else replace_var_by_term_in_binder x_id term l

let add_bt_names bt = List.append (ids_of_binder bt)

let apply_args ctxt body args =
  let need_convert_id avoid id =
    List.exists (is_free_in id) args || Id.List.mem id avoid
  in
  let need_convert avoid  bt =
    List.exists (need_convert_id avoid) (ids_of_binder bt)
  in
  let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) =
    match na with
       | Name id when Id.List.mem id avoid ->
	   let new_id = Namegen.next_ident_away id avoid in
	   Name new_id,Id.Map.add id new_id mapping,new_id::avoid
       | _ -> na,mapping,avoid
  in
  let next_bt_away bt (avoid:Id.t list) =
    match bt with
      | LetIn na ->
	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
	  LetIn new_na,mapping,new_avoid
      | Prod na ->
	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
	  Prod new_na,mapping,new_avoid
      | Lambda na ->
	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
	  Lambda new_na,mapping,new_avoid
  in
  let rec do_apply avoid ctxt body args =
    match ctxt,args with
      | _,[] -> (* No more args *)
	  (ctxt,body)
      | [],_ -> (* no more fun *)
	  let f,args' = glob_decompose_app body in
	  (ctxt,mkGApp(f,args'@args))
      | (Lambda Anonymous,t)::ctxt',arg::args' ->
	  do_apply avoid ctxt' body args'
      | (Lambda (Name id),t)::ctxt',arg::args' ->
	  let new_avoid,new_ctxt',new_body,new_id =
	    if need_convert_id avoid id
	    then
	      let new_avoid =  id::avoid in
	      let new_id = Namegen.next_ident_away id new_avoid in
	      let new_avoid' = new_id :: new_avoid in
	      let mapping = Id.Map.add id new_id Id.Map.empty in
	      let new_ctxt' = change_vars_in_binder mapping ctxt' in
	      let new_body = change_vars mapping body in
	      new_avoid',new_ctxt',new_body,new_id
	    else
	      id::avoid,ctxt',body,id
	  in
	  let new_body = replace_var_by_term new_id arg new_body in
	  let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
	  do_apply avoid new_ctxt' new_body args'
      | (bt,t)::ctxt',_ ->
	  let new_avoid,new_ctxt',new_body,new_bt =
	    let new_avoid = add_bt_names bt avoid in
	    if need_convert avoid bt
	    then
	      let new_bt,mapping,new_avoid = next_bt_away bt new_avoid in
	      (
		new_avoid,
		change_vars_in_binder mapping ctxt',
		change_vars mapping body,
		new_bt
	     )
	    else new_avoid,ctxt',body,bt
	  in
	  let new_ctxt',new_body =
	    do_apply new_avoid new_ctxt' new_body args
	  in
	  (new_bt,t)::new_ctxt',new_body
  in
  do_apply []  ctxt body args


let combine_app f args =
  let new_ctxt,new_value = apply_args f.context f.value args.value in
  {
    (* Note that the binding context of [args] MUST be placed before the one of
       the applied value in order to preserve possible type dependencies
    *)
      context = args.context@new_ctxt;
      value = new_value;
  }

let combine_lam n t b =
  {
    context = [];
    value = mkGLambda(n, compose_glob_context t.context t.value,
		      compose_glob_context b.context b.value )
  }



let combine_prod n t b =
  { context = t.context@((Prod n,t.value)::b.context); value = b.value}

let combine_letin n t b =
  { context = t.context@((LetIn n,t.value)::b.context); value = b.value}


let mk_result ctxt value avoid =
  {
    result =
      [{context = ctxt;
	value = value}]
	;
    to_avoid = avoid
  }
(*************************************************
  Some functions to deal with overlapping patterns
**************************************************)

let coq_True_ref =
  lazy  (Coqlib.gen_reference "" ["Init";"Logic"] "True")

let coq_False_ref =
  lazy  (Coqlib.gen_reference "" ["Init";"Logic"] "False")

(*
  [make_discr_match_el \[e1,...en\]] builds match e1,...,en with
  (the list of expressions on which we will do the matching)
 *)
let make_discr_match_el  =
  List.map (fun e -> (e,(Anonymous,None)))

(*
  [make_discr_match_brl i \[pat_1,...,pat_n\]]  constructs a discrimination pattern matching on the ith expression.
  that is.
  match ?????? with \\
  | pat_1 => False  \\
  | pat_{i-1} => False \\
  | pat_i => True \\
  | pat_{i+1} => False \\
  \vdots
  | pat_n => False
  end
*)
let make_discr_match_brl i =
  List.map_i
    (fun j (_,idl,patl,_) ->
       if Int.equal j i
       then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref))
       else (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_False_ref))
    )
    0
(*
   [make_discr_match brl el i] generates an hypothesis such that it reduce to true iff
   brl_{i} is the first branch matched by [el]

   Used when we want to simulate the coq pattern matching algorithm
*)
let make_discr_match brl =
  fun el i ->
  mkGCases(None,
	   make_discr_match_el el,
	   make_discr_match_brl i brl)

(**********************************************************************)
(*  functions used to build case expression from lettuple and if ones *)
(**********************************************************************)

(* [build_constructors_of_type] construct the array of pattern of its inductive argument*)
let build_constructors_of_type ind' argl =
  let (mib,ind) = Inductive.lookup_mind_specif (Global.env()) ind' in
  let npar = mib.Declarations.mind_nparams in
  Array.mapi (fun i _ ->
		let construct = ind',i+1 in
		let constructref = ConstructRef(construct) in
		let _implicit_positions_of_cst =
		  Impargs.implicits_of_global constructref
		in
		let cst_narg =
		  Inductiveops.constructor_nallargs_env
		    (Global.env ())
		    construct
		in
		let argl =
		  if List.is_empty argl
		  then
 		    Array.to_list
		      (Array.init (cst_narg - npar) (fun _ -> mkGHole ())
		      )
		  else argl
		in
		let pat_as_term =
		  mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
		in
		cases_pattern_of_glob_constr Anonymous pat_as_term
	     )
    ind.Declarations.mind_consnames

(******************)
(* Main functions *)
(******************)



let raw_push_named (na,raw_value,raw_typ) env =
  match na with
    | Anonymous -> env
    | Name id ->
	let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in
	let typ,ctx = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
	Environ.push_named (id,value,typ) env


let add_pat_variables pat typ env : Environ.env =
  let rec add_pat_variables env pat typ  : Environ.env =
    observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));

    match pat with
      | PatVar(_,na) -> Environ.push_rel (na,None,typ) env
      | PatCstr(_,c,patl,na) ->
	  let Inductiveops.IndType(indf,indargs) =
	    try Inductiveops.find_rectype env (Evd.from_env env) typ
	    with Not_found -> assert false
	  in
	  let constructors = Inductiveops.get_constructors env indf in
	  let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in
	  let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
	  List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
  in
  let new_env = add_pat_variables  env pat typ in
  let res =
    fst (
      Context.fold_rel_context
	(fun (na,v,t) (env,ctxt) ->
	 match na with
	   | Anonymous -> assert false
	   | Name id ->
	       let new_t =  substl ctxt t in
	       let new_v = Option.map (substl ctxt) v in
	       observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
			  str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
			  str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
			  Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
			  Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
		       );
	       (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt)
      )
	(Environ.rel_context new_env)
	~init:(env,[])
    )
  in
  observe (str "new var env := " ++ Printer.pr_named_context_of res (Evd.from_env env));
  res




let rec pattern_to_term_and_type env typ  = function
  | PatVar(loc,Anonymous) -> assert false
  | PatVar(loc,Name id) ->
	mkGVar id
  | PatCstr(loc,constr,patternl,_) ->
      let cst_narg =
	Inductiveops.constructor_nallargs_env
	  (Global.env ())
	  constr
      in
      let Inductiveops.IndType(indf,indargs) =
	try Inductiveops.find_rectype env (Evd.from_env env) typ
	with Not_found -> assert false
      in
      let constructors = Inductiveops.get_constructors env indf in
      let constructor  = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in
      let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
      let _,cstl = Inductiveops.dest_ind_family indf in
      let csta = Array.of_list cstl in
      let implicit_args =
	Array.to_list
	  (Array.init
	     (cst_narg - List.length patternl)
	     (fun i -> Detyping.detype false [] env (Evd.from_env env) csta.(i))
	  )
      in
      let patl_as_term =
	List.map2 (pattern_to_term_and_type env)  (List.rev cs_args_types)  patternl
      in
      mkGApp(mkGRef(ConstructRef constr),
	     implicit_args@patl_as_term
	    )

(* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return)
   of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the
   corresponding graphs.


   The idea to transform a term [t] into a list of constructors [lc] is the following:
   \begin{itemize}
   \item if the term is a binder (bind x, body) then first compute [lc'] the list corresponding
   to [body] and add (bind x. _) to each elements of [lc]
   \item if the term has the form (g t1 ... ... tn) where g does not appears in (fnames)
   then compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn],
   then combine those lists and [g] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn],
   [g c1 ... cn] is an element of [lc]
   \item if the term has the form (f t1 .... tn) where [f] appears in [fnames] then
   compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn],
   then compute those lists and [f] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn]
   create a new variable [res] and [forall res, R_f c1 ... cn res] is in [lc]
   \item if the term is a cast just treat its body part
   \item
   if the term is a match, an if or a lettuple then compute the lists corresponding to each branch of the case
   and concatenate them (informally, each branch of a match produces a new constructor)
   \end{itemize}

   WARNING: The terms constructed here are only USING the glob_constr syntax but are highly bad formed.
   We must wait to have complete all the current calculi to set the recursive calls.
   At this point, each term [f t1 ... tn]  (where f appears in [funnames]) is replaced by
   a pseudo term [forall res, res t1 ... tn, res]. A reconstruction phase is done later.
   We in fact not create a constructor list since then end of each constructor has not the expected form
   but only the value of the function
*)


let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
  observe (str " Entering : " ++ Printer.pr_glob_constr rt);
  match rt with
    | GRef _ | GVar _ | GEvar _ | GPatVar _     | GSort _  | GHole _  ->
	(* do nothing (except changing type of course) *)
	mk_result [] rt avoid
    | GApp(_,_,_) ->
	let f,args = glob_decompose_app rt in
	let args_res : (glob_constr list) build_entry_return =
	  List.fold_right (* create the arguments lists of constructors and combine them *)
	    (fun arg ctxt_argsl ->
	       let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in
	       combine_results combine_args arg_res ctxt_argsl
	    )
	    args
	    (mk_result [] [] avoid)
	in
	begin
	  match f with
	    | GLambda _  -> 
		let rec aux t l = 
		  match l with 
		    | [] -> t
		    | u::l -> 
			match t with 
			  | GLambda(loc,na,_,nat,b) -> 
			      GLetIn(Loc.ghost,na,u,aux b l)
			  | _ -> 
			      GApp(Loc.ghost,t,l)
		in
		build_entry_lc env funnames avoid (aux f args)
	    | GVar(_,id) when Id.Set.mem id funnames ->
		(* if we have [f t1 ... tn] with [f]$\in$[fnames]
		   then we create a fresh variable [res],
		   add [res] and its "value" (i.e. [res v1 ... vn]) to each
		   pseudo constructor build for the arguments (i.e. a pseudo context [ctxt] and
		   a pseudo value "v1 ... vn".
		   The "value" of this branch is then simply [res]
		*)
		let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
		let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in
		let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in
		let res = fresh_id args_res.to_avoid "_res" in
		let new_avoid = res::args_res.to_avoid in
		let res_rt = mkGVar res in
		let new_result =
		  List.map
		    (fun arg_res ->
		       let new_hyps =
			 [Prod (Name res),res_raw_type;
			  Prod Anonymous,mkGApp(res_rt,(mkGVar id)::arg_res.value)]
		       in
		       {context =  arg_res.context@new_hyps; value = res_rt }
		    )
		    args_res.result
		in
		{ result = new_result; to_avoid = new_avoid }
	    | GVar _ | GEvar _ | GPatVar _ | GHole _ | GSort _ | GRef _ ->
		(* if have [g t1 ... tn] with [g] not appearing in [funnames]
		   then
		   foreach [ctxt,v1 ... vn] in [args_res] we return
		   [ctxt, g v1 .... vn]
		*)
		{
		  args_res with
		    result =
		    List.map
		      (fun args_res ->
			 {args_res with value = mkGApp(f,args_res.value)})
		      args_res.result
		}
	    | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *)
       	    | GLetIn(_,n,t,b) ->
		(* if we have [(let x := v in b) t1 ... tn] ,
		   we discard our work and compute the list of constructor for
		   [let x = v in (b t1 ... tn)] up to alpha conversion
		*)
		let new_n,new_b,new_avoid =
		  match n with
		    | Name id when List.exists (is_free_in id) args ->
			(* need to alpha-convert the name *)
			let new_id = Namegen.next_ident_away id avoid in
			let new_avoid = id:: avoid in
			let new_b =
			  replace_var_by_term
			    id
			    (GVar(Loc.ghost,id))
			    b
			in
			(Name new_id,new_b,new_avoid)
		    | _ -> n,b,avoid
		in
		build_entry_lc
		  env
		  funnames
		  avoid
		  (mkGLetIn(new_n,t,mkGApp(new_b,args)))
	    | GCases _  | GIf _ | GLetTuple _ ->
		(* we have [(match e1, ...., en with ..... end) t1 tn]
		   we first compute the result from the case and
		   then combine each of them with each of args one
		*)
		let f_res = build_entry_lc env funnames args_res.to_avoid f in
		combine_results combine_app f_res  args_res
	    | GCast(_,b,_) ->
		(* for an applied cast we just trash the cast part
		   and restart the work.

		   WARNING: We need to restart since [b] itself should be an application term
		*)
		build_entry_lc env funnames avoid (mkGApp(b,args))
	    | GRec _ -> error "Not handled GRec"
	    | GProd _ -> error "Cannot apply a type"
	end (* end of the application treatement *)

    | GLambda(_,n,_,t,b) ->
	(* we first compute the list of constructor
	   corresponding to the body of the function,
	   then the one corresponding to the type
	   and combine the two result
	*)
	let t_res = build_entry_lc env funnames avoid t  in
	let new_n =
	  match n with
	    | Name _ -> n
	    | Anonymous -> Name (Indfun_common.fresh_id [] "_x")
	in
	let new_env = raw_push_named (new_n,None,t) env in
	let b_res = build_entry_lc new_env funnames avoid b in
	combine_results (combine_lam new_n) t_res b_res
    | GProd(_,n,_,t,b) ->
	(* we first compute the list of constructor
	   corresponding to the body of the function,
	   then the one corresponding to the type
	   and combine the two result
	*)
	let t_res = build_entry_lc env funnames avoid t in
	let new_env = raw_push_named (n,None,t) env in
	let b_res = build_entry_lc new_env funnames avoid b in
	combine_results (combine_prod n) t_res b_res
    | GLetIn(_,n,v,b) ->
	(* we first compute the list of constructor
	   corresponding to the body of the function,
	   then the one corresponding to the value [t]
	   and combine the two result
	*)
	let v_res = build_entry_lc env funnames avoid v in
	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
	let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
	let new_env =
	  match n with
	      Anonymous -> env
	    | Name id -> Environ.push_named (id,Some v_as_constr,v_type) env
	in
	let b_res = build_entry_lc new_env funnames avoid b in
	combine_results (combine_letin n) v_res b_res
    | GCases(_,_,_,el,brl) ->
	(* we create the discrimination function
	   and treat the case itself
	*)
	let make_discr = make_discr_match brl in
	build_entry_lc_from_case env funnames make_discr el brl avoid
    | GIf(_,b,(na,e_option),lhs,rhs) ->
	let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
	let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
	let (ind,_) =
	  try Inductiveops.find_inductive env (Evd.from_env env) b_typ
	  with Not_found ->
	    errorlabstrm "" (str "Cannot find the inductive associated to " ++
			       Printer.pr_glob_constr b ++ str " in " ++
			       Printer.pr_glob_constr rt ++ str ". try again with a cast")
	in
	let case_pats = build_constructors_of_type (fst ind) [] in
	assert (Int.equal (Array.length case_pats) 2);
	let brl =
	  List.map_i
	    (fun i x -> (Loc.ghost,[],[case_pats.(i)],x))
	    0
	    [lhs;rhs]
	in
	let match_expr =
	  mkGCases(None,[(b,(Anonymous,None))],brl)
	in
	(* 		Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *)
	build_entry_lc env funnames avoid match_expr
    | GLetTuple(_,nal,_,b,e) ->
	begin
	  let nal_as_glob_constr =
	    List.map
	      (function
		   Name id -> mkGVar id
		 | Anonymous -> mkGHole ()
	      )
	      nal
	  in
	  let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
	  let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
	  let (ind,_) =
	    try Inductiveops.find_inductive env (Evd.from_env env) b_typ
	    with Not_found ->
	      errorlabstrm "" (str "Cannot find the inductive associated to " ++
				 Printer.pr_glob_constr b ++ str " in " ++
				 Printer.pr_glob_constr rt ++ str ". try again with a cast")
	  in
	  let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
	  assert (Int.equal (Array.length case_pats) 1);
	  let br =
	    (Loc.ghost,[],[case_pats.(0)],e)
	  in
	  let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in
	  build_entry_lc env funnames avoid match_expr

	end
    | GRec _ -> error "Not handled GRec"
    | GCast(_,b,_) ->
	build_entry_lc env funnames  avoid b
and build_entry_lc_from_case env funname make_discr
    (el:tomatch_tuples)
    (brl:Glob_term.cases_clauses) avoid :
    glob_constr build_entry_return =
  match el with
    | [] -> assert false (* this case correspond to match <nothing> with .... !*)
    | el ->
	(* this case correspond to
	   match el with brl end
	   we first compute the list of lists corresponding to [el] and
	   combine them .
	   Then for each element of the combinations,
	   we compute the result we compute one list per branch in [brl] and
	   finally we just concatenate those list
	*)
	let case_resl =
	    List.fold_right
	      (fun (case_arg,_) ctxt_argsl ->
		let arg_res = build_entry_lc env funname avoid case_arg  in
		combine_results combine_args arg_res ctxt_argsl
	      )
	      el
	      (mk_result [] [] avoid)<commit_msg>Fix a bug preventing the generation of graphs when doing multiple pattern-matching on function calls.<commit_after>open Printer
open Pp
open Names
open Term
open Vars
open Glob_term
open Glob_ops
open Globnames
open Indfun_common
open Errors
open Util
open Glob_termops
open Misctypes

let observe strm =
  if do_observe ()
  then Pp.msg_debug strm
  else ()
(*let observennl strm =
  if do_observe ()
  then Pp.msg strm
  else ()*)


type binder_type =
  | Lambda of Name.t
  | Prod of Name.t
  | LetIn of Name.t

type glob_context = (binder_type*glob_constr) list

(*
   compose_glob_context [(bt_1,n_1,t_1);......] rt returns
   b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the
   binders corresponding to the bt_i's
*)
let compose_glob_context =
  let compose_binder  (bt,t) acc =
    match bt with
      | Lambda n -> mkGLambda(n,t,acc)
      | Prod n -> mkGProd(n,t,acc)
      | LetIn n -> mkGLetIn(n,t,acc)
  in
  List.fold_right compose_binder


(*
   The main part deals with building a list of globalized constructor expressions
   from the rhs of a fixpoint equation.
*)

type 'a build_entry_pre_return =
    {
      context : glob_context;  (* the binding context of the result *)
      value : 'a; (* The value *)
    }

type 'a build_entry_return =
    {
      result : 'a build_entry_pre_return list;
      to_avoid : Id.t list
    }

(*
  [combine_results combine_fun res1 res2] combine two results [res1] and [res2]
  w.r.t. [combine_fun].

  Informally, both [res1] and [res2] are lists of "constructors"  [res1_1;...]
  and [res2_1,....] and we need to produce
  [combine_fun res1_1 res2_1;combine_fun res1_1 res2_2;........]
*)

let combine_results
    (combine_fun : 'a build_entry_pre_return -> 'b build_entry_pre_return ->
      'c build_entry_pre_return
    )
    (res1: 'a build_entry_return)
    (res2 : 'b build_entry_return)
    : 'c build_entry_return
    =
  let pre_result =     List.map
    ( fun res1 ->  (* for each result in arg_res *)
	  List.map (* we add it in each args_res *)
	    (fun res2 ->
	       combine_fun res1 res2
	    )
	    res2.result
      )
      res1.result
  in (* and then we flatten the map *)
  {
    result = List.concat pre_result;
    to_avoid = List.union Id.equal res1.to_avoid res2.to_avoid
  }


(*
   The combination function for an argument with a list of argument
*)

let combine_args arg args =
  {
    context = arg.context@args.context;
    (* Note that the binding context of [arg] MUST be placed before the one of
       [args] in order to preserve possible type dependencies
    *)
    value = arg.value::args.value;
  }


let ids_of_binder =  function
  | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> []
  | LetIn (Name id)  | Prod (Name id) | Lambda (Name id) -> [id]

let rec change_vars_in_binder mapping = function
    [] -> []
  | (bt,t)::l ->
      let new_mapping = List.fold_right Id.Map.remove (ids_of_binder bt) mapping in
      (bt,change_vars mapping t)::
	(if Id.Map.is_empty new_mapping
	 then l
	 else change_vars_in_binder new_mapping l
	)

let rec replace_var_by_term_in_binder x_id term = function
  | [] -> []
  | (bt,t)::l ->
      (bt,replace_var_by_term x_id term t)::
	if Id.List.mem x_id (ids_of_binder bt)
	then l
	else replace_var_by_term_in_binder x_id term l

let add_bt_names bt = List.append (ids_of_binder bt)

let apply_args ctxt body args =
  let need_convert_id avoid id =
    List.exists (is_free_in id) args || Id.List.mem id avoid
  in
  let need_convert avoid  bt =
    List.exists (need_convert_id avoid) (ids_of_binder bt)
  in
  let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) =
    match na with
       | Name id when Id.List.mem id avoid ->
	   let new_id = Namegen.next_ident_away id avoid in
	   Name new_id,Id.Map.add id new_id mapping,new_id::avoid
       | _ -> na,mapping,avoid
  in
  let next_bt_away bt (avoid:Id.t list) =
    match bt with
      | LetIn na ->
	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
	  LetIn new_na,mapping,new_avoid
      | Prod na ->
	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
	  Prod new_na,mapping,new_avoid
      | Lambda na ->
	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
	  Lambda new_na,mapping,new_avoid
  in
  let rec do_apply avoid ctxt body args =
    match ctxt,args with
      | _,[] -> (* No more args *)
	  (ctxt,body)
      | [],_ -> (* no more fun *)
	  let f,args' = glob_decompose_app body in
	  (ctxt,mkGApp(f,args'@args))
      | (Lambda Anonymous,t)::ctxt',arg::args' ->
	  do_apply avoid ctxt' body args'
      | (Lambda (Name id),t)::ctxt',arg::args' ->
	  let new_avoid,new_ctxt',new_body,new_id =
	    if need_convert_id avoid id
	    then
	      let new_avoid =  id::avoid in
	      let new_id = Namegen.next_ident_away id new_avoid in
	      let new_avoid' = new_id :: new_avoid in
	      let mapping = Id.Map.add id new_id Id.Map.empty in
	      let new_ctxt' = change_vars_in_binder mapping ctxt' in
	      let new_body = change_vars mapping body in
	      new_avoid',new_ctxt',new_body,new_id
	    else
	      id::avoid,ctxt',body,id
	  in
	  let new_body = replace_var_by_term new_id arg new_body in
	  let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
	  do_apply avoid new_ctxt' new_body args'
      | (bt,t)::ctxt',_ ->
	  let new_avoid,new_ctxt',new_body,new_bt =
	    let new_avoid = add_bt_names bt avoid in
	    if need_convert avoid bt
	    then
	      let new_bt,mapping,new_avoid = next_bt_away bt new_avoid in
	      (
		new_avoid,
		change_vars_in_binder mapping ctxt',
		change_vars mapping body,
		new_bt
	     )
	    else new_avoid,ctxt',body,bt
	  in
	  let new_ctxt',new_body =
	    do_apply new_avoid new_ctxt' new_body args
	  in
	  (new_bt,t)::new_ctxt',new_body
  in
  do_apply []  ctxt body args


let combine_app f args =
  let new_ctxt,new_value = apply_args f.context f.value args.value in
  {
    (* Note that the binding context of [args] MUST be placed before the one of
       the applied value in order to preserve possible type dependencies
    *)
      context = args.context@new_ctxt;
      value = new_value;
  }

let combine_lam n t b =
  {
    context = [];
    value = mkGLambda(n, compose_glob_context t.context t.value,
		      compose_glob_context b.context b.value )
  }



let combine_prod n t b =
  { context = t.context@((Prod n,t.value)::b.context); value = b.value}

let combine_letin n t b =
  { context = t.context@((LetIn n,t.value)::b.context); value = b.value}


let mk_result ctxt value avoid =
  {
    result =
      [{context = ctxt;
	value = value}]
	;
    to_avoid = avoid
  }
(*************************************************
  Some functions to deal with overlapping patterns
**************************************************)

let coq_True_ref =
  lazy  (Coqlib.gen_reference "" ["Init";"Logic"] "True")

let coq_False_ref =
  lazy  (Coqlib.gen_reference "" ["Init";"Logic"] "False")

(*
  [make_discr_match_el \[e1,...en\]] builds match e1,...,en with
  (the list of expressions on which we will do the matching)
 *)
let make_discr_match_el  =
  List.map (fun e -> (e,(Anonymous,None)))

(*
  [make_discr_match_brl i \[pat_1,...,pat_n\]]  constructs a discrimination pattern matching on the ith expression.
  that is.
  match ?????? with \\
  | pat_1 => False  \\
  | pat_{i-1} => False \\
  | pat_i => True \\
  | pat_{i+1} => False \\
  \vdots
  | pat_n => False
  end
*)
let make_discr_match_brl i =
  List.map_i
    (fun j (_,idl,patl,_) ->
       if Int.equal j i
       then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref))
       else (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_False_ref))
    )
    0
(*
   [make_discr_match brl el i] generates an hypothesis such that it reduce to true iff
   brl_{i} is the first branch matched by [el]

   Used when we want to simulate the coq pattern matching algorithm
*)
let make_discr_match brl =
  fun el i ->
  mkGCases(None,
	   make_discr_match_el el,
	   make_discr_match_brl i brl)

(**********************************************************************)
(*  functions used to build case expression from lettuple and if ones *)
(**********************************************************************)

(* [build_constructors_of_type] construct the array of pattern of its inductive argument*)
let build_constructors_of_type ind' argl =
  let (mib,ind) = Inductive.lookup_mind_specif (Global.env()) ind' in
  let npar = mib.Declarations.mind_nparams in
  Array.mapi (fun i _ ->
		let construct = ind',i+1 in
		let constructref = ConstructRef(construct) in
		let _implicit_positions_of_cst =
		  Impargs.implicits_of_global constructref
		in
		let cst_narg =
		  Inductiveops.constructor_nallargs_env
		    (Global.env ())
		    construct
		in
		let argl =
		  if List.is_empty argl
		  then
 		    Array.to_list
		      (Array.init (cst_narg - npar) (fun _ -> mkGHole ())
		      )
		  else argl
		in
		let pat_as_term =
		  mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
		in
		cases_pattern_of_glob_constr Anonymous pat_as_term
	     )
    ind.Declarations.mind_consnames

(******************)
(* Main functions *)
(******************)



let raw_push_named (na,raw_value,raw_typ) env =
  match na with
    | Anonymous -> env
    | Name id ->
	let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in
	let typ,ctx = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
	Environ.push_named (id,value,typ) env


let add_pat_variables pat typ env : Environ.env =
  let rec add_pat_variables env pat typ  : Environ.env =
    observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));

    match pat with
      | PatVar(_,na) -> Environ.push_rel (na,None,typ) env
      | PatCstr(_,c,patl,na) ->
	  let Inductiveops.IndType(indf,indargs) =
	    try Inductiveops.find_rectype env (Evd.from_env env) typ
	    with Not_found -> assert false
	  in
	  let constructors = Inductiveops.get_constructors env indf in
	  let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in
	  let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
	  List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
  in
  let new_env = add_pat_variables  env pat typ in
  let res =
    fst (
      Context.fold_rel_context
	(fun (na,v,t) (env,ctxt) ->
	 match na with
	   | Anonymous -> assert false
	   | Name id ->
	       let new_t =  substl ctxt t in
	       let new_v = Option.map (substl ctxt) v in
	       observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
			  str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
			  str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
			  Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
			  Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
		       );
	       (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt)
      )
	(Environ.rel_context new_env)
	~init:(env,[])
    )
  in
  observe (str "new var env := " ++ Printer.pr_named_context_of res (Evd.from_env env));
  res




let rec pattern_to_term_and_type env typ  = function
  | PatVar(loc,Anonymous) -> assert false
  | PatVar(loc,Name id) ->
	mkGVar id
  | PatCstr(loc,constr,patternl,_) ->
      let cst_narg =
	Inductiveops.constructor_nallargs_env
	  (Global.env ())
	  constr
      in
      let Inductiveops.IndType(indf,indargs) =
	try Inductiveops.find_rectype env (Evd.from_env env) typ
	with Not_found -> assert false
      in
      let constructors = Inductiveops.get_constructors env indf in
      let constructor  = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in
      let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
      let _,cstl = Inductiveops.dest_ind_family indf in
      let csta = Array.of_list cstl in
      let implicit_args =
	Array.to_list
	  (Array.init
	     (cst_narg - List.length patternl)
	     (fun i -> Detyping.detype false [] env (Evd.from_env env) csta.(i))
	  )
      in
      let patl_as_term =
	List.map2 (pattern_to_term_and_type env)  (List.rev cs_args_types)  patternl
      in
      mkGApp(mkGRef(ConstructRef constr),
	     implicit_args@patl_as_term
	    )

(* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return)
   of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the
   corresponding graphs.


   The idea to transform a term [t] into a list of constructors [lc] is the following:
   \begin{itemize}
   \item if the term is a binder (bind x, body) then first compute [lc'] the list corresponding
   to [body] and add (bind x. _) to each elements of [lc]
   \item if the term has the form (g t1 ... ... tn) where g does not appears in (fnames)
   then compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn],
   then combine those lists and [g] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn],
   [g c1 ... cn] is an element of [lc]
   \item if the term has the form (f t1 .... tn) where [f] appears in [fnames] then
   compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn],
   then compute those lists and [f] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn]
   create a new variable [res] and [forall res, R_f c1 ... cn res] is in [lc]
   \item if the term is a cast just treat its body part
   \item
   if the term is a match, an if or a lettuple then compute the lists corresponding to each branch of the case
   and concatenate them (informally, each branch of a match produces a new constructor)
   \end{itemize}

   WARNING: The terms constructed here are only USING the glob_constr syntax but are highly bad formed.
   We must wait to have complete all the current calculi to set the recursive calls.
   At this point, each term [f t1 ... tn]  (where f appears in [funnames]) is replaced by
   a pseudo term [forall res, res t1 ... tn, res]. A reconstruction phase is done later.
   We in fact not create a constructor list since then end of each constructor has not the expected form
   but only the value of the function
*)


let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
  observe (str " Entering : " ++ Printer.pr_glob_constr rt);
  match rt with
    | GRef _ | GVar _ | GEvar _ | GPatVar _     | GSort _  | GHole _  ->
	(* do nothing (except changing type of course) *)
	mk_result [] rt avoid
    | GApp(_,_,_) ->
	let f,args = glob_decompose_app rt in
	let args_res : (glob_constr list) build_entry_return =
	  List.fold_right (* create the arguments lists of constructors and combine them *)
	    (fun arg ctxt_argsl ->
	       let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in
	       combine_results combine_args arg_res ctxt_argsl
	    )
	    args
	    (mk_result [] [] avoid)
	in
	begin
	  match f with
	    | GLambda _  -> 
		let rec aux t l = 
		  match l with 
		    | [] -> t
		    | u::l -> 
			match t with 
			  | GLambda(loc,na,_,nat,b) -> 
			      GLetIn(Loc.ghost,na,u,aux b l)
			  | _ -> 
			      GApp(Loc.ghost,t,l)
		in
		build_entry_lc env funnames avoid (aux f args)
	    | GVar(_,id) when Id.Set.mem id funnames ->
		(* if we have [f t1 ... tn] with [f]$\in$[fnames]
		   then we create a fresh variable [res],
		   add [res] and its "value" (i.e. [res v1 ... vn]) to each
		   pseudo constructor build for the arguments (i.e. a pseudo context [ctxt] and
		   a pseudo value "v1 ... vn".
		   The "value" of this branch is then simply [res]
		*)
		let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
		let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in
		let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in
		let res = fresh_id args_res.to_avoid "_res" in
		let new_avoid = res::args_res.to_avoid in
		let res_rt = mkGVar res in
		let new_result =
		  List.map
		    (fun arg_res ->
		       let new_hyps =
			 [Prod (Name res),res_raw_type;
			  Prod Anonymous,mkGApp(res_rt,(mkGVar id)::arg_res.value)]
		       in
		       {context =  arg_res.context@new_hyps; value = res_rt }
		    )
		    args_res.result
		in
		{ result = new_result; to_avoid = new_avoid }
	    | GVar _ | GEvar _ | GPatVar _ | GHole _ | GSort _ | GRef _ ->
		(* if have [g t1 ... tn] with [g] not appearing in [funnames]
		   then
		   foreach [ctxt,v1 ... vn] in [args_res] we return
		   [ctxt, g v1 .... vn]
		*)
		{
		  args_res with
		    result =
		    List.map
		      (fun args_res ->
			 {args_res with value = mkGApp(f,args_res.value)})
		      args_res.result
		}
	    | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *)
       	    | GLetIn(_,n,t,b) ->
		(* if we have [(let x := v in b) t1 ... tn] ,
		   we discard our work and compute the list of constructor for
		   [let x = v in (b t1 ... tn)] up to alpha conversion
		*)
		let new_n,new_b,new_avoid =
		  match n with
		    | Name id when List.exists (is_free_in id) args ->
			(* need to alpha-convert the name *)
			let new_id = Namegen.next_ident_away id avoid in
			let new_avoid = id:: avoid in
			let new_b =
			  replace_var_by_term
			    id
			    (GVar(Loc.ghost,id))
			    b
			in
			(Name new_id,new_b,new_avoid)
		    | _ -> n,b,avoid
		in
		build_entry_lc
		  env
		  funnames
		  avoid
		  (mkGLetIn(new_n,t,mkGApp(new_b,args)))
	    | GCases _  | GIf _ | GLetTuple _ ->
		(* we have [(match e1, ...., en with ..... end) t1 tn]
		   we first compute the result from the case and
		   then combine each of them with each of args one
		*)
		let f_res = build_entry_lc env funnames args_res.to_avoid f in
		combine_results combine_app f_res  args_res
	    | GCast(_,b,_) ->
		(* for an applied cast we just trash the cast part
		   and restart the work.

		   WARNING: We need to restart since [b] itself should be an application term
		*)
		build_entry_lc env funnames avoid (mkGApp(b,args))
	    | GRec _ -> error "Not handled GRec"
	    | GProd _ -> error "Cannot apply a type"
	end (* end of the application treatement *)

    | GLambda(_,n,_,t,b) ->
	(* we first compute the list of constructor
	   corresponding to the body of the function,
	   then the one corresponding to the type
	   and combine the two result
	*)
	let t_res = build_entry_lc env funnames avoid t  in
	let new_n =
	  match n with
	    | Name _ -> n
	    | Anonymous -> Name (Indfun_common.fresh_id [] "_x")
	in
	let new_env = raw_push_named (new_n,None,t) env in
	let b_res = build_entry_lc new_env funnames avoid b in
	combine_results (combine_lam new_n) t_res b_res
    | GProd(_,n,_,t,b) ->
	(* we first compute the list of constructor
	   corresponding to the body of the function,
	   then the one corresponding to the type
	   and combine the two result
	*)
	let t_res = build_entry_lc env funnames avoid t in
	let new_env = raw_push_named (n,None,t) env in
	let b_res = build_entry_lc new_env funnames avoid b in
	combine_results (combine_prod n) t_res b_res
    | GLetIn(_,n,v,b) ->
	(* we first compute the list of constructor
	   corresponding to the body of the function,
	   then the one corresponding to the value [t]
	   and combine the two result
	*)
	let v_res = build_entry_lc env funnames avoid v in
	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
	let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
	let new_env =
	  match n with
	      Anonymous -> env
	    | Name id -> Environ.push_named (id,Some v_as_constr,v_type) env
	in
	let b_res = build_entry_lc new_env funnames avoid b in
	combine_results (combine_letin n) v_res b_res
    | GCases(_,_,_,el,brl) ->
	(* we create the discrimination function
	   and treat the case itself
	*)
	let make_discr = make_discr_match brl in
	build_entry_lc_from_case env funnames make_discr el brl avoid
    | GIf(_,b,(na,e_option),lhs,rhs) ->
	let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
	let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
	let (ind,_) =
	  try Inductiveops.find_inductive env (Evd.from_env env) b_typ
	  with Not_found ->
	    errorlabstrm "" (str "Cannot find the inductive associated to " ++
			       Printer.pr_glob_constr b ++ str " in " ++
			       Printer.pr_glob_constr rt ++ str ". try again with a cast")
	in
	let case_pats = build_constructors_of_type (fst ind) [] in
	assert (Int.equal (Array.length case_pats) 2);
	let brl =
	  List.map_i
	    (fun i x -> (Loc.ghost,[],[case_pats.(i)],x))
	    0
	    [lhs;rhs]
	in
	let match_expr =
	  mkGCases(None,[(b,(Anonymous,None))],brl)
	in
	(* 		Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *)
	build_entry_lc env funnames avoid match_expr
    | GLetTuple(_,nal,_,b,e) ->
	begin
	  let nal_as_glob_constr =
	    List.map
	      (function
		   Name id -> mkGVar id
		 | Anonymous -> mkGHole ()
	      )
	      nal
	  in
	  let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
	  let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
	  let (ind,_) =
	    try Inductiveops.find_inductive env (Evd.from_env env) b_typ
	    with Not_found ->
	      errorlabstrm "" (str "Cannot find the inductive associated to " ++
				 Printer.pr_glob_constr b ++ str " in " ++
				 Printer.pr_glob_constr rt ++ str ". try again with a cast")
	  in
	  let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
	  assert (Int.equal (Array.length case_pats) 1);
	  let br =
	    (Loc.ghost,[],[case_pats.(0)],e)
	  in
	  let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in
	  build_entry_lc env funnames avoid match_expr

	end
    | GRec _ -> error "Not handled GRec"
    | GCast(_,b,_) ->
	build_entry_lc env funnames  avoid b
and build_entry_lc_from_case env funname make_discr
    (el:tomatch_tuples)
    (brl:Glob_term.cases_clauses) avoid :
    glob_constr build_entry_return =
  match el with
    | [] -> assert false (* this case correspond to match <nothing> with .... !*)
    | el ->
	(* this case correspond to
	   match el with brl end
	   we first compute the list of lists corresponding to [el] and
	   combine them .
	   Then for each element of the combinations,
	   we compute the result we compute one list per branch in [brl] and
	   finally we just concatenate those list
	*)
	let case_resl =
	    List.fold_right
	      (fun (case_arg,_) ctxt_argsl ->
		let arg_res = build_entry_lc env funname ctxt_argsl.to_avoid case_arg in
		combine_results combine_args arg_res ctxt_argsl
	      )
	      el
	      (mk_result [] [] avoid)
{'fraction_non_alphanumeric': 0.1104252850920393, 'fraction_numerical': 0.0031956574080154094, 'mean_word_length': 2.9961514912971223, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 191, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 2, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5436721', 'n_tokens_mistral': 17094, 'n_tokens_neox': 16082, 'n_words': 4937}