diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 36 | ||||
| -rw-r--r-- | interp/constrintern.ml | 114 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 6 |
3 files changed, 84 insertions, 72 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index dd8a48b85e..74504e36d4 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -274,17 +274,8 @@ let pattern_printable_in_both_syntax (ind,_ as c) = (* Better to use extern_glob_constr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = - (* pboutill: There are letins in pat which is incompatible with notations and - not explicit application. *) - match pat with - | PatCstr(loc,cstrsp,args,na) - when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp -> - let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in - let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), []) - | _ -> try - if !Flags.raw_print || !print_no_symbol then raise No_match; + if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; let (na,sc,p) = uninterp_prim_token_cases_pattern pat in match availability_of_prim_token p sc scopes with | None -> raise No_match @@ -293,7 +284,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na with No_match -> try - if !Flags.raw_print || !print_no_symbol then raise No_match; + if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_pattern scopes vars pat (uninterp_cases_pattern_notations pat) with No_match -> @@ -307,16 +298,19 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = if !Flags.raw_print then raise Exit; let projs = Recordops.lookup_projections (fst cstrsp) in let rec ip projs args acc = - match projs with - | [] -> acc - | None :: q -> ip q args acc - | Some c :: q -> - match args with - | [] -> raise No_match - | CPatAtom(_, None) :: tail -> ip q tail acc - (* we don't want to have 'x = _' in our patterns *) - | head :: tail -> ip q tail - ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc) + match projs, args with + | [], [] -> acc + | proj :: q, pat :: tail -> + let acc = + match proj, pat with + | _, CPatAtom(_, None) -> + (* we don't want to have 'x := _' in our patterns *) + acc + | Some c, _ -> + ((extern_reference loc Id.Set.empty (ConstRef c), pat) :: acc) + | _ -> raise No_match in + ip q tail acc + | _ -> assert false in CPatRecord(loc, List.rev (ip projs args [])) with diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c916fcd886..8400fdc967 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -432,31 +432,6 @@ 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 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 @@ -490,13 +465,15 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio | Some ty -> ty | None -> CHole(loc,None,Misctypes.IntroAnonymous,None) in - let env = intern_local_pattern intern lvar env p in - let cp = + let il,cp = match !intern_cases_pattern_fwd (None,env.scopes) p with - | (_, [(_, cp)]) -> cp + | (il, [(subst,cp)]) -> + if not (Id.Map.equal Id.equal subst Id.Map.empty) then + user_err_loc (loc,"",str "Unsupported nested \"as\" clause."); + il,cp | _ -> assert false in - let il = List.map snd (free_vars_of_pat [] p) in + let env = {env with ids = List.fold_right Id.Set.add il env.ids} in (env, BDPattern(loc,(cp,il),lvar,env,tyc) :: bl) let intern_generalization intern env lvar loc bk ak c = @@ -947,17 +924,6 @@ let find_remaining_scopes pl1 pl2 ref = in ((try List.firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs), simple_adjust_scopes len_pl2 (aux (impl_list,scope_list))) -let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 - -let product_of_cases_patterns ids idspl = - List.fold_right (fun (ids,pl) (ids',ptaill) -> - (ids @ ids', - (* Cartesian prod of the or-pats for the nth arg and the tail args *) - List.flatten ( - List.map (fun (subst,p) -> - List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl))) - idspl (ids,[Id.Map.empty,[]]) - (* @return the first variable that occurs twice in a pattern naive n^2 algo *) @@ -994,6 +960,45 @@ let check_constructor_length env loc cstr len_pl pl0 = (error_wrong_numarg_constructor_loc loc env cstr (Inductiveops.constructor_nrealargs cstr))) +open Term +open Declarations + +(* Similar to Cases.adjust_local_defs but on RCPat *) +let insert_local_defs_in_pattern (ind,j) l = + let (mib,mip) = Global.lookup_inductive ind in + if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then + (* Optimisation *) l + else + let typi = mip.mind_nf_lc.(j-1) in + let (_,typi) = decompose_prod_n_assum (Context.Rel.length mib.mind_params_ctxt) typi in + let (decls,_) = decompose_prod_assum typi in + let rec aux decls args = + match decls, args with + | Context.Rel.Declaration.LocalDef _ :: decls, args -> Constrexpr.RCPatAtom (Loc.ghost,None) :: aux decls args + | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *) + | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args + | _ -> assert false in + aux (List.rev decls) l + +let add_local_defs_and_check_length loc env g pl args = match g with + | ConstructRef cstr -> + (* We consider that no variables corresponding to local binders + have been given in the "explicit" arguments, which come from a + "@C args" notation or from a custom user notation *) + let pl' = insert_local_defs_in_pattern cstr pl in + let maxargs = Inductiveops.constructor_nalldecls cstr in + if List.length pl' + List.length args > maxargs then + error_wrong_numarg_constructor_loc loc env cstr (Inductiveops.constructor_nrealargs cstr); + (* Two possibilities: either the args are given with explict + variables for local definitions, then we give the explicit args + extended with local defs, so that there is nothing more to be + added later on; or the args are not enough to have all arguments, + which a priori means local defs to add in the [args] part, so we + postpone the insertion of local defs in the explicit args *) + (* Note: further checks done later by check_constructor_length *) + if List.length pl' + List.length args = maxargs then pl' else pl + | _ -> pl + let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 = let impl_list = if Int.equal len_pl1 0 then select_impargs_size (List.length pl2) impls_st @@ -1212,6 +1217,17 @@ let alias_of als = match als.alias_ids with *) +let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 + +let product_of_cases_patterns aliases idspl = + List.fold_right (fun (ids,pl) (ids',ptaill) -> + (ids @ ids', + (* Cartesian prod of the or-pats for the nth arg and the tail args *) + List.flatten ( + List.map (fun (subst,p) -> + List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl))) + idspl (aliases.alias_ids,[aliases.alias_map,[]]) + let rec subst_pat_iterator y t p = match p with | RCPatAtom (_,id) -> begin match id with Some x when Id.equal x y -> t | _ -> p end @@ -1221,7 +1237,7 @@ let rec subst_pat_iterator y t p = match p with | RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a) | RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl) -let drop_notations_pattern looked_for = +let drop_notations_pattern looked_for genv = (* At toplevel, Constructors and Inductives are accepted, in recursive calls only constructor are allowed *) let ensure_kind top loc g = @@ -1350,9 +1366,9 @@ let drop_notations_pattern looked_for = | NApp (NRef g,pl) -> ensure_kind top loc g; let (argscs1,argscs2) = find_remaining_scopes pl args g in - RCPatCstr (loc, g, - List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @ - List.map (in_pat false scopes) args, []) + let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in + let pl = add_local_defs_and_check_length loc genv g pl args in + RCPatCstr (loc, g, pl @ List.map (in_pat false scopes) args, []) | NList (x,y,iter,terminator,lassoc) -> if not (List.is_empty args) then user_err_loc (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns."); @@ -1376,7 +1392,7 @@ let drop_notations_pattern looked_for = let rec intern_pat genv aliases pat = let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 = let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in - let (ids',pll) = product_of_cases_patterns aliases.alias_ids (idslpl1@idslpl2) in + let (ids',pll) = product_of_cases_patterns aliases (idslpl1@idslpl2) in let pl' = List.map (fun (asubst,pl) -> (asubst, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in ids',pl' in @@ -1445,7 +1461,7 @@ and check_no_patcast_subst (pl,pll) = let intern_cases_pattern genv scopes aliases pat = check_no_patcast pat; intern_pat genv aliases - (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat) + (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat) let _ = intern_cases_pattern_fwd := @@ -1455,7 +1471,7 @@ let intern_ind_pattern genv scopes pat = check_no_patcast pat; let no_not = try - drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat + drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type loc in match no_not with @@ -1466,7 +1482,7 @@ let intern_ind_pattern genv scopes pat = let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in (with_letin, - match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with + match product_of_cases_patterns empty_alias (List.rev_append idslpl1 idslpl2) with | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin) | _ -> error_bad_inductive_type loc) | x -> error_bad_inductive_type (raw_cases_pattern_expr_loc x) @@ -1796,7 +1812,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = and intern_multiple_pattern env n (loc,pl) = let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in check_number_of_pattern loc n pl; - product_of_cases_patterns [] idsl_pll + product_of_cases_patterns empty_alias idsl_pll (* Expands a disjunction of multiple pattern *) and intern_disjunctive_multiple_pattern env loc n mpl = diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 0c5393cf41..5648821539 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1158,6 +1158,7 @@ let match_notation_constr u c (metas,pat) = metas ([],[],[]) (* Matching cases pattern *) + let add_patterns_for_params ind l = let mib,_ = Global.lookup_inductive ind in let nparams = mib.Declarations.mind_nparams in @@ -1190,10 +1191,11 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) | PatVar (_,Anonymous), NHole _ -> sigma,(0,[]) | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> - sigma,(0,add_patterns_for_params (fst r1) largs) + let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in + sigma,(0,l) | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) when eq_constructor r1 r2 -> - let l1 = add_patterns_for_params (fst r1) args1 in + let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 then |