(* Utility Functions *)

exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;;
let get_module_path_of_section_path path =
 let dirpath = fst (Libnames.repr_path path) in
 let modules = Lib.library_dp () :: (Library.loaded_libraries ()) in
  match
   List.filter
    (function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules
  with
     [modul] -> modul
   | _ -> raise TwoModulesWhoseDirPathIsOneAPrefixOfTheOther
;;

(*CSC: Problem: here we are using the wrong (???) hypothesis that there do *)
(*CSC: not exist two modules whose dir_paths are one a prefix of the other *)
let remove_module_dirpath_from_dirpath ~basedir dir =
 let module Ln = Libnames in
  if Ln.is_dirpath_prefix_of basedir dir then
   let ids = Names.repr_dirpath dir in
   let rec remove_firsts n l =
    match n,l with
       (0,l) -> l
     | (n,he::tl) -> remove_firsts (n-1) tl
     | _ -> assert false
   in
    let ids' =
     List.rev
      (remove_firsts
        (List.length (Names.repr_dirpath basedir))
        (List.rev ids))
    in
     ids'
  else Names.repr_dirpath dir
;;


let get_uri_of_var v pvars =
 let module D = Declare in
 let module N = Names in
  let rec search_in_pvars names =
   function
      [] -> None
    | ((name,l)::tl) ->
       let names' = name::names in
        if List.mem v l then
         Some names'
        else
         search_in_pvars names' tl
  in
  let rec search_in_open_sections =
   function
      [] -> Util.error "Variable not found"
    | he::tl as modules ->
       let dirpath = N.make_dirpath modules in
        if List.mem (N.id_of_string v) (D.last_section_hyps dirpath) then
         modules
        else
         search_in_open_sections tl
  in
   let path =
    match search_in_pvars [] pvars with
       None -> search_in_open_sections (N.repr_dirpath (Lib.cwd ()))
     | Some path -> path
   in
    "cic:" ^
     List.fold_left
      (fun i x -> "/" ^ N.string_of_id x ^ i) "" path
;;

type tag =
   Constant
 | Inductive
 | Variable
;;

let ext_of_tag =
 function
    Constant  -> "con"
  | Inductive -> "ind"
  | Variable  -> "var"
;;

exception FunctorsXMLExportationNotImplementedYet;;

let subtract l1 l2 =
 let l1' = List.rev (Names.repr_dirpath l1) in
 let l2' = List.rev (Names.repr_dirpath l2) in
  let rec aux =
   function
      he::tl when tl = l2' -> [he]
    | he::tl -> he::(aux tl)
    | [] -> assert (l2' = []) ; []
  in
   Names.make_dirpath (List.rev (aux l1'))
;;

(*CSC: Dead code to be removed
let token_list_of_kernel_name ~keep_sections kn tag =
 let module N = Names in
  let (modpath,dirpath,label) = Names.repr_kn kn in
  let token_list_of_dirpath dirpath =
   List.rev_map N.string_of_id (N.repr_dirpath dirpath) in
  let rec token_list_of_modpath =
   function
      N.MPdot (path,label) ->
       token_list_of_modpath path @ [N.string_of_label label]
    | N.MPfile dirpath -> token_list_of_dirpath dirpath
    | N.MPself self ->
       if self = Names.initial_msid then
        [ "Top" ]
       else
        let module_path =
          let f = N.string_of_id (N.id_of_msid self) in
          let _,longf = 
            System.find_file_in_path (Library.get_load_path ()) (f^".v") in
          let ldir0 = Library.find_logical_path (Filename.dirname longf) in
          let id = Names.id_of_string (Filename.basename f) in
           Libnames.extend_dirpath ldir0 id
        in
          token_list_of_dirpath module_path
    | N.MPbound _ -> raise FunctorsXMLExportationNotImplementedYet
  in
   token_list_of_modpath modpath @
    (if keep_sections then token_list_of_dirpath dirpath else []) @
    [N.string_of_label label ^ "." ^ (ext_of_tag tag)]
;;
*)

let token_list_of_path dir id tag =
 let module N = Names in
  let token_list_of_dirpath dirpath =
   List.rev_map N.string_of_id (N.repr_dirpath dirpath) in
  token_list_of_dirpath dir @ [N.string_of_id id ^ "." ^ (ext_of_tag tag)]

let token_list_of_kernel_name kn tag =
 let module N = Names in
 let module LN = Libnames in
 let dir = match tag with
   | Variable -> 
       Lib.cwd ()
   | Constant -> 
       Lib.library_part (LN.ConstRef kn)
   | Inductive ->
       Lib.library_part (LN.IndRef (kn,0))
 in
 let id = N.id_of_label (N.label kn) in
 token_list_of_path dir id tag
;;

let uri_of_kernel_name kn tag =
  let tokens = token_list_of_kernel_name kn tag in
   "cic:/" ^ String.concat "/" tokens

let uri_of_declaration id tag =
 let module LN = Libnames in
 let dir = LN.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) in
 let tokens = token_list_of_path dir id tag in
  "cic:/" ^ String.concat "/" tokens

(* Special functions for handling of CCorn's CProp "sort" *)

type sort =
   Coq_sort of Term.sorts_family
 | CProp
;;

let cprop =
 let module N = Names in
  N.make_kn
   (N.MPfile
     (Libnames.dirpath_of_string "CoRN.algebra.CLogic"))
   (N.make_dirpath [])
   (N.mk_label "CProp")
;;

let prerr_endline _ = ();;

let whd_betadeltaiotacprop env evar_map ty =
 let module R = Rawterm in
  let red_exp =
   R.Hnf  (*** Instead CProp is made Opaque ***)
(*
   R.Cbv
    {R.rBeta = true ; R.rIota = true ; R.rDelta = true; R.rZeta=true ;
     R.rConst = [Names.EvalConstRef cprop]
    }
*)
  in
Conv_oracle.set_opaque_const cprop;
prerr_endline "###whd_betadeltaiotacprop:" ;
let xxx =
(*Pp.msgerr (Printer.prterm_env env ty);*)
prerr_endline "";
   Tacred.reduction_of_redexp red_exp env evar_map ty
in
prerr_endline "###FINE" ;
(*
Pp.msgerr (Printer.prterm_env env xxx);
*)
prerr_endline "";
Conv_oracle.set_transparent_const cprop;
xxx
;;

let family_of_term ty =
 match Term.kind_of_term ty with
    Term.Sort s -> Coq_sort (Term.family_of_sort s)
  | Term.Const _ -> CProp  (* I could check that the constant is CProp *)
  | _ -> Util.anomaly "family_of_term"
;;

module CPropRetyping =
 struct
  module T = Term

  let outsort env sigma t =
   family_of_term (whd_betadeltaiotacprop env sigma t)

  let rec subst_type env sigma typ = function
  | [] -> typ
  | h::rest ->
      match T.kind_of_term (whd_betadeltaiotacprop env sigma typ) with
        | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest
        | _ -> Util.anomaly "Non-functional construction"

                                                                                
  let sort_of_atomic_type env sigma ft args =
  let rec concl_of_arity env ar =
    match T.kind_of_term (whd_betadeltaiotacprop env sigma ar) with
      | T.Prod (na, t, b) -> concl_of_arity (Environ.push_rel (na,None,t) env) b
      | T.Sort s -> Coq_sort (T.family_of_sort s)
      | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args))
  in concl_of_arity env ft
                                                                                
let typeur sigma metamap =
  let rec type_of env cstr=
    match Term.kind_of_term cstr with
    | T.Meta n ->
          (try T.strip_outer_cast (List.assoc n metamap)
           with Not_found -> Util.anomaly "type_of: this is not a well-typed term")
    | T.Rel n ->
        let (_,_,ty) = Environ.lookup_rel n env in
        T.lift n ty
    | T.Var id ->
        (try
          let (_,_,ty) = Environ.lookup_named id env in
          T.body_of_type ty
        with Not_found ->
          Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound"))
    | T.Const c ->
        let cb = Environ.lookup_constant c env in
        T.body_of_type cb.Declarations.const_type
    | T.Evar ev -> Instantiate.existential_type sigma ev
    | T.Ind ind -> T.body_of_type (Inductive.type_of_inductive env ind)
    | T.Construct cstr ->
       T.body_of_type (Inductive.type_of_constructor env cstr)
    | T.Case (_,p,c,lf) ->
        let Inductiveops.IndType(_,realargs) =
          try Inductiveops.find_rectype env sigma (type_of env c)
          with Not_found -> Util.anomaly "type_of: Bad recursive type" in
        let t = Reductionops.whd_beta (T.applist (p, realargs)) in
        (match Term.kind_of_term (whd_betadeltaiotacprop env sigma (type_of env t)) with
          | T.Prod _ -> Reductionops.whd_beta (T.applist (t, [c]))
          | _ -> t)
    | T.Lambda (name,c1,c2) ->
          T.mkProd (name, c1, type_of (Environ.push_rel (name,None,c1) env) c2)
    | T.LetIn (name,b,c1,c2) ->
         T.subst1 b (type_of (Environ.push_rel (name,Some b,c1) env) c2)
    | T.Fix ((_,i),(_,tys,_)) -> tys.(i)
    | T.CoFix (i,(_,tys,_)) -> tys.(i)
    | T.App(f,args)->
        T.strip_outer_cast
          (subst_type env sigma (type_of env f) (Array.to_list args))
    | T.Cast (c,t) -> t
    | T.Sort _ | T.Prod _ ->
       match sort_of env cstr with
          Coq_sort T.InProp -> T.mkProp
        | Coq_sort T.InSet -> T.mkSet
        | Coq_sort T.InType -> T.mkType Univ.prop_univ (* ERROR HERE *)
        | CProp -> T.mkConst cprop
                                                                                
  and sort_of env t =
    match Term.kind_of_term t with
    | T.Cast (c,s) when T.isSort s -> family_of_term s
    | T.Sort (T.Prop c) -> Coq_sort (if c = T.Pos then T.InSet else T.InProp)
    | T.Sort (T.Type u) -> Coq_sort T.InType
    | T.Prod (name,t,c2) ->
       sort_of (Environ.push_rel (name,None,t) env) c2
    | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
    | T.Lambda _ | T.Fix _ | T.Construct _ ->
        Util.anomaly "sort_of: Not a type (1)"
    | _ -> outsort env sigma (type_of env t)
                                                                                
  and sort_family_of env t =
    match T.kind_of_term t with
    | T.Cast (c,s) when T.isSort s -> family_of_term s
    | T.Sort (T.Prop c) -> Coq_sort T.InType
    | T.Sort (T.Type u) -> Coq_sort T.InType
    | T.Prod (name,t,c2) -> sort_family_of (Environ.push_rel (name,None,t) env) c2
    | T.App(f,args) ->
       sort_of_atomic_type env sigma (type_of env f) args
    | T.Lambda _ | T.Fix _ | T.Construct _ ->
        Util.anomaly "sort_of: Not a type (1)"
    | _ -> outsort env sigma (type_of env t)
                                                                                
  in type_of, sort_of, sort_family_of

  let get_sort_family_of env sigma c = let _,_,f = typeur sigma [] in f env c

 end
;;

let get_sort_family_of env evar_map ty =
 CPropRetyping.get_sort_family_of env evar_map ty
;;

let type_as_sort env evar_map ty =
(* CCorn code *)
 family_of_term (whd_betadeltaiotacprop env evar_map ty)
;;

let is_a_Prop =
 function
    "Prop"
  | "CProp" -> true
  | _ -> false
;;

(* Main Functions *)

type anntypes =
 {annsynthesized : Acic.aconstr ; annexpected : Acic.aconstr option}
;;

let gen_id seed =
 let res = "i" ^ string_of_int !seed in
  incr seed ;
  res
;;

let fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids =
 fun father t ->
  let res = gen_id seed in
   Hashtbl.add ids_to_father_ids res father ;
   Hashtbl.add ids_to_terms res t ;
   Acic.CicHash.add constr_to_ids t res ;
   res
;;

let source_id_of_id id = "#source#" ^ id;;

let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids
 ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
 pvars ?(fake_dependent_products=false) env idrefs evar_map t expectedty
=
 let module D = DoubleTypeInference in
 let module E = Environ in
 let module N = Names in
 let module A = Acic in
 let module T = Term in
  let fresh_id' = fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids in
   (* CSC: do you have any reasonable substitute for 503? *)
   let terms_to_types = Acic.CicHash.create 503 in
    D.double_type_of env evar_map t expectedty terms_to_types ;
    let rec aux computeinnertypes father passed_lambdas_or_prods_or_letins env
     idrefs ?(subst=None,[]) tt
    =
     let fresh_id'' = fresh_id' father tt in
     let aux' = aux computeinnertypes (Some fresh_id'') [] in
      let string_of_sort_family =
       function
          Coq_sort T.InProp -> "Prop"
        | Coq_sort T.InSet  -> "Set"
        | Coq_sort T.InType -> "Type"
        | CProp -> "CProp"
      in
      let string_of_sort t =
       string_of_sort_family
        (type_as_sort env evar_map t)
      in
       let ainnertypes,innertype,innersort,expected_available =
        let {D.synthesized = synthesized; D.expected = expected} =
         if computeinnertypes then
try
          Acic.CicHash.find terms_to_types tt
with _ ->
(*CSC: Warning: it really happens, for example in Ring_theory!!! *)
Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.prterm tt)) ; assert false (* buco nella double-type-inference *) ; {D.synthesized = Reductionops.nf_beta (Retyping.get_type_of env evar_map (Evarutil.refresh_universes tt)) ; D.expected = None}
         else
          (* We are already in an inner-type and Coscoy's double *)
          (* type inference algorithm has not been applied.      *)
          (* We need to refresh the universes because we are doing *)
          (* type inference on an already inferred type.           *)
          {D.synthesized =
            Reductionops.nf_beta
             (Retyping.get_type_of env evar_map
              (Evarutil.refresh_universes tt)) ;
           D.expected = None}
        in
(* Debugging only:
print_endline "TERMINE:" ; flush stdout ;
Pp.ppnl (Printer.prterm tt) ; flush stdout ;
print_endline "TIPO:" ; flush stdout ;
Pp.ppnl (Printer.prterm synthesized) ; flush stdout ;
print_endline "ENVIRONMENT:" ; flush stdout ;
Pp.ppnl (Printer.pr_context_of env) ; flush stdout ;
print_endline "FINE_ENVIRONMENT" ; flush stdout ;
*)
         let innersort = get_sort_family_of env evar_map synthesized in
(* Debugging only:
print_endline "PASSATO" ; flush stdout ;
*)
          let ainnertypes,expected_available =
           if computeinnertypes then
            let annexpected,expected_available =
               match expected with
                  None -> None,false
                | Some expectedty' ->
                   Some (aux false (Some fresh_id'') [] env idrefs expectedty'),
                    true
            in
             Some
              {annsynthesized =
                aux false (Some fresh_id'') [] env idrefs synthesized ;
               annexpected = annexpected
              }, expected_available
           else
            None,false
          in
           ainnertypes,synthesized, string_of_sort_family innersort,
            expected_available
       in
        let add_inner_type id =
         match ainnertypes with
            None -> ()
          | Some ainnertypes -> Hashtbl.add ids_to_inner_types id ainnertypes
        in

         (* explicit_substitute_and_eta_expand_if_required h t t'         *)
         (* where [t] = [] and [tt] = [h]{[t']} ("{.}" denotes explicit   *)
         (* named substitution) or [tt] = (App [h]::[t]) (and [t'] = [])  *)
         (* check if [h] is a term that requires an explicit named        *)
         (* substitution and, in that case, uses the first arguments of   *)
         (* [t] as the actual arguments of the substitution. If there     *)
         (* are not enough parameters in the list [t], then eta-expansion *)
         (* is performed.                                                 *)
         let
          explicit_substitute_and_eta_expand_if_required h t t'
           compute_result_if_eta_expansion_not_required
         =
          let subst,residual_args,uninst_vars =
           let variables,basedir =
             try
               let g = Libnames.reference_of_constr h in
               let sp =
                match g with
                   Libnames.ConstructRef ((induri,_),_)
                 | Libnames.IndRef (induri,_) ->
                    Nametab.sp_of_global (Libnames.IndRef (induri,0))
                 | Libnames.VarRef id ->
                    (* Invariant: variables are never cooked in Coq *)
                    raise Not_found
                 | _ -> Nametab.sp_of_global g
               in
               Dischargedhypsmap.get_discharged_hyps sp,
               get_module_path_of_section_path sp
             with Not_found ->
                (* no explicit substitution *)
                [], Libnames.dirpath_of_string "dummy"
           in
           (* returns a triple whose first element is  *)
           (* an explicit named substitution of "type" *)
           (* (variable * argument) list, whose        *)
           (* second element is the list of residual   *)
           (* arguments and whose third argument is    *) 
           (* the list of uninstantiated variables     *)
           let rec get_explicit_subst variables arguments =
            match variables,arguments with
               [],_ -> [],arguments,[]
             | _,[] -> [],[],variables
             | he1::tl1,he2::tl2 ->
                let subst,extra_args,uninst = get_explicit_subst tl1 tl2 in
                let (he1_sp, he1_id) = Libnames.repr_path he1 in
                let he1' = remove_module_dirpath_from_dirpath ~basedir he1_sp in
                let he1'' =
                 String.concat "/"
                  (List.map Names.string_of_id (List.rev he1')) ^ "/"
                 ^ (Names.string_of_id he1_id) ^ ".var" 
                in
                 (he1'',he2)::subst, extra_args, uninst
           in
            get_explicit_subst variables t'
          in
           let uninst_vars_length = List.length uninst_vars in
            if uninst_vars_length > 0 then
             (* Not enough arguments provided. We must eta-expand! *)
             let un_args,_ =
              T.decompose_prod_n uninst_vars_length
               (Retyping.get_type_of env evar_map tt)
             in
              let eta_expanded =
               let arguments =
                List.map (T.lift uninst_vars_length) t @
                 Termops.rel_list 0 uninst_vars_length
               in
                Unshare.unshare
                 (T.lamn uninst_vars_length un_args
                  (T.applistc h arguments))
              in
               D.double_type_of env evar_map eta_expanded
                None terms_to_types ;
               Hashtbl.remove ids_to_inner_types fresh_id'' ;
               aux' env idrefs eta_expanded
            else
             compute_result_if_eta_expansion_not_required subst residual_args
         in

          (* Now that we have all the auxiliary functions we  *)
          (* can finally proceed with the main case analysis. *) 
          match T.kind_of_term tt with
             T.Rel n ->
              let id =
               match List.nth (E.rel_context env) (n - 1) with
                  (N.Name id,_,_)   -> id
                | (N.Anonymous,_,_) -> Nameops.make_ident "_" None
              in
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort  && expected_available then
                add_inner_type fresh_id'' ;
               A.ARel (fresh_id'', n, List.nth idrefs (n-1), id)
           | T.Var id ->
              let path = get_uri_of_var (N.string_of_id id) pvars in
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort  && expected_available then
                add_inner_type fresh_id'' ;
               A.AVar
                (fresh_id'', path ^ "/" ^ (N.string_of_id id) ^ ".var")
           | T.Evar (n,l) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
              if is_a_Prop innersort  && expected_available then
               add_inner_type fresh_id'' ;
              A.AEvar
               (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l))
           | T.Meta _ -> Util.anomaly "Meta met during exporting to XML"
           | T.Sort s -> A.ASort (fresh_id'', s)
           | T.Cast (v,t) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
              if is_a_Prop innersort then
               add_inner_type fresh_id'' ;
              A.ACast (fresh_id'', aux' env idrefs v, aux' env idrefs t)
           | T.Prod (n,s,t) ->
              let n' =
               match n with
                  N.Anonymous -> N.Anonymous
                | _ ->
                  if not fake_dependent_products && T.noccurn 1 t then
                   N.Anonymous
                  else
                   N.Name
                    (Nameops.next_name_away n (Termops.ids_of_context env))
              in
               Hashtbl.add ids_to_inner_sorts fresh_id''
                (string_of_sort innertype) ;
               let sourcetype = Retyping.get_type_of env evar_map s in
                Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
                 (string_of_sort sourcetype) ;
               let new_passed_prods =
                let father_is_prod =
                 match father with
                    None -> false
                  | Some father' ->
                     match
                      Term.kind_of_term (Hashtbl.find ids_to_terms father')
                     with
                        T.Prod _ -> true
                      | _ -> false
                in
                 (fresh_id'', n', aux' env idrefs s)::
                  (if father_is_prod then
                    passed_lambdas_or_prods_or_letins
                   else [])
               in
                let new_env = E.push_rel (n', None, s) env in
                let new_idrefs = fresh_id''::idrefs in
                 (match Term.kind_of_term t with
                     T.Prod _ ->
                      aux computeinnertypes (Some fresh_id'') new_passed_prods
                       new_env new_idrefs t
                   | _ ->
                     A.AProds (new_passed_prods, aux' new_env new_idrefs t))
           | T.Lambda (n,s,t) ->
              let n' =
               match n with
                  N.Anonymous -> N.Anonymous
                | _ ->
                  N.Name (Nameops.next_name_away n (Termops.ids_of_context env))
              in
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               let sourcetype = Retyping.get_type_of env evar_map s in
                Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
                 (string_of_sort sourcetype) ;
               let father_is_lambda =
                match father with
                   None -> false
                 | Some father' ->
                    match
                     Term.kind_of_term (Hashtbl.find ids_to_terms father')
                    with
                       T.Lambda _ -> true
                     | _ -> false
               in
                if is_a_Prop innersort &&
                   ((not father_is_lambda) || expected_available)
                then add_inner_type fresh_id'' ;
                let new_passed_lambdas =
                 (fresh_id'',n', aux' env idrefs s)::
                  (if father_is_lambda then
                    passed_lambdas_or_prods_or_letins
                   else []) in
                let new_env = E.push_rel (n', None, s) env in
                let new_idrefs = fresh_id''::idrefs in
                 (match Term.kind_of_term t with
                     T.Lambda _ ->
                      aux computeinnertypes (Some fresh_id'') new_passed_lambdas
                       new_env new_idrefs t
                   | _ ->
                     let t' = aux' new_env new_idrefs t in
                      (* eta-expansion for explicit named substitutions *)
                      (* can create nested Lambdas. Here we perform the *)
                      (* flattening.                                    *)
                      match t' with
                         A.ALambdas (lambdas, t'') ->
                          A.ALambdas (lambdas@new_passed_lambdas, t'')
                       | _ ->
                         A.ALambdas (new_passed_lambdas, t')
                 )
           | T.LetIn (n,s,t,d) ->
              let n' =
               match n with
                  N.Anonymous -> N.Anonymous
                | _ ->
                  N.Name (Nameops.next_name_away n (Termops.ids_of_context env))
              in
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               let sourcesort =
                get_sort_family_of env evar_map
                 (Retyping.get_type_of env evar_map s)
               in
                Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
                 (string_of_sort_family sourcesort) ;
               let father_is_letin =
                match father with
                   None -> false
                 | Some father' ->
                    match
                     Term.kind_of_term (Hashtbl.find ids_to_terms father')
                    with
                       T.LetIn _ -> true
                     | _ -> false
               in
                if is_a_Prop innersort then
                 add_inner_type fresh_id'' ;
                let new_passed_letins =
                 (fresh_id'',n', aux' env idrefs s)::
                  (if father_is_letin then
                    passed_lambdas_or_prods_or_letins
                   else []) in
                let new_env = E.push_rel (n', Some s, t) env in
                let new_idrefs = fresh_id''::idrefs in
                 (match Term.kind_of_term d with
                     T.LetIn _ ->
                      aux computeinnertypes (Some fresh_id'') new_passed_letins
                       new_env new_idrefs d
                   | _ -> A.ALetIns
                           (new_passed_letins, aux' new_env new_idrefs d))
           | T.App (h,t) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
              if is_a_Prop innersort then
               add_inner_type fresh_id'' ;
              let
               compute_result_if_eta_expansion_not_required subst residual_args
              =
               let residual_args_not_empty = List.length residual_args > 0 in
               let h' =
                if residual_args_not_empty then
                 aux' env idrefs ~subst:(None,subst) h
                else
                 aux' env idrefs ~subst:(Some fresh_id'',subst) h
               in
                (* maybe all the arguments were used for the explicit *)
                (* named substitution                                 *)
                if residual_args_not_empty then
                 A.AApp (fresh_id'', h'::residual_args)
                else
                 h'
              in
               let t' =
                Array.fold_right (fun x i -> (aux' env idrefs x)::i) t []
               in
                explicit_substitute_and_eta_expand_if_required h
                 (Array.to_list t) t'
                 compute_result_if_eta_expansion_not_required
           | T.Const kn ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
              if is_a_Prop innersort  && expected_available then
               add_inner_type fresh_id'' ;
              let compute_result_if_eta_expansion_not_required _ _ =
               A.AConst (fresh_id'', subst, (uri_of_kernel_name kn Constant))
              in
               let (_,subst') = subst in
                explicit_substitute_and_eta_expand_if_required tt []
                 (List.map snd subst')
                 compute_result_if_eta_expansion_not_required
           | T.Ind (kn,i) ->
              let compute_result_if_eta_expansion_not_required _ _ =
               A.AInd (fresh_id'', subst, (uri_of_kernel_name kn Inductive), i)
              in
               let (_,subst') = subst in
                explicit_substitute_and_eta_expand_if_required tt []
                 (List.map snd subst')
                 compute_result_if_eta_expansion_not_required
           | T.Construct ((kn,i),j) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
              if is_a_Prop innersort  && expected_available then
               add_inner_type fresh_id'' ;
              let compute_result_if_eta_expansion_not_required _ _ =
               A.AConstruct
                (fresh_id'', subst, (uri_of_kernel_name kn Inductive), i, j)
              in
               let (_,subst') = subst in
                explicit_substitute_and_eta_expand_if_required tt []
                 (List.map snd subst')
                 compute_result_if_eta_expansion_not_required
           | T.Case ({T.ci_ind=(kn,i)},ty,term,a) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
              if is_a_Prop innersort then
               add_inner_type fresh_id'' ;
              let a' =
               Array.fold_right (fun x i -> (aux' env idrefs x)::i) a []
              in
               A.ACase
                (fresh_id'', (uri_of_kernel_name kn Inductive), i,
                  aux' env idrefs ty, aux' env idrefs term, a')
           | T.Fix ((ai,i),(f,t,b)) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
              if is_a_Prop innersort then add_inner_type fresh_id'' ;
              let fresh_idrefs =
               Array.init (Array.length t) (function _ -> gen_id seed) in
              let new_idrefs =
               (List.rev (Array.to_list fresh_idrefs)) @ idrefs
              in
               let f' =
                let ids = ref (Termops.ids_of_context env) in
                 Array.map
                  (function
                      N.Anonymous -> Util.error "Anonymous fix function met"
                    | N.Name id as n ->
                       let res = N.Name (Nameops.next_name_away n !ids) in
                        ids := id::!ids ;
                        res
                 ) f
               in
                A.AFix (fresh_id'', i,
                 Array.fold_right
                  (fun (id,fi,ti,bi,ai) i ->
                    let fi' =
                     match fi with
                        N.Name fi -> fi
                      | N.Anonymous -> Util.error "Anonymous fix function met"
                    in
                     (id, fi', ai,
                      aux' env idrefs ti,
                      aux' (E.push_rec_types (f',t,b) env) new_idrefs bi)::i)
                  (Array.mapi
                   (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j),ai.(j))) f'
                  ) []
                 )
           | T.CoFix (i,(f,t,b)) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
              if is_a_Prop innersort then add_inner_type fresh_id'' ;
              let fresh_idrefs =
               Array.init (Array.length t) (function _ -> gen_id seed) in
              let new_idrefs =
               (List.rev (Array.to_list fresh_idrefs)) @ idrefs
              in
               let f' =
                let ids = ref (Termops.ids_of_context env) in
                 Array.map
                  (function
                      N.Anonymous -> Util.error "Anonymous fix function met"
                    | N.Name id as n ->
                       let res = N.Name (Nameops.next_name_away n !ids) in
                        ids := id::!ids ;
                        res
                 ) f
               in
                A.ACoFix (fresh_id'', i,
                 Array.fold_right
                  (fun (id,fi,ti,bi) i ->
                    let fi' =
                     match fi with
                        N.Name fi -> fi
                      | N.Anonymous -> Util.error "Anonymous fix function met"
                    in
                     (id, fi',
                      aux' env idrefs ti,
                      aux' (E.push_rec_types (f',t,b) env) new_idrefs bi)::i)
                  (Array.mapi
                    (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j)) ) f'
                  ) []
                 )
    in
     aux computeinnertypes None [] env idrefs t
;;

let acic_of_cic_context metasenv context t =
 let ids_to_terms = Hashtbl.create 503 in
 let constr_to_ids = Acic.CicHash.create 503 in
 let ids_to_father_ids = Hashtbl.create 503 in
 let ids_to_inner_sorts = Hashtbl.create 503 in
 let ids_to_inner_types = Hashtbl.create 503 in
 let seed = ref 0 in
   acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids
    ids_to_inner_sorts ids_to_inner_types metasenv context t,
   ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
;;

let acic_object_of_cic_object pvars sigma obj =
 let module A = Acic in
  let ids_to_terms = Hashtbl.create 503 in
  let constr_to_ids = Acic.CicHash.create 503 in
  let ids_to_father_ids = Hashtbl.create 503 in
  let ids_to_inner_sorts = Hashtbl.create 503 in
  let ids_to_inner_types = Hashtbl.create 503 in
  let ids_to_conjectures = Hashtbl.create 11 in
  let ids_to_hypotheses = Hashtbl.create 127 in
  let hypotheses_seed = ref 0 in
  let conjectures_seed = ref 0 in
  let seed = ref 0 in
  let acic_term_of_cic_term_context' =
   acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids
    ids_to_inner_sorts ids_to_inner_types pvars in
(*CSC: is this the right env to use? Hhmmm. There is a problem: in    *)
(*CSC: Global.env () the object we are exporting is already defined,  *)
(*CSC: either in the environment or in the named context (in the case *)
(*CSC: of variables. Is this a problem?                               *)
  let env = Global.env () in
  let acic_term_of_cic_term' = acic_term_of_cic_term_context' env [] sigma in
(*CSC: the fresh_id is not stored anywhere. This _MUST_ be fixed using *)
(*CSC: a modified version of the already existent fresh_id function    *)
  let fresh_id () =
   let res = "i" ^ string_of_int !seed in
    incr seed ;
    res
  in
   let aobj =
    match obj with
      A.Constant (id,bo,ty,params) ->
       let abo =
        match bo with
           None -> None
         | Some bo' -> Some (acic_term_of_cic_term' bo' (Some ty))
       in
       let aty = acic_term_of_cic_term' ty None in
        A.AConstant (fresh_id (),id,abo,aty,params)
    | A.Variable (id,bo,ty,params) ->
       let abo =
        match bo with
           Some bo -> Some (acic_term_of_cic_term' bo (Some ty))
         | None -> None
       in
       let aty = acic_term_of_cic_term' ty None in
        A.AVariable (fresh_id (),id,abo,aty,params)
    | A.CurrentProof (id,conjectures,bo,ty) ->
       let aconjectures =
        List.map
         (function (i,canonical_context,term) as conjecture ->
           let cid = "c" ^ string_of_int !conjectures_seed in
            Hashtbl.add ids_to_conjectures cid conjecture ;
            incr conjectures_seed ;
            let canonical_env,idrefs',acanonical_context =
             let rec aux env idrefs =
              function
                 [] -> env,idrefs,[]
               | ((n,decl_or_def) as hyp)::tl ->
                  let hid = "h" ^ string_of_int !hypotheses_seed in
                  let new_idrefs = hid::idrefs in
                   Hashtbl.add ids_to_hypotheses hid hyp ;
                   incr hypotheses_seed ;
                   match decl_or_def with
                       A.Decl t ->
                        let final_env,final_idrefs,atl =
                         aux (Environ.push_rel (Names.Name n,None,t) env)
                          new_idrefs tl
                        in
                         let at =
                          acic_term_of_cic_term_context' env idrefs sigma t None
                         in
                          final_env,final_idrefs,(hid,(n,A.Decl at))::atl
                     | A.Def (t,ty) ->
                        let final_env,final_idrefs,atl =
                         aux
                          (Environ.push_rel (Names.Name n,Some t,ty) env)
                           new_idrefs tl
                        in
                         let at =
                          acic_term_of_cic_term_context' env idrefs sigma t None
                         in
                         let dummy_never_used =
                          let s = "dummy_never_used" in
                           A.ARel (s,99,s,Names.id_of_string s)
                         in
                          final_env,final_idrefs,
                           (hid,(n,A.Def (at,dummy_never_used)))::atl
             in
              aux env [] canonical_context
            in
             let aterm =
              acic_term_of_cic_term_context' canonical_env idrefs' sigma term
               None
             in
              (cid,i,List.rev acanonical_context,aterm)
         ) conjectures in
       let abo = acic_term_of_cic_term_context' env [] sigma bo (Some ty) in
       let aty = acic_term_of_cic_term_context' env [] sigma ty None in
        A.ACurrentProof (fresh_id (),id,aconjectures,abo,aty)
    | A.InductiveDefinition (tys,params,paramsno) ->
       let env' =
        List.fold_right
         (fun (name,_,arity,_) env ->
           Environ.push_rel (Names.Name name, None, arity) env
         ) (List.rev tys) env in
       let idrefs = List.map (function _ -> gen_id seed) tys in
       let atys =
        List.map2
         (fun id (name,inductive,ty,cons) ->
           let acons =
            List.map
             (function (name,ty) ->
               (name,
                 acic_term_of_cic_term_context' ~fake_dependent_products:true
                  env' idrefs Evd.empty ty None)
             ) cons
           in
            (id,name,inductive,acic_term_of_cic_term' ty None,acons)
         ) (List.rev idrefs) tys
       in
       A.AInductiveDefinition (fresh_id (),atys,params,paramsno)
   in
    aobj,ids_to_terms,constr_to_ids,ids_to_father_ids,ids_to_inner_sorts,
     ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses
;;