diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 16 | ||||
| -rw-r--r-- | interp/constrintern.ml | 22 | ||||
| -rw-r--r-- | interp/notation.ml | 47 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 388 | ||||
| -rw-r--r-- | interp/notation_ops.mli | 14 | ||||
| -rw-r--r-- | interp/reserve.ml | 2 |
6 files changed, 319 insertions, 170 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d1bec16a3f..8d3cf7274a 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -85,7 +85,7 @@ let is_reserved_type na t = | Name id -> try let pat = Reserve.find_reserved_type id in - let _ = match_notation_constr false t ([],pat) in + let _ = match_notation_constr ~print_univ:false t ~vars:Id.Set.empty ([],pat) in true with Not_found | No_match -> false @@ -1273,7 +1273,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = | AppBoundedNotation _ -> raise No_match in (* Try matching ... *) let terms,termlists,binders,binderlists = - match_notation_constr !print_universes t pat in + match_notation_constr ~print_univ:(!print_universes) t ~vars pat in (* Try availability of interpretation ... *) match keyrule with | NotationRule (_,ntn as specific_ntn) -> @@ -1293,20 +1293,20 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = | Some (scopt,key) -> let scopes' = Option.List.cons scopt (snd scopes) in let l = - List.map (fun (c,(subentry,(scopt,scl))) -> + List.map (fun ((vars,c),(subentry,(scopt,scl))) -> extern (* assuming no overloading: *) true (subentry,(scopt,scl@scopes')) vars c) terms in let ll = - List.map (fun (c,(subentry,(scopt,scl))) -> - List.map (extern true (subentry,(scopt,scl@scopes')) vars) c) + List.map (fun ((vars,l),(subentry,(scopt,scl))) -> + List.map (extern true (subentry,(scopt,scl@scopes')) vars) l) termlists in let bl = - List.map (fun (bl,(subentry,(scopt,scl))) -> + List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)) binders in let bll = - List.map (fun (bl,(subentry,(scopt,scl))) -> + List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) binderlists in let c = make_notation loc specific_ntn (l,ll,bl,bll) in @@ -1316,7 +1316,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = CAst.make ?loc @@ extern_applied_notation inctx nallargs argsimpls c args) | SynDefRule kn -> let l = - List.map (fun (c,(subentry,(scopt,scl))) -> + List.map (fun ((vars,c),(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c) terms in let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b86ad7175a..c7ed066f7e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -534,15 +534,19 @@ let intern_generalized_binder intern_type ntnvars in let na = match na with | Anonymous -> - let name = - let id = - match ty with - | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid -> - qualid_basename qid - | _ -> default_non_dependent_ident - in Implicit_quantifiers.make_fresh ids' (Global.env ()) id - in Name name - | _ -> na in + let id = + match ty with + | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid -> + qualid_basename qid + | _ -> default_non_dependent_ident + in + let ids' = List.fold_left (fun ids' lid -> Id.Set.add lid.CAst.v ids') ids' fvs in + let id = + Implicit_quantifiers.make_fresh ids' (Global.env ()) id + in + Name id + | _ -> na + in let impls = impls_type_list 1 ty' in (push_name_env ntnvars impls env' (make ?loc na), (make ?loc (na,b',ty')) :: List.rev bl) diff --git a/interp/notation.ml b/interp/notation.ml index 1a361dc1a6..286ece6cb6 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -345,11 +345,23 @@ let also_cases_notation_rule_eq (also_cases1,rule1) (also_cases2,rule2) = (* No need in principle to compare also_cases as it is inferred *) also_cases1 = also_cases2 && notation_rule_eq rule1 rule2 +let adjust_application c1 c2 = + match c1, c2 with + | NApp (t1, a1), (NList (_,_,NApp (_, a2),_,_) | NApp (_, a2)) when List.length a1 >= List.length a2 -> + NApp (t1, List.firstn (List.length a2) a1) + | NApp (t1, a1), _ -> + t1 + | _ -> c1 + +let strictly_finer_interpretation_than (_,(_,(vars1,c1),_)) (_,(_,(vars2,c2),_)) = + let c1 = adjust_application c1 c2 in + Notation_ops.strictly_finer_notation_constr (List.map fst vars1, List.map fst vars2) c1 c2 + let keymap_add key interp map = let old = try KeyMap.find key map with Not_found -> [] in - (* In case of re-import, no need to keep the previous copy *) - let old = try List.remove_first (also_cases_notation_rule_eq interp) old with Not_found -> old in - KeyMap.add key (interp :: old) map + (* strictly finer interpretation are kept in front *) + let strictly_finer, rest = List.partition (fun c -> strictly_finer_interpretation_than c interp) old in + KeyMap.add key (strictly_finer @ interp :: rest) map let keymap_remove key interp map = let old = try KeyMap.find key map with Not_found -> [] in @@ -1419,12 +1431,12 @@ let check_parsing_override (scopt,ntn) data = function | OnlyParsingData (_,old_data) -> let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in warn_override_if_needed (scopt,ntn) overridden data old_data; - None, not overridden + None | ParsingAndPrintingData (_,on_printing,old_data) -> let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in warn_override_if_needed (scopt,ntn) overridden data old_data; - (if on_printing then Some old_data.not_interp else None), not overridden - | NoParsingData -> None, false + if on_printing then Some old_data.not_interp else None + | NoParsingData -> None let check_printing_override (scopt,ntn) data parsingdata printingdata = let parsing_update = match parsingdata with @@ -1453,15 +1465,15 @@ let update_notation_data (scopt,ntn) use data table = try NotationMap.find ntn table with Not_found -> (NoParsingData, []) in match use with | OnlyParsing -> - let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in - NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update, exists + let printing_update = check_parsing_override (scopt,ntn) data parsingdata in + NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update | ParsingAndPrinting -> - let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in - NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update, exists + let printing_update = check_parsing_override (scopt,ntn) data parsingdata in + NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update | OnlyPrinting -> let parsingdata, exists = check_printing_override (scopt,ntn) data parsingdata printingdata in let printingdata = if exists then printingdata else (true,data) :: printingdata in - NotationMap.add ntn (parsingdata, printingdata) table, None, exists + NotationMap.add ntn (parsingdata, printingdata) table, None let rec find_interpretation ntn find = function | [] -> raise Not_found @@ -1734,23 +1746,22 @@ let declare_notation (scopt,ntn) pat df ~use ~also_in_cases_pattern coe deprecat not_location = df; not_deprecation = deprecation; } in - let notation_update,printing_update, exists = update_notation_data (scopt,ntn) use notdata sc.notations in - if not exists then - let sc = { sc with notations = notation_update } in - scope_map := String.Map.add scope sc !scope_map; + let notation_update,printing_update = update_notation_data (scopt,ntn) use notdata sc.notations in + let sc = { sc with notations = notation_update } in + scope_map := String.Map.add scope sc !scope_map; (* Update the uninterpretation cache *) begin match printing_update with | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) also_in_cases_pattern pat | None -> () end; - if not exists && use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat; + if use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat; (* Register visibility of lonely notations *) - if not exists then begin match scopt with + begin match scopt with | LastLonelyNotation -> scope_stack := LonelyNotationItem ntn :: !scope_stack | NotationInScope _ -> () end; (* Declare a possible coercion *) - if not exists then begin match coe with + begin match coe with | Some (IsEntryCoercion entry) -> let (_,level,_) = level_of_notation ntn in let level = match fst ntn with diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7cb3ca25ee..c4d2a2a496 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -24,82 +24,182 @@ open Notation_term (**********************************************************************) (* Utilities *) -(* helper for NVar, NVar case in eq_notation_constr *) -let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None - -let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = -(vars1 == vars2 && t1 == t2) || -match t1, t2 with -| NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2 -| NVar id1, NVar id2 -> ( - match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with - | Some n,Some m -> Int.equal n m - | None ,None -> Id.equal id1 id2 - | _ -> false) -| NApp (t1, a1), NApp (t2, a2) -> - (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2 -| NHole (_, _, _), NHole (_, _, _) -> true (* FIXME? *) -| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) -> - Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && - (eq_notation_constr vars) u1 u2 && b1 == b2 -| NLambda (na1, t1, u1), NLambda (na2, t2, u2) -> - Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 -| NProd (na1, t1, u1), NProd (na2, t2, u2) -> - Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 -| NBinderList (i1, j1, t1, u1, b1), NBinderList (i2, j2, t2, u2, b2) -> - Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && - (eq_notation_constr vars) u1 u2 && b1 == b2 -| NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr vars b1 b2 && - Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 -| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *) - let eqpat (p1, t1) (p2, t2) = - List.equal cases_pattern_eq p1 p2 && - (eq_notation_constr vars) t1 t2 - in - let eqf (t1, (na1, o1)) (t2, (na2, o2)) = - let eq (i1, n1) (i2, n2) = Ind.CanOrd.equal i1 i2 && List.equal Name.equal n1 n2 in - (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 - in - Option.equal (eq_notation_constr vars) o1 o2 && - List.equal eqf r1 r2 && - List.equal eqpat p1 p2 -| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) -> - List.equal Name.equal nas1 nas2 && - Name.equal na1 na2 && - Option.equal (eq_notation_constr vars) o1 o2 && - (eq_notation_constr vars) t1 t2 && - (eq_notation_constr vars) u1 u2 -| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) -> - (eq_notation_constr vars) t1 t2 && - Name.equal na1 na2 && - Option.equal (eq_notation_constr vars) o1 o2 && - (eq_notation_constr vars) u1 u2 && - (eq_notation_constr vars) r1 r2 -| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *) - let eq (na1, o1, t1) (na2, o2, t2) = - Name.equal na1 na2 && - Option.equal (eq_notation_constr vars) o1 o2 && - (eq_notation_constr vars) t1 t2 - in - Array.equal Id.equal ids1 ids2 && - Array.equal (List.equal eq) ts1 ts2 && - Array.equal (eq_notation_constr vars) us1 us2 && - Array.equal (eq_notation_constr vars) rs1 rs2 -| NSort s1, NSort s2 -> - glob_sort_eq s1 s2 -| NCast (t1, c1), NCast (t2, c2) -> - (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2 -| NInt i1, NInt i2 -> - Uint63.equal i1 i2 -| NFloat f1, NFloat f2 -> - Float64.equal f1 f2 -| NArray(t1,def1,ty1), NArray(t2,def2,ty2) -> - Array.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) def1 def2 - && eq_notation_constr vars ty1 ty2 -| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ - | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> false +let ldots_var = Id.of_string ".." + +let rec alpha_var id1 id2 = function + | (i1,i2)::_ when Id.equal i1 id1 -> Id.equal i2 id2 + | (i1,i2)::_ when Id.equal i2 id2 -> Id.equal i1 id1 + | _::idl -> alpha_var id1 id2 idl + | [] -> Id.equal id1 id2 + +let cast_type_iter2 f t1 t2 = match t1, t2 with + | CastConv t1, CastConv t2 -> f t1 t2 + | CastVM t1, CastVM t2 -> f t1 t2 + | CastCoerce, CastCoerce -> () + | CastNative t1, CastNative t2 -> f t1 t2 + | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> raise Exit + +(* used to update the notation variable with the local variables used + in NList and NBinderList, since the iterator has its own variable *) +let replace_var i j var = j :: List.remove Id.equal i var + +(* When [lt] is [true], tell if [t1] is a strict refinement of [t2] + (this is a partial order, so returning [false] does not mean that + [t2] is finer than [t1]); when [lt] is false, tell if [t1] is the + same pattern as [t2] *) + +let compare_notation_constr lt (vars1,vars2) t1 t2 = + (* this is used to reason up to order of notation variables *) + let alphameta = ref [] in + (* this becomes true when at least one subterm is detected as strictly smaller *) + let strictly_lt = ref false in + (* this is the stack of inner of iter patterns for comparison with a + new iteration or the tail of a recursive pattern *) + let tail = ref [] in + let check_alphameta id1 id2 = + try if not (Id.equal (List.assoc id1 !alphameta) id2) then raise Exit + with Not_found -> + if (List.mem_assoc id1 !alphameta) then raise Exit; + alphameta := (id1,id2) :: !alphameta in + let check_eq_id (vars1,vars2) renaming id1 id2 = + let ismeta1 = List.mem_f Id.equal id1 vars1 in + let ismeta2 = List.mem_f Id.equal id2 vars2 in + match ismeta1, ismeta2 with + | true, true -> check_alphameta id1 id2 + | false, false -> if not (alpha_var id1 id2 renaming) then raise Exit + | false, true -> + if not lt then raise Exit + else + (* a binder which is not bound in the notation can be + considered as strictly more precise since it prevents the + notation variables in its scope to be bound by this binder; + i.e. it is strictly more precise in the sense that it + covers strictly less patterns than a notation where the + same binder is bound in the notation; this is hawever + disputable *) + strictly_lt := true + | true, false -> if not lt then raise Exit in + let check_eq_name vars renaming na1 na2 = + match na1, na2 with + | Name id1, Name id2 -> check_eq_id vars renaming id1 id2; (id1,id2)::renaming + | Anonymous, Anonymous -> renaming + | Anonymous, Name _ when lt -> renaming + | _ -> raise Exit in + let rec aux (vars1,vars2 as vars) renaming t1 t2 = match t1, t2 with + | NVar id1, NVar id2 when id1 = ldots_var && id2 = ldots_var -> () + | _, NVar id2 when lt && id2 = ldots_var -> tail := t1 :: !tail + | NVar id1, _ when lt && id1 = ldots_var -> tail := t2 :: !tail + | NVar id1, NVar id2 -> check_eq_id vars renaming id1 id2 + | NHole _, NVar id2 when lt && List.mem_f Id.equal id2 vars2 -> () + | NVar id1, NHole (_, _, _) when lt && List.mem_f Id.equal id1 vars1 -> () + | _, NVar id2 when lt && List.mem_f Id.equal id2 vars2 -> strictly_lt := true + | NRef gr1, NRef gr2 when GlobRef.equal gr1 gr2 -> () + | NHole (_, _, _), NHole (_, _, _) -> () (* FIXME? *) + | _, NHole (_, _, _) when lt -> strictly_lt := true + | NList (i1, j1, iter1, tail1, b1), NList (i2, j2, iter2, tail2, b2) + | NBinderList (i1, j1, iter1, tail1, b1), NBinderList (i2, j2, iter2, tail2, b2) -> + if b1 <> b2 then raise Exit; + let vars1 = replace_var i1 j1 vars1 in + let vars2 = replace_var i2 j2 vars2 in + check_alphameta i1 i2; aux (vars1,vars2) renaming iter1 iter2; aux vars renaming tail1 tail2; + | NBinderList (i1, j1, iter1, tail1, b1), NList (i2, j2, iter2, tail2, b2) + | NList (i1, j1, iter1, tail1, b1), NBinderList (i2, j2, iter2, tail2, b2) -> + (* They may overlap on a unique iteration of them *) + let vars1 = replace_var i1 j1 vars1 in + let vars2 = replace_var i2 j2 vars2 in + aux (vars1,vars2) renaming iter1 iter2; + aux vars renaming tail1 tail2 + | t1, NList (i2, j2, iter2, tail2, b2) + | t1, NBinderList (i2, j2, iter2, tail2, b2) when lt -> + (* checking if t1 is a finite iteration of the pattern *) + let vars2 = replace_var i2 j2 vars2 in + aux (vars1,vars2) renaming t1 iter2; + let t1 = List.hd !tail in + tail := List.tl !tail; + (* either matching a new iteration, or matching the tail *) + (try aux vars renaming t1 tail2 with Exit -> aux vars renaming t1 t2) + | NList (i1, j1, iter1, tail1, b1), t2 + | NBinderList (i1, j1, iter1, tail1, b1), t2 when lt -> + (* we see the NList as a single iteration *) + let vars1 = replace_var i1 j1 vars1 in + aux (vars1,vars2) renaming iter1 t2; + let t2 = match !tail with + | t::rest -> tail := rest; t + | _ -> (* ".." is in a discarded fine-grained position *) raise Exit in + (* it had to be a single iteration of iter1 *) + aux vars renaming tail1 t2 + | NApp (t1, a1), NApp (t2, a2) -> aux vars renaming t1 t2; List.iter2 (aux vars renaming) a1 a2 + | NLambda (na1, t1, u1), NLambda (na2, t2, u2) + | NProd (na1, t1, u1), NProd (na2, t2, u2) -> + aux vars renaming t1 t2; + let renaming = check_eq_name vars renaming na1 na2 in + aux vars renaming u1 u2 + | NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) -> + aux vars renaming b1 b2; + Option.iter2 (aux vars renaming) t1 t2;(* TODO : subtyping? *) + let renaming = check_eq_name vars renaming na1 na2 in + aux vars renaming u1 u2 + | NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *) + let check_pat (p1, t1) (p2, t2) = + if not (List.equal cases_pattern_eq p1 p2) then raise Exit; (* TODO: subtyping and renaming *) + aux vars renaming t1 t2 + in + let eqf renaming (t1, (na1, o1)) (t2, (na2, o2)) = + aux vars renaming t1 t2; + let renaming = check_eq_name vars renaming na1 na2 in + let eq renaming (i1, n1) (i2, n2) = + if not (Ind.CanOrd.equal i1 i2) then raise Exit; + List.fold_left2 (check_eq_name vars) renaming n1 n2 in + Option.fold_left2 eq renaming o1 o2 in + let renaming = List.fold_left2 eqf renaming r1 r2 in + Option.iter2 (aux vars renaming) o1 o2; + List.iter2 check_pat p1 p2 + | NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) -> + aux vars renaming t1 t2; + let renaming = check_eq_name vars renaming na1 na2 in + Option.iter2 (aux vars renaming) o1 o2; + let renaming' = List.fold_left2 (check_eq_name vars) renaming nas1 nas2 in + aux vars renaming' u1 u2 + | NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) -> + aux vars renaming t1 t2; + aux vars renaming u1 u2; + aux vars renaming r1 r2; + let renaming = check_eq_name vars renaming na1 na2 in + Option.iter2 (aux vars renaming) o1 o2 + | NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *) + let eq renaming (na1, o1, t1) (na2, o2, t2) = + Option.iter2 (aux vars renaming) o1 o2; + aux vars renaming t1 t2; + check_eq_name vars renaming na1 na2 + in + let renaming = Array.fold_left2 (fun r id1 id2 -> check_eq_id vars r id1 id2; (id1,id2)::r) renaming ids1 ids2 in + let renamings = Array.map2 (List.fold_left2 eq renaming) ts1 ts2 in + Array.iter3 (aux vars) renamings us1 us2; + Array.iter3 (aux vars) (Array.map ((@) renaming) renamings) rs1 rs2 + | NSort s1, NSort s2 when glob_sort_eq s1 s2 -> () + | NCast (t1, c1), NCast (t2, c2) -> + aux vars renaming t1 t2; + cast_type_iter2 (aux vars renaming) c1 c2 + | NInt i1, NInt i2 when Uint63.equal i1 i2 -> () + | NFloat f1, NFloat f2 when Float64.equal f1 f2 -> () + | NArray(t1,def1,ty1), NArray(t2,def2,ty2) -> + Array.iter2 (aux vars renaming) t1 t2; + aux vars renaming def1 def2; + aux vars renaming ty1 ty2 + | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ + | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ + | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> raise Exit in + try + let _ = aux (vars1,vars2) [] t1 t2 in + if not lt then + (* Check that order of notation metavariables does not matter *) + List.iter2 check_alphameta vars1 vars2; + not lt || !strictly_lt + with Exit | (* Option.iter2: *) Option.Heterogeneous | Invalid_argument _ -> false + +let eq_notation_constr vars t1 t2 = t1 == t2 || compare_notation_constr false vars t1 t2 + +let strictly_finer_notation_constr vars t1 t2 = compare_notation_constr true vars t1 t2 (**********************************************************************) (* Re-interpret a notation as a glob_constr, taking care of binders *) @@ -154,8 +254,6 @@ let rec subst_glob_vars l gc = DAst.map (function | _ -> DAst.get (map_glob_constr (subst_glob_vars l) gc) (* assume: id is not binding *) ) gc -let ldots_var = Id.of_string ".." - type 'a binder_status_fun = { no : 'a -> 'a; restart_prod : 'a -> 'a; @@ -723,6 +821,20 @@ let abstract_return_type_context_notation_constr tml rtn = abstract_return_type_context snd (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, IntroAnonymous, None),c)) tml rtn +let rec push_pattern_binders vars pat = + match DAst.get pat with + | PatVar na -> Termops.add_vname vars na + | PatCstr (c, pl, na) -> List.fold_left push_pattern_binders (Termops.add_vname vars na) pl + +let rec push_context_binders vars = function + | [] -> vars + | b :: bl -> + let vars = match DAst.get b with + | GLocalAssum (na,_,_) -> Termops.add_vname vars na + | GLocalPattern ((disjpat,ids),p,bk,t) -> List.fold_right Id.Set.add ids vars + | GLocalDef (na,_,_,_) -> Termops.add_vname vars na in + push_context_binders vars bl + let is_term_meta id metas = try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false with Not_found -> false @@ -749,17 +861,11 @@ let is_bindinglist_meta id metas = exception No_match -let rec alpha_var id1 id2 = function - | (i1,i2)::_ when Id.equal i1 id1 -> Id.equal i2 id2 - | (i1,i2)::_ when Id.equal i2 id2 -> Id.equal i1 id1 - | _::idl -> alpha_var id1 id2 idl - | [] -> Id.equal id1 id2 - let alpha_rename alpmetas v = if alpmetas == [] then v else try rename_glob_vars alpmetas v with UnsoundRenaming -> raise No_match -let add_env (alp,alpmetas) (terms,termlists,binders,binderlists) var v = +let add_env (vars,(alp,alpmetas)) (terms,termlists,binders,binderlists) var v = (* Check that no capture of binding variables occur *) (* [alp] is used when matching a pattern "fun x => ... x ... ?var ... x ..." with an actual term "fun z => ... z ..." when "x" is not bound in the @@ -787,19 +893,19 @@ let add_env (alp,alpmetas) (terms,termlists,binders,binderlists) var v = refinement *) let v = alpha_rename alpmetas v in (* TODO: handle the case of multiple occs in different scopes *) - ((var,v)::terms,termlists,binders,binderlists) + ((var,(vars,v))::terms,termlists,binders,binderlists) -let add_termlist_env (alp,alpmetas) (terms,termlists,binders,binderlists) var vl = +let add_termlist_env (vars,(alp,alpmetas)) (terms,termlists,binders,binderlists) var vl = if List.exists (fun (id,_) -> List.exists (occur_glob_constr id) vl) alp then raise No_match; let vl = List.map (alpha_rename alpmetas) vl in - (terms,(var,vl)::termlists,binders,binderlists) + (terms,(var,(vars,vl))::termlists,binders,binderlists) -let add_binding_env alp (terms,termlists,binders,binderlists) var v = +let add_binding_env (vars,alp) (terms,termlists,binders,binderlists) var v = (* TODO: handle the case of multiple occs in different scopes *) - (terms,termlists,(var,v)::binders,binderlists) + (terms,termlists,(var,(vars,v))::binders,binderlists) -let add_bindinglist_env (terms,termlists,binders,binderlists) x bl = - (terms,termlists,binders,(x,bl)::binderlists) +let add_bindinglist_env (vars,alp) (terms,termlists,binders,binderlists) var bl = + (terms,termlists,binders,(var,(vars,bl))::binderlists) let rec map_cases_pattern_name_left f = DAst.map (function | PatVar na -> PatVar (f na) @@ -844,18 +950,19 @@ let rec pat_binder_of_term t = DAst.map (function | _ -> raise No_match ) t -let unify_name_upto alp na na' = +let unify_name_upto (vars,alp) na na' = match na, na' with - | Anonymous, na' -> alp, na' - | na, Anonymous -> alp, na + | Anonymous, na' -> (Termops.add_vname vars na',alp), na' + | na, Anonymous -> (Termops.add_vname vars na,alp), na | Name id, Name id' -> - if Id.equal id id' then alp, na' - else (fst alp,(id,id')::snd alp), na' + let vars = Termops.add_vname vars na' in + if Id.equal id id' then (vars,alp), na' + else (vars,(fst alp,(id,id')::snd alp)), na' let unify_pat_upto alp p p' = try fold_cases_pattern_eq unify_name_upto alp p p' with Failure _ -> raise No_match -let unify_term alp v v' = +let unify_term (_,alp) v v' = match DAst.get v, DAst.get v' with | GHole _, _ -> v' | _, GHole _ -> v @@ -898,13 +1005,13 @@ let rec unify_binders_upto alp bl bl' = alp, b :: bl | _ -> raise No_match -let unify_id alp id na' = +let unify_id (_,alp) id na' = match na' with | Anonymous -> Name (rename_var (snd alp) id) | Name id' -> if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match -let unify_pat alp p p' = +let unify_pat (_,alp) p p' = if cases_pattern_eq (map_cases_pattern_name_left (Name.map (rename_var (snd alp))) p) p' then p' else raise No_match @@ -930,33 +1037,37 @@ let rec unify_terms_binders alp cl bl' = let bind_term_env alp (terms,termlists,binders,binderlists as sigma) var v = try (* If already bound to a term, unify with the new term *) - let v' = Id.List.assoc var terms in + let vars,v' = Id.List.assoc var terms in let v'' = unify_term alp v v' in if v'' == v' then sigma else let sigma = (Id.List.remove_assoc var terms,termlists,binders,binderlists) in - add_env alp sigma var v + add_env (Id.Set.union vars (fst alp),snd alp) sigma var v with Not_found -> add_env alp sigma var v let bind_termlist_env alp (terms,termlists,binders,binderlists as sigma) var vl = try (* If already bound to a list of term, unify with the new terms *) - let vl' = Id.List.assoc var termlists in + let vars,vl' = Id.List.assoc var termlists in let vl = unify_terms alp vl vl' in let sigma = (terms,Id.List.remove_assoc var termlists,binders,binderlists) in - add_termlist_env alp sigma var vl + add_termlist_env (Id.Set.union vars (fst alp),snd alp) sigma var vl with Not_found -> add_termlist_env alp sigma var vl let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) var id = try (* If already bound to a term, unify the binder and the term *) - match DAst.get (Id.List.assoc var terms) with + let vars',v' = Id.List.assoc var terms in + match DAst.get v' with | GVar id' | GRef (GlobRef.VarRef id',None) -> - (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), - sigma + let (vars,(alpha,alpmetas)) = alp in + let vars = Id.Set.add id' vars in + let alpmetas = if not (Id.equal id id') then (id,id')::alpmetas else alpmetas in + (Id.Set.union vars' vars,(alpha,alpmetas)), sigma | t -> (* The term is a non-variable pattern *) raise No_match with Not_found -> + let alp = (Id.Set.add id (fst alp), snd alp) in (* The matching against a term allowing to find the instance has not been found yet *) (* If it will be a different name, we shall unfortunately fail *) (* TODO: look at the consequences for alp *) @@ -967,43 +1078,56 @@ let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) let pat = try cases_pattern_of_glob_constr env Anonymous c with Not_found -> raise No_match in try (* If already bound to a binder, unify the term and the binder *) - let patl' = Id.List.assoc var binders in + let vars,patl' = Id.List.assoc var binders in let patl'' = List.map2 (unify_pat alp) [pat] patl' in if patl' == patl'' then sigma else let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in - add_binding_env alp sigma var patl'' + add_binding_env (Id.Set.union vars (fst alp),snd alp) sigma var patl'' with Not_found -> add_binding_env alp sigma var [pat] let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var disjpat = try (* If already bound to a binder possibly *) (* generating an alpha-renaming from unifying the new binder *) - let disjpat' = Id.List.assoc var binders in + let vars,disjpat' = Id.List.assoc var binders in + (* if, maybe, there is eventually casts in patterns, the common types have *) + (* to exclude the spine of variable from the two locations they occur *) + let alp' = (Id.Set.union vars (fst alp),snd alp) in let alp, disjpat = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in + alp, add_binding_env alp' sigma var disjpat + with Not_found -> + (* Note: all patterns of the disjunction are supposed to have the same + variables, thus one is enough *) + let alp = (push_pattern_binders (fst alp) (List.hd disjpat), snd alp) in alp, add_binding_env alp sigma var disjpat - with Not_found -> alp, add_binding_env alp sigma var disjpat let bind_bindinglist_env alp (terms,termlists,binders,binderlists as sigma) var bl = let bl = List.rev bl in try (* If already bound to a list of binders possibly *) (* generating an alpha-renaming from unifying the new binders *) - let bl' = Id.List.assoc var binderlists in + let vars, bl' = Id.List.assoc var binderlists in + (* The shared subterm can be under two different spines of *) + (* variables (themselves bound in the notation) , so we take the *) + (* union of both locations *) + let alp' = (Id.Set.union vars (fst alp),snd alp) in let alp, bl = unify_binders_upto alp bl bl' in let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in - alp, add_bindinglist_env sigma var bl + alp, add_bindinglist_env alp' sigma var bl with Not_found -> - alp, add_bindinglist_env sigma var bl + let alp = (push_context_binders (fst alp) bl, snd alp) in + alp, add_bindinglist_env alp sigma var bl let bind_bindinglist_as_termlist_env alp (terms,termlists,binders,binderlists) var cl = try (* If already bound to a list of binders, unify the terms and binders *) - let bl' = Id.List.assoc var binderlists in + let vars,bl' = Id.List.assoc var binderlists in let bl = unify_terms_binders alp cl bl' in + let alp = (Id.Set.union vars (fst alp),snd alp) in let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in - add_bindinglist_env sigma var bl + add_bindinglist_env alp sigma var bl with Not_found -> anomaly (str "There should be a binder list bindings this list of terms.") @@ -1037,7 +1161,9 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (Anonymous,Name id2) when is_term_meta id2 metas -> (* We let the non-binding occurrence define the rhs *) alp, sigma - | (Name id1,Name id2) -> ((id1,id2)::fst alp, snd alp),sigma + | (Name id1,Name id2) -> + let (vars,(alp,alpmetas)) = alp in + (vars,((id1,id2)::alp,alpmetas)),sigma | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match @@ -1080,9 +1206,9 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert = try let metas = add_ldots_var (add_meta_bindinglist y metas) in let (terms,_,_,binderlists as sigma) = match_fun alp metas sigma rest iter in - let rest = Id.List.assoc ldots_var terms in + let _,rest = Id.List.assoc ldots_var terms in let b = - match Id.List.assoc y binderlists with [b] -> b | _ ->assert false + match Id.List.assoc y binderlists with _,[b] -> b | _ ->assert false in let sigma = remove_bindinglist_sigma y (remove_sigma ldots_var sigma) in (* In case y is bound not only to a binder but also to a term *) @@ -1111,18 +1237,20 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert = let add_meta_term x metas = (x,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeConstr))::metas (* Should reuse the scope of the partner of x! *) let match_termlist match_fun alp metas sigma rest x y iter termin revert = - let rec aux sigma acc rest = + let rec aux alp sigma acc rest = try let metas = add_ldots_var (add_meta_term y metas) in let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in - let rest = Id.List.assoc ldots_var terms in - let t = Id.List.assoc y terms in + let _,rest = Id.List.assoc ldots_var terms in + let vars,t = Id.List.assoc y terms in let sigma = remove_sigma y (remove_sigma ldots_var sigma) in if !print_parentheses && not (List.is_empty acc) then raise No_match; - aux sigma (t::acc) rest + (* The union is overkill at the current time because each term matches *) + (* at worst the same binder metavariable of the same pattern *) + aux (Id.Set.union vars (fst alp),snd alp) sigma (t::acc) rest with No_match when not (List.is_empty acc) -> - acc, match_fun metas sigma rest termin in - let l,(terms,termlists,binders,binderlists as sigma) = aux sigma [] rest in + alp, acc, match_fun metas sigma rest termin in + let alp,l,(terms,termlists,binders,binderlists as sigma) = aux alp sigma [] rest in let l = if revert then l else List.rev l in if is_bindinglist_meta x metas then (* This is a recursive pattern for both bindings and terms; it is *) @@ -1183,7 +1311,7 @@ let rec match_ inner u alp metas sigma a1 a2 = match_binderlist (match_hd u) alp metas sigma a1 x y iter termin revert (* Matching compositionally *) - | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma + | GVar id1, NVar id2 when alpha_var id1 id2 (fst (snd alp)) -> sigma | GRef (r1,_), NRef r2 when (GlobRef.equal r1 r2) -> sigma | GApp (f1,l1), NApp (f2,l2) -> let n1 = List.length l1 and n2 = List.length l2 in @@ -1353,9 +1481,9 @@ and match_disjunctive_equations u alp metas sigma {CAst.v=(ids,disjpatl1,rhs1)} (alp,sigma) disjpatl1 disjpatl2 in match_in u alp metas sigma rhs1 rhs2 -let match_notation_constr u c (metas,pat) = +let match_notation_constr ~print_univ c ~vars (metas,pat) = let terms,termlists,binders,binderlists = - match_ false u ([],[]) metas ([],[],[],[]) c pat in + match_ false print_univ (vars,([],[])) metas ([],[],[],[]) c pat in (* Turning substitution based on binding/constr distinction into a substitution based on entry productions *) List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders',binderlists') -> @@ -1365,9 +1493,9 @@ let match_notation_constr u c (metas,pat) = ((term, scl)::terms',termlists',binders',binderlists') | NtnTypeBinder (NtnBinderParsedAsConstr _) -> (match Id.List.assoc x binders with - | [pat] -> + | vars,[pat] -> let v = glob_constr_of_cases_pattern (Global.env()) pat in - ((v,scl)::terms',termlists',binders',binderlists') + (((vars,v),scl)::terms',termlists',binders',binderlists') | _ -> raise No_match) | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) -> (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists') diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 3cc6f82ec8..9d451a5bb9 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -16,6 +16,11 @@ open Glob_term val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool +val strictly_finer_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool +(** Tell if [t1] is a strict refinement of [t2] + (this is a partial order and returning [false] does not mean that + [t2] is finer than [t1]) *) + (** Substitution of kernel names in interpretation data *) val subst_interpretation : @@ -63,10 +68,11 @@ exception No_match val print_parentheses : bool ref -val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> - ('a glob_constr_g * extended_subscopes) list * ('a glob_constr_g list * extended_subscopes) list * - ('a cases_pattern_disjunction_g * extended_subscopes) list * - ('a extended_glob_local_binder_g list * extended_subscopes) list +val match_notation_constr : print_univ:bool -> 'a glob_constr_g -> vars:Id.Set.t -> interpretation -> + ((Id.Set.t * 'a glob_constr_g) * extended_subscopes) list * + ((Id.Set.t * 'a glob_constr_g list) * extended_subscopes) list * + ((Id.Set.t * 'a cases_pattern_disjunction_g) * extended_subscopes) list * + ((Id.Set.t * 'a extended_glob_local_binder_g list) * extended_subscopes) list val match_notation_constr_cases_pattern : 'a cases_pattern_g -> interpretation -> diff --git a/interp/reserve.ml b/interp/reserve.ml index 1d5af3ff39..274d3655d3 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -119,7 +119,7 @@ let revert_reserved_type t = then I've introduced a bug... *) let filter _ pat = try - let _ = match_notation_constr false t ([], pat) in + let _ = match_notation_constr ~print_univ:false t ~vars:Id.Set.empty ([], pat) in true with No_match -> false in |