aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml79
-rw-r--r--pretyping/coercion.ml4
-rw-r--r--pretyping/detyping.ml47
-rw-r--r--pretyping/detyping.mli6
-rw-r--r--pretyping/evarconv.ml6
-rw-r--r--pretyping/evarutil.ml77
-rw-r--r--pretyping/evarutil.mli4
-rw-r--r--pretyping/pretype_errors.ml30
-rw-r--r--pretyping/pretyping.ml42
-rw-r--r--pretyping/retyping.ml6
-rw-r--r--pretyping/tacred.ml141
-rw-r--r--pretyping/typing.ml6
12 files changed, 238 insertions, 210 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 47fcdcc159..1d25ba84df 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -25,20 +25,20 @@ let mkExistential isevars env =
new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI
let norec_branch_scheme env isevars cstr =
- prod_it (mkExistential isevars env) cstr.cs_args
+ it_mkProd_or_LetIn (mkExistential isevars env) cstr.cs_args
-let lift_args l = list_map_i (fun i (name,c) -> (name,liftn 1 i c)) 1 l
-
-let rec_branch_scheme env isevars ((sp,j),_) recargs cstr =
+let rec_branch_scheme env isevars ((sp,j),_) recargs cstr =
let rec crec (args,recargs) =
match args, recargs with
- | (name,c)::rea,(ra::reca) ->
- DOP2(Prod,c,DLAM(name,
+ | (name,None,c)::rea,(ra::reca) ->
+ DOP2(Prod,body_of_type c,DLAM(name,
match ra with
| Mrec k when k=j ->
mkArrow (mkExistential isevars env)
- (crec (lift_args rea,reca))
+ (crec (List.rev (lift_rel_context 1 (List.rev rea)),reca))
| _ -> crec (rea,reca)))
+ | (name,Some d,c)::rea, reca -> failwith "TODO"
+(* mkLetIn (name,d,body_of_type c,crec (rea,reca))) *)
| [],[] -> mkExistential isevars env
| _ -> anomaly "rec_branch_scheme"
in
@@ -145,7 +145,7 @@ let inductive_of_rawconstructor c =
(* Environment management *)
let push_rel_type sigma (na,t) env =
- push_rel (na,get_assumption_of env sigma t) env
+ push_rel_decl (na,get_assumption_of env sigma t) env
let push_rels vars env =
List.fold_right (fun nvar env -> push_rel_type Evd.empty nvar env) vars env
@@ -537,6 +537,39 @@ let prepare_unif_pb typ cs =
(* This is the problem: finding P s.t. cs_args |- (P realargs ci) = p' *)
(Array.map (lift (-n)) cs.cs_concl_realargs, ci, p')
+(*
+(* Infering the predicate *)
+let prepare_unif_pb typ cs =
+ let n = cs.cs_nargs in
+ let _,p = decompose_prod_n n typ in
+ let ci = build_dependent_constructor cs in
+ (* This is the problem: finding P s.t. cs_args |- (P realargs ci) = p *)
+ (n, cs.cs_concl_realargs, ci, p)
+
+let eq_operator_lift k (n,n') = function
+ | OpRel p, OpRel p' when p > k & p' > k ->
+ if p < k+n or p' < k+n' then false else p - n = p' - n'
+ | op, op' -> op = op'
+
+let rec transpose_args n =
+ if n=0 then []
+ else
+ (Array.map (fun l -> List.hd l) lv)::
+ (transpose_args (m-1) (Array.init (fun l -> List.tl l)))
+
+let shift_operator k = function OpLambda _ | OpProd _ -> k+1 | _ -> k
+
+let reloc_operator (k,n) = function OpRel p when p > k ->
+let rec unify_clauses k pv =
+ let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) !isevars) p) pv in
+ let n1,op1 = let (n1,(op1,args1)) = pv'.(0) in n1,op1 in
+ if Array.for_all (fun (ni,(opi,_)) -> eq_operator_lift k (n1,ni) (op1,opi)) pv'
+ then
+ let argvl = transpose_args (List.length args1) pv' in
+ let k' = shift_operator k op1 in
+ let argl = List.map (unify_clauses k') argvl in
+ gather_constr (reloc_operator (k,n1) op1) argl
+*)
let abstract_conclusion typ cs =
let n = cs.cs_nargs in
@@ -545,18 +578,17 @@ let abstract_conclusion typ cs =
let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
(* Il faudra substituer les isevars a un certain moment *)
- let eqns = array_map2 prepare_unif_pb typs cstrs in
-
- (* First strategy: no dependencies at all *)
- let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in
- let (sign,_) = get_arity indf in
- if array_for_all (fun (_,_,typ) -> the_conv_x env isevars typn typ) eqns
- then
- let pred = lam_it (lift (List.length sign) typn) sign in
- (false,pred) (* true = dependent -- par défaut *)
+ if Array.length cstrs = 0 then
+ failwith "TODO4-3"
else
- if Array.length typs = 0 then
- failwith "TODO4-3"
+ let eqns = array_map2 prepare_unif_pb typs cstrs in
+ (* First strategy: no dependencies at all *)
+ let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in
+ let (sign,_) = get_arity indf in
+ if array_for_all (fun (_,_,typ) -> the_conv_x env isevars typn typ) eqns
+ then
+ let pred = lam_it (lift (List.length sign) typn) sign in
+ (false,pred) (* true = dependent -- par défaut *)
else
let s = get_sort_of env !isevars typs.(0) in
let predpred = lam_it (mkSort s) sign in
@@ -717,7 +749,8 @@ let shift_problem pb =
(* Building the sub-pattern-matching problem for a given branch *)
let build_branch pb defaults current eqns const_info =
- let names = get_names pb.env const_info.cs_args eqns in
+ let cs_args = decls_of_rel_context const_info.cs_args in
+ let names = get_names pb.env cs_args eqns in
let newpats =
if !substitute_alias then
List.map (fun na -> PatVar (dummy_loc,na)) names
@@ -726,7 +759,7 @@ let build_branch pb defaults current eqns const_info =
let submatdef = List.map (expand_defaults newpats current) defaults in
let submat = List.map (fun (tms,eqn) -> prepend_pattern tms eqn) eqns in
if submat = [] & submatdef = [] then error "Non exhaustive";
- let typs = List.map2 (fun (_,t) na -> (na,t)) const_info.cs_args (List.rev names) in
+ let typs = List.map2 (fun (_,t) na -> (na,t)) cs_args (List.rev names) in
let tomatchs =
List.fold_left2
(fun l (na,t) dep_in_rhs ->
@@ -834,7 +867,7 @@ let matx_of_eqns env eqns =
let build_eqn (ids,lpatt,rhs) =
let rhs =
{ rhs_env = env;
- other_ids = ids@(ids_of_sign (get_globals (context env)));
+ other_ids = ids@(ids_of_var_context (var_context env));
private_ids = [];
user_ids = ids;
subst = [];
@@ -874,7 +907,7 @@ let inh_coerce_to_ind isevars env ty tyi =
List.fold_right
(fun (na,ty) (env,evl) ->
let aty = get_assumption_of env Evd.empty ty in
- (push_rel (na,aty) env,
+ (push_rel_decl (na,aty) env,
(new_isevar isevars env (incast_type aty) CCI)::evl))
ntys (env,[]) in
let expected_typ = applist (mkMutInd tyi,evarl) in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 1e90ef8f3c..8269a47412 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -130,7 +130,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
(* let jv1 = exemeta_rec def_vty_con env isevars v1 in
let assv1 = assumption_of_judgement env !isevars jv1 in *)
let assv1 = outcast_type v1 in
- let env1 = push_rel (x,assv1) env in
+ let env1 = push_rel_decl (x,assv1) env in
let h2 = inh_conv_coerce_to_fail env isevars u2
{uj_val = v2;
uj_type = get_assumption_of env1 !isevars t2 } in
@@ -140,7 +140,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
let name = (match name with
| Anonymous -> Name (id_of_string "x")
| _ -> name) in
- let env1 = push_rel (name,assu1) env in
+ let env1 = push_rel_decl (name,assu1) env in
let h1 =
inh_conv_coerce_to_fail env isevars t1
{uj_val = Rel 1;
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 01ed9dc3bb..90697191a8 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -30,7 +30,7 @@ open Rawterm
type used_idents = identifier list
-let occur_id env id0 c =
+let occur_id env_names id0 c =
let rec occur n = function
| VAR id -> id=id0
| DOPN (Const sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl)
@@ -49,26 +49,27 @@ let occur_id env id0 c =
| DLAMV(_,v) -> array_exists (occur (n+1)) v
| Rel p ->
p>n &
- (try (fst (lookup_rel (p-n) env) = Name id0)
- with Not_found -> false) (* Unbound indice : may happen in debug *)
+ (try lookup_name_of_rel (p-n) env_names = Name id0
+ with Not_found -> false) (* Unbound indice: may happen in debug *)
| DOP0 _ -> false
in
occur 1 c
-let next_name_not_occuring name l env t =
+let next_name_not_occuring name l env_names t =
let rec next id =
- if List.mem id l or occur_id env id t then next (lift_ident id) else id
+ if List.mem id l or occur_id env_names id t then next (lift_ident id)
+ else id
in
match name with
| Name id -> next id
| Anonymous -> id_of_string "_"
(* Remark: Anonymous var may be dependent in Evar's contexts *)
-let concrete_name l env n c =
+let concrete_name l env_names n c =
if n = Anonymous & not (dependent (Rel 1) c) then
(None,l)
else
- let fresh_id = next_name_not_occuring n l env c in
+ let fresh_id = next_name_not_occuring n l env_names c in
let idopt = if dependent (Rel 1) c then (Some fresh_id) else None in
(idopt, fresh_id::l)
@@ -95,8 +96,6 @@ let global_vars_and_consts t =
list_uniquize (collect [] t)
let used_of = global_vars_and_consts
-let ids_of_env = Sign.ids_of_env
-
(****************************************************************************)
(* Tools for printing of Cases *)
@@ -262,22 +261,22 @@ let ids_of_var cl =
(Array.to_list cl)
*)
-let lookup_name_as_renamed env t s =
- let rec lookup avoid env n = function
- DOP2(Prod,_,DLAM(name,c')) ->
- (match concrete_name avoid env name c' with
+let lookup_name_as_renamed ctxt t s =
+ let rec lookup avoid env_names n = function
+ DOP2(Prod,t,DLAM(name,c')) ->
+ (match concrete_name avoid env_names name c' with
(Some id,avoid') ->
if id=s then (Some n)
- else lookup avoid' (add_rel (Name id,()) env) (n+1) c'
- | (None,avoid') -> lookup avoid' env (n+1) (pop c'))
- | DOP2(Cast,c,_) -> lookup avoid env n c
+ else lookup avoid' (add_name (Name id) env_names) (n+1) c'
+ | (None,avoid') -> lookup avoid' env_names (n+1) (pop c'))
+ | DOP2(Cast,c,_) -> lookup avoid env_names n c
| _ -> None
- in lookup (ids_of_env env) env 1 t
+ in lookup (ids_of_var_context ctxt) empty_names_context 1 t
let lookup_index_as_renamed t n =
let rec lookup n d = function
DOP2(Prod,_,DLAM(name,c')) ->
- (match concrete_name [] (gLOB nil_sign) name c' with
+ (match concrete_name [] empty_names_context name c' with
(Some _,_) -> lookup n (d+1) c'
| (None ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
| DOP2(Cast,c,_) -> lookup n d c
@@ -294,11 +293,11 @@ let rec detype avoid env t =
| regular_constr ->
(match kind_of_term regular_constr with
| IsRel n ->
- (try match fst (lookup_rel n env) with
+ (try match lookup_name_of_rel n env with
| Name id -> RRef (dummy_loc, RVar id)
| Anonymous -> anomaly "detype: index to an anonymous variable"
with Not_found ->
- let s = "[REL "^(string_of_int (number_of_rels env - n))^"]"
+ let s = "[REL "^(string_of_int n)^"]"
in RRef (dummy_loc, RVar (id_of_string s)))
| IsMeta n -> RMeta (dummy_loc, n)
| IsVar id -> RRef (dummy_loc,RVar id)
@@ -363,7 +362,7 @@ and detype_fix fk avoid env cl lfn vt =
let lfi = List.map (fun id -> next_name_away id avoid) lfn in
let def_avoid = lfi@avoid in
let def_env =
- List.fold_left (fun env id -> add_rel (Name id,()) env) env lfi in
+ List.fold_left (fun env id -> add_name (Name id) env) env lfi in
RRec(dummy_loc,fk,Array.of_list lfi,Array.map (detype avoid env) cl,
Array.map (detype def_avoid def_env) vt)
@@ -372,9 +371,9 @@ and detype_eqn avoid env constr_id construct_nargs branch =
let make_pat x avoid env b ids =
if not (force_wildcard ()) or (dependent (Rel 1) b) then
let id = next_name_away_with_default "x" x avoid in
- PatVar (dummy_loc,Name id),id::avoid,(add_rel (Name id,()) env),id::ids
+ PatVar (dummy_loc,Name id),id::avoid,(add_name (Name id) env),id::ids
else
- PatVar (dummy_loc,Anonymous),avoid,(add_rel (Anonymous,()) env),ids
+ PatVar (dummy_loc,Anonymous),avoid,(add_name Anonymous env),ids
in
let rec buildrec ids patlist avoid env = function
| 0 , rhs ->
@@ -405,4 +404,4 @@ and detype_binder bk avoid env na ty c =
| (None,l') -> Anonymous, l' in
RBinder (dummy_loc,bk,
na',detype [] env ty,
- detype avoid' (add_rel (na',()) env) c)
+ detype avoid' (add_name na' env) c)
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 9e0a30d09e..e961cfe917 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -5,6 +5,7 @@
open Names
open Term
open Sign
+open Environ
open Rawterm
(*i*)
@@ -13,11 +14,10 @@ open Rawterm
exception StillDLAM
-val detype : identifier list -> unit assumptions -> constr -> rawconstr
+val detype : identifier list -> names_context -> constr -> rawconstr
(* look for the index of a named var or a nondep var as it is renamed *)
-val lookup_name_as_renamed :
- unit assumptions -> constr -> identifier -> int option
+val lookup_name_as_renamed : var_context -> constr -> identifier -> int option
val lookup_index_as_renamed : constr -> int -> int option
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a4faeb3e4b..3afc734695 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -261,9 +261,9 @@ and evar_eqappr_x env isevars pbty appr1 appr2 =
| ((DOP2(Prod,c1,DLAM(n,c2)),[]), (DOP2(Prod,c'1,DLAM(_,c'2)),[])) ->
evar_conv_x env isevars CONV c1 c'1
- & evar_conv_x
- (push_rel (n,Retyping.get_assumption_of env !isevars (nf_ise1 !isevars c1)) env) isevars
- pbty c2 c'2
+ &
+ (let d = Retyping.get_assumption_of env !isevars (nf_ise1 !isevars c1)
+ in evar_conv_x (push_rel_decl (n,d) env) isevars pbty c2 c'2)
| ((DOPN(MutInd _ as o1,cl1) as ind1,l'1),
(DOPN(MutInd _ as o2,cl2) as ind2,l'2)) ->
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2de1219e31..804d635dbc 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -29,6 +29,7 @@ let distinct_id_list =
in drec []
+(*
let filter_sign p sign x =
sign_it
(fun id ty (v,ids,sgn) ->
@@ -36,21 +37,21 @@ let filter_sign p sign x =
if disc then (v', id::ids, sgn) else (v', ids, add_sign (id,ty) sgn))
sign
(x,[],nil_sign)
-
+*)
(*------------------------------------*
* functional operations on evar sets *
*------------------------------------*)
(* All ids of sign must be distincts! *)
-let new_isevar_sign env sigma typ args =
+let new_isevar_sign env sigma typ instance =
let sign = var_context env in
- if not (list_distinct (ids_of_sign sign)) then
+ if not (list_distinct (ids_of_var_context sign)) then
error "new_isevar_sign: two vars have the same name";
let newev = Evd.new_evar() in
let info = { evar_concl = typ; evar_env = env;
evar_body = Evar_empty; evar_info = None } in
- (Evd.add sigma newev info, mkEvar newev args)
+ (Evd.add sigma newev info, mkEvar (newev,Array.of_list instance))
(* We don't try to guess in which sort the type should be defined, since
any type has type Type. May cause some trouble, but not so far... *)
@@ -60,8 +61,8 @@ let dummy_sort = mkType dummy_univ
cumulativity now includes Prop and Set in Type. *)
let new_type_var env sigma =
let sign = var_context env in
- let args = (Array.of_list (List.map mkVar (ids_of_sign sign))) in
- let (sigma',c) = new_isevar_sign env sigma dummy_sort args in
+ let instance = List.map mkVar (ids_of_var_context sign) in
+ let (sigma',c) = new_isevar_sign env sigma dummy_sort instance in
(sigma', c)
let split_evar_to_arrow sigma c =
@@ -70,16 +71,16 @@ let split_evar_to_arrow sigma c =
let evenv = evd.evar_env in
let (sigma1,dom) = new_type_var evenv sigma in
let hyps = var_context evenv in
- let nvar = next_ident_away (id_of_string "x") (ids_of_sign hyps) in
- let nevenv = push_var (nvar,make_typed dom (Type dummy_univ)) evenv in
- let (sigma2,rng) = new_type_var nevenv sigma1 in
- let prod = mkProd (named_hd nevenv dom Anonymous) dom (subst_var nvar rng) in
+ let nvar = next_ident_away (id_of_string "x") (ids_of_var_context hyps) in
+ let newenv = push_var_decl (nvar,make_typed dom (Type dummy_univ)) evenv in
+ let (sigma2,rng) = new_type_var newenv sigma1 in
+ let prod = mkProd (named_hd newenv dom Anonymous) dom (subst_var nvar rng) in
let sigma3 = Evd.define sigma2 ev prod in
let dsp = num_of_evar dom in
let rsp = num_of_evar rng in
(sigma3,
- mkEvar dsp args,
- mkEvar rsp (array_cons (mkRel 1) (Array.map (lift 1) args)))
+ mkEvar (dsp,args),
+ mkEvar (rsp, array_cons (mkRel 1) (Array.map (lift 1) args)))
(* Redefines an evar with a smaller context (i.e. it may depend on less
@@ -99,17 +100,17 @@ let do_restrict_hyps sigma c =
let (_,(rsign,ncargs)) =
List.fold_left
(fun (sign,(rs,na)) a ->
- (tl_sign sign,
+ (List.tl sign,
if not(closed0 a) then
(rs,na)
else
- (add_sign (hd_sign sign) rs, a::na)))
- (hyps,(nil_sign,[])) args
+ (add_var (List.hd sign) rs, a::na)))
+ (hyps,([],[])) args
in
- let sign' = rev_sign rsign in
+ let sign' = List.rev rsign in
let env' = change_hyps (fun _ -> sign') env in
- let args' = Array.of_list (List.map mkVar (ids_of_sign sign')) in
- let (sigma',nc) = new_isevar_sign env' sigma evd.evar_concl args' in
+ let instance = List.map mkVar (ids_of_var_context sign') in
+ let (sigma',nc) = new_isevar_sign env' sigma evd.evar_concl instance in
let sigma'' = Evd.define sigma' ev nc in
(sigma'', nc)
@@ -199,29 +200,16 @@ let real_clean isevars sp args rhs =
(* [new_isevar] declares a new existential in an env env with type typ *)
(* Converting the env into the sign of the evar to define *)
-let append_rels_to_vars ctxt =
- dbenv_it
- (fun na t (subst,sign) ->
- let na = if na = Anonymous then Name(id_of_string"_") else na in
- let id = next_name_away na (ids_of_sign sign) in
- ((VAR id)::subst, add_sign (id,typed_app (substl subst) t) sign))
- ctxt ([],get_globals ctxt)
-
let new_isevar isevars env typ k =
- let ctxt = context env in
- let subst,sign = append_rels_to_vars ctxt in
+ let subst,env' = push_rels_to_vars env in
let typ' = substl subst typ in
- let env' = change_hyps (fun _ -> sign) env in
- let newargs =
- (List.rev(rel_list 0 (number_of_rels ctxt)))
- @(List.map (fun id -> VAR id) (ids_of_sign (get_globals ctxt))) in
- let (sigma',evar) =
- new_isevar_sign env' !isevars typ' (Array.of_list newargs) in
+ let instance =
+ (List.rev (rel_list 0 (rel_context_length (rel_context env))))
+ @(List.map mkVar (ids_of_var_context (var_context env))) in
+ let (sigma',evar) = new_isevar_sign env' !isevars typ' instance in
isevars := sigma';
evar
-
-
(* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
* evar, i.e. tries to find the body ?sp for lhs=DOPN(Const sp,args)
* ?sp [ sp.hyps \ args ] unifies to rhs
@@ -247,7 +235,7 @@ let evar_define isevars lhs rhs =
let evd = ise_map isevars ev in
let hyps = var_context evd.evar_env in
(* the substitution to invert *)
- let worklist = List.combine (ids_of_sign hyps) args in
+ let worklist = List.combine (ids_of_var_context hyps) args in
let body = real_clean isevars ev worklist rhs in
ise_define isevars ev body;
[ev]
@@ -269,19 +257,19 @@ let solve_refl conv_algo isevars c1 c2 =
array_fold_left2
(fun (sgn,rsgn) a1 a2 ->
if conv_algo a1 a2 then
- (tl_sign sgn, add_sign (hd_sign sgn) rsgn)
+ (List.tl sgn, add_var (List.hd sgn) rsgn)
else
- (tl_sign sgn, rsgn))
- (hyps,nil_sign) argsv1 argsv2
+ (List.tl sgn, rsgn))
+ (hyps,[]) argsv1 argsv2
in
- let nsign = rev_sign rsign in
+ let nsign = List.rev rsign in
let nenv = change_hyps (fun _ -> nsign) env in
- let nargs = (Array.of_list (List.map mkVar (ids_of_sign nsign))) in
+ let nargs = (Array.of_list (List.map mkVar (ids_of_var_context nsign))) in
let newev = Evd.new_evar () in
let info = { evar_concl = evd.evar_concl; evar_env = nenv;
evar_body = Evar_empty; evar_info = None } in
isevars :=
- Evd.define (Evd.add !isevars newev info) ev (mkEvar newev nargs);
+ Evd.define (Evd.add !isevars newev info) ev (mkEvar (newev,nargs));
Some [ev]
@@ -419,8 +407,7 @@ let split_tycon loc env isevars = function
isevars := sigma;
Some dom, Some rng
| _ ->
- Stdpp.raise_with_loc loc (Type_errors.TypeError (CCI,context env,Type_errors.NotProduct c)))
+ Stdpp.raise_with_loc loc (Type_errors.TypeError (CCI,env,Type_errors.NotProduct c)))
let valcon_of_tycon x = x
-
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index f648e4a830..dbebeac984 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -17,10 +17,6 @@ open Reduction
val filter_unique : 'a list -> 'a list
val distinct_id_list : identifier list -> identifier list
-val filter_sign :
- ('a -> identifier * typed_type -> bool * 'a) -> var_context -> 'a ->
- 'a * identifier list * var_context
-
val dummy_sort : constr
val do_restrict_hyps : 'a evar_map -> constr -> 'a evar_map * constr
val has_ise : 'a evar_map -> constr -> bool
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 9f711f390e..247620a676 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -11,51 +11,51 @@ let raise_pretype_error (loc,k,ctx,te) =
Stdpp.raise_with_loc loc (TypeError(k,ctx,te))
let error_var_not_found_loc loc k s =
- raise_pretype_error (loc,k, Global.context() (*bidon*), VarNotFound s)
+ raise_pretype_error (loc,k, Global.env() (*bidon*), VarNotFound s)
let error_cant_find_case_type_loc loc env expr =
- raise_pretype_error (loc, CCI, context env, CantFindCaseType expr)
+ raise_pretype_error (loc, CCI, env, CantFindCaseType expr)
let error_actual_type_loc loc env c actty expty =
- raise_pretype_error (loc, CCI, context env, ActualType (c,actty,expty))
+ raise_pretype_error (loc, CCI, env, ActualType (c,actty,expty))
let error_cant_apply_not_functional_loc loc env rator randl =
raise_pretype_error
- (loc,CCI,context env, CantApplyNonFunctional (rator,randl))
+ (loc,CCI,env, CantApplyNonFunctional (rator,randl))
let error_cant_apply_bad_type_loc loc env t rator randl =
- raise_pretype_error (loc, CCI, context env, CantApplyBadType (t,rator,randl))
+ raise_pretype_error (loc, CCI, env, CantApplyBadType (t,rator,randl))
let error_ill_formed_branch k env c i actty expty =
- raise (TypeError (k, context env, IllFormedBranch (c,i,actty,expty)))
+ raise (TypeError (k, env, IllFormedBranch (c,i,actty,expty)))
let error_number_branches_loc loc k env c ct expn =
- raise_pretype_error (loc, k, context env, NumberBranches (c,ct,expn))
+ raise_pretype_error (loc, k, env, NumberBranches (c,ct,expn))
let error_case_not_inductive_loc loc k env c ct =
- raise_pretype_error (loc, k, context env, CaseNotInductive (c,ct))
+ raise_pretype_error (loc, k, env, CaseNotInductive (c,ct))
(* Pattern-matching errors *)
let error_bad_constructor_loc loc k cstr ind =
- raise_pretype_error (loc, k, Global.context(), BadConstructor (cstr,ind))
+ raise_pretype_error (loc, k, Global.env(), BadConstructor (cstr,ind))
let error_wrong_numarg_constructor_loc loc k c n =
- raise_pretype_error (loc, k, Global.context(), WrongNumargConstructor (c,n))
+ raise_pretype_error (loc, k, Global.env(), WrongNumargConstructor (c,n))
let error_wrong_predicate_arity_loc loc k env c n1 n2 =
- raise_pretype_error (loc, k, context env, WrongPredicateArity (c,n1,n2))
+ raise_pretype_error (loc, k, env, WrongPredicateArity (c,n1,n2))
let error_needs_inversion k env x t =
- raise (TypeError (k, context env, NeedsInversion (x,t)))
+ raise (TypeError (k, env, NeedsInversion (x,t)))
let error_ill_formed_branch_loc loc k env c i actty expty =
- raise_pretype_error (loc, k, context env, IllFormedBranch (c,i,actty,expty))
+ raise_pretype_error (loc, k, env, IllFormedBranch (c,i,actty,expty))
let error_occur_check k env ev c =
- raise (TypeError (k, context env, OccurCheck (ev,c)))
+ raise (TypeError (k, env, OccurCheck (ev,c)))
let error_not_clean k env ev c =
- raise (TypeError (k, context env, NotClean (ev,c)))
+ raise (TypeError (k, env, NotClean (ev,c)))
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 68a75ee32d..cadaa7f78c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -189,21 +189,19 @@ let evar_type_case isevars env ct pt lft p c =
in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
*)
-let pretype_var loc env lvar id =
+let pretype_id loc env lvar id =
try
List.assoc id lvar
- with
- Not_found ->
- (try
- match lookup_id id (context env) with
- | RELNAME (n,typ) ->
- { uj_val = Rel n;
- uj_type = typed_app (lift n) typ }
- | GLOBNAME (id,typ) ->
- { uj_val = VAR id;
- uj_type = typ }
- with Not_found ->
- error_var_not_found_loc loc CCI id);;
+ with Not_found ->
+ try
+ let (n,typ) = lookup_rel_id id (rel_context env) in
+ { uj_val = Rel n; uj_type = typed_app (lift n) typ }
+ with Not_found ->
+ try
+ let typ = lookup_id_type id (var_context env) in
+ { uj_val = VAR id; uj_type = typ }
+ with Not_found ->
+ error_var_not_found_loc loc CCI id
(*************************************************************************)
(* Main pretyping function *)
@@ -212,7 +210,7 @@ let trad_metamap = ref []
let trad_nocheck = ref false
let pretype_ref pretype loc isevars env lvar = function
-| RVar id -> pretype_var loc env lvar id
+| RVar id -> pretype_id loc env lvar id
| RConst (sp,ctxt) ->
let cst = (sp,Array.map pretype ctxt) in
@@ -287,6 +285,16 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
| RHole loc ->
if !compter then nbimpl:=!nbimpl+1;
+(* OLD
+ (match vtcon with
+ (true,(Some v, _)) ->
+ {uj_val=v.utj_val; uj_type=make_typed (mkSort v.utj_type) (Type Univ.dummy_univ)}
+ | (false,(None,Some ty)) ->
+ let c = new_isevar isevars env ty CCI in
+ {uj_val=c;uj_type=make_typed ty (Type Univ.dummy_univ)}
+ | (true,(None,None)) ->
+ let ty = mkCast dummy_sort dummy_sort in
+*)
(match tycon with
| Some ty ->
let c = new_isevar isevars env ty CCI in
@@ -305,7 +313,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
let nbfix = Array.length lfi in
let lfi = List.map (fun id -> Name id) (Array.to_list lfi) in
let newenv =
- array_fold_left2 (fun env id ar -> (push_rel (id,ar) env))
+ array_fold_left2 (fun env id ar -> (push_rel_decl (id,ar) env))
env (Array.of_list (List.rev lfi)) (vect_lift_type lara) in
let vdefj =
Array.mapi
@@ -345,7 +353,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
let j = pretype_type dom_valcon env isevars lvar lmeta c1 in
let assum = assumption_of_type_judgment (inh_ass_of_j env isevars j) in
let var = (name,assum) in
- let j' = pretype rng (push_rel var env) isevars lvar lmeta c2
+ let j' = pretype rng (push_rel_decl var env) isevars lvar lmeta c2
in
fst (abs_rel env !isevars name assum j')
@@ -353,7 +361,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
let j = pretype empty_tycon env isevars lvar lmeta c1 in
let assum = inh_ass_of_j env isevars j in
let var = (name,assumption_of_type_judgment assum) in
- let j' = pretype empty_tycon (push_rel var env) isevars lvar lmeta c2 in
+ let j' = pretype empty_tycon (push_rel_decl var env) isevars lvar lmeta c2 in
(try fst (gen_rel env !isevars name assum j')
with TypeError _ as e -> Stdpp.raise_with_loc loc e)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 60647a946c..72a3d3d519 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -43,7 +43,7 @@ let rec type_of env cstr=
IsMeta n ->
(try strip_outer_cast (List.assoc n metamap)
with Not_found -> anomaly "type_of: this is not a well-typed term")
- | IsRel n -> lift n (body_of_type (snd (lookup_rel n env)))
+ | IsRel n -> lift n (body_of_type (snd (lookup_rel_type n env)))
| IsVar id ->
(try body_of_type (snd (lookup_var id env))
with Not_found ->
@@ -65,7 +65,7 @@ let rec type_of env cstr=
whd_betadeltaiota env sigma (applist (p,al))
| IsLambda (name,c1,c2) ->
let var = make_typed c1 (sort_of env c1) in
- mkProd name c1 (type_of (push_rel (name,var) env) c2)
+ mkProd name c1 (type_of (push_rel_decl (name,var) env) c2)
| IsFix ((vn,i),(lar,lfi,vdef)) -> lar.(i)
| IsCoFix (i,(lar,lfi,vdef)) -> lar.(i)
| IsAppL(f,args)->
@@ -81,7 +81,7 @@ and sort_of env t =
| IsSort (Type u) -> Type Univ.dummy_univ
| IsProd (name,t,c2) ->
let var = make_typed t (sort_of env t) in
- (match (sort_of (push_rel (name,var) env) c2) with
+ (match (sort_of (push_rel_decl (name,var) env) c2) with
| Prop _ as s -> s
| Type u2 -> Type Univ.dummy_univ)
| IsAppL(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f97b32cd12..a0fe84ee6e 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -26,69 +26,59 @@ let rev_firstn_liftn fn ln =
in
rfprec fn []
-let make_elim_fun f largs =
- try
- let (sp, _) = destConst f in
- match constant_eval sp with
- | EliminationCases n when List.length largs >= n -> f
- | EliminationFix (lv,n) when List.length largs >= n ->
- let labs,_ = list_chop n largs in
- let p = List.length lv in
- let la' = list_map_i
- (fun q aq ->
- try (Rel (p+1-(list_index (n+1-q) (List.map fst lv))))
- with Not_found -> aq) 1
- (List.map (lift p) labs)
- in
- list_fold_left_i
- (fun i c (k,a) ->
- DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a),
- DLAM(Name(id_of_string"x"),c))) 0 (applistc f la') lv
- | _ -> raise Redelimination
- with Failure _ ->
- raise Redelimination
-
-(* F is convertible to DOPN(Fix(recindices,bodynum),bodyvect) make
- the reduction using this extra information *)
+(* EliminationFix ([(yi1,Ti1);...;(yip,Tip)],n) means f is some
+ [y1:T1,...,yn:Tn](Fix(..) yi1 ... yip);
+ f is applied to largs and we need for recursive calls to build
+ [x1:Ti1',...,xp:Tip'](f a1..a(n-p) yi1 ... yip)
+ where a1...an are the n first arguments of largs and Tik' is Tik[yil=al]
+ To check ... *)
-let rebuild_global_name id =
- let sp = Nametab.sp_of_id CCI id in
- let (oper,hyps) = Declare.global_operator sp id in
- DOPN(oper,Array.of_list(List.map (fun id -> VAR id) (Sign.ids_of_sign hyps)))
+let make_elim_fun f lv n largs =
+ let (sp,args) = destConst f in
+ let labs,_ = list_chop n largs in
+ let p = List.length lv in
+ let ylv = List.map fst lv in
+ let la' = list_map_i
+ (fun q aq ->
+ try (Rel (p+1-(list_index (n-q) ylv)))
+ with Not_found -> aq) 0
+ (List.map (lift p) labs)
+ in
+ fun id ->
+ let fi = DOPN(Const(make_path (dirpath sp) id (kind_of_path sp)),args) in
+ list_fold_left_i
+ (fun i c (k,a) ->
+ DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a),
+ DLAM(Name(id_of_string"x"),c))) 0 (applistc fi la') lv
-let mydestFix = function
- | DOPN (Fix (recindxs,i),a) ->
- let (types,funnames,bodies) = destGralFix a in
- (recindxs,i,funnames,bodies)
- | _ -> invalid_arg "destFix"
+(* [f] is convertible to [DOPN(Fix(recindices,bodynum),bodyvect)] make
+ the reduction using this extra information *)
-let contract_fix_use_function f fix =
- let (recindices,bodynum,names,bodies) = mydestFix fix in
+let contract_fix_use_function f
+ ((recindices,bodynum),(types,names,bodies as typedbodies)) =
let nbodies = Array.length recindices in
let make_Fi j =
- let id = match List.nth names j with Name id -> id | _ -> assert false in
- rebuild_global_name id in
- let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
- substl (List.rev lbodies) bodies.(bodynum)
+ match List.nth names j with Name id -> f id | _ -> assert false in
+ let lbodies = list_tabulate make_Fi nbodies in
+ substl (List.rev lbodies) bodies.(bodynum)
let reduce_fix_use_function f whfun fix stack =
- match fix with
- | DOPN (Fix(recindices,bodynum),bodyvect) ->
- (match fix_recarg fix stack with
- | None -> (false,(fix,stack))
- | Some (recargnum,recarg) ->
- let (recarg'hd,_ as recarg')= whfun recarg [] in
- let stack' = list_assign stack recargnum (applist recarg') in
- (match recarg'hd with
- | DOPN(MutConstruct _,_) ->
- (true,(contract_fix_use_function f fix,stack'))
- | _ -> (false,(fix,stack'))))
- | _ -> assert false
+ let dfix = destFix fix in
+ match fix_recarg dfix stack with
+ | None -> (false,(fix,stack))
+ | Some (recargnum,recarg) ->
+ let (recarg'hd,_ as recarg')= whfun recarg [] in
+ let stack' = list_assign stack recargnum (applist recarg') in
+ (match recarg'hd with
+ | DOPN(MutConstruct _,_) ->
+ (true,(contract_fix_use_function f dfix,stack'))
+ | _ -> (false,(fix,stack')))
-let contract_cofix_use_function f (bodynum,(_,_,bodies as typedbodies)) =
+let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) =
let nbodies = Array.length bodies in
- let make_Fi j = mkCoFix (nbodies-j-1,typedbodies) in
- let subbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
+ let make_Fi j =
+ match List.nth names j with Name id -> f id | _ -> assert false in
+ let subbodies = list_tabulate make_Fi nbodies in
substl subbodies bodies.(bodynum)
let reduce_mind_case_use_function env f mia =
@@ -106,12 +96,14 @@ let special_red_case env whfun p c ci lf =
let rec redrec c l =
let (constr,cargs) = whfun c l in
match constr with
- | DOPN(Const _,_) as g ->
+ | DOPN(Const sp,args) as g ->
if evaluable_constant env g then
let gvalue = constant_value env g in
if reducible_mind_case gvalue then
- reduce_mind_case_use_function env g
- {mP=p; mconstr=gvalue; mcargs=cargs; mci=ci; mlf=lf}
+ let build_fix_name id =
+ DOPN(Const(make_path (dirpath sp) id (kind_of_path sp)),args)
+ in reduce_mind_case_use_function env build_fix_name
+ {mP=p; mconstr=gvalue; mcargs=cargs; mci=ci; mlf=lf}
else
redrec gvalue cargs
else
@@ -127,17 +119,30 @@ let special_red_case env whfun p c ci lf =
let rec red_elim_const env sigma k largs =
if not (evaluable_constant env k) then raise Redelimination;
- let f = make_elim_fun k largs in
- match whd_betadeltaeta_stack env sigma (constant_value env k) largs with
- | (DOPN(MutCase _,_) as mc,lrest) ->
- let (ci,p,c,lf) = destCase mc in
- (special_red_case env (construct_const env sigma) p c ci lf, lrest)
- | (DOPN(Fix _,_) as fix,lrest) ->
- let (b,(c,rest)) =
- reduce_fix_use_function f (construct_const env sigma) fix lrest
- in
- if b then (nf_beta env sigma c, rest) else raise Redelimination
- | _ -> assert false
+ let (sp, args) = destConst k in
+ let elim_style = constant_eval sp in
+ match elim_style with
+ | EliminationCases n when List.length largs >= n -> begin
+ let c = constant_value env k in
+ match whd_betadeltaeta_stack env sigma c largs with
+ | (DOPN(MutCase _,_) as mc,lrest) ->
+ let (ci,p,c,lf) = destCase mc in
+ (special_red_case env (construct_const env sigma) p c ci lf,
+ lrest)
+ | _ -> assert false
+ end
+ | EliminationFix (lv,n) when List.length largs >= n -> begin
+ let c = constant_value env k in
+ match whd_betadeltaeta_stack env sigma c largs with
+ | (DOPN(Fix _,_) as fix,lrest) ->
+ let f id = make_elim_fun k lv n largs id in
+ let (b,(c,rest)) =
+ reduce_fix_use_function f (construct_const env sigma) fix lrest
+ in
+ if b then (nf_beta env sigma c, rest) else raise Redelimination
+ | _ -> assert false
+ end
+ | _ -> raise Redelimination
and construct_const env sigma c stack =
let rec hnfstack x stack =
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 985b1d3998..0dc0d0a5b8 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -92,7 +92,7 @@ let rec execute mf env sigma cstr =
| 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 env1 = push_rel_decl (name,var) env in
let j' = execute mf env1 sigma c2 in
let (j,_) = abs_rel env1 sigma name var j' in
j
@@ -101,7 +101,7 @@ let rec execute mf env sigma cstr =
let j = execute mf env sigma c1 in
let varj = type_judgment env sigma j in
let var = assumption_of_type_judgment varj in
- let env1 = push_rel (name,var) env in
+ let env1 = push_rel_decl (name,var) env in
let j' = execute mf env1 sigma c2 in
let (j,_) = gen_rel env1 sigma name varj j' in
j
@@ -119,7 +119,7 @@ and execute_fix mf env sigma lar lfi vdef =
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
+ List.fold_left (fun env nvar -> push_rel_decl 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:05:02 +0000