diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr.ml | 6 | ||||
| -rw-r--r-- | interp/constrexpr_ops.ml | 107 | ||||
| -rw-r--r-- | interp/constrextern.ml | 28 | ||||
| -rw-r--r-- | interp/constrintern.ml | 152 | ||||
| -rw-r--r-- | interp/notation.ml | 3 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 204 | ||||
| -rw-r--r-- | interp/notation_ops.mli | 11 | ||||
| -rw-r--r-- | interp/notation_term.ml | 6 | ||||
| -rw-r--r-- | interp/reserve.ml | 2 |
9 files changed, 324 insertions, 195 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 977cbbccf2..b3f06faa1c 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -83,6 +83,8 @@ type cases_pattern_expr_r = | CPatCast of cases_pattern_expr * constr_expr and cases_pattern_expr = cases_pattern_expr_r CAst.t +and kinded_cases_pattern_expr = cases_pattern_expr * Glob_term.binding_kind + and cases_pattern_notation_substitution = cases_pattern_expr list * (* for constr subterms *) cases_pattern_expr list list (* for recursive notations *) @@ -145,12 +147,12 @@ and recursion_order_expr = recursion_order_expr_r CAst.t and local_binder_expr = | CLocalAssum of lname list * binder_kind * constr_expr | CLocalDef of lname * constr_expr * constr_expr option - | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t + | CLocalPattern of cases_pattern_expr and constr_notation_substitution = constr_expr list * (* for constr subterms *) constr_expr list list * (* for recursive notations *) - cases_pattern_expr list * (* for binders *) + kinded_cases_pattern_expr list * (* for binders *) local_binder_expr list list (* for binder lists (recursive notations) *) type constr_pattern_expr = constr_expr diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index efc2a35b65..a60dc11b57 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -94,6 +94,9 @@ and cases_pattern_notation_substitution_eq (s1, n1) (s2, n2) = List.equal cases_pattern_expr_eq s1 s2 && List.equal (List.equal cases_pattern_expr_eq) n1 n2 +let kinded_cases_pattern_expr_eq (p1,bk1) (p2,bk2) = + cases_pattern_expr_eq p1 p2 && Glob_ops.binding_kind_eq bk1 bk2 + let eq_universes u1 u2 = match u1, u2 with | None, None -> true @@ -231,7 +234,7 @@ and local_binder_eq l1 l2 = match l1, l2 with and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) = List.equal constr_expr_eq e1 e2 && List.equal (List.equal constr_expr_eq) el1 el2 && - List.equal cases_pattern_expr_eq b1 b2 && + List.equal kinded_cases_pattern_expr_eq b1 b2 && List.equal (List.equal local_binder_eq) bl1 bl2 and instance_eq (x1,c1) (x2,c2) = @@ -268,39 +271,37 @@ let is_constructor id = (Nametab.locate_extended (qualid_of_ident id))) with Not_found -> false -let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with +let rec cases_pattern_fold_names f h nacc pt = match CAst.(pt.v) with | CPatRecord l -> - List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l - | CPatAlias (pat,{CAst.v=na}) -> Name.fold_right f na (cases_pattern_fold_names f a pat) + List.fold_left (fun nacc (r, cp) -> cases_pattern_fold_names f h nacc cp) nacc l + | CPatAlias (pat,{CAst.v=na}) -> Name.fold_right (fun na (n,acc) -> (f na n,acc)) na (cases_pattern_fold_names f h nacc pat) | CPatOr (patl) -> - List.fold_left (cases_pattern_fold_names f) a patl + List.fold_left (cases_pattern_fold_names f h) nacc patl | CPatCstr (_,patl1,patl2) -> - List.fold_left (cases_pattern_fold_names f) - (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2 + List.fold_left (cases_pattern_fold_names f h) + (Option.fold_left (List.fold_left (cases_pattern_fold_names f h)) nacc patl1) patl2 | CPatNotation (_,_,(patl,patll),patl') -> - List.fold_left (cases_pattern_fold_names f) - (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl' - | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat + List.fold_left (cases_pattern_fold_names f h) + (List.fold_left (cases_pattern_fold_names f h) nacc (patl@List.flatten patll)) patl' + | CPatDelimiters (_,pat) -> cases_pattern_fold_names f h nacc pat | CPatAtom (Some qid) when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) -> - f (qualid_basename qid) a - | CPatPrim _ | CPatAtom _ -> a - | CPatCast ({CAst.loc},_) -> - CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names" - (Pp.strbrk "Casts are not supported here.") - -let ids_of_pattern = - cases_pattern_fold_names Id.Set.add Id.Set.empty - -let ids_of_pattern_list = - List.fold_left - (List.fold_left (cases_pattern_fold_names Id.Set.add)) - Id.Set.empty + let (n, acc) = nacc in + (f (qualid_basename qid) n, acc) + | CPatPrim _ | CPatAtom _ -> nacc + | CPatCast (p,t) -> + let (n, acc) = nacc in + cases_pattern_fold_names f h (n, h acc t) p + +let ids_of_pattern_list p = + fst (List.fold_left + (List.fold_left (cases_pattern_fold_names Id.Set.add (fun () _ -> ()))) + (Id.Set.empty,()) p) let ids_of_cases_tomatch tms = List.fold_right (fun (_, ona, indnal) l -> - Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t) + Option.fold_right (fun t ids -> fst (cases_pattern_fold_names Id.Set.add (fun () _ -> ()) (ids,()) t)) indnal (Option.fold_right (CAst.with_val (Name.fold_right Id.Set.add)) ona l)) tms Id.Set.empty @@ -312,9 +313,9 @@ let rec fold_local_binders g f n acc b = let open CAst in function f n (fold_local_binders g f n' acc b l) t | CLocalDef ( { v = na },c,t)::l -> Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t - | CLocalPattern { v = pat,t }::l -> - let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in - Option.fold_left (f n) acc t + | CLocalPattern pat :: l -> + let n, acc = cases_pattern_fold_names g (f n) (n,acc) pat in + fold_local_binders g f n acc b l | [] -> f n acc b @@ -378,10 +379,42 @@ let names_of_constr_expr c = let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c) +let rec fold_map_cases_pattern f h acc (CAst.{v=pt;loc} as p) = match pt with + | CPatRecord l -> + let acc, l = List.fold_left_map (fun acc (r, cp) -> let acc, cp = fold_map_cases_pattern f h acc cp in acc, (r, cp)) acc l in + acc, CAst.make ?loc (CPatRecord l) + | CPatAlias (pat,({CAst.v=na} as lna)) -> + let acc, p = fold_map_cases_pattern f h acc pat in + let acc = Name.fold_right f na acc in + acc, CAst.make ?loc (CPatAlias (pat,lna)) + | CPatOr patl -> + let acc, patl = List.fold_left_map (fold_map_cases_pattern f h) acc patl in + acc, CAst.make ?loc (CPatOr patl) + | CPatCstr (c,patl1,patl2) -> + let acc, patl1 = Option.fold_left_map (List.fold_left_map (fold_map_cases_pattern f h)) acc patl1 in + let acc, patl2 = List.fold_left_map (fold_map_cases_pattern f h) acc patl2 in + acc, CAst.make ?loc (CPatCstr (c,patl1,patl2)) + | CPatNotation (sc,ntn,(patl,patll),patl') -> + let acc, patl = List.fold_left_map (fold_map_cases_pattern f h) acc patl in + let acc, patll = List.fold_left_map (List.fold_left_map (fold_map_cases_pattern f h)) acc patll in + let acc, patl' = List.fold_left_map (fold_map_cases_pattern f h) acc patl' in + acc, CAst.make ?loc (CPatNotation (sc,ntn,(patl,patll),patl')) + | CPatDelimiters (d,pat) -> + let acc, p = fold_map_cases_pattern f h acc pat in + acc, CAst.make ?loc (CPatDelimiters (d,pat)) + | CPatAtom (Some qid) + when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) -> + f (qualid_basename qid) acc, p + | CPatPrim _ | CPatAtom _ -> (acc,p) + | CPatCast (pat,t) -> + let acc, pat = fold_map_cases_pattern f h acc pat in + let t = h acc t in + acc, CAst.make ?loc (CPatCast (pat,t)) + (* Used in correctness and interface *) let map_binder g e nal = List.fold_right (CAst.with_val (Name.fold_right g)) nal e -let map_local_binders f g e bl = +let fold_map_local_binders f g e bl = (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) let open CAst in let h (e,bl) = function @@ -389,9 +422,9 @@ let map_local_binders f g e bl = (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl) | CLocalDef( { loc ; v = na } as cna ,c,ty) -> (Name.fold_right g na e, CLocalDef(cna,f e c,Option.map (f e) ty)::bl) - | CLocalPattern { loc; v = pat,t } -> - let ids = ids_of_pattern pat in - (Id.Set.fold g ids e, CLocalPattern (make ?loc (pat,Option.map (f e) t))::bl) in + | CLocalPattern pat -> + let e, pat = fold_map_cases_pattern g f e pat in + (e, CLocalPattern pat::bl) in let (e,rbl) = List.fold_left h (e,[]) bl in (e, List.rev rbl) @@ -400,16 +433,16 @@ let map_constr_expr_with_binders g f e = CAst.map (function | CApp ((p,a),l) -> CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l) | CProdN (bl,b) -> - let (e,bl) = map_local_binders f g e bl in CProdN (bl,f e b) + let (e,bl) = fold_map_local_binders f g e bl in CProdN (bl,f e b) | CLambdaN (bl,b) -> - let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b) + let (e,bl) = fold_map_local_binders f g e bl in CLambdaN (bl,f e b) | CLetIn (na,a,t,b) -> CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b) | CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c) | CNotation (inscope,n,(l,ll,bl,bll)) -> (* This is an approximation because we don't know what binds what *) CNotation (inscope,n,(List.map (f e) l,List.map (List.map (f e)) ll, bl, - List.map (fun bl -> snd (map_local_binders f g e bl)) bll)) + List.map (fun bl -> snd (fold_map_local_binders f g e bl)) bll)) | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c) | CDelimiters (s,a) -> CDelimiters (s,f e a) | CHole _ | CEvar _ | CPatVar _ | CSort _ @@ -431,7 +464,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2) | CFix (id,dl) -> CFix (id,List.map (fun (id,n,bl,t,d) -> - let (e',bl') = map_local_binders f g e bl in + let (e',bl') = fold_map_local_binders f g e bl in let t' = f e' t in (* Note: fix names should be inserted before the arguments... *) let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_) -> g id e) e' dl in @@ -439,7 +472,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function (id,n,bl',t',d')) dl) | CCoFix (id,dl) -> CCoFix (id,List.map (fun (id,bl,t,d) -> - let (e',bl') = map_local_binders f g e bl in + let (e',bl') = fold_map_local_binders f g e bl in let t' = f e' t in let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in let d' = f e'' d in @@ -472,7 +505,7 @@ let locs_of_notation ?loc locs ntn = let ntn_loc ?loc (args,argslist,binders,binderslist) = locs_of_notation ?loc (List.map constr_loc (args@List.flatten argslist)@ - List.map cases_pattern_expr_loc binders@ + List.map (fun (x,_) -> cases_pattern_expr_loc x) binders@ List.map local_binders_loc binderslist) let patntn_loc ?loc (args,argslist) = diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d1bec16a3f..cf88036f73 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 @@ -1126,7 +1126,7 @@ and factorize_prod ?impargs scopes vars na bk t c = let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in let b = extern_typ scopes vars b in let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in - let binder = CLocalPattern (make ?loc:c.loc (p,None)) in + let binder = CLocalPattern p in (match b.v with | CProdN (bl,b) -> CProdN (binder::bl,b) | _ -> CProdN ([binder],b)) @@ -1167,7 +1167,7 @@ and factorize_lambda inctx scopes vars na bk t c = let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in let b = sub_extern inctx scopes vars b in let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in - let binder = CLocalPattern (make ?loc:c.loc (p,None)) in + let binder = CLocalPattern p in (match b.v with | CLambdaN (bl,b) -> CLambdaN (binder::bl,b) | _ -> CLambdaN ([binder],b)) @@ -1219,7 +1219,10 @@ and extern_local_binder scopes vars = function if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in let p = mkCPatOr (List.map (extern_cases_pattern vars) p) in let (assums,ids,l) = extern_local_binder scopes vars l in - (assums,ids, CLocalPattern(CAst.make @@ (p,ty)) :: l) + let p = match ty with + | None -> p + | Some ty -> CAst.make @@ (CPatCast (p,ty)) in + (assums,ids, CLocalPattern p :: l) and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in @@ -1273,7 +1276,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 +1296,21 @@ 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))) -> - mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)) + List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> + (mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)), + Explicit) 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 +1320,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..8bd77abc4a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -298,21 +298,20 @@ let error_expect_binder_notation_type ?loc id = let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars = try let used_as_binder,idscopes,typ = Id.Map.find id ntnvars in - if not istermvar then used_as_binder := true; - let () = if istermvar then + if istermvar then begin (* scopes have no effect on the interpretation of identifiers *) - begin match !idscopes with + (match !idscopes with | None -> idscopes := Some scopes | Some (tmp_scope', subscopes') -> let s' = make_current_scope tmp_scope' subscopes' in let s = make_current_scope tmp_scope subscopes in - if not (List.equal String.equal s' s) then error_inconsistent_scope ?loc id s' s + if not (List.equal String.equal s' s) then error_inconsistent_scope ?loc id s' s); + (match typ with + | Notation_term.NtnInternTypeOnlyBinder -> error_expect_binder_notation_type ?loc id + | Notation_term.NtnInternTypeAny -> ()) end - in - match typ with - | Notation_term.NtnInternTypeOnlyBinder -> - if istermvar then error_expect_binder_notation_type ?loc id - | Notation_term.NtnInternTypeAny -> () + else + used_as_binder := true with Not_found -> (* Not in a notation *) () @@ -534,15 +533,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) @@ -583,7 +586,10 @@ let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) = (push_name_env ntnvars impls env locna, (na,Explicit,term,ty)) -let intern_cases_pattern_as_binder ?loc test_kind ntnvars env p = +let intern_cases_pattern_as_binder intern test_kind ntnvars env bk (CAst.{v=p;loc} as pv) = + let p,t = match p with + | CPatCast (p, t) -> (p, Some t) + | _ -> (pv, None) in let il,disjpat = let (il, subst_disjpat) = !intern_cases_pattern_fwd test_kind ntnvars (env_for_pattern (reset_tmp_scope env)) p in let substl,disjpat = List.split subst_disjpat in @@ -591,12 +597,17 @@ let intern_cases_pattern_as_binder ?loc test_kind ntnvars env p = user_err ?loc (str "Unsupported nested \"as\" clause."); il,disjpat in - let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars [] env (make ?loc @@ Name id)) il env in let na = alias_of_pat (List.hd disjpat) in + let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars [] env (make ?loc @@ Name id)) il env in let ienv = Name.fold_right Id.Set.remove na env.ids in let id = Namegen.next_name_away_with_default "pat" na ienv in let na = make ?loc @@ Name id in - env,((disjpat,il),id),na + let t = match t with + | Some t -> t + | None -> CAst.make ?loc @@ CHole(Some (Evar_kinds.BinderType na.v),IntroAnonymous,None) in + let _, bl' = intern_assumption intern ntnvars env [na] (Default bk) t in + let {v=(_,bk,t)} = List.hd bl' in + env,((disjpat,il),id),na,bk,t let intern_local_binder_aux intern ntnvars (env,bl) = function | CLocalAssum(nal,bk,ty) -> @@ -606,17 +617,9 @@ let intern_local_binder_aux intern ntnvars (env,bl) = function | CLocalDef( {loc; v=na} as locna,def,ty) -> let env,(na,bk,def,ty) = intern_letin_binder intern ntnvars env (locna,def,ty) in env, (DAst.make ?loc @@ GLocalDef (na,bk,def,ty)) :: bl - | CLocalPattern {loc;v=(p,ty)} -> - let tyc = - match ty with - | Some ty -> ty - | None -> CAst.make ?loc @@ CHole(None,IntroAnonymous,None) - in - let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc test_kind_tolerant ntnvars env p in - let bk = Default Explicit in - let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in - let {v=(_,bk,t)} = List.hd bl' in - (env, (DAst.make ?loc @@ GLocalPattern((disjpat,List.map (fun x -> x.v) il),id,bk,t)) :: bl) + | CLocalPattern p -> + let env, ((disjpat,il),id),na,bk,t = intern_cases_pattern_as_binder intern test_kind_tolerant ntnvars env Explicit p in + (env, (DAst.make ?loc:p.CAst.loc @@ GLocalPattern((disjpat,List.map (fun x -> x.v) il),id,bk,t)) :: bl) let intern_generalization intern env ntnvars loc bk ak c = let c = intern {env with unb = true} c in @@ -702,7 +705,7 @@ let is_patvar c = let is_patvar_store store pat = match DAst.get pat with - | PatVar na -> ignore(store na); true + | PatVar na -> ignore(store (CAst.make ?loc:pat.loc na)); true | _ -> false let out_patvar = CAst.map_with_loc (fun ?loc -> function @@ -711,37 +714,57 @@ let out_patvar = CAst.map_with_loc (fun ?loc -> function | CPatAtom None -> Anonymous | _ -> assert false) -let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function - | Anonymous -> (renaming,env), None, Anonymous +let canonize_type = function + | None -> None + | Some t as t' -> + match DAst.get t with + | GHole (Evar_kinds.BinderType _,IntroAnonymous,None) -> None + | _ -> t' + +let set_type ty1 ty2 = + match canonize_type ty1, canonize_type ty2 with + (* Not a meta-binding binder, we use the type given in the notation *) + | _, None -> ty1 + (* A meta-binding binder meta-bound to a possibly-typed pattern *) + (* the binder is supposed to come w/o an explicit type in the notation *) + | None, Some _ -> ty2 + | Some ty1, Some t2 -> + (* An explicitly typed meta-binding binder, not supposed to be a pattern; checked in interp_notation *) + user_err ?loc:t2.CAst.loc Pp.(str "Unexpected type constraint in notation already providing a type constraint.") + +let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) na ty = + match na with + | Anonymous -> (renaming,env), None, Anonymous, Explicit, set_type ty None | Name id -> let store,get = set_temporary_memory () in let test_kind = test_kind_tolerant in try (* We instantiate binder name with patterns which may be parsed as terms *) let pat = coerce_to_cases_pattern_expr (fst (Id.Map.find id terms)) in - let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars env pat in + let env,((disjpat,ids),id),na,bk,t = intern_pat test_kind ntnvars env Explicit pat in let pat, na = match disjpat with | [pat] when is_patvar_store store pat -> let na = get () in None, na - | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in - (renaming,env), pat, na + | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na in + (renaming,env), pat, na.v, bk, set_type ty (Some t) with Not_found -> try (* Trying to associate a pattern *) - let pat,(onlyident,scopes) = Id.Map.find id binders in + let (pat,bk),(onlyident,scopes) = Id.Map.find id binders in let env = set_env_scopes env scopes in if onlyident then (* Do not try to interpret a variable as a constructor *) let na = out_patvar pat in let env = push_name_env ntnvars [] env na in - (renaming,env), None, na.v + let ty' = DAst.make @@ GHole (Evar_kinds.BinderType na.CAst.v,IntroAnonymous,None) in + (renaming,env), None, na.v, bk, set_type ty (Some ty') else (* Interpret as a pattern *) - let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars env pat in + let env,((disjpat,ids),id),na,bk,t = intern_pat test_kind ntnvars env bk pat in let pat, na = match disjpat with | [pat] when is_patvar_store store pat -> let na = get () in None, na - | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in - (renaming,env), pat, na + | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na in + (renaming,env), pat, na.v, bk, set_type ty (Some t) with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -749,7 +772,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let renaming' = if Id.equal id id' then renaming else Id.Map.add id id' renaming in - (renaming',env), None, Name id' + (renaming',env), None, Name id', Explicit, set_type ty None type binder_action = | AddLetIn of lname * constr_expr * constr_expr option @@ -874,12 +897,13 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = Id.Map.add id (gc, None) map with Nametab.GlobalizationError _ -> map in - let mk_env' (c, (onlyident,scopes)) = - let nenv = set_env_scopes env scopes in + let mk_env' ((c,_bk), (onlyident,(tmp_scope,subscopes))) = + let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in let test_kind = if onlyident then test_kind_ident_in_notation else test_kind_pattern_in_notation in - let _,((disjpat,_),_),_ = intern_pat test_kind ntnvars nenv c in + let _,((disjpat,_),_),_,_,_ty = intern_pat test_kind ntnvars nenv Explicit c in + (* TODO: use cast? *) match disjpat with | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None) | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () @@ -904,26 +928,15 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = aux (terms,None,Some (l,terminator,iter)) subinfos (NVar ldots_var) with Not_found -> anomaly (Pp.str "Inconsistent substitution of recursive notation.")) - | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt -> + | NProd (Name id, None, c') when option_mem_assoc id binderopt -> let binder = snd (Option.get binderopt) in expand_binders ?loc mkGProd [binder] (aux subst' (renaming,env) c') - | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt -> + | NLambda (Name id, None, c') when option_mem_assoc id binderopt -> let binder = snd (Option.get binderopt) in expand_binders ?loc mkGLambda [binder] (aux subst' (renaming,env) c') - (* Two special cases to keep binder name synchronous with BinderType *) - | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c') - when Name.equal na na' -> - let subinfos,disjpat,na = traverse_binder intern_pat ntnvars subst avoid subinfos na in - let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in - DAst.make ?loc @@ GProd (na,Explicit,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c')) - | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c') - when Name.equal na na' -> - let subinfos,disjpat,na = traverse_binder intern_pat ntnvars subst avoid subinfos na in - let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in - DAst.make ?loc @@ GLambda (na,Explicit,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c')) | t -> glob_constr_of_notation_constr_with_binders ?loc - (traverse_binder intern_pat ntnvars subst avoid) (aux subst') ~h:binder_status_fun subinfos t + (traverse_binder intern_pat ntnvars subst avoid) (aux subst') ~h:binder_status_fun subinfos t and subst_var (terms, binderopt, _terminopt) (renaming, env) id = (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) @@ -932,12 +945,13 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = intern (set_env_scopes env scopes) a with Not_found -> try - let pat,(onlyident,scopes) = Id.Map.find id binders in - let nenv = set_env_scopes env scopes in + let (pat,bk),(onlyident,scopes) = Id.Map.find id binders in + let env = set_env_scopes env scopes in let test_kind = if onlyident then test_kind_ident_in_notation else test_kind_pattern_in_notation in - let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars nenv pat in + let env,((disjpat,ids),id),na,bk,_ty = intern_pat test_kind ntnvars env bk pat in + (* TODO: use cast? *) match disjpat with | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.") @@ -979,13 +993,13 @@ let split_by_type ids subst = (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in - let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in + let binders' = Id.Map.add id ((coerce_to_cases_pattern_expr a,Explicit),(false,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') | NtnTypeBinder NtnBinderParsedAsConstr AsIdent -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in - let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in + let binders' = Id.Map.add id ((cases_pattern_of_name (coerce_to_name a),Explicit),(true,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ as x) -> + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder as x) -> let onlyident = (x = NtnParsedAsIdent) in let binders,binders' = bind id (onlyident,scl) binders binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') @@ -1027,7 +1041,7 @@ let intern_notation intern env ntnvars loc ntn fullargs = (* Dispatch parsing substitution to an interpretation substitution *) let subst = split_by_type ids fullargs in (* Instantiate the notation *) - instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst (Id.Map.empty, env) c + instantiate_notation_constr loc intern (intern_cases_pattern_as_binder intern) ntnvars subst (Id.Map.empty, env) c (**********************************************************************) (* Discriminating between bound variables and global references *) @@ -1155,7 +1169,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = check_no_explicitation args1; let subst = split_by_type ids (List.map fst args1,[],[],[]) in let infos = (Id.Map.empty, env) in - let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in + let c = instantiate_notation_constr loc intern (intern_cases_pattern_as_binder intern) ntnvars subst infos c in let loc = c.loc in let err () = user_err ?loc (str "Notation " ++ pr_qualid qid diff --git a/interp/notation.ml b/interp/notation.ml index 286ece6cb6..b5951a9c59 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -64,7 +64,8 @@ let notation_binder_source_eq s1 s2 = match s1, s2 with | NtnParsedAsIdent, NtnParsedAsIdent -> true | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 | NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2 -| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false +| NtnParsedAsBinder, NtnParsedAsBinder -> true +| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index d393dcaecb..f51d3bfdfb 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -131,7 +131,11 @@ let compare_notation_constr lt (vars1,vars2) t1 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; + (match t1, t2 with + | None, None -> () + | Some _, None -> if lt then strictly_lt := true + | Some t1, Some t2 -> aux vars renaming t1 t2 + | None, Some _ -> raise Exit); 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) -> @@ -272,11 +276,25 @@ let default_binder_status_fun = { slide = (fun x -> x); } +let test_implicit_argument_mark bk = + if not (Glob_ops.binding_kind_eq bk Explicit) then + user_err (Pp.str "Unexpected implicit argument mark.") + +let test_pattern_cast = function + | None -> () + | Some t -> user_err ?loc:t.CAst.loc (Pp.str "Unsupported pattern cast.") + let protect g e na = - let e',disjpat,na = g e na in + let e',disjpat,na,bk,t = g e na None in if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern."); + test_implicit_argument_mark bk; + test_pattern_cast t; e',na +let set_anonymous_type na = function + | None -> DAst.make @@ GHole (Evar_kinds.BinderType na, IntroAnonymous, None) + | Some t -> t + let apply_cases_pattern_term ?loc (ids,disjpat) tm c = let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns) @@ -302,15 +320,21 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat DAst.get (subst_glob_vars outerl it) | NLambda (na,ty,c) -> let e = h.switch_lambda e in - let e',disjpat,na = g e na in GLambda (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) + let ty = Option.map (f (h.restart_prod e)) ty in + let e',disjpat,na',bk,ty = g e na ty in + GLambda (na',bk,set_anonymous_type na ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) | NProd (na,ty,c) -> let e = h.switch_prod e in - let e',disjpat,na = g e na in GProd (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) + let ty = Option.map (f (h.restart_prod e)) ty in + let e',disjpat,na',bk,ty = g e na ty in + GProd (na',bk,set_anonymous_type na ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) | NLetIn (na,b,t,c) -> - let e',disjpat,na = g e na in + let t = Option.map (f (h.restart_prod e)) t in + let e',disjpat,na,bk,t = g e na t in + test_implicit_argument_mark bk; (match disjpat with - | None -> GLetIn (na,f (h.restart_lambda e) b,Option.map (f (h.restart_prod e)) t,f e' c) - | Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c))) + | None -> GLetIn (na,f (h.restart_lambda e) b,t,f e' c) + | Some (disjpat,_id) -> test_pattern_cast t; DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c))) | NCases (sty,rtntypopt,tml,eqnl) -> let e = h.no e in let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> @@ -323,7 +347,11 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat e',Some (CAst.make ?loc (ind,nal')) in let e',na' = protect g e' na in (e',(f e tm,(na',t'))::tml')) tml (e,[]) in - let fold (idl,e) na = let (e,disjpat,na) = g e na in ((Name.cons na idl,e),disjpat,na) in + let fold (idl,e) na = + let (e,disjpat,na,bk,t) = g e na None in + test_implicit_argument_mark bk; + test_pattern_cast t; + ((Name.cons na idl,e),disjpat,na) in let eqnl' = List.map (fun (patl,rhs) -> let ((idl,e),patl) = List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in @@ -356,7 +384,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat let glob_constr_of_notation_constr ?loc x = let rec aux () x = - glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),None,id)) aux () x + glob_constr_of_notation_constr_with_binders ?loc (fun () id t -> ((),None,id,Explicit,t)) aux () x in aux () x (******************************************************************************) @@ -551,8 +579,8 @@ let notation_constr_and_vars_of_glob_constr recvars a = | GApp (g,args) -> (* Treat applicative notes as binary nodes *) let a,args = List.sep_last args in mkNApp1 (aux (DAst.make (GApp (g, args))), aux a) - | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c) - | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c) + | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux_type ty,aux c) + | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux_type ty,aux c) | GLetIn (na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t, aux c) | GCases (sty,rtntypopt,tml,eqnl) -> let f {CAst.v=(idl,pat,rhs)} = List.iter (add_id found) idl; (pat,aux rhs) in @@ -589,6 +617,9 @@ let notation_constr_and_vars_of_glob_constr recvars a = | GEvar _ | GPatVar _ -> user_err Pp.(str "Existential variables not allowed in notations.") ) x + and aux_type t = DAst.with_val (function + | GHole (Evar_kinds.BinderType _,IntroAnonymous,None) -> None + | _ -> Some (aux t)) t in let t = aux a in (* Side effect *) @@ -697,13 +728,13 @@ let rec subst_notation_constr subst bound raw = NList (id1,id2,r1',r2',b) | NLambda (n,r1,r2) -> - let r1' = subst_notation_constr subst bound r1 + let r1' = Option.Smart.map (subst_notation_constr subst bound) r1 and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else NLambda (n,r1',r2') | NProd (n,r1,r2) -> - let r1' = subst_notation_constr subst bound r1 + let r1' = Option.Smart.map (subst_notation_constr subst bound) r1 and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else NProd (n,r1',r2') @@ -819,7 +850,21 @@ let abstract_return_type_context_glob_constr tml rtn = 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 + (fun na c -> NLambda(na,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 @@ -838,6 +883,7 @@ let is_onlybinding_pattern_like_meta isvar id metas = | _,NtnTypeBinder (NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern)) -> true | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar) + | _,NtnTypeBinder NtnParsedAsBinder -> not isvar | _ -> false with Not_found -> false @@ -851,7 +897,7 @@ 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 @@ -879,19 +925,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) @@ -936,18 +982,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 @@ -990,13 +1037,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 @@ -1022,33 +1069,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 *) @@ -1059,43 +1110,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.") @@ -1129,7 +1193,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 @@ -1172,9 +1238,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 *) @@ -1203,18 +1269,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 *) @@ -1275,7 +1343,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 @@ -1289,9 +1357,9 @@ let rec match_ inner u alp metas sigma a1 a2 = List.fold_left2 (match_ may_use_eta u alp metas) (match_hd u alp metas sigma f1 f2) l1 l2 | GLambda (na1,bk1,t1,b1), NLambda (na2,t2,b2) -> - match_extended_binders false u alp metas na1 na2 bk1 t1 (match_in u alp metas sigma t1 t2) b1 b2 + match_extended_binders false u alp metas na1 na2 bk1 t1 (match_in_type u alp metas sigma t1 t2) b1 b2 | GProd (na1,bk1,t1,b1), NProd (na2,t2,b2) -> - match_extended_binders true u alp metas na1 na2 bk1 t1 (match_in u alp metas sigma t1 t2) b1 b2 + match_extended_binders true u alp metas na1 na2 bk1 t1 (match_in_type u alp metas sigma t1 t2) b1 b2 | GLetIn (na1,b1,_,c1), NLetIn (na2,b2,None,c2) | GLetIn (na1,b1,None,c1), NLetIn (na2,b2,_,c2) -> match_binders u alp metas na1 na2 (match_in u alp metas sigma b1 b2) c1 c2 @@ -1360,14 +1428,14 @@ let rec match_ inner u alp metas sigma a1 a2 = otherwise how to ensure it corresponds to a well-typed eta-expansion; we make an exception for types which are metavariables: this is useful e.g. to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *) - | _b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner -> + | _b1, NLambda (Name id as na,(None | Some (NVar _) as t2),b2) when inner -> let avoid = Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in let id' = Namegen.next_ident_away id avoid in let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),IntroAnonymous,None) in let sigma = match t2 with - | NHole _ -> sigma - | NVar id2 -> bind_term_env alp sigma id2 t1 + | None -> sigma + | Some (NVar id2) -> bind_term_env alp sigma id2 t1 | _ -> assert false in let (alp,sigma) = if is_bindinglist_meta id metas then @@ -1387,6 +1455,10 @@ let rec match_ inner u alp metas sigma a1 a2 = | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ | GInt _ | GFloat _ | GArray _), _ -> raise No_match +and match_in_type u alp metas sigma t = function + | None -> sigma + | Some t' -> match_in u alp metas sigma t t' + and match_in u = match_ true u and match_hd u = match_ false u @@ -1445,9 +1517,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') -> @@ -1457,11 +1529,11 @@ 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 _) -> + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder) -> (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists') | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists') diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 3182ea96d7..e7a0429b35 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -53,7 +53,7 @@ val apply_cases_pattern : ?loc:Loc.t -> (Id.t list * cases_pattern_disjunction) * Id.t -> glob_constr -> glob_constr val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t -> - ('a -> Name.t -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t) -> + ('a -> Name.t -> glob_constr option -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t * Glob_term.binding_kind * glob_constr option) -> ('a -> notation_constr -> glob_constr) -> ?h:'a binder_status_fun -> 'a -> notation_constr -> glob_constr @@ -68,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/notation_term.ml b/interp/notation_term.ml index 82238b71b7..29db23cc54 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -27,8 +27,8 @@ type notation_constr = | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool (* Part only in [glob_constr] *) - | NLambda of Name.t * notation_constr * notation_constr - | NProd of Name.t * notation_constr * notation_constr + | NLambda of Name.t * notation_constr option * notation_constr + | NProd of Name.t * notation_constr option * notation_constr | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr | NCases of Constr.case_style * notation_constr option * @@ -78,6 +78,8 @@ type notation_binder_source = | NtnParsedAsIdent (* This accepts ident, or pattern, or both *) | NtnBinderParsedAsConstr of constr_as_binder_kind + (* This accepts ident, _, and quoted pattern *) + | NtnParsedAsBinder type notation_var_instance_type = | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList 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 |