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 +++++++++---------- intf/constrexpr.ml | 7 +-- plugins/funind/glob_term_to_relation.ml | 8 ++-- plugins/funind/indfun.ml | 34 +++++++------- plugins/ltac/g_tactic.ml4 | 6 ++- plugins/ltac/pptactic.ml | 7 +-- plugins/ssr/ssrcommon.ml | 6 +-- plugins/ssr/ssrparser.ml4 | 22 ++++----- plugins/ssrmatching/ssrmatching.ml4 | 2 +- pretyping/cases.ml | 5 -- pretyping/glob_ops.ml | 5 ++ pretyping/glob_ops.mli | 2 + printing/ppconstr.ml | 68 +-------------------------- printing/ppconstr.mli | 8 ---- test-suite/output/PatternsInBinders.out | 2 +- 17 files changed, 135 insertions(+), 240 deletions(-) diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index da04d8786..9fe890e90 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 4f7d537d3..ef20086e6 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 2761b6528..7276b917f 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 diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index fbf9e248a..2575b71ea 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -70,8 +70,8 @@ and constr_expr_r = | CRef of reference * instance_expr option | CFix of Id.t Loc.located * fix_expr list | CCoFix of Id.t Loc.located * cofix_expr list - | CProdN of binder_expr list * constr_expr - | CLambdaN of binder_expr list * constr_expr + | CProdN of local_binder_expr list * constr_expr + | CLambdaN of local_binder_expr list * constr_expr | CLetIn of Name.t Loc.located * constr_expr * constr_expr option * constr_expr | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list | CApp of (proj_flag * constr_expr) * @@ -107,9 +107,6 @@ and case_expr = constr_expr (* expression that is being matched and branch_expr = (cases_pattern_expr list list * constr_expr) Loc.located -and binder_expr = - Name.t Loc.located list * binder_kind * constr_expr - and fix_expr = Id.t Loc.located * (Id.t Loc.located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index f7639d22d..693ab464d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1295,8 +1295,8 @@ let rec rebuild_return_type rt = CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t') | Constrexpr.CLetIn(na,v,t,t') -> CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') - | _ -> CAst.make ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous], - Constrexpr.Default Decl_kinds.Explicit, rt], + | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([Loc.tag Anonymous], + Constrexpr.Default Decl_kinds.Explicit, rt)], CAst.make @@ Constrexpr.CSort(GType [])) let do_build_inductive @@ -1356,7 +1356,7 @@ let do_build_inductive acc) | None -> CAst.make @@ Constrexpr.CProdN - ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], acc ) ) @@ -1423,7 +1423,7 @@ let do_build_inductive acc) | None -> CAst.make @@ Constrexpr.CProdN - ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], acc ) ) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 58154d310..96e4a94d3 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -591,11 +591,11 @@ and rebuild_nal aux bk bl' nal typ = match nal,typ with | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ | [], _ -> rebuild_bl aux bl' typ - | na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } -> + | na::nal,{ CAst.v = CProdN(CLocalAssum(na'::nal',bk',nal't)::rest,typ') } -> if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na') then let assum = CLocalAssum([na],bk,nal't) in - let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in + let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in rebuild_nal (assum::aux) bk @@ -604,7 +604,7 @@ and rebuild_nal aux bk bl' nal typ = (CAst.make @@ CProdN(new_rest,typ')) else let assum = CLocalAssum([na'],bk,nal't) in - let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in + let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in rebuild_nal (assum::aux) bk @@ -731,10 +731,14 @@ let rec add_args id new_args = CAst.map (function end | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.") | CProdN(nal,b1) -> - CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, + CProdN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) + | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t) + | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal, add_args id new_args b1) | CLambdaN(nal,b1) -> - CLambdaN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, + CLambdaN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) + | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t) + | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal, add_args id new_args b1) | CLetIn(na,b1,t,b2) -> CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) @@ -793,7 +797,7 @@ let rec chop_n_arrow n t = then t (* If we have already removed all the arrows then return the type *) else (* If not we check the form of [t] *) match t.CAst.v with - | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible : + | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, two results are possible : either we need to discard more than the number of arrows contained in this product declaration then we just recall [chop_n_arrow] on the remaining number of arrow to chop and [t'] we discard it and @@ -805,7 +809,7 @@ let rec chop_n_arrow n t = let new_n = let rec aux (n:int) = function [] -> n - | (nal,k,t'')::nal_ta' -> + | CLocalAssum(nal,k,t'')::nal_ta' -> let nal_l = List.length nal in if n >= nal_l then @@ -813,9 +817,10 @@ let rec chop_n_arrow n t = else let new_t' = CAst.make @@ Constrexpr.CProdN( - ((snd (List.chop n nal)),k,t'')::nal_ta',t') + CLocalAssum((snd (List.chop n nal)),k,t'')::nal_ta',t') in raise (Stop new_t') + | _ -> anomaly (Pp.str "Not enough products.") in aux n nal_ta' in @@ -828,16 +833,13 @@ let rec chop_n_arrow n t = let rec get_args b t : Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr = match b.CAst.v with - | Constrexpr.CLambdaN ((nal_ta), b') -> + | Constrexpr.CLambdaN (CLocalAssum(nal,k,ta) as d::rest, b') -> begin - let n = - (List.fold_left (fun n (nal,_,_) -> - n+List.length nal) 0 nal_ta ) - in - let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in - (List.map (fun (nal,k,ta) -> - (Constrexpr.CLocalAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' + let n = List.length nal in + let nal_tas,b'',t'' = get_args (CAst.make ?loc:b.CAst.loc @@ Constrexpr.CLambdaN (rest,b')) (chop_n_arrow n t) in + d :: nal_tas, b'',t'' end + | Constrexpr.CLambdaN ([], b) -> [],b,t | _ -> [],b,t diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index d792d4ff7..e68140828 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -115,10 +115,11 @@ let mk_fix_tac (loc,id,bl,ann,ty) = match bl,ann with [([_],_,_)], None -> 1 | _, Some x -> - let ids = List.map snd (List.flatten (List.map pi1 bl)) in + let ids = List.map snd (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in (try List.index Names.Name.equal (snd x) ids with Not_found -> user_err Pp.(str "No such fix variable.")) | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in + let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in (id,n, CAst.make ~loc @@ CProdN(bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = @@ -126,6 +127,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) = user_err ~loc:aloc ~hdr:"Constr:mk_cofix_tac" (Pp.str"Annotation forbidden in cofix expression.")) ann in + let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in (id,CAst.make ~loc @@ CProdN(bl,ty)) (* Functions overloaded by quotifier *) @@ -160,7 +162,7 @@ let mkTacCase with_evar = function let rec mkCLambdaN_simple_loc ?loc bll c = match bll with | ((loc1,_)::_ as idl,bk,t) :: bll -> - CAst.make ?loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) + CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c | [] -> c diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index e5ff47356..4f430b79e 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -353,9 +353,10 @@ let string_of_genarg_arg (ArgumentType arg) = let rec strip_ty acc n ty = match ty.CAst.v with Constrexpr.CProdN(bll,a) -> - let nb = - List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in - let bll = List.map (fun (x, _, y) -> x, y) bll in + let bll = List.map (function + | CLocalAssum (nal,_,t) -> nal,t + | _ -> user_err Pp.(str "Cannot translate fix tactic: not only products")) bll in + let nb = List.fold_left (fun i (nal,t) -> i + List.length nal) 0 bll in if nb >= n then (List.rev (bll@acc)), a else strip_ty (bll@acc) (n-nb) a | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 9822da1c7..499154d50 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -835,9 +835,9 @@ let rec mkCHoles ?loc n = if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ - CLambdaN ([[loc, name], Default Explicit, ty], t) + CLambdaN ([CLocalAssum([loc, name], Default Explicit, ty)], t) let mkCArrow ?loc ty t = CAst.make ?loc @@ - CProdN ([[Loc.tag Anonymous], Default Explicit, ty], t) + CProdN ([CLocalAssum([Loc.tag Anonymous], Default Explicit, ty)], t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv ty) let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = [] @@ -855,7 +855,7 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty = | _, (_, Some ty) -> let rec force_type ty = CAst.(map (function | CProdN (abs, t) -> - n_binders := !n_binders + List.length (List.flatten (List.map pi1 abs)); + n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern (_,_) -> (* We count a 'pat for 1; TO BE CHECKED *) [Loc.tag Name.Anonymous]) abs)); CProdN (abs, force_type t) | CLetIn (n, v, oty, t) -> incr n_binders; CLetIn (n, v, oty, force_type t) | _ -> (mkCCast ty (mkCType None)).v)) ty in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 46403aef3..211cad3f5 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1023,10 +1023,10 @@ let rec format_local_binders h0 bl0 = match h0, bl0 with | _ -> [] let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with - | BFvar :: h, { v = CLambdaN ([[_, x], _, _], c) } -> + | BFvar :: h, { v = CLambdaN ([CLocalAssum([_, x], _, _)], c) } -> let bs, c' = format_constr_expr h c in Bvar x :: bs, c' - | BFdecl _:: h, { v = CLambdaN ([lxs, _, t], c) } -> + | BFdecl _:: h, { v = CLambdaN ([CLocalAssum(lxs, _, t)], c) } -> let bs, c' = format_constr_expr h c in Bdecl (List.map snd lxs, t) :: bs, c' | BFdef :: h, { v = CLetIn((_, x), v, oty, c) } -> @@ -1165,20 +1165,20 @@ ARGUMENT EXTEND ssrbinder TYPED AS ssrfwdfmt * constr PRINTED BY pr_ssrbinder | [ ssrbvar(bv) ] -> [ let xloc, _ as x = bvar_lname bv in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([[x],Default Explicit,mkCHole xloc],mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ] | [ "(" ssrbvar(bv) ")" ] -> [ let xloc, _ as x = bvar_lname bv in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([[x],Default Explicit,mkCHole xloc],mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ] | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] -> [ let x = bvar_lname bv in (FwdPose, [BFdecl 1]), - CAst.make ~loc @@ CLambdaN ([[x], Default Explicit, t], mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Explicit, t)], mkCHole (Some loc)) ] | [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] -> [ let xs = List.map bvar_lname (bv :: bvs) in let n = List.length xs in (FwdPose, [BFdecl n]), - CAst.make ~loc @@ CLambdaN ([xs, Default Explicit, t], mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Explicit, t)], mkCHole (Some loc)) ] | [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] -> [ (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) ] | [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] -> @@ -1191,7 +1191,7 @@ GEXTEND Gram [ ["of" | "&"]; c = operconstr LEVEL "99" -> let loc = !@loc in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([[Loc.tag ~loc Anonymous],Default Explicit,c],mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum ([Loc.tag ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ] ]; END @@ -1217,7 +1217,7 @@ let push_binders c2 bs = | ct -> loop false ct bs let rec fix_binders = let open CAst in function - | (_, { v = CLambdaN ([xs, _, t], _) } ) :: bs -> + | (_, { v = CLambdaN ([CLocalAssum(xs, _, t)], _) } ) :: bs -> CLocalAssum (xs, Default Explicit, t) :: fix_binders bs | (_, { v = CLetIn (x, v, oty, _) } ) :: bs -> CLocalDef (x, v, oty) :: fix_binders bs @@ -1325,13 +1325,13 @@ let intro_id_to_binder = List.map (function | IPatId id -> let xloc, _ as x = bvar_lname (mkCVar id) in (FwdPose, [BFvar]), - CAst.make @@ CLambdaN ([[x], Default Explicit, mkCHole xloc], + CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)], mkCHole None) | _ -> anomaly "non-id accepted as binder") let binder_to_intro_id = CAst.(List.map (function - | (FwdPose, [BFvar]), { v = CLambdaN ([ids,_,_],_) } - | (FwdPose, [BFdecl _]), { v = CLambdaN ([ids,_,_],_) } -> + | (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } + | (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } -> List.map (function (_, Name id) -> IPatId id | _ -> IPatAnon One) ids | (FwdPose, [BFdef]), { v = CLetIn ((_,Name id),_,_,_) } -> [IPatId id] | (FwdPose, [BFdef]), { v = CLetIn ((_,Anonymous),_,_,_) } -> [IPatAnon One] diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 7d0584a00..17409595a 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -137,7 +137,7 @@ let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c) let isGHole c = match DAst.get c with GHole _ -> true | _ -> false let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ - CLambdaN ([[Loc.tag ?loc name], Default Explicit, ty], t) + CLambdaN ([CLocalAssum([Loc.tag ?loc name], Default Explicit, ty)], t) let mkCLetIn ?loc name bo t = CAst.make ?loc @@ CLetIn ((Loc.tag ?loc name), bo, None, t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 311c1c09e..a0434f927 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -450,11 +450,6 @@ let current_pattern eqn = | pat::_ -> pat | [] -> anomaly (Pp.str "Empty list of patterns.") -let alias_of_pat = DAst.with_val (function - | PatVar name -> name - | PatCstr(_,_,name) -> name - ) - let remove_current_pattern eqn = match eqn.patterns with | pat::pats -> diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index a21137a05..eb8a22a88 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -19,6 +19,11 @@ open Ltac_pretype let cases_pattern_loc c = c.CAst.loc +let alias_of_pat pat = DAst.with_val (function + | PatVar name -> name + | PatCstr(_,_,name) -> name + ) pat + let cases_predicate_names tml = List.flatten (List.map (function | (tm,(na,None)) -> [na] diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 9dd7068cb..c894db18e 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -13,6 +13,8 @@ open Glob_term val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool +val alias_of_pat : 'a cases_pattern_g -> Name.t + val cast_type_eq : ('a -> 'a -> bool) -> 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 1146b42a0..c58d9eb9a 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -394,68 +394,6 @@ let tag_var = tag Tag.variable if is_open then pr_delimited_binders pr_com_at sep pr_c else pr_undelimited_binders sep pr_c - let rec extract_prod_binders = let open CAst in function - (* | CLetIn (loc,na,b,c) as x -> - let bl,c = extract_prod_binders c in - if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) - | { v = CProdN ([],c) } -> - extract_prod_binders c - | { loc; v = CProdN ([[_,Name id],bk,t], - { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} ) } - when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) -> - let bl,c = extract_prod_binders b in - CLocalPattern (loc, (p,None)) :: bl, c - | { loc; v = CProdN ((nal,bk,t)::bl,c) } -> - let bl,c = extract_prod_binders (CAst.make ?loc @@ CProdN(bl,c)) in - CLocalAssum (nal,bk,t) :: bl, c - | c -> [], c - - let rec extract_lam_binders ce = let open CAst in match ce.v with - (* | CLetIn (loc,na,b,c) as x -> - let bl,c = extract_lam_binders c in - if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) - | CLambdaN ([],c) -> - extract_lam_binders c - | CLambdaN ([[_,Name id],bk,t], - { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} ) - when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) -> - let bl,c = extract_lam_binders b in - CLocalPattern (ce.loc,(p,None)) :: bl, c - | CLambdaN ((nal,bk,t)::bl,c) -> - let bl,c = extract_lam_binders (CAst.make ?loc:ce.loc @@ CLambdaN(bl,c)) in - CLocalAssum (nal,bk,t) :: bl, c - | _ -> [], ce - - let split_lambda = CAst.with_loc_val (fun ?loc -> function - | CLambdaN ([[na],bk,t],c) -> (na,t,c) - | CLambdaN (([na],bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN(bl,c)) - | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN((nal,bk,t)::bl,c)) - | _ -> anomaly (Pp.str "ill-formed fixpoint body.") - ) - - let rename na na' t c = - match (na,na') with - | (_,Name id), (_,Name id') -> - (na',t,replace_vars_constr_expr (Id.Map.singleton id id') c) - | (_,Name id), (_,Anonymous) -> (na,t,c) - | _ -> (na',t,c) - - let split_product na' = CAst.with_loc_val (fun ?loc -> function - | CProdN ([[na],bk,t],c) -> rename na na' t c - | CProdN (([na],bk,t)::bl,c) -> rename na na' t (CAst.make ?loc @@ CProdN(bl,c)) - | CProdN ((na::nal,bk,t)::bl,c) -> - rename na na' t (CAst.make ?loc @@ CProdN((nal,bk,t)::bl,c)) - | _ -> anomaly (Pp.str "ill-formed fixpoint body.") - ) - - let rec split_fix n typ def = - if Int.equal n 0 then ([],typ,def) - else - let (na,_,def) = split_lambda def in - let (na,t,typ) = split_product na typ in - let (bl,typ,def) = split_fix (n-1) typ def in - (CLocalAssum ([na],default_binder_kind,t)::bl,typ,def) - let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = let pr_body = if dangling_with_for then pr_dangling else pr in @@ -574,8 +512,7 @@ let tag_var = tag Tag.variable (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix), lfix ) - | CProdN _ -> - let (bl,a) = extract_prod_binders a in + | CProdN (bl,a) -> return ( hov 0 ( hov 2 (pr_delimited_binders pr_forall spc @@ -583,8 +520,7 @@ let tag_var = tag Tag.variable str "," ++ pr spc ltop a), lprod ) - | CLambdaN _ -> - let (bl,a) = extract_lam_binders a in + | CLambdaN (bl,a) -> return ( hov 0 ( hov 2 (pr_delimited_binders pr_fun spc diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 1320cce9b..158906dd2 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -17,14 +17,6 @@ open Names open Misctypes open Notation_term -val extract_lam_binders : - constr_expr -> local_binder_expr list * constr_expr -val extract_prod_binders : - constr_expr -> local_binder_expr list * constr_expr -val split_fix : - int -> constr_expr -> constr_expr -> - local_binder_expr list * constr_expr * constr_expr - val prec_less : precedence -> tolerability -> bool val pr_tight_coma : unit -> Pp.t diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 95be04c32..6b09c3308 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -31,7 +31,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w) : Prop both_z = fun pat : nat * nat => -let '(n, p) as pat0 := pat return (F pat0) in (Z n, Z p) : F (n, p) +let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p) : forall pat : nat * nat, F pat fun '(x, y) '(z, t) => swap (x, y) = (z, t) : A * B -> B * A -> Prop -- cgit v1.2.3