diff options
author | Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> | 2016-02-15 16:22:45 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-06-27 12:31:23 +0200 |
commit | c6d9d4fb142ef42634be25b60c0995b541e86629 (patch) | |
tree | e6cd36fc03ae7a79d9b65f08b0295bedc485f855 /interp | |
parent | 4d4e2f421c1a4f0339568d3c96ff2459a027aa09 (diff) |
Adding ability to put any pattern in binders, prefixed by a quote.
Cf CHANGES for details.
Diffstat (limited to 'interp')
-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 |
8 files changed, 271 insertions, 71 deletions
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) |