summaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-01-31 14:34:14 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-01-31 14:34:14 +0000
commit6497f27021fec4e01f2182014f2bb1989b4707f9 (patch)
tree473be7e63895a42966970ab6a70998113bc1bd59 /pretyping
parent6b649aba925b6f7462da07599fe67ebb12a3460e (diff)
Imported Upstream version 8.0pl2upstream/8.0pl2
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml172
-rw-r--r--pretyping/evarconv.ml9
-rw-r--r--pretyping/evarutil.ml38
-rw-r--r--pretyping/inductiveops.ml6
-rw-r--r--pretyping/inductiveops.mli4
-rw-r--r--pretyping/matching.mli4
-rw-r--r--pretyping/pattern.ml5
-rw-r--r--pretyping/rawterm.ml6
-rw-r--r--pretyping/rawterm.mli10
-rw-r--r--pretyping/tacred.ml12
-rw-r--r--pretyping/tacred.mli4
-rw-r--r--pretyping/termops.mli4
12 files changed, 137 insertions, 137 deletions
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