aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml8
-rw-r--r--proofs/evar_refiner.ml2
-rw-r--r--proofs/logic.ml8
-rw-r--r--proofs/logic.mli4
-rw-r--r--proofs/proof_trees.ml2
-rw-r--r--proofs/refiner.ml2
-rw-r--r--proofs/tacmach.ml14
-rw-r--r--proofs/tacmach.mli3
-rw-r--r--proofs/typing_ev.ml154
-rw-r--r--proofs/typing_ev.mli18
10 files changed, 27 insertions, 188 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 4c14040bdd..80aae11823 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -33,7 +33,7 @@ type 'a clausenv = {
type wc = walking_constraints
let new_evar_in_sign env =
- let hyps = get_globals (Environ.context env) in
+ let hyps = Environ.var_context env in
let ev = new_evar () in
DOPN(Evar ev,
Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps)))
@@ -881,10 +881,10 @@ let clenv_type_of ce c =
| (n,Cltyp typ) -> (n,typ.rebus))
(intmap_to_list ce.env)
in
- failwith "TODO: clenv_type_of"
+ failwith "TODO"
(***
- (Trad.ise_resolve true (w_Underlying ce.hook) metamap
- (gLOB(w_hyps ce.hook)) c)._TYPE
+ (Pretyping.ise_resolve true (w_Underlying ce.hook) metamap
+ (gLOB(w_hyps ce.hook)) c).uj_type
***)
let clenv_instance_type_of ce c =
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index f3421cfdcc..e63648576d 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -10,7 +10,7 @@ open Term
open Environ
open Evd
open Reduction
-open Typing_ev
+open Typing
open Proof_trees
open Logic
open Refiner
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b0823c1b2d..f89c6e9b4e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -10,7 +10,7 @@ open Term
open Sign
open Environ
open Reduction
-open Typing_ev
+open Typing
open Proof_trees
open Typeops
open Coqast
@@ -215,7 +215,7 @@ let move_after with_dep toleft (left,htfrom,right) hto =
let prim_refiner r sigma goal =
let env = goal.evar_env in
- let sign = get_globals (context env) in
+ let sign = var_context env in
let cl = goal.evar_concl in
let info = goal.evar_info in
match r with
@@ -401,8 +401,8 @@ let prim_refiner r sigma goal =
| _ -> anomaly "prim_refiner: Unrecognized primitive rule"
let abst_value c =
- let env = Global.env () in
- Environ.abst_value (Typing.unsafe_env_of_env env) c
+ let env = Global.unsafe_env () in
+ Environ.abst_value env c
let extract_constr =
let rec crec vl = function
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 2b2f9b8b44..88b632882e 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -15,8 +15,8 @@ open Proof_trees
val prim_refiner : prim_rule -> 'a evar_map -> goal -> goal list
val prim_extractor :
- ((typed_type, constr) env -> proof_tree -> constr) ->
- (typed_type, constr) env -> proof_tree -> constr
+ ((typed_type, constr) sign -> proof_tree -> constr) ->
+ (typed_type, constr) sign -> proof_tree -> constr
val extract_constr : constr assumptions -> constr -> constr
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 3523f42182..ee0f3de895 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -8,7 +8,7 @@ open Sign
open Evd
open Stamps
open Environ
-open Typing_ev
+open Typing
type bindOcc =
| Dep of identifier
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 834ee67343..1dc43f4134 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -714,7 +714,7 @@ let extract_pftreestate pts =
[< 'sTR"Cannot extract from a proof-tree in which we have descended;" ;
'sPC; 'sTR"Please ascend to the root" >];
let env = pts.tpf.goal.evar_env in
- let hyps = get_globals (Environ.context env) in
+ let hyps = Environ.var_context env in
strong whd_betadeltatiota env (ts_it pts.tpfsigma)
(extract_proof hyps pts.tpf)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8bb6fba486..85f2973c03 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -11,7 +11,7 @@ open Instantiate
open Environ
open Reduction
open Evd
-open Typing_ev
+open Typing
open Tacred
open Proof_trees
open Logic
@@ -45,7 +45,7 @@ let pf_concl gls = (sig_it gls).evar_concl
let pf_untyped_hyps gls =
let env = pf_env gls in
- let (idl,tyl) = get_globals (Environ.context env) in
+ let (idl,tyl) = Environ.var_context env in
(idl, List.map (fun x -> x.body) tyl)
let pf_nth_hyp gls n = nth_sign (pf_untyped_hyps gls) n
@@ -69,6 +69,14 @@ let hnf_type_of gls =
let pf_check_type gls c1 c2 =
let casted = mkCast c1 c2 in pf_type_of gls casted
+let pf_constr_of_com gls c =
+ let evc = project gls in
+ Astterm.constr_of_com evc (sig_it gls).hyps c
+
+let pf_constr_of_com_sort gls c =
+ let evc = project gls in
+ Astterm.constr_of_com_sort evc (sig_it gls).hyps c
+
let pf_reduction_of_redexp gls re c =
reduction_of_redexp re (pf_env gls) (project gls) c
@@ -242,7 +250,7 @@ let mutual_cofix lf lar pf =
let rename_bound_var_goal gls =
let { evar_env = env; evar_concl = cl } as gl = sig_it gls in
- let ids = ids_of_sign (get_globals (Environ.context env)) in
+ let ids = ids_of_sign (Environ.var_context env) in
convert_concl (rename_bound_var ids cl) gls
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 863023b79a..ea13c75a79 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -41,6 +41,9 @@ val pf_check_type : goal sigma -> constr -> constr -> constr
val pf_fexecute : goal sigma -> constr -> unsafe_judgment
val hnf_type_of : goal sigma -> constr -> constr
+val pf_constr_of_com : goal sigma -> Coqast.t -> constr
+val pf_constr_of_com_sort : goal sigma -> Coqast.t -> constr
+
val pf_get_hyp : goal sigma -> identifier -> constr
val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
diff --git a/proofs/typing_ev.ml b/proofs/typing_ev.ml
deleted file mode 100644
index 741ef10409..0000000000
--- a/proofs/typing_ev.ml
+++ /dev/null
@@ -1,154 +0,0 @@
-
-(* $Id$ *)
-
-open Util
-open Names
-open Generic
-open Term
-open Environ
-open Reduction
-open Type_errors
-open Typeops
-
-let vect_lift = Array.mapi lift
-let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
-
-type 'a mach_flags = {
- fix : bool;
- nocheck : bool }
-
-(* The typing machine without information, without universes but with
- existential variables. *)
-
-let rec execute mf env sigma cstr =
- match kind_of_term cstr with
- | IsMeta n ->
- error "execute: found a non-instanciated goal"
-
- | IsEvar _ ->
- let ty = type_of_existential env sigma cstr in
- let jty = execute mf env sigma ty in
- { uj_val = cstr; uj_type = ty; uj_kind = jty.uj_type }
-
- | IsRel n ->
- relative env n
-
- | IsVar id ->
- make_judge cstr (snd (lookup_var id env))
-
- | IsAbst _ ->
- if evaluable_abst env cstr then
- execute mf env sigma (abst_value env cstr)
- else
- error "Cannot typecheck an unevaluable abstraction"
-
- | IsConst _ ->
- make_judge cstr (type_of_constant env sigma cstr)
-
- | IsMutInd _ ->
- make_judge cstr (type_of_inductive env sigma cstr)
-
- | IsMutConstruct _ ->
- let (typ,kind) = destCast (type_of_constructor env sigma cstr) in
- { uj_val = cstr; uj_type = typ; uj_kind = kind }
-
- | IsMutCase (_,p,c,lf) ->
- let cj = execute mf env sigma c in
- let pj = execute mf env sigma p in
- let lfj = execute_array mf env sigma lf in
- type_of_case env sigma pj cj lfj
-
- | IsFix (vn,i,lar,lfi,vdef) ->
- if (not mf.fix) && array_exists (fun n -> n < 0) vn then
- error "General Fixpoints not allowed";
- let larv,vdefv = execute_fix mf env sigma lar lfi vdef in
- let fix = mkFix vn i larv lfi vdefv in
- check_fix env sigma fix;
- make_judge fix larv.(i)
-
- | IsCoFix (i,lar,lfi,vdef) ->
- let (larv,vdefv) = execute_fix mf env sigma lar lfi vdef in
- let cofix = mkCoFix i larv lfi vdefv in
- check_cofix env sigma cofix;
- make_judge cofix larv.(i)
-
- | IsSort (Prop c) ->
- make_judge_of_prop_contents c
-
- | IsSort (Type u) ->
- let (j,_) = make_judge_of_type u in j
-
- | IsAppL (f,args) ->
- let j = execute mf env sigma f in
- let jl = execute_list mf env sigma args in
- let (j,_) = apply_rel_list env sigma mf.nocheck jl j in
- j
-
- | IsLambda (name,c1,c2) ->
- let j = execute mf env sigma c1 in
- let var = assumption_of_judgment env sigma j in
- let env1 = push_rel (name,var) env in
- let j' = execute mf env1 sigma c2 in
- let (j,_) = abs_rel env1 sigma name var j' in
- j
-
- | IsProd (name,c1,c2) ->
- let j = execute mf env sigma c1 in
- let var = assumption_of_judgment env sigma j in
- let env1 = push_rel (name,var) env in
- let j' = execute mf env1 sigma c2 in
- let (j,_) = gen_rel env1 sigma name var j' in
- j
-
- | IsCast (c,t) ->
- let cj = execute mf env sigma c in
- let tj = execute mf env sigma t in
- cast_rel env sigma cj tj
-
- | _ -> error_cant_execute CCI env cstr
-
-and execute_fix mf env sigma lar lfi vdef =
- let larj = execute_array mf env sigma lar in
- let lara = Array.map (assumption_of_judgment env sigma) larj in
- let nlara =
- List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
- let env1 =
- List.fold_left (fun env nvar -> push_rel nvar env) env nlara in
- let vdefj = execute_array mf env1 sigma vdef in
- let vdefv = Array.map j_val_only vdefj in
- let cst3 = type_fixpoint env1 sigma lfi lara vdefj in
- (lara,vdefv)
-
-and execute_array mf env sigma v =
- let jl = execute_list mf env sigma (Array.to_list v) in
- Array.of_list jl
-
-and execute_list mf env sigma = function
- | [] ->
- []
- | c::r ->
- let j = execute mf env sigma c in
- let jr = execute_list mf env sigma r in
- j::jr
-
-
-let safe_machine env sigma constr =
- let mf = { fix = false; nocheck = false } in
- execute mf env sigma constr
-
-
-(* Type of a constr *)
-
-let type_of env sigma c =
- let j = safe_machine env sigma c in
- nf_betaiota env sigma j.uj_type
-
-(* The typed type of a judgment. *)
-
-let execute_type env sigma constr =
- let j = execute { fix=false; nocheck=true } env sigma constr in
- assumption_of_judgment env sigma j
-
-let execute_type env sigma constr =
- let j = execute { fix=false; nocheck=false } env sigma constr in
- assumption_of_judgment env sigma j
diff --git a/proofs/typing_ev.mli b/proofs/typing_ev.mli
deleted file mode 100644
index b12cd369d3..0000000000
--- a/proofs/typing_ev.mli
+++ /dev/null
@@ -1,18 +0,0 @@
-
-(* $Id$ *)
-
-(*i*)
-open Term
-open Environ
-open Evd
-(*i*)
-
-(* This module provides the typing machine with existential variables
- (but without universes). *)
-
-val type_of : unsafe_env -> 'a evar_map -> constr -> constr
-
-val execute_type : unsafe_env -> 'a evar_map -> constr -> typed_type
-
-val execute_rec_type : unsafe_env -> 'a evar_map -> constr -> typed_type
-
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:59:15 +0000