diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/topconstr.ml | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 06a8ec9d02..c613bf0dbe 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -394,6 +394,15 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match +let rec match_cases_pattern metas acc pat1 pat2 = + match (pat1,pat2) with + | PatVar (_,na1), PatVar (_,na2) -> match_names metas acc na1 na2 + | PatCstr (_,c1,patl1,na1), PatCstr (_,c2,patl2,na2) + when c1 = c2 & List.length patl1 = List.length patl2 -> + List.fold_left2 (match_cases_pattern metas) + (match_names metas acc na1 na2) patl1 patl2 + | _ -> raise No_match + let rec match_ alp metas sigma a1 a2 = match (a1,a2) with | r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1 | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma @@ -462,10 +471,12 @@ and match_binders alp metas na1 na2 sigma b1 b2 = let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in match_ alp metas sigma b1 b2 -and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) = - if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then - match_ alp metas sigma rhs1 rhs2 - else raise No_match +and match_equations alp metas sigma (_,_,patl1,rhs1) (_,patl2,rhs2) = + (* patl1 and patl2 have the same length because they respectively + correspond to some tml1 and tml2 that have the same length *) + let (alp,sigma) = + List.fold_left2 (match_cases_pattern metas) (alp,sigma) patl1 patl2 in + match_ alp metas sigma rhs1 rhs2 type scope_name = string |