diff options
-rw-r--r-- | CHANGES | 3 | ||||
-rw-r--r-- | doc/refman/RefMan-gal.tex | 4 | ||||
-rw-r--r-- | ide/texmacspp.ml | 3 | ||||
-rw-r--r-- | interp/constrexpr_ops.ml | 91 | ||||
-rw-r--r-- | interp/constrexpr_ops.mli | 5 | ||||
-rw-r--r-- | interp/constrextern.ml | 17 | ||||
-rw-r--r-- | interp/constrintern.ml | 182 | ||||
-rw-r--r-- | interp/implicit_quantifiers.ml | 1 | ||||
-rw-r--r-- | interp/notation_ops.ml | 33 | ||||
-rw-r--r-- | interp/notation_ops.mli | 5 | ||||
-rw-r--r-- | interp/topconstr.ml | 8 | ||||
-rw-r--r-- | intf/constrexpr.mli | 8 | ||||
-rw-r--r-- | parsing/g_constr.ml4 | 15 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 16 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 3 | ||||
-rw-r--r-- | printing/ppconstr.ml | 38 | ||||
-rw-r--r-- | test-suite/output/Binder.out | 8 | ||||
-rw-r--r-- | test-suite/output/Binder.v | 7 | ||||
-rw-r--r-- | toplevel/command.ml | 1 | ||||
-rw-r--r-- | toplevel/record.ml | 3 |
20 files changed, 374 insertions, 77 deletions
@@ -6,6 +6,9 @@ Specification language - Giving implicit arguments explicitly to a constant with multiple choices of implicit arguments does not break any more insertion of further maximal implicit arguments. +- Ability to put any pattern in binders, prefixed by quote, e.g. + "fun '(a,b) => ...", "λ '(a,(b,c)), ...", "Definition foo '(x,y) := ...". + It expands into a "let 'pattern := ..." Tactics diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index fcccd9cb4..99eee44e0 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -273,6 +273,7 @@ called \CIC). The formal presentation of {\CIC} is given in Chapter {\binder} & ::= & {\name} & (\ref{Binders}) \\ & $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\ & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\ + & $|$ & {\tt '} {\pattern} &\\ & & &\\ {\name} & ::= & {\ident} &\\ & $|$ & {\tt \_} &\\ @@ -410,7 +411,8 @@ bound variable cannot be synthesized by the system, it can be specified with the notation {\tt (}\,{\ident}\,{\tt :}\,{\type}\,{\tt )}. There is also a notation for a sequence of binding variables sharing the same type: {\tt (}\,{\ident$_1$}\ldots{\ident$_n$}\,{\tt -:}\,{\type}\,{\tt )}. +:}\,{\type}\,{\tt )}. A binder can also be any pattern prefixed by a quote, +e.g. {\tt '(x,y)}. Some constructions allow the binding of a variable to value. This is called a ``let-binder''. The entry {\binder} of the grammar accepts diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index f445f2e08..53a29008a 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -238,6 +238,8 @@ and pp_local_binder lb = (* don't know what it is for now *) let ppl = List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in xmlTyped (ppl @ [pp_expr ce]) + | LocalPattern _ -> + assert false and pp_local_decl_expr lde = (* don't know what it is for now *) match lde with | AssumExpr (_, ce) -> pp_expr ce @@ -351,6 +353,7 @@ and pp_cases_pattern_expr cpe = xmlApply loc (xmlOperator "delimiter" ~attr:["name", delim] loc :: [pp_cases_pattern_expr cpe]) + | CPatCast _ -> assert false and pp_case_expr (e, name, pat) = match name, pat with | None, None -> xmlScrutinee [pp_expr e] diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index c5730e626..f49ed9a5f 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -40,7 +40,7 @@ let names_of_local_assums bl = List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl) let names_of_local_binders bl = - List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl) + List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalPattern _ -> assert false) bl) (**********************************************************************) (* Functions on constr_expr *) @@ -260,6 +260,7 @@ let cases_pattern_expr_loc = function | CPatRecord (loc, _) -> loc | CPatPrim (loc,_) -> loc | CPatDelimiters (loc,_,_) -> loc + | CPatCast(loc,_,_) -> loc let raw_cases_pattern_expr_loc = function | RCPatAlias (loc,_,_) -> loc @@ -271,6 +272,7 @@ let local_binder_loc = function | LocalRawAssum ((loc,_)::_,_,t) | LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t) | LocalRawAssum ([],_,_) -> assert false + | LocalPattern (loc,_,_) -> loc let local_binders_loc bll = match bll with | [] -> Loc.ghost @@ -292,23 +294,74 @@ let mkAppC (f,l) = | CApp (_,g,l') -> CApp (Loc.ghost, g, l' @ l) | _ -> CApp (Loc.ghost, (None, f), l) -let rec mkCProdN loc bll c = - match bll with - | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> - CProdN (loc,[idl,bk,t],mkCProdN (Loc.merge loc1 loc) bll c) - | LocalRawDef ((loc1,_) as id,b) :: bll -> - CLetIn (loc,id,b,mkCProdN (Loc.merge loc1 loc) bll c) - | [] -> c - | LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c - -let rec mkCLambdaN loc bll c = - match bll with - | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> - CLambdaN (loc,[idl,bk,t],mkCLambdaN (Loc.merge loc1 loc) bll c) - | LocalRawDef ((loc1,_) as id,b) :: bll -> - CLetIn (loc,id,b,mkCLambdaN (Loc.merge loc1 loc) bll c) - | [] -> c - | LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c +let add_name_in_env env n = + match snd n with + | Anonymous -> env + | Name id -> id :: env + +let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) () + +let expand_pattern_binders mkC bl c = + let rec loop bl c = + match bl with + | [] -> ([], [], c) + | b :: bl -> + let (env, bl, c) = loop bl c in + match b with + | LocalRawDef (n, _) -> + let env = add_name_in_env env n in + (env, b :: bl, c) + | LocalRawAssum (nl, _, _) -> + let env = List.fold_left add_name_in_env env nl in + (env, b :: bl, c) + | LocalPattern (loc, p, ty) -> + let ni = Hook.get fresh_var env c in + let id = (loc, Name ni) in + let b = + LocalRawAssum + ([id], Default Explicit, + match ty with + | Some ty -> ty + | None -> CHole (loc, None, IntroAnonymous, None)) + in + let e = CRef (Libnames.Ident (loc, ni), None) in + let c = + CCases + (loc, LetPatternStyle, None, [(e,None,None)], + [(loc, [(loc,[p])], mkC loc bl c)]) + in + (ni :: env, [b], c) + in + let (_, bl, c) = loop bl c in + (bl, c) + +let mkCProdN loc bll c = + let rec loop loc bll c = + match bll with + | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> + CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c) + | LocalRawDef ((loc1,_) as id,b) :: bll -> + CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c) + | [] -> c + | LocalRawAssum ([],_,_) :: bll -> loop loc bll c + | LocalPattern (loc,p,ty) :: bll -> assert false + in + let (bll, c) = expand_pattern_binders loop bll c in + loop loc bll c + +let mkCLambdaN loc bll c = + let rec loop loc bll c = + match bll with + | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> + CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c) + | LocalRawDef ((loc1,_) as id,b) :: bll -> + CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c) + | [] -> c + | LocalRawAssum ([],_,_) :: bll -> loop loc bll c + | LocalPattern (loc,p,ty) :: bll -> assert false + in + let (bll, c) = expand_pattern_binders loop bll c in + loop loc bll c let rec abstract_constr_expr c = function | [] -> c @@ -316,6 +369,7 @@ let rec abstract_constr_expr c = function | LocalRawAssum (idl,bk,t)::bl -> List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl (abstract_constr_expr c bl) + | LocalPattern _::_ -> assert false let rec prod_constr_expr c = function | [] -> c @@ -323,6 +377,7 @@ let rec prod_constr_expr c = function | LocalRawAssum (idl,bk,t)::bl -> List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl (prod_constr_expr c bl) + | LocalPattern _::_ -> assert false let coerce_reference_to_id = function | Ident (_,id) -> id diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 3f5be4855..a92da035f 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -58,6 +58,11 @@ val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr (** Same as [prod_constr_expr], with location *) +val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t +val expand_pattern_binders : + (Loc.t -> local_binder list -> constr_expr -> constr_expr) -> + local_binder list -> constr_expr -> local_binder list * constr_expr + (** {6 Destructors}*) val coerce_reference_to_id : reference -> Id.t diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 82fa85f69..99b229251 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -765,6 +765,7 @@ let rec extern inctx scopes vars r = let listdecl = Array.mapi (fun i fi -> let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in + let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) bl in let (assums,ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in @@ -781,7 +782,8 @@ let rec extern inctx scopes vars r = | GCoFix n -> let listdecl = Array.mapi (fun i fi -> - let (_,ids,bl) = extern_local_binder scopes vars blv.(i) in + let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) blv.(i) in + let (_,ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in ((Loc.ghost, fi),bl,extern_typ scopes vars0 tyv.(i), @@ -824,13 +826,13 @@ and factorize_lambda inctx scopes vars na bk aty c = and extern_local_binder scopes vars = function [] -> ([],[],[]) - | (na,bk,Some bd,ty)::l -> + | (Inl na,bk,Some bd,ty)::l -> let (assums,ids,l) = extern_local_binder scopes (name_fold Id.Set.add na vars) l in (assums,na::ids, LocalRawDef((Loc.ghost,na), extern false scopes vars bd) :: l) - | (na,bk,None,ty)::l -> + | (Inl na,bk,None,ty)::l -> let ty = extern_typ scopes vars ty in (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with (assums,ids,LocalRawAssum(nal,k,ty')::l) @@ -843,6 +845,14 @@ and extern_local_binder scopes vars = function (na::assums,na::ids, LocalRawAssum([(Loc.ghost,na)],Default bk,ty) :: l)) + | (Inr p,bk,Some bd,ty)::l -> assert false + + | (Inr p,bk,None,ty)::l -> + let ty = extern_typ scopes vars ty in + let p = extern_cases_pattern vars p in + let (assums,ids,l) = extern_local_binder scopes vars l in + (assums,ids, LocalPattern(Loc.ghost,p,Some ty) :: l) + and extern_eqn inctx scopes vars (loc,ids,pl,c) = (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], extern inctx scopes vars c) @@ -1050,4 +1060,5 @@ let extern_constr_pattern env sigma pat = let extern_rel_context where env sigma sign = let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in let vars = vars_of_env env in + let a = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) a in pi3 (extern_local_binder (None,[]) vars a) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0c02c5dab..ff1fd929b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -369,7 +369,7 @@ let check_hidden_implicit_parameters id impls = errorlabstrm "" (strbrk "A parameter of an inductive type " ++ pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") -let push_name_env ?(global_level=false) lvar implargs env = +let push_name_env ?(global_level=false) ntnvars implargs env = function | loc,Anonymous -> if global_level then @@ -377,7 +377,6 @@ let push_name_env ?(global_level=false) lvar implargs env = env | loc,Name id -> check_hidden_implicit_parameters id env.impls ; - let (_,ntnvars) = lvar in if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var loc; set_var_scope loc id false env ntnvars; @@ -433,14 +432,72 @@ let intern_assumption intern lvar env nal bk ty = let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in env, b +let obj_string x = + if Obj.is_block (Obj.repr x) then + "tag = " ^ string_of_int (Obj.tag (Obj.repr x)) + else "int_val = " ^ string_of_int (Obj.magic x) + +let rec free_vars_of_pat il = + function + | CPatCstr (loc, c, l1, l2) -> + let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in + List.fold_left free_vars_of_pat il l2 + | CPatAtom (loc, ro) -> + begin match ro with + | Some (Ident (loc, i)) -> (loc, i) :: il + | Some _ | None -> il + end + | CPatNotation (loc, n, l1, l2) -> + let il = List.fold_left free_vars_of_pat il (fst l1) in + List.fold_left (List.fold_left free_vars_of_pat) il (snd l1) + | _ -> anomaly (str "free_vars_of_pat") + +let intern_local_pattern intern lvar env p = + List.fold_left + (fun env (loc, i) -> + let bk = Default Implicit in + let ty = CHole (loc, None, Misctypes.IntroAnonymous, None) in + let n = Name i in + let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in + env) + env (free_vars_of_pat [] p) + +type binder_data = + | BDRawDef of (Loc.t * glob_binder) + | BDPattern of + (Loc.t * (cases_pattern * Id.t list) * + (bool ref * + (Notation_term.tmp_scope_name option * + Notation_term.tmp_scope_name list) + option ref * Notation_term.notation_var_internalization_type) + Names.Id.Map.t * + intern_env * constr_expr) + +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 | LocalRawAssum(nal,bk,ty) -> let env, bl' = intern_assumption intern lvar env nal bk ty in + let bl' = List.map (fun a -> BDRawDef a) bl' in env, bl' @ bl | LocalRawDef((loc,na as locna),def) -> let indef = intern env def in (push_name_env lvar (impls_term_list indef) env locna, - (loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)))::bl) + (BDRawDef ((loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)))))::bl) + | LocalPattern (loc,p,ty) -> + let tyc = + match ty with + | Some ty -> ty + | None -> CHole(loc,None,Misctypes.IntroAnonymous,None) + in + let env = intern_local_pattern intern lvar env p in + let cp = + match !intern_cases_pattern_fwd (None,env.scopes) p with + | (_, [(_, cp)]) -> cp + | _ -> assert false + in + let il = List.map snd (free_vars_of_pat [] p) in + (env, BDPattern(loc,(cp,il),lvar,env,tyc) :: bl) let intern_generalization intern env lvar loc bk ak c = let c = intern {env with unb = true} c in @@ -509,16 +566,36 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function in (renaming',env), Name id' -let make_letins = List.fold_right (fun (loc,(na,b,t)) c -> GLetIn (loc,na,b,c)) - -let rec subordinate_letins letins = function +type letin_param = + | LPLetIn of Loc.t * (Name.t * glob_constr) + | LPCases of Loc.t * (cases_pattern * Id.t list) * Id.t + +let make_letins = + List.fold_right + (fun a c -> + match a with + | LPLetIn (loc,(na,b)) -> + GLetIn(loc,na,b,c) + | LPCases (loc,(cp,il),id) -> + let tt = (GVar(loc,id),(Name id,None)) in + GCases(loc,Misctypes.LetPatternStyle,None,[tt],[(loc,il,[cp],c)])) + +let rec subordinate_letins intern letins = function (* binders come in reverse order; the non-let are returned in reverse order together *) (* with the subordinated let-in in writing order *) - | (loc,(na,_,Some b,t))::l -> - subordinate_letins ((loc,(na,b,t))::letins) l - | (loc,(na,bk,None,t))::l -> - let letins',rest = subordinate_letins [] l in + | BDRawDef (loc,(na,_,Some b,t))::l -> + subordinate_letins intern (LPLetIn (loc,(na,b))::letins) l + | BDRawDef (loc,(na,bk,None,t))::l -> + let letins',rest = subordinate_letins intern [] l in letins',((loc,(na,bk,t)),letins)::rest + | BDPattern (loc,u,lvar,env,tyc) :: l -> + let ienv = Id.Set.elements env.ids in + let id = Namegen.next_ident_away (Id.of_string "pat") 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' = List.map (fun a -> BDRawDef a) bl' in + subordinate_letins intern (LPCases (loc,u,id)::letins) (bl'@ l) | [] -> letins,[] @@ -526,7 +603,7 @@ let rec subst_iterator y t = function | GVar (_,id) as x -> if Id.equal id y then t else x | x -> map_glob_constr (subst_iterator y t) x -let instantiate_notation_constr loc intern (_,ntnvars as lvar) subst infos c = +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) *) @@ -585,8 +662,8 @@ let instantiate_notation_constr loc intern (_,ntnvars as lvar) 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 lvar) (env,[]) bl in - let letins,bl = subordinate_letins [] bl in + let env,bl = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in + let letins,bl = subordinate_letins intern [] bl in let termin = aux subst' (renaming,env) terminator in let res = List.fold_left (fun t binder -> subst_iterator ldots_var t @@ -596,11 +673,14 @@ let instantiate_notation_constr loc intern (_,ntnvars as lvar) subst infos c = with Not_found -> anomaly (Pp.str "Inconsistent substitution of recursive notation")) | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt -> - let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in - GProd (loc,na,bk,t,make_letins letins (aux subst' infos c')) + 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 + GProd (loc,na,bk,t,e) | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt -> - let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in - GLambda (loc,na,bk,t,make_letins letins (aux subst' infos c')) + let a,letins = snd (Option.get binderopt) in + let (loc,(na,bk,t)) = a in + GLambda (loc,na,bk,t,make_letins letins (aux 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' -> @@ -775,10 +855,10 @@ let intern_non_secvar_qualid loc qid intern env lvar us args = | GRef (_, VarRef _, _),_,_ -> raise Not_found | r -> r -let intern_applied_reference intern env namedctx lvar us args = function +let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function | Qualid (loc, qid) -> let r,projapp,args2 = - try intern_qualid loc qid intern env lvar us args + try intern_qualid loc qid intern env ntnvars us args with Not_found -> error_global_not_found_loc loc qid in let x, imp, scopes, l = find_appl_head_data r in @@ -788,7 +868,7 @@ let intern_applied_reference intern env namedctx lvar us args = function with Not_found -> let qid = qualid_of_ident id in try - let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env lvar us args in + let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env ntnvars us args in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 with Not_found -> @@ -1195,6 +1275,8 @@ let drop_notations_pattern looked_for = | CPatAtom (loc,None) -> RCPatAtom (loc,None) | CPatOr (loc, pl) -> RCPatOr (loc,List.map (in_pat top scopes) pl) + | CPatCast _ -> + assert false and in_pat_sc scopes x = in_pat false (x,snd scopes) and in_not top loc scopes (subst,substlist as fullsubst) args = function | NVar id -> @@ -1280,6 +1362,10 @@ let intern_cases_pattern genv scopes aliases pat = intern_pat genv aliases (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat) +let _ = + intern_cases_pattern_fwd := + fun scopes p -> intern_cases_pattern (Global.env ()) scopes empty_alias p + let intern_ind_pattern genv scopes pat = let no_not = try @@ -1362,7 +1448,7 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Main loop *) -let internalize globalenv env allow_patvar lvar c = +let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let rec intern env = function | CRef (ref,us) as x -> let (c,imp,subscopes,l),_ = @@ -1383,10 +1469,11 @@ let internalize globalenv env allow_patvar lvar c = (fun (id,(n,order),bl,ty,_) -> let intern_ro_arg f = let before, after = split_at_annot bl n in - let (env',rbefore) = - List.fold_left intern_local_binder (env,[]) before in + let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in + let rbefore = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbefore in let ro = f (intern env') in let n' = Option.map (fun _ -> List.count (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore) n in + let rbefore = List.map (fun a -> BDRawDef a) rbefore in n', ro, List.fold_left intern_local_binder (env',rbefore) after in let n, ro, (env',rbl) = @@ -1398,12 +1485,18 @@ let internalize globalenv env allow_patvar lvar c = | CMeasureRec (m,r) -> intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r)) in - ((n, ro), List.rev rbl, intern_type env' ty, env')) dl in + let bl = + List.rev_map + (function + | BDRawDef a -> a + | BDPattern (loc,_,_,_,_) -> + Loc.raise loc (Stream.Error "pattern with quote not allowed after fix")) rbl in + ((n, ro), bl, intern_type env' ty, env')) dl in let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') -> let env'' = List.fold_left_i (fun i en name -> let (_,bli,tyi,_) = idl_temp.(i) in let fix_args = (List.map (fun (_,(na, bk, _, _)) -> (build_impls bk na)) bli) in - push_name_env lvar (impls_type_list ~args:fix_args tyi) + push_name_env ntnvars (impls_type_list ~args:fix_args tyi) en (Loc.ghost, Name name)) 0 env' lf in (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in GRec (loc,GFix @@ -1422,15 +1515,15 @@ let internalize globalenv env allow_patvar lvar c = in let idl_tmp = Array.map (fun ((loc,id),bl,ty,_) -> - let (env',rbl) = - List.fold_left intern_local_binder (env,[]) bl in + let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in + let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbl in (List.rev rbl, intern_type env' ty,env')) dl in let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') -> let env'' = List.fold_left_i (fun i en name -> let (bli,tyi,_) = idl_tmp.(i) in let cofix_args = List.map (fun (_, (na, bk, _, _)) -> (build_impls bk na)) bli in - push_name_env lvar (impls_type_list ~args:cofix_args tyi) + push_name_env ntnvars (impls_type_list ~args:cofix_args tyi) en (Loc.ghost, Name name)) 0 env' lf in (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in GRec (loc,GCoFix n, @@ -1449,15 +1542,15 @@ let internalize globalenv env allow_patvar lvar c = | CLetIn (loc,na,c1,c2) -> let inc1 = intern (reset_tmp_scope env) c1 in GLetIn (loc, snd na, inc1, - intern (push_name_env lvar (impls_term_list inc1) env na) c2) + intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[])) when Bigint.is_strictly_pos p -> intern env (CPrim (loc,Numeral (Bigint.neg p))) | CNotation (_,"( _ )",([a],[],[])) -> intern env a | CNotation (loc,ntn,args) -> - intern_notation intern env lvar loc ntn args + intern_notation intern env ntnvars loc ntn args | CGeneralization (loc,b,a,c) -> - intern_generalization intern env lvar loc b a c + intern_generalization intern env ntnvars loc b a c | CPrim (loc, p) -> fst (Notation.interp_prim_token loc p (env.tmp_scope,env.scopes)) | CDelimiters (loc, key, e) -> @@ -1485,7 +1578,7 @@ let internalize globalenv env allow_patvar lvar c = intern_applied_reference intern env (Environ.named_context globalenv) lvar us args ref | CNotation (loc,ntn,([],[],[])) -> - let c = intern_notation intern env lvar loc ntn ([],[],[]) in + 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 | x -> (intern env f,[],[],[]), args in @@ -1518,7 +1611,7 @@ let internalize globalenv env allow_patvar lvar c = (tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs) tms ([],Id.Set.empty,[]) in let env' = Id.Set.fold - (fun var bli -> push_name_env lvar (Variable,[],[],[]) bli (Loc.ghost,Name var)) + (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (Loc.ghost,Name var)) (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in (* PatVars before a real pattern do not need to be matched *) let stripped_match_from_in = @@ -1552,16 +1645,16 @@ let internalize globalenv env allow_patvar lvar c = (* "in" is None so no match to add *) let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in let p' = Option.map (fun u -> - let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env') + let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env') (Loc.ghost,na') in intern_type env'' u) po in GLetTuple (loc, List.map snd nal, (na', p'), b', - intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) + intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *) let p' = Option.map (fun p -> - let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env) + let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env) (Loc.ghost,na') in intern_type env'' p) po in GIf (loc, c', (na', p'), intern env b1, intern env b2) @@ -1606,7 +1699,7 @@ let internalize globalenv env allow_patvar lvar c = and intern_type env = intern (set_type_scope env) and intern_local_binder env bind = - intern_local_binder_aux intern lvar env bind + intern_local_binder_aux intern ntnvars env bind (* Expands a multiple pattern into a disjunction of multiple patterns *) and intern_multiple_pattern env n (loc,pl) = @@ -1685,11 +1778,11 @@ let internalize globalenv env allow_patvar lvar c = (tm',(snd na,typ)), extra_id, match_td and iterate_prod loc2 env bk ty body nal = - let env, bl = intern_assumption intern lvar env nal bk ty in + let env, bl = intern_assumption intern ntnvars env nal bk ty in it_mkGProd loc2 bl (intern_type env body) and iterate_lam loc2 env bk ty body nal = - let env, bl = intern_assumption intern lvar env nal bk ty in + let env, bl = intern_assumption intern ntnvars env nal bk ty in it_mkGLambda loc2 bl (intern env body) and intern_impargs c env l subscopes args = @@ -1895,7 +1988,16 @@ let intern_context global_level env impl_env binders = try let lvar = (empty_ltac_sign, Id.Map.empty) in let lenv, bl = List.fold_left - (intern_local_binder_aux ~global_level (my_intern_constr env lvar) lvar) + (fun (lenv, bl) b -> + let bl = List.map (fun a -> BDRawDef a) bl in + let (env, bl) = intern_local_binder_aux ~global_level (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in + let bl = + List.map + (function + | BDRawDef a -> a + | BDPattern (loc,_,_,_,_) -> + Loc.raise loc (Stream.Error "pattern with quote not allowed here")) bl in + (env, bl)) ({ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impl_env}, []) binders in (lenv.impls, List.map snd bl) diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 567150a5d..b50732e4e 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -112,6 +112,7 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) = let l' = free_vars_of_constr_expr c ~bound:bdvars l in aux (Id.Set.union (ids_of_list bound) bdvars) l' tl + | LocalPattern _ :: tl -> assert false | [] -> bdvars, l in aux bound l binders diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 3efd50b17..d8e022ce6 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -692,12 +692,12 @@ let glue_letin_with_decls = true let rec match_iterated_binders islambda decls = function | GLambda (_,na,bk,t,b) when islambda -> - match_iterated_binders islambda ((na,bk,None,t)::decls) b + match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b | GProd (_,(Name _ as na),bk,t,b) when not islambda -> - match_iterated_binders islambda ((na,bk,None,t)::decls) b + match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b | GLetIn (loc,na,c,b) when glue_letin_with_decls -> match_iterated_binders islambda - ((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b + ((Inl na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b | b -> (decls,b) let remove_sigma x (terms,onlybinders,termlists,binderlists) = @@ -756,14 +756,27 @@ let rec match_ inner u alp metas sigma a1 a2 = | r1, NList (x,_,iter,termin,lassoc) -> match_alist (match_hd u alp) metas sigma r1 x iter termin lassoc + (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *) + | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],t)])), + NBinderList (x,_,NLambda (Name id2,_,b2),(NVar v as termin)) when p = e -> + let decls = [(Inr cp,bk,None,t1)] in + match_in u alp metas (add_bindinglist_env sigma x decls) t termin + (* Matching recursive notations for binders: ad hoc cases supporting let-in *) | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name id2,_,b2),termin)-> - let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in + let (decls,b) = match_iterated_binders true [(Inl na1,bk,None,t1)] b1 in (* TODO: address the possibility that termin is a Lambda itself *) match_in u alp metas (add_bindinglist_env sigma x decls) b termin + + (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *) + | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],t)])), + NBinderList (x,_,NProd (Name id2,_,b2),(NVar v as termin)) when p = e -> + let decls = [(Inr cp,bk,None,t1)] in + match_in u alp metas (add_bindinglist_env sigma x decls) t termin + | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name id2,_,b2),termin) when na1 != Anonymous -> - let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in + let (decls,b) = match_iterated_binders false [(Inl na1,bk,None,t1)] b1 in (* TODO: address the possibility that termin is a Prod itself *) match_in u alp metas (add_bindinglist_env sigma x decls) b termin (* Matching recursive notations for binders: general case *) @@ -773,10 +786,10 @@ let rec match_ inner u alp metas sigma a1 a2 = (* Matching individual binders as part of a recursive pattern *) | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when is_bindinglist_meta id metas -> - match_in u alp metas (add_bindinglist_env sigma id [(na,bk,None,t)]) b1 b2 + match_in u alp metas (add_bindinglist_env sigma id [(Inl na,bk,None,t)]) b1 b2 | GProd (_,na,bk,t,b1), NProd (Name id,_,b2) when is_bindinglist_meta id metas && na != Anonymous -> - match_in u alp metas (add_bindinglist_env sigma id [(na,bk,None,t)]) b1 b2 + match_in u alp metas (add_bindinglist_env sigma id [(Inl na,bk,None,t)]) b1 b2 (* Matching compositionally *) | GVar (_,id1), NVar id2 when alpha_var id1 id2 (fst alp) -> sigma @@ -863,7 +876,7 @@ let rec match_ inner u alp metas sigma a1 a2 = | _ -> assert false in let (alp,sigma) = if is_bindinglist_meta id metas then - alp, add_bindinglist_env sigma id [(Name id',Explicit,None,t1)] + alp, add_bindinglist_env sigma id [(Inl (Name id'),Explicit,None,t1)] else match_names metas (alp,sigma) (Name id') na in match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2 @@ -891,6 +904,10 @@ let term_of_binder = function | Name id -> GVar (Loc.ghost,id) | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) +type glob_decl2 = + (name, cases_pattern) Util.union * Decl_kinds.binding_kind * + glob_constr option * glob_constr + let match_notation_constr u c (metas,pat) = let terms,binders,termlists,binderlists = match_ false u ([],[]) metas ([],[],[],[]) c pat in diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 576c5b943..0f1b1a875 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -47,9 +47,12 @@ val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr exception No_match +type glob_decl2 = + (name, cases_pattern) Util.union * Decl_kinds.binding_kind * + glob_constr option * glob_constr val match_notation_constr : bool -> glob_constr -> interpretation -> (glob_constr * subscopes) list * (glob_constr list * subscopes) list * - (glob_decl list * subscopes) list + (glob_decl2 list * subscopes) list val match_notation_constr_cases_pattern : cases_pattern -> interpretation -> diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 91099bbb1..4109bdb7f 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -59,6 +59,7 @@ let rec cases_pattern_fold_names f a = function | CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat | CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a | CPatPrim _ | CPatAtom _ -> a + | CPatCast _ -> assert false let ids_of_pattern_list = List.fold_left @@ -92,6 +93,8 @@ let rec fold_local_binders g f n acc b = function f n (fold_local_binders g f n' acc b l) t | LocalRawDef ((_,na),t)::l -> f n (fold_local_binders g f (name_fold g na n) acc b l) t + | LocalPattern _::l -> + assert false | [] -> f n acc b @@ -170,6 +173,7 @@ let split_at_annot bl na = (List.rev ans, LocalRawAssum (r, k, t) :: rest) end | LocalRawDef _ as x :: rest -> aux (x :: acc) rest + | LocalPattern _ :: rest -> assert false | [] -> user_err_loc(loc,"", str "No parameter named " ++ Nameops.pr_id id ++ str".") @@ -191,7 +195,9 @@ let map_local_binders f g e bl = LocalRawAssum(nal,k,ty) -> (map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl) | LocalRawDef((loc,na),ty) -> - (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) in + (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) + | LocalPattern _ -> + assert false in let (e,rbl) = List.fold_left h (e,[]) bl in (e, List.rev rbl) diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index efd5129b6..0cbb29575 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -44,6 +44,8 @@ type raw_cases_pattern_expr = | RCPatAtom of Loc.t * Id.t option | RCPatOr of Loc.t * raw_cases_pattern_expr list +type instance_expr = Misctypes.glob_level list + type cases_pattern_expr = | CPatAlias of Loc.t * cases_pattern_expr * Id.t | CPatCstr of Loc.t * reference @@ -58,14 +60,13 @@ type cases_pattern_expr = | CPatPrim of Loc.t * prim_token | CPatRecord of Loc.t * (reference * cases_pattern_expr) list | CPatDelimiters of Loc.t * string * cases_pattern_expr + | CPatCast of Loc.t * cases_pattern_expr * constr_expr and cases_pattern_notation_substitution = cases_pattern_expr list * (** for constr subterms *) cases_pattern_expr list list (** for recursive notations *) -type instance_expr = Misctypes.glob_level list - -type constr_expr = +and constr_expr = | CRef of reference * instance_expr option | CFix of Loc.t * Id.t located * fix_expr list | CCoFix of Loc.t * Id.t located * cofix_expr list @@ -124,6 +125,7 @@ and recursion_order_expr = and local_binder = | LocalRawDef of Name.t located * constr_expr | LocalRawAssum of Name.t located list * binder_kind * constr_expr + | LocalPattern of Loc.t * cases_pattern_expr * constr_expr option and constr_notation_substitution = constr_expr list * (** for constr subterms *) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 243f71416..014b41ae9 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -401,6 +401,14 @@ GEXTEND Gram CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> CPatNotation(!@loc,"( _ )",([p],[]),[]) | _ -> p) + | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" -> + let p = + match p with + CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> + CPatNotation(!@loc,"( _ )",([p],[]),[]) + | _ -> p + in + CPatCast (!@loc, p, ty) | n = INT -> CPatPrim (!@loc, Numeral (Bigint.of_string n)) | s = string -> CPatPrim (!@loc, String s) ] ] ; @@ -476,6 +484,13 @@ GEXTEND Gram List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc + | "'"; p = pattern LEVEL "0" -> + let (p, ty) = + match p with + | CPatCast (_, p, ty) -> (p, Some ty) + | _ -> (p, None) + in + [LocalPattern (!@loc, p, ty)] ] ] ; typeclass_constraint: diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 9c1f5afb8..f0475ee25 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -135,6 +135,12 @@ let test_plural_form_types = function (strbrk "Keywords Implicit Types expect more than one type") | _ -> () +let fresh_var env c = + Namegen.next_ident_away (Id.of_string "pat") + (env @ Id.Set.elements (Topconstr.free_vars_of_constr_expr c)) + +let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var + (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion @@ -235,11 +241,19 @@ GEXTEND Gram (* Simple definitions *) def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> + let (bl, c) = expand_pattern_binders mkCLambdaN bl c in (match c with CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> - DefineBody (bl, red, c, Some t) + let ((bl, c), tyo) = + if List.exists (function LocalPattern _ -> true | _ -> false) bl + then + let c = CCast (!@loc, c, CastConv t) in + (expand_pattern_binders mkCLambdaN bl c, None) + else ((bl, c), Some t) + in + DefineBody (bl, red, c, tyo) | bl = binders; ":"; t = lconstr -> ProveBody (bl, t) ] ] ; diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 0cacb003d..1c5eb1621 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -132,6 +132,7 @@ let rec abstract_glob_constr c = function | Constrexpr.LocalRawAssum (idl,k,t)::bl -> List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl (abstract_glob_constr c bl) + | Constrexpr.LocalPattern _::bl -> assert false let interp_casted_constr_with_implicits env sigma impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls @@ -215,6 +216,7 @@ let rec local_binders_length = function | [] -> 0 | Constrexpr.LocalRawDef _::bl -> 1 + local_binders_length bl | Constrexpr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl + | Constrexpr.LocalPattern _::bl -> assert false let prepare_body ((name,_,args,types,_),_) rt = let n = local_binders_length args in @@ -861,6 +863,7 @@ let make_graph (f_ref:global_reference) = (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n),None)) nal + | Constrexpr.LocalPattern _ -> assert false ) nal_tas ) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index eead3a684..1ea502539 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -279,6 +279,8 @@ end) = struct | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimplepatt p), 1 + | CPatCast _ -> + assert false in let loc = cases_pattern_expr_loc p in pr_with_comments loc @@ -298,6 +300,7 @@ end) = struct let begin_of_binder = function LocalRawDef((loc,_),_) -> fst (Loc.unloc loc) | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) + | LocalPattern(loc,_,_) -> fst (Loc.unloc loc) | _ -> assert false let begin_of_binders = function @@ -346,6 +349,8 @@ end) = struct | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) + | LocalPattern _ -> + assert false let pr_undelimited_binders sep pr_c = prlist_with_sep sep (pr_binder_among_many pr_c) @@ -357,6 +362,8 @@ end) = struct pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t) | LocalRawAssum _ :: _ as bdl -> pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl + | LocalPattern (loc,p,tyo) :: _ -> + str "'" ++ pr_patt ltop p | _ -> assert false let pr_binders_gen pr_c sep is_open = @@ -430,6 +437,7 @@ end) = struct let names_of_binder = function | LocalRawAssum (nal,_,_) -> nal | LocalRawDef (_,_) -> [] + | LocalPattern _ -> assert false in let ids = List.flatten (List.map names_of_binder bl) in if List.length ids > 1 then spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" @@ -530,6 +538,21 @@ end) = struct (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix), lfix ) + | CProdN + (_, + [([(_,Name n)],_,_)], + CCases + (_,LetPatternStyle,None,[(CRef(Ident(_,m),None),None,None)], + [(_,[(_,[p])],a)])) + when + Id.equal m n && + not (Id.Set.mem n (Topconstr.free_vars_of_constr_expr a)) -> + return ( + hov 0 ( + keyword "forall" ++ spc () ++ str "'" ++ pr_patt ltop p ++ + str "," ++ pr spc ltop a), + llambda + ) | CProdN _ -> let (bl,a) = extract_prod_binders a in return ( @@ -539,6 +562,21 @@ end) = struct str "," ++ pr spc ltop a), lprod ) + | CLambdaN + (_, + [([(_,Name n)],_,_)], + CCases + (_,LetPatternStyle,None,[(CRef(Ident(_,m),None),None,None)], + [(_,[(_,[p])],a)])) + when + Id.equal m n && + not (Id.Set.mem n (Topconstr.free_vars_of_constr_expr a)) -> + return ( + hov 0 ( + keyword "fun" ++ spc () ++ str "'" ++ pr_patt ltop p ++ + pr_fun_sep ++ pr spc ltop a), + llambda + ) | CLambdaN _ -> let (bl,a) = extract_lam_binders a in return ( diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out new file mode 100644 index 000000000..34558e9a6 --- /dev/null +++ b/test-suite/output/Binder.out @@ -0,0 +1,8 @@ +foo = fun '(x, y) => x + y + : nat * nat -> nat +forall '(a, b), a /\ b + : Prop +foo = λ '(x, y), x + y + : nat * nat → nat +∀ '(a, b), a ∧ b + : Prop diff --git a/test-suite/output/Binder.v b/test-suite/output/Binder.v new file mode 100644 index 000000000..9aced9f66 --- /dev/null +++ b/test-suite/output/Binder.v @@ -0,0 +1,7 @@ +Definition foo '(x,y) := x + y. +Print foo. +Check forall '(a,b), a /\ b. + +Require Import Utf8. +Print foo. +Check forall '(a,b), a /\ b. diff --git a/toplevel/command.ml b/toplevel/command.ml index 5041d78a3..1fda5b9f7 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -548,6 +548,7 @@ let check_param = function | LocalRawDef (na, _) -> check_named na | LocalRawAssum (nas, Default _, _) -> List.iter check_named nas | LocalRawAssum (nas, Generalized _, _) -> () +| LocalPattern _ -> assert false let interp_mutual_inductive (paramsl,indl) notations poly prv finite = check_all_names_different indl; diff --git a/toplevel/record.ml b/toplevel/record.ml index c9b46983e..fe6ed55a7 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -107,7 +107,8 @@ let typecheck_params_and_fields def id pl t ps nots fs = in List.iter (function LocalRawDef (b, _) -> error default_binder_kind b - | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps + | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls + | LocalPattern _ -> assert false) ps in let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in let t', template = match t with |