From 09122b77b4f556281fec338cbb2ec43c5520dc8d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 21 Nov 2017 18:03:11 +0100 Subject: Again one more step in fixing #5762 ("where" clause). We enforce that variables of the notation hide the variables in the implicit-arguments map. Will be useful when there will be a special map of single binders when interpreting notations. --- interp/constrintern.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4afe301dd7..b52a280291 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2161,6 +2161,7 @@ let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = (* [vl] is intended to remember the scope of the free variables of [a] *) let vl = Id.Map.map (fun typ -> (ref true, ref None, typ)) nenv.ninterp_var_type in + let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in let c = internalize (Global.env()) {ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impls} false (empty_ltac_sign, vl) a in -- cgit v1.2.3 From 65505b835d6a77b8702d11d09e8cf6b84c529c65 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 13:42:01 +0200 Subject: Adding support for re-folding notation referring to isolated "forall '(x,y), t". Was apparently forgotten in a67bd7f9. --- interp/notation_ops.ml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) (limited to 'interp') diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 326d05cba6..2e3f19a37d 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1084,11 +1084,18 @@ let rec match_ inner u alp metas sigma a1 a2 = | _ -> match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 end - - | GProd (na,bk,t,b1), NProd (Name id,_,b2) - when is_bindinglist_meta id metas && na != Anonymous -> - let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na,bk,t)] in + | GProd (na1, bk, t1, b1), NProd (na2, t2, b2) -> + begin match na1, DAst.get b1, na2 with + | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id + when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) -> + let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] in match_in u alp metas sigma b1 b2 + | _, _, Name id when is_bindinglist_meta id metas && na1 != Anonymous -> + let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] in + match_in u alp metas sigma b1 b2 + | _ -> + match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 + end (* Matching compositionally *) | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma @@ -1104,8 +1111,6 @@ let rec match_ inner u alp metas sigma a1 a2 = let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in List.fold_left2 (match_ may_use_eta u alp metas) (match_in u alp metas sigma f1 f2) l1 l2 - | GProd (na1,_,t1,b1), NProd (na2,t2,b2) -> - match_binders u alp metas na1 na2 (match_in 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 -- cgit v1.2.3 From 6e1f26a075a48fb32bce32e07d6b58e2f38b97a5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 14:23:11 +0200 Subject: More precise explanation when a notation is not reversible for printing. --- interp/constrintern.mli | 2 +- interp/notation_ops.ml | 11 +++++++---- interp/notation_ops.mli | 2 +- 3 files changed, 9 insertions(+), 6 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 632b423b05..87b587b71c 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -185,7 +185,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_ val interp_notation_constr : env -> ?impls:internalization_env -> notation_interp_env -> constr_expr -> (bool * subscopes * notation_var_internalization_type) Id.Map.t * - notation_constr * reversibility_flag + notation_constr * reversibility_status (** Globalization options *) val parsing_explicit : bool ref diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 2e3f19a37d..472b9de599 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -396,7 +396,7 @@ let notation_constr_and_vars_of_glob_constr a = t, !found, !has_ltac let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = - let injective = ref true in + let injective = ref [] in let recvars = nenv.ninterp_rec_vars in let fold _ y accu = Id.Set.add y accu in let useless_vars = Id.Map.fold fold recvars Id.Set.empty in @@ -419,7 +419,7 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = user_err Pp.(str (Id.to_string x ^ " should not be bound in a recursive pattern of the right-hand side.")) - else injective := false + else injective := x :: !injective in let check_pair s x y where = if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then @@ -440,12 +440,15 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = end | NtnInternTypeIdent -> check_bound x in Id.Map.iter check_type vars; - !injective + List.rev !injective let notation_constr_of_glob_constr nenv a = let a, found, has_ltac = notation_constr_and_vars_of_glob_constr a in let injective = check_variables_and_reversibility nenv found in - a, not has_ltac && injective + let status = if has_ltac then HasLtac else match injective with + | [] -> APrioriReversible + | l -> NonInjective l in + a, status (**********************************************************************) (* Substitution of kernel names, avoiding a list of bound identifiers *) diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 0904a4ea3e..80348c78ee 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -29,7 +29,7 @@ val ldots_var : Id.t bound by the notation; also interpret recursive patterns *) val notation_constr_of_glob_constr : notation_interp_env -> - glob_constr -> notation_constr * reversibility_flag + glob_constr -> notation_constr * reversibility_status (** Re-interpret a notation as a [glob_constr], taking care of binders *) -- cgit v1.2.3 From 66eae7fa7f8e1f075a8c84afad48af4d35c4bfaf Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 22 Nov 2017 05:32:17 +0100 Subject: Notations: Do not consider a non-occurring variable as a binder-only variable. --- interp/constrintern.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b52a280291..2761b65285 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2170,8 +2170,9 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = (* Splits variables into those that are binding, bound, or both *) (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l in - let vars = Id.Map.map (fun (isonlybinding, sc, typ) -> - (!isonlybinding, out_scope !sc, typ)) vl in + let unused = match reversible with NonInjective ids -> ids | _ -> [] in + let vars = Id.Map.mapi (fun id (isonlybinding, sc, typ) -> + (!isonlybinding && not (List.mem_f Id.equal id unused), out_scope !sc, typ)) vl in (* Returns [a] and the ordered list of variables with their scopes *) vars, a, reversible -- cgit v1.2.3 From 6b9a9124d3bd24fe9305df613547139f6f609c60 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Aug 2017 16:15:57 +0200 Subject: Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr. The motivations are: - To reflect the concrete syntax more closely. - To factorize the different places where "contexts" are internalized: before this patch, there is a different treatment of `Definition f '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack to interpret `Definition f `pat := c : t`. With the patch, the fix to avoid seeing a variable named `pat` works for both `fun 'x => ...` and `Definition f 'x := ...`. The drawbacks are: - Counterpart to reflecting the concrete syntax more closerly, there are more redundancies in the syntax. For instance, the case `CLetIn (na,b,t,c)` can appears also in the form `CProdN (CLocalDef (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`. - Changes in the API, hence adaptation of plugins referring to `constr_expr` needed. --- interp/constrexpr_ops.ml | 81 ++++++------------------------------------------ interp/constrextern.ml | 66 +++++++++++++++++++++++++++------------ interp/constrintern.ml | 46 +++++++++++++-------------- 3 files changed, 78 insertions(+), 115 deletions(-) (limited to 'interp') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index da04d8786b..9fe890e901 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -112,10 +112,10 @@ let rec constr_expr_eq e1 e2 = eq_located Id.equal id1 id2 && List.equal cofix_expr_eq fl1 fl2 | CProdN(bl1,a1), CProdN(bl2,a2) -> - List.equal binder_expr_eq bl1 bl2 && + List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 | CLambdaN(bl1,a1), CLambdaN(bl2,a2) -> - List.equal binder_expr_eq bl1 bl2 && + List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 | CLetIn((_,na1),a1,t1,b1), CLetIn((_,na2),a2,t2,b2) -> Name.equal na1 na2 && @@ -193,10 +193,6 @@ and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) = List.equal (List.equal cases_pattern_expr_eq) p1 p2 && constr_expr_eq e1 e2 -and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) = - (** Don't care about the [binder_kind] *) - List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 - and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) = (eq_located Id.equal id1 id2) && Option.equal (eq_located Id.equal) j1 j2 && @@ -307,14 +303,6 @@ let ids_of_cases_tomatch tms = (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l)) tms Id.Set.empty -let rec fold_constr_expr_binders g f n acc b = function - | (nal,bk,t)::l -> - let nal = snd (List.split nal) in - let n' = List.fold_right (Name.fold_right g) nal n in - f n (fold_constr_expr_binders g f n' acc b l) t - | [] -> - f n acc b - let rec fold_local_binders g f n acc b = function | CLocalAssum (nal,bk,t)::l -> let nal = snd (List.split nal) in @@ -331,7 +319,7 @@ let rec fold_local_binders g f n acc b = function let fold_constr_expr_with_binders g f n acc = CAst.with_val (function | CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) - | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l + | CProdN (l,b) | CLambdaN (l,b) -> fold_local_binders g f n acc b l | CLetIn (na,a,t,b) -> f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b @@ -382,12 +370,6 @@ let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c) (* Used in correctness and interface *) let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e -let map_binders f g e bl = - (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) - let h (e,bl) (nal,bk,t) = (map_binder g e nal,(nal,bk,f e t)::bl) in - let (e,rbl) = List.fold_left h (e,[]) bl in - (e, List.rev rbl) - let map_local_binders f g e bl = (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) let h (e,bl) = function @@ -406,9 +388,9 @@ 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_binders f g e bl in CProdN (bl,f e b) + let (e,bl) = map_local_binders f g e bl in CProdN (bl,f e b) | CLambdaN (bl,b) -> - let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b) + let (e,bl) = 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 (snd na) e) b) | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) @@ -529,9 +511,9 @@ let split_at_annot bl na = let mkIdentC id = CAst.make @@ CRef (Ident (Loc.tag id),None) let mkRefC r = CAst.make @@ CRef (r,None) let mkCastC (a,k) = CAst.make @@ CCast (a,k) -let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([idl,bk,a],b) +let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,bk,a)],b) let mkLetInC (id,a,t,b) = CAst.make @@ CLetIn (id,a,t,b) -let mkProdC (idl,bk,a,b) = CAst.make @@ CProdN ([idl,bk,a],b) +let mkProdC (idl,bk,a,b) = CAst.make @@ CProdN ([CLocalAssum (idl,bk,a)],b) let mkAppC (f,l) = let l = List.map (fun x -> (x,None)) l in @@ -539,56 +521,11 @@ let mkAppC (f,l) = | CApp (g,l') -> CAst.make @@ CApp (g, l' @ l) | _ -> CAst.make @@ CApp ((None, f), l) -let add_name_in_env env n = - match snd n with - | Anonymous -> env - | Name id -> id :: env - -let fresh_var env c = - Namegen.next_ident_away (Id.of_string "pat") - (List.fold_left (fun accu id -> Id.Set.add id accu) (free_vars_of_constr_expr c) env) - -let expand_binders ?loc mkC bl c = - let rec loop ?loc bl c = - match bl with - | [] -> ([], c) - | b :: bl -> - match b with - | CLocalDef ((loc1,_) as n, oty, b) -> - let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in - let env = add_name_in_env env n in - (env, CAst.make ?loc @@ CLetIn (n,oty,b,c)) - | CLocalAssum ((loc1,_)::_ as nl, bk, t) -> - let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in - let env = List.fold_left add_name_in_env env nl in - (env, mkC ?loc (nl,bk,t) c) - | CLocalAssum ([],_,_) -> loop ?loc bl c - | CLocalPattern (loc1, (p, ty)) -> - let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in - let ni = fresh_var env c in - let id = (loc1, Name ni) in - let ty = match ty with - | Some ty -> ty - | None -> CAst.make ?loc:loc1 @@ CHole (None, IntroAnonymous, None) - in - let e = CAst.make @@ CRef (Libnames.Ident (loc1, ni), None) in - let c = CAst.make ?loc @@ - CCases - (LetPatternStyle, None, [(e,None,None)], - [(Loc.tag ?loc:loc1 ([[p]], c))]) - in - (ni :: env, mkC ?loc ([id],Default Explicit,ty) c) - in - let (_, c) = loop ?loc bl c in - c - let mkCProdN ?loc bll c = - let mk ?loc b c = CAst.make ?loc @@ CProdN ([b],c) in - expand_binders ?loc mk bll c + CAst.make ?loc @@ CProdN (bll,c) let mkCLambdaN ?loc bll c = - let mk ?loc b c = CAst.make ?loc @@ CLambdaN ([b],c) in - expand_binders ?loc mk bll c + CAst.make ?loc @@ CLambdaN (bll,c) let coerce_reference_to_id = function | Ident (_,id) -> id diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 4f7d537d3f..ef20086e65 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -533,6 +533,10 @@ let occur_name na aty = | Name id -> occur_var_constr_expr id aty | Anonymous -> false +let is_gvar id c = match DAst.get c with +| GVar id' -> Id.equal id id' +| _ -> false + let is_projection nargs = function | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections -> (try @@ -817,13 +821,11 @@ let rec extern inctx scopes vars r = | GProd (na,bk,t,c) -> let t = extern_typ scopes vars t in - let (idl,c) = factorize_prod scopes (add_vname vars na) na bk t c in - CProdN ([(Loc.tag na)::idl,Default bk,t],c) + factorize_prod scopes (add_vname vars na) na bk t c | GLambda (na,bk,t,c) -> let t = extern_typ scopes vars t in - let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) na bk t c in - CLambdaN ([(Loc.tag na)::idl,Default bk,t],c) + factorize_lambda inctx scopes (add_vname vars na) na bk t c | GCases (sty,rtntypopt,tml,eqns) -> let vars' = @@ -919,24 +921,48 @@ and extern_typ (_,scopes) = and sub_extern inctx (_,scopes) = extern inctx (None,scopes) and factorize_prod scopes vars na bk aty c = - let c = extern_typ scopes vars c in - match na, c with - | Name id, { CAst.loc ; v = CProdN ([nal,Default bk',ty],c) } - when binding_kind_eq bk bk' && constr_expr_eq aty ty - && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> - nal,c - | _ -> - [],c + match na, DAst.get c with + | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],[(_,(_,[p],b))]) + when is_gvar id e && not (occur_glob_constr id b) -> + let b = extern_typ scopes vars b in + let p = extern_cases_pattern_in_scope scopes vars p in + let binder = CLocalPattern (c.loc,(p,None)) in + (match b.v with + | CProdN (bl,b) -> CProdN (binder::bl,b) + | _ -> CProdN ([binder],b)) + | _, _ -> + let c = extern_typ scopes vars c in + match na, c.v with + | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b) + when binding_kind_eq bk bk' && constr_expr_eq aty ty + && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> + CProdN (CLocalAssum(Loc.tag na::nal,Default bk,aty)::bl,b) + | _, CProdN (bl,b) -> + CProdN (CLocalAssum([Loc.tag na],Default bk,aty)::bl,b) + | _, _ -> + CProdN ([CLocalAssum([Loc.tag na],Default bk,aty)],c) and factorize_lambda inctx scopes vars na bk aty c = - let c = sub_extern inctx scopes vars c in - match c with - | { CAst.loc; v = CLambdaN ([nal,Default bk',ty],c) } - when binding_kind_eq bk bk' && constr_expr_eq aty ty - && not (occur_name na ty) (* avoid na in ty escapes scope *) -> - nal,c - | _ -> - [],c + match na, DAst.get c with + | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],[(_,(_,[p],b))]) + when is_gvar id e && not (occur_glob_constr id b) -> + let b = sub_extern inctx scopes vars b in + let p = extern_cases_pattern_in_scope scopes vars p in + let binder = CLocalPattern (c.loc,(p,None)) in + (match b.v with + | CLambdaN (bl,b) -> CLambdaN (binder::bl,b) + | _ -> CLambdaN ([binder],b)) + | _, _ -> + let c = sub_extern inctx scopes vars c in + match c.v with + | CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b) + when binding_kind_eq bk bk' && constr_expr_eq aty ty + && not (occur_name na ty) (* avoid na in ty escapes scope *) -> + CLambdaN (CLocalAssum(Loc.tag na::nal,Default bk,aty)::bl,b) + | CLambdaN (bl,b) -> + CLambdaN (CLocalAssum([Loc.tag na],Default bk,aty)::bl,b) + | _ -> + CLambdaN ([CLocalAssum([Loc.tag na],Default bk,aty)],c) and extern_local_binder scopes vars = function [] -> ([],[],[]) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 2761b65285..7276b917fa 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -302,15 +302,8 @@ let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_name let reset_tmp_scope env = {env with tmp_scope = None} -let rec it_mkGProd ?loc env body = - match env with - (loc2, (na, bk, t)) :: tl -> it_mkGProd ?loc:loc2 tl (DAst.make ?loc:(Loc.merge_opt loc loc2) @@ GProd (na, bk, t, body)) - | [] -> body - -let rec it_mkGLambda ?loc env body = - match env with - (loc2, (na, bk, t)) :: tl -> it_mkGLambda ?loc:loc2 tl (DAst.make ?loc:(Loc.merge_opt loc loc2) @@ GLambda (na, bk, t, body)) - | [] -> body +let mkGProd ?loc (na,bk,t) body = DAst.make ?loc @@ GProd (na, bk, t, body) +let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body) (**********************************************************************) (* Utilities for binders *) @@ -508,6 +501,20 @@ let intern_generalization intern env lvar loc bk ak c = (env', abs lid acc)) fvs (env,c) in c' +let rec expand_binders ?loc mk bl c = + match bl with + | [] -> c + | b :: bl -> + match DAst.get b with + | GLocalDef (n, bk, b, oty) -> + expand_binders ?loc mk bl (DAst.make ?loc @@ GLetIn (n, b, oty, c)) + | GLocalAssum (n, bk, t) -> + expand_binders ?loc mk bl (mk ?loc (n,bk,t) c) + | GLocalPattern ((pat,ids), id, bk, ty) -> + let tm = DAst.make ?loc (GVar id) in + let c = DAst.make ?loc @@ GCases (Misctypes.LetPatternStyle, None, [tm,(Anonymous,None)], [loc,(ids,[pat], c)]) in + expand_binders ?loc mk bl (mk ?loc (Name id,Explicit,ty) c) + (**********************************************************************) (* Syntax extensions *) @@ -1697,14 +1704,15 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = Array.map (fun (bl,_,_) -> bl) idl, Array.map (fun (_,ty,_) -> ty) idl, Array.map (fun (_,_,bd) -> bd) idl) - | CProdN ([],c2) -> - intern_type env c2 - | CProdN ((nal,bk,ty)::bll,c2) -> - iterate_prod ?loc env bk ty (CAst.make ?loc @@ CProdN (bll, c2)) nal + | CProdN (bl,c2) -> + let (env',bl) = List.fold_left intern_local_binder (env,[]) bl in + expand_binders ?loc mkGProd bl (intern_type env' c2) | CLambdaN ([],c2) -> + (* Such a term is built sometimes: it should not change scope *) intern env c2 - | CLambdaN ((nal,bk,ty)::bll,c2) -> - iterate_lam loc (reset_tmp_scope env) bk ty (CAst.make ?loc @@ CLambdaN (bll, c2)) nal + | CLambdaN (bl,c2) -> + let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope env,[]) bl in + expand_binders ?loc mkGLambda bl (intern env' c2) | CLetIn (na,c1,t,c2) -> let inc1 = intern (reset_tmp_scope env) c1 in let int = Option.map (intern_type env) t in @@ -1979,14 +1987,6 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = [], None in (tm',(snd na,typ)), extra_id, match_td - and iterate_prod ?loc env bk ty body nal = - let env, bl = intern_assumption intern ntnvars env nal bk ty in - it_mkGProd ?loc bl (intern_type env body) - - and iterate_lam loc env bk ty body nal = - let env, bl = intern_assumption intern ntnvars env nal bk ty in - it_mkGLambda ?loc bl (intern env body) - and intern_impargs c env l subscopes args = let eargs, rargs = extract_explicit_arg l args in if !parsing_explicit then -- cgit v1.2.3 From 9324dcf528f16be420b08c376a6580c8987f50fd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Aug 2017 17:10:48 +0200 Subject: Using name given by user to name a 'pat, if any. This works for contexts in Definition and co, but not yet for "fun" and co. --- interp/constrintern.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7276b917fa..4658b6a33a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -461,7 +461,9 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio | _ -> assert false in let env = {env with ids = List.fold_right Id.Set.add il env.ids} in - let id = Namegen.next_ident_away (Id.of_string "pat") env.ids in + let na = alias_of_pat cp in + let ienv = Name.fold_right Id.Set.remove na env.ids in + let id = Namegen.next_name_away_with_default "pat" (alias_of_pat cp) ienv in let na = (loc, Name id) in let bk = Default Explicit in let _, bl' = intern_assumption intern lvar env [na] bk tyc in -- cgit v1.2.3 From 7ef99814a02a0eb7c37dd28fb9ce603e70501745 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 11 Aug 2017 06:06:54 +0200 Subject: Minor clarifying of name variables in constrintern.ml. - renaming lvar into ntnvars when relevant, for consistency - renaming sometimes genv into env (intern_env) so as to remain consistent with other parts of the code --- interp/constrintern.ml | 44 ++++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4658b6a33a..cab95d57cd 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -376,7 +376,7 @@ let push_name_env ?(global_level=false) ntnvars implargs env = else Dumpglob.dump_binding ?loc id; {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} -let intern_generalized_binder ?(global_level=false) intern_type lvar +let intern_generalized_binder ?(global_level=false) intern_type ntnvars env (loc, na) b b' t ty = let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in let ty, ids' = @@ -387,7 +387,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar let ty' = intern_type {env with ids = ids; unb = true} ty in let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in let env' = List.fold_left - (fun env (l, x) -> push_name_env ~global_level lvar (Variable,[],[],[])(*?*) env (l, Name x)) + (fun env (l, x) -> push_name_env ~global_level ntnvars (Variable,[],[],[])(*?*) env (l, Name x)) env fvs in let bl = List.map (fun (loc, id) -> @@ -406,9 +406,9 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name | _ -> na - in (push_name_env ~global_level lvar (impls_type_list ty')(*?*) env' (loc,na)), (loc,(na,b',ty')) :: List.rev bl + in (push_name_env ~global_level ntnvars (impls_type_list ty')(*?*) env' (loc,na)), (loc,(na,b',ty')) :: List.rev bl -let intern_assumption intern lvar env nal bk ty = +let intern_assumption intern ntnvars env nal bk ty = let intern_type env = intern (set_type_scope env) in match bk with | Default k -> @@ -417,11 +417,11 @@ let intern_assumption intern lvar env nal bk ty = let impls = impls_type_list ty in List.fold_left (fun (env, bl) (loc, na as locna) -> - (push_name_env lvar impls env locna, + (push_name_env ntnvars impls env locna, (Loc.tag ?loc (na,k,locate_if_hole ?loc na ty))::bl)) (env, []) nal | Generalized (b,b',t) -> - let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in + let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b b' t ty in env, b let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function @@ -436,15 +436,15 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd") -let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function +let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = function | CLocalAssum(nal,bk,ty) -> - let env, bl' = intern_assumption intern lvar env nal bk ty in + let env, bl' = intern_assumption intern ntnvars env nal bk ty in let bl' = List.map (fun (loc,(na,c,t)) -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in env, bl' @ bl | CLocalDef((loc,na as locna),def,ty) -> let term = intern env def in let ty = Option.map (intern env) ty in - (push_name_env lvar (impls_term_list term) env locna, + (push_name_env ntnvars (impls_term_list term) env locna, (DAst.make ?loc @@ GLocalDef (na,Explicit,term,ty)) :: bl) | CLocalPattern (loc,(p,ty)) -> let tyc = @@ -466,11 +466,11 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio let id = Namegen.next_name_away_with_default "pat" (alias_of_pat cp) ienv in let na = (loc, Name id) in let bk = Default Explicit in - let _, bl' = intern_assumption intern lvar env [na] bk tyc in + let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in let _,(_,bk,t) = List.hd bl' in (env, (DAst.make ?loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl) -let intern_generalization intern env lvar loc bk ak c = +let intern_generalization intern env ntnvars loc bk ak c = let c = intern {env with unb = true} c in let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:env.ids c in let env', c' = @@ -499,7 +499,7 @@ let intern_generalization intern env lvar loc bk ak c = GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) in List.fold_right (fun (loc, id as lid) (env, acc) -> - let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in + let env' = push_name_env ntnvars (Variable,[],[],[]) env (loc, Name id) in (env', abs lid acc)) fvs (env,c) in c' @@ -729,7 +729,7 @@ let make_subst ids l = let fold accu (id, scl) a = Id.Map.add id (a, scl) accu in List.fold_left2 fold Id.Map.empty ids l -let intern_notation intern env lvar loc ntn fullargs = +let intern_notation intern env ntnvars loc ntn fullargs = let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in let ((ids,c),df) = interp_notation ?loc ntn (env.tmp_scope,env.scopes) in Dumpglob.dump_notation_location (ntn_loc ?loc fullargs ntn) ntn df; @@ -737,7 +737,7 @@ let intern_notation intern env lvar loc ntn fullargs = let terms = make_subst ids args in let termlists = make_subst idsl argslist in let binders = make_subst idsbl bll in - instantiate_notation_constr loc intern lvar + instantiate_notation_constr loc intern ntnvars (terms, termlists, binders) (Id.Map.empty, env) c (**********************************************************************) @@ -755,17 +755,17 @@ let gvar (loc, id) us = match us with user_err ?loc (str "Variable " ++ Id.print id ++ str " cannot have a universe instance") -let intern_var genv (ltacvars,ntnvars) namedctx loc id us = +let intern_var env (ltacvars,ntnvars) namedctx loc id us = (* Is [id] a notation variable *) if Id.Map.mem id ntnvars then begin - if not (Id.Map.mem id genv.impls) then set_var_scope ?loc id true genv ntnvars; + if not (Id.Map.mem id env.impls) then set_var_scope ?loc id true env ntnvars; gvar (loc,id) us, [], [], [] end else (* Is [id] registered with implicit arguments *) try - let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in + let ty,expl_impls,impls,argsc = Id.Map.find id env.impls in let expl_impls = List.map (fun id -> CAst.make ?loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in let tys = string_of_ty ty in @@ -773,7 +773,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us = gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls with Not_found -> (* Is [id] bound in current term or is an ltac var bound to constr *) - if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars + if Id.Set.mem id env.ids || Id.Set.mem id ltacvars.ltac_vars then gvar (loc,id) us, [], [], [] else if Id.equal id ldots_var @@ -858,7 +858,7 @@ let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort = | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info] (* Is it a global reference or a syntactic definition? *) -let intern_qualid loc qid intern env lvar us args = +let intern_qualid loc qid intern env ntnvars us args = match intern_extended_global_of_qualid (loc,qid) with | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args | SynDef sp -> @@ -871,7 +871,7 @@ let intern_qualid loc qid intern env lvar us args = let subst = (terms, Id.Map.empty, Id.Map.empty) in let infos = (Id.Map.empty, env) in let projapp = match c with NRef _ -> true | _ -> false in - let c = instantiate_notation_constr loc intern lvar subst infos c in + let c = instantiate_notation_constr loc intern ntnvars subst infos c in let loc = c.CAst.loc in let err () = user_err ?loc (str "Notation " ++ pr_qualid qid @@ -897,8 +897,8 @@ let intern_qualid loc qid intern env lvar us args = c, projapp, args2 (* Rule out section vars since these should have been found by intern_var *) -let intern_non_secvar_qualid loc qid intern env lvar us args = - let c, _, _ as r = intern_qualid loc qid intern env lvar us args in +let intern_non_secvar_qualid loc qid intern env ntnvars us args = + let c, _, _ as r = intern_qualid loc qid intern env ntnvars us args in match DAst.get c with | GRef (VarRef _, _) -> raise Not_found | _ -> r -- cgit v1.2.3 From 6901f720c6115c8eec1343846641a5c8453c3268 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 17:18:36 +0200 Subject: Notations: documenting structure collecting variables occurring in notation. --- interp/notation_ops.ml | 29 ++++++++++++++++++----------- 1 file changed, 18 insertions(+), 11 deletions(-) (limited to 'interp') diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 472b9de599..301ec69847 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -201,7 +201,13 @@ let glob_constr_of_notation_constr ?loc x = (******************************************************************************) (* Translating a glob_constr into a notation, interpreting recursive patterns *) -let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r) +type found_variables = { + vars : Id.t list; + recursive_term_vars : (Id.t * Id.t) list; + recursive_binders_vars : (Id.t * Id.t) list; + } + +let add_id r id = r := { !r with vars = id :: (!r).vars } let add_name r = function Anonymous -> () | Name id -> add_id r id let is_gvar id c = match DAst.get c with @@ -301,12 +307,12 @@ let compare_recursive_parts found f f' (iterator,subc) = (str "Both ends of the recursive pattern are the same.") | Some (x,y,RecursiveTerms lassoc) -> let toadd,x,y,lassoc = - if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) || - List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found) + if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_term_vars || + List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_binders_vars then None,x,y,lassoc - else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) || - List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi3 !found) + else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_term_vars || + List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_binders_vars then None,y,x,not lassoc else @@ -315,14 +321,14 @@ let compare_recursive_parts found f f' (iterator,subc) = f' (if lassoc then iterator else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in (* found variables have been collected by compare_constr *) - found := (List.remove Id.equal y (pi1 !found), - Option.fold_right (fun a l -> a::l) toadd (pi2 !found), - pi3 !found); + found := { !found with vars = List.remove Id.equal y (!found).vars; + recursive_term_vars = Option.fold_right (fun a l -> a::l) toadd (!found).recursive_term_vars }; NList (x,y,iterator,f (Option.get !terminator),lassoc) | Some (x,y,RecursiveBinders (t_x,t_y)) -> let iterator = f' (subst_glob_vars [x, DAst.make @@ GVar y] iterator) in (* found have been collected by compare_constr *) - found := (List.remove Id.equal y (pi1 !found), pi2 !found, (x,y) :: pi3 !found); + found := { !found with vars = List.remove Id.equal y (!found).vars; + recursive_binders_vars = (x,y) :: (!found).recursive_binders_vars }; check_is_hole x t_x; check_is_hole y t_y; NBinderList (x,y,iterator,f (Option.get !terminator)) @@ -330,7 +336,7 @@ let compare_recursive_parts found f f' (iterator,subc) = raise Not_found let notation_constr_and_vars_of_glob_constr a = - let found = ref ([],[],[]) in + let found = ref { vars = []; recursive_term_vars = []; recursive_binders_vars = [] } in let has_ltac = ref false in let rec aux c = let keepfound = !found in @@ -395,7 +401,8 @@ let notation_constr_and_vars_of_glob_constr a = (* Side effect *) t, !found, !has_ltac -let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = +let check_variables_and_reversibility nenv + { vars = found; recursive_term_vars = foundrec; recursive_binders_vars = foundrecbinding } = let injective = ref [] in let recvars = nenv.ninterp_rec_vars in let fold _ y accu = Id.Set.add y accu in -- cgit v1.2.3 From 51976c9f2157953f794ed1efcd68403a8545d346 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 9 Aug 2017 13:58:59 +0200 Subject: A bit of miscellaneous code documentation around notations. --- interp/notation.mli | 8 ++++---- interp/notation_ops.ml | 1 + 2 files changed, 5 insertions(+), 4 deletions(-) (limited to 'interp') diff --git a/interp/notation.mli b/interp/notation.mli index 7d055571c8..d100122129 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -176,10 +176,10 @@ val scope_class_of_class : Classops.cl_typ -> scope_class (** Building notation key *) type symbol = - | Terminal of string - | NonTerminal of Id.t - | SProdList of Id.t * symbol list - | Break of int + | Terminal of string (* an expression including symbols or a simply-quoted ident, e.g. "'U'" or "!" *) + | NonTerminal of Id.t (* an identifier "x" *) + | SProdList of Id.t * symbol list (* an expression "x sep .. sep y", remembering x (or y) and sep *) + | Break of int (* a sequence of blanks > 1, e.g. " " *) val symbol_eq : symbol -> symbol -> bool diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 301ec69847..c414ba67a9 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -338,6 +338,7 @@ let compare_recursive_parts found f f' (iterator,subc) = let notation_constr_and_vars_of_glob_constr a = let found = ref { vars = []; recursive_term_vars = []; recursive_binders_vars = [] } in let has_ltac = ref false in + (* Turn a glob_constr into a notation_constr by first trying to find a recursive pattern *) let rec aux c = let keepfound = !found in (* n^2 complexity but small and done only once per notation *) -- cgit v1.2.3 From 7c10b4020e061fb14e01cb3abc92bb5265aa65b9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Aug 2017 18:17:32 +0200 Subject: Fixing/improving notations with recursive patterns. - The "terminator" of a recursive notation is now interpreted in the environment in which it occurs rather than the environment at the beginning of the recursive patterns. Note that due to a tolerance in checking unbound variables of notations, a variable unbound in the environment was still working ok as long as no user-given variable was shadowing a private variable of the notation - see the "exists_mixed" example in test-suite. Conversely, in a notation such as: Notation "!! x .. y # A #" := ((forall x, True), .. ((forall y, True), A) ..) (at level 200, x binder). Check !! a b # a=b #. The unbound "a" was detected only at pretyping and not as expected at internalizing time, due to "a=b" interpreted in context containing a and b. - Similarly, each binder is now interpreted in the environment in which it occurs rather than as if the sequence of binders was dependent from the left to the right (such a dependency was ok for "forall" or "exists" but not in general). For instance, in: Notation "!! x .. y # A #" := ((forall x, True), .. ((forall y, True), A) ..) (at level 200, x binder). Check !! (a:nat) (b:a=a) # True #. The illegal dependency of the type of b in a was detected only at pretyping time. - If a let-in occurs in the sequence of binders of a notation with a recursive pattern, it is now inserted in between the occurrences of the iterator rather than glued with the forall/fun of the iterator. For instance, in: Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder). Check exists_true '(x,y) (u:=0), x=y. We now get exists '(x, y), True /\ (let u := 0 in True /\ x = y) while we had before the let-in breaking the repeated pattern: exists '(x, y), (let u := 0 in True /\ x = y) This is more compositional, and, in particular, the printer algorithm now recognizes the pattern which is otherwise broken. --- interp/constrintern.ml | 112 +++++++++++++++++++++++-------------------------- 1 file changed, 53 insertions(+), 59 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index cab95d57cd..3c8643ee36 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -436,16 +436,20 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd") +let intern_letin_binder intern ntnvars env ((loc,na as locna),def,ty) = + let term = intern env def in + let ty = Option.map (intern env) ty in + (push_name_env ntnvars (impls_term_list term) env locna, + (na,Explicit,term,ty)) + let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = function | CLocalAssum(nal,bk,ty) -> let env, bl' = intern_assumption intern ntnvars env nal bk ty in let bl' = List.map (fun (loc,(na,c,t)) -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in env, bl' @ bl | CLocalDef((loc,na as locna),def,ty) -> - let term = intern env def in - let ty = Option.map (intern env) ty in - (push_name_env ntnvars (impls_term_list term) env locna, - (DAst.make ?loc @@ GLocalDef (na,Explicit,term,ty)) :: bl) + 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,(p,ty)) -> let tyc = match ty with @@ -554,39 +558,11 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function in (renaming',env), Name id' -type letin_param_r = - | LPLetIn of Name.t * glob_constr * glob_constr option - | LPCases of (cases_pattern * Id.t list) * Id.t -(* Unused thus fatal warning *) -(* and letin_param = letin_param_r Loc.located *) - -let make_letins = - List.fold_right - (fun a c -> - match a with - | loc, LPLetIn (na,b,t) -> - DAst.make ?loc @@ GLetIn(na,b,t,c) - | loc, LPCases ((cp,il),id) -> - let tt = (DAst.make ?loc @@ GVar id, (Name id,None)) in - DAst.make ?loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))])) - -let rec subordinate_letins letins l = match l with - | bnd :: l -> - let loc = bnd.CAst.loc in - begin match DAst.get bnd with - (* binders come in reverse order; the non-let are returned in reverse order together *) - (* with the subordinated let-in in writing order *) - | GLocalDef (na,_,b,t) -> - subordinate_letins ((Loc.tag ?loc @@ LPLetIn (na,b,t))::letins) l - | GLocalAssum (na,bk,t) -> - let letins',rest = subordinate_letins [] l in - letins',((loc,(na,bk,t)),letins)::rest - | GLocalPattern (u,id,bk,t) -> - subordinate_letins ((Loc.tag ?loc @@ LPCases (u,id))::letins) - ([DAst.make ?loc @@ GLocalAssum (Name id,bk,t)] @ l) - end - | [] -> - letins,[] +type binder_action = +| AddLetIn of Name.t Loc.located * constr_expr * constr_expr option +| AddTermIter of (constr_expr * subscopes) Names.Id.Map.t +| AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *) +| AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *) let dmap_with_loc f n = CAst.map_with_loc (fun ?loc c -> f ?loc (DAst.get_thunk c)) n @@ -613,15 +589,40 @@ let terms_of_binders bl = | [] -> [] in extract_variables bl +let flatten_generalized_binders_if_any y l = + match List.rev l with + | [] -> assert false + | a::l -> a, List.map (fun a -> AddBinderIter (y,a)) l (* if l not empty, this means we had a generalized binder *) + +let flatten_binders bl = + let dispatch = function + | CLocalAssum (nal,bk,t) -> List.map (fun na -> CLocalAssum ([na],bk,t)) nal + | a -> [a] in + List.flatten (List.map dispatch bl) + let instantiate_notation_constr loc intern ntnvars subst infos c = let (terms,termlists,binders) = subst in (* when called while defining a notation, avoid capturing the private binders of the expression by variables bound by the notation (see #3892) *) let avoid = Id.Map.domain ntnvars in - let rec aux (terms,binderopt,terminopt as subst') (renaming,env) c = + let rec aux (terms,binderopt,iteropt as subst') (renaming,env) c = let subinfos = renaming,{env with tmp_scope = None} in match c with - | NVar id when Id.equal id ldots_var -> Option.get terminopt + | NVar id when Id.equal id ldots_var -> + let rec aux_letin env = function + | [],terminator,_ -> aux (terms,None,None) (renaming,env) terminator + | AddPreBinderIter (y,binder)::rest,terminator,iter -> + let env,binders = intern_local_binder_aux intern ntnvars (env,[]) binder in + let binder,extra = flatten_generalized_binders_if_any y binders in + aux (terms,Some (y,binder),Some (extra@rest,terminator,iter)) (renaming,env) iter + | AddBinderIter (y,binder)::rest,terminator,iter -> + aux (terms,Some (y,binder),Some (rest,terminator,iter)) (renaming,env) iter + | AddTermIter nterms::rest,terminator,iter -> + aux (nterms,None,Some (rest,terminator,iter)) (renaming,env) iter + | AddLetIn (na,c,t)::rest,terminator,iter -> + let env,(na,_,c,t) = intern_letin_binder intern ntnvars env (na,c,t) in + DAst.make ?loc (GLetIn (na,c,t,aux_letin env (rest,terminator,iter))) in + aux_letin env (Option.get iteropt) | NVar id -> subst_var subst' (renaming, env) id | NList (x,y,iter,terminator,lassoc) -> let l,(scopt,subscopes) = @@ -636,12 +637,8 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = terms_of_binders (if lassoc then bl' else List.rev bl'),(None,[]) with Not_found -> anomaly (Pp.str "Inconsistent substitution of recursive notation.") in - let termin = aux (terms,None,None) subinfos terminator in - let fold a t = - let nterms = Id.Map.add y (a, (scopt, subscopes)) terms in - aux (nterms,None,Some t) subinfos iter - in - List.fold_right fold l termin + let l = List.map (fun a -> AddTermIter ((Id.Map.add y (a,(scopt,subscopes)) terms))) l in + aux (terms,None,Some (l,terminator,iter)) subinfos (NVar ldots_var) | NHole (knd, naming, arg) -> let knd = match knd with | Evar_kinds.BinderType (Name id as na) -> @@ -670,24 +667,21 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = (try (* All elements of the list are in scopes (scopt,subscopes) *) let (bl,(scopt,subscopes)) = Id.Map.find x binders in - let env,bl = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in - let letins,bl = subordinate_letins [] bl in - let termin = aux (terms,None,None) (renaming,env) terminator in - let res = List.fold_left (fun t binder -> - aux (terms,Some(y,binder),Some t) subinfos iter) - termin bl in - make_letins letins res + (* We flatten binders so that we can interpret them at substitution time *) + let bl = flatten_binders bl in + (* We isolate let-ins which do not contribute to the repeated pattern *) + let l = List.map (function | CLocalDef (na,c,t) -> AddLetIn (na,c,t) + | binder -> AddPreBinderIter (y,binder)) bl in + (* We stack the binders to iterate or let-ins to insert *) + 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 -> - let a,letins = snd (Option.get binderopt) in - let e = make_letins letins (aux subst' infos c') in - let (_loc,(na,bk,t)) = a in - DAst.make ?loc @@ GProd (na,bk,t,e) + 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 -> - let a,letins = snd (Option.get binderopt) in - let (_loc,(na,bk,t)) = a in - DAst.make ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c')) + 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' -> -- cgit v1.2.3 From d4c2ed95fcfd64cdcc10e51e40be739d9f1c4a74 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Aug 2017 20:05:03 +0200 Subject: Allows recursive patterns for binders to be associative on the left. This makes treatment of recursive binders closer to the one of recursive terms. It is unclear whether there are interesting notations liable to use this, but this shall make easier mixing recursive binders and recursive terms as in next commits. Example of (artificial) notation that this commit supports: Notation "! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder). --- interp/constrintern.ml | 3 ++- interp/notation.ml | 2 +- interp/notation_ops.ml | 69 ++++++++++++++++++++++++++------------------------ interp/reserve.ml | 2 +- 4 files changed, 40 insertions(+), 36 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3c8643ee36..bedf932b03 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -663,12 +663,13 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = Some (Genintern.generic_substitute_notation bindings arg) in DAst.make ?loc @@ GHole (knd, naming, arg) - | NBinderList (x,y,iter,terminator) -> + | NBinderList (x,y,iter,terminator,lassoc) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) let (bl,(scopt,subscopes)) = Id.Map.find x binders in (* We flatten binders so that we can interpret them at substitution time *) let bl = flatten_binders bl in + let bl = if lassoc then List.rev bl else bl in (* We isolate let-ins which do not contribute to the repeated pattern *) let l = List.map (function | CLocalDef (na,c,t) -> AddLetIn (na,c,t) | binder -> AddPreBinderIter (y,binder)) bl in diff --git a/interp/notation.ml b/interp/notation.ml index 94ce2a6c8d..31f16e1a90 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -292,7 +292,7 @@ let cases_pattern_key c = match DAst.get c with let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) | NList (_,_,NApp (NRef ref,args),_,_) - | NBinderList (_,_,NApp (NRef ref,args),_) -> + | NBinderList (_,_,NApp (NRef ref,args),_,_) -> RefKey (canonical_gr ref), Some (List.length args) | NRef ref -> RefKey(canonical_gr ref), None | NApp (_,args) -> Oth, Some (List.length args) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index c414ba67a9..73b5100ca6 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -42,9 +42,9 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with 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), NBinderList (i2, j2, t2, 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 + (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 @@ -146,11 +146,11 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let inner = lt @@ GApp (lt @@ GVar (ldots_var),[subst_glob_vars innerl it]) in let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in DAst.get (subst_glob_vars outerl it) - | NBinderList (x,y,iter,tail) -> + | NBinderList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in - let innerl = [(ldots_var,t);(x, lt @@ GVar y)] in + let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in let inner = lt @@ GApp (lt @@ GVar ldots_var,[subst_glob_vars innerl it]) in - let outerl = [(ldots_var,inner)] in + let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in DAst.get (subst_glob_vars outerl it) | NLambda (na,ty,c) -> let e',na = g e na in GLambda (na,Explicit,f e ty,f e' c) @@ -255,7 +255,7 @@ let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' type recursive_pattern_kind = | RecursiveTerms of bool (* associativity *) -| RecursiveBinders of glob_constr * glob_constr +| RecursiveBinders of bool (* associativity *) * glob_constr * glob_constr let compare_recursive_parts found f f' (iterator,subc) = let diff = ref None in @@ -289,9 +289,11 @@ let compare_recursive_parts found f f' (iterator,subc) = | GLambda (Name x,_,t_x,c), GLambda (Name y,_,t_y,term) | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) when not (Id.equal x y) -> (* We found a binding position where it differs *) + let lassoc = match !terminator with None -> false | Some _ -> true in + let x,t_x,y,t_y = if lassoc then y,t_y,x,t_x else x,t_x,y,t_y in begin match !diff with | None -> - let () = diff := Some (x, y, RecursiveBinders (t_x,t_y)) in + let () = diff := Some (x, y, RecursiveBinders (lassoc,t_x,t_y)) in aux c term | Some _ -> false end @@ -323,15 +325,15 @@ let compare_recursive_parts found f f' (iterator,subc) = (* found variables have been collected by compare_constr *) found := { !found with vars = List.remove Id.equal y (!found).vars; recursive_term_vars = Option.fold_right (fun a l -> a::l) toadd (!found).recursive_term_vars }; - NList (x,y,iterator,f (Option.get !terminator),lassoc) - | Some (x,y,RecursiveBinders (t_x,t_y)) -> - let iterator = f' (subst_glob_vars [x, DAst.make @@ GVar y] iterator) in - (* found have been collected by compare_constr *) + NList (x,y,iterator,f (Option.get !terminator),lassoc) + | Some (x,y,RecursiveBinders (lassoc,t_x,t_y)) -> + let iterator = f' (if lassoc then iterator else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in + (* found have been collected by compare_constr *) found := { !found with vars = List.remove Id.equal y (!found).vars; recursive_binders_vars = (x,y) :: (!found).recursive_binders_vars }; - check_is_hole x t_x; - check_is_hole y t_y; - NBinderList (x,y,iterator,f (Option.get !terminator)) + check_is_hole x t_x; + check_is_hole y t_y; + NBinderList (x,y,iterator,f (Option.get !terminator),lassoc) else raise Not_found @@ -512,11 +514,11 @@ let rec subst_notation_constr subst bound raw = if r1' == r1 && r2' == r2 then raw else NProd (n,r1',r2') - | NBinderList (id1,id2,r1,r2) -> + | NBinderList (id1,id2,r1,r2,b) -> let r1' = subst_notation_constr subst bound r1 and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else - NBinderList (id1,id2,r1',r2') + NBinderList (id1,id2,r1',r2',b) | NLetIn (n,r1,t,r2) -> let r1' = subst_notation_constr subst bound r1 in @@ -929,28 +931,28 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 = let glue_letin_with_decls = true -let rec match_iterated_binders islambda decls bi = DAst.(with_loc_val (fun ?loc -> function +let rec match_iterated_binders islambda decls bi lassoc = DAst.(with_loc_val (fun ?loc -> function | GLambda (na,bk,t,b) as b0 -> begin match na, DAst.get b with | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))]) when islambda && is_gvar p e && not (occur_glob_constr p b) -> - match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b + match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b lassoc | _, _ when islambda -> - match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b + match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b lassoc | _ -> (decls, DAst.make ?loc b0) end | GProd (na,bk,t,b) as b0 -> begin match na, DAst.get b with | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))]) when not islambda && is_gvar p e && not (occur_glob_constr p b) -> - match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b + match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b lassoc | Name _, _ when not islambda -> - match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b + match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b lassoc | _ -> (decls, DAst.make ?loc b0) end | GLetIn (na,c,t,b) when glue_letin_with_decls -> match_iterated_binders islambda - ((DAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b + ((DAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b lassoc | b -> (decls, DAst.make ?loc b) )) bi @@ -964,7 +966,7 @@ let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas -let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin = +let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin lassoc = let rec aux sigma bl rest = try let metas = add_ldots_var (add_meta_bindinglist y metas) in @@ -978,6 +980,7 @@ let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin = with No_match when not (List.is_empty bl) -> bl, rest, sigma in let bl,rest,sigma = aux sigma [] rest in + let bl = if lassoc then List.rev bl else bl in let alp,sigma = bind_bindinglist_env alp sigma x bl in match_fun alp metas sigma rest termin @@ -1041,46 +1044,46 @@ let rec match_ inner u alp metas sigma a1 a2 = | r1, NList (x,y,iter,termin,lassoc) -> match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin lassoc - | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin) -> + | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin,lassoc) -> begin match na1, DAst.get b1, iter with (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *) | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _) when is_gvar p e && not (occur_glob_constr p b1) -> - let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in + let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 lassoc in let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin (* Matching recursive notations for binders: ad hoc cases supporting let-in *) | _, _, NLambda (Name _,_,_) -> - let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in + let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 lassoc in (* TODO: address the possibility that termin is a Lambda itself *) let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin (* Matching recursive notations for binders: general case *) | _, _, _ -> - match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin + match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin lassoc end - | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin) -> + | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin,lassoc) -> (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *) begin match na1, DAst.get b1, iter, termin with | Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _ when is_gvar p e && not (occur_glob_constr p b1) -> - let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in + let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 lassoc in let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin | _, _, NProd (Name _,_,_), _ when na1 != Anonymous -> - let (decls,b) = match_iterated_binders false [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in + let (decls,b) = match_iterated_binders false [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 lassoc in (* TODO: address the possibility that termin is a Prod itself *) let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin (* Matching recursive notations for binders: general case *) | _, _, _, _ -> - match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin + match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin lassoc end (* Matching recursive notations for binders: general case *) - | _r, NBinderList (x,y,iter,termin) -> - match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin + | _r, NBinderList (x,y,iter,termin,lassoc) -> + match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin lassoc (* Matching individual binders as part of a recursive pattern *) | GLambda (na1, bk, t1, b1), NLambda (na2, t2, b2) -> diff --git a/interp/reserve.ml b/interp/reserve.ml index 22c5a2f5e5..04710282f5 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -71,7 +71,7 @@ let reserve_revtable = Summary.ref KeyMap.empty ~name:"reserved-type-rev" let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) | NList (_,_,NApp (NRef ref,args),_,_) - | NBinderList (_,_,NApp (NRef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args) + | NBinderList (_,_,NApp (NRef ref,args),_,_) -> RefKey (canonical_gr ref), Some (List.length args) | NRef ref -> RefKey(canonical_gr ref), None | _ -> Oth, None -- cgit v1.2.3 From a18e87f6a929ce296f8c277b310e286151e06293 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 14 Aug 2017 01:27:04 +0200 Subject: Allowing variables used in recursive notation to occur several times in pattern. This allows for instance to support recursive notations of the form: Notation "! x .. y # A #" := (((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..) (at level 200, x binder). --- interp/constrintern.ml | 10 +++++++++- interp/notation_ops.ml | 25 ++++++++++++++++++++++--- 2 files changed, 31 insertions(+), 4 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index bedf932b03..7411c7e357 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -697,7 +697,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = | t -> glob_constr_of_notation_constr_with_binders ?loc (traverse_binder subst avoid) (aux subst') subinfos t - and subst_var (terms, _binderopt, _terminopt) (renaming, env) id = + and subst_var (terms, binderopt, _terminopt) (renaming, env) id = (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) try @@ -705,6 +705,14 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = intern {env with tmp_scope = scopt; scopes = subscopes @ env.scopes} a with Not_found -> + try + match binderopt with + | Some (x,binder) when Id.equal x id -> + let terms = terms_of_binders [binder] in + assert (List.length terms = 1); + intern env (List.hd terms) + | _ -> raise Not_found + with Not_found -> DAst.make ?loc ( try GVar (Id.Map.find id renaming) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 73b5100ca6..ac65f6875f 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -284,7 +284,9 @@ let compare_recursive_parts found f f' (iterator,subc) = | None -> let () = diff := Some (x, y, RecursiveTerms lassoc) in true - | Some _ -> false + | Some (x', y', RecursiveTerms lassoc') + | Some (x', y', RecursiveBinders (lassoc',_,_)) -> + Id.equal x x' && Id.equal y y' && lassoc = lassoc' end | GLambda (Name x,_,t_x,c), GLambda (Name y,_,t_y,term) | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) when not (Id.equal x y) -> @@ -295,7 +297,11 @@ let compare_recursive_parts found f f' (iterator,subc) = | None -> let () = diff := Some (x, y, RecursiveBinders (lassoc,t_x,t_y)) in aux c term - | Some _ -> false + | Some (x', y', RecursiveBinders (lassoc',_,_)) -> + Id.equal x x' && Id.equal y y' && lassoc = lassoc' + | Some (x', y', RecursiveTerms lassoc') -> + let () = diff := Some (x, y, RecursiveBinders (lassoc,t_x,t_y)) in + Id.equal x x' && Id.equal y y' && lassoc = lassoc' end | _ -> mk_glob_constr_eq aux c1 c2 in @@ -327,10 +333,21 @@ let compare_recursive_parts found f f' (iterator,subc) = recursive_term_vars = Option.fold_right (fun a l -> a::l) toadd (!found).recursive_term_vars }; NList (x,y,iterator,f (Option.get !terminator),lassoc) | Some (x,y,RecursiveBinders (lassoc,t_x,t_y)) -> + let toadd,x,y,lassoc = + if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_term_vars || + List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_binders_vars + then + None,x,y,lassoc + else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_term_vars || + List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_binders_vars + then + None,y,x,not lassoc + else + Some (x,y),x,y,lassoc in let iterator = f' (if lassoc then iterator else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in (* found have been collected by compare_constr *) found := { !found with vars = List.remove Id.equal y (!found).vars; - recursive_binders_vars = (x,y) :: (!found).recursive_binders_vars }; + recursive_binders_vars = Option.fold_right (fun a l -> a::l) toadd (!found).recursive_binders_vars }; check_is_hole x t_x; check_is_hole y t_y; NBinderList (x,y,iterator,f (Option.get !terminator),lassoc) @@ -976,6 +993,8 @@ let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin las 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 *) + let sigma = remove_sigma y sigma in aux sigma (b::bl) rest with No_match when not (List.is_empty bl) -> bl, rest, sigma in -- cgit v1.2.3 From 96d6ef7036e19bf1def1512abae5ef8c6ace06b0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 14 Aug 2017 13:29:39 +0200 Subject: Supporting recursive notations reversing the left-to-right order. Seizing this opportunity to generalize the possibility for different associativity into simply reversing the order or not. Also dropping some dead code. Example of recursive notation now working: Notation "[ a , .. , b |- A ]" := (cons b .. (cons a nil) .., A). --- interp/constrintern.ml | 14 ++-- interp/notation_ops.ml | 172 ++++++++++++++++++++++++------------------------- 2 files changed, 93 insertions(+), 93 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7411c7e357..52b51ece5f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -624,17 +624,17 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = DAst.make ?loc (GLetIn (na,c,t,aux_letin env (rest,terminator,iter))) in aux_letin env (Option.get iteropt) | NVar id -> subst_var subst' (renaming, env) id - | NList (x,y,iter,terminator,lassoc) -> + | NList (x,y,iter,terminator,revert) -> let l,(scopt,subscopes) = (* All elements of the list are in scopes (scopt,subscopes) *) try let l,scopes = Id.Map.find x termlists in - (if lassoc then List.rev l else l),scopes + (if revert then List.rev l else l),scopes with Not_found -> try let (bl,(scopt,subscopes)) = Id.Map.find x binders in let env,bl' = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in - terms_of_binders (if lassoc then bl' else List.rev bl'),(None,[]) + terms_of_binders (if revert then bl' else List.rev bl'),(None,[]) with Not_found -> anomaly (Pp.str "Inconsistent substitution of recursive notation.") in let l = List.map (fun a -> AddTermIter ((Id.Map.add y (a,(scopt,subscopes)) terms))) l in @@ -663,13 +663,13 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = Some (Genintern.generic_substitute_notation bindings arg) in DAst.make ?loc @@ GHole (knd, naming, arg) - | NBinderList (x,y,iter,terminator,lassoc) -> + | NBinderList (x,y,iter,terminator,revert) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) let (bl,(scopt,subscopes)) = Id.Map.find x binders in (* We flatten binders so that we can interpret them at substitution time *) let bl = flatten_binders bl in - let bl = if lassoc then List.rev bl else bl in + let bl = if revert then List.rev bl else bl in (* We isolate let-ins which do not contribute to the repeated pattern *) let l = List.map (function | CLocalDef (na,c,t) -> AddLetIn (na,c,t) | binder -> AddPreBinderIter (y,binder)) bl in @@ -1471,7 +1471,7 @@ let drop_notations_pattern looked_for genv = let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in let pl = add_local_defs_and_check_length loc genv g pl args in DAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, []) - | NList (x,y,iter,terminator,lassoc) -> + | NList (x,y,iter,terminator,revert) -> if not (List.is_empty args) then user_err ?loc (strbrk "Application of arguments to a recursive notation not supported in patterns."); (try @@ -1482,7 +1482,7 @@ let drop_notations_pattern looked_for genv = let nsubst = Id.Map.add y (a, (scopt, subscopes)) subst in let u = in_not false loc scopes (nsubst, substlist) [] iter in subst_pat_iterator ldots_var t u) - (if lassoc then List.rev l else l) termin + (if revert then List.rev l else l) termin with Not_found -> anomaly (Pp.str "Inconsistent substitution of recursive notation.")) | NHole _ -> diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ac65f6875f..602271bf62 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -251,13 +251,25 @@ let check_is_hole id t = match DAst.get t with GHole _ -> () | _ -> (strbrk "In recursive notation with binders, " ++ Id.print id ++ strbrk " is expected to come without type.") +let check_pair_matching ?loc x y x' y' revert revert' = + if not (Id.equal x x' && Id.equal y y' && revert = revert') then + let x,y = if revert then y,x else x,y in + let x',y' = if revert' then y',x' else x',y' in + (* This is a case where one would like to highlight two locations! *) + user_err ?loc + (strbrk "Found " ++ Id.print x ++ strbrk " matching " ++ Id.print y ++ + strbrk " while " ++ Id.print x' ++ strbrk " matching " ++ Id.print y' ++ + strbrk " was first found.") + let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' +let mem_recursive_pair (x,y) l = List.mem_f (pair_equal Id.equal Id.equal) (x,y) l + type recursive_pattern_kind = -| RecursiveTerms of bool (* associativity *) -| RecursiveBinders of bool (* associativity *) * glob_constr * glob_constr +| RecursiveTerms of bool (* in reverse order *) +| RecursiveBinders of bool (* in reverse order *) -let compare_recursive_parts found f f' (iterator,subc) = +let compare_recursive_parts recvars found f f' (iterator,subc) = let diff = ref None in let terminator = ref None in let rec aux c1 c2 = match DAst.get c1, DAst.get c2 with @@ -276,32 +288,41 @@ let compare_recursive_parts found f f' (iterator,subc) = List.for_all2eq aux l1 l2 | _ -> mk_glob_constr_eq aux c1 c2 end - | GVar x, GVar y when not (Id.equal x y) -> + | GVar x, GVar y + when mem_recursive_pair (x,y) recvars || mem_recursive_pair (y,x) recvars -> (* We found the position where it differs *) - let lassoc = match !terminator with None -> false | Some _ -> true in - let x,y = if lassoc then y,x else x,y in + let revert = mem_recursive_pair (y,x) recvars in + let x,y = if revert then y,x else x,y in begin match !diff with | None -> - let () = diff := Some (x, y, RecursiveTerms lassoc) in + let () = diff := Some (x, y, RecursiveTerms revert) in + true + | Some (x', y', RecursiveTerms revert') + | Some (x', y', RecursiveBinders revert') -> + check_pair_matching ?loc:c1.CAst.loc x y x' y' revert revert'; true - | Some (x', y', RecursiveTerms lassoc') - | Some (x', y', RecursiveBinders (lassoc',_,_)) -> - Id.equal x x' && Id.equal y y' && lassoc = lassoc' end | GLambda (Name x,_,t_x,c), GLambda (Name y,_,t_y,term) - | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) when not (Id.equal x y) -> + | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) + when mem_recursive_pair (x,y) recvars || mem_recursive_pair (y,x) recvars -> (* We found a binding position where it differs *) - let lassoc = match !terminator with None -> false | Some _ -> true in - let x,t_x,y,t_y = if lassoc then y,t_y,x,t_x else x,t_x,y,t_y in + check_is_hole x t_x; + check_is_hole y t_y; + let revert = mem_recursive_pair (y,x) recvars in + let x,y = if revert then y,x else x,y in begin match !diff with | None -> - let () = diff := Some (x, y, RecursiveBinders (lassoc,t_x,t_y)) in + let () = diff := Some (x, y, RecursiveBinders revert) in aux c term - | Some (x', y', RecursiveBinders (lassoc',_,_)) -> - Id.equal x x' && Id.equal y y' && lassoc = lassoc' - | Some (x', y', RecursiveTerms lassoc') -> - let () = diff := Some (x, y, RecursiveBinders (lassoc,t_x,t_y)) in - Id.equal x x' && Id.equal y y' && lassoc = lassoc' + | Some (x', y', RecursiveBinders revert') -> + check_pair_matching ?loc:c1.CAst.loc x y x' y' revert revert'; + true + | Some (x', y', RecursiveTerms revert') -> + (* Recursive binders have precedence: they can be coerced to + terms but not reciprocally *) + check_pair_matching ?loc:c1.CAst.loc x y x' y' revert revert'; + let () = diff := Some (x, y, RecursiveBinders revert) in + true end | _ -> mk_glob_constr_eq aux c1 c2 in @@ -310,58 +331,36 @@ let compare_recursive_parts found f f' (iterator,subc) = | None -> let loc1 = loc_of_glob_constr iterator in let loc2 = loc_of_glob_constr (Option.get !terminator) in - (* Here, we would need a loc made of several parts ... *) - user_err ?loc:(subtract_loc loc1 loc2) + (* Here, we would need a loc made of several parts ... *) + user_err ?loc:(subtract_loc loc1 loc2) (str "Both ends of the recursive pattern are the same.") - | Some (x,y,RecursiveTerms lassoc) -> - let toadd,x,y,lassoc = - if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_term_vars || - List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_binders_vars - then - None,x,y,lassoc - else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_term_vars || - List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_binders_vars - then - None,y,x,not lassoc - else - Some (x,y),x,y,lassoc in - let iterator = - f' (if lassoc then iterator - else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in - (* found variables have been collected by compare_constr *) + | Some (x,y,RecursiveTerms revert) -> + (* By arbitrary convention, we use the second variable of the pair + as the place-holder for the iterator *) + let iterator = + f' (if revert then iterator else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in + (* found variables have been collected by compare_constr *) found := { !found with vars = List.remove Id.equal y (!found).vars; - recursive_term_vars = Option.fold_right (fun a l -> a::l) toadd (!found).recursive_term_vars }; - NList (x,y,iterator,f (Option.get !terminator),lassoc) - | Some (x,y,RecursiveBinders (lassoc,t_x,t_y)) -> - let toadd,x,y,lassoc = - if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_term_vars || - List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_binders_vars - then - None,x,y,lassoc - else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_term_vars || - List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_binders_vars - then - None,y,x,not lassoc - else - Some (x,y),x,y,lassoc in - let iterator = f' (if lassoc then iterator else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in + recursive_term_vars = List.add_set (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_term_vars }; + NList (x,y,iterator,f (Option.get !terminator),revert) + | Some (x,y,RecursiveBinders revert) -> + let iterator = + f' (if revert then iterator else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in (* found have been collected by compare_constr *) found := { !found with vars = List.remove Id.equal y (!found).vars; - recursive_binders_vars = Option.fold_right (fun a l -> a::l) toadd (!found).recursive_binders_vars }; - check_is_hole x t_x; - check_is_hole y t_y; - NBinderList (x,y,iterator,f (Option.get !terminator),lassoc) + recursive_binders_vars = List.add_set (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_binders_vars }; + NBinderList (x,y,iterator,f (Option.get !terminator),revert) else raise Not_found -let notation_constr_and_vars_of_glob_constr a = +let notation_constr_and_vars_of_glob_constr recvars a = let found = ref { vars = []; recursive_term_vars = []; recursive_binders_vars = [] } in let has_ltac = ref false in (* Turn a glob_constr into a notation_constr by first trying to find a recursive pattern *) let rec aux c = let keepfound = !found in (* n^2 complexity but small and done only once per notation *) - try compare_recursive_parts found aux aux' (split_at_recursive_part c) + try compare_recursive_parts recvars found aux aux' (split_at_recursive_part c) with Not_found -> found := keepfound; match DAst.get c with @@ -449,7 +448,7 @@ let check_variables_and_reversibility nenv else injective := x :: !injective in let check_pair s x y where = - if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then + if not (mem_recursive_pair (x,y) where) then user_err (strbrk "in the right-hand side, " ++ Id.print x ++ str " and " ++ Id.print y ++ strbrk " should appear in " ++ str s ++ str " position as part of a recursive pattern.") in @@ -470,7 +469,8 @@ let check_variables_and_reversibility nenv List.rev !injective let notation_constr_of_glob_constr nenv a = - let a, found, has_ltac = notation_constr_and_vars_of_glob_constr a in + let recvars = Id.Map.bindings nenv.ninterp_rec_vars in + let a, found, has_ltac = notation_constr_and_vars_of_glob_constr recvars a in let injective = check_variables_and_reversibility nenv found in let status = if has_ltac then HasLtac else match injective with | [] -> APrioriReversible @@ -948,28 +948,28 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 = let glue_letin_with_decls = true -let rec match_iterated_binders islambda decls bi lassoc = DAst.(with_loc_val (fun ?loc -> function +let rec match_iterated_binders islambda decls bi revert = DAst.(with_loc_val (fun ?loc -> function | GLambda (na,bk,t,b) as b0 -> begin match na, DAst.get b with | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))]) when islambda && is_gvar p e && not (occur_glob_constr p b) -> - match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b lassoc + match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b revert | _, _ when islambda -> - match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b lassoc + match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b revert | _ -> (decls, DAst.make ?loc b0) end | GProd (na,bk,t,b) as b0 -> begin match na, DAst.get b with | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))]) when not islambda && is_gvar p e && not (occur_glob_constr p b) -> - match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b lassoc + match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b revert | Name _, _ when not islambda -> - match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b lassoc + match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b revert | _ -> (decls, DAst.make ?loc b0) end | GLetIn (na,c,t,b) when glue_letin_with_decls -> match_iterated_binders islambda - ((DAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b lassoc + ((DAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b revert | b -> (decls, DAst.make ?loc b) )) bi @@ -983,7 +983,7 @@ let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas -let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin lassoc = +let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin revert = let rec aux sigma bl rest = try let metas = add_ldots_var (add_meta_bindinglist y metas) in @@ -999,13 +999,13 @@ let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin las with No_match when not (List.is_empty bl) -> bl, rest, sigma in let bl,rest,sigma = aux sigma [] rest in - let bl = if lassoc then List.rev bl else bl in + let bl = if revert then List.rev bl else bl in let alp,sigma = bind_bindinglist_env alp sigma x bl in match_fun alp metas sigma rest termin let add_meta_term x metas = (x,((None,[]),NtnTypeConstr))::metas -let match_termlist match_fun alp metas sigma rest x y iter termin lassoc = +let match_termlist match_fun alp metas sigma rest x y iter termin revert = let rec aux sigma acc rest = try let metas = add_ldots_var (add_meta_term y metas) in @@ -1017,7 +1017,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin lassoc = with No_match when not (List.is_empty acc) -> acc, match_fun metas sigma rest termin in let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in - let l = if lassoc then l else List.rev l 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 *) (* registered for binders *) @@ -1060,49 +1060,49 @@ let rec match_ inner u alp metas sigma a1 a2 = | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1 (* Matching recursive notations for terms *) - | r1, NList (x,y,iter,termin,lassoc) -> - match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin lassoc + | r1, NList (x,y,iter,termin,revert) -> + match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin revert - | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin,lassoc) -> + | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin,revert) -> begin match na1, DAst.get b1, iter with (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *) | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _) when is_gvar p e && not (occur_glob_constr p b1) -> - let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 lassoc in + let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 revert in let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin (* Matching recursive notations for binders: ad hoc cases supporting let-in *) | _, _, NLambda (Name _,_,_) -> - let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 lassoc in + let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 revert in (* TODO: address the possibility that termin is a Lambda itself *) let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin (* Matching recursive notations for binders: general case *) | _, _, _ -> - match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin lassoc + match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert end - | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin,lassoc) -> + | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin,revert) -> (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *) begin match na1, DAst.get b1, iter, termin with | Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _ when is_gvar p e && not (occur_glob_constr p b1) -> - let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 lassoc in + let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 revert in let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin | _, _, NProd (Name _,_,_), _ when na1 != Anonymous -> - let (decls,b) = match_iterated_binders false [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 lassoc in + let (decls,b) = match_iterated_binders false [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 revert in (* TODO: address the possibility that termin is a Prod itself *) let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin (* Matching recursive notations for binders: general case *) | _, _, _, _ -> - match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin lassoc + match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert end (* Matching recursive notations for binders: general case *) - | _r, NBinderList (x,y,iter,termin,lassoc) -> - match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin lassoc + | _r, NBinderList (x,y,iter,termin,revert) -> + match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert (* Matching individual binders as part of a recursive pattern *) | GLambda (na1, bk, t1, b1), NLambda (na2, t2, b2) -> @@ -1278,7 +1278,7 @@ let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v = (* TODO: handle the case of multiple occs in different scopes *) (var,v)::terms,x,termlists,y -let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc = +let match_cases_pattern_list match_fun metas sigma rest x y iter termin revert = let rec aux sigma acc rest = try let metas = add_ldots_var (add_meta_term y metas) in @@ -1290,7 +1290,7 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc = with No_match when not (List.is_empty acc) -> acc, match_fun metas sigma rest termin in let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in - (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists) + (terms,onlybinders,(x,if revert then l else List.rev l)::termlists, binderlists) let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = match DAst.get a1, a2 with @@ -1309,9 +1309,9 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = else let l1',more_args = Util.List.chop le2 l1 in (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) - | r1, NList (x,y,iter,termin,lassoc) -> + | r1, NList (x,y,iter,termin,revert) -> (match_cases_pattern_list (match_cases_pattern_no_more_args) - metas (terms,(),termlists,()) a1 x y iter termin lassoc),(0,[]) + metas (terms,(),termlists,()) a1 x y iter termin revert),(0,[]) | _ -> raise No_match and match_cases_pattern_no_more_args metas sigma a1 a2 = -- cgit v1.2.3 From 6480c7e1d89558252f2e8a8f1b7d3b03f7ef6a74 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Aug 2017 01:11:53 +0200 Subject: Make pattern variables of "match" substitutable in notations. --- interp/constrintern.ml | 72 ++++++++++++++++++++++++++------------------------ 1 file changed, 38 insertions(+), 34 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 52b51ece5f..8e2e3bd238 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -271,18 +271,18 @@ let error_expect_binder_notation_type ?loc id = (Id.print id ++ str " is expected to occur in binding position in the right-hand side.") -let set_var_scope ?loc id istermvar env ntnvars = +let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars = try let isonlybinding,idscopes,typ = Id.Map.find id ntnvars in if istermvar then isonlybinding := false; let () = if istermvar then (* scopes have no effect on the interpretation of identifiers *) begin match !idscopes with - | None -> idscopes := Some (env.tmp_scope, env.scopes) - | Some (tmp, scope) -> - let s1 = make_current_scope tmp scope in - let s2 = make_current_scope env.tmp_scope env.scopes in - if not (List.equal String.equal s1 s2) then error_inconsistent_scope ?loc id s1 s2 + | 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 end in match typ with @@ -371,7 +371,7 @@ let push_name_env ?(global_level=false) ntnvars implargs env = check_hidden_implicit_parameters ?loc id env.impls ; if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var ?loc; - set_var_scope ?loc id false env ntnvars; + set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars; if global_level then Dumpglob.dump_definition (loc,id) true "var" else Dumpglob.dump_binding ?loc id; {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} @@ -457,7 +457,7 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None) in let il,cp = - match !intern_cases_pattern_fwd (None,env.scopes) p with + match !intern_cases_pattern_fwd ntnvars (None,env.scopes) p with | (il, [(subst,cp)]) -> if not (Id.Map.equal Id.equal subst Id.Map.empty) then user_err ?loc (str "Unsupported nested \"as\" clause."); @@ -762,7 +762,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = (* Is [id] a notation variable *) if Id.Map.mem id ntnvars then begin - if not (Id.Map.mem id env.impls) then set_var_scope ?loc id true env ntnvars; + if not (Id.Map.mem id env.impls) then set_var_scope ?loc id true (env.tmp_scope,env.scopes) ntnvars; gvar (loc,id) us, [], [], [] end else @@ -945,7 +945,7 @@ type 'a raw_cases_pattern_expr_r = | RCPatCstr of Globnames.global_reference * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *) - | RCPatAtom of Id.t option + | RCPatAtom of (Id.t * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option | RCPatOr of 'a raw_cases_pattern_expr list and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t @@ -1071,7 +1071,7 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 then let (b,out) = aux i (q,[]) in (b,(DAst.make @@ RCPatAtom None)::out) else fail (remaining_args (len_pl1+i) il) |imp::q,(hh::tt as l) -> if is_status_implicit imp - then let (b,out) = aux i (q,l) in (b,(DAst.make @@ RCPatAtom(None))::out) + then let (b,out) = aux i (q,l) in (b,(DAst.make @@ RCPatAtom None)::out) else let (b,out) = aux (succ i) (q,tt) in (b,hh::out) in aux 0 (impl_list,pl2) @@ -1293,7 +1293,7 @@ let product_of_cases_patterns aliases idspl = let rec subst_pat_iterator y t = DAst.(map (function | RCPatAtom id as p -> - begin match id with Some x when Id.equal x y -> DAst.get t | _ -> p end + begin match id with Some (x,_) when Id.equal x y -> DAst.get t | _ -> p end | RCPatCstr (id,l1,l2) -> RCPatCstr (id,List.map (subst_pat_iterator y t) l1, List.map (subst_pat_iterator y t) l2) @@ -1322,13 +1322,16 @@ let drop_notations_pattern looked_for genv = if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found in (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) - let rec rcp_of_glob x = DAst.(map (function - | GVar id -> RCPatAtom (Some id) + let rec rcp_of_glob scopes x = DAst.(map (function + | GVar id -> RCPatAtom (Some (id,scopes)) | GHole (_,_,_) -> RCPatAtom (None) | GRef (g,_) -> RCPatCstr (g,[],[]) | GApp (r, l) -> begin match DAst.get r with - | GRef (g,_) -> RCPatCstr (g, List.map rcp_of_glob l,[]) + | GRef (g,_) -> + let allscs = find_arguments_scope g in + let allscs = simple_adjust_scopes (List.length l) allscs in (* TO CHECK *) + RCPatCstr (g, List.map2 (fun sc a -> rcp_of_glob (sc,snd scopes) a) allscs l,[]) | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr.") end @@ -1408,7 +1411,7 @@ let drop_notations_pattern looked_for genv = | CPatNotation ("- _",([a],[]),[]) when is_non_zero_pat a -> let p = match a.CAst.v with CPatPrim (Numeral (p, _)) -> p | _ -> assert false in let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (p,false)) scopes in - rcp_of_glob pat + rcp_of_glob scopes pat | CPatNotation ("( _ )",([a],[]),[]) -> in_pat top scopes a | CPatNotation (ntn, fullargs,extrargs) -> @@ -1423,12 +1426,12 @@ let drop_notations_pattern looked_for genv = in_pat top (None,find_delimiters_scope ?loc key::snd scopes) e | CPatPrim p -> let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (test_kind false) p scopes in - rcp_of_glob pat + rcp_of_glob scopes pat | CPatAtom Some id -> begin match drop_syndef top scopes id [] with | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c) - | None -> DAst.make ?loc @@ RCPatAtom (Some (find_pattern_variable id)) + | None -> DAst.make ?loc @@ RCPatAtom (Some (find_pattern_variable id,scopes)) end | CPatAtom None -> DAst.make ?loc @@ RCPatAtom None | CPatOr pl -> DAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl) @@ -1458,7 +1461,7 @@ let drop_notations_pattern looked_for genv = let (a,(scopt,subscopes)) = Id.Map.find id subst in in_pat top (scopt,subscopes@snd scopes) a with Not_found -> - if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some id) else + if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some (id,scopes)) else anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".") end | NRef g -> @@ -1491,9 +1494,9 @@ let drop_notations_pattern looked_for genv = | t -> error_invalid_pattern_notation ?loc () in in_pat true -let rec intern_pat genv aliases pat = +let rec intern_pat genv ntnvars aliases pat = let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 = - let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in + let idslpl2 = List.map (intern_pat genv ntnvars empty_alias) pl2 in let (ids',pll) = product_of_cases_patterns aliases (idslpl1@idslpl2) in let pl' = List.map (fun (asubst,pl) -> (asubst, DAst.make ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in @@ -1502,7 +1505,7 @@ let rec intern_pat genv aliases pat = match DAst.get pat with | RCPatAlias (p, id) -> let aliases' = merge_aliases aliases id in - intern_pat genv aliases' p + intern_pat genv ntnvars aliases' p | RCPatCstr (head, expl_pl, pl) -> if !asymmetric_patterns then let len = if List.is_empty expl_pl then Some (List.length pl) else None in @@ -1515,29 +1518,30 @@ let rec intern_pat genv aliases pat = let with_letin, pl2 = add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2) - | RCPatAtom (Some id) -> + | RCPatAtom (Some (id,scopes)) -> let aliases = merge_aliases aliases id in - (aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)]) + set_var_scope ?loc id false scopes ntnvars; + (aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)]) (* TO CHECK: aura-t-on id? *) | RCPatAtom (None) -> let { alias_ids = ids; alias_map = asubst; } = aliases in (ids, [asubst, DAst.make ?loc @@ PatVar (alias_of aliases)]) | RCPatOr pl -> assert (not (List.is_empty pl)); - let pl' = List.map (intern_pat genv aliases) pl in + let pl' = List.map (intern_pat genv ntnvars aliases) pl in let (idsl,pl') = List.split pl' in let ids = List.hd idsl in check_or_pat_variables loc ids (List.tl idsl); (ids,List.flatten pl') -let intern_cases_pattern genv scopes aliases pat = - intern_pat genv aliases +let intern_cases_pattern genv ntnvars scopes aliases pat = + intern_pat genv ntnvars aliases (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat) let _ = intern_cases_pattern_fwd := - fun scopes p -> intern_cases_pattern (Global.env ()) scopes empty_alias p + fun ntnvars scopes p -> intern_cases_pattern (Global.env ()) ntnvars scopes empty_alias p -let intern_ind_pattern genv scopes pat = +let intern_ind_pattern genv ntnvars scopes pat = let no_not = try drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat @@ -1549,8 +1553,8 @@ let intern_ind_pattern genv scopes pat = let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in let with_letin, pl2 = add_implicits_check_ind_length genv loc c (List.length expl_pl) pl in - let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in - let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in + let idslpl1 = List.rev_map (intern_pat genv ntnvars empty_alias) expl_pl in + let idslpl2 = List.map (intern_pat genv ntnvars empty_alias) pl2 in (with_letin, match product_of_cases_patterns empty_alias (List.rev_append idslpl1 idslpl2) with | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin) @@ -1912,7 +1916,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* Expands a multiple pattern into a disjunction of multiple patterns *) and intern_multiple_pattern env n pl = - let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in + let idsl_pll = List.map (intern_cases_pattern globalenv ntnvars (None,env.scopes) empty_alias) pl in let loc = loc_of_multiple_pattern pl in check_number_of_pattern loc n pl; product_of_cases_patterns empty_alias idsl_pll @@ -1951,7 +1955,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* the "in" part *) let match_td,typ = match t with | Some t -> - let with_letin,(ind,l) = intern_ind_pattern globalenv (None,env.scopes) t in + let with_letin,(ind,l) = intern_ind_pattern globalenv ntnvars (None,env.scopes) t in let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in (* for "in Vect n", we answer (["n","n"],[(loc,"n")]) @@ -2094,7 +2098,7 @@ let intern_type env c = intern_gen IsType env c let intern_pattern globalenv patt = try - intern_cases_pattern globalenv (None,[]) empty_alias patt + intern_cases_pattern globalenv Id.Map.empty (None,[]) empty_alias patt with InternalizationError (loc,e) -> user_err ?loc ~hdr:"internalize" (explain_internalization_error e) -- cgit v1.2.3 From 00bfd6fa443232bc908cfa13553e2fa1cf783ffa Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Aug 2017 01:04:51 +0200 Subject: Preliminary work before extending support for binders in notations (binders shall be substitutable by arbitrary cases patterns). --- interp/constrintern.ml | 30 +++++++++++++++++------------- 1 file changed, 17 insertions(+), 13 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8e2e3bd238..5c9a12c298 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -442,6 +442,22 @@ let intern_letin_binder intern ntnvars env ((loc,na as locna),def,ty) = (push_name_env ntnvars (impls_term_list term) env locna, (na,Explicit,term,ty)) +let intern_cases_pattern_as_binder ?loc ntnvars env p = + let il,cp = + match !intern_cases_pattern_fwd ntnvars (None,env.scopes) p with + | (il, [(subst,cp)]) -> + if not (Id.Map.equal Id.equal subst Id.Map.empty) then + user_err ?loc (str "Unsupported nested \"as\" clause."); + il,cp + | _ -> assert false + in + let env = {env with ids = List.fold_right Id.Set.add il env.ids} in + let na = alias_of_pat cp in + let ienv = Name.fold_right Id.Set.remove na env.ids in + let id = Namegen.next_name_away_with_default "pat" (alias_of_pat cp) ienv in + let na = (loc, Name id) in + env,((cp,il),id),na + let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = function | CLocalAssum(nal,bk,ty) -> let env, bl' = intern_assumption intern ntnvars env nal bk ty in @@ -456,19 +472,7 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func | Some ty -> ty | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None) in - let il,cp = - match !intern_cases_pattern_fwd ntnvars (None,env.scopes) p with - | (il, [(subst,cp)]) -> - if not (Id.Map.equal Id.equal subst Id.Map.empty) then - user_err ?loc (str "Unsupported nested \"as\" clause."); - il,cp - | _ -> assert false - in - let env = {env with ids = List.fold_right Id.Set.add il env.ids} in - let na = alias_of_pat cp in - let ienv = Name.fold_right Id.Set.remove na env.ids in - let id = Namegen.next_name_away_with_default "pat" (alias_of_pat cp) ienv in - let na = (loc, Name id) in + let env, ((cp,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in let bk = Default Explicit in let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in let _,(_,bk,t) = List.hd bl' in -- cgit v1.2.3 From 34cf92821e03a2c6ce64c78c66a00624d0fe9c99 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Aug 2017 14:55:44 +0200 Subject: In printing notations with "match", reasoning up to the order of clauses. --- interp/notation_ops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 602271bf62..e68e8dd97f 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1163,7 +1163,7 @@ let rec match_ inner u alp metas sigma a1 a2 = let sigma = List.fold_left2 (fun s (tm1,_) (tm2,_) -> match_in u alp metas s tm1 tm2) sigma tml1 tml2 in - List.fold_left2 (match_equations u alp metas) sigma eqnl1 eqnl2 + List.fold_left2_set No_match (match_equations u alp metas) sigma eqnl1 eqnl2 | GLetTuple (nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2) when Int.equal (List.length nal1) (List.length nal2) -> let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in -- cgit v1.2.3 From 84e3da72fc14b996b0a917c5b6f011df4b79ab86 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Aug 2017 15:14:46 +0200 Subject: Preliminary steps before adding general support for patterns in notations. Moving earlier functions which will be needed earlier. --- interp/notation_ops.ml | 60 +++++++++++++++++++++++++------------------------- 1 file changed, 30 insertions(+), 30 deletions(-) (limited to 'interp') diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index e68e8dd97f..2a2b6fc911 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -708,6 +708,36 @@ let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v = let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl = (terms,onlybinders,termlists,(x,bl)::binderlists) +let rec map_cases_pattern_name_left f = DAst.map (function + | PatVar na -> PatVar (f na) + | PatCstr (c,l,na) -> PatCstr (c,List.map_left (map_cases_pattern_name_left f) l,f na) + ) + +let rec fold_cases_pattern_eq f x p p' = + let loc = p.CAst.loc in + match DAst.get p, DAst.get p' with + | PatVar na, PatVar na' -> let x,na = f x na na' in x, DAst.make ?loc @@ PatVar na + | PatCstr (c,l,na), PatCstr (c',l',na') when eq_constructor c c' -> + let x,l = fold_cases_pattern_list_eq f x l l' in + let x,na = f x na na' in + x, DAst.make ?loc @@ PatCstr (c,l,na) + | _ -> failwith "Not equal" + +and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with + | [], [] -> x, [] + | p::pl, p'::pl' -> + let x, p = fold_cases_pattern_eq f x p p' in + let x, pl = fold_cases_pattern_list_eq f x pl pl' in + x, p :: pl + | _ -> assert false + +let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with +| PatVar na1, PatVar na2 -> Name.equal na1 na2 +| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> + eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && + Name.equal na1 na2 +| _ -> false + let rec pat_binder_of_term t = DAst.map (function | GVar id -> PatVar (Name id) | GApp (t, l) -> @@ -790,36 +820,6 @@ let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var else (fst alp,(id1,id2)::snd alp),sigma with Not_found -> alp, add_binding_env alp sigma var v -let rec map_cases_pattern_name_left f = DAst.map (function - | PatVar na -> PatVar (f na) - | PatCstr (c,l,na) -> PatCstr (c,List.map_left (map_cases_pattern_name_left f) l,f na) - ) - -let rec fold_cases_pattern_eq f x p p' = - let loc = p.CAst.loc in - match DAst.get p, DAst.get p' with - | PatVar na, PatVar na' -> let x,na = f x na na' in x, DAst.make ?loc @@ PatVar na - | PatCstr (c,l,na), PatCstr (c',l',na') when eq_constructor c c' -> - let x,l = fold_cases_pattern_list_eq f x l l' in - let x,na = f x na na' in - x, DAst.make ?loc @@ PatCstr (c,l,na) - | _ -> failwith "Not equal" - -and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with - | [], [] -> x, [] - | p::pl, p'::pl' -> - let x, p = fold_cases_pattern_eq f x p p' in - let x, pl = fold_cases_pattern_list_eq f x pl pl' in - x, p :: pl - | _ -> assert false - -let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with -| PatVar na1, PatVar na2 -> Name.equal na1 na2 -| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> - eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && - Name.equal na1 na2 -| _ -> false - let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) var bl = let bl = List.rev bl in try -- cgit v1.2.3 From bfed8dcbe7f91ec65ae5e6d1c0a2f06ca7fa01f6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Aug 2017 17:28:32 +0200 Subject: Preliminary work before extending support for binders in notations (binders shall be substitutable by arbitrary cases patterns). Giving a proper status to the functions unifying different instance of the same notation variable (up to alpha-renaming). Note: The a priori change of semantics in "bind_binding_as_term_env" which now apply renaming from "unify_id" (as it did in "bind_bindinglist_as_term_env") should not have an effect since, as the former comment said, this corresponds to a "Anonymous" case which should not occur, since the term would have to be bound upwards. --- interp/notation_ops.ml | 215 +++++++++++++++++++++++++------------------------ 1 file changed, 111 insertions(+), 104 deletions(-) (limited to 'interp') diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 2a2b6fc911..4c4c73fab5 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -751,39 +751,111 @@ let rec pat_binder_of_term t = DAst.map (function | _ -> raise No_match ) t +let unify_name_upto alp na na' = + match na, na' with + | Anonymous, na' -> alp, na' + | na, Anonymous -> alp, na + | Name id, Name id' -> + if Id.equal id id' then alp, na' + else (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' = + match DAst.get v, DAst.get v' with + | GHole _, _ -> v' + | _, GHole _ -> v + | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match + +let unify_opt_term alp v v' = + match v, v' with + | Some t, Some t' -> Some (unify_term alp t t') + | (Some _ as x), None | None, (Some _ as x) -> x + | None, None -> None + +let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match + +let unify_binder_upto alp b b' = + let loc, loc' = CAst.(b.loc, b'.loc) in + match DAst.get b, DAst.get b' with + | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') -> + let alp, na = unify_name_upto alp na na' in + alp, DAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t') + | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') -> + let alp, na = unify_name_upto alp na na' in + alp, DAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t') + | GLocalPattern ((p,ids),id,bk,t), GLocalPattern ((p',_),_,bk',t') -> + let alp, p = unify_pat_upto alp p p' in + alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t') + | _ -> raise No_match + +let rec unify_terms alp vl vl' = + match vl, vl' with + | [], [] -> [] + | v :: vl, v' :: vl' -> unify_term alp v v' :: unify_terms alp vl vl' + | _ -> raise No_match + +let rec unify_binders_upto alp bl bl' = + match bl, bl' with + | [], [] -> alp, [] + | b :: bl, b' :: bl' -> + let alp,b = unify_binder_upto alp b b' in + let alp,bl = unify_binders_upto alp bl bl' in + alp, b :: bl + | _ -> raise No_match + +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' = + if cases_pattern_eq (map_cases_pattern_name_left (Name.map (rename_var (snd alp))) p) p' then p' + else raise No_match + +let unify_term_binder alp c = DAst.(map (fun b' -> + match DAst.get c, b' with + | GVar id, GLocalAssum (na', bk', t') -> + GLocalAssum (unify_id alp id na', bk', t') + | _, GLocalPattern ((p',ids), id, bk', t') -> + let p = pat_binder_of_term c in + GLocalPattern ((unify_pat alp p p',ids), id, bk', t') + | _ -> raise No_match)) + +let rec unify_terms_binders alp cl bl' = + match cl, bl' with + | [], [] -> [] + | c :: cl, b' :: bl' -> + begin match DAst.get b' with + | GLocalDef ( _, _, _, t) -> unify_terms_binders alp cl bl' + | _ -> unify_term_binder alp c b' :: unify_terms_binders alp cl bl' + end + | _ -> raise No_match + let bind_term_env alp (terms,onlybinders,termlists,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 - match DAst.get v, DAst.get v' with - | GHole _, _ -> sigma - | _, GHole _ -> - let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in - add_env alp sigma var v - | _, _ -> - if glob_constr_eq (alpha_rename (snd alp) v) v' then sigma - else raise No_match + let v'' = unify_term alp v v' in + if v'' == v' then sigma else + let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in + add_env alp sigma var v with Not_found -> add_env alp sigma var v let bind_termlist_env alp (terms,onlybinders,termlists,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 unify_term v v' = - match DAst.get v, DAst.get v' with - | GHole _, _ -> v' - | _, GHole _ -> v - | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v' else raise No_match in - let rec unify vl vl' = - match vl, vl' with - | [], [] -> [] - | v :: vl, v' :: vl' -> unify_term v v' :: unify vl vl' - | _ -> raise No_match in - let vl = unify vl vl' in + let vl = unify_terms alp vl vl' in let sigma = (terms,onlybinders,Id.List.remove_assoc var termlists,binderlists) in add_termlist_env alp sigma var vl with Not_found -> add_termlist_env alp sigma var vl let bind_term_as_binding_env alp (terms,onlybinders,termlists,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 | GVar id' -> (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), @@ -797,109 +869,44 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id = try + (* If already bound to a binder, unify the term and the binder *) let v' = Id.List.assoc var onlybinders in - match v' with - | Anonymous -> - (* Should not occur, since the term has to be bound upwards *) - let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in - add_binding_env alp sigma var (Name id) - | Name id' -> - if Id.equal (rename_var (snd alp) id) id' then sigma else raise No_match + let v'' = unify_id alp id v' in + if v' == v'' then sigma + else + let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in + add_binding_env alp sigma var v'' with Not_found -> add_binding_env alp sigma var (Name id) let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var v = try + (* If already bound to a binder possibly *) + (* generating an alpha-renaming from unifying the new binder *) let v' = Id.List.assoc var onlybinders in - match v, v' with - | Anonymous, _ -> alp, sigma - | _, Anonymous -> - let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in - alp, add_binding_env alp sigma var v - | Name id1, Name id2 -> - if Id.equal id1 id2 then alp,sigma - else (fst alp,(id1,id2)::snd alp),sigma + let alp, v'' = unify_name_upto alp v v' in + if v' == v'' then alp, sigma + else + let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in + alp, add_binding_env alp sigma var v with Not_found -> alp, add_binding_env alp sigma var v let bind_bindinglist_env alp (terms,onlybinders,termlists,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 unify_name alp na na' = - match na, na' with - | Anonymous, na' -> alp, na' - | na, Anonymous -> alp, na - | Name id, Name id' -> - if Id.equal id id' then alp, na' - else (fst alp,(id,id')::snd alp), na' in - let unify_pat alp p p' = - try fold_cases_pattern_eq unify_name alp p p' with Failure _ -> raise No_match in - let unify_term alp v v' = - match DAst.get v, DAst.get v' with - | GHole _, _ -> v' - | _, GHole _ -> v - | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in - let unify_opt_term alp v v' = - match v, v' with - | Some t, Some t' -> Some (unify_term alp t t') - | (Some _ as x), None | None, (Some _ as x) -> x - | None, None -> None in - let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in - let unify_binder alp b b' = - let loc, loc' = CAst.(b.loc, b'.loc) in - match DAst.get b, DAst.get b' with - | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') -> - let alp, na = unify_name alp na na' in - alp, DAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t') - | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') -> - let alp, na = unify_name alp na na' in - alp, DAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t') - | GLocalPattern ((p,ids),id,bk,t), GLocalPattern ((p',_),_,bk',t') -> - let alp, p = unify_pat alp p p' in - alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t') - | _ -> raise No_match in - let rec unify alp bl bl' = - match bl, bl' with - | [], [] -> alp, [] - | b :: bl, b' :: bl' -> - let alp,b = unify_binder alp b b' in - let alp,bl = unify alp bl bl' in - alp, b :: bl - | _ -> raise No_match in - let alp, bl = unify alp bl bl' in + let alp, bl = unify_binders_upto alp bl bl' in let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in alp, add_bindinglist_env sigma var bl with Not_found -> alp, add_bindinglist_env sigma var bl -let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) var cl = +let bind_bindinglist_as_termlist_env alp (terms,onlybinders,termlists,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 unify_id 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 in - let unify_pat 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 in - let unify_term_binder c = DAst.(map (fun b' -> - match DAst.get c, b' with - | GVar id, GLocalAssum (na', bk', t') -> - GLocalAssum (unify_id id na', bk', t') - | _, GLocalPattern ((p',ids), id, bk', t') -> - let p = pat_binder_of_term c in - GLocalPattern ((unify_pat p p',ids), id, bk', t') - | _ -> raise No_match )) in - let rec unify cl bl' = - match cl, bl' with - | [], [] -> [] - | c :: cl, b' :: bl' -> - begin match DAst.get b' with - | GLocalDef ( _, _, _, t) -> unify cl bl' - | _ -> unify_term_binder c b' :: unify cl bl' - end - | _ -> raise No_match in - let bl = unify cl bl' in + let bl = unify_terms_binders alp cl bl' in let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in add_bindinglist_env sigma var bl with Not_found -> @@ -1021,7 +1028,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin revert = if is_bindinglist_meta x metas then (* This is a recursive pattern for both bindings and terms; it is *) (* registered for binders *) - bind_bindinglist_as_term_env alp sigma x l + bind_bindinglist_as_termlist_env alp sigma x l else bind_termlist_env alp sigma x l -- cgit v1.2.3 From ecc5658d7efd3a79a6309be6440d1005d30e6285 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Aug 2017 18:19:50 +0200 Subject: Preliminary work before adding general support for patterns in notations I. Factorizing the place where the different form of extended binders (i.e. possibly including the 'pat form) are matched. --- interp/notation_ops.ml | 46 ++++++++++++++++++++-------------------------- 1 file changed, 20 insertions(+), 26 deletions(-) (limited to 'interp') diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 4c4c73fab5..9d338b27f8 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1111,32 +1111,6 @@ let rec match_ inner u alp metas sigma a1 a2 = | _r, NBinderList (x,y,iter,termin,revert) -> match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert - (* Matching individual binders as part of a recursive pattern *) - | GLambda (na1, bk, t1, b1), NLambda (na2, t2, b2) -> - begin match na1, DAst.get b1, na2 with - | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id - when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) -> - let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] in - match_in u alp metas sigma b1 b2 - | _, _, Name id when is_bindinglist_meta id metas -> - let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] in - match_in u alp metas sigma b1 b2 - | _ -> - match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 - end - | GProd (na1, bk, t1, b1), NProd (na2, t2, b2) -> - begin match na1, DAst.get b1, na2 with - | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id - when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) -> - let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] in - match_in u alp metas sigma b1 b2 - | _, _, Name id when is_bindinglist_meta id metas && na1 != Anonymous -> - let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] in - match_in u alp metas sigma b1 b2 - | _ -> - match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 - end - (* Matching compositionally *) | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma | GRef (r1,_), NRef r2 when (eq_gr r1 r2) -> sigma @@ -1151,6 +1125,10 @@ let rec match_ inner u alp metas sigma a1 a2 = let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in List.fold_left2 (match_ may_use_eta u alp metas) (match_in 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 + | 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 | 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 @@ -1236,9 +1214,25 @@ and match_in u = match_ true u and match_hd u = match_ false u and match_binders u alp metas na1 na2 sigma b1 b2 = + (* Match binders which cannot be substituted by a pattern *) let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in match_in u alp metas sigma b1 b2 +and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = + (* Match binders which can be substituted by a pattern *) + match na1, DAst.get b1, na2 with + (* Matching individual binders as part of a recursive pattern *) + | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id + when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) -> + let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in + match_in u alp metas sigma b1 b2 + | _, _, Name id when is_bindinglist_meta id metas && (not isprod || na1 != Anonymous)-> + let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t)] in + match_in u alp metas sigma b1 b2 + | _, _, _ -> + let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in + match_in u alp metas sigma b1 b2 + and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) = (* patl1 and patl2 have the same length because they respectively correspond to some tml1 and tml2 that have the same length *) -- cgit v1.2.3 From e21f70cc2b284a3cf489b16e0251492fb864cf1e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 18 Aug 2017 09:50:17 +0200 Subject: Preliminary work before adding general support for patterns in notations II. Reordering the maps for binders and terms while uninterpreting a notation the same way it will be at the time of interpreting a notation. --- interp/notation_ops.ml | 72 +++++++++++++++++++++++++------------------------- 1 file changed, 36 insertions(+), 36 deletions(-) (limited to 'interp') diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 9d338b27f8..9ea52821c1 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -666,7 +666,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,onlybinders,termlists,binderlists) var v = +let add_env (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 @@ -694,19 +694,19 @@ let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v = refinement *) let v = alpha_rename alpmetas v in (* TODO: handle the case of multiple occs in different scopes *) - ((var,v)::terms,onlybinders,termlists,binderlists) + ((var,v)::terms,termlists,binders,binderlists) -let add_termlist_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var vl = +let add_termlist_env (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,onlybinders,(var,vl)::termlists,binderlists) + (terms,(var,vl)::termlists,binders,binderlists) -let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v = +let add_binding_env alp (terms,termlists,binders,binderlists) var v = (* TODO: handle the case of multiple occs in different scopes *) - (terms,(var,v)::onlybinders,termlists,binderlists) + (terms,termlists,(var,v)::binders,binderlists) -let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl = - (terms,onlybinders,termlists,(x,bl)::binderlists) +let add_bindinglist_env (terms,termlists,binders,binderlists) x bl = + (terms,termlists,binders,(x,bl)::binderlists) let rec map_cases_pattern_name_left f = DAst.map (function | PatVar na -> PatVar (f na) @@ -834,26 +834,26 @@ let rec unify_terms_binders alp cl bl' = end | _ -> raise No_match -let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v = +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 v'' = unify_term alp v v' in if v'' == v' then sigma else - let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in + let sigma = (Id.List.remove_assoc var terms,termlists,binders,binderlists) in add_env alp sigma var v with Not_found -> add_env alp sigma var v -let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var vl = +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 vl = unify_terms alp vl vl' in - let sigma = (terms,onlybinders,Id.List.remove_assoc var termlists,binderlists) in + let sigma = (terms,Id.List.remove_assoc var termlists,binders,binderlists) in add_termlist_env alp sigma var vl with Not_found -> add_termlist_env alp sigma var vl -let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id = +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 @@ -867,47 +867,47 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig (* TODO: look at the consequences for alp *) alp, add_env alp sigma var (DAst.make @@ GVar id) -let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id = +let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var id = try (* If already bound to a binder, unify the term and the binder *) - let v' = Id.List.assoc var onlybinders in + let v' = Id.List.assoc var binders in let v'' = unify_id alp id v' in if v' == v'' then sigma else - let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in + let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in add_binding_env alp sigma var v'' with Not_found -> add_binding_env alp sigma var (Name id) -let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var v = +let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var v = try (* If already bound to a binder possibly *) (* generating an alpha-renaming from unifying the new binder *) - let v' = Id.List.assoc var onlybinders in + let v' = Id.List.assoc var binders in let alp, v'' = unify_name_upto alp v v' in if v' == v'' then alp, sigma else - let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in + let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in alp, add_binding_env alp sigma var v with Not_found -> alp, add_binding_env alp sigma var v -let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) var bl = +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 alp, bl = unify_binders_upto alp bl bl' in - let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in + let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in alp, add_bindinglist_env sigma var bl with Not_found -> alp, add_bindinglist_env sigma var bl -let bind_bindinglist_as_termlist_env alp (terms,onlybinders,termlists,binderlists) var cl = +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 bl = unify_terms_binders alp cl bl' in - let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in + let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in add_bindinglist_env sigma var bl with Not_found -> anomaly (str "There should be a binder list bindings this list of terms.") @@ -980,11 +980,11 @@ let rec match_iterated_binders islambda decls bi revert = DAst.(with_loc_val (fu | b -> (decls, DAst.make ?loc b) )) bi -let remove_sigma x (terms,onlybinders,termlists,binderlists) = - (Id.List.remove_assoc x terms,onlybinders,termlists,binderlists) +let remove_sigma x (terms,termlists,binders,binderlists) = + (Id.List.remove_assoc x terms,termlists,binders,binderlists) -let remove_bindinglist_sigma x (terms,onlybinders,termlists,binderlists) = - (terms,onlybinders,termlists,Id.List.remove_assoc x binderlists) +let remove_bindinglist_sigma x (terms,termlists,binders,binderlists) = + (terms,termlists,binders,Id.List.remove_assoc x binderlists) let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas @@ -1023,7 +1023,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin revert = aux sigma (t::acc) rest with No_match when not (List.is_empty acc) -> acc, match_fun metas sigma rest termin in - let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in + let l,(terms,termlists,binders,binderlists as sigma) = aux 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 *) @@ -1246,7 +1246,7 @@ let term_of_binder bi = DAst.make @@ match bi with | Anonymous -> GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) let match_notation_constr u c (metas,pat) = - let terms,binders,termlists,binderlists = + let terms,termlists,binders,binderlists = match_ false u ([],[]) metas ([],[],[],[]) c pat in (* Reorder canonically the substitution *) let find_binder x = @@ -1290,10 +1290,10 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin revert = aux sigma (t::acc) rest with No_match when not (List.is_empty acc) -> acc, match_fun metas sigma rest termin in - let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in - (terms,onlybinders,(x,if revert then l else List.rev l)::termlists, binderlists) + let l,(terms,termlists,binders,binderlists as sigma) = aux sigma [] rest in + (terms,(x,if revert then l else List.rev l)::termlists,binders,binderlists) -let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = +let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 = match DAst.get a1, a2 with | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) | PatVar Anonymous, NHole _ -> sigma,(0,[]) @@ -1309,10 +1309,10 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = raise No_match else let l1',more_args = Util.List.chop le2 l1 in - (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) + (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) | r1, NList (x,y,iter,termin,revert) -> (match_cases_pattern_list (match_cases_pattern_no_more_args) - metas (terms,(),termlists,()) a1 x y iter termin revert),(0,[]) + metas (terms,termlists,(),()) a1 x y iter termin revert),(0,[]) | _ -> raise No_match and match_cases_pattern_no_more_args metas sigma a1 a2 = @@ -1345,9 +1345,9 @@ let reorder_canonically_substitution terms termlists metas = metas ([],[]) let match_notation_constr_cases_pattern c (metas,pat) = - let (terms,(),termlists,()),more_args = match_cases_pattern metas ([],(),[],()) c pat in + let (terms,termlists,(),()),more_args = match_cases_pattern metas ([],[],(),()) c pat in reorder_canonically_substitution terms termlists metas, more_args let match_notation_constr_ind_pattern ind args (metas,pat) = - let (terms,(),termlists,()),more_args = match_ind_pattern metas ([],(),[],()) ind args pat in + let (terms,termlists,(),()),more_args = match_ind_pattern metas ([],[],(),()) ind args pat in reorder_canonically_substitution terms termlists metas, more_args -- cgit v1.2.3 From 398358618bb3eabfe822b79c669703c1c33b67e6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Aug 2017 18:32:02 +0200 Subject: Adding patterns in the category of binders for notations. For instance, the following is now possible: Check {(x,y)|x+y=0}. Some questions remains. Maybe, by consistency, the notation should be "{'(x,y)|x+y=0}"... --- interp/constrexpr_ops.ml | 39 +++++++++++++++++++++ interp/constrexpr_ops.mli | 5 +++ interp/constrintern.ml | 30 ++++++++++------ interp/notation_ops.ml | 89 ++++++++++++++++++++++++++++------------------- interp/notation_ops.mli | 5 ++- 5 files changed, 120 insertions(+), 48 deletions(-) (limited to 'interp') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 9fe890e901..83add7a7cc 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -545,6 +545,45 @@ let coerce_to_name = function | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" (str "This expression should be a name.") +let mkAppPattern ?loc p lp = + let open CAst in + make ?loc @@ (match p.v with + | CPatAtom (Some r) -> CPatCstr (r, None, lp) + | CPatCstr (r, None, l2) -> + CErrors.user_err ?loc:p.loc ~hdr:"compound_pattern" + (Pp.str "Nested applications not supported.") + | CPatCstr (r, l1, l2) -> CPatCstr (r, l1 , l2@lp) + | CPatNotation (n, s, l) -> CPatNotation (n , s, l@lp) + | _ -> CErrors.user_err + ?loc:p.loc ~hdr:"compound_pattern" + (Pp.str "Such pattern cannot have arguments.")) + +let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function + | CRef (r,None) -> + CPatAtom (Some r) + | CHole (None,Misctypes.IntroAnonymous,None) -> + CPatAtom None + | CLetIn ((loc,Name id),b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' -> + CPatAlias (coerce_to_cases_pattern_expr b, id) + | CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args -> + (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v + | CAppExpl ((None,r,i),args) -> + CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[]) + | CNotation (ntn,(c,cl,[])) -> + CPatNotation (ntn,(List.map coerce_to_cases_pattern_expr c, + List.map (List.map coerce_to_cases_pattern_expr) cl),[]) + | CPrim p -> + CPatPrim p + | CRecord l -> + CPatRecord (List.map (fun (r,p) -> (r,coerce_to_cases_pattern_expr p)) l) + | CDelimiters (s,p) -> + CPatDelimiters (s,coerce_to_cases_pattern_expr p) + | CCast (p,CastConv t) -> + CPatCast (coerce_to_cases_pattern_expr p,t) + | _ -> + CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr" + (str "This expression should be coercible to a pattern.")) c + let asymmetric_patterns = ref (false) let _ = Goptions.declare_bool_option { Goptions.optdepr = false; diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 6e5c0f8515..9a59d66f42 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -54,6 +54,9 @@ val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_e val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [prod_constr_expr], with location *) +val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr +(** Apply a list of pattern arguments to a pattern *) + (** @deprecated variant of mkCLambdaN *) val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr [@@ocaml.deprecated "deprecated variant of mkCLambdaN"] @@ -73,6 +76,8 @@ val coerce_to_id : constr_expr -> Id.t located val coerce_to_name : constr_expr -> Name.t located (** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *) +val coerce_to_cases_pattern_expr : constr_expr -> cases_pattern_expr + (** {6 Binder manipulation} *) val default_binder_kind : binder_kind diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 5c9a12c298..000c7dab37 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -451,7 +451,7 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p = il,cp | _ -> assert false in - let env = {env with ids = List.fold_right Id.Set.add il env.ids} in + let env = List.fold_right (fun id env -> push_name_env Id.Map.empty (Variable,[],[],[]) env (None,Name id)) il env in let na = alias_of_pat cp in let ienv = Name.fold_right Id.Set.remove na env.ids in let id = Namegen.next_name_away_with_default "pat" (alias_of_pat cp) ienv in @@ -546,13 +546,21 @@ let find_fresh_name renaming (terms,termlists,binders) avoid id = next_ident_away_from id (fun id -> Id.Set.mem id fvs3) let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function - | Anonymous -> (renaming,env),Anonymous + | Anonymous -> (renaming,env), None, Anonymous | Name id -> try - (* Binders bound in the notation are considered first-order objects *) - let _,na as locna = coerce_to_name (fst (Id.Map.find id terms)) in - let env = push_name_env Id.Map.empty (Variable,[],[],[]) env locna in - (renaming,env), na + (* 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,((pat,ids),id),na = intern_cases_pattern_as_binder ?loc:pat.CAst.loc Id.Map.empty env pat in + let pat, na = match DAst.get pat with + | PatVar na -> None, na + | _ -> + Some ((ids,pat),id), snd na in + (renaming,env), pat, na + with Not_found -> + try + (* Trying to associate a pattern *) + raise Not_found with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -560,7 +568,7 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function let renaming' = if Id.equal id id' then renaming else Id.Map.add id id' renaming in - (renaming',env), Name id' + (renaming',env), None, Name id' type binder_action = | AddLetIn of Name.t Loc.located * constr_expr * constr_expr option @@ -690,14 +698,14 @@ let instantiate_notation_constr loc intern ntnvars subst infos 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,na = traverse_binder subst avoid subinfos na in + let subinfos,pat,na = traverse_binder 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,aux subst' subinfos c') + DAst.make ?loc @@ GProd (na,Explicit,ty,Option.fold_right apply_cases_pattern pat (aux subst' subinfos c')) | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c') when Name.equal na na' -> - let subinfos,na = traverse_binder subst avoid subinfos na in + let subinfos,pat,na = traverse_binder 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,aux subst' subinfos c') + DAst.make ?loc @@ GLambda (na,Explicit,ty,Option.fold_right apply_cases_pattern pat (aux subst' subinfos c')) | t -> glob_constr_of_notation_constr_with_binders ?loc (traverse_binder subst avoid) (aux subst') subinfos t diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 9ea52821c1..3a3d4ffa8b 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -103,9 +103,13 @@ let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na let rec cases_pattern_fold_map ?loc g e = DAst.with_val (function | PatVar na -> - let e',na' = g e na in e', DAst.make ?loc @@ PatVar na' + let e',pat,na' = g e na in + e', (match pat with + | None -> DAst.make ?loc @@ PatVar na' + | Some ((_,pat),_) -> pat) | PatCstr (cstr,patl,na) -> - let e',na' = g e na in + let e',pat,na' = g e na in + if pat <> None then user_err (Pp.str "Unable to instantiate an \"as\" clause with a pattern."); let e',patl' = List.fold_left_map (cases_pattern_fold_map ?loc g) e patl in e', DAst.make ?loc @@ PatCstr (cstr,patl',na') ) @@ -136,6 +140,16 @@ let rec subst_glob_vars l gc = DAst.map (function let ldots_var = Id.of_string ".." +let protect g e na = + let e',pat,na = g e na in + if pat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern."); + e',na + +let apply_cases_pattern ?loc ((ids,pat),id) c = + let tm = DAst.make ?loc (GVar id) in + DAst.make ?loc @@ + GCases (LetPatternStyle, None, [tm,(Anonymous,None)], [loc,(ids,[pat], c)]) + let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let lt x = DAst.make ?loc x in lt @@ match nc with | NVar id -> GVar id @@ -153,39 +167,43 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in DAst.get (subst_glob_vars outerl it) | NLambda (na,ty,c) -> - let e',na = g e na in GLambda (na,Explicit,f e ty,f e' c) + let e',pat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) pat (f e' c)) | NProd (na,ty,c) -> - let e',na = g e na in GProd (na,Explicit,f e ty,f e' c) + let e',pat,na = g e na in GProd (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) pat (f e' c)) | NLetIn (na,b,t,c) -> - let e',na = g e na in GLetIn (na,f e b,Option.map (f e) t,f e' c) + let e',pat,na = g e na in + (match pat with + | None -> GLetIn (na,f e b,Option.map (f e) t,f e' c) + | Some pat -> DAst.get (apply_cases_pattern ?loc pat (f e' c))) | NCases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with | None -> e',None | Some (ind,nal) -> let e',nal' = List.fold_right (fun na (e',nal) -> - let e',na' = g e' na in e',na'::nal) nal (e',[]) in + let e',na' = protect g e' na in + e',na'::nal) nal (e',[]) in e',Some (Loc.tag ?loc (ind,nal')) in - let e',na' = g e' na 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,na) = g e na in ((Name.cons na idl,e),na) in + let fold (idl,e) na = let (e,pat,na) = g e na in ((Name.cons na idl,e),pat,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 Loc.tag (idl,patl,f e rhs)) eqnl in GCases (sty,Option.map (f e') rtntypopt,tml',eqnl') | NLetTuple (nal,(na,po),b,c) -> - let e',nal = List.fold_left_map g e nal in - let e'',na = g e na in + let e',nal = List.fold_left_map (protect g) e nal in + let e'',na = protect g e na in GLetTuple (nal,(na,Option.map (f e'') po),f e b,f e' c) | NIf (c,(na,po),b1,b2) -> - let e',na = g e na in + let e',na = protect g e na in GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2) | NRec (fk,idl,dll,tl,bl) -> - let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) -> - let e,na = g e na in + let e,dll = Array.fold_left_map (List.fold_map (fun e (na,oc,b) -> + let e,na = protect g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in - let e',idl = Array.fold_left_map (to_id g) e idl in + let e',idl = Array.fold_left_map (to_id (protect g)) e idl in GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) | NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k) | NSort x -> GSort x @@ -195,7 +213,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let glob_constr_of_notation_constr ?loc x = let rec aux () x = - glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),id)) aux () x + glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),None,id)) aux () x in aux () x (******************************************************************************) @@ -867,28 +885,27 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) (* TODO: look at the consequences for alp *) alp, add_env alp sigma var (DAst.make @@ GVar id) -let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var id = +let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c = + let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in try (* If already bound to a binder, unify the term and the binder *) - let v' = Id.List.assoc var binders in - let v'' = unify_id alp id v' in - if v' == v'' then sigma + let pat' = Id.List.assoc var binders in + let pat'' = unify_pat alp pat pat' in + if pat' == pat'' then sigma else let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in - add_binding_env alp sigma var v'' - with Not_found -> add_binding_env alp sigma var (Name id) + add_binding_env alp sigma var pat'' + with Not_found -> add_binding_env alp sigma var pat -let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var v = +let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var pat = try (* If already bound to a binder possibly *) (* generating an alpha-renaming from unifying the new binder *) - let v' = Id.List.assoc var binders in - let alp, v'' = unify_name_upto alp v v' in - if v' == v'' then alp, sigma - else - let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in - alp, add_binding_env alp sigma var v - with Not_found -> alp, add_binding_env alp sigma var v + let pat' = Id.List.assoc var binders in + let alp, pat = unify_pat_upto alp pat pat' in + let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in + alp, add_binding_env alp sigma var pat + with Not_found -> alp, add_binding_env alp sigma var pat let bind_bindinglist_env alp (terms,termlists,binders,binderlists as sigma) var bl = let bl = List.rev bl in @@ -932,7 +949,7 @@ let match_opt f sigma t1 t2 = match (t1,t2) with let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (na1,Name id2) when is_onlybinding_meta id2 metas -> - bind_binding_env alp sigma id2 na1 + bind_binding_env alp sigma id2 (DAst.make (PatVar na1)) | (Name id1,Name id2) when is_term_meta id2 metas -> (* We let the non-binding occurrence define the rhs and hence reason up to *) (* alpha-conversion for the given occurrence of the name (see #4592)) *) @@ -1063,7 +1080,7 @@ let rec match_ inner u alp metas sigma a1 a2 = match DAst.get a1, a2 with (* Matching notation variable *) | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1 - | GVar id1, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1 + | r1, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1 | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1 (* Matching recursive notations for terms *) @@ -1226,6 +1243,10 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) -> let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in match_in u alp metas sigma b1 b2 + | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(_,[cp],b1))]), Name id + when is_gvar p e && is_onlybinding_meta id metas && not (occur_glob_constr p b1) -> + let alp,sigma = bind_binding_env alp sigma id cp in + match_in u alp metas sigma b1 b2 | _, _, Name id when is_bindinglist_meta id metas && (not isprod || na1 != Anonymous)-> let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t)] in match_in u alp metas sigma b1 b2 @@ -1241,16 +1262,12 @@ and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) = (alp,sigma) patl1 patl2 in match_in u alp metas sigma rhs1 rhs2 -let term_of_binder bi = DAst.make @@ match bi with - | Name id -> GVar id - | Anonymous -> GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) - let match_notation_constr u c (metas,pat) = let terms,termlists,binders,binderlists = match_ false u ([],[]) metas ([],[],[],[]) c pat in (* Reorder canonically the substitution *) let find_binder x = - try term_of_binder (Id.List.assoc x binders) + try glob_constr_of_cases_pattern (Id.List.assoc x binders) with Not_found -> (* Happens for binders bound to Anonymous *) (* Find a better way to propagate Anonymous... *) diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 80348c78ee..74be6f5120 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -33,8 +33,11 @@ val notation_constr_of_glob_constr : notation_interp_env -> (** Re-interpret a notation as a [glob_constr], taking care of binders *) +val apply_cases_pattern : ?loc:Loc.t -> + (Id.t list * cases_pattern) * Id.t -> glob_constr -> glob_constr + val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t -> - ('a -> Name.t -> 'a * Name.t) -> + ('a -> Name.t -> 'a * ((Id.t list * cases_pattern) * Id.t) option * Name.t) -> ('a -> notation_constr -> glob_constr) -> 'a -> notation_constr -> glob_constr -- cgit v1.2.3 From edd0d22429354a5f2c703a8c7bd1f775e2f97d9e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 09:15:40 +0200 Subject: Adding support for parsing subterms of a notation as "pattern". This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms. --- interp/constrexpr_ops.ml | 20 ++-- interp/constrextern.ml | 31 +++--- interp/constrintern.ml | 208 +++++++++++++++++++++++++++-------------- interp/constrintern.mli | 5 +- interp/implicit_quantifiers.ml | 4 +- interp/notation.ml | 29 ++++-- interp/notation_ops.ml | 46 ++++----- interp/notation_ops.mli | 1 + interp/ppextend.ml | 1 + interp/ppextend.mli | 1 + 10 files changed, 219 insertions(+), 127 deletions(-) (limited to 'interp') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 83add7a7cc..4877bf271f 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -67,7 +67,7 @@ let rec cases_pattern_expr_eq p1 p2 = if CAst.(p1.v == p2.v) then true else match CAst.(p1.v, p2.v) with | CPatAlias(a1,i1), CPatAlias(a2,i2) -> - Id.equal i1 i2 && cases_pattern_expr_eq a1 a2 + Name.equal (snd i1) (snd i2) && cases_pattern_expr_eq a1 a2 | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) -> eq_reference c1 c2 && Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && @@ -222,9 +222,10 @@ and local_binder_eq l1 l2 = match l1, l2 with List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false -and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) = +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 (List.equal local_binder_eq) bl1 bl2 and instance_eq (x1,c1) (x2,c2) = @@ -268,7 +269,7 @@ let is_constructor id = let rec cases_pattern_fold_names f a 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,id) -> f id a + | CPatAlias (pat,(loc,na)) -> Name.fold_right f na (cases_pattern_fold_names f a pat) | CPatOr (patl) -> List.fold_left (cases_pattern_fold_names f) a patl | CPatCstr (_,patl1,patl2) -> @@ -324,7 +325,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b | CCast (a,CastCoerce) -> f n acc a - | CNotation (_,(l,ll,bll)) -> + | CNotation (_,(l,ll,bl,bll)) -> (* The following is an approximation: we don't know exactly if an ident is binding nor to which subterms bindings apply *) let acc = List.fold_left (f n) acc (l@List.flatten ll) in @@ -394,9 +395,9 @@ let map_constr_expr_with_binders g f e = CAst.map (function | CLetIn (na,a,t,b) -> CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b) | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) - | CNotation (n,(l,ll,bll)) -> + | CNotation (n,(l,ll,bl,bll)) -> (* This is an approximation because we don't know what binds what *) - CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, + CNotation (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)) | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c) | CDelimiters (s,a) -> CDelimiters (s,f e a) @@ -455,9 +456,10 @@ let locs_of_notation ?loc locs ntn = | (ba,ea)::l -> if Int.equal pos ba then aux ea l else (pos,ba)::aux ea l in aux bl (List.sort (fun l1 l2 -> fst l1 - fst l2) locs) -let ntn_loc ?loc (args,argslist,binderslist) = +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 local_binders_loc binderslist) let patntn_loc ?loc (args,argslist) = @@ -564,12 +566,12 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function | CHole (None,Misctypes.IntroAnonymous,None) -> CPatAtom None | CLetIn ((loc,Name id),b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' -> - CPatAlias (coerce_to_cases_pattern_expr b, id) + CPatAlias (coerce_to_cases_pattern_expr b, (loc,Name id)) | CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args -> (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v | CAppExpl ((None,r,i),args) -> CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[]) - | CNotation (ntn,(c,cl,[])) -> + | CNotation (ntn,(c,cl,[],[])) -> CPatNotation (ntn,(List.map coerce_to_cases_pattern_expr c, List.map (List.map coerce_to_cases_pattern_expr) cl),[]) | CPrim p -> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index ef20086e65..013f5713e1 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -257,7 +257,7 @@ let insert_pat_delimiters ?loc p = function let insert_pat_alias ?loc p = function | Anonymous -> p - | Name id -> CAst.make ?loc @@ CPatAlias (p,id) + | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(loc,na)) (**********************************************************************) (* conversion of references *) @@ -323,34 +323,35 @@ let is_zero s = Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1)) in aux 0 -let make_notation_gen loc ntn mknot mkprim destprim l = +let make_notation_gen loc ntn mknot mkprim destprim l bl = match ntn,List.map destprim l with (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *) | "- _", [Some (Numeral (p,true))] when not (is_zero p) -> - mknot (loc,ntn,([mknot (loc,"( _ )",l)])) + assert (bl=[]); + mknot (loc,ntn,([mknot (loc,"( _ )",l,[])]),[]) | _ -> match decompose_notation_key ntn, l with | [Terminal "-"; Terminal x], [] when is_number x -> mkprim (loc, Numeral (x,false)) | [Terminal x], [] when is_number x -> mkprim (loc, Numeral (x,true)) - | _ -> mknot (loc,ntn,l) + | _ -> mknot (loc,ntn,l,bl) -let make_notation loc ntn (terms,termlists,binders as subst) = - if not (List.is_empty termlists) || not (List.is_empty binders) then +let make_notation loc ntn (terms,termlists,binders,binderlists as subst) = + if not (List.is_empty termlists) || not (List.is_empty binderlists) then CAst.make ?loc @@ CNotation (ntn,subst) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> CAst.make ?loc @@ CNotation (ntn,(l,[],[]))) + (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (ntn,(l,[],bl,[]))) (fun (loc,p) -> CAst.make ?loc @@ CPrim p) - destPrim terms + destPrim terms binders let make_pat_notation ?loc ntn (terms,termlists as subst) args = if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (ntn,subst,args)) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args)) + (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args)) (fun (loc,p) -> CAst.make ?loc @@ CPatPrim p) - destPatPrim terms + destPatPrim terms [] let mkPat ?loc qid l = CAst.make ?loc @@ (* Normally irrelevant test with v8 syntax, but let's do it anyway *) @@ -1040,7 +1041,7 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function | _, None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) - let terms,termlists,binders = + let terms,termlists,binders,binderlists = match_notation_constr !print_universes t pat in (* Try availability of interpretation ... *) let e = @@ -1061,11 +1062,15 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function List.map (fun (c,(scopt,scl)) -> List.map (extern true (scopt,scl@scopes') vars) c) termlists in + let bl = + List.map (fun (bl,(scopt,scl)) -> + extern_cases_pattern_in_scope (scopt,scl@scopes') vars bl) + binders in let bll = List.map (fun (bl,(scopt,scl)) -> pi3 (extern_local_binder (scopt,scl@scopes') vars bl)) - binders in - insert_delimiters (make_notation loc ntn (l,ll,bll)) key) + binderlists in + insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key) | SynDefRule kn -> let l = List.map (fun (c,(scopt,scl)) -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 000c7dab37..6a415a8e57 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -213,20 +213,20 @@ let expand_notation_string ntn n = (* This contracts the special case of "{ _ }" for sumbool, sumor notations *) (* Remark: expansion of squash at definition is done in metasyntax.ml *) -let contract_notation ntn (l,ll,bll) = +let contract_curly_brackets ntn (l,ll,bl,bll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | { CAst.v = CNotation ("{ _ }",([a],[],[])) } :: l -> + | { CAst.v = CNotation ("{ _ }",([a],[],[],[])) } :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> a::contract_squash (n+1) l in let l = contract_squash 0 l in (* side effect; don't inline *) - !ntn',(l,ll,bll) + !ntn',(l,ll,bl,bll) -let contract_pat_notation ntn (l,ll) = +let contract_curly_brackets_pat ntn (l,ll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] @@ -286,14 +286,9 @@ let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars = end in match typ with - | NtnInternTypeBinder -> + | Notation_term.NtnInternTypeOnlyBinder -> if istermvar then error_expect_binder_notation_type ?loc id - | NtnInternTypeConstr -> - (* We need sometimes to parse idents at a constr level for - factorization and we cannot enforce this constraint: - if not istermvar then error_expect_constr_notation_type loc id *) - () - | NtnInternTypeIdent -> () + | Notation_term.NtnInternTypeAny -> () with Not_found -> (* Not in a notation *) () @@ -302,6 +297,9 @@ let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_name let reset_tmp_scope env = {env with tmp_scope = None} +let set_env_scopes env (scopt,subscopes) = + {env with tmp_scope = scopt; scopes = subscopes @ env.scopes} + let mkGProd ?loc (na,bk,t) body = DAst.make ?loc @@ GProd (na, bk, t, body) let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body) @@ -451,7 +449,7 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p = il,cp | _ -> assert false in - let env = List.fold_right (fun id env -> push_name_env Id.Map.empty (Variable,[],[],[]) env (None,Name id)) il env in + let env = List.fold_right (fun (loc,id) env -> push_name_env ntnvars (Variable,[],[],[]) env (loc,Name id)) il env in let na = alias_of_pat cp in let ienv = Name.fold_right Id.Set.remove na env.ids in let id = Namegen.next_name_away_with_default "pat" (alias_of_pat cp) ienv in @@ -476,7 +474,7 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func let bk = Default Explicit in let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in let _,(_,bk,t) = List.hd bl' in - (env, (DAst.make ?loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl) + (env, (DAst.make ?loc @@ GLocalPattern((cp,List.map snd il),id,bk,t)) :: bl) let intern_generalization intern env ntnvars loc bk ak c = let c = intern {env with unb = true} c in @@ -532,7 +530,7 @@ let option_mem_assoc id = function | Some (id',c) -> Id.equal id id' | None -> false -let find_fresh_name renaming (terms,termlists,binders) avoid id = +let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id = let fold1 _ (c, _) accu = Id.Set.union (free_vars_of_constr_expr c) accu in let fold2 _ (l, _) accu = let fold accu c = Id.Set.union (free_vars_of_constr_expr c) accu in @@ -545,22 +543,27 @@ let find_fresh_name renaming (terms,termlists,binders) avoid id = (* TODO binders *) next_ident_away_from id (fun id -> Id.Set.mem id fvs3) -let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function +let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function | Anonymous -> (renaming,env), None, Anonymous | Name id -> 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,((pat,ids),id),na = intern_cases_pattern_as_binder ?loc:pat.CAst.loc Id.Map.empty env pat in + let env,((pat,ids),id),na = intern_pat ntnvars env pat in let pat, na = match DAst.get pat with | PatVar na -> None, na - | _ -> - Some ((ids,pat),id), snd na in + | _ -> Some ((List.map snd ids,pat),id), snd na in (renaming,env), pat, na with Not_found -> try (* Trying to associate a pattern *) - raise Not_found + let pat,scopes = Id.Map.find id binders in + let env = set_env_scopes env scopes in + let env,((pat,ids),id),na = intern_pat ntnvars env pat in + let pat, na = match DAst.get pat with + | PatVar na -> None, na + | _ -> Some ((List.map snd ids,pat),id), snd na in + (renaming,env), pat, na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -612,8 +615,8 @@ let flatten_binders bl = | a -> [a] in List.flatten (List.map dispatch bl) -let instantiate_notation_constr loc intern ntnvars subst infos c = - let (terms,termlists,binders) = subst in +let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = + let (terms,termlists,binders,binderlists) = subst in (* when called while defining a notation, avoid capturing the private binders of the expression by variables bound by the notation (see #3892) *) let avoid = Id.Map.domain ntnvars in @@ -644,7 +647,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = (if revert then List.rev l else l),scopes with Not_found -> try - let (bl,(scopt,subscopes)) = Id.Map.find x binders in + let (bl,(scopt,subscopes)) = Id.Map.find x binderlists in let env,bl' = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in terms_of_binders (if revert then bl' else List.rev bl'),(None,[]) with Not_found -> @@ -671,14 +674,21 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = let gc = intern nenv c in (gc, Some c) in - let bindings = Id.Map.map mk_env terms in + let mk_env' (c, (tmp_scope, subscopes)) = + let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in + let _,((pat,_),_),_ = intern_pat ntnvars nenv c in + (glob_constr_of_cases_pattern pat, None) + in + let terms = Id.Map.map mk_env terms in + let binders = Id.Map.map mk_env' binders in + let bindings = Id.Map.fold Id.Map.add terms binders in Some (Genintern.generic_substitute_notation bindings arg) in DAst.make ?loc @@ GHole (knd, naming, arg) | NBinderList (x,y,iter,terminator,revert) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) - let (bl,(scopt,subscopes)) = Id.Map.find x binders in + let (bl,(scopt,subscopes)) = Id.Map.find x binderlists in (* We flatten binders so that we can interpret them at substitution time *) let bl = flatten_binders bl in let bl = if revert then List.rev bl else bl in @@ -698,17 +708,17 @@ let instantiate_notation_constr loc intern ntnvars subst infos 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,pat,na = traverse_binder subst avoid subinfos na in + let subinfos,pat,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 pat (aux subst' subinfos c')) | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c') when Name.equal na na' -> - let subinfos,pat,na = traverse_binder subst avoid subinfos na in + let subinfos,pat,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 pat (aux subst' subinfos c')) | t -> glob_constr_of_notation_constr_with_binders ?loc - (traverse_binder subst avoid) (aux subst') subinfos t + (traverse_binder intern_pat ntnvars subst avoid) (aux subst') subinfos t and subst_var (terms, binderopt, _terminopt) (renaming, env) id = (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) @@ -717,6 +727,15 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = intern {env with tmp_scope = scopt; scopes = subscopes @ env.scopes} a with Not_found -> + try + let pat,scopes = Id.Map.find id binders in + let env = set_env_scopes env scopes in + (* We deactivate the check on hidden parameters *) + (* since we are only interested in the pattern as a term *) + let env = reset_hidden_inductive_implicit_test env in + let env,((pat,ids),id),na = intern_pat ntnvars env pat in + glob_constr_of_cases_pattern pat + with Not_found -> try match binderopt with | Some (x,binder) when Id.equal x id -> @@ -733,27 +752,71 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = GVar id) in aux (terms,None,None) infos c -let split_by_type ids = - List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) -> +(* Turning substitution coming from parsing and based on production + into a substitution for interpretation and based on binding/constr + distinction *) + +let split_by_type ids subst = + let bind id scl l s = + match l with + | [] -> assert false + | a::l -> l, Id.Map.add id (a,scl) s in + let (terms,termlists,binders,binderlists),subst = + List.fold_left (fun ((terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')) (id,(scl,typ)) -> + match typ with + | NtnTypeConstr -> + let terms,terms' = bind id scl terms terms' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') + | NtnTypeBinder true -> + 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,scl) binders' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') + | NtnTypeBinder false -> + let binders,binders' = bind id scl binders binders' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') + | NtnTypeConstrList -> + let termlists,termlists' = bind id scl termlists termlists' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') + | NtnTypeBinderList -> + let binderlists,binderlists' = bind id scl binderlists binderlists' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')) + (subst,(Id.Map.empty,Id.Map.empty,Id.Map.empty,Id.Map.empty)) ids in + assert (terms = [] && termlists = [] && binders = [] && binderlists = []); + subst + +let split_by_type_pat ?loc ids subst = + let bind id scl l s = + match l with + | [] -> assert false + | a::l -> l, Id.Map.add id (a,scl) s in + let (terms,termlists),subst = + List.fold_left (fun ((terms,termlists),(terms',termlists')) (id,(scl,typ)) -> match typ with - | NtnTypeConstr | NtnTypeOnlyBinder -> ((x,scl)::l1,l2,l3) - | NtnTypeConstrList -> (l1,(x,scl)::l2,l3) - | NtnTypeBinderList -> (l1,l2,(x,scl)::l3)) ids ([],[],[]) + | NtnTypeConstr | NtnTypeBinder _ -> + let terms,terms' = bind id scl terms terms' in + (terms,termlists),(terms',termlists') + | NtnTypeConstrList -> + let termlists,termlists' = bind id scl termlists termlists' in + (terms,termlists),(terms',termlists') + | NtnTypeBinderList -> error_invalid_pattern_notation ?loc ()) + (subst,(Id.Map.empty,Id.Map.empty)) ids in + assert (terms = [] && termlists = []); + subst let make_subst ids l = let fold accu (id, scl) a = Id.Map.add id (a, scl) accu in List.fold_left2 fold Id.Map.empty ids l let intern_notation intern env ntnvars loc ntn fullargs = - let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in + (* Adjust to parsing of { } *) + let ntn,fullargs = contract_curly_brackets ntn fullargs in + (* Recover interpretation { } *) let ((ids,c),df) = interp_notation ?loc ntn (env.tmp_scope,env.scopes) in Dumpglob.dump_notation_location (ntn_loc ?loc fullargs ntn) ntn df; - let ids,idsl,idsbl = split_by_type ids in - let terms = make_subst ids args in - let termlists = make_subst idsl argslist in - let binders = make_subst idsbl bll in - instantiate_notation_constr loc intern ntnvars - (terms, termlists, binders) (Id.Map.empty, env) c + (* 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 (**********************************************************************) (* Discriminating between bound variables and global references *) @@ -883,10 +946,10 @@ let intern_qualid loc qid intern env ntnvars us args = let args1,args2 = List.chop nids args in check_no_explicitation args1; let terms = make_subst ids (List.map fst args1) in - let subst = (terms, Id.Map.empty, Id.Map.empty) in + let subst = (terms, Id.Map.empty, Id.Map.empty, Id.Map.empty) in let infos = (Id.Map.empty, env) in let projapp = match c with NRef _ -> true | _ -> false in - let c = instantiate_notation_constr loc intern ntnvars subst infos c in + let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in let loc = c.CAst.loc in let err () = user_err ?loc (str "Notation " ++ pr_qualid qid @@ -953,11 +1016,11 @@ let interp_reference vars r = (** Private internalization patterns *) type 'a raw_cases_pattern_expr_r = - | RCPatAlias of 'a raw_cases_pattern_expr * Id.t + | RCPatAlias of 'a raw_cases_pattern_expr * Name.t Loc.located | RCPatCstr of Globnames.global_reference * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *) - | RCPatAtom of (Id.t * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option + | RCPatAtom of (Id.t Loc.located * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option | RCPatOr of 'a raw_cases_pattern_expr list and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t @@ -1017,7 +1080,7 @@ let check_number_of_pattern loc n l = if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p))) let check_or_pat_variables loc ids idsl = - if List.exists (fun ids' -> not (List.eq_set Id.equal ids ids')) idsl then + if List.exists (fun ids' -> not (List.eq_set (fun (loc,id) (_,id') -> Id.equal id id') ids ids')) idsl then user_err ?loc (str "The components of this disjunctive pattern must bind the same variables.") @@ -1256,7 +1319,7 @@ let sort_fields ~complete loc fields completer = (** {6 Manage multiple aliases} *) type alias = { - alias_ids : Id.t list; + alias_ids : Id.t Loc.located list; alias_map : Id.t Id.Map.t; } @@ -1267,17 +1330,20 @@ let empty_alias = { (* [merge_aliases] returns the sets of all aliases encountered at this point and a substitution mapping extra aliases to the first one *) -let merge_aliases aliases id = - let alias_ids = aliases.alias_ids @ [id] in +let merge_aliases aliases (loc,na) = + match na with + | Anonymous -> aliases + | Name id -> + let alias_ids = aliases.alias_ids @ [loc,id] in let alias_map = match aliases.alias_ids with | [] -> aliases.alias_map - | id' :: _ -> Id.Map.add id id' aliases.alias_map + | (_,id') :: _ -> Id.Map.add id id' aliases.alias_map in { alias_ids; alias_map; } let alias_of als = match als.alias_ids with | [] -> Anonymous -| id :: _ -> Name id +| (_,id) :: _ -> Name id (** {6 Expanding notations } @@ -1295,6 +1361,8 @@ let is_zero s = let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 let product_of_cases_patterns aliases idspl = + (* each [pl] is a disjunction of patterns over common identifiers [ids] *) + (* We stepwise build a disjunction of patterns [ptaill] over common [ids'] *) List.fold_right (fun (ids,pl) (ids',ptaill) -> (ids @ ids', (* Cartesian prod of the or-pats for the nth arg and the tail args *) @@ -1305,7 +1373,7 @@ let product_of_cases_patterns aliases idspl = let rec subst_pat_iterator y t = DAst.(map (function | RCPatAtom id as p -> - begin match id with Some (x,_) when Id.equal x y -> DAst.get t | _ -> p end + begin match id with Some ((_,x),_) when Id.equal x y -> DAst.get t | _ -> p end | RCPatCstr (id,l1,l2) -> RCPatCstr (id,List.map (subst_pat_iterator y t) l1, List.map (subst_pat_iterator y t) l2) @@ -1335,7 +1403,7 @@ let drop_notations_pattern looked_for genv = in (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) let rec rcp_of_glob scopes x = DAst.(map (function - | GVar id -> RCPatAtom (Some (id,scopes)) + | GVar id -> RCPatAtom (Some ((x.CAst.loc,id),scopes)) | GHole (_,_,_) -> RCPatAtom (None) | GRef (g,_) -> RCPatCstr (g,[],[]) | GApp (r, l) -> @@ -1426,24 +1494,22 @@ let drop_notations_pattern looked_for genv = rcp_of_glob scopes pat | CPatNotation ("( _ )",([a],[]),[]) -> in_pat top scopes a - | CPatNotation (ntn, fullargs,extrargs) -> - let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in + | CPatNotation (ntn,fullargs,extrargs) -> + let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in - let (ids',idsl',_) = split_by_type ids' in + let (terms,termlists) = split_by_type_pat ?loc ids' (terms,termlists) in Dumpglob.dump_notation_location (patntn_loc ?loc fullargs ntn) ntn df; - let substlist = make_subst idsl' argsl in - let subst = make_subst ids' args in - in_not top loc scopes (subst,substlist) extrargs c + in_not top loc scopes (terms,termlists) extrargs c | CPatDelimiters (key, e) -> in_pat top (None,find_delimiters_scope ?loc key::snd scopes) e | CPatPrim p -> let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (test_kind false) p scopes in rcp_of_glob scopes pat - | CPatAtom Some id -> + | CPatAtom (Some id) -> begin match drop_syndef top scopes id [] with | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c) - | None -> DAst.make ?loc @@ RCPatAtom (Some (find_pattern_variable id,scopes)) + | None -> DAst.make ?loc @@ RCPatAtom (Some ((loc,find_pattern_variable id),scopes)) end | CPatAtom None -> DAst.make ?loc @@ RCPatAtom None | CPatOr pl -> DAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl) @@ -1473,7 +1539,7 @@ let drop_notations_pattern looked_for genv = let (a,(scopt,subscopes)) = Id.Map.find id subst in in_pat top (scopt,subscopes@snd scopes) a with Not_found -> - if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some (id,scopes)) else + if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some ((loc,id),scopes)) else anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".") end | NRef g -> @@ -1530,8 +1596,8 @@ let rec intern_pat genv ntnvars aliases pat = let with_letin, pl2 = add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2) - | RCPatAtom (Some (id,scopes)) -> - let aliases = merge_aliases aliases id in + | RCPatAtom (Some ((loc,id),scopes)) -> + let aliases = merge_aliases aliases (loc,Name id) in set_var_scope ?loc id false scopes ntnvars; (aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)]) (* TO CHECK: aura-t-on id? *) | RCPatAtom (None) -> @@ -1565,10 +1631,9 @@ let intern_ind_pattern genv ntnvars scopes pat = let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in let with_letin, pl2 = add_implicits_check_ind_length genv loc c (List.length expl_pl) pl in - let idslpl1 = List.rev_map (intern_pat genv ntnvars empty_alias) expl_pl in - let idslpl2 = List.map (intern_pat genv ntnvars empty_alias) pl2 in + let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in (with_letin, - match product_of_cases_patterns empty_alias (List.rev_append idslpl1 idslpl2) with + match product_of_cases_patterns empty_alias idslpl with | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin) | _ -> error_bad_inductive_type ?loc) | x -> error_bad_inductive_type ?loc @@ -1740,10 +1805,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = DAst.make ?loc @@ GLetIn (snd na, inc1, int, intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) - | CNotation ("- _", ([a],[],[])) when is_non_zero a -> + | CNotation ("- _", ([a],[],[],[])) when is_non_zero a -> let p = match a.CAst.v with CPrim (Numeral (p, _)) -> p | _ -> assert false in intern env (CAst.make ?loc @@ CPrim (Numeral (p,false))) - | CNotation ("( _ )",([a],[],[])) -> intern env a + | CNotation ("( _ )",([a],[],[],[])) -> intern env a | CNotation (ntn,args) -> intern_notation intern env ntnvars loc ntn args | CGeneralization (b,a,c) -> @@ -1775,8 +1840,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CRef (ref,us) -> intern_applied_reference intern env (Environ.named_context globalenv) lvar us args ref - | CNotation (ntn,([],[],[])) -> - let c = intern_notation intern env ntnvars loc ntn ([],[],[]) in + | CNotation (ntn,([],[],[],[])) -> + let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in let x, impl, scopes, l = find_appl_head_data c in (x,impl,scopes,l), args | _ -> (intern env f,[],[],[]), args in @@ -1878,6 +1943,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | None -> None | Some gen -> let (ltacvars, ntnvars) = lvar in + (* Preventively declare notation variables in ltac as non-bindings *) + Id.Map.iter (fun x (isonlybinding,_,_) -> isonlybinding := false) ntnvars; let ntnvars = Id.Map.domain ntnvars in let extra = ltacvars.ltac_extra in let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in @@ -1946,6 +2013,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = and intern_eqn n env (loc,(lhs,rhs)) = let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in (* Linearity implies the order in ids is irrelevant *) + let eqn_ids = List.map snd eqn_ids in check_linearity lhs eqn_ids; let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in List.map (fun (asubst,pl) -> @@ -2193,7 +2261,7 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = let out_scope = function None -> None,[] | Some (a,l) -> a,l in let unused = match reversible with NonInjective ids -> ids | _ -> [] in let vars = Id.Map.mapi (fun id (isonlybinding, sc, typ) -> - (!isonlybinding && not (List.mem_f Id.equal id unused), out_scope !sc, typ)) vl in + (!isonlybinding && not (List.mem_f Id.equal id unused), out_scope !sc)) vl in (* Returns [a] and the ordered list of variables with their scopes *) vars, a, reversible diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 87b587b71c..f09b17a49f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -87,7 +87,7 @@ val intern_gen : typing_constraint -> env -> constr_expr -> glob_constr val intern_pattern : env -> cases_pattern_expr -> - Id.t list * (Id.t Id.Map.t * cases_pattern) list + Id.t Loc.located list * (Id.t Id.Map.t * cases_pattern) list val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list @@ -184,8 +184,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_ guaranteed to have the same domain as the input one. *) val interp_notation_constr : env -> ?impls:internalization_env -> notation_interp_env -> constr_expr -> - (bool * subscopes * notation_var_internalization_type) Id.Map.t * - notation_constr * reversibility_status + (bool * subscopes) Id.Map.t * notation_constr * reversibility_status (** Globalization options *) val parsing_explicit : bool ref diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 519f2480ba..a838d7106b 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -93,8 +93,8 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = in let rec aux bdvars l c = match CAst.(c.v) with | CRef (Ident (loc,id),_) -> found loc id bdvars l - | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (Ident (_, id),_) } :: _, [], [])) when not (Id.Set.mem id bdvars) -> - Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c + | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (Ident (_, id),_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) -> + Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c diff --git a/interp/notation.ml b/interp/notation.ml index 31f16e1a90..e6186e08c2 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -82,18 +82,31 @@ let parenRelation_eq t1 t2 = match t1, t2 with | Prec l1, Prec l2 -> Int.equal l1 l2 | _ -> false -let notation_var_internalization_type_eq v1 v2 = match v1, v2 with -| NtnInternTypeConstr, NtnInternTypeConstr -> true -| NtnInternTypeBinder, NtnInternTypeBinder -> true -| NtnInternTypeIdent, NtnInternTypeIdent -> true -| (NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent), _ -> false +open Extend + +let production_level_eq l1 l2 = true (* (l1 = l2) *) + +let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with +| NextLevel, NextLevel -> true +| NumLevel n1, NumLevel n2 -> Int.equal n1 n2 +| (NextLevel | NumLevel _), _ -> false *) + +let constr_entry_key_eq v1 v2 = match v1, v2 with +| ETName, ETName -> true +| ETReference, ETReference -> true +| ETBigint, ETBigint -> true +| ETBinder b1, ETBinder b2 -> b1 == b2 +| ETConstr (n1,pp1), ETConstr (n2,pp2) -> production_level_eq n1 n2 && production_position_eq pp1 pp2 +| ETPattern n1, ETPattern n2 -> Int.equal n1 n2 +| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2' +| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _), _ -> false let level_eq (l1, t1, u1) (l2, t2, u2) = let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in Int.equal l1 l2 && List.equal tolerability_eq t1 t2 - && List.equal notation_var_internalization_type_eq u1 u2 + && List.equal constr_entry_key_eq u1 u2 let declare_scope scope = try let _ = String.Map.find scope !scope_map in () @@ -611,10 +624,10 @@ let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true -| NtnTypeOnlyBinder, NtnTypeOnlyBinder -> true +| NtnTypeBinder b1, NtnTypeBinder b2 -> b1 = (b2:bool) | NtnTypeConstrList, NtnTypeConstrList -> true | NtnTypeBinderList, NtnTypeBinderList -> true -| (NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList), _ -> false +| (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) = pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 3a3d4ffa8b..ec568823e3 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -472,17 +472,16 @@ let check_variables_and_reversibility nenv str " position as part of a recursive pattern.") in let check_type x typ = match typ with - | NtnInternTypeConstr -> + | NtnInternTypeAny -> begin try check_pair "term" x (Id.Map.find x recvars) foundrec with Not_found -> check_bound x end - | NtnInternTypeBinder -> + | NtnInternTypeOnlyBinder -> begin try check_pair "binding" x (Id.Map.find x recvars) foundrecbinding with Not_found -> check_bound x - end - | NtnInternTypeIdent -> check_bound x in + end in Id.Map.iter check_type vars; List.rev !injective @@ -665,7 +664,7 @@ let is_term_meta id metas = with Not_found -> false let is_onlybinding_meta id metas = - try match Id.List.assoc id metas with _,NtnTypeOnlyBinder -> true | _ -> false + try match Id.List.assoc id metas with _,NtnTypeBinder _ -> true | _ -> false with Not_found -> false let is_bindinglist_meta id metas = @@ -885,8 +884,11 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) (* TODO: look at the consequences for alp *) alp, add_env alp sigma var (DAst.make @@ GVar id) +let force_cases_pattern c = + DAst.make ?loc:c.CAst.loc (DAst.get c) + let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c = - let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in + let pat = try force_cases_pattern (cases_pattern_of_glob_constr Anonymous c) with Not_found -> raise No_match in try (* If already bound to a binder, unify the term and the binder *) let pat' = Id.List.assoc var binders in @@ -961,8 +963,10 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match -let rec match_cases_pattern_binders metas acc pat1 pat2 = +let rec match_cases_pattern_binders metas (alp,sigma as acc) pat1 pat2 = match DAst.get pat1, DAst.get pat2 with + | _, PatVar (Name id2) when is_onlybinding_meta id2 metas -> + bind_binding_env alp sigma id2 pat1 | PatVar na1, PatVar na2 -> match_names metas acc na1 na2 | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2) when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) -> @@ -1265,26 +1269,24 @@ and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) = let match_notation_constr u c (metas,pat) = let terms,termlists,binders,binderlists = match_ false u ([],[]) metas ([],[],[],[]) c pat in - (* Reorder canonically the substitution *) - let find_binder x = - try glob_constr_of_cases_pattern (Id.List.assoc x binders) - with Not_found -> - (* Happens for binders bound to Anonymous *) - (* Find a better way to propagate Anonymous... *) - DAst.make @@GVar x in - List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> + (* 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') -> match typ with | NtnTypeConstr -> let term = try Id.List.assoc x terms with Not_found -> raise No_match in - ((term, scl)::terms',termlists',binders') - | NtnTypeOnlyBinder -> - ((find_binder x, scl)::terms',termlists',binders') + ((term, scl)::terms',termlists',binders',binderlists') + | NtnTypeBinder true -> + let v = glob_constr_of_cases_pattern (Id.List.assoc x binders) in + ((v,scl)::terms',termlists',binders',binderlists') + | NtnTypeBinder false -> + (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists') | NtnTypeConstrList -> - (terms',(Id.List.assoc x termlists,scl)::termlists',binders') + (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists') | NtnTypeBinderList -> let bl = try Id.List.assoc x binderlists with Not_found -> raise No_match in - (terms',termlists',(bl, scl)::binders')) - metas ([],[],[]) + (terms',termlists',binders',(bl, scl)::binderlists')) + metas ([],[],[],[]) (* Matching cases pattern *) @@ -1356,7 +1358,7 @@ let reorder_canonically_substitution terms termlists metas = List.fold_right (fun (x,(scl,typ)) (terms',termlists') -> match typ with | NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists') - | NtnTypeOnlyBinder -> assert false + | NtnTypeBinder _ -> assert false | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists') | NtnTypeBinderList -> assert false) metas ([],[]) diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 74be6f5120..1a2dfc9cac 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -52,6 +52,7 @@ exception No_match val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> ('a glob_constr_g * subscopes) list * ('a glob_constr_g list * subscopes) list * + ('a cases_pattern_g * subscopes) list * ('a extended_glob_local_binder_g list * subscopes) list val match_notation_constr_cases_pattern : diff --git a/interp/ppextend.ml b/interp/ppextend.ml index ce19dd8a92..606196fcd1 100644 --- a/interp/ppextend.ml +++ b/interp/ppextend.ml @@ -33,6 +33,7 @@ let ppcmd_of_cut = function type unparsing = | UnpMetaVar of int * parenRelation + | UnpBinderMetaVar of int * parenRelation | UnpListMetaVar of int * parenRelation * unparsing list | UnpBinderListMetaVar of int * bool * unparsing list | UnpTerminal of string diff --git a/interp/ppextend.mli b/interp/ppextend.mli index 7b62a2074b..77823e32a5 100644 --- a/interp/ppextend.mli +++ b/interp/ppextend.mli @@ -26,6 +26,7 @@ val ppcmd_of_cut : ppcut -> Pp.t type unparsing = | UnpMetaVar of int * parenRelation + | UnpBinderMetaVar of int * parenRelation | UnpListMetaVar of int * parenRelation * unparsing list | UnpBinderListMetaVar of int * bool * unparsing list | UnpTerminal of string -- cgit v1.2.3 From 3a6b1d2c04ceeb568accbc9ddfc3fc0f14faf25b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 17 Aug 2017 12:35:56 +0200 Subject: Respecting the ident/pattern distinction in notation modifiers. --- interp/constrintern.ml | 4 ++-- interp/notation.ml | 8 +++++++- interp/notation_ops.ml | 15 ++++++++++----- 3 files changed, 19 insertions(+), 8 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6a415a8e57..63cf66bdda 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -767,11 +767,11 @@ let split_by_type ids subst = | NtnTypeConstr -> let terms,terms' = bind id scl terms terms' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder true -> + | NtnTypeBinder NtnParsedAsConstr -> 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,scl) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder false -> + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) -> let binders,binders' = bind id scl binders binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') | NtnTypeConstrList -> diff --git a/interp/notation.ml b/interp/notation.ml index e6186e08c2..e2e769d2fc 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -622,9 +622,15 @@ let availability_of_prim_token n printer_scope local_scopes = let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 +let notation_binder_source_eq s1 s2 = match s1, s2 with + | NtnParsedAsConstr, NtnParsedAsConstr -> true + | NtnParsedAsIdent, NtnParsedAsIdent -> true + | NtnParsedAsPattern, NtnParsedAsPattern -> true + | (NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern), _ -> false + let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true -| NtnTypeBinder b1, NtnTypeBinder b2 -> b1 = (b2:bool) +| NtnTypeBinder s1, NtnTypeBinder s2 -> notation_binder_source_eq s1 s2 | NtnTypeConstrList, NtnTypeConstrList -> true | NtnTypeBinderList, NtnTypeBinderList -> true | (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ec568823e3..b7c1d84f13 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -667,6 +667,10 @@ let is_onlybinding_meta id metas = try match Id.List.assoc id metas with _,NtnTypeBinder _ -> true | _ -> false with Not_found -> false +let is_onlybinding_pattern_like_meta id metas = + try match Id.List.assoc id metas with _,NtnTypeBinder (NtnParsedAsConstr | NtnParsedAsPattern) -> true | _ -> false + with Not_found -> false + let is_bindinglist_meta id metas = try match Id.List.assoc id metas with _,NtnTypeBinderList -> true | _ -> false with Not_found -> false @@ -965,7 +969,7 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with let rec match_cases_pattern_binders metas (alp,sigma as acc) pat1 pat2 = match DAst.get pat1, DAst.get pat2 with - | _, PatVar (Name id2) when is_onlybinding_meta id2 metas -> + | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta id2 metas -> bind_binding_env alp sigma id2 pat1 | PatVar na1, PatVar na2 -> match_names metas acc na1 na2 | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2) @@ -1084,7 +1088,8 @@ let rec match_ inner u alp metas sigma a1 a2 = match DAst.get a1, a2 with (* Matching notation variable *) | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1 - | r1, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1 + | r1, NVar id2 when is_onlybinding_pattern_like_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1 + | GVar _, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1 | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1 (* Matching recursive notations for terms *) @@ -1248,7 +1253,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in match_in u alp metas sigma b1 b2 | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(_,[cp],b1))]), Name id - when is_gvar p e && is_onlybinding_meta id metas && not (occur_glob_constr p b1) -> + when is_gvar p e && is_onlybinding_pattern_like_meta id metas && not (occur_glob_constr p b1) -> let alp,sigma = bind_binding_env alp sigma id cp in match_in u alp metas sigma b1 b2 | _, _, Name id when is_bindinglist_meta id metas && (not isprod || na1 != Anonymous)-> @@ -1276,10 +1281,10 @@ let match_notation_constr u c (metas,pat) = | NtnTypeConstr -> let term = try Id.List.assoc x terms with Not_found -> raise No_match in ((term, scl)::terms',termlists',binders',binderlists') - | NtnTypeBinder true -> + | NtnTypeBinder NtnParsedAsConstr -> let v = glob_constr_of_cases_pattern (Id.List.assoc x binders) in ((v,scl)::terms',termlists',binders',binderlists') - | NtnTypeBinder false -> + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) -> (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists') | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists') -- cgit v1.2.3 From bc73f267ad2da0f1e24e66cb481725be018a8ce6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 21 Aug 2017 23:25:21 +0200 Subject: A (significant) simplification in printing notations with recursive binders. For historical reasons (this was one of the first examples of notations with binders), there was a special treatment for notations whose right-hand side had the form "forall x, P" or "fun x => P". Not only this is not necessary, but this prevents notations binding to expressions such as "forall x, x>0 -> P" to be used in printing. We let the general case absorb this particular case. We add the integration of "let x:=c in ..." in the middle of a notation with recursive binders as part of the binder list, reprinting it "(x:=c)" (this was formerly the case only for the above particular case). Note that integrating "let" in sequence of binders is stil not the case for the regular "forall"/"fun". Should we? --- interp/notation_ops.ml | 80 +++++++------------------------------------------- 1 file changed, 11 insertions(+), 69 deletions(-) (limited to 'interp') diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index b7c1d84f13..0480a93e27 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -975,36 +975,9 @@ let rec match_cases_pattern_binders metas (alp,sigma as acc) pat1 pat2 = | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2) when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) -> List.fold_left2 (match_cases_pattern_binders metas) - (match_names metas acc na1 na2) patl1 patl2 + (match_names metas acc na1 na2) patl1 patl2 | _ -> raise No_match -let glue_letin_with_decls = true - -let rec match_iterated_binders islambda decls bi revert = DAst.(with_loc_val (fun ?loc -> function - | GLambda (na,bk,t,b) as b0 -> - begin match na, DAst.get b with - | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))]) - when islambda && is_gvar p e && not (occur_glob_constr p b) -> - match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b revert - | _, _ when islambda -> - match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b revert - | _ -> (decls, DAst.make ?loc b0) - end - | GProd (na,bk,t,b) as b0 -> - begin match na, DAst.get b with - | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))]) - when not islambda && is_gvar p e && not (occur_glob_constr p b) -> - match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b revert - | Name _, _ when not islambda -> - match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b revert - | _ -> (decls, DAst.make ?loc b0) - end - | GLetIn (na,c,t,b) when glue_letin_with_decls -> - match_iterated_binders islambda - ((DAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b revert - | b -> (decls, DAst.make ?loc b) - )) bi - let remove_sigma x (terms,termlists,binders,binderlists) = (Id.List.remove_assoc x terms,termlists,binders,binderlists) @@ -1015,7 +988,9 @@ let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas -let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin revert = +let glue_letin_with_decls = true + +let match_binderlist match_fun alp metas sigma rest x y iter termin revert = let rec aux sigma bl rest = try let metas = add_ldots_var (add_meta_bindinglist y metas) in @@ -1028,8 +1003,12 @@ let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin rev (* In case y is bound not only to a binder but also to a term *) let sigma = remove_sigma y sigma in aux sigma (b::bl) rest - with No_match when not (List.is_empty bl) -> - bl, rest, sigma in + with No_match -> + match DAst.get rest with + | GLetIn (na,c,t,rest) when glue_letin_with_decls -> + let b = DAst.make ?loc:rest.CAst.loc @@ GLocalDef (na,Explicit (*?*), c,t) in + aux sigma (b::bl) rest + | _ -> if not (List.is_empty bl) then bl, rest, sigma else raise No_match in let bl,rest,sigma = aux sigma [] rest in let bl = if revert then List.rev bl else bl in let alp,sigma = bind_bindinglist_env alp sigma x bl in @@ -1096,46 +1075,9 @@ let rec match_ inner u alp metas sigma a1 a2 = | r1, NList (x,y,iter,termin,revert) -> match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin revert - | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin,revert) -> - begin match na1, DAst.get b1, iter with - (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *) - | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _) - when is_gvar p e && not (occur_glob_constr p b1) -> - let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 revert in - let alp,sigma = bind_bindinglist_env alp sigma x decls in - match_in u alp metas sigma b termin - (* Matching recursive notations for binders: ad hoc cases supporting let-in *) - | _, _, NLambda (Name _,_,_) -> - let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 revert in - (* TODO: address the possibility that termin is a Lambda itself *) - let alp,sigma = bind_bindinglist_env alp sigma x decls in - match_in u alp metas sigma b termin - (* Matching recursive notations for binders: general case *) - | _, _, _ -> - match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert - end - - | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin,revert) -> - (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *) - begin match na1, DAst.get b1, iter, termin with - | Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _ - when is_gvar p e && not (occur_glob_constr p b1) -> - let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 revert in - let alp,sigma = bind_bindinglist_env alp sigma x decls in - match_in u alp metas sigma b termin - | _, _, NProd (Name _,_,_), _ when na1 != Anonymous -> - let (decls,b) = match_iterated_binders false [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 revert in - (* TODO: address the possibility that termin is a Prod itself *) - let alp,sigma = bind_bindinglist_env alp sigma x decls in - match_in u alp metas sigma b termin - (* Matching recursive notations for binders: general case *) - | _, _, _, _ -> - match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert - end - (* Matching recursive notations for binders: general case *) | _r, NBinderList (x,y,iter,termin,revert) -> - match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert + 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 -- cgit v1.2.3 From 15abe33f55b317410223bd48576fa35c81943ff9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 14 Feb 2018 19:55:21 +0100 Subject: Refining the strategy for glueing let-ins to a sequence of binders. To deal with existing notations starting with a "let" (see notation "for" in output/Notation2.v) we adopt the pragmatic approach of glueing only inner let by default. Ideally, it might be nicer to detect if there is an overlap of notation, and not to glue only in case of overlap. We could also decide that a notation starting with a "let" should always be protected by some constant, say "id", so as to avoid possible collisions, but this would require changes user side. --- interp/notation_ops.ml | 31 ++++++++++++++++++++++++------- 1 file changed, 24 insertions(+), 7 deletions(-) (limited to 'interp') diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 0480a93e27..5fe12e5705 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -988,10 +988,18 @@ let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas -let glue_letin_with_decls = true +(* This tells if letins in the middle of binders should be included in + the sequence of binders *) +let glue_inner_letin_with_decls = true + +(* This tells if trailing letins (with no further proper binders) + should be included in sequence of binders *) +let glue_trailing_letin_with_decls = false + +exception OnlyTrailingLetIns let match_binderlist match_fun alp metas sigma rest x y iter termin revert = - let rec aux sigma bl rest = + let rec aux trailing_letins sigma bl rest = 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 @@ -1002,14 +1010,23 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert = 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 *) let sigma = remove_sigma y sigma in - aux sigma (b::bl) rest + aux false sigma (b::bl) rest with No_match -> match DAst.get rest with - | GLetIn (na,c,t,rest) when glue_letin_with_decls -> + | GLetIn (na,c,t,rest') when glue_inner_letin_with_decls -> let b = DAst.make ?loc:rest.CAst.loc @@ GLocalDef (na,Explicit (*?*), c,t) in - aux sigma (b::bl) rest - | _ -> if not (List.is_empty bl) then bl, rest, sigma else raise No_match in - let bl,rest,sigma = aux sigma [] rest in + (* collect let-in *) + (try aux true sigma (b::bl) rest' + with OnlyTrailingLetIns + when not (trailing_letins && not glue_trailing_letin_with_decls) -> + (* renounce to take into account trailing let-ins *) + if not (List.is_empty bl) then bl, rest, sigma else raise No_match) + | _ -> + if trailing_letins && not glue_trailing_letin_with_decls then + (* Backtrack to when we tried to glue letins *) + raise OnlyTrailingLetIns; + if not (List.is_empty bl) then bl, rest, sigma else raise No_match in + let bl,rest,sigma = aux false sigma [] rest in let bl = if revert then List.rev bl else bl in let alp,sigma = bind_bindinglist_env alp sigma x bl in match_fun alp metas sigma rest termin -- cgit v1.2.3 From 50970e4043d73d9a4fbd17ffe765745f6d726317 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 21 Aug 2017 23:01:04 +0200 Subject: Using an "as" clause when needed for printing irrefutable patterns. Example which is now reprinted as parsed: fun '((x,y) as z) => (y,x)=z --- interp/constrextern.ml | 6 ++++-- interp/notation_ops.ml | 6 ++++-- 2 files changed, 8 insertions(+), 4 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 013f5713e1..67e19d1258 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -924,7 +924,8 @@ and sub_extern inctx (_,scopes) = extern inctx (None,scopes) and factorize_prod scopes vars na bk aty c = match na, DAst.get c with | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],[(_,(_,[p],b))]) - when is_gvar id e && not (occur_glob_constr id b) -> + when is_gvar id e -> + let p = if occur_glob_constr id b then set_pat_alias id p else p in let b = extern_typ scopes vars b in let p = extern_cases_pattern_in_scope scopes vars p in let binder = CLocalPattern (c.loc,(p,None)) in @@ -946,7 +947,8 @@ and factorize_prod scopes vars na bk aty c = and factorize_lambda inctx scopes vars na bk aty c = match na, DAst.get c with | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],[(_,(_,[p],b))]) - when is_gvar id e && not (occur_glob_constr id b) -> + when is_gvar id e -> + let p = if occur_glob_constr id b then set_pat_alias id p else p in let b = sub_extern inctx scopes vars b in let p = extern_cases_pattern_in_scope scopes vars p in let binder = CLocalPattern (c.loc,(p,None)) in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 5fe12e5705..c44863791e 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1208,11 +1208,13 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = match na1, DAst.get b1, na2 with (* Matching individual binders as part of a recursive pattern *) | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id - when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) -> + when is_gvar p e && is_bindinglist_meta id metas -> + let cp = if occur_glob_constr p b1 then set_pat_alias p cp else cp in let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in match_in u alp metas sigma b1 b2 | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(_,[cp],b1))]), Name id - when is_gvar p e && is_onlybinding_pattern_like_meta id metas && not (occur_glob_constr p b1) -> + when is_gvar p e && is_onlybinding_pattern_like_meta id metas -> + let cp = if occur_glob_constr p b1 then set_pat_alias p cp else cp in let alp,sigma = bind_binding_env alp sigma id cp in match_in u alp metas sigma b1 b2 | _, _, Name id when is_bindinglist_meta id metas && (not isprod || na1 != Anonymous)-> -- cgit v1.2.3 From e4d93d1cef27d3a8c1e36139fc1e118730406f67 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 17 Aug 2017 20:12:55 +0200 Subject: Adding general support for irrefutable disjunctive patterns. This now works not only for parsing of fun/forall (as in 8.6), but also for arbitraty notations with binders and for printing. --- interp/constrexpr_ops.ml | 4 ++ interp/constrexpr_ops.mli | 2 + interp/constrextern.ml | 34 ++++++++----- interp/constrintern.ml | 86 ++++++++++++++++++++------------- interp/notation_ops.ml | 120 +++++++++++++++++++++++++++------------------- interp/notation_ops.mli | 6 +-- 6 files changed, 153 insertions(+), 99 deletions(-) (limited to 'interp') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 4877bf271f..8aca6e3333 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -547,6 +547,10 @@ let coerce_to_name = function | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" (str "This expression should be a name.") +let mkCPatOr ?loc = function + | [pat] -> pat + | disjpat -> CAst.make ?loc @@ (CPatOr disjpat) + let mkAppPattern ?loc p lp = let open CAst in make ?loc @@ (match p.v with diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 9a59d66f42..0b00b0e4dc 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -54,6 +54,8 @@ val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_e val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [prod_constr_expr], with location *) +val mkCPatOr : ?loc:Loc.t -> cases_pattern_expr list -> cases_pattern_expr + val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr (** Apply a list of pattern arguments to a pattern *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 67e19d1258..9e18966b63 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -922,16 +922,21 @@ and extern_typ (_,scopes) = and sub_extern inctx (_,scopes) = extern inctx (None,scopes) and factorize_prod scopes vars na bk aty c = + let store, get = set_temporary_memory () in match na, DAst.get c with - | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],[(_,(_,[p],b))]) - when is_gvar id e -> - let p = if occur_glob_constr id b then set_pat_alias id p else p in + | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) + when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 -> + (match get () with + | [(_,(ids,disj_of_patl,b))] -> + let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in + 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 = extern_cases_pattern_in_scope scopes vars p in + let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in let binder = CLocalPattern (c.loc,(p,None)) in (match b.v with | CProdN (bl,b) -> CProdN (binder::bl,b) | _ -> CProdN ([binder],b)) + | _ -> assert false) | _, _ -> let c = extern_typ scopes vars c in match na, c.v with @@ -945,16 +950,21 @@ and factorize_prod scopes vars na bk aty c = CProdN ([CLocalAssum([Loc.tag na],Default bk,aty)],c) and factorize_lambda inctx scopes vars na bk aty c = + let store, get = set_temporary_memory () in match na, DAst.get c with - | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],[(_,(_,[p],b))]) - when is_gvar id e -> - let p = if occur_glob_constr id b then set_pat_alias id p else p in + | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) + when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 -> + (match get () with + | [(_,(ids,disj_of_patl,b))] -> + let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in + 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 = extern_cases_pattern_in_scope scopes vars p in + let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in let binder = CLocalPattern (c.loc,(p,None)) in (match b.v with | CLambdaN (bl,b) -> CLambdaN (binder::bl,b) | _ -> CLambdaN ([binder],b)) + | _ -> assert false) | _, _ -> let c = sub_extern inctx scopes vars c in match c.v with @@ -994,7 +1004,7 @@ and extern_local_binder scopes vars = function | GLocalPattern ((p,_),_,bk,ty) -> let ty = if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in - let p = extern_cases_pattern vars p 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(Loc.tag @@ (p,ty)) :: l) @@ -1066,10 +1076,10 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function termlists in let bl = List.map (fun (bl,(scopt,scl)) -> - extern_cases_pattern_in_scope (scopt,scl@scopes') vars bl) + mkCPatOr (List.map (extern_cases_pattern_in_scope (scopt,scl@scopes') vars) bl)) binders in - let bll = - List.map (fun (bl,(scopt,scl)) -> + let bll = + List.map (fun (bl,(scopt,scl)) -> pi3 (extern_local_binder (scopt,scl@scopes') vars bl)) binderlists in insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 63cf66bdda..379d09e895 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -441,20 +441,19 @@ let intern_letin_binder intern ntnvars env ((loc,na as locna),def,ty) = (na,Explicit,term,ty)) let intern_cases_pattern_as_binder ?loc ntnvars env p = - let il,cp = - match !intern_cases_pattern_fwd ntnvars (None,env.scopes) p with - | (il, [(subst,cp)]) -> - if not (Id.Map.equal Id.equal subst Id.Map.empty) then - user_err ?loc (str "Unsupported nested \"as\" clause."); - il,cp - | _ -> assert false + let il,disjpat = + let (il, subst_disjpat) = !intern_cases_pattern_fwd ntnvars (None,env.scopes) p in + let substl,disjpat = List.split subst_disjpat in + if not (List.for_all (fun subst -> Id.Map.equal Id.equal subst Id.Map.empty) substl) then + user_err ?loc (str "Unsupported nested \"as\" clause."); + il,disjpat in let env = List.fold_right (fun (loc,id) env -> push_name_env ntnvars (Variable,[],[],[]) env (loc,Name id)) il env in - let na = alias_of_pat cp in + let na = alias_of_pat (List.hd disjpat) in let ienv = Name.fold_right Id.Set.remove na env.ids in - let id = Namegen.next_name_away_with_default "pat" (alias_of_pat cp) ienv in + let id = Namegen.next_name_away_with_default "pat" na ienv in let na = (loc, Name id) in - env,((cp,il),id),na + env,((disjpat,il),id),na let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = function | CLocalAssum(nal,bk,ty) -> @@ -470,11 +469,11 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func | Some ty -> ty | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None) in - let env, ((cp,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in + let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in let bk = Default Explicit in let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in let _,(_,bk,t) = List.hd bl' in - (env, (DAst.make ?loc @@ GLocalPattern((cp,List.map snd il),id,bk,t)) :: bl) + (env, (DAst.make ?loc @@ GLocalPattern((disjpat,List.map snd il),id,bk,t)) :: bl) let intern_generalization intern env ntnvars loc bk ak c = let c = intern {env with unb = true} c in @@ -518,9 +517,11 @@ let rec expand_binders ?loc mk bl c = expand_binders ?loc mk bl (DAst.make ?loc @@ GLetIn (n, b, oty, c)) | GLocalAssum (n, bk, t) -> expand_binders ?loc mk bl (mk ?loc (n,bk,t) c) - | GLocalPattern ((pat,ids), id, bk, ty) -> + | GLocalPattern ((disjpat,ids), id, bk, ty) -> let tm = DAst.make ?loc (GVar id) in - let c = DAst.make ?loc @@ GCases (Misctypes.LetPatternStyle, None, [tm,(Anonymous,None)], [loc,(ids,[pat], c)]) in + (* Distribute the disjunctive patterns over the shared right-hand side *) + let eqnl = List.map (fun pat -> (loc,(ids,[pat],c))) disjpat in + let c = DAst.make ?loc @@ GCases (Misctypes.LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in expand_binders ?loc mk bl (mk ?loc (Name id,Explicit,ty) c) (**********************************************************************) @@ -543,26 +544,32 @@ let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id = (* TODO binders *) next_ident_away_from id (fun id -> Id.Set.mem id fvs3) +let is_var store pat = + match DAst.get pat with + | PatVar na -> store na; true + | _ -> false + let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function | Anonymous -> (renaming,env), None, Anonymous | Name id -> + let store,get = set_temporary_memory () 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,((pat,ids),id),na = intern_pat ntnvars env pat in - let pat, na = match DAst.get pat with - | PatVar na -> None, na - | _ -> Some ((List.map snd ids,pat),id), snd na in + let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in + let pat, na = match disjpat with + | [pat] when is_var store pat -> let na = get () in None, na + | _ -> Some ((List.map snd ids,disjpat),id), snd na in (renaming,env), pat, na with Not_found -> try (* Trying to associate a pattern *) let pat,scopes = Id.Map.find id binders in let env = set_env_scopes env scopes in - let env,((pat,ids),id),na = intern_pat ntnvars env pat in - let pat, na = match DAst.get pat with - | PatVar na -> None, na - | _ -> Some ((List.map snd ids,pat),id), snd na in + let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in + let pat, na = match disjpat with + | [pat] when is_var store pat -> let na = get () in None, na + | _ -> Some ((List.map snd ids,disjpat),id), snd na in (renaming,env), pat, na with Not_found -> (* Binders not bound in the notation do not capture variables *) @@ -582,10 +589,16 @@ type binder_action = let dmap_with_loc f n = CAst.map_with_loc (fun ?loc c -> f ?loc (DAst.get_thunk c)) n +let error_cannot_coerce_wildcard_term ?loc () = + user_err ?loc Pp.(str "Cannot turn \"_\" into a term.") + +let error_cannot_coerce_disjunctive_pattern_term ?loc () = + user_err ?loc Pp.(str "Cannot turn a disjunctive pattern into a term.") + let terms_of_binders bl = let rec term_of_pat pt = dmap_with_loc (fun ?loc -> function | PatVar (Name id) -> CRef (Ident (loc,id), None) - | PatVar (Anonymous) -> user_err Pp.(str "Cannot turn \"_\" into a term.") + | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in @@ -599,7 +612,8 @@ let terms_of_binders bl = | GLocalDef (Name id,_,_,_) -> extract_variables l | GLocalDef (Anonymous,_,_,_) | GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.") - | GLocalPattern ((u,_),_,_,_) -> term_of_pat u :: extract_variables l + | GLocalPattern (([u],_),_,_,_) -> term_of_pat u :: extract_variables l + | GLocalPattern ((_,_),_,_,_) -> error_cannot_coerce_disjunctive_pattern_term ?loc () end | [] -> [] in extract_variables bl @@ -676,8 +690,10 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = in let mk_env' (c, (tmp_scope, subscopes)) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in - let _,((pat,_),_),_ = intern_pat ntnvars nenv c in - (glob_constr_of_cases_pattern pat, None) + let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in + match disjpat with + | [pat] -> (glob_constr_of_cases_pattern pat, None) + | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.CAst.loc () in let terms = Id.Map.map mk_env terms in let binders = Id.Map.map mk_env' binders in @@ -708,14 +724,14 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos 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,pat,na = traverse_binder intern_pat ntnvars subst avoid subinfos na in + 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 pat (aux subst' subinfos c')) + 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,pat,na = traverse_binder intern_pat ntnvars subst avoid subinfos na in + 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 pat (aux subst' subinfos c')) + 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') subinfos t @@ -730,11 +746,13 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = try let pat,scopes = Id.Map.find id binders in let env = set_env_scopes env scopes in - (* We deactivate the check on hidden parameters *) - (* since we are only interested in the pattern as a term *) + (* We deactivate impls to avoid the check on hidden parameters *) + (* and since we are only interested in the pattern as a term *) let env = reset_hidden_inductive_implicit_test env in - let env,((pat,ids),id),na = intern_pat ntnvars env pat in - glob_constr_of_cases_pattern pat + let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in + match disjpat with + | [pat] -> glob_constr_of_cases_pattern pat + | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.") with Not_found -> try match binderopt with diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index c44863791e..81cdecf03d 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -101,17 +101,24 @@ let name_to_ident = function let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na +let product_of_cases_patterns patl = + List.fold_right (fun patl restl -> + List.flatten (List.map (fun p -> List.map (fun rest -> p::rest) restl) patl)) + patl [[]] + let rec cases_pattern_fold_map ?loc g e = DAst.with_val (function | PatVar na -> - let e',pat,na' = g e na in - e', (match pat with - | None -> DAst.make ?loc @@ PatVar na' - | Some ((_,pat),_) -> pat) + let e',disjpat,na' = g e na in + e', (match disjpat with + | None -> [DAst.make ?loc @@ PatVar na'] + | Some ((_,disjpat),_) -> disjpat) | PatCstr (cstr,patl,na) -> - let e',pat,na' = g e na in - if pat <> None then user_err (Pp.str "Unable to instantiate an \"as\" clause with a pattern."); + let e',disjpat,na' = g e na in + if disjpat <> None then user_err (Pp.str "Unable to instantiate an \"as\" clause with a pattern."); let e',patl' = List.fold_left_map (cases_pattern_fold_map ?loc g) e patl in - e', DAst.make ?loc @@ PatCstr (cstr,patl',na') + (* Distribute outwards the inner disjunctive patterns *) + let disjpatl' = product_of_cases_patterns patl' in + e', List.map (fun patl' -> DAst.make ?loc @@ PatCstr (cstr,patl',na')) disjpatl' ) let subst_binder_type_vars l = function @@ -141,14 +148,14 @@ let rec subst_glob_vars l gc = DAst.map (function let ldots_var = Id.of_string ".." let protect g e na = - let e',pat,na = g e na in - if pat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern."); + let e',disjpat,na = g e na in + if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern."); e',na -let apply_cases_pattern ?loc ((ids,pat),id) c = +let apply_cases_pattern ?loc ((ids,disjpat),id) c = let tm = DAst.make ?loc (GVar id) in - DAst.make ?loc @@ - GCases (LetPatternStyle, None, [tm,(Anonymous,None)], [loc,(ids,[pat], c)]) + let eqns = List.map (fun pat -> (loc,(ids,[pat],c))) disjpat in + DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqns) let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let lt x = DAst.make ?loc x in lt @@ match nc with @@ -167,14 +174,14 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in DAst.get (subst_glob_vars outerl it) | NLambda (na,ty,c) -> - let e',pat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) pat (f e' c)) + let e',disjpat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) | NProd (na,ty,c) -> - let e',pat,na = g e na in GProd (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) pat (f e' c)) + let e',disjpat,na = g e na in GProd (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) | NLetIn (na,b,t,c) -> - let e',pat,na = g e na in - (match pat with + let e',disjpat,na = g e na in + (match disjpat with | None -> GLetIn (na,f e b,Option.map (f e) t,f e' c) - | Some pat -> DAst.get (apply_cases_pattern ?loc pat (f e' c))) + | Some disjpat -> DAst.get (apply_cases_pattern ?loc disjpat (f e' c))) | NCases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with @@ -183,15 +190,16 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let e',nal' = List.fold_right (fun na (e',nal) -> let e',na' = protect g e' na in e',na'::nal) nal (e',[]) in - e',Some (Loc.tag ?loc (ind,nal')) in + e',Some (Loc.tag ?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,pat,na) = g e na in ((Name.cons na idl,e),pat,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 eqnl' = List.map (fun (patl,rhs) -> - let ((idl,e),patl) = - List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in - Loc.tag (idl,patl,f e rhs)) eqnl in - GCases (sty,Option.map (f e') rtntypopt,tml',eqnl') + let ((idl,e),patl) = + List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in + let disjpatl = product_of_cases_patterns patl in + List.map (fun patl -> Loc.tag (idl,patl,f e rhs)) disjpatl) eqnl in + GCases (sty,Option.map (f e') rtntypopt,tml',List.flatten eqnl') | NLetTuple (nal,(na,po),b,c) -> let e',nal = List.fold_left_map (protect g) e nal in let e'',na = protect g e na in @@ -806,8 +814,8 @@ let unify_binder_upto alp b b' = | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') -> let alp, na = unify_name_upto alp na na' in alp, DAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t') - | GLocalPattern ((p,ids),id,bk,t), GLocalPattern ((p',_),_,bk',t') -> - let alp, p = unify_pat_upto alp p p' in + | GLocalPattern ((disjpat,ids),id,bk,t), GLocalPattern ((disjpat',_),_,bk',t') when List.length disjpat = List.length disjpat' -> + let alp, p = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t') | _ -> raise No_match @@ -840,9 +848,9 @@ let unify_term_binder alp c = DAst.(map (fun b' -> match DAst.get c, b' with | GVar id, GLocalAssum (na', bk', t') -> GLocalAssum (unify_id alp id na', bk', t') - | _, GLocalPattern ((p',ids), id, bk', t') -> + | _, GLocalPattern (([p'],ids), id, bk', t') -> let p = pat_binder_of_term c in - GLocalPattern ((unify_pat alp p p',ids), id, bk', t') + GLocalPattern (([unify_pat alp p p'],ids), id, bk', t') | _ -> raise No_match)) let rec unify_terms_binders alp cl bl' = @@ -895,23 +903,23 @@ let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) let pat = try force_cases_pattern (cases_pattern_of_glob_constr Anonymous c) with Not_found -> raise No_match in try (* If already bound to a binder, unify the term and the binder *) - let pat' = Id.List.assoc var binders in - let pat'' = unify_pat alp pat pat' in - if pat' == pat'' then sigma + let 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 pat'' - with Not_found -> add_binding_env alp sigma var pat + add_binding_env 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 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 pat' = Id.List.assoc var binders in - let alp, pat = unify_pat_upto alp pat pat' in + let disjpat' = Id.List.assoc var binders 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 pat - with Not_found -> alp, add_binding_env alp sigma var pat + 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 @@ -955,7 +963,7 @@ let match_opt f sigma t1 t2 = match (t1,t2) with let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (na1,Name id2) when is_onlybinding_meta id2 metas -> - bind_binding_env alp sigma id2 (DAst.make (PatVar na1)) + bind_binding_env alp sigma id2 [DAst.make (PatVar na1)] | (Name id1,Name id2) when is_term_meta id2 metas -> (* We let the non-binding occurrence define the rhs and hence reason up to *) (* alpha-conversion for the given occurrence of the name (see #4592)) *) @@ -970,7 +978,7 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with let rec match_cases_pattern_binders metas (alp,sigma as acc) pat1 pat2 = match DAst.get pat1, DAst.get pat2 with | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta id2 metas -> - bind_binding_env alp sigma id2 pat1 + bind_binding_env alp sigma id2 [pat1] | PatVar na1, PatVar na2 -> match_names metas acc na1 na2 | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2) when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) -> @@ -1205,18 +1213,27 @@ and match_binders u alp metas na1 na2 sigma b1 b2 = and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = (* Match binders which can be substituted by a pattern *) + let store, get = set_temporary_memory () in match na1, DAst.get b1, na2 with (* Matching individual binders as part of a recursive pattern *) - | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id - when is_gvar p e && is_bindinglist_meta id metas -> - let cp = if occur_glob_constr p b1 then set_pat_alias p cp else cp in - let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in + | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id + when is_gvar p e && is_bindinglist_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 -> + (match get () with + | [(_,(ids,disj_of_patl,b1))] -> + let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in + let disjpat = if occur_glob_constr p b1 then List.map (set_pat_alias p) disjpat else disjpat in + let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((disjpat,ids),p,bk,t)] in match_in u alp metas sigma b1 b2 - | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(_,[cp],b1))]), Name id - when is_gvar p e && is_onlybinding_pattern_like_meta id metas -> - let cp = if occur_glob_constr p b1 then set_pat_alias p cp else cp in - let alp,sigma = bind_binding_env alp sigma id cp in + | _ -> assert false) + | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id + when is_gvar p e && is_onlybinding_pattern_like_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 -> + (match get () with + | [(_,(ids,disj_of_patl,b1))] -> + let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in + let disjpat = if occur_glob_constr p b1 then List.map (set_pat_alias p) disjpat else disjpat in + let alp,sigma = bind_binding_env alp sigma id disjpat in match_in u alp metas sigma b1 b2 + | _ -> assert false) | _, _, Name id when is_bindinglist_meta id metas && (not isprod || na1 != Anonymous)-> let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t)] in match_in u alp metas sigma b1 b2 @@ -1243,8 +1260,11 @@ let match_notation_constr u c (metas,pat) = let term = try Id.List.assoc x terms with Not_found -> raise No_match in ((term, scl)::terms',termlists',binders',binderlists') | NtnTypeBinder NtnParsedAsConstr -> - let v = glob_constr_of_cases_pattern (Id.List.assoc x binders) in - ((v,scl)::terms',termlists',binders',binderlists') + (match Id.List.assoc x binders with + | [pat] -> + let v = glob_constr_of_cases_pattern pat in + ((v,scl)::terms',termlists',binders',binderlists') + | _ -> raise No_match) | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) -> (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists') | NtnTypeConstrList -> diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 1a2dfc9cac..746f52e485 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -34,10 +34,10 @@ val notation_constr_of_glob_constr : notation_interp_env -> (** Re-interpret a notation as a [glob_constr], taking care of binders *) val apply_cases_pattern : ?loc:Loc.t -> - (Id.t list * cases_pattern) * Id.t -> glob_constr -> glob_constr + (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) * Id.t) option * Name.t) -> + ('a -> Name.t -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t) -> ('a -> notation_constr -> glob_constr) -> 'a -> notation_constr -> glob_constr @@ -52,7 +52,7 @@ exception No_match val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> ('a glob_constr_g * subscopes) list * ('a glob_constr_g list * subscopes) list * - ('a cases_pattern_g * subscopes) list * + ('a cases_pattern_disjunction_g * subscopes) list * ('a extended_glob_local_binder_g list * subscopes) list val match_notation_constr_cases_pattern : -- cgit v1.2.3 From 5806b0476a1ac9b903503641cc3e2997d3e8d960 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 24 Aug 2017 15:18:23 +0200 Subject: When printing a notation with "match", more flexibility in matching equations. We reason up to order, and accept to match a final catch-all clauses with any other clause. This allows for instance to parse and print a notation of the form "if t is S n then p else q". --- interp/notation_ops.ml | 33 +++++++++++++++++++++++++-------- 1 file changed, 25 insertions(+), 8 deletions(-) (limited to 'interp') diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 81cdecf03d..44073c3b5e 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -975,14 +975,15 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match -let rec match_cases_pattern_binders metas (alp,sigma as acc) pat1 pat2 = +let rec match_cases_pattern_binders allow_catchall metas (alp,sigma as acc) pat1 pat2 = match DAst.get pat1, DAst.get pat2 with | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta id2 metas -> bind_binding_env alp sigma id2 [pat1] | PatVar na1, PatVar na2 -> match_names metas acc na1 na2 + | _, PatVar Anonymous when allow_catchall -> acc | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2) when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) -> - List.fold_left2 (match_cases_pattern_binders metas) + List.fold_left2 (match_cases_pattern_binders false metas) (match_names metas acc na1 na2) patl1 patl2 | _ -> raise No_match @@ -1129,9 +1130,7 @@ let rec match_ inner u alp metas sigma a1 a2 = match_binders u alp metas na1 na2 (match_in u alp metas (match_in u alp metas sigma b1 b2) t1 t2) c1 c2 | GCases (sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2) - when sty1 == sty2 - && Int.equal (List.length tml1) (List.length tml2) - && Int.equal (List.length eqnl1) (List.length eqnl2) -> + when sty1 == sty2 && Int.equal (List.length tml1) (List.length tml2) -> let rtno1' = abstract_return_type_context_glob_constr tml1 rtno1 in let rtno2' = abstract_return_type_context_notation_constr tml2 rtno2 in let sigma = @@ -1141,7 +1140,14 @@ let rec match_ inner u alp metas sigma a1 a2 = let sigma = List.fold_left2 (fun s (tm1,_) (tm2,_) -> match_in u alp metas s tm1 tm2) sigma tml1 tml2 in - List.fold_left2_set No_match (match_equations u alp metas) sigma eqnl1 eqnl2 + (* Try two different strategies for matching clauses *) + (try + List.fold_left2_set No_match (match_equations u alp metas) sigma eqnl1 eqnl2 + with + No_match -> + List.fold_left2_set No_match (match_disjunctive_equations u alp metas) sigma + (Detyping.factorize_eqns eqnl1) + (List.map (fun (patl,rhs) -> ([patl],rhs)) eqnl2)) | GLetTuple (nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2) when Int.equal (List.length nal1) (List.length nal2) -> let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in @@ -1241,14 +1247,25 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in match_in u alp metas sigma b1 b2 -and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) = +and match_equations u alp metas sigma (_,(ids,patl1,rhs1)) (patl2,rhs2) rest1 rest2 = (* patl1 and patl2 have the same length because they respectively correspond to some tml1 and tml2 that have the same length *) + let allow_catchall = (rest2 = [] && ids = []) in let (alp,sigma) = - List.fold_left2 (match_cases_pattern_binders metas) + List.fold_left2 (match_cases_pattern_binders allow_catchall metas) (alp,sigma) patl1 patl2 in match_in u alp metas sigma rhs1 rhs2 +and match_disjunctive_equations u alp metas sigma (_,(ids,disjpatl1,rhs1)) (disjpatl2,rhs2) _ _ = + (* patl1 and patl2 have the same length because they respectively + correspond to some tml1 and tml2 that have the same length *) + let (alp,sigma) = + List.fold_left2_set No_match + (fun alp_sigma patl1 patl2 _ _ -> + List.fold_left2 (match_cases_pattern_binders false metas) alp_sigma patl1 patl2) + (alp,sigma) disjpatl1 disjpatl2 in + match_in u alp metas sigma rhs1 rhs2 + let match_notation_constr u c (metas,pat) = let terms,termlists,binders,binderlists = match_ false u ([],[]) metas ([],[],[],[]) c pat in -- cgit v1.2.3 From b176959335a8cc097c254ea10b910e8ecbcde54b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 24 Aug 2017 21:14:43 +0200 Subject: More flexibility in locating or referring to a notation. We generalize the possibility to refer to a notation not only by its "_ U _" form but also using its "a 'U' b". (Wish from EJGA) --- interp/notation.ml | 59 +++++++++++++++++++++++++++++++++++++++++++++++++++-- interp/notation.mli | 4 ++++ 2 files changed, 61 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/notation.ml b/interp/notation.ml index e2e769d2fc..c1b66f7d61 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -945,8 +945,63 @@ let factorize_entries = function (ntn,[c],[]) l in (ntn,l_of_ntn)::rest +type symbol_token = WhiteSpace of int | String of string + +let split_notation_string str = + let push_token beg i l = + if Int.equal beg i then l else + let s = String.sub str beg (i - beg) in + String s :: l + in + let push_whitespace beg i l = + if Int.equal beg i then l else WhiteSpace (i-beg) :: l + in + let rec loop beg i = + if i < String.length str then + if str.[i] == ' ' then + push_token beg i (loop_on_whitespace (i+1) (i+1)) + else + loop beg (i+1) + else + push_token beg i [] + and loop_on_whitespace beg i = + if i < String.length str then + if str.[i] != ' ' then + push_whitespace beg i (loop i (i+1)) + else + loop_on_whitespace beg (i+1) + else + push_whitespace beg i [] + in + loop 0 0 + +let rec raw_analyze_notation_tokens = function + | [] -> [] + | String ".." :: sl -> NonTerminal Notation_ops.ldots_var :: raw_analyze_notation_tokens sl + | String "_" :: _ -> user_err Pp.(str "_ must be quoted.") + | String x :: sl when Id.is_valid x -> + NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl + | String s :: sl -> + Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl + | WhiteSpace n :: sl -> + Break n :: raw_analyze_notation_tokens sl + +let decompose_raw_notation ntn = raw_analyze_notation_tokens (split_notation_string ntn) + +let possible_notations ntn = + (* We collect the possible interpretations of a notation string depending on whether it is + in "x 'U' y" or "_ U _" format *) + let toks = split_notation_string ntn in + if List.exists (function String "_" -> true | _ -> false) toks then + (* Only "_ U _" format *) + [ntn] + else + let ntn' = make_notation_key (raw_analyze_notation_tokens toks) in + if String.equal ntn ntn' then (* Only symbols *) [ntn] else [ntn;ntn'] + let browse_notation strict ntn map = - let find ntn' = + let ntns = possible_notations ntn in + let find ntn' ntn = if String.contains ntn ' ' then String.equal ntn ntn' else let toks = decompose_notation_key ntn' in @@ -959,7 +1014,7 @@ let browse_notation strict ntn map = String.Map.fold (fun scope_name sc -> String.Map.fold (fun ntn { not_interp = (_, r); not_location = df } l -> - if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations) + if List.exists (find ntn) ntns then (ntn,(scope_name,r,df))::l else l) sc.notations) map [] in List.sort (fun x y -> String.compare (fst x) (fst y)) l diff --git a/interp/notation.mli b/interp/notation.mli index d100122129..a4c79d6d35 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -183,9 +183,13 @@ type symbol = val symbol_eq : symbol -> symbol -> bool +(** Make/decompose a notation of the form "_ U _" *) val make_notation_key : symbol list -> notation val decompose_notation_key : notation -> symbol list +(** Decompose a notation of the form "a 'U' b" *) +val decompose_raw_notation : string -> symbol list + (** Prints scopes (expects a pure aconstr printer) *) val pr_scope_class : scope_class -> Pp.t val pr_scope : (glob_constr -> Pp.t) -> scope_name -> Pp.t -- cgit v1.2.3 From 8f93f9a2df6e17386f46f79b2a7eda4104d0a94e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 25 Nov 2017 17:09:21 +0100 Subject: Notations: A step in cleaning constr_entry_key. - Avoid dummy use of unit - Do not decide as early as parsing the default level for pattern - Prepare to further extensions --- interp/notation.ml | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) (limited to 'interp') diff --git a/interp/notation.ml b/interp/notation.ml index c1b66f7d61..13ff960f64 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -91,22 +91,25 @@ let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with | NumLevel n1, NumLevel n2 -> Int.equal n1 n2 | (NextLevel | NumLevel _), _ -> false *) -let constr_entry_key_eq v1 v2 = match v1, v2 with +let constr_entry_key_eq eq v1 v2 = match v1, v2 with | ETName, ETName -> true | ETReference, ETReference -> true | ETBigint, ETBigint -> true | ETBinder b1, ETBinder b2 -> b1 == b2 -| ETConstr (n1,pp1), ETConstr (n2,pp2) -> production_level_eq n1 n2 && production_position_eq pp1 pp2 -| ETPattern n1, ETPattern n2 -> Int.equal n1 n2 +| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2 +| ETPattern n1, ETPattern n2 -> Option.equal Int.equal n1 n2 | ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2' | (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _), _ -> false -let level_eq (l1, t1, u1) (l2, t2, u2) = - let tolerability_eq (i1, r1) (i2, r2) = - Int.equal i1 i2 && parenRelation_eq r1 r2 - in +let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) = + let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in + let prod_eq (l1,pp1) (l2,pp2) = + if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2 + else production_level_eq l1 l2 in Int.equal l1 l2 && List.equal tolerability_eq t1 t2 - && List.equal constr_entry_key_eq u1 u2 + && List.equal (constr_entry_key_eq prod_eq) u1 u2 + +let level_eq = level_eq_gen false let declare_scope scope = try let _ = String.Map.find scope !scope_map in () -- cgit v1.2.3 From dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 25 Nov 2017 20:50:03 +0100 Subject: Notations: Adding modifiers to tell which kind of binder a constr can parse. Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x|P} and {'pat|P}. --- interp/constrintern.ml | 75 ++++++++++++++++++++++++++++++++++++-------------- interp/notation.ml | 13 +++++---- interp/notation_ops.ml | 28 ++++++++++++++----- 3 files changed, 83 insertions(+), 33 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 379d09e895..158ac24b2e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -549,6 +549,18 @@ let is_var store pat = | PatVar na -> store na; true | _ -> false +let out_var pat = + match pat.CAst.v with + | CPatAtom (Some (Ident (_,id))) -> Name id + | CPatAtom None -> Anonymous + | _ -> assert false + +let term_of_name = function + | Name id -> DAst.make (GVar id) + | Anonymous -> + let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in + DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), Misctypes.IntroAnonymous, None)) + let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function | Anonymous -> (renaming,env), None, Anonymous | Name id -> @@ -564,13 +576,21 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam with Not_found -> try (* Trying to associate a pattern *) - let pat,scopes = Id.Map.find id binders in + let pat,(onlyident,scopes) = Id.Map.find id binders in let env = set_env_scopes env scopes in - let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in - let pat, na = match disjpat with - | [pat] when is_var store pat -> let na = get () in None, na - | _ -> Some ((List.map snd ids,disjpat),id), snd na in - (renaming,env), pat, na + if onlyident then + (* Do not try to interpret a variable as a constructor *) + let na = out_var pat in + let env = push_name_env ntnvars (Variable,[],[],[]) env (pat.CAst.loc, na) in + (renaming,env), None, na + else + (* Interpret as a pattern *) + let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in + let pat, na = + match disjpat with + | [pat] when is_var store pat -> let na = get () in None, na + | _ -> Some ((List.map snd ids,disjpat),id), snd na in + (renaming,env), pat, na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -688,12 +708,15 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let gc = intern nenv c in (gc, Some c) in - let mk_env' (c, (tmp_scope, subscopes)) = + let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in - let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in - match disjpat with - | [pat] -> (glob_constr_of_cases_pattern pat, None) - | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.CAst.loc () + if onlyident then + let na = out_var c in term_of_name na, None + else + let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in + match disjpat with + | [pat] -> (glob_constr_of_cases_pattern pat, None) + | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.CAst.loc () in let terms = Id.Map.map mk_env terms in let binders = Id.Map.map mk_env' binders in @@ -744,15 +767,18 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = scopes = subscopes @ env.scopes} a with Not_found -> try - let pat,scopes = Id.Map.find id binders in + let pat,(onlyident,scopes) = Id.Map.find id binders in let env = set_env_scopes env scopes in (* We deactivate impls to avoid the check on hidden parameters *) (* and since we are only interested in the pattern as a term *) let env = reset_hidden_inductive_implicit_test env in - let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in - match disjpat with - | [pat] -> glob_constr_of_cases_pattern pat - | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.") + if onlyident then + term_of_name (out_var pat) + else + let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in + match disjpat with + | [pat] -> glob_constr_of_cases_pattern pat + | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.") with Not_found -> try match binderopt with @@ -774,6 +800,10 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = into a substitution for interpretation and based on binding/constr distinction *) +let cases_pattern_of_name (loc,na) = + let atom = match na with Name id -> Some (Ident (loc,id)) | Anonymous -> None in + CAst.make ?loc (CPatAtom atom) + let split_by_type ids subst = let bind id scl l s = match l with @@ -785,12 +815,17 @@ let split_by_type ids subst = | NtnTypeConstr -> let terms,terms' = bind id scl terms terms' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnParsedAsConstr -> + | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.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 + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') + | NtnTypeBinder NtnBinderParsedAsConstr Extend.AsIdent -> 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,scl) binders' in + let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) -> - let binders,binders' = bind id scl binders binders' in + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ 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') | NtnTypeConstrList -> let termlists,termlists' = bind id scl termlists termlists' in diff --git a/interp/notation.ml b/interp/notation.ml index 13ff960f64..ea7ef21b19 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -97,9 +97,10 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with | ETBigint, ETBigint -> true | ETBinder b1, ETBinder b2 -> b1 == b2 | ETConstr lev1, ETConstr lev2 -> eq lev1 lev2 -| ETPattern n1, ETPattern n2 -> Option.equal Int.equal n1 n2 +| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2 +| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 | ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2' -| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _), _ -> false +| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) = let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in @@ -626,10 +627,10 @@ let availability_of_prim_token n printer_scope local_scopes = let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 let notation_binder_source_eq s1 s2 = match s1, s2 with - | NtnParsedAsConstr, NtnParsedAsConstr -> true - | NtnParsedAsIdent, NtnParsedAsIdent -> true - | NtnParsedAsPattern, NtnParsedAsPattern -> true - | (NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern), _ -> false +| NtnParsedAsIdent, NtnParsedAsIdent -> true +| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 +| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2 +| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> 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 44073c3b5e..c65f4785ef 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -671,12 +671,20 @@ let is_term_meta id metas = try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false with Not_found -> false +let is_onlybinding_strict_meta id metas = + try match Id.List.assoc id metas with _,NtnTypeBinder (NtnParsedAsPattern true) -> true | _ -> false + with Not_found -> false + let is_onlybinding_meta id metas = try match Id.List.assoc id metas with _,NtnTypeBinder _ -> true | _ -> false with Not_found -> false -let is_onlybinding_pattern_like_meta id metas = - try match Id.List.assoc id metas with _,NtnTypeBinder (NtnParsedAsConstr | NtnParsedAsPattern) -> true | _ -> false +let is_onlybinding_pattern_like_meta isvar id metas = + try match Id.List.assoc id metas with + | _,NtnTypeBinder (NtnBinderParsedAsConstr + (Extend.AsIdentOrPattern | Extend.AsStrictPattern)) -> true + | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar) + | _ -> false with Not_found -> false let is_bindinglist_meta id metas = @@ -962,6 +970,8 @@ let match_opt f sigma t1 t2 = match (t1,t2) with | _ -> raise No_match let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with + | (na1,Name id2) when is_onlybinding_strict_meta id2 metas -> + raise No_match | (na1,Name id2) when is_onlybinding_meta id2 metas -> bind_binding_env alp sigma id2 [DAst.make (PatVar na1)] | (Name id1,Name id2) when is_term_meta id2 metas -> @@ -977,7 +987,9 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with let rec match_cases_pattern_binders allow_catchall metas (alp,sigma as acc) pat1 pat2 = match DAst.get pat1, DAst.get pat2 with - | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta id2 metas -> + | PatVar _, PatVar (Name id2) when is_onlybinding_pattern_like_meta true id2 metas -> + bind_binding_env alp sigma id2 [pat1] + | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta false id2 metas -> bind_binding_env alp sigma id2 [pat1] | PatVar na1, PatVar na2 -> match_names metas acc na1 na2 | _, PatVar Anonymous when allow_catchall -> acc @@ -1093,7 +1105,9 @@ let rec match_ inner u alp metas sigma a1 a2 = match DAst.get a1, a2 with (* Matching notation variable *) | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1 - | r1, NVar id2 when is_onlybinding_pattern_like_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1 + | GVar _, NVar id2 when is_onlybinding_pattern_like_meta true id2 metas -> bind_binding_as_term_env alp sigma id2 a1 + | r1, NVar id2 when is_onlybinding_pattern_like_meta false id2 metas -> bind_binding_as_term_env alp sigma id2 a1 + | GVar _, NVar id2 when is_onlybinding_strict_meta id2 metas -> raise No_match | GVar _, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1 | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1 @@ -1232,7 +1246,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = match_in u alp metas sigma b1 b2 | _ -> assert false) | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id - when is_gvar p e && is_onlybinding_pattern_like_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 -> + when is_gvar p e && is_onlybinding_pattern_like_meta false id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 -> (match get () with | [(_,(ids,disj_of_patl,b1))] -> let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in @@ -1276,13 +1290,13 @@ let match_notation_constr u c (metas,pat) = | NtnTypeConstr -> let term = try Id.List.assoc x terms with Not_found -> raise No_match in ((term, scl)::terms',termlists',binders',binderlists') - | NtnTypeBinder NtnParsedAsConstr -> + | NtnTypeBinder (NtnBinderParsedAsConstr _) -> (match Id.List.assoc x binders with | [pat] -> let v = glob_constr_of_cases_pattern pat in ((v,scl)::terms',termlists',binders',binderlists') | _ -> raise No_match) - | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) -> + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) -> (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists') | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists') -- cgit v1.2.3 From 0c4eea2553d5b3b70d0b5baaf92781a544de83bd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 23 Nov 2017 13:30:36 +0100 Subject: Change default for notations with variables bound to both terms and binders. For compatibility, the default is to parse as ident and not as pattern. --- interp/constrintern.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 158ac24b2e..694bec8972 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -273,8 +273,8 @@ let error_expect_binder_notation_type ?loc id = let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars = try - let isonlybinding,idscopes,typ = Id.Map.find id ntnvars in - if istermvar then isonlybinding := false; + let used_as_binder,idscopes,typ = Id.Map.find id ntnvars in + if not istermvar then used_as_binder := true; let () = if istermvar then (* scopes have no effect on the interpretation of identifiers *) begin match !idscopes with @@ -1997,7 +1997,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | Some gen -> let (ltacvars, ntnvars) = lvar in (* Preventively declare notation variables in ltac as non-bindings *) - Id.Map.iter (fun x (isonlybinding,_,_) -> isonlybinding := false) ntnvars; + Id.Map.iter (fun x (used_as_binder,_,_) -> used_as_binder := false) ntnvars; let ntnvars = Id.Map.domain ntnvars in let extra = ltacvars.ltac_extra in let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in @@ -2302,7 +2302,7 @@ let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = (* [vl] is intended to remember the scope of the free variables of [a] *) - let vl = Id.Map.map (fun typ -> (ref true, ref None, typ)) nenv.ninterp_var_type in + let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in let c = internalize (Global.env()) {ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impls} @@ -2313,8 +2313,8 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l in let unused = match reversible with NonInjective ids -> ids | _ -> [] in - let vars = Id.Map.mapi (fun id (isonlybinding, sc, typ) -> - (!isonlybinding && not (List.mem_f Id.equal id unused), out_scope !sc)) vl in + let vars = Id.Map.mapi (fun id (used_as_binder, sc, typ) -> + (!used_as_binder && not (List.mem_f Id.equal id unused), out_scope !sc)) vl in (* Returns [a] and the ordered list of variables with their scopes *) vars, a, reversible -- cgit v1.2.3