From 6497f27021fec4e01f2182014f2bb1989b4707f9 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 31 Jan 2005 14:34:14 +0000 Subject: Imported Upstream version 8.0pl2 --- pretyping/cases.ml | 172 ++++++++++++++++++++++++++------------------- pretyping/evarconv.ml | 9 ++- pretyping/evarutil.ml | 38 ++-------- pretyping/inductiveops.ml | 6 +- pretyping/inductiveops.mli | 4 +- pretyping/matching.mli | 4 +- pretyping/pattern.ml | 5 +- pretyping/rawterm.ml | 6 +- pretyping/rawterm.mli | 10 +-- pretyping/tacred.ml | 12 ++-- pretyping/tacred.mli | 4 +- pretyping/termops.mli | 4 +- 12 files changed, 137 insertions(+), 137 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 2126f015..378eee30 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml,v 1.111.2.1 2004/07/16 19:30:43 herbelin Exp $ *) +(* $Id: cases.ml,v 1.111.2.4 2004/12/09 20:07:01 herbelin Exp $ *) open Util open Names @@ -262,9 +262,10 @@ type tomatch_stack = tomatch_status list (* The type [predicate_signature] types the terms to match and the rhs: - - [PrLetIn (n,dep,pred)] types a pushed term ([Pushed]), if dep is true, - the term is dependent, if n<>0 then the type of the pushed term is - necessarily inductive with n real arguments. Otherwise, it may be + - [PrLetIn (names,dep,pred)] types a pushed term ([Pushed]), + if dep<>Anonymous, the term is dependent, let n=|names|, if + n<>0 then the type of the pushed term is necessarily an + inductive with n real arguments. Otherwise, it may be non inductive, or inductive without real arguments, or inductive originating from a subterm in which case real args are not dependent; it accounts for n+1 binders if dep or n binders if not dep @@ -274,7 +275,7 @@ type tomatch_stack = tomatch_status list *) type predicate_signature = - | PrLetIn of (int * bool) * predicate_signature + | PrLetIn of (name list * name) * predicate_signature | PrProd of predicate_signature | PrCcl of constr @@ -408,12 +409,11 @@ let inh_coerce_to_ind isevars env tmloc ty tyi = let hole_source = match tmloc with | Some loc -> fun i -> (loc, TomatchTypeParameter (tyi,i)) | None -> fun _ -> (dummy_loc, InternalHole) in - let (_,evarl,_) = + let (evarl,_) = List.fold_right - (fun (na,ty) (env,evl,n) -> - (push_rel (na,None,ty) env, - (new_isevar isevars env (hole_source n) ty)::evl,n+1)) - ntys (env,[],1) in + (fun (na,ty) (evl,n) -> + (new_isevar isevars env (hole_source n) (substl evl ty))::evl,n+1) + ntys ([],1) in let expected_typ = applist (mkInd tyi,evarl) in (* devrait être indifférent d'exiger leq ou pas puisque pour un inductif cela doit être égal *) @@ -976,10 +976,17 @@ let rec map_predicate f k = function | PrCcl ccl -> PrCcl (f k ccl) | PrProd pred -> PrProd (map_predicate f (k+1) pred) - | PrLetIn ((nargs,dep as tm),pred) -> - let k' = nargs + (if dep then 1 else 0) in + | PrLetIn ((names,dep as tm),pred) -> + let k' = List.length names + (if dep<>Anonymous then 1 else 0) in PrLetIn (tm, map_predicate f (k+k') pred) +let rec noccurn_predicate k = function + | PrCcl ccl -> noccurn k ccl + | PrProd pred -> noccurn_predicate (k+1) pred + | PrLetIn ((names,dep as tm),pred) -> + let k' = List.length names + (if dep<>Anonymous then 1 else 0) in + noccurn_predicate (k+k') pred + let liftn_predicate n = map_predicate (liftn n) let lift_predicate n = liftn_predicate n 1 @@ -998,12 +1005,12 @@ let subst_predicate (args,copt) pred = let specialize_predicate_var (cur,typ) = function | PrProd _ | PrCcl _ -> anomaly "specialize_predicate_var: a pattern-variable must be pushed" - | PrLetIn ((0,dep),pred) -> - subst_predicate ([],if dep then Some cur else None) pred + | PrLetIn (([],dep),pred) -> + subst_predicate ([],if dep<>Anonymous then Some cur else None) pred | PrLetIn ((_,dep),pred) -> (match typ with | IsInd (_,IndType (_,realargs)) -> - subst_predicate (realargs,if dep then Some cur else None) pred + subst_predicate (realargs,if dep<>Anonymous then Some cur else None) pred | _ -> anomaly "specialize_predicate_var") let ungeneralize_predicate = function @@ -1020,9 +1027,9 @@ let ungeneralize_predicate = function (* then we have to replace x by x' in t(x) and y by y' in P *) (*****************************************************************************) let generalize_predicate c ny d = function - | PrLetIn ((nargs,dep as tm),pred) -> - if not dep then anomaly "Undetected dependency"; - let p = nargs + 1 in + | PrLetIn ((names,dep as tm),pred) -> + if dep=Anonymous then anomaly "Undetected dependency"; + let p = List.length names + 1 in let pred = lift_predicate 1 pred in let pred = regeneralize_index_predicate (ny+p+1) pred in PrLetIn (tm, PrProd pred) @@ -1038,18 +1045,18 @@ let rec extract_predicate l = function | PrProd pred, Abstract d'::tms -> let d' = map_rel_declaration (lift (List.length l)) d' in substl l (mkProd_or_LetIn d' (extract_predicate [] (pred,tms))) - | PrLetIn ((0,dep),pred), Pushed ((cur,_),_)::tms -> - extract_predicate (if dep then cur::l else l) (pred,tms) + | PrLetIn (([],dep),pred), Pushed ((cur,_),_)::tms -> + extract_predicate (if dep<>Anonymous then cur::l else l) (pred,tms) | PrLetIn ((_,dep),pred), Pushed ((cur,IsInd (_,(IndType(_,realargs)))),_)::tms -> let l = List.rev realargs@l in - extract_predicate (if dep then cur::l else l) (pred,tms) + extract_predicate (if dep<>Anonymous then cur::l else l) (pred,tms) | PrCcl ccl, [] -> substl l ccl | _ -> anomaly"extract_predicate: predicate inconsistent with terms to match" let abstract_predicate env sigma indf cur tms = function | (PrProd _ | PrCcl _) -> anomaly "abstract_predicate: must be some LetIn" - | PrLetIn ((nrealargs,dep),pred) -> + | PrLetIn ((names,dep),pred) -> let sign = make_arity_signature env true indf in (* n is the number of real args + 1 *) let n = List.length sign in @@ -1061,18 +1068,24 @@ let abstract_predicate env sigma indf cur tms = function (* Depending on whether the predicate is dependent or not, and has real args or not, we lift it to make room for [sign] *) (* Even if not intrinsically dep, we move the predicate into a dep one *) - let k = - if nrealargs = 0 & n <> 1 then - (* Real args were not considered *) if dep then n-1 else n + let sign,k = + if names = [] & n <> 1 then + (* Real args were not considered *) + (if dep<>Anonymous then + ((let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign),n-1) + else + (sign,n)) else - (* Real args are OK *) if dep then 0 else 1 in + (* Real args are OK *) + (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign, + if dep<>Anonymous then 0 else 1) in let pred = lift_predicate k pred in let pred = extract_predicate [] (pred,tms) in (true, it_mkLambda_or_LetIn_name env pred sign) let rec known_dependent = function | None -> false - | Some (PrLetIn ((_,dep),_)) -> dep + | Some (PrLetIn ((_,dep),_)) -> dep<>Anonymous | Some (PrCcl _) -> false | Some (PrProd _) -> anomaly "known_dependent: can only be used when patterns remain" @@ -1084,10 +1097,13 @@ let rec known_dependent = function let expand_arg n alreadydep (na,t) deps (k,pred) = (* current can occur in pred even if the original problem is not dependent *) - let dep = deps <> [] || alreadydep in - let pred = if dep then pred else lift_predicate (-1) pred in + let dep = + if alreadydep<>Anonymous then alreadydep + else if deps = [] && noccurn_predicate 1 pred then Anonymous + else Name (id_of_string "x") in + let pred = if dep<>Anonymous then pred else lift_predicate (-1) pred in (* There is no dependency in realargs for subpattern *) - (k-1, PrLetIn ((0,dep), pred)) + (k-1, PrLetIn (([],dep), pred)) (*****************************************************************************) @@ -1107,14 +1123,15 @@ let expand_arg n alreadydep (na,t) deps (k,pred) = let specialize_predicate tomatchs deps cs = function | (PrProd _ | PrCcl _) -> anomaly "specialize_predicate: a matched pattern must be pushed" - | PrLetIn ((nrealargs,isdep),pred) -> + | PrLetIn ((names,isdep),pred) -> (* Assume some gamma st: gamma, (X,x:=realargs,copt) |- pred *) - let k = nrealargs + (if isdep then 1 else 0) in + let nrealargs = List.length names in + let k = nrealargs + (if isdep<>Anonymous then 1 else 0) in (* We adjust pred st: gamma, x1..xn, (X,x:=realargs,copt) |- pred' *) let n = cs.cs_nargs in let pred' = liftn_predicate n (k+1) pred in let argsi = if nrealargs <> 0 then Array.to_list cs.cs_concl_realargs else [] in - let copti = if isdep then Some (build_dependent_constructor cs) else None in + let copti = if isdep<>Anonymous then Some (build_dependent_constructor cs) else None in (* The substituends argsi, copti are all defined in gamma, x1...xn *) (* We need _parallel_ bindings to get gamma, x1...xn |- pred'' *) let pred'' = subst_predicate (argsi, copti) pred' in @@ -1513,24 +1530,28 @@ let extract_predicate_conclusion isdep tomatchl pred = let cook = function | _,IsInd (_,IndType(_,args)) -> Some (List.length args) | _,NotInd _ -> None in - let decomp_lam_force p = + let rec decomp_lam_force n l p = + if n=0 then (l,p) else match kind_of_term p with - | Lambda (_,_,c) -> c - | _ -> (* eta-expansion *) applist (lift 1 p, [mkRel 1]) in - let rec buildrec p = function - | [] -> p + | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c + | _ -> (* eta-expansion *) + let na = Name (id_of_string "x") in + decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in + let rec buildrec allnames p = function + | [] -> (List.rev allnames,p) | tm::ltm -> match cook tm with | None -> let p = (* adjust to a sign containing the NotInd's *) if isdep then lift 1 p else p in - buildrec p ltm + let names = if isdep then [Anonymous] else [] in + buildrec (names::allnames) p ltm | Some n -> let n = if isdep then n+1 else n in - let p = iterate decomp_lam_force n p in - buildrec p ltm - in buildrec pred tomatchl + let names,p = decomp_lam_force n [] p in + buildrec (names::allnames) p ltm + in buildrec [] pred tomatchl let set_arity_signature dep n arsign tomatchl pred x = (* avoid is not exhaustive ! *) @@ -1572,18 +1593,19 @@ let set_arity_signature dep n arsign tomatchl pred x = decomp_block [] pred (tomatchl,arsign) let prepare_predicate_from_tycon loc dep env isevars tomatchs c = - let cook (n, l, env) = function + let cook (n, l, signs) = function | c,IsInd (_,IndType(indf,realargs)) -> let indf' = lift_inductive_family n indf in - let sign = make_arity_signature env dep indf' in + let arsign = make_arity_signature env dep indf' in let p = List.length realargs in if dep then - (n + p + 1, c::(List.rev realargs)@l, push_rels sign env) + (n + p + 1, c::(List.rev realargs)@l, arsign::signs) else - (n + p, (List.rev realargs)@l, push_rels sign env) + (n + p, (List.rev realargs)@l, arsign::signs) | c,NotInd _ -> - (n, l, env) in - let n, allargs, env = List.fold_left cook (0, [], env) tomatchs in + (n, l, []::signs) in + let n, allargs, signs = List.fold_left cook (0, [], []) tomatchs in + let env = List.fold_right push_rels signs env in let allargs = List.map (fun c -> lift n (nf_betadeltaiota env (evars_of isevars) c)) allargs in let rec build_skeleton env c = @@ -1594,28 +1616,32 @@ let prepare_predicate_from_tycon loc dep env isevars tomatchs c = mkExistential isevars env (loc, CasesType) else map_constr_with_full_binders push_rel build_skeleton env c in - build_skeleton env (lift n c) + List.rev (List.map (List.map pi1) signs), build_skeleton env (lift n c) (* Here, [pred] is assumed to be in the context built from all *) (* realargs and terms to match *) -let build_initial_predicate isdep pred tomatchl = - let nar = List.fold_left (fun n (_,t) -> - let p = match t with IsInd (_,IndType(_,a)) -> List.length a | _ -> 0 in - if isdep then n+p+1 else n+p) 0 tomatchl in - let cook = function - | _,IsInd (_,IndType(_,realargs)) -> List.length realargs - | _,NotInd _ -> 0 in +let build_initial_predicate isdep allnames pred = + let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in let rec buildrec n pred = function | [] -> PrCcl pred - | tm::ltm -> - let nrealargs = cook tm in + | names::lnames -> + let names' = if isdep then List.tl names else names in + let n' = n + List.length names' in let pred, p, user_p = if isdep then - if dependent (mkRel (nar-n)) pred then pred, 1, 1 - else liftn (-1) (nar-n) pred, 0, 1 + if dependent (mkRel (nar-n')) pred then pred, 1, 1 + else liftn (-1) (nar-n') pred, 0, 1 else pred, 0, 0 in - PrLetIn ((nrealargs,p=1), buildrec (n+nrealargs+user_p) pred ltm) - in buildrec 0 pred tomatchl + let na = + if p=1 then + let na = List.hd names in + if na = Anonymous then + (* peut arriver en raison des evars *) + Name (id_of_string "x") (*Hum*) + else na + else Anonymous in + PrLetIn ((names',na), buildrec (n'+user_p) pred lnames) + in buildrec 0 pred allnames let extract_arity_signature env0 tomatchl tmsign = let get_one_sign n tm {contents = (na,t)} = @@ -1652,9 +1678,9 @@ let extract_arity_signature env0 tomatchl tmsign = | [],[] -> [] | (_,tm)::ltm, x::tmsign -> let l = get_one_sign n tm x in - (buildrec (n + List.length l) (ltm,tmsign)) @ l + l :: buildrec (n + List.length l) (ltm,tmsign) | _ -> assert false - in buildrec 0 (tomatchl,tmsign) + in List.rev (buildrec 0 (tomatchl,tmsign)) (* Builds the predicate. If the predicate is dependent, its context is * made of 1+nrealargs assumptions for each matched term in an inductive @@ -1683,17 +1709,18 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function (match tycon with | None -> None | Some t -> - let pred = prepare_predicate_from_tycon loc false env isevars tomatchs t in - Some (build_initial_predicate false pred tomatchs)) + let names,pred = prepare_predicate_from_tycon loc false env isevars tomatchs t in + Some (build_initial_predicate false names pred)) (* v8 style type annotation *) | (None,{contents = Some rtntyp}) -> (* We extract the signature of the arity *) - let arsign = extract_arity_signature env tomatchs sign in - let env = push_rels arsign env in + let arsigns = extract_arity_signature env tomatchs sign in + let env = List.fold_right push_rels arsigns env in + let allnames = List.rev (List.map (List.map pi1) arsigns) in let predccl = (typing_fun (mk_tycon (new_Type ())) env rtntyp).uj_val in - Some (build_initial_predicate true predccl tomatchs) + Some (build_initial_predicate true allnames predccl) (* v7 style type annotation; set the v8 annotation by side effect *) | (Some pred,x) -> @@ -1721,12 +1748,9 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function error_wrong_predicate_arity_loc loc env predj.uj_val ndep_arity dep_arity in - let predccl = extract_predicate_conclusion dep tomatchs predj.uj_val in -(* - let etapred,cdep = case_dependent env (evars_of isevars) loc predj tomatchs in -*) + let ln,predccl= extract_predicate_conclusion dep tomatchs predj.uj_val in set_arity_signature dep n sign tomatchs pred x; - Some (build_initial_predicate dep predccl tomatchs) + Some (build_initial_predicate dep ln predccl) (**************************************************************************) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6f396b43..0ee95a0f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarconv.ml,v 1.44.6.1 2004/07/16 19:30:44 herbelin Exp $ *) +(* $Id: evarconv.ml,v 1.44.6.2 2004/11/26 23:51:39 herbelin Exp $ *) open Util open Names @@ -39,8 +39,11 @@ let flex_kind_of_term c l = let eval_flexible_term env c = match kind_of_term c with | Const c -> constant_opt_value env c - | Rel n -> let (_,v,_) = lookup_rel n env in option_app (lift n) v - | Var id -> let (_,v,_) = lookup_named id env in v + | Rel n -> + (try let (_,v,_) = lookup_rel n env in option_app (lift n) v + with Not_found -> None) + | Var id -> + (try let (_,v,_) = lookup_named id env in v with Not_found -> None) | LetIn (_,b,_,c) -> Some (subst1 b c) | Lambda _ -> Some c | _ -> assert false diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 441070fe..4337c0fc 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarutil.ml,v 1.64.2.3 2004/07/16 19:30:44 herbelin Exp $ *) +(* $Id: evarutil.ml,v 1.64.2.5 2004/12/09 14:45:38 herbelin Exp $ *) open Util open Pp @@ -30,25 +30,6 @@ let rec filter_unique = function if List.mem x l then filter_unique (List.filter (fun y -> x<>y) l) else x::filter_unique l -(* -let distinct_id_list = - let rec drec fresh = function - [] -> List.rev fresh - | id::rest -> - let id' = next_ident_away_from id fresh in drec (id'::fresh) rest - in drec [] -*) - -(* -let filter_sign p sign x = - sign_it - (fun id ty (v,ids,sgn) -> - let (disc,v') = p v (id,ty) in - if disc then (v', id::ids, sgn) else (v', ids, add_sign (id,ty) sgn)) - sign - (x,[],nil_sign) -*) - (* Expanding existential variables (pretyping.ml) *) (* 1- whd_ise fails if an existential is undefined *) @@ -183,20 +164,9 @@ let do_restrict_hyps sigma ev args = let evd = Evd.map sigma ev in let env = evar_env evd in let hyps = evd.evar_hyps in - let (_,(rsign,ncargs)) = - List.fold_left - (fun (sign,(rs,na)) a -> - (List.tl sign, - if not(closed0 a) then - (rs,na) - else - (add_named_decl (List.hd sign) rs, a::na))) - (hyps,([],[])) args - in - let sign' = List.rev rsign in - let env' = reset_with_named_context sign' env in - let instance = make_evar_instance env' in - let (sigma',nc) = new_isevar_sign env' sigma evd.evar_concl instance in + let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in + let env' = reset_with_named_context sign env in + let (sigma',nc) = new_isevar_sign env' sigma evd.evar_concl ncargs in let nc = refresh_universes nc in (* needed only if nc is an inferred type *) let sigma'' = Evd.define sigma' ev nc in (sigma'', nc) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 24a8fbc7..c33a261b 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductiveops.ml,v 1.14.2.1 2004/07/16 19:30:45 herbelin Exp $ *) +(* $Id: inductiveops.ml,v 1.14.2.2 2004/12/29 12:15:00 herbelin Exp $ *) open Util open Names @@ -341,9 +341,9 @@ let control_only_guard env = Inductive.check_fix env fix; Array.iter control_rec tys; Array.iter control_rec bds; - | Case(_,p,c,b) ->control_rec p;control_rec c;Array.iter control_rec b + | Case(_,p,c,b) -> control_rec p;control_rec c;Array.iter control_rec b | Evar (_,cl) -> Array.iter control_rec cl - | App (_,cl) -> Array.iter control_rec cl + | App (c,cl) -> control_rec c; Array.iter control_rec cl | Cast (c1,c2) -> control_rec c1; control_rec c2 | Prod (_,c1,c2) -> control_rec c1; control_rec c2 | Lambda (_,c1,c2) -> control_rec c1; control_rec c2 diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index a8dcef29..8cfa9b3c 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductiveops.mli,v 1.10.2.1 2004/07/16 19:30:45 herbelin Exp $ *) +(*i $Id: inductiveops.mli,v 1.10.2.3 2005/01/21 17:19:37 herbelin Exp $ i*) open Names open Term @@ -66,7 +66,7 @@ val make_arity_signature : val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types -(* Raise Not_found if not given an valid inductive type *) +(* Raise [Not_found] if not given an valid inductive type *) val extract_mrectype : constr -> inductive * constr list val find_mrectype : env -> evar_map -> constr -> inductive * constr list val find_rectype : env -> evar_map -> constr -> inductive_type diff --git a/pretyping/matching.mli b/pretyping/matching.mli index 808c46a4..2f666880 100644 --- a/pretyping/matching.mli +++ b/pretyping/matching.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: matching.mli,v 1.3.2.1 2004/07/16 19:30:45 herbelin Exp $ i*) +(*i $Id: matching.mli,v 1.3.2.2 2005/01/21 16:42:37 herbelin Exp $ i*) (*i*) open Names @@ -42,7 +42,7 @@ val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map (* To skip to the next occurrence *) exception NextOccurrence of int -(* Tries to match a _closed_ subterm of [c] with [pat] *) +(* Tries to match a **closed** subterm of [c] with [pat] *) val sub_match : int -> constr_pattern -> constr -> patvar_map * constr (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat] diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 80ab1b6e..f58a12c6 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pattern.ml,v 1.24.2.1 2004/07/16 19:30:45 herbelin Exp $ *) +(* $Id: pattern.ml,v 1.24.2.2 2004/11/26 17:51:52 herbelin Exp $ *) open Util open Names @@ -182,8 +182,7 @@ let rec pattern_of_constr t = Some (pattern_of_constr p),pattern_of_constr a, Array.map pattern_of_constr br) | Fix f -> PFix f - | CoFix _ -> - error "pattern_of_constr: (co)fix currently not supported" + | CoFix f -> PCoFix f (* To process patterns, we need a translation without typing at all. *) diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 520f09e9..ef4a4670 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: rawterm.ml,v 1.43.2.2 2004/07/16 19:30:46 herbelin Exp $ *) +(* $Id: rawterm.ml,v 1.43.2.4 2004/12/29 10:17:10 herbelin Exp $ *) (*i*) open Util @@ -49,7 +49,7 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings type hole_kind = - | ImplicitArg of global_reference * int + | ImplicitArg of global_reference * (int * identifier option) | BinderType of name | QuestionMark | CasesType @@ -356,7 +356,7 @@ type ('a,'b) red_expr_gen = | Unfold of 'b occurrences list | Fold of 'a list | Pattern of 'a occurrences list - | ExtraRedExpr of string * 'a + | ExtraRedExpr of string type ('a,'b) may_eval = | ConstrTerm of 'a diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index d78d1866..97e11af6 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: rawterm.mli,v 1.47.2.2 2004/07/16 19:30:46 herbelin Exp $ i*) +(*i $Id: rawterm.mli,v 1.47.2.5 2005/01/21 16:42:37 herbelin Exp $ i*) (*i*) open Util @@ -47,7 +47,7 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings type hole_kind = - | ImplicitArg of global_reference * int + | ImplicitArg of global_reference * (int * identifier option) | BinderType of name | QuestionMark | CasesType @@ -97,11 +97,11 @@ i*) val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr -(* +(*i val map_rawconstr_with_binders_loc : loc -> (identifier -> 'a -> identifier * 'a) -> ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr -*) +i*) val occur_rawconstr : identifier -> rawconstr -> bool @@ -130,7 +130,7 @@ type ('a,'b) red_expr_gen = | Unfold of 'b occurrences list | Fold of 'a list | Pattern of 'a occurrences list - | ExtraRedExpr of string * 'a + | ExtraRedExpr of string type ('a,'b) may_eval = | ConstrTerm of 'a diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 7e79a4fe..f225e79f 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml,v 1.75.2.2 2004/07/16 19:30:46 herbelin Exp $ *) +(* $Id: tacred.ml,v 1.75.2.6 2004/12/29 10:17:10 herbelin Exp $ *) open Pp open Util @@ -329,7 +329,7 @@ let make_elim_fun (names,(nbfix,lv,n)) largs = mkLambda (Name(id_of_string"x"), substl (rev_firstn_liftn (n-k) (-i) la') a, c)) - 0 (applistc (mkEvalRef ref) la') lv) + 1 (applistc (mkEvalRef ref) la') (List.rev lv)) (* [f] is convertible to [Fix(recindices,bodynum),bodyvect)] make the reduction using this extra information *) @@ -808,6 +808,7 @@ let abstract_scheme env sigma (locc,a) t = let pattern_occs loccs_trm env sigma c = let abstr_trm = List.fold_right (abstract_scheme env sigma) loccs_trm c in + let _ = Typing.type_of env sigma abstr_trm in applist(abstr_trm, List.map snd loccs_trm) (* Generic reduction: reduction functions used in reduction tactics *) @@ -858,7 +859,7 @@ let reduction_of_redexp = function | Unfold ubinds -> unfoldn ubinds | Fold cl -> fold_commands cl | Pattern lp -> pattern_occs lp - | ExtraRedExpr (s,c) -> + | ExtraRedExpr s -> (try Stringmap.find s !red_expr_tab with Not_found -> error("unknown user-defined reduction \""^s^"\"")) (* Used in several tactics. *) @@ -945,7 +946,10 @@ let reduce_to_ref_gen allow_product env sigma ref t = try let t' = nf_betaiota (one_step_reduce env sigma t) in elimrec env t' l - with NotStepReducible -> raise Not_found + with NotStepReducible -> + errorlabstrm "" + (str "Not a statement of conclusion " ++ + Nametab.pr_global_env Idset.empty ref) in elimrec env t [] diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 162275d5..7998a8fd 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacred.mli,v 1.21.2.1 2004/07/16 19:30:46 herbelin Exp $ i*) +(*i $Id: tacred.mli,v 1.21.2.2 2005/01/21 16:42:37 herbelin Exp $ i*) (*i*) open Names @@ -62,7 +62,7 @@ val reduce_to_atomic_ind : env -> evar_map -> types -> inductive * types val reduce_to_quantified_ind : env -> evar_map -> types -> inductive * types (* [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form - [t'=(x1:A1)..(xn:An)(ref args)] and raise Not_found if not possible *) + [t'=(x1:A1)..(xn:An)(ref args)] and raise [Not_found] if not possible *) val reduce_to_quantified_ref : env -> evar_map -> Libnames.global_reference -> types -> types diff --git a/pretyping/termops.mli b/pretyping/termops.mli index dd9742ea..22bd0aba 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: termops.mli,v 1.21.2.1 2004/07/16 19:30:46 herbelin Exp $ *) +(*i $Id: termops.mli,v 1.21.2.3 2005/01/21 17:19:37 herbelin Exp $ i*) open Util open Pp @@ -16,7 +16,7 @@ open Sign open Environ (* Universes *) -(*val set_module : Names.dir_path -> unit*) +(*i val set_module : Names.dir_path -> unit i*) val new_univ : unit -> Univ.universe val new_sort_in_family : sorts_family -> sorts -- cgit v1.2.3