diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 35 |
1 files changed, 23 insertions, 12 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 0967d21f01..20492e38c8 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -239,7 +239,7 @@ let subtract_loc loc1 loc2 = let check_is_hole id t = match DAst.get t with GHole _ -> () | _ -> user_err ?loc:(loc_of_glob_constr t) - (strbrk "In recursive notation with binders, " ++ pr_id id ++ + (strbrk "In recursive notation with binders, " ++ Id.print id ++ strbrk " is expected to come without type.") let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' @@ -400,7 +400,7 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = let vars = Id.Map.filter filter nenv.ninterp_var_type in let check_recvar x = if Id.List.mem x found then - user_err (pr_id x ++ + user_err (Id.print x ++ strbrk " should only be used in the recursive part of a pattern.") in let check (x, y) = check_recvar x; check_recvar y in let () = List.iter check foundrec in @@ -419,8 +419,8 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = in let check_pair s x y where = if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then - user_err (strbrk "in the right-hand side, " ++ pr_id x ++ - str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++ + user_err (strbrk "in the right-hand side, " ++ Id.print x ++ + str " and " ++ Id.print y ++ strbrk " should appear in " ++ str s ++ str " position as part of a recursive pattern.") in let check_type x typ = match typ with @@ -838,7 +838,7 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v | Name id' -> if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match in let unify_pat p p' = - if cases_pattern_eq (map_cases_pattern_name_left (name_app (rename_var (snd alp))) p) p' then p' + if cases_pattern_eq (map_cases_pattern_name_left (Name.map (rename_var (snd alp))) p) p' then p' else raise No_match in let unify_term_binder c = DAst.(map (fun b' -> match DAst.get c, b' with @@ -980,6 +980,19 @@ let match_termlist match_fun alp metas sigma rest x y iter termin lassoc = else bind_termlist_env alp sigma x l +let match_cast match_fun sigma c1 c2 = + match c1, c2 with + | CastConv t1, CastConv t2 + | CastVM t1, CastVM t2 + | CastNative t1, CastNative t2 -> + match_fun sigma t1 t2 + | CastCoerce, CastCoerce -> + sigma + | CastConv _, _ + | CastVM _, _ + | CastNative _, _ + | CastCoerce, _ -> raise No_match + let does_not_come_from_already_eta_expanded_var glob = (* This is hack to avoid looping on a rule with rhs of the form *) (* "?f (fun ?x => ?g)" since otherwise, matching "F H" expands in *) @@ -1125,11 +1138,8 @@ let rec match_ inner u alp metas sigma a1 a2 = let alp,sigma = Array.fold_right2 (fun id1 id2 alsig -> match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in Array.fold_left2 (match_in u alp metas) sigma bl1 bl2 - | GCast(c1,CastConv t1), NCast (c2,CastConv t2) - | GCast(c1,CastVM t1), NCast (c2,CastVM t2) -> - match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2 - | GCast(c1, CastCoerce), NCast(c2, CastCoerce) -> - match_in u alp metas sigma c1 c2 + | GCast(t1, c1), NCast(t2, c2) -> + match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2 | GSort (GType _), NSort (GType _) when not u -> sigma | GSort s1, NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match @@ -1157,8 +1167,9 @@ let rec match_ inner u alp metas sigma a1 a2 = match_names metas (alp,sigma) (Name id') na in match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2 - | (GRec _ | GEvar _), _ - | _,_ -> raise No_match + | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ + | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ + | GCast _), _ -> raise No_match and match_in u = match_ true u |