diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 1794 |
1 files changed, 1008 insertions, 786 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b6f18fe3..68f0050d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1,33 +1,50 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp +open Errors open Util -open Flags open Names open Nameops open Namegen open Libnames +open Globnames open Impargs open Glob_term -open Pattern +open Glob_ops +open Patternops open Pretyping open Cases +open Constrexpr +open Constrexpr_ops +open Notation_term +open Notation_ops open Topconstr open Nametab open Notation open Inductiveops +open Decl_kinds + +(** constr_expr -> glob_constr translation: + - it adds holes for implicit arguments + - it remplaces notations by their value (scopes stuff are here) + - it recognizes global vars from local ones + - it prepares pattern maching problems (a pattern becomes a tree where nodes + are constructor/variable pairs and leafs are variables) + + All that at once, fasten your seatbelt! +*) (* To interpret implicits and arg scopes of variables in inductive types and recursive definitions and of projection names in records *) type var_internalization_type = - | Inductive of identifier list (* list of params *) + | Inductive of Id.t list (* list of params *) | Recursive | Method | Variable @@ -38,16 +55,21 @@ type var_internalization_data = var_internalization_type * (* impargs to automatically add to the variable, e.g. for "JMeq A a B b" in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) - identifier list * + Id.t list * (* signature of impargs of the variable *) Impargs.implicit_status list * (* subscopes of the args of the variable *) scope_name option list type internalization_env = - (var_internalization_data) Idmap.t + (var_internalization_data) Id.Map.t + +type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) -type glob_binder = (name * binding_kind * glob_constr option * glob_constr) +type ltac_sign = { + ltac_vars : Id.Set.t; + ltac_bound : Id.Set.t; +} let interning_grammar = ref false @@ -75,38 +97,33 @@ let global_reference_of_reference ref = locate_reference (snd (qualid_of_reference ref)) let global_reference id = - constr_of_global (locate_reference (qualid_of_ident id)) + Universes.constr_of_global (locate_reference (qualid_of_ident id)) let construct_reference ctx id = try - Term.mkVar (let _ = Sign.lookup_named id ctx in id) + Term.mkVar (let _ = Context.lookup_named id ctx in id) with Not_found -> global_reference id let global_reference_in_absolute_module dir id = - constr_of_global (Nametab.global_of_path (Libnames.make_path dir id)) + Universes.constr_of_global (Nametab.global_of_path (Libnames.make_path dir id)) (**********************************************************************) (* Internalization errors *) type internalization_error = - | VariableCapture of identifier - | WrongExplicitImplicit + | VariableCapture of Id.t * Id.t | IllegalMetavariable | NotAConstructor of reference - | UnboundFixName of bool * identifier - | NonLinearPattern of identifier + | UnboundFixName of bool * Id.t + | NonLinearPattern of Id.t | BadPatternsNumber of int * int - | BadExplicitationNumber of explicitation * int option -exception InternalizationError of loc * internalization_error +exception InternalizationError of Loc.t * internalization_error -let explain_variable_capture id = - str "The variable " ++ pr_id id ++ str " occurs in its type" - -let explain_wrong_explicit_implicit = - str "Found an explicitly given implicit argument but was expecting" ++ - fnl () ++ str "a regular one" +let explain_variable_capture id id' = + pr_id id ++ str " is dependent in the type of " ++ pr_id id' ++ + strbrk ": cannot interpret both of them with the same type" let explain_illegal_metavariable = str "Metavariables allowed only in patterns" @@ -123,44 +140,31 @@ let explain_non_linear_pattern id = str "The variable " ++ pr_id id ++ str " is bound several times in pattern" let explain_bad_patterns_number n1 n2 = - str "Expecting " ++ int n1 ++ str (plural n1 " pattern") ++ + str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++ str " but found " ++ int n2 -let explain_bad_explicitation_number n po = - match n with - | ExplByPos (n,_id) -> - let s = match po with - | None -> str "a regular argument" - | Some p -> int p in - str "Bad explicitation number: found " ++ int n ++ - str" but was expecting " ++ s - | ExplByName id -> - let s = match po with - | None -> str "a regular argument" - | Some p -> (*pr_id (name_of_position p) in*) failwith "" in - str "Bad explicitation name: found " ++ pr_id id ++ - str" but was expecting " ++ s - let explain_internalization_error e = let pp = match e with - | VariableCapture id -> explain_variable_capture id - | WrongExplicitImplicit -> explain_wrong_explicit_implicit + | VariableCapture (id,id') -> explain_variable_capture id id' | IllegalMetavariable -> explain_illegal_metavariable | NotAConstructor ref -> explain_not_a_constructor ref | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id | NonLinearPattern id -> explain_non_linear_pattern id | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 - | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po in - pp ++ str "." + in pp ++ str "." let error_bad_inductive_type loc = user_err_loc (loc,"",str - "This should be an inductive type applied to names or \"_\".") + "This should be an inductive type applied to patterns.") -let error_inductive_parameter_not_implicit loc = +let error_parameter_not_implicit loc = user_err_loc (loc,"", str - ("The parameters of inductive types do not bind in\n"^ - "the 'return' clauses; they must be replaced by '_' in the 'in' clauses.")) + "The parameters do not bind in patterns;" ++ spc () ++ str + "they must be replaced by '_'.") + +let error_ldots_var loc = + user_err_loc (loc,"",str "Special token " ++ pr_id ldots_var ++ + str " is for use in the Notation command.") (**********************************************************************) (* Pre-computing the implicit arguments and arguments scopes needed *) @@ -168,12 +172,12 @@ let error_inductive_parameter_not_implicit loc = let parsing_explicit = ref false -let empty_internalization_env = Idmap.empty +let empty_internalization_env = Id.Map.empty let compute_explicitable_implicit imps = function | Inductive params -> (* In inductive types, the parameters are fixed implicit arguments *) - let sub_impl,_ = list_chop (List.length params) imps in + let sub_impl,_ = List.chop (List.length params) imps in let sub_impl' = List.filter is_status_implicit sub_impl in List.map name_of_implicit sub_impl' | Recursive | Method | Variable -> @@ -186,25 +190,25 @@ let compute_internalization_data env ty typ impl = (ty, expls_impl, impl, compute_arguments_scope typ) let compute_internalization_env env ty = - list_fold_left3 - (fun map id typ impl -> Idmap.add id (compute_internalization_data env ty typ impl) map) + List.fold_left3 + (fun map id typ impl -> Id.Map.add id (compute_internalization_data env ty typ impl) map) empty_internalization_env (**********************************************************************) (* Contracting "{ _ }" in notations *) let rec wildcards ntn n = - if n = String.length ntn then [] - else let l = spaces ntn (n+1) in if ntn.[n] = '_' then n::l else l + if Int.equal n (String.length ntn) then [] + else let l = spaces ntn (n+1) in if ntn.[n] == '_' then n::l else l and spaces ntn n = - if n = String.length ntn then [] - else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1) + if Int.equal n (String.length ntn) then [] + else if ntn.[n] == ' ' then wildcards ntn (n+1) else spaces ntn (n+1) let expand_notation_string ntn n = let pos = List.nth (wildcards ntn 0) n in - let hd = if pos = 0 then "" else String.sub ntn 0 pos in + let hd = if Int.equal pos 0 then "" else String.sub ntn 0 pos in let tl = - if pos = String.length ntn then "" + if Int.equal pos (String.length ntn) then "" else String.sub ntn (pos+1) (String.length ntn - pos -1) in hd ^ "{ _ }" ^ tl @@ -227,7 +231,7 @@ let contract_pat_notation ntn (l,ll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | CPatNotation (_,"{ _ }",([a],[])) :: l -> + | CPatNotation (_,"{ _ }",([a],[]),[]) :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> @@ -237,19 +241,19 @@ let contract_pat_notation ntn (l,ll) = !ntn',(l,ll) type intern_env = { - ids: Names.Idset.t; + ids: Names.Id.Set.t; unb: bool; - tmp_scope: Topconstr.tmp_scope_name option; - scopes: Topconstr.scope_name list; + tmp_scope: Notation_term.tmp_scope_name option; + scopes: Notation_term.scope_name list; impls: internalization_env } (**********************************************************************) (* Remembering the parsing scope of variables in notations *) -let make_current_scope = function - | (Some tmp_scope,(sc::_ as scopes)) when sc = tmp_scope -> scopes - | (Some tmp_scope,scopes) -> tmp_scope::scopes - | None,scopes -> scopes +let make_current_scope tmp scopes = match tmp, scopes with +| Some tmp_scope, (sc :: _) when String.equal sc tmp_scope -> scopes +| Some tmp_scope, scopes -> tmp_scope :: scopes +| None, scopes -> scopes let pr_scope_stack = function | [] -> str "the empty scope stack" @@ -263,10 +267,6 @@ let error_inconsistent_scope loc id scopes1 scopes2 = pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++ pr_scope_stack scopes1) -let error_expect_constr_notation_type loc id = - user_err_loc (loc,"", - pr_id id ++ str " is bound in the notation to a term variable.") - let error_expect_binder_notation_type loc id = user_err_loc (loc,"", pr_id id ++ @@ -274,18 +274,17 @@ let error_expect_binder_notation_type loc id = let set_var_scope loc id istermvar env ntnvars = try - let idscopes,typ = List.assoc id ntnvars in - if istermvar then + let idscopes,typ = Id.Map.find id ntnvars in + let () = if istermvar then (* scopes have no effect on the interpretation of identifiers *) - if !idscopes = None then - idscopes := Some (env.tmp_scope,env.scopes) - else - if make_current_scope (Option.get !idscopes) - <> make_current_scope (env.tmp_scope,env.scopes) - then - error_inconsistent_scope loc id - (make_current_scope (Option.get !idscopes)) - (make_current_scope (env.tmp_scope,env.scopes)); + begin match !idscopes with + | None -> idscopes := Some (env.tmp_scope, env.scopes) + | Some (tmp, scope) -> + let s1 = make_current_scope tmp scope in + let s2 = make_current_scope env.tmp_scope env.scopes in + if not (List.equal String.equal s1 s2) then error_inconsistent_scope loc id s1 s2 + end + in match typ with | NtnInternTypeBinder -> if istermvar then error_expect_binder_notation_type loc id @@ -303,14 +302,14 @@ let set_type_scope env = {env with tmp_scope = Some Notation.type_scope} let reset_tmp_scope env = {env with tmp_scope = None} -let rec it_mkGProd env body = +let rec it_mkGProd loc2 env body = match env with - (na, bk, _, t) :: tl -> it_mkGProd tl (GProd (dummy_loc, na, bk, t, body)) + (loc1, (na, bk, _, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body)) | [] -> body -let rec it_mkGLambda env body = +let rec it_mkGLambda loc2 env body = match env with - (na, bk, _, t) :: tl -> it_mkGLambda tl (GLambda (dummy_loc, na, bk, t, body)) + (loc1, (na, bk, _, t)) :: tl -> it_mkGLambda loc2 tl (GLambda (Loc.merge loc1 loc2, na, bk, t, body)) | [] -> body (**********************************************************************) @@ -318,7 +317,7 @@ let rec it_mkGLambda env body = let build_impls = function |Implicit -> (function |Name id -> Some (id, Impargs.Manual, (true,true)) - |Anonymous -> anomaly "Anonymous implicit argument") + |Anonymous -> anomaly (Pp.str "Anonymous implicit argument")) |Explicit -> fun _ -> None let impls_type_list ?(args = []) = @@ -337,30 +336,32 @@ let impls_term_list ?(args = []) = |_ -> (Variable,[],List.append args (List.rev acc),[]) in aux [] -let check_capture loc ty = function - | Name id when occur_var_constr_expr id ty -> - raise (InternalizationError (loc,VariableCapture id)) - | _ -> +(* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *) +let rec check_capture ty = function + | (loc,Name id)::(_,Name id')::_ when occur_glob_constr id ty -> + raise (InternalizationError (loc,VariableCapture (id,id'))) + | _::nal -> + check_capture ty nal + | [] -> () -let locate_if_isevar loc na = function - | GHole _ -> +let locate_if_hole loc na = function + | GHole (_,_,naming,arg) -> (try match na with - | Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id) + | Name id -> glob_constr_of_notation_constr loc + (Reserve.find_reserved_type id) | Anonymous -> raise Not_found - with Not_found -> GHole (loc, Evd.BinderType na)) + with Not_found -> GHole (loc, Evar_kinds.BinderType na, naming, arg)) | x -> x let reset_hidden_inductive_implicit_test env = - { env with impls = Idmap.fold (fun id x -> - let x = match x with + { env with impls = Id.Map.map (function | (Inductive _,b,c,d) -> (Inductive [],b,c,d) - | x -> x - in Idmap.add id x) env.impls Idmap.empty } + | x -> x) env.impls } let check_hidden_implicit_parameters id impls = - if Idmap.exists (fun _ -> function - | (Inductive indparams,_,_,_) -> List.mem id indparams + if Id.Map.exists (fun _ -> function + | (Inductive indparams,_,_,_) -> Id.List.mem id indparams | _ -> false) impls then errorlabstrm "" (strbrk "A parameter of an inductive type " ++ @@ -374,14 +375,17 @@ let push_name_env ?(global_level=false) lvar implargs env = env | loc,Name id -> check_hidden_implicit_parameters id env.impls ; - set_var_scope loc id false env (let (_,ntnvars) = lvar in ntnvars); + 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; if global_level then Dumpglob.dump_definition (loc,id) true "var" else Dumpglob.dump_binding loc id; - {env with ids = Idset.add id env.ids; impls = Idmap.add id implargs env.impls} + {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} let intern_generalized_binder ?(global_level=false) intern_type lvar - env bl (loc, na) b b' t ty = - let ids = (match na with Anonymous -> fun x -> x | Name na -> Idset.add na) env.ids in + env (loc, na) b b' t ty = + let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in let ty, ids' = if t then ty, ids else Implicit_quantifiers.implicit_application ids @@ -392,7 +396,11 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar let env' = List.fold_left (fun env (x, l) -> push_name_env ~global_level lvar (Variable,[],[],[])(*?*) env (l, Name x)) env fvs in - let bl = List.map (fun (id, loc) -> (Name id, b, None, GHole (loc, Evd.BinderType (Name id)))) fvs in + let bl = List.map + (fun (id, loc) -> + (loc, (Name id, b, None, GHole (loc, Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) + fvs + in let na = match na with | Anonymous -> if global_level then na @@ -400,183 +408,221 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar let name = let id = match ty with - | CApp (_, (_, CRef (Ident (loc,id))), _) -> id - | _ -> id_of_string "H" + | CApp (_, (_, CRef (Ident (loc,id),_)), _) -> id + | _ -> default_non_dependent_ident in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name | _ -> na - in (push_name_env ~global_level lvar (impls_type_list ty')(*?*) env' (loc,na)), (na,b',None,ty') :: List.rev bl - -let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,bl) = function + in (push_name_env ~global_level lvar (impls_type_list ty')(*?*) env' (loc,na)), (loc,(na,b',None,ty')) :: List.rev bl + +let intern_assumption intern lvar env nal bk ty = + let intern_type env = intern (set_type_scope env) in + match bk with + | Default k -> + let ty = intern_type env ty in + check_capture ty nal; + let impls = impls_type_list ty in + List.fold_left + (fun (env, bl) (loc, na as locna) -> + (push_name_env lvar impls env locna, + (loc,(na,k,None,locate_if_hole loc na ty))::bl)) + (env, []) nal + | Generalized (b,b',t) -> + let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in + env, b + +let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function | LocalRawAssum(nal,bk,ty) -> - (match bk with - | Default k -> - let ty = intern_type env ty in - let impls = impls_type_list ty in - List.fold_left - (fun (env,bl) (loc,na as locna) -> - (push_name_env lvar impls env locna, - (na,k,None,locate_if_isevar loc na ty)::bl)) - (env,bl) nal - | Generalized (b,b',t) -> - let env, b = intern_generalized_binder ~global_level intern_type lvar env bl (List.hd nal) b b' t ty in - env, b @ bl) + let env, bl' = intern_assumption intern lvar env nal bk ty 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, - (na,Explicit,Some(indef),GHole(loc,Evd.BinderType na))::bl) + (loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)))::bl) let intern_generalization intern env lvar loc bk ak c = let c = intern {env with unb = true} c in let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:env.ids c in let env', c' = let abs = - let pi = - match ak with + let pi = match ak with | Some AbsPi -> true - | None when env.tmp_scope = Some Notation.type_scope - || List.mem Notation.type_scope env.scopes -> true - | _ -> false + | Some _ -> false + | None -> + let is_type_scope = match env.tmp_scope with + | None -> false + | Some sc -> String.equal sc Notation.type_scope + in + is_type_scope || + String.List.mem Notation.type_scope env.scopes in if pi then (fun (id, loc') acc -> - GProd (join_loc loc' loc, Name id, bk, GHole (loc', Evd.BinderType (Name id)), acc)) + GProd (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) else (fun (id, loc') acc -> - GLambda (join_loc loc' loc, Name id, bk, GHole (loc', Evd.BinderType (Name id)), acc)) + GLambda (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) in List.fold_right (fun (id, loc as lid) (env, acc) -> let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in (env', abs lid acc)) fvs (env,c) in c' -let iterate_binder intern lvar (env,bl) = function - | LocalRawAssum(nal,bk,ty) -> - let intern_type env = intern (set_type_scope env) in - (match bk with - | Default k -> - let ty = intern_type env ty in - let impls = impls_type_list ty in - List.fold_left - (fun (env,bl) (loc,na as locna) -> - (push_name_env lvar impls env locna, - (na,k,None,locate_if_isevar loc na ty)::bl)) - (env,bl) nal - | Generalized (b,b',t) -> - let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in - env, b @ bl) - | LocalRawDef((loc,na as locna),def) -> - let indef = intern env def in - (push_name_env lvar (impls_term_list indef) env locna, - (na,Explicit,Some(indef),GHole(loc,Evd.BinderType na))::bl) - (**********************************************************************) (* Syntax extensions *) let option_mem_assoc id = function - | Some (id',c) -> id = id' + | Some (id',c) -> Id.equal id id' | None -> false -let find_fresh_name renaming (terms,termlists,binders) id = - let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) terms in - let fvs2 = List.flatten (List.map (fun (_,(l,_)) -> List.map free_vars_of_constr_expr l) termlists) in - let fvs3 = List.map snd renaming in +let find_fresh_name renaming (terms,termlists,binders) avoid id = + let fold1 _ (c, _) accu = Id.Set.union (free_vars_of_constr_expr c) accu in + let fold2 _ (l, _) accu = + let fold accu c = Id.Set.union (free_vars_of_constr_expr c) accu in + List.fold_left fold accu l + in + let fold3 _ x accu = Id.Set.add x accu in + let fvs1 = Id.Map.fold fold1 terms avoid in + let fvs2 = Id.Map.fold fold2 termlists fvs1 in + let fvs3 = Id.Map.fold fold3 renaming fvs2 in (* TODO binders *) - let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in - next_ident_away id fvs + next_ident_away_from id (fun id -> Id.Set.mem id fvs3) -let traverse_binder (terms,_,_ as subst) - (renaming,env)= - function +let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function | Anonymous -> (renaming,env),Anonymous | Name id -> try (* Binders bound in the notation are considered first-order objects *) - let _,na = coerce_to_name (fst (List.assoc id terms)) in - (renaming,{env with ids = name_fold Idset.add na env.ids}), na + let _,na = coerce_to_name (fst (Id.Map.find id terms)) in + (renaming,{env with ids = name_fold Id.Set.add na env.ids}), na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) - let id' = find_fresh_name renaming subst id in - let renaming' = if id=id' then renaming else (id,id')::renaming in + let id' = find_fresh_name renaming subst avoid id in + let renaming' = + if Id.equal id id' then renaming else Id.Map.add id id' renaming + in (renaming',env), Name id' -let make_letins loc = List.fold_right (fun (na,b,t) c -> GLetIn (loc,na,b,c)) +let make_letins = List.fold_right (fun (loc,(na,b,t)) c -> GLetIn (loc,na,b,c)) let rec subordinate_letins letins = function (* binders come in reverse order; the non-let are returned in reverse order together *) (* with the subordinated let-in in writing order *) - | (na,_,Some b,t)::l -> - subordinate_letins ((na,b,t)::letins) l - | (na,bk,None,t)::l -> + | (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 - letins',((na,bk,t),letins)::rest + letins',((loc,(na,bk,t)),letins)::rest | [] -> letins,[] let rec subst_iterator y t = function - | GVar (_,id) as x -> if id = y then t else x + | GVar (_,id) as x -> if Id.equal id y then t else x | x -> map_glob_constr (subst_iterator y t) x -let subst_aconstr_in_glob_constr loc intern lvar subst infos c = +let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) 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) *) + let avoid = Id.Map.domain ntnvars in let rec aux (terms,binderopt as subst') (renaming,env) c = let subinfos = renaming,{env with tmp_scope = None} in match c with - | AVar id -> - begin - (* subst remembers the delimiters stack in the interpretation *) - (* of the notations *) - try - let (a,(scopt,subscopes)) = List.assoc id terms in - intern {env with tmp_scope = scopt; - scopes = subscopes @ env.scopes} a - with Not_found -> - try - GVar (loc,List.assoc id renaming) - with Not_found -> - (* Happens for local notation joint with inductive/fixpoint defs *) - GVar (loc,id) - end - | AList (x,_,iter,terminator,lassoc) -> + | NVar id -> subst_var subst' (renaming, env) id + | NList (x,_,iter,terminator,lassoc) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) - let (l,(scopt,subscopes)) = List.assoc x termlists in + let (l,(scopt,subscopes)) = Id.Map.find x termlists in let termin = aux subst' subinfos terminator in - List.fold_right (fun a t -> - subst_iterator ldots_var t - (aux ((x,(a,(scopt,subscopes)))::terms,binderopt) subinfos iter)) - (if lassoc then List.rev l else l) termin + let fold a t = + let nterms = Id.Map.add x (a, (scopt, subscopes)) terms in + subst_iterator ldots_var t (aux (nterms, binderopt) subinfos iter) + in + List.fold_right fold (if lassoc then List.rev l else l) termin with Not_found -> - anomaly "Inconsistent substitution of recursive notation") - | AHole (Evd.BinderType (Name id as na)) -> - let na = - try snd (coerce_to_name (fst (List.assoc id terms))) - with Not_found -> na in - GHole (loc,Evd.BinderType na) - | ABinderList (x,_,iter,terminator) -> + anomaly (Pp.str "Inconsistent substitution of recursive notation")) + | NHole (knd, naming, arg) -> + let knd = match knd with + | Evar_kinds.BinderType (Name id as na) -> + let na = + try snd (coerce_to_name (fst (Id.Map.find id terms))) + with Not_found -> + try Name (Id.Map.find id renaming) + with Not_found -> na + in + Evar_kinds.BinderType na + | _ -> knd + in + let arg = match arg with + | None -> None + | Some arg -> + let open Tacexpr in + let open Genarg in + let wit = glbwit Constrarg.wit_tactic in + let body = + if has_type arg wit then out_gen wit arg + else assert false (** FIXME *) + in + let mk_env id (c, (tmp_scope, subscopes)) accu = + let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in + let gc = intern nenv c in + let c = ConstrMayEval (Genredexpr.ConstrTerm (gc, Some c)) in + ((loc, id), c) :: accu + in + let bindings = Id.Map.fold mk_env terms [] in + let tac = TacLetIn (false, bindings, body) in + let arg = in_gen wit tac in + Some arg + in + GHole (loc, knd, naming, arg) + | NBinderList (x,_,iter,terminator) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) - let (bl,(scopt,subscopes)) = List.assoc x binders in - let env,bl = List.fold_left (iterate_binder intern lvar) (env,[]) bl in + 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 termin = aux subst' (renaming,env) terminator in let res = List.fold_left (fun t binder -> subst_iterator ldots_var t (aux (terms,Some(x,binder)) subinfos iter)) termin bl in - make_letins loc letins res + make_letins letins res with Not_found -> - anomaly "Inconsistent substitution of recursive notation") - | AProd (Name id, AHole _, c') when option_mem_assoc id binderopt -> - let (na,bk,t),letins = snd (Option.get binderopt) in - GProd (loc,na,bk,t,make_letins loc letins (aux subst' infos c')) - | ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt -> - let (na,bk,t),letins = snd (Option.get binderopt) in - GLambda (loc,na,bk,t,make_letins loc letins (aux subst' infos c')) + 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')) + | 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')) + (* 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' -> + let subinfos,na = traverse_binder subst avoid subinfos na in + let ty = GHole (loc,Evar_kinds.BinderType na,naming,arg) in + GProd (loc,na,Explicit,ty,aux subst' subinfos c') + | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c') + when Name.equal na na' -> + let subinfos,na = traverse_binder subst avoid subinfos na in + let ty = GHole (loc,Evar_kinds.BinderType na,naming,arg) in + GLambda (loc,na,Explicit,ty,aux subst' subinfos c') | t -> - glob_constr_of_aconstr_with_binders loc (traverse_binder subst) - (aux subst') subinfos t + glob_constr_of_notation_constr_with_binders loc + (traverse_binder subst avoid) (aux subst') subinfos t + and subst_var (terms, binderopt) (renaming, env) id = + (* subst remembers the delimiters stack in the interpretation *) + (* of the notations *) + try + let (a,(scopt,subscopes)) = Id.Map.find id terms in + intern {env with tmp_scope = scopt; + scopes = subscopes @ env.scopes} a + with Not_found -> + try + GVar (loc, Id.Map.find id renaming) + with Not_found -> + (* Happens for local notation joint with inductive/fixpoint defs *) + GVar (loc,id) in aux (terms,None) infos c let split_by_type ids = @@ -586,7 +632,9 @@ let split_by_type ids = | NtnTypeConstrList -> (l1,(x,scl)::l2,l3) | NtnTypeBinderList -> (l1,l2,(x,scl)::l3)) ids ([],[],[]) -let make_subst ids l = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids l +let make_subst ids l = + let fold accu (id, scl) a = Id.Map.add id (a, scl) accu in + List.fold_left2 fold Id.Map.empty ids l let intern_notation intern env lvar loc ntn fullargs = let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in @@ -597,7 +645,7 @@ let intern_notation intern env lvar loc ntn fullargs = let termlists = make_subst idsl argslist in let binders = make_subst idsbl bll in subst_aconstr_in_glob_constr loc intern lvar - (terms,termlists,binders) ([],env) c + (terms, termlists, binders) (Id.Map.empty, env) c (**********************************************************************) (* Discriminating between bound variables and global references *) @@ -609,39 +657,35 @@ let string_of_ty = function | Variable -> "var" let intern_var genv (ltacvars,ntnvars) namedctx loc id = - let (ltacvars,unbndltacvars) = ltacvars in (* Is [id] an inductive type potentially with implicit *) try - let ty,expl_impls,impls,argsc = Idmap.find id genv.impls in + let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in let expl_impls = List.map - (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in + (fun id -> CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in let tys = string_of_ty ty in - Dumpglob.dump_reference loc "<>" (string_of_id id) tys; + Dumpglob.dump_reference loc "<>" (Id.to_string id) tys; GVar (loc,id), make_implicits_list impls, argsc, expl_impls with Not_found -> (* Is [id] bound in current term or is an ltac var bound to constr *) - if Idset.mem id genv.ids or List.mem id ltacvars + if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars then GVar (loc,id), [], [], [] (* Is [id] a notation variable *) - - else if List.mem_assoc id ntnvars + else if Id.Map.mem id ntnvars then (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], []) (* Is [id] the special variable for recursive notations *) - else if ntnvars <> [] && id = ldots_var - then - GVar (loc,id), [], [], [] + else if Id.equal id ldots_var + then if Id.Map.is_empty ntnvars + then error_ldots_var loc + else GVar (loc,id), [], [], [] + else if Id.Set.mem id ltacvars.ltac_bound then + (* Is [id] bound to a free name in ltac (this is an ltac error message) *) + user_err_loc (loc,"intern_var", + str "variable " ++ pr_id id ++ str " should be bound to a term.") else - (* Is [id] bound to a free name in ltac (this is an ltac error message) *) - try - match List.assoc id unbndltacvars with - | None -> user_err_loc (loc,"intern_var", - str "variable " ++ pr_id id ++ str " should be bound to a term.") - | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0 - with Not_found -> (* Is [id] a goal or section variable *) - let _ = Sign.lookup_named id namedctx in + let _ = Context.lookup_named id namedctx in try (* [id] a section variable *) (* Redundant: could be done in intern_qualid *) @@ -649,128 +693,171 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var"; - GRef (loc, ref), impls, scopes, [] + GRef (loc, ref, None), impls, scopes, [] with e when Errors.noncritical e -> (* [id] a goal variable *) GVar (loc,id), [], [], [] -let find_appl_head_data = function - | GRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[] - | GApp (_,GRef (_,ref),l) as x - when l <> [] & Flags.version_strictly_greater Flags.V8_2 -> +let proj_impls r impls = + let env = Global.env () in + let f (x, l) = x, projection_implicits env r l in + List.map f impls + +let proj_scopes n scopes = + List.skipn_at_least n scopes + +let proj_impls_scopes p impls scopes = + match p with + | Some (r, n) -> proj_impls r impls, proj_scopes n scopes + | None -> impls, scopes + +let find_appl_head_data c = + match c with + | GRef (loc,ref,_) as x -> + let impls = implicits_of_global ref in + let scopes = find_arguments_scope ref in + x, impls, scopes, [] + | GApp (_,GRef (_,ref,_),l) as x + when l != [] && Flags.version_strictly_greater Flags.V8_2 -> let n = List.length l in - x,List.map (drop_first_implicits n) (implicits_of_global ref), - list_skipn_at_least n (find_arguments_scope ref),[] + let impls = implicits_of_global ref in + let scopes = find_arguments_scope ref in + x, List.map (drop_first_implicits n) impls, + List.skipn_at_least n scopes,[] | x -> x,[],[],[] let error_not_enough_arguments loc = user_err_loc (loc,"",str "Abbreviation is not applied enough.") let check_no_explicitation l = - let l = List.filter (fun (a,b) -> b <> None) l in - if l <> [] then - let loc = fst (Option.get (snd (List.hd l))) in - user_err_loc - (loc,"",str"Unexpected explicitation of the argument of an abbreviation.") + let is_unset (a, b) = match b with None -> false | Some _ -> true in + let l = List.filter is_unset l in + match l with + | [] -> () + | (_, None) :: _ -> assert false + | (_, Some (loc, _)) :: _ -> + user_err_loc (loc,"",str"Unexpected explicitation of the argument of an abbreviation.") let dump_extended_global loc = function - | TrueGlobal ref -> Dumpglob.add_glob loc ref + | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob loc ref | SynDef sp -> Dumpglob.add_glob_kn loc sp let intern_extended_global_of_qualid (loc,qid) = - try let r = Nametab.locate_extended qid in dump_extended_global loc r; r - with Not_found -> error_global_not_found_loc loc qid + let r = Nametab.locate_extended qid in dump_extended_global loc r; r let intern_reference ref = - Smartlocate.global_of_extended_global - (intern_extended_global_of_qualid (qualid_of_reference ref)) + let qid = qualid_of_reference ref in + let r = + try intern_extended_global_of_qualid qid + with Not_found -> error_global_not_found_loc (fst qid) (snd qid) + in + Smartlocate.global_of_extended_global r (* Is it a global reference or a syntactic definition? *) -let intern_qualid loc qid intern env lvar args = +let intern_qualid loc qid intern env lvar us args = match intern_extended_global_of_qualid (loc,qid) with - | TrueGlobal ref -> - GRef (loc, ref), args + | TrueGlobal ref -> GRef (loc, ref, us), true, args | SynDef sp -> let (ids,c) = Syntax_def.search_syntactic_definition sp in let nids = List.length ids in if List.length args < nids then error_not_enough_arguments loc; - let args1,args2 = list_chop nids args in + let args1,args2 = List.chop nids args in check_no_explicitation args1; - let subst = make_subst ids (List.map fst args1) in - subst_aconstr_in_glob_constr loc intern lvar (subst,[],[]) ([],env) c, args2 + let terms = make_subst ids (List.map fst args1) in + let subst = (terms, Id.Map.empty, Id.Map.empty) in + let infos = (Id.Map.empty, env) in + let projapp = match c with NRef _ -> true | _ -> false in + subst_aconstr_in_glob_constr loc intern lvar subst infos c, projapp, args2 (* Rule out section vars since these should have been found by intern_var *) -let intern_non_secvar_qualid loc qid intern env lvar args = - match intern_qualid loc qid intern env lvar args with - | GRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid +let intern_non_secvar_qualid loc qid intern env lvar us args = + match intern_qualid loc qid intern env lvar us args with + | GRef (_, VarRef _, _),_,_ -> raise Not_found | r -> r -let intern_applied_reference intern env namedctx lvar args = function +let intern_applied_reference intern env namedctx lvar us args = function | Qualid (loc, qid) -> - let r,args2 = intern_qualid loc qid intern env lvar args in - find_appl_head_data r, args2 + let r,projapp,args2 = + try intern_qualid loc qid intern env lvar us args + with Not_found -> error_global_not_found_loc loc qid + in + let x, imp, scopes, l = find_appl_head_data r in + (x,imp,scopes,l), args2 | Ident (loc, id) -> try intern_var env lvar namedctx loc id, args with Not_found -> let qid = qualid_of_ident id in try - let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in - find_appl_head_data r, args2 - with e when Errors.noncritical e -> + let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env lvar us args in + let x, imp, scopes, l = find_appl_head_data r in + (x,imp,scopes,l), args2 + with Not_found -> (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then - (GVar (loc,id), [], [], []),args - else raise e + (GVar (loc,id), [], [], []), args + else error_global_not_found_loc loc qid let interp_reference vars r = let (r,_,_,_),_ = - intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc) - {ids = Idset.empty; unb = false ; + intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost) + {ids = Id.Set.empty; unb = false ; tmp_scope = None; scopes = []; impls = empty_internalization_env} [] - (vars,[]) [] r + (vars, Id.Map.empty) None [] r in r +(**********************************************************************) +(** {5 Cases } *) + +(** {6 Elemtary bricks } *) let apply_scope_env env = function | [] -> {env with tmp_scope = None}, [] | sc::scl -> {env with tmp_scope = sc}, scl let rec simple_adjust_scopes n scopes = - if n=0 then [] else match scopes with + (* Note: they can be less scopes than arguments but also more scopes *) + (* than arguments because extra scopes are used in the presence of *) + (* coercions to funclass *) + if Int.equal n 0 then [] else match scopes with | [] -> None :: simple_adjust_scopes (n-1) [] | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes -let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) = - let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in - let npar = mib.Declarations.mind_nparams in - snd (list_chop (npar + List.length pl1) - (simple_adjust_scopes (npar + List.length pl1 + List.length pl2) - (find_arguments_scope (ConstructRef cstr)))) +let find_remaining_scopes pl1 pl2 ref = + let impls_st = implicits_of_global ref in + let len_pl1 = List.length pl1 in + let len_pl2 = List.length pl2 in + let impl_list = if Int.equal len_pl1 0 + then select_impargs_size len_pl2 impls_st + else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in + let allscs = find_arguments_scope ref in + let scope_list = List.skipn_at_least len_pl1 allscs in + let rec aux = function + |[],l -> l + |_,[] -> [] + |h::t,_::tt when is_status_implicit h -> aux (t,tt) + |_::t,h::tt -> h :: aux (t,tt) + 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))) -(**********************************************************************) -(* Cases *) +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) -> (subst@subst',p::ptail)) ptaill) pl))) - idspl (ids,[[],[]]) - -let simple_product_of_cases_patterns pl = - List.fold_right (fun pl ptaill -> - List.flatten (List.map (fun (subst,p) -> - List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl)) - pl [[],[]] - -(* Check linearity of pattern-matching *) + (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 *) let rec has_duplicate = function | [] -> None - | x::l -> if List.mem x l then (Some x) else has_duplicate l + | x::l -> if Id.List.mem x l then (Some x) else has_duplicate l let loc_of_lhs lhs = - join_loc (fst (List.hd lhs)) (fst (list_last lhs)) + Loc.merge (fst (List.hd lhs)) (fst (List.last lhs)) let check_linearity lhs ids = match has_duplicate ids with @@ -782,167 +869,89 @@ let check_linearity lhs ids = (* Match the number of pattern against the number of matched args *) let check_number_of_pattern loc n l = let p = List.length l in - if n<>p then raise (InternalizationError (loc,BadPatternsNumber (n,p))) + if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p))) let check_or_pat_variables loc ids idsl = - if List.exists (fun ids' -> not (list_eq_set ids ids')) idsl then + if List.exists (fun ids' -> not (List.eq_set Id.equal ids ids')) idsl then user_err_loc (loc, "", str "The components of this disjunctive pattern must bind the same variables.") -let check_constructor_length env loc cstr pl pl0 = - let n = List.length pl + List.length pl0 in - let nargs = Inductiveops.constructor_nrealargs env cstr in - let nhyps = Inductiveops.constructor_nrealhyps env cstr in - if n <> nargs && n <> nhyps (* i.e. with let's *) then - error_wrong_numarg_constructor_loc loc env cstr nargs - -(* Manage multiple aliases *) - - (* [merge_aliases] returns the sets of all aliases encountered at this - point and a substitution mapping extra aliases to the first one *) -let merge_aliases (ids,asubst as _aliases) id = - ids@[id], if ids=[] then asubst else (id, List.hd ids)::asubst - -let alias_of = function - | ([],_) -> Anonymous - | (id::_,_) -> Name id - -let message_redundant_alias (id1,id2) = - if_warn msg_warning - (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2) - -(* Expanding notations *) - -let chop_aconstr_constructor loc (ind,k) args = - if List.length args = 0 then (* Tolerance for a @id notation *) args else - begin - let mib,_ = Global.lookup_inductive ind in - let nparams = mib.Declarations.mind_nparams in - if nparams > List.length args then error_invalid_pattern_notation loc; - let params,args = list_chop nparams args in - List.iter (function AHole _ -> () - | _ -> error_invalid_pattern_notation loc) params; - args - end - -let rec subst_pat_iterator y t (subst,p) = match p with - | PatVar (_,id) as x -> - if id = Name y then t else [subst,x] - | PatCstr (loc,id,l,alias) -> - let l' = List.map (fun a -> (subst_pat_iterator y t ([],a))) l in - let pl = simple_product_of_cases_patterns l' in - List.map (fun (subst',pl) -> subst'@subst,PatCstr (loc,id,pl,alias)) pl - -let subst_cases_pattern loc alias intern fullsubst env a = - let rec aux alias (subst,substlist as fullsubst) = function - | AVar id -> - begin - (* subst remembers the delimiters stack in the interpretation *) - (* of the notations *) - try - let (a,(scopt,subscopes)) = List.assoc id subst in - intern {env with scopes=subscopes@env.scopes; - tmp_scope = scopt} ([],[]) a - with Not_found -> - if id = ldots_var then [], [[], PatVar (loc,Name id)] else - anomaly ("Unbound pattern notation variable: "^(string_of_id id)) - (* - (* Happens for local notation joint with inductive/fixpoint defs *) - if aliases <> ([],[]) then - anomaly "Pattern notation without constructors"; - [[id],[]], PatVar (loc,Name id) - *) - end - | ARef (ConstructRef c) -> - ([],[[], PatCstr (loc,c, [], alias)]) - | AApp (ARef (ConstructRef cstr),args) -> - let args = chop_aconstr_constructor loc cstr args in - let idslpll = List.map (aux Anonymous fullsubst) args in - let ids',pll = product_of_cases_patterns [] idslpll in - let pl' = List.map (fun (asubst,pl) -> - asubst,PatCstr (loc,cstr,pl,alias)) pll in - ids', pl' - | AList (x,_,iter,terminator,lassoc) -> - (try - (* All elements of the list are in scopes (scopt,subscopes) *) - let (l,(scopt,subscopes)) = List.assoc x substlist in - let termin = aux Anonymous fullsubst terminator in - let idsl,v = - List.fold_right (fun a (tids,t) -> - let uids,u = aux Anonymous ((x,(a,(scopt,subscopes)))::subst,substlist) iter in - let pll = List.map (subst_pat_iterator ldots_var t) u in - tids@uids, List.flatten pll) - (if lassoc then List.rev l else l) termin in - idsl, List.map (fun ((asubst, pl) as x) -> - match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v - with Not_found -> - anomaly "Inconsistent substitution of recursive notation") - | AHole _ -> ([],[[], PatVar (loc,Anonymous)]) - | t -> error_invalid_pattern_notation loc - in aux alias fullsubst a - -(* Differentiating between constructors and matching variables *) -type pattern_qualid_kind = - | ConstrPat of constructor * (identifier list * - ((identifier * identifier) list * cases_pattern) list) list - | VarPat of identifier - -let find_constructor ref f aliases pats env = - let (loc,qid) = qualid_of_reference ref in - let gref = - try locate_extended qid - with Not_found -> raise (InternalizationError (loc,NotAConstructor ref)) in - match gref with - | SynDef sp -> - let (vars,a) = Syntax_def.search_syntactic_definition sp in - (match a with - | ARef (ConstructRef cstr) -> - assert (vars=[]); - cstr, [], pats - | AApp (ARef (ConstructRef cstr),args) -> - let args = chop_aconstr_constructor loc cstr args in - let nvars = List.length vars in - if List.length pats < nvars then error_not_enough_arguments loc; - let pats1,pats2 = list_chop nvars pats in - let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in - let idspl1 = List.map (subst_cases_pattern loc Anonymous f (subst,[]) env) args in - cstr, idspl1, pats2 - | _ -> raise Not_found) - - | TrueGlobal r -> - let rec unf = function - | ConstRef cst -> - let v = Environ.constant_value (Global.env()) cst in - unf (global_of_constr v) - | ConstructRef cstr -> - Dumpglob.add_glob loc r; - cstr, [], pats - | _ -> raise Not_found - in unf r +(** Use only when params were NOT asked to the user. + @return if letin are included *) +let check_constructor_length env loc cstr len_pl pl0 = + let n = len_pl + List.length pl0 in + if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else + (Int.equal n (Inductiveops.constructor_nalldecls cstr) || + (error_wrong_numarg_constructor_loc loc env cstr + (Inductiveops.constructor_nrealargs cstr))) + +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 + else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in + let remaining_args = List.fold_left (fun i x -> if is_status_implicit x then i else succ i) in + let rec aux i = function + |[],l -> let args_len = List.length l + List.length impl_list + len_pl1 in + ((if Int.equal args_len nargs then false + else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i)))) + ,l) + |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp + then let (b,out) = aux i (q,[]) in (b,RCPatAtom(Loc.ghost,None)::out) + else fail (remaining_args (len_pl1+i) il) + |imp::q,(hh::tt as l) -> if is_status_implicit imp + then let (b,out) = aux i (q,l) in (b,RCPatAtom(Loc.ghost,None)::out) + else let (b,out) = aux (succ i) (q,tt) in (b,hh::out) + in aux 0 (impl_list,pl2) + +let add_implicits_check_constructor_length env loc c len_pl1 pl2 = + let nargs = Inductiveops.constructor_nallargs c in + let nargs' = Inductiveops.constructor_nalldecls c in + let impls_st = implicits_of_global (ConstructRef c) in + add_implicits_check_length (error_wrong_numarg_constructor_loc loc env c) + nargs nargs' impls_st len_pl1 pl2 + +let add_implicits_check_ind_length env loc c len_pl1 pl2 = + let nallargs = inductive_nallargs_env env c in + let nalldecls = inductive_nalldecls_env env c in + let impls_st = implicits_of_global (IndRef c) in + add_implicits_check_length (error_wrong_numarg_inductive_loc loc env c) + nallargs nalldecls impls_st len_pl1 pl2 + +(** Do not raise NotEnoughArguments thanks to preconditions*) +let chop_params_pattern loc ind args with_letin = + let nparams = if with_letin + then Inductiveops.inductive_nparamdecls ind + else Inductiveops.inductive_nparams ind in + assert (nparams <= List.length args); + let params,args = List.chop nparams args in + List.iter (function PatVar(_,Anonymous) -> () + | PatVar (loc',_) | PatCstr(loc',_,_,_) -> error_parameter_not_implicit loc') params; + args + +let find_constructor loc add_params ref = + let cstr = match ref with + | ConstructRef cstr -> cstr + | IndRef _ -> + let error = str "There is an inductive name deep in a \"in\" clause." in + user_err_loc (loc, "find_constructor", error) + | ConstRef _ | VarRef _ -> + let error = str "This reference is not a constructor." in + user_err_loc (loc, "find_constructor", error) + in + cstr, (function (ind,_ as c) -> match add_params with + |Some nb_args -> + let nb = + if Int.equal nb_args (Inductiveops.constructor_nrealdecls c) + then Inductiveops.inductive_nparamdecls ind + else Inductiveops.inductive_nparams ind + in + List.make nb ([], [(Id.Map.empty, PatVar(Loc.ghost,Anonymous))]) + |None -> []) cstr let find_pattern_variable = function | Ident (loc,id) -> id | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x)) -let maybe_constructor ref f aliases env = - try - let c,idspl1,pl2 = find_constructor ref f aliases [] env in - assert (pl2 = []); - ConstrPat (c,idspl1) - with - (* patt var does not exists globally *) - | InternalizationError _ -> VarPat (find_pattern_variable ref) - (* patt var also exists globally but does not satisfy preconditions *) - | (Environ.NotEvaluableConst _ | Not_found) -> - if_warn msg_warning (str "pattern " ++ pr_reference ref ++ - str " is understood as a pattern variable"); - VarPat (find_pattern_variable ref) - -let mustbe_constructor loc ref f aliases patl env = - try find_constructor ref f aliases patl env - with (Environ.NotEvaluableConst _ | Not_found) -> - raise (InternalizationError (loc,NotAConstructor ref)) - let sort_fields mode loc l completer = (*mode=false if pattern and true if constructor*) match l with @@ -966,18 +975,19 @@ let sort_fields mode loc l completer = | [] -> (i, acc) | (Some name) :: b-> (match m with - | [] -> anomaly "Number of projections mismatch" + | [] -> anomaly (Pp.str "Number of projections mismatch") | (_, regular)::tm -> let boolean = not regular in - (match global_reference_of_reference refer with - | ConstRef name' when eq_constant name name' -> + begin match global_reference_of_reference refer with + | ConstRef name' when eq_constant name name' -> if boolean && mode then user_err_loc (loc, "", str"No local fields allowed in a record construction.") else build_patt b tm (i + 1) (i, snd acc) (* we found it *) | _ -> build_patt b tm (if boolean&&mode then i else i + 1) (if boolean && mode then acc - else fst acc, (i, ConstRef name) :: snd acc))) + else fst acc, (i, ConstRef name) :: snd acc) + end) | None :: b-> (* we don't want anonymous fields *) if mode then user_err_loc (loc, "", str "This record contains anonymous fields.") @@ -987,9 +997,9 @@ let sort_fields mode loc l completer = let ind = record.Recordops.s_CONST in try (* insertion of Constextern.reference_global *) (record.Recordops.s_EXPECTEDPARAM, - Qualid (loc, shortest_qualid_of_global Idset.empty (ConstructRef ind)), + Qualid (loc, shortest_qualid_of_global Id.Set.empty (ConstructRef ind)), build_patt record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 (0,[])) - with Not_found -> anomaly "Environment corruption for records." + with Not_found -> anomaly (Pp.str "Environment corruption for records.") in (* now we want to have all fields of the pattern indexed by their place in the constructor *) @@ -1032,111 +1042,287 @@ let sort_fields mode loc l completer = Some (nparams, base_constructor, List.rev (clean_list sorted_indexed_pattern 0 [])) -let rec intern_cases_pattern genv env (ids,asubst as aliases) pat = - let intern_pat = intern_cases_pattern genv in - match pat with - | CPatAlias (loc, p, id) -> - let aliases' = merge_aliases aliases id in - intern_pat env aliases' p +(** {6 Manage multiple aliases} *) + +type alias = { + alias_ids : Id.t list; + alias_map : Id.t Id.Map.t; +} + +let empty_alias = { + alias_ids = []; + alias_map = Id.Map.empty; +} + + (* [merge_aliases] returns the sets of all aliases encountered at this + point and a substitution mapping extra aliases to the first one *) +let merge_aliases aliases id = + let alias_ids = aliases.alias_ids @ [id] in + let alias_map = match aliases.alias_ids with + | [] -> aliases.alias_map + | id' :: _ -> Id.Map.add id id' aliases.alias_map + in + { alias_ids; alias_map; } + +let alias_of als = match als.alias_ids with +| [] -> Anonymous +| id :: _ -> Name id + +let message_redundant_alias id1 id2 = + msg_warning + (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2) + +(** {6 Expanding notations } + + @returns a raw_case_pattern_expr : + - no notations and syntactic definition + - global reference and identifeir instead of reference + +*) + +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 + | RCPatCstr (loc,id,l1,l2) -> + RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1, + List.map (subst_pat_iterator y t) l2) + | 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 = + (* At toplevel, Constructors and Inductives are accepted, in recursive calls + only constructor are allowed *) + let ensure_kind top loc g = + try + if top then looked_for g else + match g with ConstructRef _ -> () | _ -> raise Not_found + with Not_found -> + error_invalid_pattern_notation loc + in + let test_kind top = + if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found + in + let rec drop_syndef top env re pats = + let (loc,qid) = qualid_of_reference re in + try + match locate_extended qid with + |SynDef sp -> + let (vars,a) = Syntax_def.search_syntactic_definition sp in + (match a with + | NRef g -> + test_kind top g; + let () = assert (List.is_empty vars) in + let (_,argscs) = find_remaining_scopes [] pats g in + Some (g, [], List.map2 (in_pat_sc env) argscs pats) + | NApp (NRef g,[]) -> (* special case : Syndef for @Cstr *) + test_kind top g; + let () = assert (List.is_empty vars) in + let (argscs,_) = find_remaining_scopes pats [] g in + Some (g, List.map2 (in_pat_sc env) argscs pats, []) + | NApp (NRef g,args) -> + ensure_kind top loc g; + let nvars = List.length vars in + if List.length pats < nvars then error_not_enough_arguments loc; + let pats1,pats2 = List.chop nvars pats in + let subst = make_subst vars pats1 in + let idspl1 = List.map (in_not false loc env (subst, Id.Map.empty) []) args in + let (_,argscs) = find_remaining_scopes pats1 pats2 g in + Some (g, idspl1, List.map2 (in_pat_sc env) argscs pats2) + | _ -> raise Not_found) + |TrueGlobal g -> + test_kind top g; + Dumpglob.add_glob loc g; + let (_,argscs) = find_remaining_scopes [] pats g in + Some (g,[],List.map2 (fun x -> in_pat false {env with tmp_scope = x}) argscs pats) + with Not_found -> None + and in_pat top env = function + | CPatAlias (loc, p, id) -> RCPatAlias (loc, in_pat top env p, id) | CPatRecord (loc, l) -> - let sorted_fields = sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in - let self_patt = - match sorted_fields with - | None -> CPatAtom (loc, None) - | Some (_, head, pl) -> CPatCstr(loc, head, pl) - in - intern_pat env aliases self_patt - | CPatCstr (loc, head, pl) | CPatCstrExpl (loc, head, pl) -> - let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl env in - check_constructor_length genv loc c idslpl1 pl2; - let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in - let idslpl2 = List.map2 (fun x -> intern_pat {env with tmp_scope = x} ([],[])) argscs2 pl2 in - let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in - let pl' = List.map (fun (asubst,pl) -> - (asubst, PatCstr (loc,c,pl,alias_of aliases))) pll in - ids',pl' - | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[])) - when Bigint.is_strictly_pos p -> - intern_pat env aliases (CPatPrim(loc,Numeral(Bigint.neg p))) - | CPatNotation (_,"( _ )",([a],[])) -> - intern_pat env aliases a - | CPatNotation (loc, ntn, fullargs) -> + let sorted_fields = + sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in + begin match sorted_fields with + | None -> RCPatAtom (loc, None) + | Some (_, head, pl) -> + match drop_syndef top env head pl with + |Some (a,b,c) -> RCPatCstr(loc, a, b, c) + |None -> raise (InternalizationError (loc,NotAConstructor head)) + end + | CPatCstr (loc, head, [], pl) -> + begin + match drop_syndef top env head pl with + | Some (a,b,c) -> RCPatCstr(loc, a, b, c) + | None -> raise (InternalizationError (loc,NotAConstructor head)) + end + | CPatCstr (loc, r, expl_pl, pl) -> + let g = try + (locate (snd (qualid_of_reference r))) + with Not_found -> + raise (InternalizationError (loc,NotAConstructor r)) in + let (argscs1,argscs2) = find_remaining_scopes expl_pl pl g in + RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl, List.map2 (in_pat_sc env) argscs2 pl) + | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[]) + when Bigint.is_strictly_pos p -> + fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) + (env.tmp_scope,env.scopes)) + | CPatNotation (_,"( _ )",([a],[]),[]) -> + in_pat top env a + | CPatNotation (loc, ntn, fullargs,extrargs) -> let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in let ((ids',c),df) = Notation.interp_notation loc ntn (env.tmp_scope,env.scopes) in let (ids',idsl',_) = split_by_type ids' in Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df; - let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in - let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in - let ids'',pl = - subst_cases_pattern loc (alias_of aliases) intern_pat (subst,substlist) - env c - in ids@ids'', pl - | CPatPrim (loc, p) -> - let a = alias_of aliases in - let (c,_) = Notation.interp_prim_token_cases_pattern loc p a - (env.tmp_scope,env.scopes) in - (ids,[asubst,c]) - | CPatDelimiters (loc, key, e) -> - intern_pat {env with scopes=find_delimiters_scope loc key::env.scopes; - tmp_scope = None} aliases e - | CPatAtom (loc, Some head) -> - (match maybe_constructor head intern_pat aliases env with - | ConstrPat (c,idspl) -> - check_constructor_length genv loc c idspl []; - let (ids',pll) = product_of_cases_patterns ids idspl in - (ids,List.map (fun (asubst,pl) -> - (asubst, PatCstr (loc,c,pl,alias_of aliases))) pll) - | VarPat id -> - let ids,asubst = merge_aliases aliases id in - (ids,[asubst, PatVar (loc,alias_of (ids,asubst))])) - | CPatAtom (loc, None) -> - (ids,[asubst, PatVar (loc,alias_of aliases)]) - | CPatOr (loc, pl) -> - assert (pl <> []); - let pl' = List.map (intern_pat env aliases) pl in + let substlist = make_subst idsl' argsl in + let subst = make_subst ids' args in + in_not top loc env (subst,substlist) extrargs c + | CPatDelimiters (loc, key, e) -> + in_pat top {env with scopes=find_delimiters_scope loc key::env.scopes; + tmp_scope = None} e + | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p + (env.tmp_scope,env.scopes)) + | CPatAtom (loc, Some id) -> + begin + match drop_syndef top env id [] with + |Some (a,b,c) -> RCPatCstr (loc, a, b, c) + |None -> RCPatAtom (loc, Some (find_pattern_variable id)) + end + | CPatAtom (loc,None) -> RCPatAtom (loc,None) + | CPatOr (loc, pl) -> + RCPatOr (loc,List.map (in_pat top env) pl) + and in_pat_sc env x = in_pat false {env with tmp_scope = x} + and in_not top loc env (subst,substlist as fullsubst) args = function + | NVar id -> + let () = assert (List.is_empty args) in + begin + (* subst remembers the delimiters stack in the interpretation *) + (* of the notations *) + try + let (a,(scopt,subscopes)) = Id.Map.find id subst in + in_pat top {env with scopes=subscopes@env.scopes; + tmp_scope = scopt} a + with Not_found -> + if Id.equal id ldots_var then RCPatAtom (loc,Some id) else + anomaly (str "Unbound pattern notation variable: " ++ Id.print id) + end + | NRef g -> + ensure_kind top loc g; + let (_,argscs) = find_remaining_scopes [] args g in + RCPatCstr (loc, g, [], List.map2 (in_pat_sc env) argscs args) + | 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 {env with tmp_scope = x} fullsubst []) argscs1 pl, + List.map2 (in_pat_sc env) argscs2 args) + | NList (x,_,iter,terminator,lassoc) -> + let () = assert (List.is_empty args) in + (try + (* All elements of the list are in scopes (scopt,subscopes) *) + let (l,(scopt,subscopes)) = Id.Map.find x substlist in + let termin = in_not top loc env fullsubst [] terminator in + List.fold_right (fun a t -> + let nsubst = Id.Map.add x (a, (scopt, subscopes)) subst in + let u = in_not false loc env (nsubst, substlist) [] iter in + subst_pat_iterator ldots_var t u) + (if lassoc then List.rev l else l) termin + with Not_found -> + anomaly (Pp.str "Inconsistent substitution of recursive notation")) + | NHole _ -> + let () = assert (List.is_empty args) in + RCPatAtom (loc, None) + | t -> error_invalid_pattern_notation loc + in in_pat true + +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 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 + match pat with + | RCPatAlias (loc, p, id) -> + let aliases' = merge_aliases aliases id in + intern_pat genv aliases' p + | RCPatCstr (loc, head, expl_pl, pl) -> + if !oldfashion_patterns then + let len = if List.is_empty expl_pl then Some (List.length pl) else None in + let c,idslpl1 = find_constructor loc len head in + let with_letin = + check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in + intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl) + else + let c,idslpl1 = find_constructor loc None head in + let with_letin, pl2 = + add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in + intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2) + | RCPatAtom (loc, Some id) -> + let aliases = merge_aliases aliases id in + (aliases.alias_ids,[aliases.alias_map, PatVar (loc, alias_of aliases)]) + | RCPatAtom (loc, None) -> + let { alias_ids = ids; alias_map = asubst; } = aliases in + (ids, [asubst, PatVar (loc, alias_of aliases)]) + | RCPatOr (loc, pl) -> + assert (not (List.is_empty pl)); + let pl' = List.map (intern_pat genv aliases) pl in let (idsl,pl') = List.split pl' in let ids = List.hd idsl in check_or_pat_variables loc ids (List.tl idsl); (ids,List.flatten pl') +let intern_cases_pattern genv env aliases pat = + intern_pat genv aliases + (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) env pat) + +let intern_ind_pattern genv env pat = + let no_not = + try + drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) env pat + with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type loc + in + match no_not with + | RCPatCstr (loc, head,expl_pl, pl) -> + let c = (function IndRef ind -> ind + |_ -> error_bad_inductive_type loc) head in + let with_letin, pl2 = add_implicits_check_ind_length genv loc c + (List.length expl_pl) pl in + 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 + |_,[_,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) + (**********************************************************************) (* Utilities for application *) let merge_impargs l args = + let test x = function + | (_, Some (_, y)) -> explicitation_eq x y + | _ -> false + in List.fold_right (fun a l -> match a with | (_,Some (_,(ExplByName id as x))) when - List.exists (function (_,Some (_,y)) -> x=y | _ -> false) args -> l + List.exists (test x) args -> l | _ -> a::l) l args -let check_projection isproj nargs r = - match (r,isproj) with - | GRef (loc, ref), Some _ -> - (try - let n = Recordops.find_projection_nparams ref + 1 in - if nargs <> n then - user_err_loc (loc,"",str "Projection does not have the right number of explicit parameters."); - with Not_found -> - user_err_loc - (loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection.")) - | _, Some _ -> user_err_loc (loc_of_glob_constr r, "", str "Not a projection.") - | _, None -> () - let get_implicit_name n imps = Some (Impargs.name_of_implicit (List.nth imps (n-1))) let set_hole_implicit i b = function - | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evd.ImplicitArg (r,i,b)) - | GVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b)) - | _ -> anomaly "Only refs have implicits" + | GRef (loc,r,_) | GApp (_,GRef (loc,r,_),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) + | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None) + | _ -> anomaly (Pp.str "Only refs have implicits") let exists_implicit_name id = - List.exists (fun imp -> is_status_implicit imp & id = name_of_implicit imp) + List.exists (fun imp -> is_status_implicit imp && Id.equal id (name_of_implicit imp)) let extract_explicit_arg imps args = let rec aux = function - | [] -> [],[] + | [] -> Id.Map.empty, [] | (a,e)::l -> let (eargs,rargs) = aux l in match e with @@ -1147,7 +1333,7 @@ let extract_explicit_arg imps args = if not (exists_implicit_name id imps) then user_err_loc (loc,"",str "Wrong argument name: " ++ pr_id id ++ str "."); - if List.mem_assoc id eargs then + if Id.Map.mem id eargs then user_err_loc (loc,"",str "Argument name " ++ pr_id id ++ str " occurs more than once."); id @@ -1161,29 +1347,30 @@ let extract_explicit_arg imps args = user_err_loc (loc,"",str"Wrong argument position: " ++ int p ++ str ".") in - if List.mem_assoc id eargs then + if Id.Map.mem id eargs then user_err_loc (loc,"",str"Argument at position " ++ int p ++ str " is mentioned more than once."); id in - ((id,(loc,a))::eargs,rargs) + (Id.Map.add id (loc, a) eargs, rargs) in aux args (**********************************************************************) (* Main loop *) -let internalize sigma globalenv env allow_patvar lvar c = +let internalize globalenv env allow_patvar lvar c = let rec intern env = function - | CRef ref as x -> + | CRef (ref,us) as x -> let (c,imp,subscopes,l),_ = - intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in - (match intern_impargs c env imp subscopes l with - | [] -> c - | l -> GApp (constr_loc x, c, l)) + intern_applied_reference intern env (Environ.named_context globalenv) + lvar us [] ref + in + apply_impargs c env imp subscopes l (constr_loc x) + | CFix (loc, (locid,iddef), dl) -> let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in let dl = Array.of_list dl in let n = - try list_index0 iddef lf + try List.index0 Id.equal iddef lf with Not_found -> raise (InternalizationError (locid,UnboundFixName (false,iddef))) in @@ -1194,7 +1381,7 @@ let internalize sigma globalenv env allow_patvar lvar c = let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in let ro = f (intern env') in - let n' = Option.map (fun _ -> List.length rbefore) n in + let n' = Option.map (fun _ -> List.length (List.filter (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore)) n in n', ro, List.fold_left intern_local_binder (env',rbefore) after in let n, ro, (env',rbl) = @@ -1207,47 +1394,45 @@ let internalize sigma globalenv env allow_patvar lvar c = 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 idl = array_map2 (fun (_,_,_,_,bd) (a,b,c,env') -> - let env'' = list_fold_left_i (fun i en name -> + 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 + 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) - en (dummy_loc, Name name)) 0 env' lf in + 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 (Array.map (fun (ro,_,_,_) -> ro) idl,n), Array.of_list lf, - Array.map (fun (_,bl,_,_) -> bl) idl, + Array.map (fun (_,bl,_,_) -> List.map snd bl) idl, Array.map (fun (_,_,ty,_) -> ty) idl, Array.map (fun (_,_,_,bd) -> bd) idl) | CCoFix (loc, (locid,iddef), dl) -> let lf = List.map (fun ((_, id),_,_,_) -> id) dl in let dl = Array.of_list dl in let n = - try list_index0 iddef lf + try List.index0 Id.equal iddef lf with Not_found -> raise (InternalizationError (locid,UnboundFixName (true,iddef))) in let idl_tmp = Array.map - (fun (id,bl,ty,_) -> + (fun ((loc,id),bl,ty,_) -> let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl 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 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 + 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) - en (dummy_loc, Name name)) 0 env' lf in + 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, Array.of_list lf, - Array.map (fun (bl,_,_) -> bl) idl, + Array.map (fun (bl,_,_) -> List.map snd bl) idl, Array.map (fun (_,ty,_) -> ty) idl, Array.map (fun (_,_,bd) -> bd) idl) - | CArrow (loc,c1,c2) -> - GProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2) | CProdN (loc,[],c2) -> intern_type env c2 | CProdN (loc,(nal,bk,ty)::bll,c2) -> @@ -1273,100 +1458,154 @@ let internalize sigma globalenv env allow_patvar lvar c = | CDelimiters (loc, key, e) -> intern {env with tmp_scope = None; scopes = find_delimiters_scope loc key :: env.scopes} e - | CAppExpl (loc, (isproj,ref), args) -> + | CAppExpl (loc, (isproj,ref,us), args) -> let (f,_,args_scopes,_),args = let args = List.map (fun a -> (a,None)) args in - intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref in - check_projection isproj (List.length args) f; - (* Rem: GApp(_,f,[]) stands for @f *) - GApp (loc, f, intern_args env args_scopes (List.map fst args)) + intern_applied_reference intern env (Environ.named_context globalenv) + lvar us args ref + in + (* Rem: GApp(_,f,[]) stands for @f *) + GApp (loc, f, intern_args env args_scopes (List.map fst args)) + | CApp (loc, (isproj,f), args) -> - let isproj,f,args = match f with + let f,args = match f with (* Compact notations like "t.(f args') args" *) - | CApp (_,(Some _,f), args') when isproj=None -> isproj,f,args'@args + | CApp (_,(Some _,f), args') when not (Option.has_some isproj) -> + f,args'@args (* Don't compact "(f args') args" to resolve implicits separately *) - | _ -> isproj,f,args in + | _ -> f,args in let (c,impargs,args_scopes,l),args = match f with - | CRef ref -> intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref + | CRef (ref,us) -> + 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 - find_appl_head_data c, args + let x, impl, scopes, l = find_appl_head_data c in + (x,impl,scopes,l), args | x -> (intern env f,[],[],[]), args in - let args = - intern_impargs c env impargs args_scopes (merge_impargs l args) in - check_projection isproj (List.length args) c; - (match c with - (* Now compact "(f args') args" *) - | GApp (loc', f', args') -> GApp (join_loc loc' loc, f',args'@args) - | _ -> GApp (loc, c, args)) + apply_impargs c env impargs args_scopes + (merge_impargs l args) loc + | CRecord (loc, _, fs) -> let cargs = sort_fields true loc fs - (fun k l -> CHole (loc, Some (Evd.QuestionMark (Evd.Define true))) :: l) - in + (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None) :: l) + in begin match cargs with | None -> user_err_loc (loc, "intern", str"No constructor inference.") | Some (n, constrname, args) -> - let pars = list_make n (CHole (loc, None)) in - let app = CAppExpl (loc, (None, constrname), List.rev_append pars args) in + let pars = List.make n (CHole (loc, None, Misctypes.IntroAnonymous, None)) in + let app = CAppExpl (loc, (None, constrname,None), List.rev_append pars args) in intern env app end | CCases (loc, sty, rtnpo, tms, eqns) -> - let tms,env' = List.fold_right - (fun citm (inds,env) -> - let (tm,ind),nal = intern_case_item env citm in - (tm,ind)::inds,List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) - tms ([],env) in - let rtnpo = Option.map (intern_type env') rtnpo in + let as_in_vars = List.fold_left (fun acc (_,(na,inb)) -> + Option.fold_left (fun x tt -> List.fold_right Id.Set.add (ids_of_cases_indtype tt) x) + (Option.fold_left (fun x (_,y) -> match y with | Name y' -> Id.Set.add y' x |_ -> x) acc na) + inb) Id.Set.empty tms in + (* as, in & return vars *) + let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in + let tms,ex_ids,match_from_in = List.fold_right + (fun citm (inds,ex_ids,matchs) -> + let ((tm,ind),extra_id,match_td) = intern_case_item env forbidden_vars citm in + (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)) + (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 = let rec aux = function + |[] -> [] + |(_,PatVar _) :: q -> aux q + |l -> l + in aux match_from_in in + let rtnpo = match stripped_match_from_in with + | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *) + | l -> let thevars,thepats=List.split l in + Some ( + GCases(Loc.ghost,Term.RegularStyle,(* Some (GSort (Loc.ghost,GType None)) *)None, (* "return Type" *) + List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars, (* "match v1,..,vn" *) + [Loc.ghost,[],thepats, (* "|p1,..,pn" *) + Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None)) rtnpo; (* "=> P" is there were a P "=> _" else *) + Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *) + GHole(Loc.ghost,Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None) (* "=> _" *)])) + in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in GCases (loc, sty, rtnpo, tms, List.flatten eqns') | CLetTuple (loc, nal, (na,po), b, c) -> let env' = reset_tmp_scope env in - let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in - let p' = Option.map (fun p -> - let env'' = List.fold_left (push_name_env lvar (Variable,[],[],[])) env ids in - intern_type env'' p) po in + (* "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') + (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) | CIf (loc, c, (na,po), b1, b2) -> - let env' = reset_tmp_scope env in - let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in - let p' = Option.map (fun p -> - let env'' = List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) ids in + 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) + (Loc.ghost,na') in intern_type env'' p) po in GIf (loc, c', (na', p'), intern env b1, intern env b2) - | CHole (loc, k) -> - GHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true)) + | CHole (loc, k, naming, solve) -> + let k = match k with + | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true) + | Some k -> k + in + let solve = match solve with + | None -> None + | Some gen -> + let (ltacvars, ntnvars) = lvar in + let ntnvars = Id.Map.domain ntnvars in + let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in + let lvars = Id.Set.union lvars ntnvars in + let lvars = Id.Set.union lvars env.ids in + let ist = { + Genintern.ltacvars = lvars; + ltacrecvars = Id.Map.empty; + genv = globalenv; + } in + let (_, glb) = Genintern.generic_intern ist gen in + Some glb + in + GHole (loc, k, naming, solve) + (* Parsing pattern variables *) | CPatVar (loc, n) when allow_patvar -> - GPatVar (loc, n) - | CPatVar (loc, _) -> - raise (InternalizationError (loc,IllegalMetavariable)) + GPatVar (loc, (true,n)) + | CEvar (loc, n, []) when allow_patvar -> + GPatVar (loc, (false,n)) + (* end *) + (* Parsing existential variables *) | CEvar (loc, n, l) -> - GEvar (loc, n, Option.map (List.map (intern env)) l) + GEvar (loc, n, List.map (on_snd (intern env)) l) + | CPatVar (loc, _) -> + raise (InternalizationError (loc,IllegalMetavariable)) + (* end *) | CSort (loc, s) -> GSort(loc,s) - | CCast (loc, c1, CastConv (k, c2)) -> - GCast (loc,intern env c1, CastConv (k, intern_type env c2)) - | CCast (loc, c1, CastCoerce) -> - GCast (loc,intern env c1, CastCoerce) + | CCast (loc, c1, c2) -> + GCast (loc,intern env c1, Miscops.map_cast_type (intern_type env) c2) and intern_type env = intern (set_type_scope env) and intern_local_binder env bind = - intern_local_binder_aux intern intern_type lvar env bind + intern_local_binder_aux intern lvar env bind (* Expands a multiple pattern into a disjunction of multiple patterns *) and intern_multiple_pattern env n (loc,pl) = let idsl_pll = - List.map (intern_cases_pattern globalenv {env with tmp_scope = None} ([],[])) pl in + List.map (intern_cases_pattern globalenv {env with tmp_scope = None} empty_alias) pl in check_number_of_pattern loc n pl; product_of_cases_patterns [] idsl_pll (* Expands a disjunction of multiple pattern *) and intern_disjunctive_multiple_pattern env loc n mpl = - assert (mpl <> []); + assert (not (List.is_empty mpl)); let mpl' = List.map (intern_multiple_pattern env n) mpl in let (idsl,mpl') = List.split mpl' in let ids = List.hd idsl in @@ -1378,91 +1617,77 @@ let internalize sigma globalenv env allow_patvar lvar c = let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in (* Linearity implies the order in ids is irrelevant *) check_linearity lhs eqn_ids; - let env_ids = List.fold_right Idset.add eqn_ids env.ids in + 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 - List.iter message_redundant_alias asubst; + Id.Map.iter message_redundant_alias asubst; let rhs' = intern {env with ids = env_ids} rhs in (loc,eqn_ids,pl,rhs')) pll - and intern_case_item env (tm,(na,t)) = + and intern_case_item env forbidden_names_for_gen (tm,(na,t)) = + (*the "match" part *) let tm' = intern env tm in - let ids,typ = match t with + (* the "as" part *) + let extra_id,na = match tm', na with + | GVar (loc,id), None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id) + | GRef (loc, VarRef id, _), None -> Some id,(loc,Name id) + | _, None -> None,(Loc.ghost,Anonymous) + | _, Some (loc,na) -> None,(loc,na) in + (* the "in" part *) + let match_td,typ = match t with | Some t -> let tids = ids_of_cases_indtype t in - let tids = List.fold_right Idset.add tids Idset.empty in - let t = intern_type {env with ids = tids; tmp_scope = None} t in - let loc,ind,l = match t with - | GRef (loc,IndRef ind) -> (loc,ind,[]) - | GApp (loc,GRef (_,IndRef ind),l) -> (loc,ind,l) - | _ -> error_bad_inductive_type (loc_of_glob_constr t) in - let nparams, nrealargs = inductive_nargs globalenv ind in - let nindargs = nparams + nrealargs in - if List.length l <> nindargs then - error_wrong_numarg_inductive_loc loc globalenv ind nindargs; - let nal = List.map (function - | GHole (loc,_) -> loc,Anonymous - | GVar (loc,id) -> loc,Name id - | c -> user_err_loc (loc_of_glob_constr c,"",str "Not a name.")) l in - let parnal,realnal = list_chop nparams nal in - if List.exists (fun (_,na) -> na <> Anonymous) parnal then - error_inductive_parameter_not_implicit loc; - realnal, Some (loc,ind,nparams,List.map snd realnal) + let tids = List.fold_right Id.Set.add tids Id.Set.empty in + let with_letin,(ind,l) = intern_ind_pattern globalenv {env with ids = tids; tmp_scope = None} t in + let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in + let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in + (* for "in Vect n", we answer (["n","n"],[(loc,"n")]) + + for "in Vect (S n)", we answer ((match over "m", relevant branch is "S + n"), abstract over "m") = ([("m","S n")],[(loc,"m")]) where "m" is + generated from the canonical name of the inductive and outside of + {forbidden_names_for_gen} *) + let (match_to_do,nal) = + let rec canonize_args case_rel_ctxt arg_pats forbidden_names match_acc var_acc = + let add_name l = function + |_,Anonymous -> l + |loc,(Name y as x) -> (y,PatVar(loc,x)) :: l in + match case_rel_ctxt,arg_pats with + (* LetIn in the rel_context *) + |(_,Some _,_)::t, l when not with_letin -> + canonize_args t l forbidden_names match_acc ((Loc.ghost,Anonymous)::var_acc) + |[],[] -> + (add_name match_acc na, var_acc) + |_::t,PatVar (loc,x)::tt -> + canonize_args t tt forbidden_names + (add_name match_acc (loc,x)) ((loc,x)::var_acc) + |(cano_name,_,ty)::t,c::tt -> + let fresh = + Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names ty in + canonize_args t tt (fresh::forbidden_names) + ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc) + |_ -> assert false in + let _,args_rel = + List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in + canonize_args args_rel l (Id.Set.elements forbidden_names_for_gen) [] [] in + match_to_do, Some (cases_pattern_expr_loc t,ind,List.rev_map snd nal) | None -> - [], None in - let na = match tm', na with - | GVar (loc,id), None when not (List.mem_assoc id (snd lvar)) -> - loc,Name id - | GRef (loc, VarRef id), None -> loc,Name id - | _, None -> dummy_loc,Anonymous - | _, Some (loc,na) -> loc,na in - (tm',(snd na,typ)), na::ids + [], None in + (tm',(snd na,typ)), extra_id, match_td and iterate_prod loc2 env bk ty body nal = - let default env bk = function - | (loc1,na)::nal' as nal -> - if nal' <> [] then check_capture loc1 ty na; - let ty = intern_type env ty in - let impls = impls_type_list ty in - let env = List.fold_left (push_name_env lvar impls) env nal in - List.fold_right (fun (loc,na) c -> - GProd (join_loc loc loc2, na, bk, locate_if_isevar loc na ty, c)) - nal (intern_type env body) - | [] -> assert false - in - match bk with - | Default b -> default env b nal - | Generalized (b,b',t) -> - let env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in - let body = intern_type env body in - it_mkGProd ibind body + let env, bl = intern_assumption intern lvar env nal bk ty in + it_mkGProd loc2 bl (intern_type env body) and iterate_lam loc2 env bk ty body nal = - let default env bk = function - | (loc1,na)::nal' as nal -> - if nal' <> [] then check_capture loc1 ty na; - let ty = intern_type env ty in - let impls = impls_type_list ty in - let env = List.fold_left (push_name_env lvar impls) env nal in - List.fold_right (fun (loc,na) c -> - GLambda (join_loc loc loc2, na, bk, locate_if_isevar loc na ty, c)) - nal (intern env body) - | [] -> assert false - in match bk with - | Default b -> default env b nal - | Generalized (b, b', t) -> - let env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in - let body = intern env body in - it_mkGLambda ibind body + let env, bl = intern_assumption intern lvar env nal bk ty in + it_mkGLambda loc2 bl (intern env body) and intern_impargs c env l subscopes args = - let l = select_impargs_size (List.length args) l in let eargs, rargs = extract_explicit_arg l args in if !parsing_explicit then - if eargs <> [] then - error "Arguments given by name or position not supported in explicit mode." - else - intern_args env subscopes rargs + if Id.Map.is_empty eargs then intern_args env subscopes rargs + else error "Arguments given by name or position not supported in explicit mode." else let rec aux n impl subscopes eargs rargs = let (enva,subscopes') = apply_scope_env env subscopes in @@ -1470,11 +1695,11 @@ let internalize sigma globalenv env allow_patvar lvar c = | (imp::impl', rargs) when is_status_implicit imp -> begin try let id = name_of_implicit imp in - let (_,a) = List.assoc id eargs in - let eargs' = List.remove_assoc id eargs in + let (_,a) = Id.Map.find id eargs in + let eargs' = Id.Map.remove id eargs in intern enva a :: aux (n+1) impl' subscopes' eargs' rargs with Not_found -> - if rargs=[] & eargs=[] & not (maximal_insertion_of imp) then + if List.is_empty rargs && Id.Map.is_empty eargs && not (maximal_insertion_of imp) then (* Less regular arguments than expected: complete *) (* with implicit arguments if maximal insertion is set *) [] @@ -1485,17 +1710,28 @@ let internalize sigma globalenv env allow_patvar lvar c = | (imp::impl', a::rargs') -> intern enva a :: aux (n+1) impl' subscopes' eargs rargs' | (imp::impl', []) -> - if eargs <> [] then - (let (id,(loc,_)) = List.hd eargs in + if not (Id.Map.is_empty eargs) then + (let (id,(loc,_)) = Id.Map.choose eargs in user_err_loc (loc,"",str "Not enough non implicit \ arguments to accept the argument bound to " ++ pr_id id ++ str".")); [] | ([], rargs) -> - assert (eargs = []); + assert (Id.Map.is_empty eargs); intern_args env subscopes rargs in aux 1 l subscopes eargs rargs + and apply_impargs c env imp subscopes l loc = + let imp = select_impargs_size (List.length l) imp in + let l = intern_impargs c env imp subscopes l in + smart_gapp c loc l + + and smart_gapp f loc = function + | [] -> f + | l -> match f with + | GApp (loc', g, args) -> GApp (Loc.merge loc' loc, g, args@l) + | _ -> GApp (Loc.merge (loc_of_glob_constr f) loc, f, l) + and intern_args env subscopes = function | [] -> [] | a::args -> @@ -1515,29 +1751,38 @@ let internalize sigma globalenv env allow_patvar lvar c = (**************************************************************************) let extract_ids env = - List.fold_right Idset.add + List.fold_right Id.Set.add (Termops.ids_of_rel_context (Environ.rel_context env)) - Idset.empty + Id.Set.empty + +let scope_of_type_kind = function + | IsType -> Some Notation.type_scope + | OfType typ -> compute_type_scope typ + | WithoutTypeConstraint -> None + +let empty_ltac_sign = { + ltac_vars = Id.Set.empty; + ltac_bound = Id.Set.empty; +} -let intern_gen isarity sigma env - ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[])) +let intern_gen kind env + ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign) c = - let tmp_scope = - if isarity then Some Notation.type_scope else None in - internalize sigma env {ids = extract_ids env; unb = false; - tmp_scope = tmp_scope; scopes = []; - impls = impls} - allow_patvar (ltacvars, []) c + let tmp_scope = scope_of_type_kind kind in + internalize env {ids = extract_ids env; unb = false; + tmp_scope = tmp_scope; scopes = []; + impls = impls} + allow_patvar (ltacvars, Id.Map.empty) c -let intern_constr sigma env c = intern_gen false sigma env c +let intern_constr env c = intern_gen WithoutTypeConstraint env c -let intern_type sigma env c = intern_gen true sigma env c +let intern_type env c = intern_gen IsType env c let intern_pattern globalenv patt = try intern_cases_pattern globalenv {ids = extract_ids globalenv; unb = false; tmp_scope = None; scopes = []; - impls = empty_internalization_env} ([],[]) patt + impls = empty_internalization_env} empty_alias patt with InternalizationError (loc,e) -> user_err_loc (loc,"internalize",explain_internalization_error e) @@ -1546,158 +1791,135 @@ let intern_pattern globalenv patt = (*********************************************************************) (* Functions to parse and interpret constructions *) -let interp_gen kind sigma env - ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[])) - c = - let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in - Default.understand_gen kind sigma env c +(* All evars resolved *) -let interp_constr sigma env c = - interp_gen (OfType None) sigma env c +let interp_gen kind env sigma ?(impls=empty_internalization_env) c = + let c = intern_gen kind ~impls env c in + understand ~expected_type:kind env sigma c -let interp_type sigma env ?(impls=empty_internalization_env) c = - interp_gen IsType sigma env ~impls c +let interp_constr env sigma ?(impls=empty_internalization_env) c = + interp_gen WithoutTypeConstraint env sigma c -let interp_casted_constr sigma env ?(impls=empty_internalization_env) c typ = - interp_gen (OfType (Some typ)) sigma env ~impls c +let interp_type env sigma ?(impls=empty_internalization_env) c = + interp_gen IsType env sigma ~impls c -let interp_open_constr sigma env c = - Default.understand_tcc sigma env (intern_constr sigma env c) +let interp_casted_constr env sigma ?(impls=empty_internalization_env) c typ = + interp_gen (OfType typ) env sigma ~impls c -let interp_open_constr_patvar sigma env c = - let raw = intern_gen false sigma env c ~allow_patvar:true in - let sigma = ref sigma in - let evars = ref (Gmap.empty : (identifier,glob_constr) Gmap.t) in - let rec patvar_to_evar r = match r with - | GPatVar (loc,(_,id)) -> - ( try Gmap.find id !evars - with Not_found -> - let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in - let ev = Evarutil.e_new_evar sigma env ev in - let rev = GEvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in - evars := Gmap.add id rev !evars; - rev - ) - | _ -> map_glob_constr patvar_to_evar r in - let raw = patvar_to_evar raw in - Default.understand_tcc !sigma env raw - -let interp_constr_judgment sigma env c = - Default.understand_judgment sigma env (intern_constr sigma env c) - -let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true) - env ?(impls=empty_internalization_env) kind c = - let evdref = - match evdref with - | None -> ref Evd.empty - | Some evdref -> evdref - in - let istype = kind = IsType in - let c = intern_gen istype ~impls !evdref env c in - let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:istype c in - Default.understand_tcc_evars ~fail_evar evdref env kind c, imps +(* Not all evars expected to be resolved *) + +let interp_open_constr env sigma c = + understand_tcc env sigma (intern_constr env c) -let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true) - env ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c +(* Not all evars expected to be resolved and computation of implicit args *) -let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c = - interp_constr_evars_gen_impls ?evdref ~fail_evar env IsType ~impls c +let interp_constr_evars_gen_impls env evdref + ?(impls=empty_internalization_env) expected_type c = + let c = intern_gen expected_type ~impls env c in + let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in + understand_tcc_evars env evdref ~expected_type c, imps -let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c = - interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c +let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c = + interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c -let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) kind c = - let c = intern_gen (kind=IsType) ~impls !evdref env c in - Default.understand_tcc_evars evdref env kind c +let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ = + interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c -let interp_casted_constr_evars evdref env ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c +let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c = + interp_constr_evars_gen_impls env evdref ~impls IsType c -let interp_type_evars evdref env ?(impls=empty_internalization_env) c = - interp_constr_evars_gen evdref env IsType ~impls c +(* Not all evars expected to be resolved, with side-effect on evars *) -type ltac_sign = identifier list * unbound_ltac_var_map +let interp_constr_evars_gen env evdref ?(impls=empty_internalization_env) expected_type c = + let c = intern_gen expected_type ~impls env c in + understand_tcc_evars env evdref ~expected_type c -let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c = - let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in +let interp_constr_evars env evdref ?(impls=empty_internalization_env) c = + interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c + +let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ = + interp_constr_evars_gen env evdref ~impls (OfType typ) c + +let interp_type_evars env evdref ?(impls=empty_internalization_env) c = + interp_constr_evars_gen env evdref IsType ~impls c + +(* Miscellaneous *) + +let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = + let c = intern_gen (if as_type then IsType else WithoutTypeConstraint) + ~allow_patvar:true ~ltacvars env c in pattern_of_glob_constr c -let interp_aconstr ?(impls=empty_internalization_env) vars recvars a = +let interp_notation_constr ?(impls=empty_internalization_env) nenv a = let env = Global.env () in (* [vl] is intended to remember the scope of the free variables of [a] *) - let vl = List.map (fun (id,typ) -> (id,(ref None,typ))) vars in - let c = internalize Evd.empty (Global.env()) {ids = extract_ids env; unb = false; + let vl = Id.Map.map (fun typ -> (ref None, typ)) nenv.ninterp_var_type in + let c = internalize (Global.env()) {ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impls} - false (([],[]),vl) a in + false (empty_ltac_sign, vl) a in (* Translate and check that [c] has all its free variables bound in [vars] *) - let a = aconstr_of_glob_constr vars recvars c in + let a = notation_constr_of_glob_constr nenv c in (* Splits variables into those that are binding, bound, or both *) (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l in - let vars = List.map (fun (id,(sc,typ)) -> (id,(out_scope !sc,typ))) vl in + let vars = Id.Map.map (fun (sc, typ) -> (out_scope !sc, typ)) vl in (* Returns [a] and the ordered list of variables with their scopes *) vars, a (* Interpret binders and contexts *) -let interp_binder sigma env na t = - let t = intern_gen true sigma env t in - let t' = locate_if_isevar (loc_of_glob_constr t) na t in - Default.understand_type sigma env t' +let interp_binder env sigma na t = + let t = intern_gen IsType env t in + let t' = locate_if_hole (loc_of_glob_constr t) na t in + understand ~expected_type:IsType env sigma t' -let interp_binder_evars evdref env na t = - let t = intern_gen true !evdref env t in - let t' = locate_if_isevar (loc_of_glob_constr t) na t in - Default.understand_tcc_evars evdref env IsType t' +let interp_binder_evars env evdref na t = + let t = intern_gen IsType env t in + let t' = locate_if_hole (loc_of_glob_constr t) na t in + understand_tcc_evars env evdref ~expected_type:IsType t' open Environ -open Term -let my_intern_constr sigma env lvar acc c = - internalize sigma env acc false lvar c +let my_intern_constr env lvar acc c = + internalize env acc false lvar c -let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c - -let intern_context global_level sigma env impl_env params = - let lvar = (([],[]), []) in +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 sigma env lvar) (my_intern_type sigma env lvar) lvar) + (intern_local_binder_aux ~global_level (my_intern_constr env lvar) lvar) ({ids = extract_ids env; unb = false; - tmp_scope = None; scopes = []; impls = impl_env}, []) params in (lenv.impls, bl) + tmp_scope = None; scopes = []; impls = impl_env}, []) binders in + (lenv.impls, List.map snd bl) + with InternalizationError (loc,e) -> + user_err_loc (loc,"internalize", explain_internalization_error e) -let interp_rawcontext_gen understand_type understand_judgment env bl = +let interp_rawcontext_evars env evdref bl = let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> match b with None -> - let t' = locate_if_isevar (loc_of_glob_constr t) na t in - let t = understand_type env t' in + let t' = locate_if_hole (loc_of_glob_constr t) na t in + let t = + understand_tcc_evars env evdref ~expected_type:IsType t' in let d = (na,None,t) in let impls = - if k = Implicit then + if k == Implicit then let na = match na with Name n -> Some n | Anonymous -> None in (ExplByPos (n, na), (true, true, true)) :: impls else impls in (push_rel d env, d::params, succ n, impls) | Some b -> - let c = understand_judgment env b in - let d = (na, Some c.uj_val, Termops.refresh_universes c.uj_type) in + let c = understand_judgment_tcc env evdref b in + let d = (na, Some c.uj_val, c.uj_type) in (push_rel d env, d::params, succ n, impls)) (env,[],1,[]) (List.rev bl) in (env, par), impls -let interp_context_gen understand_type understand_judgment ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params = - let int_env,bl = intern_context global_level sigma env impl_env params in - int_env, interp_rawcontext_gen understand_type understand_judgment env bl - -let interp_context ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params = - interp_context_gen (Default.understand_type sigma) - (Default.understand_judgment sigma) ~global_level ~impl_env sigma env params - -let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) evdref env params = - interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t) - (Default.understand_judgment_tcc evdref) ~global_level ~impl_env !evdref env params +let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) env evdref params = + let int_env,bl = intern_context global_level env impl_env params in + let x = interp_rawcontext_evars env evdref bl in + int_env, x |