diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 39 |
1 files changed, 18 insertions, 21 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b0fe83a3..58dda021 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 8875 2006-05-29 19:59:11Z msozeau $ *) +(* $Id: cases.ml 9215 2006-10-05 15:40:31Z herbelin $ *) open Util open Names @@ -336,8 +336,8 @@ let inh_coerce_to_ind isevars env ty tyi = un inductif cela doit être égal *) let _ = e_cumul env isevars expected_typ ty in () -let unify_tomatch_with_patterns isevars env typ tm = - match find_row_ind tm with +let unify_tomatch_with_patterns isevars env loc typ pats = + match find_row_ind pats with | None -> NotInd (None,typ) | Some (_,(ind,_)) -> inh_coerce_to_ind isevars env typ ind; @@ -345,29 +345,26 @@ let unify_tomatch_with_patterns isevars env typ tm = with Not_found -> NotInd (None,typ) let find_tomatch_tycon isevars env loc = function - (* Try first if some 'in I ...' is present and can be used as a constraint *) - | Some (_,ind,_,_),_ - (* Otherwise try to get constraints from (the 1st) constructor in clauses *) - | None, Some (_,(ind,_)) -> - mk_tycon (inductive_template isevars env loc ind) - | None, None -> - empty_tycon - -let coerce_row typing_fun isevars env cstropt (tomatch,(_,indopt)) = + (* Try if some 'in I ...' is present and can be used as a constraint *) + | Some (_,ind,_,_) -> mk_tycon (inductive_template isevars env loc ind) + | None -> empty_tycon + +let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) = let loc = Some (loc_of_rawconstr tomatch) in - let tycon = find_tomatch_tycon isevars env loc (indopt,cstropt) in + let tycon = find_tomatch_tycon isevars env loc indopt in let j = typing_fun tycon env tomatch in let typ = nf_evar (Evd.evars_of !isevars) j.uj_type in - let t = + let t = try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ) - with Not_found -> NotInd (None,typ) in + with Not_found -> + unify_tomatch_with_patterns isevars env loc typ pats in (j.uj_val,t) let coerce_to_indtype typing_fun isevars env matx tomatchl = let pats = List.map (fun r -> r.patterns) matx in let matx' = match matrix_transpose pats with - | [] -> List.map (fun _ -> None) tomatchl (* no patterns at all *) - | m -> List.map find_row_ind m in + | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *) + | m -> m in List.map2 (coerce_row typing_fun isevars env) matx' tomatchl (************************************************************************) @@ -500,12 +497,12 @@ let rec adjust_local_defs loc = function | [], [] -> [] | _ -> raise NotAdjustable -let check_and_adjust_constructor ind cstrs = function +let check_and_adjust_constructor env ind cstrs = function | PatVar _ as pat -> pat | PatCstr (loc,((_,i) as cstr),args,alias) as pat -> (* Check it is constructor of the right type *) let ind' = inductive_of_constructor cstr in - if ind' = ind then + if Closure.mind_equiv env ind' ind then (* Check the constructor has the right number of args *) let ci = cstrs.(i-1) in let nb_args_constr = ci.cs_nargs in @@ -1132,7 +1129,7 @@ let first_clause_irrefutable env = function | eqn::mat -> List.for_all (irrefutable env) eqn.patterns | _ -> false -let group_equations pb mind current cstrs mat = +let group_equations pb ind current cstrs mat = let mat = if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in let brs = Array.create (Array.length cstrs) [] in @@ -1142,7 +1139,7 @@ let group_equations pb mind current cstrs mat = (fun eqn () -> let rest = remove_current_pattern eqn in let pat = current_pattern eqn in - match check_and_adjust_constructor mind cstrs pat with + match check_and_adjust_constructor pb.env ind cstrs pat with | PatVar (_,name) -> (* This is a default clause that we expand *) for i=1 to Array.length cstrs do |