path: root/pretyping/pretyping.ml

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id: pretyping.ml 8875 2006-05-29 19:59:11Z msozeau $ *)

open Pp
open Util
open Names
open Sign
open Evd
open Term
open Termops
open Reductionops
open Environ
open Type_errors
open Typeops
open Libnames
open Nameops
open Classops
open List
open Recordops 
open Evarutil
open Pretype_errors
open Rawterm
open Evarconv
open Pattern
open Dyn

type typing_constraint = OfType of types option | IsType
type var_map = (identifier * unsafe_judgment) list
type unbound_ltac_var_map = (identifier * identifier option) list

(************************************************************************)
(* This concerns Cases *)
open Declarations
open Inductive
open Inductiveops

(************************************************************************)

(* To embed constr in rawconstr *)
let ((constr_in : constr -> Dyn.t),
     (constr_out : Dyn.t -> constr)) = create "constr"

(** Miscellaneous interpretation functions *)
  
let interp_sort = function
  | RProp c -> Prop c
  | RType _ -> new_Type_sort ()
      
let interp_elimination_sort = function
  | RProp Null -> InProp
  | RProp Pos  -> InSet
  | RType _ -> InType

module type S = 
sig

  module Cases : Cases.S
  
  (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
  val allow_anonymous_refs : bool ref

  (* Generic call to the interpreter from rawconstr to open_constr, leaving
     unresolved holes as evars and returning the typing contexts of
     these evars. Work as [understand_gen] for the rest. *)
  
  val understand_tcc :
    evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr

  val understand_tcc_evars :
    evar_defs ref -> env -> typing_constraint -> rawconstr -> constr
    
  (* More general entry point with evars from ltac *)
    
  (* Generic call to the interpreter from rawconstr to constr, failing
     unresolved holes in the rawterm cannot be instantiated.
     
     In [understand_ltac sigma env ltac_env constraint c],
     
     sigma : initial set of existential variables (typically dependent subgoals)
     ltac_env : partial substitution of variables (used for the tactic language)
     constraint : tell if interpreted as a possibly constrained term or a type 
  *)
    
  val understand_ltac :
    evar_map -> env -> var_map * unbound_ltac_var_map ->
    typing_constraint -> rawconstr -> evar_defs * constr
    
  (* Standard call to get a constr from a rawconstr, resolving implicit args *)
    
  val understand : evar_map -> env -> ?expected_type:Term.types ->
    rawconstr -> constr
    
  (* Idem but the rawconstr is intended to be a type *)
    
  val understand_type : evar_map -> env -> rawconstr -> constr
    
  (* A generalization of the two previous case *)
    
  val understand_gen : typing_constraint -> evar_map -> env -> 
    rawconstr -> constr
    
  (* Idem but returns the judgment of the understood term *)
    
  val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment

  (* Idem but do not fail on unresolved evars *)

  val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment

  (*i*)
  (* Internal of Pretyping...
   * Unused outside, but useful for debugging
   *)
  val pretype : 
    type_constraint -> env -> evar_defs ref -> 
    var_map * (identifier * identifier option) list ->
    rawconstr -> unsafe_judgment
    
  val pretype_type : 
    val_constraint -> env -> evar_defs ref ->
    var_map * (identifier * identifier option) list ->
    rawconstr -> unsafe_type_judgment

  val pretype_gen :
    evar_defs ref -> env -> 
    var_map * (identifier * identifier option) list ->
    typing_constraint -> rawconstr -> constr

    (*i*)
end

module Pretyping_F (Coercion : Coercion.S) = struct

  module Cases = Cases.Cases_F(Coercion)

  (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
  let allow_anonymous_refs = ref false

  let evd_comb0 f isevars =
    let (evd',x) = f !isevars in
      isevars := evd';
      x

  let evd_comb1 f isevars x =
    let (evd',y) = f !isevars x in
      isevars := evd';
      y

  let evd_comb2 f isevars x y =
    let (evd',z) = f !isevars x y in
      isevars := evd';
      z

  let evd_comb3 f isevars x y z =
    let (evd',t) = f !isevars x y z in
      isevars := evd';
      t
	
  let mt_evd = Evd.empty
    
  let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
      
  (* Utilisé pour inférer le prédicat des Cases *)
  (* Semble exagérement fort *)
  (* Faudra préférer une unification entre les types de toutes les clauses *)
  (* et autoriser des ? à rester dans le résultat de l'unification *)
  
  let evar_type_fixpoint loc env isevars lna lar vdefj =
    let lt = Array.length vdefj in 
      if Array.length lar = lt then 
	for i = 0 to lt-1 do 
          if not (e_cumul env isevars (vdefj.(i)).uj_type
		    (lift lt lar.(i))) then
            error_ill_typed_rec_body_loc loc env (evars_of !isevars)
              i lna vdefj lar
	done

  let check_branches_message loc env isevars c (explft,lft) = 
    for i = 0 to Array.length explft - 1 do
      if not (e_cumul env isevars lft.(i) explft.(i)) then 
	let sigma = evars_of !isevars in
	  error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
    done

  (* coerce to tycon if any *)
  let inh_conv_coerce_to_tycon loc env isevars j = function
    | None -> j
    | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t

  let push_rels vars env = List.fold_right push_rel vars env

  (*
    let evar_type_case isevars env ct pt lft p c =
    let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c
    in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
  *)

  let strip_meta id = (* For Grammar v7 compatibility *)
    let s = string_of_id id in
      if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
      else id

  let pretype_id loc env (lvar,unbndltacvars) id =
    let id = strip_meta id in (* May happen in tactics defined by Grammar *)
      try
	let (n,typ) = lookup_rel_id id (rel_context env) in
	  { uj_val  = mkRel n; uj_type = type_app (lift n) typ }
      with Not_found ->
	try
	  List.assoc id lvar
	with Not_found ->
	  try
	    let (_,_,typ) = lookup_named id env in
	      { uj_val  = mkVar id; uj_type = typ }
	  with Not_found ->
	    try (* To build a nicer ltac error message *)
	      match List.assoc id unbndltacvars with
		| None -> user_err_loc (loc,"",
					str "variable " ++ pr_id id ++ str " should be bound to a term")
		| Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
	    with Not_found ->
	      error_var_not_found_loc loc id

  (* make a dependent predicate from an undependent one *)

  let make_dep_of_undep env (IndType (indf,realargs)) pj =
    let n = List.length realargs in
    let rec decomp n p =
      if n=0 then p else
	match kind_of_term p with
	  | Lambda (_,_,c) -> decomp (n-1) c
	  | _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1])) 
    in
    let sign,s = decompose_prod_n n pj.uj_type in
    let ind = build_dependent_inductive env indf in
    let s' = mkProd (Anonymous, ind, s) in
    let ccl = lift 1 (decomp n pj.uj_val) in
    let ccl' = mkLambda (Anonymous, ind, ccl) in
      {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign} 

  (*************************************************************************)
  (* Main pretyping function                                               *)

  let pretype_ref isevars env ref = 
    let c = constr_of_global ref in
      make_judge c (Retyping.get_type_of env Evd.empty c)

  let pretype_sort = function
    | RProp c -> judge_of_prop_contents c
    | RType _ -> judge_of_new_Type ()

  (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
  (* in environment [env], with existential variables [(evars_of isevars)] and *)
  (* the type constraint tycon *)
  let rec pretype (tycon : type_constraint) env isevars lvar = function
    | RRef (loc,ref) ->
	inh_conv_coerce_to_tycon loc env isevars
	  (pretype_ref isevars env ref)
	  tycon

    | RVar (loc, id) ->
	inh_conv_coerce_to_tycon loc env isevars
	  (pretype_id loc env lvar id)
	  tycon

    | REvar (loc, ev, instopt) ->
	(* Ne faudrait-il pas s'assurer que hyps est bien un
	   sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
	let hyps = evar_context (Evd.find (evars_of !isevars) ev) in
	let args = match instopt with
          | None -> instance_from_named_context hyps
          | Some inst -> failwith "Evar subtitutions not implemented" in
	let c = mkEvar (ev, args) in
	let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
	  inh_conv_coerce_to_tycon loc env isevars j tycon

    | RPatVar (loc,(someta,n)) -> 
	anomaly "Found a pattern variable in a rawterm to type"
	  
    | RHole (loc,k) ->
	let ty =
          match tycon with 
            | Some (None, ty) -> ty
            | None | Some _ ->
		e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in
	  { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }

    | RRec (loc,fixkind,names,bl,lar,vdef) ->
	let rec type_bl env ctxt = function
            [] -> ctxt
          | (na,None,ty)::bl ->
              let ty' = pretype_type empty_valcon env isevars lvar ty in
              let dcl = (na,None,ty'.utj_val) in
		type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
          | (na,Some bd,ty)::bl ->
              let ty' = pretype_type empty_valcon env isevars lvar ty in
              let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in
              let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
		type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
	let ctxtv = Array.map (type_bl env empty_rel_context) bl in
	let larj =
          array_map2
            (fun e ar ->
               pretype_type empty_valcon (push_rel_context e env) isevars lvar ar)
            ctxtv lar in
	let lara = Array.map (fun a -> a.utj_val) larj in
	let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
	let nbfix = Array.length lar in
	let names = Array.map (fun id -> Name id) names in
	  (* Note: bodies are not used by push_rec_types, so [||] is safe *)
	let newenv = push_rec_types (names,ftys,[||]) env in
	let vdefj =
	  array_map2_i 
	    (fun i ctxt def ->
               (* we lift nbfix times the type in tycon, because of
		* the nbfix variables pushed to newenv *)
               let (ctxt,ty) =
		 decompose_prod_n_assum (rel_context_length ctxt)
                   (lift nbfix ftys.(i)) in
               let nenv = push_rel_context ctxt newenv in
               let j = pretype (mk_tycon ty) nenv isevars lvar def in
		 { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
		   uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
            ctxtv vdef in
	evar_type_fixpoint loc env isevars names ftys vdefj;
	let fixj = match fixkind with
	  | RFix (vn,i) ->
	      let guard_indexes = Array.mapi 
		(fun i (n,_) -> match n with 
		   | Some n -> n 
		   | None -> 
		       (* Recursive argument was not given by the user : We
			  check that there is only one inductive argument *)
		       let ctx = ctxtv.(i) in 
		       let isIndApp t = 
			 isInd (fst (decompose_app (strip_head_cast t))) in
			 (* This could be more precise (e.g. do some delta) *)
		       let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in
		       try (list_unique_index true lb) - 1
		       with Not_found -> 
			 Util.user_err_loc
			   (loc,"pretype",
			    Pp.str "cannot guess decreasing argument of fix"))
		vn 
	      in
	      let fix = ((guard_indexes, i),(names,ftys,Array.map j_val vdefj)) in
	      (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
	      make_judge (mkFix fix) ftys.(i)
	  | RCoFix i -> 
	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
	      make_judge (mkCoFix cofix) ftys.(i) in
	inh_conv_coerce_to_tycon loc env isevars fixj tycon

    | RSort (loc,s) ->
	inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon

    | RApp (loc,f,args) -> 
	let fj = pretype empty_tycon env isevars lvar f in
 	let floc = loc_of_rawconstr f in
	let rec apply_rec env n resj = function
	  | [] -> resj
	  | c::rest ->
	      let argloc = loc_of_rawconstr c in
	      let resj = evd_comb1 (Coercion.inh_app_fun env) isevars resj in
              let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
      		match kind_of_term resty with
		  | Prod (na,c1,c2) ->
		      let hj = pretype (mk_tycon c1) env isevars lvar c in
		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
		      let typ' = nf_isevar !isevars typ in
			apply_rec env (n+1) 
			  { uj_val = nf_isevar !isevars value;
			    uj_type = typ' }
			  rest
		  | _ ->
		      let hj = pretype empty_tycon env isevars lvar c in
			error_cant_apply_not_functional_loc 
			  (join_loc floc argloc) env (evars_of !isevars)
	      		  resj [hj]
	in
	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in
	let resj =
	  match kind_of_term resj.uj_val with
	  | App (f,args) when isInd f ->
	      let sigma = evars_of !isevars in
	      let t = Retyping.type_of_inductive_knowing_parameters env sigma (destInd f) args in
	      let s = snd (splay_arity env sigma t) in
	      on_judgment_type (set_inductive_level env s) resj
		(* Rem: no need to send sigma: no head evar, it's an arity *)
	  | _ -> resj in
	inh_conv_coerce_to_tycon loc env isevars resj tycon

    | RLambda(loc,name,c1,c2)      ->
	let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
	let dom_valcon = valcon_of_tycon dom in
	let j = pretype_type dom_valcon env isevars lvar c1 in
	let var = (name,None,j.utj_val) in
	let j' = pretype rng (push_rel var env) isevars lvar c2 in 
	  judge_of_abstraction env name j j'

    | RProd(loc,name,c1,c2)        ->
	let j = pretype_type empty_valcon env isevars lvar c1 in
	let var = (name,j.utj_val) in
	let env' = push_rel_assum var env in
	let j' = pretype_type empty_valcon env' isevars lvar c2 in
	let resj =
	  try judge_of_product env name j j'
	  with TypeError _ as e -> Stdpp.raise_with_loc loc e in
	  inh_conv_coerce_to_tycon loc env isevars resj tycon
	    
    | RLetIn(loc,name,c1,c2)      ->
	let j = pretype empty_tycon env isevars lvar c1 in
	let t = refresh_universes j.uj_type in
	let var = (name,Some j.uj_val,t) in
        let tycon = lift_tycon 1 tycon in
	let j' = pretype tycon (push_rel var env) isevars lvar c2 in
	  { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
	    uj_type = subst1 j.uj_val j'.uj_type }

    | RLetTuple (loc,nal,(na,po),c,d) ->
	let cj = pretype empty_tycon env isevars lvar c in
	let (IndType (indf,realargs)) = 
	  try find_rectype env (evars_of !isevars) cj.uj_type
	  with Not_found ->
	    let cloc = loc_of_rawconstr c in
	      error_case_not_inductive_loc cloc env (evars_of !isevars) cj 
	in
	let cstrs = get_constructors env indf in
	  if Array.length cstrs <> 1 then
            user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor");
	  let cs = cstrs.(0) in
	    if List.length nal <> cs.cs_nargs then
              user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables");
	    let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
              (List.rev nal) cs.cs_args in
	    let env_f = push_rels fsign env in
	      (* Make dependencies from arity signature impossible *)
	    let arsgn =
	      let arsgn,_ = get_arity env indf in
		if not !allow_anonymous_refs then
		  List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
		else arsgn
	    in
	    let psign = (na,None,build_dependent_inductive env indf)::arsgn in
	    let nar = List.length arsgn in
	      (match po with
		 | Some p ->
		     let env_p = push_rels psign env in
		     let pj = pretype_type empty_valcon env_p isevars lvar p in
		     let ccl = nf_evar (evars_of !isevars) pj.utj_val in
		     let psign = make_arity_signature env true indf in (* with names *)
		     let p = it_mkLambda_or_LetIn ccl psign in
		     let inst = 
		       (Array.to_list cs.cs_concl_realargs)
		       @[build_dependent_constructor cs] in
		     let lp = lift cs.cs_nargs p in
		     let fty = hnf_lam_applist env (evars_of !isevars) lp inst in
		     let fj = pretype (mk_tycon fty) env_f isevars lvar d in
		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
		     let v =
		       let mis,_ = dest_ind_family indf in
		       let ci = make_default_case_info env LetStyle mis in
			 mkCase (ci, p, cj.uj_val,[|f|]) in 
		       { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }

		 | None -> 
		     let tycon = lift_tycon cs.cs_nargs tycon in
		     let fj = pretype tycon env_f isevars lvar d in
		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
		     let ccl = nf_evar (evars_of !isevars) fj.uj_type in
		     let ccl =
		       if noccur_between 1 cs.cs_nargs ccl then
			 lift (- cs.cs_nargs) ccl 
		       else
			 error_cant_find_case_type_loc loc env (evars_of !isevars) 
			   cj.uj_val in
		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
		     let v =
		       let mis,_ = dest_ind_family indf in
		       let ci = make_default_case_info env LetStyle mis in
			 mkCase (ci, p, cj.uj_val,[|f|] ) 
		     in
		       { uj_val = v; uj_type = ccl })

    | RIf (loc,c,(na,po),b1,b2) ->
	let cj = pretype empty_tycon env isevars lvar c in
	let (IndType (indf,realargs)) = 
	  try find_rectype env (evars_of !isevars) cj.uj_type
	  with Not_found ->
	    let cloc = loc_of_rawconstr c in
	      error_case_not_inductive_loc cloc env (evars_of !isevars) cj in
	let cstrs = get_constructors env indf in 
	  if Array.length cstrs <> 2 then
            user_err_loc (loc,"",
			  str "If is only for inductive types with two constructors");

	  let arsgn = 
	    let arsgn,_ = get_arity env indf in
	      if not !allow_anonymous_refs then
		(* Make dependencies from arity signature impossible *)
		List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn 
	      else arsgn
	  in
	  let nar = List.length arsgn in
	  let psign = (na,None,build_dependent_inductive env indf)::arsgn in
	  let pred,p = match po with
	    | Some p ->
		let env_p = push_rels psign env in
		let pj = pretype_type empty_valcon env_p isevars lvar p in
		let ccl = nf_evar (evars_of !isevars) pj.utj_val in
		let pred = it_mkLambda_or_LetIn ccl psign in
		let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
		let jtyp = inh_conv_coerce_to_tycon loc env isevars {uj_val = pred;
								     uj_type = typ} tycon 
		in
		  jtyp.uj_val, jtyp.uj_type
	    | None -> 
		let p = match tycon with
		  | Some (None, ty) -> ty
		  | None | Some _ ->
                      e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
		in
		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
	  let pred = nf_evar (evars_of !isevars) pred in
	  let p = nf_evar (evars_of !isevars) p in
	 (*   msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
	  let f cs b =
	    let n = rel_context_length cs.cs_args in
	    let pi = lift n pred in (* liftn n 2 pred ? *)
	    let pi = beta_applist (pi, [build_dependent_constructor cs]) in
	    let csgn = 
	      if not !allow_anonymous_refs then
		List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args 
	      else 
		List.map 
		  (fun (n, b, t) ->
		     match n with
                         Name _ -> (n, b, t)
                       | Anonymous -> (Name (id_of_string "H"), b, t))
		cs.cs_args
	    in
	    let env_c = push_rels csgn env in 
(* 	      msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *)
	    let bj = pretype (mk_tycon pi) env_c isevars lvar b in
	      it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
	  let b1 = f cstrs.(0) b1 in
	  let b2 = f cstrs.(1) b2 in
	  let v =
	    let mis,_ = dest_ind_family indf in
	    let ci = make_default_case_info env IfStyle mis in
	      mkCase (ci, pred, cj.uj_val, [|b1;b2|])
	  in
	    { uj_val = v; uj_type = p }

    | RCases (loc,po,tml,eqns) ->
	Cases.compile_cases loc
	  ((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
	  tycon env (* loc *) (po,tml,eqns)

    | RCast(loc,c,k,t) ->
	let cj =
	  match k with
	      CastCoerce ->
		let cj = pretype empty_tycon env isevars lvar c in
		  evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj
	    | CastConv k ->
		let tj = pretype_type empty_valcon env isevars lvar t in
		let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
		  (* User Casts are for helping pretyping, experimentally not to be kept*)
		  (* ... except for Correctness *)
		let v = mkCast (cj.uj_val, k, tj.utj_val) in
		  { uj_val = v; uj_type = tj.utj_val }
	in
	  inh_conv_coerce_to_tycon loc env isevars cj tycon

    | RDynamic (loc,d) ->
	if (tag d) = "constr" then
	  let c = constr_out d in
	  let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
	    j
	      (*inh_conv_coerce_to_tycon loc env isevars j tycon*)
	else
	  user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic"))

  (* [pretype_type valcon env isevars lvar c] coerces [c] into a type *)
  and pretype_type valcon env isevars lvar = function
    | RHole loc ->
	(match valcon with
	   | Some v ->
               let s =
		 let sigma = evars_of !isevars in
		 let t = Retyping.get_type_of env sigma v in
		   match kind_of_term (whd_betadeltaiota env sigma t) with
                     | Sort s -> s
                     | Evar v when is_Type (existential_type sigma v) -> 
			 evd_comb1 (define_evar_as_sort) isevars v
                     | _ -> anomaly "Found a type constraint which is not a type"
               in
		 { utj_val = v;
		   utj_type = s }
	   | None ->
	       let s = new_Type_sort () in
		 { utj_val = e_new_evar isevars env ~src:loc (mkSort s);
		   utj_type = s})
    | c ->
	let j = pretype empty_tycon env isevars lvar c in
	let loc = loc_of_rawconstr c in
	let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) isevars j in
	  match valcon with
	    | None -> tj
	    | Some v ->
		if e_cumul env isevars v tj.utj_val then tj
		else
		  error_unexpected_type_loc
                    (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v

  let pretype_gen isevars env lvar kind c =
    let c' = match kind with
      | OfType exptyp ->
	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
	    (pretype tycon env isevars lvar c).uj_val
      | IsType ->
	  (pretype_type empty_valcon env isevars lvar c).utj_val in
      nf_evar (evars_of !isevars) c'

  (* [check_evars] fails if some unresolved evar remains *)
  (* it assumes that the defined existentials have already been substituted
     (should be done in unsafe_infer and unsafe_infer_type) *)

  let check_evars env initial_sigma isevars c =
    let sigma = evars_of !isevars in
    let rec proc_rec c =
      match kind_of_term c with
	| Evar (ev,args) ->
            assert (Evd.mem sigma ev);
	    if not (Evd.mem initial_sigma ev) then
              let (loc,k) = evar_source ev !isevars in
		error_unsolvable_implicit loc env sigma k
	| _ -> iter_constr proc_rec c
    in
      proc_rec c(*;
		  let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in
		  if pbs <> [] then begin
		  pperrnl
		  (str"TYPING OF "++Termops.print_constr_env env c++fnl()++
		  prlist_with_sep fnl
		  (fun  (pb,c1,c2) ->
		  Termops.print_constr c1 ++
		  (if pb=Reduction.CUMUL then str " <="++ spc()
		  else str" =="++spc()) ++
		  Termops.print_constr c2)
		  pbs ++ fnl())
		  end*)

  (* TODO: comment faire remonter l'information si le typage a resolu des
     variables du sigma original. il faudrait que la fonction de typage
     retourne aussi le nouveau sigma...
  *)

  let understand_judgment sigma env c =
    let isevars = ref (create_evar_defs sigma) in
    let j = pretype empty_tycon env isevars ([],[]) c in
    let j = j_nf_evar (evars_of !isevars) j in
      check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
      j

  let understand_judgment_tcc isevars env c =
    let j = pretype empty_tycon env isevars ([],[]) c in
    let sigma = evars_of !isevars in
    let j = j_nf_evar sigma j in
      j

  (* Raw calls to the unsafe inference machine: boolean says if we must
     fail on unresolved evars; the unsafe_judgment list allows us to
     extend env with some bindings *)

  let ise_pretype_gen fail_evar sigma env lvar kind c =
    let isevars = ref (Evd.create_evar_defs sigma) in
    let c = pretype_gen isevars env lvar kind c in
      if fail_evar then check_evars env sigma isevars c;
      !isevars, c

  (** Entry points of the high-level type synthesis algorithm *)

  let understand_gen kind sigma env c =
    snd (ise_pretype_gen true sigma env ([],[]) kind c)

  let understand sigma env ?expected_type:exptyp c =
    snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c)

  let understand_type sigma env c =
    snd (ise_pretype_gen true sigma env ([],[]) IsType c)

  let understand_ltac sigma env lvar kind c =
    ise_pretype_gen false sigma env lvar kind c
      
  let understand_tcc_evars isevars env kind c =
    pretype_gen isevars env ([],[]) kind c

  let understand_tcc sigma env ?expected_type:exptyp c =
    let ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
      Evd.evars_of ev, t
end

module Default : S = Pretyping_F(Coercion.Default)