Merge PR #946: Functional pretyping interface

2 files changed, 6 insertions, 92 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b4d87dfdb0..40b8bcad92 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -47,8 +47,6 @@ open Misctypes
 module NamedDecl = Context.Named.Declaration
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
-type glob_constr_ltac_closure = ltac_var_map * glob_constr
-type pure_open_constr = evar_map * EConstr.constr
 
 (************************************************************************)
 (* This concerns Cases *)
@@ -385,9 +383,6 @@ let adjust_evar_source evdref na c =
      end
   | _, _ -> c
 
-(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
-let allow_anonymous_refs = ref false
-
 (* coerce to tycon if any *)
 let inh_conv_coerce_to_tycon ?loc resolve_tc env evdref j = function
   | None -> j
@@ -918,9 +913,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       (* Make dependencies from arity signature impossible *)
     let arsgn =
       let arsgn,_ = get_arity env.ExtraEnv.env indf in
-	if not !allow_anonymous_refs then
-	  List.map (set_name Anonymous) arsgn
-	else arsgn
+      List.map (set_name Anonymous) arsgn
     in
       let indt = build_dependent_inductive env.ExtraEnv.env indf in
       let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *)
@@ -981,10 +974,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 
       let arsgn =
 	let arsgn,_ = get_arity env.ExtraEnv.env indf in
-	  if not !allow_anonymous_refs then
-	      (* Make dependencies from arity signature impossible *)
-	    List.map (set_name Anonymous) arsgn
-	  else arsgn
+        (* Make dependencies from arity signature impossible *)
+        List.map (set_name Anonymous) arsgn
       in
       let nar = List.length arsgn in
       let indt = build_dependent_inductive env.ExtraEnv.env indf in
@@ -1018,13 +1009,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
         let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in
 	let csgn =
-	  if not !allow_anonymous_refs then
-	    List.map (set_name Anonymous) cs_args
-	  else
-	    List.map (map_name (function Name _ as n -> n
-				       | Anonymous -> Name Namegen.default_non_dependent_ident))
-		     cs_args
-	in
+          List.map (set_name Anonymous) cs_args
+        in
 	let env_c = push_rel_context !evdref csgn env in
 	let bj = pretype (mk_tycon pi) env_c evdref lvar b in
 	  it_mkLambda_or_LetIn bj.uj_val cs_args in
@@ -1191,29 +1177,6 @@ let no_classes_no_fail_inference_flags = {
 let all_and_fail_flags = default_inference_flags true
 let all_no_fail_flags = default_inference_flags false
 
-let on_judgment sigma f j =
-  let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in
-  let (c,_,t) = destCast sigma (f c) in
-  {uj_val = c; uj_type = t}
-
-let understand_judgment env sigma c =
-  let env = make_env env sigma in
-  let evdref = ref sigma in
-  let k0 = Context.Rel.length (rel_context env) in
-  let j = pretype k0 true empty_tycon env evdref empty_lvar c in
-  let j = on_judgment sigma (fun c ->
-    let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in 
-      evdref := evd; c) j
-  in j, Evd.evar_universe_context !evdref
-
-let understand_judgment_tcc env evdref c =
-  let env = make_env env !evdref in
-  let k0 = Context.Rel.length (rel_context env) in
-  let j = pretype k0 true empty_tycon env evdref empty_lvar c in
-  on_judgment !evdref (fun c ->
-    let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in
-    evdref := evd; c) j
-
 let ise_pretype_gen_ctx flags env sigma lvar kind c =
   let evd, c = ise_pretype_gen flags env sigma lvar kind c in
   let evd, f = Evarutil.nf_evars_and_universes evd in
@@ -1231,36 +1194,10 @@ let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutT
   let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in
   (sigma, c)
 
-let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c =
-  let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in
-  evdref := sigma;
-  c
-
 let understand_ltac flags env sigma lvar kind c =
   let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in
   (sigma, c)
 
-let constr_flags = {
-  use_typeclasses = true;
-  solve_unification_constraints = true;
-  use_hook = None;
-  fail_evar = true;
-  expand_evars = true }
-
-(* Fully evaluate an untyped constr *)
-let type_uconstr ?(flags = constr_flags)
-  ?(expected_type = WithoutTypeConstraint) ist c =
-  begin fun env sigma ->
-  let { closure; term } = c in
-  let vars = {
-    ltac_constrs = closure.typed;
-    ltac_uconstrs = closure.untyped;
-    ltac_idents = closure.idents;
-    ltac_genargs = Id.Map.empty;
-  } in
-  understand_ltac flags env sigma vars expected_type term
-  end
-
 let pretype k0 resolve_tc typcon env evdref lvar t =
   pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 6e533f1784..7395e94a09 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -27,9 +27,6 @@ val search_guard :
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
-type glob_constr_ltac_closure = ltac_var_map * glob_constr
-type pure_open_constr = evar_map * constr
-
 type inference_hook = env -> evar_map -> evar -> evar_map * constr
 
 type inference_flags = {
@@ -48,9 +45,6 @@ val all_no_fail_flags : inference_flags
 
 val all_and_fail_flags : inference_flags
 
-(** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
-val allow_anonymous_refs : bool ref
-  
 (** Generic calls to the interpreter from glob_constr to open_constr;
     by default, inference_flags tell to use type classes and
     heuristics (but no external tactic solver hooks), as well as to
@@ -61,9 +55,6 @@ val allow_anonymous_refs : bool ref
 val understand_tcc : ?flags:inference_flags -> env -> evar_map ->
   ?expected_type:typing_constraint -> glob_constr -> evar_map * constr
 
-val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref ->
-  ?expected_type:typing_constraint -> glob_constr -> constr
-
 (** More general entry point with evars from ltac *)
 
 (** Generic call to the interpreter from glob_constr to constr
@@ -78,7 +69,7 @@ val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref ->
 
 val understand_ltac : inference_flags ->
   env -> evar_map -> ltac_var_map ->
-  typing_constraint -> glob_constr -> pure_open_constr
+  typing_constraint -> glob_constr -> evar_map * EConstr.t
 
 (** Standard call to get a constr from a glob_constr, resolving
     implicit arguments and coercions, and compiling pattern-matching;
@@ -90,20 +81,6 @@ val understand_ltac : inference_flags ->
 val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
   env -> evar_map -> glob_constr -> Constr.constr Evd.in_evar_universe_context
 
-(** Idem but returns the judgment of the understood term *)
-
-val understand_judgment : env -> evar_map -> 
-  glob_constr -> unsafe_judgment Evd.in_evar_universe_context
-
-(** Idem but do not fail on unresolved evars (type cl*)
-val understand_judgment_tcc : env -> evar_map ref ->
-  glob_constr -> unsafe_judgment
-
-val type_uconstr :
-  ?flags:inference_flags ->
-  ?expected_type:typing_constraint ->
-  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open
-
 (** Trying to solve remaining evars and remaining conversion problems
     possibly using type classes, heuristics, external tactic solver
     hook depending on given flags. *)