path: root/plugins/funind/glob_term_to_relation.ml

open Printer
open Pp
open Names
open Term
open Constr
open Vars
open Glob_term
open Glob_ops
open Globnames
open Indfun_common
open CErrors
open Util
open Glob_termops
open Misctypes

module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration

let observe strm =
  if do_observe ()
  then Feedback.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


let rec solve_trivial_holes pat_as_term e =
  match DAst.get pat_as_term, DAst.get e with
  | GHole _,_ -> e
  | GApp(fp,argsp),GApp(fe,argse) when glob_constr_eq fp fe ->
       DAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse))
  | _,_ -> pat_as_term
                                              
(*
   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,None,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 -> Id.Set.empty
  | LetIn (Name id)  | Prod (Name id) | Lambda (Name id) -> Id.Set.singleton id

let rec change_vars_in_binder mapping = function
    [] -> []
  | (bt,t)::l ->
      let new_mapping = Id.Set.fold 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.Set.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 = Id.Set.union (ids_of_binder bt)

let apply_args ctxt body args =
  let need_convert_id avoid id =
    List.exists (is_free_in id) args || Id.Set.mem id avoid
  in
  let need_convert avoid  bt =
    Id.Set.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.Set.t) =
    match na with
       | Name id when Id.Set.mem id avoid ->
	   let new_id = Namegen.next_ident_away id avoid in
	   Name new_id,Id.Map.add id new_id mapping,Id.Set.add new_id avoid
       | _ -> na,mapping,avoid
  in
  let next_bt_away bt (avoid:Id.Set.t) =
    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.Set.add id avoid in
	      let new_id = Namegen.next_ident_away id new_avoid in
	      let new_avoid' = Id.Set.add 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.Set.add 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 Id.Set.empty 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_prod2 n t b =
  {
    context = [];
    value = mkGProd(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.coq_reference "" ["Init";"Logic"] "True")

let coq_False_ref =
  lazy  (Coqlib.coq_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,_)) -> Loc.tag @@
       if Int.equal j i
       then (idl,patl, mkGRef (Lazy.force coq_True_ref))
       else (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 typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
        (match raw_value with
        | None ->
           Environ.push_named (NamedDecl.LocalAssum (id,typ)) env
        | Some value ->
           Environ.push_named (NamedDecl.LocalDef (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 DAst.get pat with
      | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env
      | PatCstr(c,patl,na) ->
	  let Inductiveops.IndType(indf,indargs) =
	    try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr 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 RelDecl.get_type 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.Rel.fold_outside
	(fun decl (env,ctxt) ->
         let open Context.Rel.Declaration in
	 match decl with
	   | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false
	   | LocalAssum (Name id, t) ->
	       let new_t =  substl ctxt t 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 ()
		       );
               let open Context.Named.Declaration in
	       (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt)
	   | LocalDef (Name id, v, t) ->
	       let new_t =  substl ctxt t in
	       let new_v = 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 () ++
			  str "old value := " ++ Printer.pr_lconstr v ++ fnl () ++
			  str "new value := " ++ Printer.pr_lconstr new_v ++ fnl ()
		       );
               let open Context.Named.Declaration in
	       (Environ.push_named (LocalDef (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  = DAst.with_val (function
  | PatVar Anonymous -> assert false
  | PatVar (Name id) ->
	mkGVar id
  | PatCstr(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) (EConstr.of_constr 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 RelDecl.get_type 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 Detyping.Now false Id.Set.empty env (Evd.from_env env) (EConstr.of_constr 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);
  let open CAst in
  match DAst.get 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 DAst.get f with
	    | GLambda _  -> 
		let rec aux t l = 
		  match l with 
		    | [] -> t
		    | u::l -> DAst.make @@
			match DAst.get t with 
			  | GLambda(na,_,nat,b) -> 
			      GLetIn(na,u,None,aux b l)
			  | _ -> 
			      GApp(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) (EConstr.of_constr rt_as_constr) in
		let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty 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,v,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 (Id.Set.of_list avoid) in
			let new_avoid = id:: avoid in
			let new_b =
			  replace_var_by_term
			    id
			    (DAst.make @@ GVar id)
			    b
			in
			(Name new_id,new_b,new_avoid)
		    | _ -> n,b,avoid
		in
		build_entry_lc
		  env
		  funnames
		  avoid
		  (mkGLetIn(new_n,v,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 _ -> user_err Pp.(str "Not handled GRec")
	    | GProd _ -> user_err Pp.(str "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
        if List.length t_res.result = 1 && List.length b_res.result = 1
        then combine_results (combine_prod2 n) t_res b_res
        else combine_results (combine_prod n) t_res b_res
    | GLetIn(n,v,typ,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 = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
	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) (EConstr.of_constr v_as_constr) in
	let v_type = EConstr.Unsafe.to_constr v_type in
	let new_env =
	  match n with
	      Anonymous -> env
	    | Name id -> Environ.push_named (NamedDecl.LocalDef (id,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) (EConstr.of_constr b_as_constr) in
	let (ind,_) =
	  try Inductiveops.find_inductive env (Evd.from_env env) b_typ
	  with Not_found ->
	    user_err  (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.tag ([],[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) (EConstr.of_constr b_as_constr) in
	  let (ind,_) =
	    try Inductiveops.find_inductive env (Evd.from_env env) b_typ
	    with Not_found ->
	      user_err  (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.tag ([],[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 _ -> user_err Pp.(str "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)
	in
	let types =
	  List.map (fun (case_arg,_) ->
		      let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
		      EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr case_arg_as_constr))
		   ) el
	in
	(****** The next works only if the match is not dependent ****)
	let results =
	  List.map
	    (fun ca ->
	       let res = build_entry_lc_from_case_term
	       env types
	       funname (make_discr)
	       []  brl
	       case_resl.to_avoid
	       ca
	       in
	       res
	    )
	    case_resl.result
	in
	{
	  result = List.concat (List.map (fun r -> r.result) results);
	  to_avoid =
	    List.fold_left (fun acc r -> List.union Id.equal acc r.to_avoid)
              [] results
	}

and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid
    matched_expr =
  match brl with
    | [] -> (* computed_branches  *) {result = [];to_avoid = avoid}
    | br::brl' ->
	(* alpha conversion to prevent name clashes *)
	let _,(idl,patl,return) = alpha_br avoid br in
	let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an identifier *)
	(* building a list of precondition stating that we are not in this branch
	   (will be used in the following recursive calls)
	*)
	let new_env = List.fold_right2 add_pat_variables patl types env in
	let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list =
	  List.map2
	    (fun pat typ ->
	       fun avoid pat'_as_term ->
		 let renamed_pat,_,_ = alpha_pat avoid pat in
		 let pat_ids = get_pattern_id renamed_pat  in
		 let env_with_pat_ids = add_pat_variables pat typ new_env in
		   List.fold_right
		     (fun id acc ->
			let typ_of_id =
			  Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
			in
			let raw_typ_of_id =
			  Detyping.detype Detyping.Now false Id.Set.empty
			    env_with_pat_ids (Evd.from_env env) typ_of_id
			in
			mkGProd (Name id,raw_typ_of_id,acc))
		     pat_ids
		     (glob_make_neq pat'_as_term (pattern_to_term renamed_pat))
	    )
	    patl
	    types
	in
	(* Checking if we can be in this branch
	   (will be used in the following recursive calls)
	*)
	let unify_with_those_patterns : (cases_pattern -> bool*bool) list =
	  List.map
	    (fun pat pat' -> are_unifiable pat pat',eq_cases_pattern pat pat')
	    patl
	in
	(*
	   we first compute the other branch result (in ordrer to keep the order of the matching
	   as much as possible)
	*)
	let brl'_res =
	  build_entry_lc_from_case_term
	    env
	    types
	    funname
	    make_discr
	    ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent)
	    brl'
	    avoid
	    matched_expr
	in
	(* We now create the precondition of this branch i.e.
	   1- the list of variable appearing in the different patterns of this branch and
	      the list of equation stating than el = patl (List.flatten ...)
	   2- If there exists a previous branch which pattern unify with the one of this branch
              then a discrimination precond stating that we are not in a previous branch (if List.exists ...)
	*)
      	let those_pattern_preconds =
	  (List.flatten
	    (
	      List.map3
	      (fun pat e typ_as_constr ->
		 let this_pat_ids = ids_of_pat pat in
		 let typ_as_constr = EConstr.of_constr typ_as_constr in
		 let typ = Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_as_constr in
		 let pat_as_term = pattern_to_term pat in
                 (* removing trivial holes *) 
                 let pat_as_term = solve_trivial_holes pat_as_term e in 
                  (* observe (str "those_pattern_preconds" ++ spc () ++ *)
                  (*            str "pat" ++ spc () ++ pr_glob_constr pat_as_term ++ spc ()++ *)
                  (*            str "e" ++ spc () ++ pr_glob_constr e ++spc ()++ *)
                  (*            str "typ_as_constr" ++ spc () ++ pr_lconstr typ_as_constr); *)
		 List.fold_right
		   (fun id  acc ->
		      if Id.Set.mem id this_pat_ids
		      then (Prod (Name id),
		      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
		      let raw_typ_of_id =
			Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id
		      in
		      raw_typ_of_id
			   )::acc
		      else acc
		   )
		   idl
		   [(Prod Anonymous,glob_make_eq ~typ pat_as_term e)]
	      )
	      patl
	      matched_expr.value
	      types
	  )
	  )
	  @
	  (if List.exists (function (unifl,_) ->
			     let (unif,_) =
			       List.split (List.map2 (fun x y -> x y) unifl patl)
			     in
			     List.for_all (fun x -> x) unif) patterns_to_prevent
	   then
	     let i = List.length patterns_to_prevent in
	     let pats_as_constr = List.map2 (pattern_to_term_and_type new_env) types patl in
	     [(Prod Anonymous,make_discr pats_as_constr i  )]
	   else
	     []
	  )
	in
	(* We compute the result of the value returned by the branch*)
	let return_res = build_entry_lc new_env funname new_avoid return in
	(* and combine it with the preconds computed for this branch *)
	let this_branch_res =
	  List.map
	    (fun res  ->
	       { context = matched_expr.context@those_pattern_preconds@res.context ;
		 value = res.value}
	    )
	    return_res.result
	in
	{ brl'_res with result = this_branch_res@brl'_res.result }


let is_res r = match DAst.get r with
| GVar id ->
  begin try
    String.equal (String.sub (Id.to_string id) 0 4) "_res"
  with Invalid_argument _ -> false end
| _ -> false

let is_gr c gr = match DAst.get c with
| GRef (r, _) -> Globnames.eq_gr r gr
| _ -> false

let is_gvar c = match DAst.get c with
| GVar id -> true
| _ -> false

let same_raw_term rt1 rt2 = 
  match DAst.get rt1, DAst.get rt2 with 
    | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2
    | GHole _, GHole _ -> true
    | _ -> false
let decompose_raw_eq lhs rhs = 
  let rec decompose_raw_eq lhs rhs acc = 
    observe (str "decomposing eq for " ++ pr_glob_constr lhs ++ str " " ++ pr_glob_constr rhs);
    let (rhd,lrhs) = glob_decompose_app rhs in 
    let (lhd,llhs) = glob_decompose_app lhs in 
    observe (str "lhd := " ++ pr_glob_constr lhd);
    observe (str "rhd := " ++ pr_glob_constr rhd);
    observe (str "llhs := " ++ int (List.length llhs));
    observe (str "lrhs := " ++ int (List.length lrhs));
    let sllhs = List.length llhs in 
    let slrhs = List.length lrhs in 
    if same_raw_term lhd rhd && Int.equal sllhs slrhs 
    then
      (* let _ = assert false in  *)
      List.fold_right2 decompose_raw_eq	llhs lrhs acc
    else (lhs,rhs)::acc
  in
  decompose_raw_eq lhs rhs []
     

exception Continue
(*
   The second phase which reconstruct the real type of the constructor.
   rebuild the globalized constructors expression.
   eliminates some meaningless equalities, applies some rewrites......
*)
let rec rebuild_cons env nb_args relname args crossed_types depth rt =
  observe (str "rebuilding : " ++ pr_glob_constr rt);
  let open Context.Rel.Declaration in
  let open CAst in
  match DAst.get rt with
    | GProd(n,k,t,b) ->
	let not_free_in_t id = not (is_free_in id t) in
	let new_crossed_types = t::crossed_types in
	begin
	  match DAst.get t with
	    | GApp(res_rt ,args') when is_res res_rt ->
		begin
                  let arg = List.hd args' in
		  match DAst.get arg with
		    | GVar this_relname ->
			(*i The next call to mk_rel_id is
			  valid since we are constructing the graph
			  Ensures by: obvious
			  i*)

			let new_t =
			  mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt])
			in
			let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
			let new_env = Environ.push_rel (LocalAssum (n,t')) env in
			let new_b,id_to_exclude =
			  rebuild_cons new_env
			    nb_args relname
			    args new_crossed_types
			    (depth + 1) b
			in
			mkGProd(n,new_t,new_b),
			Id.Set.filter not_free_in_t id_to_exclude
		    | _ -> (* the first args is the name of the function! *)
			assert false
		end
	    | GApp(eq_as_ref,[ty; id ;rt])
		when is_gvar id && is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref)  && n == Anonymous
		  ->
                let loc1 = rt.CAst.loc in
                let loc2 = eq_as_ref.CAst.loc in
                let loc3 = id.CAst.loc in
                let id = match DAst.get id with GVar id -> id | _ -> assert false in
		begin
		  try
		    observe (str "computing new type for eq : " ++ pr_glob_constr rt);
		    let t' =
		      try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*)
                      with e when CErrors.noncritical e -> raise Continue
		    in
		    let is_in_b = is_free_in id b in
		    let _keep_eq =
		      not (List.exists (is_free_in id) args) || is_in_b  ||
			List.exists (is_free_in id) crossed_types
		    in
		    let new_args = List.map (replace_var_by_term id rt) args in
		    let subst_b =
		      if is_in_b then b else  replace_var_by_term id rt b
		    in
		    let new_env = Environ.push_rel (LocalAssum (n,t')) env in
		    let new_b,id_to_exclude =
		      rebuild_cons
			new_env
			nb_args relname
			new_args new_crossed_types
			(depth + 1) subst_b
		    in
		    mkGProd(n,t,new_b),id_to_exclude
		  with Continue ->
		    let jmeq = Globnames.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
		    let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in
		    let ind,args' = Inductive.find_inductive env ty' in
		    let mib,_ = Global.lookup_inductive (fst ind) in
		    let nparam = mib.Declarations.mind_nparams in
		    let params,arg' =
		      ((Util.List.chop nparam args'))
		    in
		    let rt_typ = DAst.make @@
		       GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None),
			    (List.map
			      (fun p -> Detyping.detype Detyping.Now false Id.Set.empty
				 env (Evd.from_env env)
				 (EConstr.of_constr p)) params)@(Array.to_list
				      (Array.make
					 (List.length args' - nparam)
					 (mkGHole ()))))
		    in
		    let eq' =
		      DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
		    in
		    observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
		    let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
		    observe (str " computing new type for jmeq : done") ;
		    let new_args =
		      match Constr.kind eq'_as_constr with
			| App(_,[|_;_;ty;_|]) ->
			    let ty = Array.to_list (snd (destApp ty)) in
			    let ty' = snd (Util.List.chop nparam ty) in
			    List.fold_left2
			      (fun acc var_as_constr arg ->
                                let arg = EConstr.of_constr arg in
				 if isRel var_as_constr
				 then
				   let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in
				   match na with
				     | Anonymous -> acc
				     | Name id' ->
					 (id',Detyping.detype Detyping.Now false Id.Set.empty
					    env
                                            (Evd.from_env env)
					    arg)::acc
				 else if isVar var_as_constr
				 then (destVar var_as_constr,Detyping.detype Detyping.Now false Id.Set.empty
					 env
                                         (Evd.from_env env)
					 arg)::acc
				 else acc
			      )
			      []
			      arg'
			      ty'
			| _ -> assert false
		    in
		    let is_in_b = is_free_in id b in
		    let _keep_eq =
		      not (List.exists (is_free_in id) args) || is_in_b  ||
			List.exists (is_free_in id) crossed_types
		    in
		    let new_args =
		      List.fold_left
			(fun args (id,rt) ->
			   List.map (replace_var_by_term id rt) args
			)
			args
			((id,rt)::new_args)
		    in
		    let subst_b =
		     if is_in_b then b else  replace_var_by_term id rt b
		    in
		    let new_env =
		      let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in
		      Environ.push_rel (LocalAssum (n,t')) env
		    in
		    let new_b,id_to_exclude =
		      rebuild_cons
			new_env
			nb_args relname
			new_args new_crossed_types
			(depth + 1) subst_b
		    in
		    mkGProd(n,eq',new_b),id_to_exclude
		end
		  (* J.F:. keep this comment  it explain how to remove some meaningless equalities
		     if keep_eq then
		     mkGProd(n,t,new_b),id_to_exclude
		     else new_b, Id.Set.add id id_to_exclude
		  *)
	    | GApp(eq_as_ref,[ty;rt1;rt2])
		when is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
		  ->
	      begin
		try 
		  let l = decompose_raw_eq rt1 rt2 in 
		  if List.length l > 1 
		  then 
		    let new_rt =
		      List.fold_left 
			(fun acc (lhs,rhs) -> 
			  mkGProd(Anonymous,
				  mkGApp(mkGRef(Lazy.force Coqlib.coq_eq_ref),[mkGHole ();lhs;rhs]),acc)
			)
			b
			l
		    in
		    rebuild_cons env nb_args relname args crossed_types depth new_rt
		  else raise Continue
	      with Continue -> 
		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
		let t',ctx = Pretyping.understand env (Evd.from_env env) t in
		let new_env = Environ.push_rel (LocalAssum (n,t')) env in
		let new_b,id_to_exclude =
		  rebuild_cons new_env
		    nb_args relname
		    args new_crossed_types
		    (depth + 1) b
		in
		match n with
		  | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
		      new_b,Id.Set.remove id
			(Id.Set.filter not_free_in_t id_to_exclude)
		  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
	      end
	    | _ ->
		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
		let t',ctx = Pretyping.understand env (Evd.from_env env) t in
		let new_env = Environ.push_rel (LocalAssum (n,t')) env in
		let new_b,id_to_exclude =
		  rebuild_cons new_env
		    nb_args relname
		    args new_crossed_types
		    (depth + 1) b
		in
		match n with
		  | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
		      new_b,Id.Set.remove id
			(Id.Set.filter not_free_in_t id_to_exclude)
		  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
	end
    | GLambda(n,k,t,b) ->
	begin
	  let not_free_in_t id = not (is_free_in id t) in
	  let new_crossed_types = t :: crossed_types in
	  observe (str "computing new type for lambda : " ++ pr_glob_constr rt);
	  let t',ctx = Pretyping.understand env (Evd.from_env env) t in
	  match n with
	    | Name id ->
		let new_env = Environ.push_rel (LocalAssum (n,t')) env in
		let new_b,id_to_exclude =
		  rebuild_cons new_env
		    nb_args relname
		    (args@[mkGVar id])new_crossed_types
		    (depth + 1 ) b
		in
		if Id.Set.mem id id_to_exclude && depth >= nb_args
		then
		  new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
		else
		  DAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
	    | _ -> anomaly (Pp.str "Should not have an anonymous function here.")
		(* We have renamed all the anonymous functions during alpha_renaming phase *)

	end
    | GLetIn(n,v,t,b) ->
	begin
          let t = match t with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
	  let not_free_in_t id = not (is_free_in id t) in
	  let evd = (Evd.from_env env) in
	  let t',ctx = Pretyping.understand env evd t in
	  let evd = Evd.from_ctx ctx in
	  let type_t' = Typing.unsafe_type_of env evd (EConstr.of_constr t') in
	  let type_t' = EConstr.Unsafe.to_constr type_t' in
	  let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in
	  let new_b,id_to_exclude =
	    rebuild_cons new_env
	      nb_args relname
	      args (t::crossed_types)
	      (depth + 1 ) b in
	  match n with
	    | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args  ->
		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
	    | _ -> DAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *)
		Id.Set.filter not_free_in_t id_to_exclude
	end
    | GLetTuple(nal,(na,rto),t,b) ->
	assert (Option.is_empty rto);
	begin
	  let not_free_in_t id = not (is_free_in id t) in
	  let new_t,id_to_exclude' =
	    rebuild_cons env
	      nb_args
	      relname
	      args (crossed_types)
	      depth t
	  in
	  let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
	  let new_env = Environ.push_rel (LocalAssum (na,t')) env in
	  let new_b,id_to_exclude =
	    rebuild_cons new_env
	      nb_args relname
	      args (t::crossed_types)
	      (depth + 1) b
	  in
(* 	  match n with  *)
(* 	    | Name id when Id.Set.mem id id_to_exclude ->  *)
(* 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *)
(* 	    | _ -> *)
	  DAst.make @@ GLetTuple(nal,(na,None),t,new_b),
		Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude')

	end

    | _ -> mkGApp(mkGVar  relname,args@[rt]),Id.Set.empty


(* debugging wrapper *)
let rebuild_cons env nb_args relname args crossed_types rt =
(*   observennl  (str "rebuild_cons : rt := "++ pr_glob_constr rt ++  *)
(* 		 str "nb_args := " ++ str (string_of_int nb_args)); *)
  let res =
    rebuild_cons env nb_args relname args crossed_types 0 rt
  in
(*   observe (str " leads to "++ pr_glob_constr (fst res)); *)
  res


(* naive implementation of parameter detection.

   A parameter is an argument which is only preceded by parameters and whose
   calls are all syntactically equal.

   TODO: Find a valid way to deal with implicit arguments here!
*)
let rec compute_cst_params relnames params gt = DAst.with_val (function
  | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params
  | GApp(f,args) ->
    begin match DAst.get f with
    | GVar relname' when Id.Set.mem relname' relnames ->
      compute_cst_params_from_app [] (params,args)
    | _ ->
      List.fold_left (compute_cst_params relnames) params (f::args)
    end
  | GLambda(_,_,t,b) | GProd(_,_,t,b) | GLetTuple(_,_,t,b) ->
      let t_params = compute_cst_params relnames params t in
      compute_cst_params relnames t_params b
  | GLetIn(_,v,t,b) ->
      let v_params = compute_cst_params relnames params v in
      let t_params = Option.fold_left (compute_cst_params relnames) v_params t in
      compute_cst_params relnames t_params b
  | GCases _ ->
      params  (* If there is still cases at this point they can only be
		 discrimination ones *)
  | GSort _ -> params
  | GHole _ -> params
  | GIf _ | GRec _ | GCast _ ->
      raise (UserError(Some "compute_cst_params", str "Not handled case"))
  ) gt
and compute_cst_params_from_app acc (params,rtl) =
  let is_gid id c = match DAst.get c with GVar id' -> Id.equal id id' | _ -> false in
  match params,rtl with
    | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
    | ((Name id,_,None) as param)::params', c::rtl' when is_gid id c ->
	compute_cst_params_from_app (param::acc) (params',rtl')
    | _  -> List.rev acc

let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_constr option) list array) csts =
  let rels_params =
    Array.mapi
      (fun i args ->
	 List.fold_left
	   (fun params (_,cst) -> compute_cst_params relnames params cst)
	   args
	   csts.(i)
      )
      args
  in
  let l = ref [] in
  let _ =
    try
      List.iteri
	(fun i ((n,nt,typ) as param) ->
	   if Array.for_all
	     (fun l ->
		let (n',nt',typ') = List.nth l i in
		Name.equal n n' && glob_constr_eq nt nt' && Option.equal glob_constr_eq typ typ')
	     rels_params
	   then
	     l := param::!l
	)
	rels_params.(0)
    with e when CErrors.noncritical e ->
      ()
  in
  List.rev !l

let rec rebuild_return_type rt =
  let loc = rt.CAst.loc in
  match rt.CAst.v with
    | Constrexpr.CProdN(n,t') ->
        CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
    | Constrexpr.CLetIn(na,v,t,t') ->
	CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
    | _ -> CAst.make ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous],
				       Constrexpr.Default Decl_kinds.Explicit, rt],
			    CAst.make @@ Constrexpr.CSort(GType []))

let do_build_inductive
      evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
      returned_types
      (rtl:glob_constr list) =
  let _time1 = System.get_time () in
  let funnames = List.map (fun c -> Label.to_id (KerName.label (Constant.canonical (fst c)))) funconstants in
  (*   Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *)
  let funnames_as_set = List.fold_right Id.Set.add funnames Id.Set.empty in
  let funnames = Array.of_list funnames in
  let funsargs = Array.of_list funsargs in
  let returned_types = Array.of_list returned_types in
  (* alpha_renaming of the body to prevent variable capture during manipulation *)
  let rtl_alpha = List.map (function rt ->  expand_as (alpha_rt [] rt)) rtl in
  let rta = Array.of_list rtl_alpha in
  (*i The next call to mk_rel_id is valid since we are constructing the graph
    Ensures by: obvious
    i*)
  let relnames = Array.map mk_rel_id funnames in
  let relnames_as_set = Array.fold_right Id.Set.add relnames Id.Set.empty in
  (* Construction of the pseudo constructors *)
  let open Context.Named.Declaration in
  let evd,env =
    Array.fold_right2
      (fun id (c, u) (evd,env) ->
       let u = EConstr.EInstance.make u in
       let evd,t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in
       let t = EConstr.Unsafe.to_constr t in
       evd,
       Environ.push_named (LocalAssum (id,t))
			 env
      )
      funnames
      (Array.of_list funconstants)
      (evd,Global.env ())
  in
  (* we solve and replace the implicits *)
  let rta =
    Array.mapi (fun i rt ->
        let _,t = Typing.type_of env evd (EConstr.of_constr (mkConstU ((Array.of_list funconstants).(i)))) in
        resolve_and_replace_implicits ~expected_type:(Pretyping.OfType t) env evd rt
      ) rta
  in
  let resa = Array.map (build_entry_lc env funnames_as_set []) rta in
  let env_with_graphs =
    let rel_arity i funargs =  (* Rebuilding arities (with parameters) *)
      let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list  =
	funargs
      in
      List.fold_right
	(fun (n,t,typ) acc ->
          match typ with
          | Some typ ->
	     CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
                              Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
			      acc)
	  | None ->
	     CAst.make @@ Constrexpr.CProdN
	       ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
		acc
	       )
	)
	rel_first_args
	(rebuild_return_type returned_types.(i))
    in
    (* We need to lift back our work topconstr but only with all information
       We mimick a Set Printing All.
       Then save the graphs and reset Printing options to their primitive values
    *)
    let rel_arities = Array.mapi rel_arity funsargs in
    Util.Array.fold_left2 (fun env rel_name rel_ar ->
			     Environ.push_named (LocalAssum (rel_name,
						             fst (with_full_print (Constrintern.interp_constr env evd) rel_ar))) env) env relnames rel_arities
  in
  (* and of the real constructors*)
  let constr i res =
    List.map
      (function result (* (args',concl') *) ->
	 let rt = compose_glob_context result.context result.value in
	 let nb_args = List.length funsargs.(i) in
	 (*  with_full_print (fun rt -> Pp.msgnl (str "glob constr " ++ pr_glob_constr rt)) rt; *)
	 fst (
	   rebuild_cons env_with_graphs nb_args relnames.(i)
	     []
	     []
	     rt
	 )
      )
      res.result
  in
  (* adding names to constructors  *)
 let next_constructor_id = ref (-1) in
  let mk_constructor_id i =
    incr next_constructor_id;
    (*i The next call to mk_rel_id is valid since we are constructing the graph
      Ensures by: obvious
      i*)
    Id.of_string ((Id.to_string (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
  in
  let rel_constructors i rt : (Id.t*glob_constr) list =
    next_constructor_id := (-1);
    List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt)
  in
  let rel_constructors = Array.mapi rel_constructors resa in
  (* Computing the set of parameters if asked *)
  let rels_params = compute_params_name relnames_as_set funsargs  rel_constructors in
  let nrel_params = List.length rels_params in
  let rel_constructors = (* Taking into account the parameters in constructors *)
    Array.map (List.map
    (fun (id,rt) -> (id,snd (chop_rprod_n nrel_params rt))))
    rel_constructors
  in
  let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
    let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list  =
      (snd (List.chop nrel_params funargs))
    in
    List.fold_right
      (fun (n,t,typ) acc ->
         match typ with
         | Some typ ->
	   CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
                              Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
			    acc)
	 | None ->
           CAst.make @@ Constrexpr.CProdN
	   ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
	    acc
	   )
      )
      rel_first_args
      (rebuild_return_type returned_types.(i))
  in
  (* We need to lift back our work topconstr but only with all information
     We mimick a Set Printing All.
     Then save the graphs and reset Printing options to their primitive values
  *)
  let rel_arities = Array.mapi rel_arity funsargs in
  let rel_params_ids =
    List.fold_left
      (fun  acc (na,_,_) ->
       match na with
	 Anonymous -> acc
       | Name id -> id::acc
      )
      []
      rels_params
  in
  let rel_params =
    List.map
      (fun (n,t,typ) ->
         match typ with
         | Some typ ->
	   Constrexpr.CLocalDef((Loc.tag n), Constrextern.extern_glob_constr Id.Set.empty t,
                                  Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ))
	 | None ->
	 Constrexpr.CLocalAssum
	   ([(Loc.tag n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
      )
      rels_params
  in
  let ext_rels_constructors =
    Array.map (List.map
      (fun (id,t) ->
	 false,((Loc.tag id),
		with_full_print
		  (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t))
	       )
      ))
      (rel_constructors)
  in
  let rel_ind i ext_rel_constructors =
    (((Loc.tag @@ relnames.(i)), None),
    rel_params,
    Some rel_arities.(i),
    ext_rel_constructors),[]
  in
  let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in
  let rel_inds = Array.to_list ext_rel_constructors in
(*   let _ =  *)
(*   Pp.msgnl  (\* observe *\) ( *)
(*       str "Inductive" ++ spc () ++ *)
(* 	prlist_with_sep  *)
(* 	(fun () -> fnl ()++spc () ++ str "with" ++ spc ())  *)
(* 	(function ((_,id),_,params,ar,constr) ->  *)
(* 	   Ppconstr.pr_id id ++ spc () ++  *)
(* 	     Ppconstr.pr_binders params ++ spc () ++ *)
(* 	     str ":" ++ spc () ++  *)
(* 	     Ppconstr.pr_lconstr_expr ar ++ spc () ++ str ":=" ++ *)
(* 	     prlist_with_sep  *)
(* 	     (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ()) *)
(* 	     (function (_,((_,id),t)) ->  *)
(* 		Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++ *)
(* 		  Ppconstr.pr_lconstr_expr t) *)
(* 	     constr *)
(* 	) *)
(* 	rel_inds *)
(*     ) *)
(*   in *)
  let _time2 = System.get_time () in
  try
    with_full_print
      (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false))
      Decl_kinds.Finite
  with
    | UserError(s,msg) as e ->
	let _time3 = System.get_time () in
(* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
	let repacked_rel_inds =
	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
	                  rel_inds
	in
	let msg =
	  str "while trying to define"++ spc () ++
	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))
	    ++ fnl () ++
	    msg
	in
	observe (msg);
	raise e
    | reraise ->
	let _time3 = System.get_time () in
(* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
	let repacked_rel_inds =
	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
	                  rel_inds
	in
	let msg =
	  str "while trying to define"++ spc () ++
	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))
	    ++ fnl () ++
	    CErrors.print reraise
	in
 	observe msg;
	raise reraise



let build_inductive evd funconstants funsargs returned_types rtl =
  let pu = !Detyping.print_universes in
  let cu = !Constrextern.print_universes in
  try
    Detyping.print_universes := true;
    Constrextern.print_universes := true;
    do_build_inductive evd funconstants funsargs returned_types rtl;
    Detyping.print_universes := pu;
    Constrextern.print_universes := cu
  with e when CErrors.noncritical e ->
    Detyping.print_universes := pu;
    Constrextern.print_universes := cu;
    raise (Building_graph e)