(* $Id$ *)

open Pp
open Util
open Names
open Univ
open Generic
open Term
open Himsg
open Reduction
open Environ
open Machops

(* Fonctions temporaires pour relier la forme castée de la forme jugement *)
let tjudge_of_cast env = function
  | DOP2 (Cast, b, t) ->
      (match whd_betadeltaiota env t with
	 | DOP0 (Sort s) -> {body=b; typ=s}
	 | DOP2 (Cast, b',t') -> anomaly "Supercast (tjudge_of_cast) [Mach]"
	 | _ -> anomaly "Not a type (tjudge_of_cast) [Mach]")
  | _ -> anomaly "Not casted (tjudge_of_cast)"
	
let tjudge_of_judge env j =
  { body = j.uj_val;
    typ = match whd_betadeltaiota env j.uj_type with
      (* Nécessaire pour ZFC *)
      | DOP0 (Sort s) -> s
      | DOP0 Implicit -> anomaly "Tiens, un implicit"
      | _ -> anomaly "Not a type (tjudge_ofjudge)" }

let vect_lift = Array.mapi lift
let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)

(* Ce type est introduit pour rendre un peu plus lisibles les appels a la
   machine de typage.

   nofix indique si on autorise les points fixes generaux (recarg < 0)
     comme Acc_rec.fw
   nocheck devrait indiquer que l'on cherche juste a calculer le type, sans
     faire toutes les verifications (par exemple, pour l'application, on
     n'a pas a calculer le type des arguments, et les Cast devraient etre
     utilises). Pour l'instant, on fait trop de verifications
   noverify indique qu'il ne faut pas verifier si les contextes sont bien
     castes
   Rem: is_ass a disparu; les fonctions attendant un type retourne
        maintenant un "type_judgement" et non un "judgement" complet
 *)

type 'a mach_flags = {
  nofix : bool;
  nocheck : bool;
  noverify : bool }

(* WARNING: some destCast are not guarded.
   Invariant: assumptions in env are casted (checked when noverify=false) *)
let rec execute mf env cstr =
  let u0 = universes env in
  match kind_of_term cstr with
    | IsMeta n ->
       	let metaty =
          try lookup_meta n env
          with Not_found -> error "A variable remains non instanciated" 
	in
        (match kind_of_term metaty with
           | IsCast (typ,kind) -> 
	       ({ uj_val = cstr; uj_type = typ; uj_kind = kind}, u0)
           | _ ->
	       let (jty,u1) = execute mf env metaty in
	       let k = hnf_constr env jty.uj_type in
	       ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, u1))
	
    | IsRel n -> 
	(relative env n, u0)

    | IsVar id -> 
	(make_judge cstr (snd (lookup_var id env)), u0)
	  
    | IsAbst _ ->
        if evaluable_abst env cstr then 
	  execute mf env (abst_value env cstr)
        else 
	  error "Cannot typecheck an unevaluable abstraction"
	      
    | IsConst _ ->
        (make_judge cstr (type_of_const env cstr), u0)
	  
    | IsMutInd _ ->
	(make_judge cstr (type_of_mind env cstr), u0)
	  
    | IsMutConstruct _ -> 
        (make_judge cstr (type_of_mconstr env cstr), u0)
	  
    | IsMutCase (_,p,c,lf) ->
        let (cj,u1) = execute mf env c in
	let env1 = set_universes u1 env in
        let (pj,u2) = execute mf env1 p in
	let env2 = set_universes u2 env1 in
        let (lfj,u3) = execute_array mf env2 lf in
	let env3 = set_universes u3 env2 in
        (type_of_case env3 pj cj lfj, u3)
  
    | IsFix (vn,i,lar,lfi,vdef) ->
        if mf.nofix & array_exists (fun n -> n < 0) vn then
          error "General Fixpoints not allowed";
        let (larv,vdefv,u1) = execute_fix mf env lar lfi vdef in
        let fix = mkFix vn i larv lfi vdefv in
        check_fix env fix;
	(make_judge fix larv.(i), u1)
	  
    | IsCoFix (i,lar,lfi,vdef) ->
        let (larv,vdefv,u1) = execute_fix mf env lar lfi vdef in
        let cofix = mkCoFix i larv lfi vdefv in
        check_cofix env cofix;
	(make_judge cofix larv.(i), u1)
	  
    | IsSort (Prop c) -> 
	(type_of_proposition c, u0)

    | IsSort (Type u) ->
	type_of_type u u0
	  
    | IsAppL a ->
	let la = Array.length a in
	if la = 0 then error_cant_execute CCI env cstr;
	let hd = a.(0)
	and tl = Array.to_list (Array.sub a 1 (la - 1)) in
	let (j,u1) = execute mf env hd in
	let env1 = set_universes u1 env in
        let (jl,u2) = execute_list mf env1 tl in
	let env2 = set_universes u2 env1 in
	apply_rel_list env2 mf.nocheck jl j
	    
    | IsLambda (name,c1,c2) -> 
        let (j,u1) = execute mf env c1 in
        let var = assumption_of_judgement env j in
	let env1 = push_rel (name,var) (set_universes u1 env) in
        let (j',u2) = execute mf env1 c2 in 
	let env2 = set_universes u2 env1 in
        (abs_rel env2 name var j', u2)
	  
    | IsProd (name,c1,c2) ->
        let (j,u1) = execute mf env c1 in
        let var = assumption_of_judgement env j in
	let env1 = push_rel (name,var) (set_universes u1 env) in
        let (j',u2) = execute mf env1 c2 in
	let env2 = set_universes u2 env1 in
        (gen_rel env2 name var j', u2)
	  
    | IsCast (c,t) ->
        let (cj,u1) = execute mf env c in
	let env1 = set_universes u1 env in
        let (tj,u2) = execute mf env1 t in
	let env2 = set_universes u2 env1 in
        (cast_rel env2 cj tj, u2)
	  
      | _ -> error_cant_execute CCI env cstr
	  
and execute_fix mf env lar lfi vdef =
  let (larj,u1) = execute_array mf env lar in
  let env1 = set_universes u1 env in
  let lara = Array.map (assumption_of_judgement env1) larj in
  let nlara = 
    List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
  let env2 = 
    List.fold_left (fun env nvar -> push_rel nvar env) env1 nlara in
  let (vdefj,u2) = execute_array mf env2 vdef in
  let env3 = set_universes u2 env2 in
  let vdefv = Array.map j_val_only vdefj in
  let u3 = type_fixpoint env3 lfi lara vdefj in
  (lara,vdefv,u3)

and execute_array mf env v =
  let (jl,u1) = execute_list mf env (Array.to_list v) in
  (Array.of_list jl, u1)

and execute_list mf env = function
  | [] -> ([], universes env)
  | c::r -> 
      let (j,u') = execute mf env c in 
      let (jr,u'') = execute_list mf (set_universes u' env) r in
      (j::jr, u'')


(** ICI **)

let flag_fmachine mf env constr = 
  if not mf.noverify then verify_wf_env env; 
  exemeta_rec mf env constr

let flag_fmachine_type mf env constr = 
  if not mf.noverify then verify_wf_env env; 
  let j = exemeta_rec mf env constr in
  type_judgement mf.sigma env j


(* This function castifies the term (nocheck=true).
 * It must be applied to well-formed terms.
 * Casts are all removed before re-computing them. This avoids casting
 * Casts, which leads to terrible inefficiencies. *)
let cast_fmachine (sigma,metamap) env t =
  flag_fmachine
    { nofix = true;
      nocheck = true;
      noverify = true;
      sigma = sigma;
      metamap = metamap}
    env (strip_all_casts t)
    
(* core_fmachine* :
   No general fixpoint allowed; checks that environments are casted *)
let core_fmachine nocheck (sigma,metamap) env constr = 
  flag_fmachine
    { nofix = true;
      nocheck = nocheck;
      noverify = false;
      sigma = sigma;
      metamap = metamap}
    env
    constr

let core_fmachine_type nocheck (sigma,metamap) env constr = 
  flag_fmachine_type
    { nofix = true;
     nocheck = nocheck;
     noverify = false;
     sigma = sigma;
     metamap = metamap}
    env
    constr

(* WITHOUT INFORMATION *)
let fmachine nocheck sig_meta sign constr =
  let j = core_fmachine nocheck sig_meta sign constr in
  { uj_val = strip_all_casts j.uj_val;
    uj_type = strip_all_casts j.uj_type;
    uj_kind = j.uj_kind }

let fmachine_type nocheck sig_meta sign constr =
  let j = core_fmachine_type nocheck sig_meta sign constr in
  type_app strip_all_casts j
    
    
let fexemeta_type sigma metamap env c = 
  fmachine_type true (sigma,metamap) env c

let execute_rec_type sigma env c = 
  fmachine_type false (sigma,[]) env c

let fexecute_type sigma sign c = 
  fmachine_type false (sigma,[]) (gLOB sign) c

let fexemeta sigma metamap env c = 
  fmachine true (sigma,metamap) env c

let execute_rec sigma env c = 
  fmachine false (sigma,[]) env c

let fexecute sigma sign c = 
  fmachine false (sigma,[]) (gLOB sign) c

let type_of_rel_type sigma env c = 
  try 
    let j = core_fmachine_type false (sigma,[]) env c in
    DOP0 (Sort j.typ)
  with Invalid_argument s -> 
    error ("Invalid arg " ^ s)

let type_of_rel sigma env c = 
  try 
    let j = core_fmachine false (sigma,[]) env c in
    nf_betaiota j.uj_type
  with Invalid_argument s -> 
    error ("Invalid arg " ^ s)

let type_of sigma sign c = type_of_rel sigma (gLOB sign) c

let type_of_type sigma sign c = type_of_rel_type sigma (gLOB sign) c


(* Allows general fixpoints to appear in the term *)
let fixfexemeta sigma metamap env constr =
  let j =
    flag_fmachine
      { nofix = false;
       nocheck = true;
       noverify = false;
       sigma = sigma;
       metamap = metamap }
      env
      constr
  in 
  { uj_val = strip_all_casts j.uj_val;
    uj_type = strip_all_casts j.uj_type;
    uj_kind = j.uj_kind }

let unsafe_type_of sigma env c = 
  try 
    nf_betaiota
      (flag_fmachine
	 { nofix = false;
           nocheck = true;
           noverify = true;
	   sigma = sigma;
           metamap = [] }
	 env
	 c).uj_type
  with Invalid_argument s -> 
    error ("Invalid arg " ^ s)
      
let compute_type sigma env c = 
  match c with
    | DOP2(Cast,_,t) -> nf_betaiota t 
    | _ -> unsafe_type_of sigma env c

(* Les fonctions suivantes sont pour l'inversion (inv.ml, gelim.ml, leminv.ml):
   sign_of_sign*
   env_of_env*
   castify_env*
   castify_sign*

   A uniformiser...
 *)

let sign_of_sign sigma sign =
  sign_it
    (fun id a sign ->
       match a with
           DOP2(Cast,t,DOP0 (Sort s)) -> add_sign (id,make_type t s) sign
         | _ -> let j = fexecute sigma sign a in
             (add_sign (id,assumption_of_judgement sigma (gLOB sign) j) sign))
    sign nil_sign


(*
let env_of_env1 is_ass sigma env =
  dbenv_it
    (fun na a env ->
       match a with
           DOP2(Cast,_,_) -> add_rel (na,a) env
         | _ -> let j = execute_rec1 is_ass sigma env a in
             add_rel (na,assumption_of_judgement sigma env j) env)
    env (gLOB(get_globals env))

*)
let env_of_env sigma env =
  dbenv_it
    (fun na a env ->
       let j = execute_rec sigma env a in
         add_rel (na,assumption_of_judgement sigma env j) env)
    env (gLOB(get_globals env))


let castify_sign sigma sign = sign_of_sign sigma sign

let castify_env sigma env =
  let sign = (* castify_sign sigma *) (get_globals env)
  in env_of_env sigma (ENVIRON(sign,get_rels env))


(* Fin fonctions pour l'inversion *)

(**)

let implicit_judgment = {body=mkImplicit;typ=implicit_sort}

let add_inf_rel (na,inf) env =
  match inf with
      Logic -> add_rel (na,implicit_judgment) env
    | Inf j -> add_rel (na,tjudge_of_judge j) env


let fw_mutind sigma fenv k =
  let (sp,x,args) = destMutInd k in
  let mis = mind_specif_of_mind k in
    match mis_singl mis with 
	Some a -> Some (a,true)
      | None ->
	  if is_info_cast_type sigma (mis_arity mis) then
	    let infK =
              global_reference fenv (fwsp_of sp) (id_of_global (MutInd (sp,x)))
	    in Some (infK,false)
	  else None

let inf_of_mind sigma fenv mind = 
  try
    match fw_mutind sigma fenv mind with
        Some (infK,singl) -> Inf(cast_fmachine (sigma,[]) fenv infK)
      | None -> Logic
  with
      Not_found | Failure _ -> 
	anomaly "cannot convert an inductive to an finductive"

let inf_mconstructor (sigma,metamap) fenv k = 
  let (sp,x,i,cl) = destMutConstruct k in
  let mind = mkMutInd sp x cl in 
    (match fw_mutind sigma fenv mind with
         None -> Logic
       | Some(infi,singl) ->
	   (match mind_lamexp mind with
	      | Some clamexp ->
		  if singl
		  then Inf(cast_fmachine (sigma,[]) fenv clamexp)
		  else
		    let (infsp, infx, infcl) = destMutInd infi in
		    let infmconstructor = mkMutConstruct infsp infx i infcl in
		    let infval = subst1 infmconstructor clamexp in
		      Inf (cast_fmachine (sigma,fst metamap) fenv infval)
	      | _ -> assert false))


exception DefinedExtraction

(* when c is an evaluable constant with an extraction which 
   contains an implicit, gives the value of the c constant
   otherwise raise DefinedExtraction
*)

let value_implicit_const sigma c cinf = 
  match c with DOPN(Const(_),_) -> 
    if evaluable_const sigma c then 
      let cv = const_value sigma cinf in 
	if is_implicit cv (* or contains_implicit sigma cv *)
	then const_value sigma c 
	else raise DefinedExtraction
    else raise DefinedExtraction
    | _ -> raise DefinedExtraction

let unsafe_infmachine (sigma,metamap) env fenv c = 
  let rec infexec env fenv cstr = match cstr with
       DOP2(Cast,c,DOP0(Sort(Prop(Null)))) -> Logic
    |  DOP2(Cast,c,DOP2(Cast,_,DOP0(Sort(Prop(Null))))) -> Logic
    |  DOP2(Cast,c,_) -> infexec env fenv c
    |  DOP0(Meta n) ->
         (match List.assoc n (snd metamap) with
             Logic -> Logic
           | Inf j -> Inf{uj_val=DOP0(Meta n);
                          uj_type=j.uj_val;
                          uj_kind = hnf_constr sigma j.uj_type})

    | Rel n ->
        inf_rel fenv
          (contents_of_type sigma (snd (lookup_rel n env))) n

    | VAR str ->
        inf_var fenv
          (contents_of_type sigma (snd(lookup_glob str env))) str

    | DOPN(Const _,_) -> inf_of_const sigma (env,fenv) cstr

    | DOPN(Abst _,_) ->
        if evaluable_abst cstr then infexec env fenv (abst_value cstr)
        else error "cannot extract from an unevaluable abstraction"

    | DOP0(Sort s) -> inf_sort s

    | DOPN(AppL,tl) ->
        let c1 =  (hd_vect tl)
        and cl = tl_vect tl in
          let funinf = infexec env fenv c1 in
            (match funinf with Logic -> Logic
	      | Inf(j) -> let cinf = j.uj_val in
             (* try to expand constants corresponding 
		    to non extractable terms *)
	      (try if is_extraction_expanded() then 
		 let valcte = value_implicit_const sigma c1 cinf 
		 in infexec env fenv (whd_betaiota (appvect(valcte,cl))) 
	       else raise DefinedExtraction
               with DefinedExtraction -> 
		 let argsinf = Array.map (infexec env fenv) cl
		 in it_vect inf_apply funinf argsinf))

    | DOP2(Lambda,c1,DLAM(name,c2)) ->
        let varinf = infexec env fenv c1 in
        let bodyinf = infexec (add_rel (name,tjudge_of_cast sigma c1) env)
                        (add_inf_rel (name,varinf) fenv) c2
        in inf_abs_rel name bodyinf varinf

    | DOP2(Prod,c1,DLAM(name,c2)) ->
        let c1inf = infexec env fenv c1 in
        let c2inf = infexec (add_rel (name,tjudge_of_cast sigma c1) env)
                      (add_inf_rel (name,c1inf) fenv) c2
        in inf_gen_rel name c2inf c1inf

    | DOPN(MutInd _,_) -> inf_of_mind sigma fenv cstr

    | DOPN(MutConstruct _,_) ->
        inf_mconstructor (sigma,metamap) fenv cstr

    | DOPN(Fix(vn,i),cl) ->
        let lar = Array.sub cl 0 ((Array.length cl) - 1) in
        let inflar = Array.map (infexec env fenv) lar in
        let infAi = inflar.(i) in 
          (match infAi with 
              Logic   -> Logic 
            | Inf aij ->
                let (lfi,ldefs) = decomp_all_DLAMV_name (last_vect cl) in
                let (new_env,new_fenv) =
                  it_vect2
                    (fun (ne,nfe) fk ak -> 
                       (add_rel (fk,tjudge_of_cast sigma ak) ne,
                        let infAk = infexec ne nfe ak
                        in (add_inf_rel (fk,infAk) nfe)))
                    (env,fenv)
                    (Array.of_list (List.rev lfi)) (vect_lift lar) in 
(* a special function to localize the recursive index in the extracted term *)
                let rec exec_def ne nfe n def = 
                  (match hnf_constr sigma def with 
                      DOP2(Lambda,c1,DLAM(name,c2)) ->
                        let varinf = infexec ne nfe c1 in
                        let ne' = (add_rel (name,tjudge_of_cast sigma c1) ne) 
                        and nfe' = add_inf_rel (name,varinf) nfe in
                          if n = 0 then
                            let infc2 = infexec ne' nfe' c2 
                            in let infdef = inf_abs_rel name infc2 varinf
                               and index =
                                 if varinf = Logic then -1
                        (* the recursive call was on a non-informative term *) 
                                 else 0 in (infdef,index)
                          else
                            let bodyinf,countl = 
                              exec_def (add_rel (name,tjudge_of_cast sigma c1) ne) 
                                (add_inf_rel (name,varinf) nfe) (n-1) c2 in
                            let (infabs,abs) =
                              inf_abs_rel_count name bodyinf varinf
                            in (infabs,
                                if abs = ERASE then countl
                                else if countl<0 then countl-1
                                else countl+1)
                    | _ -> anomaly "exec_def : should be a lambda") in
                let infdefs_ind =
                  map2_vect (exec_def new_env new_fenv) vn ldefs
                in inf_fix sigma i aij.uj_type lfi inflar infdefs_ind)

    | DOPN(CoFix i,cl) ->
        let lar    = Array.sub cl 0 ((Array.length cl) - 1) in 
        let inflar = Array.map (infexec env fenv) lar in
        let infAi  = inflar.(i) in
          (match infAi with 
              Logic   -> Logic 
            | Inf aij -> 
                let lfi,ldefs = decomp_all_DLAMV_name (last_vect cl) in 
                let (new_env,new_fenv) = 
                  it_vect2 (fun (ne,nfe) fk ak -> 
                              (add_rel (fk,tjudge_of_cast sigma ak) ne, 
                               let infAk = infexec ne nfe ak
                               in (add_inf_rel (fk,infAk) nfe)))
                    (env,fenv) 
                    (Array.of_list (List.rev lfi)) (vect_lift lar) in 
                                   
                let infdefs = Array.map (infexec new_env new_fenv) ldefs 
                in  inf_cofix sigma i aij.uj_type lfi inflar infdefs)

    | DOPN(MutCase _,_) ->
        let (ci,p,c,lf) = destCase cstr in
        let pinf = infexec env fenv p in 
          (match pinf with
              Logic  -> Logic 
            | Inf pj -> 
		if is_extraction_expanded() then 
		  let (d,l) = whd_betadeltaiota_stack sigma c [] in 
                 (match d with (DOPN(MutConstruct(_,_),_)) ->
		    let cstr' = 
		      DOPN(MutCase(ci),Array.append [|p;applist(d,l)|] lf)
		    in infexec env fenv (whd_betaiota cstr')
		    | _ -> 
                  let cinf = infexec env fenv c
                  and lfinf = Array.map (infexec env fenv) lf
                  in inf_mutcase fenv sigma pj ci cinf lfinf
		 )
               else let cinf = infexec env fenv c
                  and lfinf = Array.map (infexec env fenv) lf
                  in inf_mutcase fenv sigma pj ci cinf lfinf)
	 
    | _ -> error "Cannot extract information"
  in infexec env fenv c


let core_infmachine meta env fenv c =
  try unsafe_infmachine meta env fenv c
  with (UserError _ | Failure _) -> Logic

(* WITH INFORMATION *)
(* does not check anymore that extracted terms are well-formed *)
let judgement_infmachine meta env fenv c ct = 
  try
    match unsafe_infmachine meta env fenv c with
        Inf infj ->
          let inftyp =
            try unsafe_infmachine meta env fenv ct
            with (UserError _ | Failure _) ->
              (warning "Failed to extract in type"; Logic)
          in (match inftyp with
                  Inf infjt ->
                    Inf{uj_val=infj.uj_val;
                        uj_type=infjt.uj_val;
                        uj_kind=infj.uj_kind}
                | Logic -> Inf infj)
      | Logic -> Logic
  with (UserError _ | Failure _) -> (warning "Failed to extract"; Logic)

let infmachine_type nocheck (sigma,metamap) env fenv constr =
  let constr_metamap = List.map (fun (id,(c,_)) -> (id,c)) metamap in
  let inf_metamap = List.map (fun (id,(_,i)) -> (id,i)) metamap in
  let t = core_fmachine_type nocheck (sigma,constr_metamap) env constr in
  let inf = 
    if is_info_type sigma t then (* Case the term is informative *)
      let uniarc = get_uniarc () in
      let infjt =
        judgement_infmachine
          (sigma,(constr_metamap,inf_metamap)) env fenv 
	  t.body 
	  (DOP0 (Sort t.typ)) in
      let _ = set_uniarc uniarc in
        infjt
    else Logic

  in hash_jpair_type
       ({body = strip_all_casts t.body; typ = t.typ},
        (inf_app (fun j -> {uj_val = nf_beta j.uj_val;
                            uj_type = nf_beta j.uj_type;
                            uj_kind = j.uj_kind }) inf))

let infmachine nocheck (sigma,metamap) env fenv constr =
  let constr_metamap = List.map (fun (id,(c,_)) -> (id,c)) metamap in
  let inf_metamap = List.map (fun (id,(_,i)) -> (id,i)) metamap in
  let j = core_fmachine nocheck (sigma,constr_metamap) env constr in
  let inf = 
    if is_info_judge sigma j then (* Case the term is informative *)
      let uniarc = get_uniarc () in
      let jt = cast_fmachine (sigma,constr_metamap) env j.uj_type in
      let infjt =
        judgement_infmachine
          (sigma,(constr_metamap,inf_metamap)) env fenv j.uj_val jt.uj_val in
      let _ = set_uniarc uniarc in
        infjt
    else Logic

  in hash_jpair
       ({uj_val = strip_all_casts j.uj_val;
         uj_type = strip_all_casts j.uj_type;
         uj_kind = j.uj_kind},
        (inf_app (fun j -> {uj_val = nf_beta j.uj_val;
                            uj_type = nf_beta j.uj_type;
                            uj_kind = j.uj_kind }) inf))


let jsign_of_sign sigma sign =
  sign_it
    (fun id a (sign,fsign) ->
      let sign' = add_sign (id,a) sign in
      let fsign' =
        match infmachine_type true (sigma,[]) (gLOB sign) (gLOB fsign) a.body
 	with
          (_,Logic) -> fsign
        | (_,Inf ft) -> add_sign (id,tjudge_of_judge ft) fsign
      in (sign',fsign'))
    sign (([],[]),([],[]))


let fsign_of_sign sigma sign = snd (jsign_of_sign sigma sign)

let infexemeta_type sigma metamap (env,fenv) c =
  infmachine_type true (sigma,metamap) env fenv c

let infexecute_rec_type sigma (env,fenv) c =
  infmachine_type false (sigma,[]) env fenv c

let infexecute_type sigma (sign,fsign) c =
  infmachine_type false (sigma,[]) (gLOB sign) (gLOB fsign) c

let infexemeta sigma metamap (env,fenv) c =
  infmachine true (sigma,metamap) env fenv c

let infexecute_rec sigma (env,fenv) c =
  infmachine false (sigma,[]) env fenv c

let infexecute sigma (sign,fsign) c =
  infmachine false (sigma,[]) (gLOB sign) (gLOB fsign) c

(* A adapter pour les nouveaux env
let fvar_type sigma (sign,fsign) v = 
  let na = destVar v in
  let varty = (snd(lookup_sign na sign))
  in match (snd(infexemeta sigma [] (gLOB sign, gLOB fsign) varty)) with
      Inf ft -> ft.uj_val
    | Logic -> invalid_arg "Fvar with a non-informative type (1)!"

*)

(* MACHINE WITH UNIVERSES *)
(* Il vaudrait mieux typer dans le graphe d'univers de Constraintab,
   recuperer le graphe local, et restaurer l'acien graphe global *)

let whd_instuni = function
    DOP0(Sort(Type(u))) ->
      let u = (if u = dummy_univ then new_univ() else u)
      in DOP0(Sort(Type(u)))
  | c -> c

(* Instantiate universes: replace all dummy_univ by fresh universes.
   This is already done by the machine.
   Indtypes instantiates the universes itself, because in the case of
   large constructor, additionnal constraints must be considered. *)
let instantiate_universes c = strong whd_instuni c


(* sp est le nom de la constante pour laquelle il faut que c soit bien type.
   Cela sert a eviter un clash entre le noms d'univers de 2 modules compiles
   independamment.
   Au lieu de sp, Lib.cwd() serait peut-etre suffisant.
   Cela eviterai de donner un section-path quand on veut typer. *)
let fexecute_type_with_univ sigma sign sp c =
  with_universes (fexecute_type sigma sign) (sp,initial_universes,c) 


let fexecute_with_univ sigma sign sp c =
  with_universes (fexecute sigma sign) (sp,initial_universes,c) 


let infexecute_type_with_univ sigma psign sp c =
  with_universes (infexecute_type sigma psign) (sp,initial_universes,c) 


let infexecute_with_univ sigma psign sp c =
  with_universes (infexecute sigma psign) (sp,initial_universes,c)