diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 260 |
1 files changed, 179 insertions, 81 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c699f79351..a071ba7ec9 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -32,6 +32,7 @@ open Notation_ops open Notation open Inductiveops open Context.Rel.Declaration +open NumTok (** constr_expr -> glob_constr translation: - it adds holes for implicit arguments @@ -226,7 +227,7 @@ let contract_curly_brackets ntn (l,ll,bl,bll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | { CAst.v = CNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l -> + | { CAst.v = CNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> @@ -242,7 +243,7 @@ let contract_curly_brackets_pat ntn (l,ll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | { CAst.v = CPatNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l -> + | { CAst.v = CPatNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> @@ -257,7 +258,7 @@ type intern_env = { tmp_scope: Notation_term.tmp_scope_name option; scopes: Notation_term.scope_name list; impls: internalization_env; - impl_binder_index: int option; + binder_block_names: (abstraction_kind option (* None = unknown *) * Id.Set.t) option; } (**********************************************************************) @@ -330,15 +331,18 @@ let exists_name na l = | _ -> false let build_impls ?loc n bk na acc = - match bk with - | Implicit -> + let impl_status max = let na = - if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end - else na in + if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end + else na in let impl = match na with - | Name id -> Some (ExplByName id,Manual,(true,true)) - | Anonymous -> Some (ExplByPos (n,None),Manual,(true,true)) in - impl :: acc + | Name id -> Some (ExplByName id,Manual,(max,true)) + | Anonymous -> Some (ExplByPos (n,None),Manual,(max,true)) in + impl + in + match bk with + | NonMaxImplicit -> impl_status false :: acc + | MaxImplicit -> impl_status true :: acc | Explicit -> None :: acc let impls_binder_list = @@ -373,6 +377,49 @@ let rec check_capture ty = let open CAst in function | [] -> () +(** Status of the internalizer wrt "Arguments" of names *) + +let restart_no_binders env = + { env with binder_block_names = None} + (* Not in relation with the "Arguments" of a name *) + +let restart_prod_binders env = + { env with binder_block_names = Some (Some AbsPi, Id.Set.empty) } + (* In a position binding a type to a name *) + +let restart_lambda_binders env = + { env with binder_block_names = Some (Some AbsLambda, Id.Set.empty) } + (* In a position binding a body to a name *) + +let switch_prod_binders env = + match env.binder_block_names with + | Some (o,ids) when o <> Some AbsLambda -> restart_prod_binders env + | _ -> restart_no_binders env + (* In a position switching to a type *) + +let switch_lambda_binders env = + match env.binder_block_names with + | Some (o,ids) when o <> Some AbsPi -> restart_lambda_binders env + | _ -> restart_no_binders env + (* In a position switching to a term *) + +let slide_binders env = + match env.binder_block_names with + | Some (o,ids) when o <> Some AbsPi -> restart_prod_binders env + | _ -> restart_no_binders env + (* In a position of cast *) + +let binder_status_fun = { + no = (fun x -> x); + restart_prod = on_snd restart_prod_binders; + restart_lambda = on_snd restart_lambda_binders; + switch_prod = on_snd switch_prod_binders; + switch_lambda = on_snd switch_lambda_binders; + slide = on_snd slide_binders; +} + +(**) + let locate_if_hole ?loc na c = match DAst.get c with | GHole (_,naming,arg) -> (try match na with @@ -397,7 +444,11 @@ let check_hidden_implicit_parameters ?loc id impls = strbrk "the type of a constructor shall use a different name.") let pure_push_name_env (id,implargs) env = - {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} + {env with + ids = Id.Set.add id env.ids; + impls = Id.Map.add id implargs env.impls; + binder_block_names = Option.map (fun (b,ids) -> (b,Id.Set.add id ids)) env.binder_block_names; + } let push_name_env ntnvars implargs env = let open CAst in @@ -421,13 +472,15 @@ let remember_binders_impargs env bl = let restore_binders_impargs env l = List.fold_right pure_push_name_env l env -let warn_unexpected_implicit_binder_declaration = +let warn_ignoring_unexpected_implicit_binder_declaration = CWarnings.create ~name:"unexpected-implicit-declaration" ~category:"syntax" - Pp.(fun () -> str "Unexpected implicit binder declaration.") + Pp.(fun () -> str "Ignoring implicit binder declaration in unexpected position.") let check_implicit_meaningful ?loc k env = - if k = Implicit && env.impl_binder_index = None then - warn_unexpected_implicit_binder_declaration ?loc () + if k <> Explicit && env.binder_block_names = None then + (warn_ignoring_unexpected_implicit_binder_declaration ?loc (); Explicit) + else + k let intern_generalized_binder intern_type ntnvars env {loc;v=na} b' t ty = @@ -441,10 +494,10 @@ let intern_generalized_binder intern_type ntnvars let env' = List.fold_left (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x)) env fvs in - check_implicit_meaningful ?loc b' env; + let b' = check_implicit_meaningful ?loc b' env in let bl = List.map CAst.(map (fun id -> - (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) + (Name id, MaxImplicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) fvs in let na = match na with @@ -463,7 +516,7 @@ let intern_generalized_binder intern_type ntnvars (make ?loc (na,b',ty')) :: List.rev bl) let intern_assumption intern ntnvars env nal bk ty = - let intern_type env = intern (set_type_scope env) in + let intern_type env = intern (restart_prod_binders (set_type_scope env)) in match bk with | Default k -> let ty = intern_type env ty in @@ -471,7 +524,7 @@ let intern_assumption intern ntnvars env nal bk ty = let impls = impls_type_list 1 ty in List.fold_left (fun (env, bl) ({loc;v=na} as locna) -> - check_implicit_meaningful ?loc k env; + let k = check_implicit_meaningful ?loc k env in (push_name_env ntnvars impls env locna, (make ?loc (na,k,locate_if_hole ?loc na ty))::bl)) (env, []) nal @@ -492,8 +545,8 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd") let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) = - let term = intern env def in - let ty = Option.map (intern env) ty in + let term = intern (reset_tmp_scope (restart_lambda_binders env)) def in + let ty = Option.map (intern (set_type_scope (restart_prod_binders env))) ty in let impls = impls_term_list 1 term in (push_name_env ntnvars impls env locna, (na,Explicit,term,ty)) @@ -585,6 +638,14 @@ let rec expand_binders ?loc mk bl c = (**********************************************************************) (* Syntax extensions *) +let check_not_notation_variable f ntnvars = + (* Check bug #4690 *) + match DAst.get f with + | GVar id when Id.Map.mem id ntnvars -> + user_err (str "Prefix @ is not applicable to notation variables.") + | _ -> + () + let option_mem_assoc id = function | Some (id',c) -> Id.equal id id' | None -> false @@ -713,6 +774,19 @@ let flatten_binders bl = | a -> [a] in List.flatten (List.map dispatch bl) +let rec adjust_env env = function + (* We need to adjust scopes, binder blocks ... to the env expected + at the recursive occurrence; We do an underapproximation... *) + | NProd (_,_,c) -> adjust_env (switch_prod_binders env) c + | NLambda (_,_,c) -> adjust_env (switch_lambda_binders env) c + | NLetIn (_,_,_,c) -> adjust_env env c + | NVar id when Id.equal id ldots_var -> env + | NCast (c,_) -> adjust_env env c + | NApp _ -> restart_no_binders env + | NVar _ | NRef _ | NHole _ | NCases _ | NLetTuple _ | NIf _ + | NRec _ | NSort _ | NInt _ | NFloat _ + | NList _ | NBinderList _ -> env (* to be safe, but restart should be ok *) + let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let (terms,termlists,binders,binderlists) = subst in (* when called while defining a notation, avoid capturing the private binders @@ -725,7 +799,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let rec aux_letin env = function | [],terminator,_ -> aux (terms,None,None) (renaming,env) terminator | AddPreBinderIter (y,binder)::rest,terminator,iter -> - let env,binders = intern_local_binder_aux intern ntnvars (env,[]) binder in + let env,binders = intern_local_binder_aux intern ntnvars (adjust_env env iter,[]) binder in let binder,extra = flatten_generalized_binders_if_any y binders in aux (terms,Some (y,binder),Some (extra@rest,terminator,iter)) (renaming,env) iter | AddBinderIter (y,binder)::rest,terminator,iter -> @@ -733,7 +807,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = | AddTermIter nterms::rest,terminator,iter -> aux (nterms,None,Some (rest,terminator,iter)) (renaming,env) iter | AddLetIn (na,c,t)::rest,terminator,iter -> - let env,(na,_,c,t) = intern_letin_binder intern ntnvars env (na,c,t) in + let env,(na,_,c,t) = intern_letin_binder intern ntnvars (adjust_env env iter) (na,c,t) in DAst.make ?loc (GLetIn (na,c,t,aux_letin env (rest,terminator,iter))) in aux_letin env (Option.get iteropt) | NVar id -> subst_var subst' (renaming, env) id @@ -823,7 +897,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = DAst.make ?loc @@ GLambda (na,Explicit,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c')) | t -> glob_constr_of_notation_constr_with_binders ?loc - (traverse_binder intern_pat ntnvars subst avoid) (aux subst') subinfos t + (traverse_binder intern_pat ntnvars subst avoid) (aux subst') ~h:binder_status_fun subinfos t and subst_var (terms, binderopt, _terminopt) (renaming, env) id = (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) @@ -1006,11 +1080,11 @@ let find_appl_head_data c = c, impls, scopes, [] | GApp (r, l) -> begin match DAst.get r with - | GRef (ref,_) when l != [] -> + | GRef (ref,_) -> let n = List.length l in let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in - c, List.map (drop_first_implicits n) impls, + c, (if n = 0 then [] else List.map (drop_first_implicits n) impls), List.skipn_at_least n scopes,[] | _ -> c,[],[],[] end @@ -1144,7 +1218,7 @@ let interp_reference vars r = intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None) {ids = Id.Set.empty; unb = false ; tmp_scope = None; scopes = []; impls = empty_internalization_env; - impl_binder_index = None} + binder_block_names = None} Environ.empty_named_context_val (vars, Id.Map.empty) None [] r in r @@ -1512,12 +1586,6 @@ let alias_of als = match als.alias_ids with *) -let is_zero s = - let rec aux i = - Int.equal (String.length s) i || ((s.[i] == '0' || s.[i] == '_') && aux (i+1)) - in aux 0 -let is_zero n = is_zero n.NumTok.int && is_zero n.NumTok.frac - let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 let product_of_cases_patterns aliases idspl = @@ -1541,16 +1609,15 @@ let rec subst_pat_iterator y t = DAst.(map (function | RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl))) let is_non_zero c = match c with -| { CAst.v = CPrim (Numeral (SPlus, p)) } -> not (is_zero p) +| { CAst.v = CPrim (Numeral p) } -> not (NumTok.Signed.is_zero p) | _ -> false let is_non_zero_pat c = match c with -| { CAst.v = CPatPrim (Numeral (SPlus, p)) } -> not (is_zero p) +| { CAst.v = CPatPrim (Numeral p) } -> not (NumTok.Signed.is_zero p) | _ -> false let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"no parameters in constructors" ~key:["Asymmetric";"Patterns"] ~value:false @@ -1595,10 +1662,11 @@ let drop_notations_pattern looked_for genv = let () = assert (List.is_empty vars) in let (_,argscs) = find_remaining_scopes [] pats g in Some (g, [], List.map2 (in_pat_sc scopes) argscs pats) - | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *) + | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *) test_kind top g; let () = assert (List.is_empty vars) in - Some (g, List.map (in_pat false scopes) pats, []) + let (_,argscs) = find_remaining_scopes [] pats g in + Some (g, List.map2 (in_pat_sc scopes) argscs pats, []) | NApp (NRef g,args) -> (* Convention: do not deactivate implicit arguments and scopes for further arguments *) test_kind top g; @@ -1616,7 +1684,7 @@ let drop_notations_pattern looked_for genv = test_kind top g; Dumpglob.add_glob ?loc:qid.loc g; let (_,argscs) = find_remaining_scopes [] pats g in - Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats) + Some (g,[],List.map2 (in_pat_sc scopes) argscs pats) with Not_found -> None and in_pat top scopes pt = let open CAst in @@ -1643,7 +1711,7 @@ let drop_notations_pattern looked_for genv = | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (qid, Some expl_pl, pl) -> + | CPatCstr (qid, Some expl_pl, pl) -> let g = try Nametab.locate qid with Not_found -> raise (InternalizationError (loc,NotAConstructor qid)) in @@ -1655,13 +1723,13 @@ let drop_notations_pattern looked_for genv = (* but not scopes in expl_pl *) let (argscs1,_) = find_remaining_scopes expl_pl pl g in DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) - | CPatNotation ((InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a -> + | CPatNotation (_,(InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a -> let p = match a.CAst.v with CPatPrim (Numeral (_, p)) -> p | _ -> assert false in let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (SMinus,p)) scopes in rcp_of_glob scopes pat - | CPatNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) -> + | CPatNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) -> in_pat top scopes a - | CPatNotation (ntn,fullargs,extrargs) -> + | CPatNotation (_,ntn,fullargs,extrargs) -> let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in let (terms,termlists) = split_by_type_pat ?loc ids' (terms,termlists) in @@ -1716,7 +1784,15 @@ let drop_notations_pattern looked_for genv = let (argscs1,argscs2) = find_remaining_scopes pl args g in let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in let pl = add_local_defs_and_check_length loc genv g pl args in - DAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, []) + let args = List.map2 (fun x -> in_pat false (x,snd scopes)) argscs2 args in + let pat = + if List.length pl = 0 then + (* Convention: if notation is @f, encoded as NApp(Nref g,[]), then + implicit arguments are not inherited *) + RCPatCstr (g, pl @ args, []) + else + RCPatCstr (g, pl, args) in + DAst.make ?loc @@ pat | NList (x,y,iter,terminator,revert) -> if not (List.is_empty args) then user_err ?loc (strbrk "Application of arguments to a recursive notation not supported in patterns."); @@ -1892,6 +1968,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = with Not_found -> raise (InternalizationError (locid,UnboundFixName (false,iddef))) in + let env = restart_lambda_binders env in let idl_temp = Array.map (fun (id,recarg,bl,ty,_) -> let recarg = Option.map (function { CAst.v = v } -> match v with @@ -1934,6 +2011,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = with Not_found -> raise (InternalizationError (locid,UnboundFixName (true,iddef))) in + let env = restart_lambda_binders env in let idl_tmp = Array.map (fun ({ CAst.loc; v = id },bl,ty,_) -> let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in @@ -1957,24 +2035,26 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = Array.map (fun (_,_,bd) -> bd) idl) | CProdN ([],c2) -> anomaly (Pp.str "The AST is malformed, found prod without binders.") | CProdN (bl,c2) -> - let (env',bl) = List.fold_left intern_local_binder (env,[]) bl in + let (env',bl) = List.fold_left intern_local_binder (switch_prod_binders env,[]) bl in expand_binders ?loc mkGProd bl (intern_type env' c2) | CLambdaN ([],c2) -> anomaly (Pp.str "The AST is malformed, found lambda without binders.") | CLambdaN (bl,c2) -> - let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope env,[]) bl in + let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope (switch_lambda_binders env),[]) bl in expand_binders ?loc mkGLambda bl (intern env' c2) | CLetIn (na,c1,t,c2) -> - let inc1 = intern_restart_implicit (reset_tmp_scope env) c1 in - let int = Option.map (intern_type_restart_implicit env) t in + let inc1 = intern_restart_binders (reset_tmp_scope env) c1 in + let int = Option.map (intern_type_restart_binders env) t in DAst.make ?loc @@ GLetIn (na.CAst.v, inc1, int, - intern_restart_implicit (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2) - | CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a -> + intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2) + | CNotation (_,(InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a -> let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p))) - | CNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a - | CNotation (ntn,args) -> - intern_notation intern env ntnvars loc ntn args + | CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a + | CNotation (_,ntn,args) -> + let c = intern_notation intern env ntnvars loc ntn args in + let x, impl, scopes, l = find_appl_head_data c in + apply_impargs x env impl scopes l loc | CGeneralization (b,a,c) -> intern_generalization intern env ntnvars loc b a c | CPrim p -> @@ -1988,6 +2068,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv) lvar us args ref in + check_not_notation_variable f ntnvars; (* Rem: GApp(_,f,[]) stands for @f *) if args = [] then DAst.make ?loc @@ GApp (f,[]) else smart_gapp f loc (intern_args env args_scopes (List.map fst args)) @@ -2004,12 +2085,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CRef (ref,us) -> intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv) lvar us args ref - | CNotation (ntn,([],[],[],[])) -> + | CNotation (_,ntn,ntnargs) -> assert (Option.is_empty isproj); - let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in + let c = intern_notation intern env ntnvars loc ntn ntnargs in let x, impl, scopes, l = find_appl_head_data c in (x,impl,scopes,l), args - | _ -> assert (Option.is_empty isproj); (intern env f,[],[],[]), args in + | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in apply_impargs c env impargs args_scopes (merge_impargs l args) loc @@ -2053,7 +2134,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = tms ([],Id.Set.empty,Id.Map.empty,[]) in let env' = Id.Set.fold (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var)) - (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in + (Id.Set.union ex_ids as_in_vars) + (reset_hidden_inductive_implicit_test (restart_lambda_binders env)) in (* PatVars before a real pattern do not need to be matched *) let stripped_match_from_in = let rec aux = function @@ -2063,7 +2145,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = in aux match_from_in in let rtnpo = Option.map (replace_vars_constr_expr aliases) rtnpo in let rtnpo = match stripped_match_from_in with - | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *) + | [] -> Option.map (intern_type (slide_binders env')) rtnpo (* Only PatVar in "in" clauses *) | l -> (* Build a return predicate by expansion of the patterns of the "in" clause *) let thevars, thepats = List.split l in @@ -2071,7 +2153,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let sub_tms = List.map (fun id -> (DAst.make @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in let main_sub_eqn = CAst.make @@ ([],thepats, (* "|p1,..,pn" *) - Option.cata (intern_type env') + Option.cata (intern_type_no_implicit env') (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,IntroAnonymous,None)) rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in let catch_all_sub_eqn = @@ -2090,7 +2172,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let p' = Option.map (fun u -> let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env') (CAst.make na') in - intern_type env'' u) po in + intern_type (slide_binders env'') u) po in DAst.make ?loc @@ GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b', intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) @@ -2100,7 +2182,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let p' = Option.map (fun p -> let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env) (CAst.make na') in - intern_type env'' p) po in + intern_type (slide_binders env'') p) po in DAst.make ?loc @@ GIf (c', (na', p'), intern env b1, intern env b2) | CHole (k, naming, solve) -> @@ -2160,18 +2242,20 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = GSort s | CCast (c1, c2) -> DAst.make ?loc @@ - GCast (intern env c1, map_cast_type (intern_type env) c2) + GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2) ) and intern_type env = intern (set_type_scope env) - and intern_no_implicit env = intern {env with impl_binder_index = None} + and intern_type_no_implicit env = intern (restart_no_binders (set_type_scope env)) + + and intern_no_implicit env = intern (restart_no_binders env) - and intern_restart_implicit env = intern {env with impl_binder_index = Some 0} + and intern_restart_binders env = intern (restart_lambda_binders env) - and intern_type_restart_implicit env = intern {(set_type_scope env) with impl_binder_index = Some 0} + and intern_type_restart_binders env = intern (restart_prod_binders (set_type_scope env)) and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list = - intern_local_binder_aux intern_restart_implicit ntnvars 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 pl = @@ -2198,7 +2282,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in List.map (fun (asubst,pl) -> let rhs = replace_vars_constr_expr asubst rhs in - let rhs' = intern {env with ids = env_ids} rhs in + let rhs' = intern_no_implicit {env with ids = env_ids} rhs in CAst.make ?loc (eqn_ids,pl,rhs')) pll and intern_case_item env forbidden_names_for_gen (tm,na,t) = @@ -2336,7 +2420,12 @@ let extract_ids env = let scope_of_type_kind sigma = function | IsType -> Notation.current_type_scope_name () | OfType typ -> compute_type_scope sigma typ - | WithoutTypeConstraint -> None + | WithoutTypeConstraint | UnknownIfTermOrType -> None + +let allowed_binder_kind_of_type_kind = function + | IsType -> Some AbsPi + | OfType _ | WithoutTypeConstraint -> Some AbsLambda + | UnknownIfTermOrType -> None let empty_ltac_sign = { ltac_vars = Id.Set.empty; @@ -2348,9 +2437,10 @@ let intern_gen kind env sigma ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) c = let tmp_scope = scope_of_type_kind sigma kind in + let k = allowed_binder_kind_of_type_kind kind in internalize env {ids = extract_ids env; unb = false; tmp_scope = tmp_scope; scopes = []; - impls; impl_binder_index = Some 0} + impls; binder_block_names = Some (k,Id.Map.domain impls)} pattern_mode (ltacvars, Id.Map.empty) c let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c @@ -2372,8 +2462,8 @@ let interp_gen kind env sigma ?(impls=empty_internalization_env) c = let c = intern_gen kind ~impls env sigma c in understand ~expected_type:kind env sigma c -let interp_constr env sigma ?(impls=empty_internalization_env) c = - interp_gen WithoutTypeConstraint env sigma c +let interp_constr ?(expected_type=WithoutTypeConstraint) env sigma ?(impls=empty_internalization_env) c = + interp_gen expected_type env sigma c let interp_type env sigma ?(impls=empty_internalization_env) c = interp_gen IsType env sigma ~impls c @@ -2383,8 +2473,8 @@ let interp_casted_constr env sigma ?(impls=empty_internalization_env) c typ = (* Not all evars expected to be resolved *) -let interp_open_constr env sigma c = - understand_tcc env sigma (intern_constr env sigma c) +let interp_open_constr ?(expected_type=WithoutTypeConstraint) env sigma c = + understand_tcc env sigma (intern_gen expected_type env sigma c) (* Not all evars expected to be resolved and computation of implicit args *) @@ -2432,8 +2522,10 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c = let tmp_scope = scope_of_type_kind sigma kind in let impls = empty_internalization_env in + let k = allowed_binder_kind_of_type_kind kind in internalize env - {ids; unb = false; tmp_scope; scopes = []; impls; impl_binder_index = Some 0} + {ids; unb = false; tmp_scope; scopes = []; impls; + binder_block_names = Some (k,Id.Set.empty)} pattern_mode (ltacvars, vl) c let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = @@ -2442,7 +2534,7 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in let c = internalize env - {ids; unb = false; tmp_scope = None; scopes = []; impls; impl_binder_index = None} + {ids; unb = false; tmp_scope = None; scopes = []; impls; binder_block_names = None} false (empty_ltac_sign, vl) a in (* Splits variables into those that are binding, bound, or both *) (* Translate and check that [c] has all its free variables bound in [vars] *) @@ -2473,13 +2565,17 @@ let my_intern_constr env lvar acc c = let intern_context env impl_env binders = try let lvar = (empty_ltac_sign, Id.Map.empty) in + let ids = + (* We assume all ids around are parts of the prefix of the current + context being interpreted *) + extract_ids env in let lenv, bl = List.fold_left (fun (lenv, bl) b -> let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in (env, bl)) - ({ids = extract_ids env; unb = false; + ({ids; unb = false; tmp_scope = None; scopes = []; impls = impl_env; - impl_binder_index = Some 0}, []) binders in + binder_block_names = Some (Some AbsPi,ids)}, []) binders in (lenv.impls, List.map glob_local_binder_of_extended bl) with InternalizationError (loc,e) -> user_err ?loc ~hdr:"internalize" (explain_internalization_error e) @@ -2500,8 +2596,10 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = let r = Retyping.relevance_of_type env sigma t in let d = LocalAssum (make_annot na r,t) in let impls = - if k == Implicit then CAst.make (Some (na,true)) :: impls - else CAst.make None :: impls + match k with + | NonMaxImplicit -> CAst.make (Some (na,false)) :: impls + | MaxImplicit -> CAst.make (Some (na,true)) :: impls + | Explicit -> CAst.make None :: impls in (push_rel d env, sigma, d::params, succ n, impls) | Some b -> |