From f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 6 Aug 2010 16:15:08 -0400 Subject: Imported Upstream version 8.3~rc1+dfsg --- interp/constrextern.ml | 65 ++-- interp/constrextern.mli | 2 +- interp/constrintern.ml | 704 ++++++++++++++++++++++------------------ interp/constrintern.mli | 73 +++-- interp/coqlib.ml | 5 +- interp/coqlib.mli | 8 +- interp/dumpglob.ml | 9 +- interp/dumpglob.mli | 3 +- interp/genarg.ml | 2 +- interp/genarg.mli | 2 +- interp/implicit_quantifiers.ml | 39 ++- interp/implicit_quantifiers.mli | 4 +- interp/modintern.ml | 2 +- interp/modintern.mli | 2 +- interp/notation.ml | 5 +- interp/notation.mli | 2 +- interp/ppextend.ml | 3 +- interp/ppextend.mli | 3 +- interp/reserve.ml | 2 +- interp/reserve.mli | 2 +- interp/syntax_def.ml | 6 +- interp/syntax_def.mli | 2 +- interp/topconstr.ml | 588 +++++++++++++++++++++------------ interp/topconstr.mli | 76 +++-- 24 files changed, 948 insertions(+), 661 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 77a79883..b2b21925 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: constrextern.ml 13329 2010-07-26 11:05:39Z herbelin $ *) (*i*) open Pp @@ -178,9 +178,10 @@ let rec check_same_type ty1 ty2 = check_same_type b1 b2 | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) -> check_same_type a1 a2 - | CNotation(_,n1,(e1,el1)), CNotation(_,n2,(e2,el2)) when n1=n2 -> + | CNotation(_,n1,(e1,el1,bl1)), CNotation(_,n2,(e2,el2,bl2)) when n1=n2 -> List.iter2 check_same_type e1 e2; - List.iter2 (List.iter2 check_same_type) el1 el2 + List.iter2 (List.iter2 check_same_type) el1 el2; + List.iter2 check_same_fix_binder bl1 bl2 | CPrim(_,i1), CPrim(_,i2) when i1=i2 -> () | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 -> check_same_type e1 e2 @@ -287,7 +288,7 @@ and spaces ntn n = if n = String.length ntn then [] else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1) -let expand_curly_brackets loc mknot ntn (l,ll) = +let expand_curly_brackets loc mknot ntn l = let ntn' = ref ntn in let rec expand_ntn i = function @@ -300,12 +301,12 @@ let expand_curly_brackets loc mknot ntn (l,ll) = ntn' := String.sub !ntn' 0 p ^ "_" ^ String.sub !ntn' (p+5) (String.length !ntn' -p-5); - mknot (loc,"{ _ }",([a],[])) end + mknot (loc,"{ _ }",[a]) end else a in a' :: expand_ntn (i+1) l in let l = expand_ntn 0 l in (* side effect *) - mknot (loc,!ntn',(l,ll)) + mknot (loc,!ntn',l) let destPrim = function CPrim(_,t) -> Some t | _ -> None let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None @@ -313,32 +314,34 @@ let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None let make_notation_gen loc ntn mknot mkprim destprim l = if has_curly_brackets ntn then expand_curly_brackets loc mknot ntn l - else match ntn,List.map destprim (fst l),(snd l) with + else match ntn,List.map destprim l with (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *) - | "- _", [Some (Numeral p)],[] when Bigint.is_strictly_pos p -> - mknot (loc,ntn,([mknot (loc,"( _ )",l)],[])) + | "- _", [Some (Numeral p)] when Bigint.is_strictly_pos p -> + mknot (loc,ntn,([mknot (loc,"( _ )",l)])) | _ -> match decompose_notation_key ntn, l with - | [Terminal "-"; Terminal x], ([],[]) -> + | [Terminal "-"; Terminal x], [] -> (try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x))) - with _ -> mknot (loc,ntn,([],[]))) - | [Terminal x], ([],[]) -> + with _ -> mknot (loc,ntn,[])) + | [Terminal x], [] -> (try mkprim (loc, Numeral (Bigint.of_string x)) - with _ -> mknot (loc,ntn,([],[]))) + with _ -> mknot (loc,ntn,[])) | _ -> mknot (loc,ntn,l) -let make_notation loc ntn l = +let make_notation loc ntn (terms,termlists,binders as subst) = + if termlists <> [] or binders <> [] then CNotation (loc,ntn,subst) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> CNotation (loc,ntn,l)) + (fun (loc,ntn,l) -> CNotation (loc,ntn,(l,[],[]))) (fun (loc,p) -> CPrim (loc,p)) - destPrim l + destPrim terms -let make_pat_notation loc ntn l = +let make_pat_notation loc ntn (terms,termlists as subst) = + if termlists <> [] then CPatNotation (loc,ntn,subst) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> CPatNotation (loc,ntn,l)) + (fun (loc,ntn,l) -> CPatNotation (loc,ntn,(l,[]))) (fun (loc,p) -> CPatPrim (loc,p)) - destPatPrim l + destPatPrim terms (* Better to use extern_rawconstr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = @@ -686,10 +689,10 @@ let rec extern inctx scopes vars r = let na' = match na,tm with Anonymous, RVar (_,id) when rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt) - -> Some Anonymous + -> Some (dummy_loc,Anonymous) | Anonymous, _ -> None | Name id, RVar (_,id') when id=id' -> None - | Name _, _ -> Some na in + | Name _, _ -> Some (dummy_loc,na) in (sub_extern false scopes vars tm, (na',Option.map (fun (loc,ind,n,nal) -> let params = list_tabulate @@ -703,15 +706,15 @@ let rec extern inctx scopes vars r = CCases (loc,sty,rtntypopt',tml,eqns) | RLetTuple (loc,nal,(na,typopt),tm,b) -> - CLetTuple (loc,nal, - (Option.map (fun _ -> na) typopt, + CLetTuple (loc,List.map (fun na -> (dummy_loc,na)) nal, + (Option.map (fun _ -> (dummy_loc,na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern inctx scopes (List.fold_left add_vname vars nal) b) | RIf (loc,c,(na,typopt),b1,b2) -> CIf (loc,sub_extern false scopes vars c, - (Option.map (fun _ -> na) typopt, + (Option.map (fun _ -> (dummy_loc,na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2) @@ -836,7 +839,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | _, None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) - let subst,substlist = match_aconstr t pat in + let terms,termlists,binders = match_aconstr t pat in (* Try availability of interpretation ... *) let e = match keyrule with @@ -851,17 +854,21 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function List.map (fun (c,(scopt,scl)) -> extern (* assuming no overloading: *) true (scopt,scl@scopes') vars c) - subst in + terms in let ll = List.map (fun (c,(scopt,scl)) -> List.map (extern true (scopt,scl@scopes') vars) c) - substlist in - insert_delimiters (make_notation loc ntn (l,ll)) key) + termlists in + let bll = + List.map (fun (bl,(scopt,scl)) -> + snd (extern_local_binder (scopt,scl@scopes') vars bl)) + binders in + insert_delimiters (make_notation loc ntn (l,ll,bll)) key) | SynDefRule kn -> let l = List.map (fun (c,(scopt,scl)) -> extern true (scopt,scl@scopes) vars c, None) - subst in + terms in let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in if l = [] then a else CApp (loc,(None,a),l) in if args = [] then e diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 5f170bdc..248abeda 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: constrextern.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Util diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0fed211d..3bf556f1 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: constrintern.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Pp open Util @@ -28,7 +28,10 @@ open Inductiveops (* 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 | Recursive | Method +type var_internalization_type = + | Inductive of identifier list (* list of params *) + | Recursive + | Method type var_internalization_data = (* type of the "free" variable, for coqdoc, e.g. while typing the @@ -45,19 +48,12 @@ type var_internalization_data = type internalization_env = (identifier * var_internalization_data) list -type full_internalization_env = - (* a superset of the list of variables that may be automatically - inserted and that must not occur as binders *) - identifier list * - (* mapping of the variables to their internalization data *) - internalization_env - type raw_binder = (name * binding_kind * rawconstr option * rawconstr) let interning_grammar = ref false (* Historically for parsing grammar rules, but in fact used only for - translator, v7 parsing, and unstrict tactic internalisation *) + translator, v7 parsing, and unstrict tactic internalization *) let for_grammar f x = interning_grammar := true; let a = f x in @@ -92,9 +88,9 @@ let global_reference_in_absolute_module dir id = constr_of_global (Nametab.global_of_path (Libnames.make_path dir id)) (**********************************************************************) -(* Internalisation errors *) +(* Internalization errors *) -type internalisation_error = +type internalization_error = | VariableCapture of identifier | WrongExplicitImplicit | IllegalMetavariable @@ -104,7 +100,7 @@ type internalisation_error = | BadPatternsNumber of int * int | BadExplicitationNumber of explicitation * int option -exception InternalisationError of loc * internalisation_error +exception InternalizationError of loc * internalization_error let explain_variable_capture id = str "The variable " ++ pr_id id ++ str " occurs in its type" @@ -146,7 +142,7 @@ let explain_bad_explicitation_number n po = str "Bad explicitation name: found " ++ pr_id id ++ str" but was expecting " ++ s -let explain_internalisation_error e = +let explain_internalization_error e = let pp = match e with | VariableCapture id -> explain_variable_capture id | WrongExplicitImplicit -> explain_wrong_explicit_implicit @@ -171,30 +167,26 @@ let error_inductive_parameter_not_implicit loc = (* Pre-computing the implicit arguments and arguments scopes needed *) (* for interpretation *) -let empty_internalization_env = ([],[]) +let empty_internalization_env = [] -let set_internalization_env_params ienv params = - let nparams = List.length params in - if nparams = 0 then - ([],ienv) - else - let ienv_with_implicit_params = - List.map (fun (id,(ty,_,impl,scopes)) -> - let sub_impl,_ = list_chop nparams impl in - let sub_impl' = List.filter is_status_implicit sub_impl in - (id,(ty,List.map name_of_implicit sub_impl',impl,scopes))) ienv in - (params, ienv_with_implicit_params) - -let compute_internalization_data env ty typ impls = - let impl = compute_implicits_with_manual env typ (is_implicit_args()) impls in - (ty, [], impl, compute_arguments_scope typ) - -let compute_full_internalization_env env ty params idl typl impll = - set_internalization_env_params - (list_map3 - (fun id typ impl -> (id,compute_internalization_data env ty typ impl)) - idl typl impll) - params +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.filter is_status_implicit sub_impl in + List.map name_of_implicit sub_impl' + | Recursive | Method -> + (* Unable to know in advance what the implicit arguments will be *) + [] + +let compute_internalization_data env ty typ impl = + let impl = compute_implicits_with_manual env typ (is_implicit_args()) impl in + let expls_impl = compute_explicitable_implicit impl ty in + (ty, expls_impl, impl, compute_arguments_scope typ) + +let compute_internalization_env env ty = + list_map3 + (fun id typ impl -> (id,compute_internalization_data env ty typ impl)) (**********************************************************************) (* Contracting "{ _ }" in notations *) @@ -216,18 +208,18 @@ let expand_notation_string ntn n = (* This contracts the special case of "{ _ }" for sumbool, sumor notations *) (* Remark: expansion of squash at definition is done in metasyntax.ml *) -let contract_notation ntn (l,ll) = +let contract_notation ntn (l,ll,bll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | CNotation (_,"{ _ }",([a],[])) :: l -> + | CNotation (_,"{ _ }",([a],[],[])) :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> a::contract_squash (n+1) l in let l = contract_squash 0 l in (* side effect; don't inline *) - !ntn',(l,ll) + !ntn',(l,ll,bll) let contract_pat_notation ntn (l,ll) = let ntn' = ref ntn in @@ -250,43 +242,219 @@ let make_current_scope = function | (Some tmp_scope,scopes) -> tmp_scope::scopes | None,scopes -> scopes -let set_var_scope loc id (_,_,scopt,scopes) varscopes = - let idscopes = List.assoc id varscopes in - if !idscopes <> None & - make_current_scope (Option.get !idscopes) - <> make_current_scope (scopt,scopes) then - let pr_scope_stack = function - | [] -> str "the empty scope stack" - | [a] -> str "scope " ++ str a - | l -> str "scope stack " ++ - str "[" ++ prlist_with_sep pr_comma str l ++ str "]" in - user_err_loc (loc,"set_var_scope", - pr_id id ++ str " is used both in " ++ - pr_scope_stack (make_current_scope (Option.get !idscopes)) ++ - strbrk " and in " ++ - pr_scope_stack (make_current_scope (scopt,scopes))) - else - idscopes := Some (scopt,scopes) +let pr_scope_stack = function + | [] -> str "the empty scope stack" + | [a] -> str "scope " ++ str a + | l -> str "scope stack " ++ + str "[" ++ prlist_with_sep pr_comma str l ++ str "]" + +let error_inconsistent_scope loc id scopes1 scopes2 = + user_err_loc (loc,"set_var_scope", + pr_id id ++ str " is used both in " ++ + pr_scope_stack scopes1 ++ strbrk " and in " ++ pr_scope_stack scopes2) + +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 ++ + str " is expected to occur in binding position in the right-hand side.") + +let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars = + try + let idscopes,typ = List.assoc id ntnvars in + if !idscopes <> None & + make_current_scope (Option.get !idscopes) + <> make_current_scope (scopt,scopes) then + error_inconsistent_scope loc id + (make_current_scope (Option.get !idscopes)) + (make_current_scope (scopt,scopes)) + else + idscopes := Some (scopt,scopes); + match typ with + | NtnInternTypeBinder -> + if istermvar then error_expect_binder_notation_type loc id + | NtnInternTypeConstr -> + (* We need sometimes to parse idents at a constr level for + factorization and we cannot enforce this constraint: + if not istermvar then error_expect_constr_notation_type loc id *) + () + | NtnInternTypeIdent -> () + with Not_found -> + (* Not in a notation *) + () + +let set_type_scope (ids,unb,tmp_scope,scopes) = + (ids,unb,Some Notation.type_scope,scopes) + +let reset_tmp_scope (ids,unb,tmp_scope,scopes) = + (ids,unb,None,scopes) + +let rec it_mkRProd env body = + match env with + (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body)) + | [] -> body + +let rec it_mkRLambda env body = + match env with + (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body)) + | [] -> body + +(**********************************************************************) +(* Utilities for binders *) + +let check_capture loc ty = function + | Name id when occur_var_constr_expr id ty -> + raise (InternalizationError (loc,VariableCapture id)) + | _ -> + () + +let locate_if_isevar loc na = function + | RHole _ -> + (try match na with + | Name id -> Reserve.find_reserved_type id + | Anonymous -> raise Not_found + with Not_found -> RHole (loc, Evd.BinderType na)) + | x -> x + +let check_hidden_implicit_parameters id (_,_,_,impls) = + if List.exists (function + | (_,(Inductive indparams,_,_,_)) -> List.mem id indparams + | _ -> false) impls + then + errorlabstrm "" (strbrk "A parameter of an inductive type " ++ + pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") + +let push_name_env ?(global_level=false) lvar (ids,unb,tmpsc,scopes as env) = + function + | loc,Anonymous -> + if global_level then + user_err_loc (loc,"", str "Anonymous variables not allowed"); + env + | loc,Name id -> + check_hidden_implicit_parameters id lvar; + set_var_scope loc id false env (let (_,_,ntnvars,_) = lvar in ntnvars); + if global_level then Dumpglob.dump_definition (loc,id) true "var" + else Dumpglob.dump_binding loc id; + (Idset.add id ids,unb,tmpsc,scopes) + +let intern_generalized_binder ?(global_level=false) intern_type lvar + (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty = + let ids = match na with Anonymous -> ids | Name na -> Idset.add na ids in + let ty, ids' = + if t then ty, ids else + Implicit_quantifiers.implicit_application ids + Implicit_quantifiers.combine_params_freevar ty + in + let ty' = intern_type (ids,true,tmpsc,sc) ty in + let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids ~allowed:ids' ty' in + let env' = List.fold_left (fun env (x, l) -> push_name_env ~global_level lvar env (l, Name x)) env fvs in + let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in + let na = match na with + | Anonymous -> + if global_level then na + else + let name = + let id = + match ty with + | CApp (_, (_, CRef (Ident (loc,id))), _) -> id + | _ -> id_of_string "H" + in Implicit_quantifiers.make_fresh ids' (Global.env ()) id + in Name name + | _ -> na + in (push_name_env ~global_level lvar 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 + | LocalRawAssum(nal,bk,ty) -> + (match bk with + | Default k -> + let (loc,na) = List.hd nal in + (* TODO: fail if several names with different implicit types *) + let ty = locate_if_isevar loc na (intern_type env ty) in + List.fold_left + (fun (env,bl) na -> + (push_name_env lvar env na,(snd na,k,None,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) + | LocalRawDef((loc,na as locna),def) -> + (push_name_env lvar env locna, + (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) + +let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c = + let c = intern (ids,true,tmp_scope,scopes) c in + let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids c in + let env', c' = + let abs = + let pi = + match ak with + | Some AbsPi -> true + | None when tmp_scope = Some Notation.type_scope + || List.mem Notation.type_scope scopes -> true + | _ -> false + in + if pi then + (fun (id, loc') acc -> + RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc)) + else + (fun (id, loc') acc -> + RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc)) + in + List.fold_right (fun (id, loc as lid) (env, acc) -> + let env' = push_name_env lvar 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 (loc,na) = List.hd nal in + (* TODO: fail if several names with different implicit types *) + let ty = intern_type env ty in + let ty = locate_if_isevar loc na ty in + List.fold_left + (fun (env,bl) na -> (push_name_env lvar env na,(snd na,k,None,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) -> + (push_name_env lvar env locna, + (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) (**********************************************************************) (* Syntax extensions *) -let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env))= +let option_mem_assoc id = function + | Some (id',c) -> 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 + (* TODO binders *) + let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in + next_ident_away id fvs + +let traverse_binder (terms,_,_ as subst) + (renaming,(ids,unb,tmpsc,scopes as 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 subst)) in + let _,na = coerce_to_name (fst (List.assoc id terms)) in (renaming,(name_fold Idset.add na ids,unb,tmpsc,scopes)), na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) - let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) subst in - let fvs2 = List.flatten (List.map (fun (_,(l,_)) -> List.map free_vars_of_constr_expr l) substlist) in - let fvs3 = List.map snd renaming in - let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in - let id' = next_ident_away id fvs in + let id' = find_fresh_name renaming subst id in let renaming' = if id=id' then renaming else (id,id')::renaming in (renaming',env), Name id' @@ -294,17 +462,18 @@ let rec subst_iterator y t = function | RVar (_,id) as x -> if id = y then t else x | x -> map_rawconstr (subst_iterator y t) x -let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c = - let (renaming,(ids,unb,_,scopes)) = infos in - let subinfos = renaming,(ids,unb,None,scopes) in - match c with - | AVar id -> +let subst_aconstr_in_rawconstr loc intern lvar subst infos c = + let (terms,termlists,binders) = subst in + let rec aux (terms,binderopt as subst') (renaming,(ids,unb,_,scopes as env)) c = + let subinfos = renaming,(ids,unb,None,scopes) 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 subst in - interp (ids,unb,scopt,subscopes@scopes) a + let (a,(scopt,subscopes)) = List.assoc id terms in + intern (ids,unb,scopt,subscopes@scopes) a with Not_found -> try RVar (loc,List.assoc id renaming) @@ -312,83 +481,96 @@ let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c = (* Happens for local notation joint with inductive/fixpoint defs *) RVar (loc,id) end - | AList (x,_,iter,terminator,lassoc) -> + | 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 = - subst_aconstr_in_rawconstr loc interp sub subinfos terminator in + let (l,(scopt,subscopes)) = List.assoc x termlists in + let termin = aux subst' subinfos terminator in List.fold_right (fun a t -> subst_iterator ldots_var t - (subst_aconstr_in_rawconstr loc interp - ((x,(a,(scopt,subscopes)))::subst,substlist) subinfos iter)) + (aux ((x,(a,(scopt,subscopes)))::terms,binderopt) subinfos iter)) (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)) -> + | AHole (Evd.BinderType (Name id as na)) -> let na = - try snd (coerce_to_name (fst (List.assoc id subst))) + try snd (coerce_to_name (fst (List.assoc id terms))) with Not_found -> na in RHole (loc,Evd.BinderType na) - | t -> - rawconstr_of_aconstr_with_binders loc (traverse_binder sub) - (subst_aconstr_in_rawconstr loc interp sub) subinfos t - -let intern_notation intern (_,_,tmp_scope,scopes as env) loc ntn fullargs = - let ntn,(args,argslist as fullargs) = contract_notation ntn fullargs in - let (((ids,idsl),c),df) = interp_notation loc ntn (tmp_scope,scopes) in + | ABinderList (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 termin = aux subst' (renaming,env) terminator in + List.fold_left (fun t binder -> + subst_iterator ldots_var t + (aux (terms,Some(x,binder)) subinfos iter)) + termin bl + with Not_found -> + anomaly "Inconsistent substitution of recursive notation") + | AProd (Name id, AHole _, c') when option_mem_assoc id binderopt -> + let (na,bk,_,t) = snd (Option.get binderopt) in + RProd (loc,na,bk,t,aux subst' infos c') + | ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt -> + let (na,bk,_,t) = snd (Option.get binderopt) in + RLambda (loc,na,bk,t,aux subst' infos c') + | t -> + rawconstr_of_aconstr_with_binders loc (traverse_binder subst) + (aux subst') subinfos t + in aux (terms,None) infos c + +let split_by_type ids = + List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) -> + match typ with + | NtnTypeConstr -> ((x,scl)::l1,l2,l3) + | 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 intern_notation intern (_,_,tmp_scope,scopes as env) lvar loc ntn fullargs = + let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in + let ((ids,c),df) = interp_notation loc ntn (tmp_scope,scopes) in Dumpglob.dump_notation_location (ntn_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 argslist in - subst_aconstr_in_rawconstr loc intern (subst,substlist) ([],env) c - -let set_type_scope (ids,unb,tmp_scope,scopes) = - (ids,unb,Some Notation.type_scope,scopes) - -let reset_tmp_scope (ids,unb,tmp_scope,scopes) = - (ids,unb,None,scopes) - -let rec it_mkRProd env body = - match env with - (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body)) - | [] -> body - -let rec it_mkRLambda env body = - match env with - (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body)) - | [] -> body + let ids,idsl,idsbl = split_by_type ids in + let terms = make_subst ids args in + let termlists = make_subst idsl argslist in + let binders = make_subst idsbl bll in + subst_aconstr_in_rawconstr loc intern lvar + (terms,termlists,binders) ([],env) c (**********************************************************************) (* Discriminating between bound variables and global references *) -(* [vars1] is a set of name to avoid (used for the tactic language); - [vars2] is the set of global variables, env is the set of variables - abstracted until this point *) - let string_of_ty = function - | Inductive -> "ind" + | Inductive _ -> "ind" | Recursive -> "def" | Method -> "meth" -let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id = - let (vars1,unbndltacvars) = ltacvars in +let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id = + let (ltacvars,unbndltacvars) = ltacvars in (* Is [id] an inductive type potentially with implicit *) try - let ty,l,impl,argsc = List.assoc id impls in - let l = List.map - (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in + let ty,expl_impls,impls,argsc = List.assoc id impls in + let expl_impls = List.map + (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in let tys = string_of_ty ty in - Dumpglob.dump_reference loc "<>" (string_of_id id) tys; - RVar (loc,id), impl, argsc, l + Dumpglob.dump_reference loc "<>" (string_of_id id) tys; + RVar (loc,id), impls, argsc, expl_impls with Not_found -> - (* Is [id] bound in current env or is an ltac var bound to constr *) - if Idset.mem id env or List.mem id vars1 + (* Is [id] bound in current term or is an ltac var bound to constr *) + if Idset.mem id ids or List.mem id ltacvars then RVar (loc,id), [], [], [] (* Is [id] a notation variable *) - else if List.mem_assoc id vars3 + else if List.mem_assoc id ntnvars + then + (set_var_scope loc id true genv ntnvars; RVar (loc,id), [], [], []) + (* Is [id] the special variable for recursive notations *) + else if ntnvars <> [] && id = ldots_var then - (set_var_scope loc id genv vars3; RVar (loc,id), [], [], []) + RVar (loc,id), [], [], [] else (* Is [id] bound to a free name in ltac (this is an ltac error message) *) try @@ -398,7 +580,7 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l | 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 vars2 in + let _ = Sign.lookup_named id namedctxvars in try (* [id] a section variable *) (* Redundant: could be done in intern_qualid *) @@ -443,7 +625,7 @@ let intern_reference ref = (intern_extended_global_of_qualid (qualid_of_reference ref)) (* Is it a global reference or a syntactic definition? *) -let intern_qualid loc qid intern env args = +let intern_qualid loc qid intern env lvar args = match intern_extended_global_of_qualid (loc,qid) with | TrueGlobal ref -> RRef (loc, ref), args @@ -453,25 +635,25 @@ let intern_qualid loc qid intern env args = if List.length args < nids then error_not_enough_arguments loc; let args1,args2 = list_chop nids args in check_no_explicitation args1; - let subst = List.map2 (fun (id,scl) a -> (id,(fst a,scl))) ids args1 in - subst_aconstr_in_rawconstr loc intern (subst,[]) ([],env) c, args2 + let subst = make_subst ids (List.map fst args1) in + subst_aconstr_in_rawconstr loc intern lvar (subst,[],[]) ([],env) c, args2 (* Rule out section vars since these should have been found by intern_var *) -let intern_non_secvar_qualid loc qid intern env args = - match intern_qualid loc qid intern env args with +let intern_non_secvar_qualid loc qid intern env lvar args = + match intern_qualid loc qid intern env lvar args with | RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid | r -> r let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function | Qualid (loc, qid) -> - let r,args2 = intern_qualid loc qid intern env args in + let r,args2 = intern_qualid loc qid intern env lvar args in find_appl_head_data r, args2 | Ident (loc, id) -> try intern_var env lvar 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 args in + let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in find_appl_head_data r, args2 with e -> (* Extra allowance for non globalizing functions *) @@ -482,7 +664,7 @@ let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function let interp_reference vars r = let (r,_,_,_),_ = intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc) - (Idset.empty,false,None,[]) (vars,[],[],([],[])) [] r + (Idset.empty,false,None,[]) (vars,[],[],[]) [] r in r let apply_scope_env (ids,unb,_,scopes) = function @@ -529,14 +711,14 @@ let loc_of_lhs lhs = let check_linearity lhs ids = match has_duplicate ids with | Some id -> - raise (InternalisationError (loc_of_lhs lhs,NonLinearPattern id)) + raise (InternalizationError (loc_of_lhs lhs,NonLinearPattern id)) | None -> () (* 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 (InternalisationError (loc,BadPatternsNumber (n,p))) + if 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 @@ -646,7 +828,7 @@ let find_constructor ref f aliases pats scopes = let (loc,qid) = qualid_of_reference ref in let gref = try locate_extended qid - with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in + with Not_found -> raise (InternalizationError (loc,NotAConstructor ref)) in match gref with | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in @@ -677,7 +859,7 @@ let find_constructor ref f aliases pats scopes = let find_pattern_variable = function | Ident (loc,id) -> id - | Qualid (loc,_) as x -> raise (InternalisationError(loc,NotAConstructor x)) + | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x)) let maybe_constructor ref f aliases scopes = try @@ -686,7 +868,7 @@ let maybe_constructor ref f aliases scopes = ConstrPat (c,idspl1) with (* patt var does not exists globally *) - | InternalisationError _ -> VarPat (find_pattern_variable ref) + | InternalizationError _ -> VarPat (find_pattern_variable ref) (* patt var also exists globally but does not satisfy preconditions *) | (Environ.NotEvaluableConst _ | Not_found) -> if_verbose msg_warning (str "pattern " ++ pr_reference ref ++ @@ -696,7 +878,7 @@ let maybe_constructor ref f aliases scopes = let mustbe_constructor loc ref f aliases patl scopes = try find_constructor ref f aliases patl scopes with (Environ.NotEvaluableConst _ | Not_found) -> - raise (InternalisationError (loc,NotAConstructor ref)) + raise (InternalizationError (loc,NotAConstructor ref)) let sort_fields mode loc l completer = (*mode=false if pattern and true if constructor*) @@ -813,7 +995,8 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat= intern_pat scopes aliases tmp_scope a | CPatNotation (loc, ntn, fullargs) -> let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in - let (((ids',idsl'),c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in + let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,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 @@ -848,116 +1031,6 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat= check_or_pat_variables loc ids (List.tl idsl); (ids,List.flatten pl') -(**********************************************************************) -(* Fix and CoFix *) - -(**********************************************************************) -(* Utilities for binders *) - -let check_capture loc ty = function - | Name id when occur_var_constr_expr id ty -> - raise (InternalisationError (loc,VariableCapture id)) - | _ -> - () - -let locate_if_isevar loc na = function - | RHole _ -> - (try match na with - | Name id -> Reserve.find_reserved_type id - | Anonymous -> raise Not_found - with Not_found -> RHole (loc, Evd.BinderType na)) - | x -> x - -let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) = - if List.mem id indnames then - errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++ - pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") - -let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function - | Anonymous -> - if fail_anonymous then errorlabstrm "" (str "Anonymous variables not allowed"); - env - | Name id -> - check_hidden_implicit_parameters id lvar; - (Idset.add id ids, unb,tmpsc,scopes) - -let push_loc_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) loc = function - | Anonymous -> - if fail_anonymous then user_err_loc (loc,"", str "Anonymous variables not allowed"); - env - | Name id -> - check_hidden_implicit_parameters id lvar; - Dumpglob.dump_binding loc id; - (Idset.add id ids,unb,tmpsc,scopes) - -let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar - (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty = - let ids = match na with Anonymous -> ids | Name na -> Idset.add na ids in - let ty, ids' = - if t then ty, ids else - Implicit_quantifiers.implicit_application ids - Implicit_quantifiers.combine_params_freevar ty - in - let ty' = intern_type (ids,true,tmpsc,sc) ty in - let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids ~allowed:ids' ty' in - let env' = List.fold_left (fun env (x, l) -> push_loc_name_env ~fail_anonymous lvar env l (Name x)) env fvs in - let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in - let na = match na with - | Anonymous -> - if fail_anonymous then na - else - let name = - let id = - match ty with - | CApp (_, (_, CRef (Ident (loc,id))), _) -> id - | _ -> id_of_string "H" - in Implicit_quantifiers.make_fresh ids' (Global.env ()) id - in Name name - | _ -> na - in (push_loc_name_env ~fail_anonymous lvar env' loc na), (na,b',None,ty') :: List.rev bl - -let intern_local_binder_aux ?(fail_anonymous=false) intern intern_type lvar ((ids,unb,ts,sc as env),bl) = function - | LocalRawAssum(nal,bk,ty) -> - (match bk with - | Default k -> - let (loc,na) = List.hd nal in - (* TODO: fail if several names with different implicit types *) - let ty = locate_if_isevar loc na (intern_type env ty) in - List.fold_left - (fun ((ids,unb,ts,sc),bl) (_,na) -> - ((name_fold Idset.add na ids,unb,ts,sc), (na,k,None,ty)::bl)) - (env,bl) nal - | Generalized (b,b',t) -> - let env, b = intern_generalized_binder ~fail_anonymous intern_type lvar env bl (List.hd nal) b b' t ty in - env, b @ bl) - | LocalRawDef((loc,na),def) -> - ((name_fold Idset.add na ids,unb,ts,sc), - (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) - -let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c = - let c = intern (ids,true,tmp_scope,scopes) c in - let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids c in - let env', c' = - let abs = - let pi = - match ak with - | Some AbsPi -> true - | None when tmp_scope = Some Notation.type_scope - || List.mem Notation.type_scope scopes -> true - | _ -> false - in - if pi then - (fun (id, loc') acc -> - RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc)) - else - (fun (id, loc') acc -> - RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc)) - in - List.fold_right (fun (id, loc as lid) (env, acc) -> - let env' = push_loc_name_env lvar env loc (Name id) in - (env', abs lid acc)) fvs (env,c) - in c' - (**********************************************************************) (* Utilities for application *) @@ -1030,7 +1103,7 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Main loop *) -let internalise sigma globalenv env allow_patvar lvar c = +let internalize sigma globalenv env allow_patvar lvar c = let rec intern (ids,unb,tmp_scope,scopes as env) = function | CRef ref as x -> let (c,imp,subscopes,l),_ = @@ -1044,17 +1117,16 @@ let internalise sigma globalenv env allow_patvar lvar c = let n = try list_index0 iddef lf with Not_found -> - raise (InternalisationError (locid,UnboundFixName (false,iddef))) + raise (InternalizationError (locid,UnboundFixName (false,iddef))) in let idl = Array.map (fun (id,(n,order),bl,ty,bd) -> let intern_ro_arg f = - let idx = Option.default 0 (index_of_annot bl n) in - let before, after = list_chop idx bl in + let before, after = split_at_annot bl n in let ((ids',_,_,_) as env',rbefore) = List.fold_left intern_local_binder (env,[]) before in let ro = f (intern (ids', unb, tmp_scope, scopes)) in - let n' = Option.map (fun _ -> List.length before) n in + let n' = Option.map (fun _ -> List.length rbefore) n in n', ro, List.fold_left intern_local_binder (env',rbefore) after in let n, ro, ((ids',_,_,_),rbl) = @@ -1082,7 +1154,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let n = try list_index0 iddef lf with Not_found -> - raise (InternalisationError (locid,UnboundFixName (true,iddef))) + raise (InternalizationError (locid,UnboundFixName (true,iddef))) in let idl = Array.map (fun (id,bl,ty,bd) -> @@ -1107,15 +1179,15 @@ let internalise sigma globalenv env allow_patvar lvar c = intern env c2 | CLambdaN (loc,(nal,bk,ty)::bll,c2) -> iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal - | CLetIn (loc,(loc1,na),c1,c2) -> - RLetIn (loc, na, intern (reset_tmp_scope env) c1, - intern (push_loc_name_env lvar env loc1 na) c2) - | CNotation (loc,"- _",([CPrim (_,Numeral p)],[])) + | CLetIn (loc,na,c1,c2) -> + RLetIn (loc, snd na, intern (reset_tmp_scope env) c1, + intern (push_name_env lvar env na) c2) + | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[])) when Bigint.is_strictly_pos p -> intern env (CPrim (loc,Numeral (Bigint.neg p))) - | CNotation (_,"( _ )",([a],[])) -> intern env a + | CNotation (_,"( _ )",([a],[],[])) -> intern env a | CNotation (loc,ntn,args) -> - intern_notation intern env loc ntn args + intern_notation intern env lvar loc ntn args | CGeneralization (loc,b,a,c) -> intern_generalization intern env lvar loc b a c | CPrim (loc, p) -> @@ -1138,8 +1210,8 @@ let internalise sigma globalenv env allow_patvar lvar c = let (c,impargs,args_scopes,l),args = match f with | CRef ref -> intern_applied_reference intern env lvar args ref - | CNotation (loc,ntn,([],[])) -> - let c = intern_notation intern env loc ntn ([],[]) in + | CNotation (loc,ntn,([],[],[])) -> + let c = intern_notation intern env lvar loc ntn ([],[],[]) in find_appl_head_data c, args | x -> (intern env f,[],[],[]), args in let args = @@ -1177,7 +1249,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let p' = Option.map (fun p -> let env'' = List.fold_left (push_name_env lvar) env ids in intern_type env'' p) po in - RLetTuple (loc, nal, (na', p'), b', + RLetTuple (loc, List.map snd nal, (na', p'), b', intern (List.fold_left (push_name_env lvar) env nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in @@ -1191,7 +1263,7 @@ let internalise sigma globalenv env allow_patvar lvar c = | CPatVar (loc, n) when allow_patvar -> RPatVar (loc, n) | CPatVar (loc, _) -> - raise (InternalisationError (loc,IllegalMetavariable)) + raise (InternalizationError (loc,IllegalMetavariable)) | CEvar (loc, n, l) -> REvar (loc, n, Option.map (List.map (intern env)) l) | CSort (loc, s) -> @@ -1252,27 +1324,27 @@ let internalise sigma globalenv env allow_patvar lvar c = if List.length l <> nindargs then error_wrong_numarg_inductive_loc loc globalenv ind nindargs; let nal = List.map (function - | RHole loc -> Anonymous - | RVar (_,id) -> Name id + | RHole (loc,_) -> loc,Anonymous + | RVar (loc,id) -> loc,Name id | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name.")) l in let parnal,realnal = list_chop nparams nal in - if List.exists ((<>) Anonymous) parnal then + if List.exists (fun (_,na) -> na <> Anonymous) parnal then error_inductive_parameter_not_implicit loc; - realnal, Some (loc,ind,nparams,realnal) + realnal, Some (loc,ind,nparams,List.map snd realnal) | None -> [], None in let na = match tm', na with - | RVar (_,id), None when Idset.mem id vars -> Name id - | RRef (loc, VarRef id), None -> Name id - | _, None -> Anonymous - | _, Some na -> na in - (tm',(na,typ)), na::ids + | RVar (loc,id), None when Idset.mem id vars -> loc,Name id + | RRef (loc, VarRef id), None -> loc,Name id + | _, None -> dummy_loc,Anonymous + | _, Some (loc,na) -> loc,na in + (tm',(snd na,typ)), na::ids and iterate_prod loc2 env bk ty body nal = let rec default env bk = function - | (loc1,na)::nal -> + | (loc1,na as locna)::nal -> if nal <> [] then check_capture loc1 ty na; - let body = default (push_loc_name_env lvar env loc1 na) bk nal in + let body = default (push_name_env lvar env locna) bk nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in RProd (join_loc loc1 loc2, na, bk, ty, body) | [] -> intern_type env body @@ -1280,24 +1352,22 @@ let internalise sigma globalenv env allow_patvar lvar c = 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 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_mkRProd ibind body and iterate_lam loc2 env bk ty body nal = let rec default env bk = function - | (loc1,na)::nal -> + | (loc1,na as locna)::nal -> if nal <> [] then check_capture loc1 ty na; - let body = default (push_loc_name_env lvar env loc1 na) bk nal in + let body = default (push_name_env lvar env locna) bk nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in RLambda (join_loc loc1 loc2, na, bk, ty, body) | [] -> intern env body 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 env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in let body = intern env body in it_mkRLambda ibind body @@ -1345,9 +1415,9 @@ let internalise sigma globalenv env allow_patvar lvar c = try intern env c with - InternalisationError (loc,e) -> + InternalizationError (loc,e) -> user_err_loc (loc,"internalize", - explain_internalisation_error e) + explain_internalization_error e) (**************************************************************************) (* Functions to translate constr_expr into rawconstr *) @@ -1359,11 +1429,11 @@ let extract_ids env = Idset.empty let intern_gen isarity sigma env - ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) + ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let tmp_scope = if isarity then Some Notation.type_scope else None in - internalise sigma env (extract_ids env, false, tmp_scope,[]) + internalize sigma env (extract_ids env, false, tmp_scope,[]) allow_patvar (ltacvars,Environ.named_context env, [], impls) c let intern_constr sigma env c = intern_gen false sigma env c @@ -1374,8 +1444,8 @@ let intern_pattern env patt = try intern_cases_pattern env [] ([],[]) None patt with - InternalisationError (loc,e) -> - user_err_loc (loc,"internalize",explain_internalisation_error e) + InternalizationError (loc,e) -> + user_err_loc (loc,"internalize",explain_internalization_error e) type manual_implicits = (explicitation * (bool * bool * bool)) list @@ -1384,7 +1454,7 @@ type manual_implicits = (explicitation * (bool * bool * bool)) list (* Functions to parse and interpret constructions *) let interp_gen kind sigma env - ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) + ?(impls=[]) ?(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 @@ -1392,10 +1462,10 @@ let interp_gen kind sigma env let interp_constr sigma env c = interp_gen (OfType None) sigma env c -let interp_type sigma env ?(impls=([],[])) c = +let interp_type sigma env ?(impls=[]) c = interp_gen IsType sigma env ~impls c -let interp_casted_constr sigma env ?(impls=([],[])) c typ = +let interp_casted_constr sigma env ?(impls=[]) c typ = interp_gen (OfType (Some typ)) sigma env ~impls c let interp_open_constr sigma env c = @@ -1423,34 +1493,35 @@ 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=([],[])) kind c = + env ?(impls=[]) kind c = let evdref = match evdref with | None -> ref Evd.empty | Some evdref -> evdref in - let c = intern_gen (kind=IsType) ~impls !evdref env c in - let imps = Implicit_quantifiers.implicits_of_rawterm c in + let istype = kind = IsType in + let c = intern_gen istype ~impls !evdref env c in + let imps = Implicit_quantifiers.implicits_of_rawterm ~with_products:istype c in Default.understand_tcc_evars ~fail_evar evdref env kind c, imps let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true) - env ?(impls=([],[])) c typ = + env ?(impls=[]) c typ = interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c -let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=([],[])) c = +let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c = interp_constr_evars_gen_impls ?evdref ~fail_evar env IsType ~impls c -let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=([],[])) c = +let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c = interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c -let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c = +let interp_constr_evars_gen evdref env ?(impls=[]) 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 evdref env ?(impls=([],[])) c typ = +let interp_casted_constr_evars evdref env ?(impls=[]) c typ = interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c -let interp_type_evars evdref env ?(impls=([],[])) c = +let interp_type_evars evdref env ?(impls=[]) c = interp_constr_evars_gen evdref env IsType ~impls c type ltac_sign = identifier list * unbound_ltac_var_map @@ -1459,19 +1530,20 @@ 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 pattern_of_rawconstr c -let interp_aconstr ?(impls=([],[])) (vars,varslist) a = +let interp_aconstr ?(impls=[]) vars recvars 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 -> (id,ref None)) (vars@varslist) in - let c = internalise Evd.empty (Global.env()) (extract_ids env, false, None, []) + let vl = List.map (fun (id,typ) -> (id,(ref None,typ))) vars in + let c = internalize Evd.empty (Global.env()) (extract_ids env, false, None, []) false (([],[]),Environ.named_context env,vl,impls) a in (* Translate and check that [c] has all its free variables bound in [vars] *) - let a = aconstr_of_rawconstr vars c in + let a = aconstr_of_rawconstr vars recvars 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 (* Returns [a] and the ordered list of variables with their scopes *) - (* Variables occurring in binders have no relevant scope since bound *) - let vl = List.map (fun (id,r) -> - (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl in - list_chop (List.length vars) vl, a + vars, a (* Interpret binders and contexts *) @@ -1489,14 +1561,14 @@ open Environ open Term let my_intern_constr sigma env lvar acc c = - internalise sigma env acc false lvar c + internalize sigma 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 fail_anonymous sigma env params = - let lvar = (([],[]),Environ.named_context env, [], ([], [])) in +let intern_context global_level sigma env params = + let lvar = (([],[]),Environ.named_context env, [], []) in snd (List.fold_left - (intern_local_binder_aux ~fail_anonymous (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar) + (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar) ((extract_ids env,false,None,[]), []) params) let interp_rawcontext_gen understand_type understand_judgment env bl = @@ -1522,15 +1594,15 @@ let interp_rawcontext_gen understand_type understand_judgment env bl = (env,[],1,[]) (List.rev bl) in (env, par), impls -let interp_context_gen understand_type understand_judgment ?(fail_anonymous=false) sigma env params = - let bl = intern_context fail_anonymous sigma env params in +let interp_context_gen understand_type understand_judgment ?(global_level=false) sigma env params = + let bl = intern_context global_level sigma env params in interp_rawcontext_gen understand_type understand_judgment env bl -let interp_context ?(fail_anonymous=false) sigma env params = +let interp_context ?(global_level=false) sigma env params = interp_context_gen (Default.understand_type sigma) - (Default.understand_judgment sigma) ~fail_anonymous sigma env params + (Default.understand_judgment sigma) ~global_level sigma env params -let interp_context_evars ?(fail_anonymous=false) evdref env params = +let interp_context_evars ?(global_level=false) evdref env params = interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t) - (Default.understand_judgment_tcc evdref) ~fail_anonymous !evdref env params + (Default.understand_judgment_tcc evdref) ~global_level !evdref env params diff --git a/interp/constrintern.mli b/interp/constrintern.mli index ebee4eda..acb13a8b 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: constrintern.mli 13329 2010-07-26 11:05:39Z herbelin $ i*) (*i*) open Names @@ -30,45 +30,45 @@ open Pretyping - check all variables are bound - make absolute the references to global objets - resolution of symbolic notations using scopes - - insert existential variables for implicit arguments + - insertion of implicit arguments *) -(* To interpret implicits and arg scopes of recursive variables while - internalizing inductive types and recursive definitions, and also +(* To interpret implicit arguments and arg scopes of recursive variables + while internalizing inductive types and recursive definitions, and also projection while typing records. the third and fourth arguments associate a list of implicit positions and scopes to identifiers declared in the [rel_context] of [env] *) -type var_internalization_type = Inductive | Recursive | Method +type var_internalization_type = + | Inductive of identifier list (* list of params *) + | Recursive + | Method type var_internalization_data = var_internalization_type * + (* type of the "free" variable, for coqdoc, e.g. while typing the + constructor of JMeq, "JMeq" behaves as a variable of type Inductive *) identifier list * - Impargs.implicits_list * - scope_name option list + (* 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) *) + Impargs.implicits_list * (* signature of impargs of the variable *) + scope_name option list (* subscopes of the args of the variable *) (* A map of free variables to their implicit arguments and scopes *) type internalization_env = (identifier * var_internalization_data) list (* Contains also a list of identifiers to automatically apply to the variables*) -type full_internalization_env = - identifier list * internalization_env - -val empty_internalization_env : full_internalization_env +val empty_internalization_env : internalization_env val compute_internalization_data : env -> var_internalization_type -> types -> Impargs.manual_explicitation list -> var_internalization_data -val set_internalization_env_params : - internalization_env -> identifier list -> full_internalization_env - -val compute_full_internalization_env : env -> - var_internalization_type -> - identifier list -> identifier list -> types list -> - Impargs.manual_explicitation list list -> full_internalization_env +val compute_internalization_env : env -> var_internalization_type -> + identifier list -> types list -> Impargs.manual_explicitation list list -> + internalization_env type manual_implicits = (explicitation * (bool * bool * bool)) list @@ -83,7 +83,7 @@ val intern_constr : evar_map -> env -> constr_expr -> rawconstr val intern_type : evar_map -> env -> constr_expr -> rawconstr val intern_gen : bool -> evar_map -> env -> - ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> + ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> rawconstr val intern_pattern : env -> cases_pattern_expr -> @@ -97,7 +97,7 @@ val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder (* Main interpretation function *) val interp_gen : typing_constraint -> evar_map -> env -> - ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> + ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr (* Particular instances *) @@ -105,33 +105,33 @@ val interp_gen : typing_constraint -> evar_map -> env -> val interp_constr : evar_map -> env -> constr_expr -> constr -val interp_type : evar_map -> env -> ?impls:full_internalization_env -> - constr_expr -> types +val interp_type : evar_map -> env -> ?impls:internalization_env -> + constr_expr -> types val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * constr -val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env -> +val interp_casted_constr : evar_map -> env -> ?impls:internalization_env -> constr_expr -> types -> constr (* Accepting evars and giving back the manual implicits in addition. *) val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> - ?impls:full_internalization_env -> constr_expr -> types -> constr * manual_implicits + ?impls:internalization_env -> constr_expr -> types -> constr * manual_implicits val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> - env -> ?impls:full_internalization_env -> + env -> ?impls:internalization_env -> constr_expr -> types * manual_implicits val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> - env -> ?impls:full_internalization_env -> + env -> ?impls:internalization_env -> constr_expr -> constr * manual_implicits val interp_casted_constr_evars : evar_map ref -> env -> - ?impls:full_internalization_env -> constr_expr -> types -> constr + ?impls:internalization_env -> constr_expr -> types -> constr -val interp_type_evars : evar_map ref -> env -> ?impls:full_internalization_env -> +val interp_type_evars : evar_map ref -> env -> ?impls:internalization_env -> constr_expr -> types (*s Build a judgment *) @@ -160,13 +160,13 @@ val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types val interp_context_gen : (env -> rawconstr -> types) -> (env -> rawconstr -> unsafe_judgment) -> - ?fail_anonymous:bool -> + ?global_level:bool -> evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits -val interp_context : ?fail_anonymous:bool -> +val interp_context : ?global_level:bool -> evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits -val interp_context_evars : ?fail_anonymous:bool -> +val interp_context_evars : ?global_level:bool -> evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits (* Locating references of constructions, possibly via a syntactic definition *) @@ -177,10 +177,15 @@ val construct_reference : named_context -> identifier -> constr val global_reference : identifier -> constr val global_reference_in_absolute_module : dir_path -> identifier -> constr -(* Interprets into a abbreviatable constr *) +(* Interprets a term as the left-hand side of a notation; the boolean + list is a set and this set is [true] for a variable occurring in + term position, [false] for a variable occurring in binding + position; [true;false] if in both kinds of position *) -val interp_aconstr : ?impls:full_internalization_env -> - identifier list * identifier list -> constr_expr -> interpretation +val interp_aconstr : ?impls:internalization_env -> + (identifier * notation_var_internalization_type) list -> + (identifier * identifier) list -> constr_expr -> + (identifier * (subscopes * notation_var_internalization_type)) list * aconstr (* Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b diff --git a/interp/coqlib.ml b/interp/coqlib.ml index dbec915d..0848ccc7 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: coqlib.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Util open Pp @@ -182,14 +182,11 @@ type coq_bool_data = { andb_prop : constr; andb_true_intro : constr} -type 'a delayed = unit -> 'a - let build_bool_type () = { andb = init_constant ["Datatypes"] "andb"; andb_prop = init_constant ["Datatypes"] "andb_prop"; andb_true_intro = init_constant ["Datatypes"] "andb_true_intro" } - let build_sigma_set () = anomaly "Use build_sigma_type" let build_sigma_type () = diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 12791139..81cc3baa 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: coqlib.mli 13332 2010-07-26 22:12:43Z msozeau $ i*) (*i*) open Names @@ -14,6 +14,7 @@ open Libnames open Nametab open Term open Pattern +open Util (*i*) (*s This module collects the global references, constructions and @@ -86,9 +87,8 @@ val glob_jmeq : global_reference at compile time. Therefore, we can only provide methods to build them at runtime. This is the purpose of the [constr delayed] and [constr_pattern delayed] types. Objects of this time needs to be - applied to [()] to get the actual constr or pattern at runtime *) - -type 'a delayed = unit -> 'a + forced with [delayed_force] to get the actual constr or pattern + at runtime. *) type coq_bool_data = { andb : constr; diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index ec02146e..0a42b78b 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: dumpglob.ml 13328 2010-07-26 11:05:30Z herbelin $ *) (* Dump of globalization (to be used by coqdoc) *) @@ -161,13 +161,6 @@ let dump_name (loc, n) sec ty = | Names.Name id -> dump_definition (loc, id) sec ty | Names.Anonymous -> () -let dump_local_binder b sec ty = - if dump () then - match b with - | Topconstr.LocalRawAssum (nl, _, _) -> - List.iter (fun x -> dump_name x sec ty) nl - | Topconstr.LocalRawDef _ -> () - let dump_modref loc mp ty = if dump () then let (dp, l) = Lib.split_modpath mp in diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 2d5b1468..049bad5a 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: dumpglob.mli 13328 2010-07-26 11:05:30Z herbelin $ *) val open_glob_file : string -> unit @@ -39,7 +39,6 @@ val dump_notation_location : (int * int) list -> Topconstr.notation -> (Notation val dump_binding : Util.loc -> Names.Idset.elt -> unit val dump_notation : Util.loc * (Topconstr.notation * Notation.notation_location) -> Topconstr.scope_name option -> bool -> unit val dump_constraint : Topconstr.typeclass_constraint -> bool -> string -> unit -val dump_local_binder : Topconstr.local_binder -> bool -> string -> unit val dump_string : string -> unit diff --git a/interp/genarg.ml b/interp/genarg.ml index a6a042d6..310420aa 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: genarg.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/interp/genarg.mli b/interp/genarg.mli index f410e1ed..9c9096bb 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: genarg.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Util open Names diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 73e3910a..22075654 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: implicit_quantifiers.ml 13332 2010-07-26 22:12:43Z msozeau $ i*) (*i*) open Names @@ -93,7 +93,7 @@ let is_freevar ids env x = with _ -> not (is_global x) with _ -> true -(* Auxilliary functions for the inference of implicitly quantified variables. *) +(* Auxiliary functions for the inference of implicitly quantified variables. *) let ungeneralizable loc id = user_err_loc (loc, "Generalization", @@ -110,7 +110,7 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l = in let rec aux bdvars l c = match c with | CRef (Ident (loc,id)) -> found loc id bdvars l - | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [])) when not (Idset.mem id bdvars) -> + | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [], [])) when not (Idset.mem id bdvars) -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c in aux bound l c @@ -297,19 +297,28 @@ let implicit_application env ?(allow_partial=true) f ty = CAppExpl (loc, (None, id), args), avoid in c, avoid -let implicits_of_rawterm l = +let implicits_of_rawterm ?(with_products=true) l = let rec aux i c = - match c with - RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> - let rest = aux (succ i) b in - if bk = Implicit then - let name = - match na with - Name id -> Some id - | Anonymous -> None - in - (ExplByPos (i, name), (true, true, true)) :: rest - else rest + let abs loc na bk t b = + let rest = aux (succ i) b in + if bk = Implicit then + let name = + match na with + | Name id -> Some id + | Anonymous -> None + in + (ExplByPos (i, name), (true, true, true)) :: rest + else rest + in + match c with + | RProd (loc, na, bk, t, b) -> + if with_products then abs loc na bk t b + else + (if bk = Implicit then + msg_warning (str "Ignoring implicit status of product binder " ++ + pr_name na ++ str " and following binders"); + []) + | RLambda (loc, na, bk, t, b) -> abs loc na bk t b | RLetIn (loc, na, t, b) -> aux i b | _ -> [] in aux 1 l diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 315541e2..b8f6594a 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: implicit_quantifiers.mli 13332 2010-07-26 22:12:43Z msozeau $ i*) (*i*) open Names @@ -46,7 +46,7 @@ val generalizable_vars_of_rawconstr : ?bound:Idset.t -> ?allowed:Idset.t -> val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier -val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list +val implicits_of_rawterm : ?with_products:bool -> Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list val combine_params_freevar : Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) -> diff --git a/interp/modintern.ml b/interp/modintern.ml index f414adab..bed5597e 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: modintern.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/interp/modintern.mli b/interp/modintern.mli index 304db5be..1cf8a5bd 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: modintern.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Declarations diff --git a/interp/notation.ml b/interp/notation.ml index 4a89dbd7..fe9d8b6d 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: notation.ml 13329 2010-07-26 11:05:39Z herbelin $ *) (*i*) open Util @@ -209,7 +209,8 @@ let cases_pattern_key = function let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *) | AApp (ARef ref,args) -> RefKey(make_gr ref), Some (List.length args) - | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey (make_gr ref), Some (List.length args) + | AList (_,_,AApp (ARef ref,args),_,_) + | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (make_gr ref), Some (List.length args) | ARef ref -> RefKey(make_gr ref), None | _ -> Oth, None diff --git a/interp/notation.mli b/interp/notation.mli index 533ccb76..72b576eb 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: notation.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Util diff --git a/interp/ppextend.ml b/interp/ppextend.ml index 653aefed..618f8320 100644 --- a/interp/ppextend.ml +++ b/interp/ppextend.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ *) +(*i $Id: ppextend.ml 13329 2010-07-26 11:05:39Z herbelin $ *) (*i*) open Pp @@ -53,6 +53,7 @@ let ppcmd_of_cut = function type unparsing = | UnpMetaVar of int * parenRelation | UnpListMetaVar of int * parenRelation * unparsing list + | UnpBinderListMetaVar of int * bool * unparsing list | UnpTerminal of string | UnpBox of ppbox * unparsing list | UnpCut of ppcut diff --git a/interp/ppextend.mli b/interp/ppextend.mli index 7b988786..6c386162 100644 --- a/interp/ppextend.mli +++ b/interp/ppextend.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ppextend.mli 13329 2010-07-26 11:05:39Z herbelin $ i*) (*i*) open Pp @@ -43,6 +43,7 @@ val ppcmd_of_cut : ppcut -> std_ppcmds type unparsing = | UnpMetaVar of int * parenRelation | UnpListMetaVar of int * parenRelation * unparsing list + | UnpBinderListMetaVar of int * bool * unparsing list | UnpTerminal of string | UnpBox of ppbox * unparsing list | UnpCut of ppcut diff --git a/interp/reserve.ml b/interp/reserve.ml index 7f9b35a6..2225bb6e 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: reserve.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) (* Reserved names *) diff --git a/interp/reserve.mli b/interp/reserve.mli index e1853a74..613ba830 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: reserve.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Util open Names diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index e6bb468e..77b34d4f 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: syntax_def.ml 13329 2010-07-26 11:05:39Z herbelin $ *) open Util open Pp @@ -76,8 +76,8 @@ type syndef_interpretation = (identifier * subscopes) list * aconstr (* Coercions to the general format of notation that also supports variables bound to list of expressions *) -let in_pat (ids,ac) = ((ids,[]),ac) -let out_pat ((ids,idsl),ac) = assert (idsl=[]); (ids,ac) +let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,(sc,NtnTypeConstr))) ids,ac) +let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac) let declare_syntactic_definition local id onlyparse pat = let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 49e74b65..33d4c5d3 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: syntax_def.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Util diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 5911f667..b8a90088 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: topconstr.ml 13357 2010-07-29 22:59:55Z herbelin $ *) (*i*) open Pp @@ -36,6 +36,7 @@ type aconstr = (* Part only in rawconstr *) | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr + | ABinderList of identifier * identifier * aconstr * aconstr | ALetIn of name * aconstr * aconstr | ACases of case_style * aconstr option * (aconstr * (name * (inductive * int * name list) option)) list * @@ -50,6 +51,21 @@ type aconstr = | APatVar of patvar | ACast of aconstr * aconstr cast_type +type scope_name = string + +type tmp_scope_name = scope_name + +type subscopes = tmp_scope_name option * scope_name list + +type notation_var_instance_type = + | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList + +type notation_var_internalization_type = + | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent + +type interpretation = + (identifier * (subscopes * notation_var_instance_type)) list * aconstr + (**********************************************************************) (* Re-interpret a notation as a rawconstr, taking care of binders *) @@ -69,6 +85,16 @@ let rec cases_pattern_fold_map loc g e = function let rec subst_rawvars l = function | RVar (_,id) as r -> (try List.assoc id l with Not_found -> r) + | RProd (loc,Name id,bk,t,c) -> + let id = + try match List.assoc id l with RVar(_,id') -> id' | _ -> id + with Not_found -> id in + RProd (loc,Name id,bk,subst_rawvars l t,subst_rawvars l c) + | RLambda (loc,Name id,bk,t,c) -> + let id = + try match List.assoc id l with RVar(_,id') -> id' | _ -> id + with Not_found -> id in + RLambda (loc,Name id,bk,subst_rawvars l t,subst_rawvars l c) | r -> map_rawconstr (subst_rawvars l) r (* assume: id is not binding *) let ldots_var = id_of_string ".." @@ -82,6 +108,12 @@ let rawconstr_of_aconstr_with_binders loc g f e = function let inner = RApp (loc,RVar (loc,ldots_var),[subst_rawvars innerl it]) in let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in subst_rawvars outerl it + | ABinderList (x,y,iter,tail) -> + let t = f e tail in let it = f e iter in + let innerl = [(ldots_var,t);(x,RVar(loc,y))] in + let inner = RApp (loc,RVar (loc,ldots_var),[subst_rawvars innerl it]) in + let outerl = [(ldots_var,inner)] in + subst_rawvars outerl it | ALambda (na,ty,c) -> let e,na = g e na in RLambda (loc,na,Explicit,f e ty,f e c) | AProd (na,ty,c) -> @@ -134,72 +166,135 @@ let rec rawconstr_of_aconstr loc x = (****************************************************************************) (* Translating a rawconstr into a notation, interpreting recursive patterns *) -let add_name r = function - | Anonymous -> () - | Name id -> r := id :: !r +let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r) +let add_name r = function Anonymous -> () | Name id -> add_id r id -let has_ldots = - List.exists - (function RApp (_,RVar(_,v),_) when v = ldots_var -> true | _ -> false) - -let compare_rawconstr f t1 t2 = match t1,t2 with - | RRef (_,r1), RRef (_,r2) -> eq_gr r1 r2 - | RVar (_,v1), RVar (_,v2) -> v1 = v2 - | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & List.for_all2 f l1 l2 - | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> - f ty1 ty2 & f c1 c2 +let split_at_recursive_part c = + let sub = ref None in + let rec aux = function + | RApp (loc0,RVar(loc,v),c::l) when v = ldots_var -> + if !sub <> None then + (* Not narrowed enough to find only one recursive part *) + raise Not_found + else + (sub := Some c; + if l = [] then RVar (loc,ldots_var) + else RApp (loc0,RVar (loc,ldots_var),l)) + | c -> map_rawconstr aux c in + let outer_iterator = aux c in + match !sub with + | None -> (* No recursive pattern found *) raise Not_found + | Some c -> + match outer_iterator with + | RVar (_,v) when v = ldots_var -> (* Not enough context *) raise Not_found + | _ -> outer_iterator, c + +let on_true_do b f c = if b then (f c; b) else b + +let compare_rawconstr f add t1 t2 = match t1,t2 with + | RRef (_,r1), RRef (_,r2) -> eq_gr r1 r2 + | RVar (_,v1), RVar (_,v2) -> on_true_do (v1 = v2) add (Name v1) + | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & list_for_all2eq f l1 l2 + | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1 | RProd (_,na1,bk1,ty1,c1), RProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> - f ty1 ty2 & f c1 c2 + on_true_do (f ty1 ty2 & f c1 c2) add na1 | RHole _, RHole _ -> true | RSort (_,s1), RSort (_,s2) -> s1 = s2 - | (RLetIn _ | RCases _ | RRec _ | RDynamic _ + | RLetIn (_,na1,b1,c1), RLetIn (_,na2,b2,c2) when na1 = na2 -> + on_true_do (f b1 b2 & f c1 c2) add na1 + | (RCases _ | RRec _ | RDynamic _ | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_ - | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _ + | _,(RCases _ | RRec _ | RDynamic _ | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _) -> error "Unsupported construction in recursive notations." - | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _ + | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ + | RHole _ | RSort _ | RLetIn _), _ -> false -let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr t1 t2 +let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr (fun _ -> ()) t1 t2 + +let subtract_loc loc1 loc2 = make_loc (fst (unloc loc1),fst (unloc loc2)-1) -let discriminate_patterns foundvars nl l1 l2 = +let check_is_hole id = function RHole _ -> () | t -> + user_err_loc (loc_of_rawconstr t,"", + strbrk "In recursive notation with binders, " ++ pr_id id ++ + strbrk " is expected to come without type.") + +let compare_recursive_parts found f (iterator,subc) = let diff = ref None in - let rec aux n c1 c2 = match c1,c2 with - | RVar (_,v1), RVar (_,v2) when v1<>v2 -> - if !diff = None then (diff := Some (v1,v2,(n>=nl)); true) - else - !diff = Some (v1,v2,(n>=nl)) or !diff = Some (v2,v1,(n compare_rawconstr (aux (n+1)) c1 c2 in - let l = list_map2_i aux 0 l1 l2 in - if not (List.for_all ((=) true) l) then - error "Both ends of the recursive pattern differ."; - match !diff with - | None -> error "Both ends of the recursive pattern are the same." - | Some (x,y,_ as discr) -> - List.iter (fun id -> - if List.mem id !foundvars - then errorlabstrm "" (strbrk "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part."); - foundvars := id::!foundvars) [x;y]; - discr + let terminator = ref None in + let rec aux c1 c2 = match c1,c2 with + | RVar(_,v), term when v = ldots_var -> + (* We found the pattern *) + assert (!terminator = None); terminator := Some term; + true + | RApp (_,RVar(_,v),l1), RApp (_,term,l2) when v = ldots_var -> + (* We found the pattern, but there are extra arguments *) + (* (this allows e.g. alternative (recursive) notation of application) *) + assert (!terminator = None); terminator := Some term; + list_for_all2eq aux l1 l2 + | RVar (_,x), RVar (_,y) when x<>y -> + (* We found the position where it differs *) + let lassoc = (!terminator <> None) in + let x,y = if lassoc then y,x else x,y in + !diff = None && (diff := Some (x,y,Some lassoc); true) + | RLambda (_,Name x,_,t_x,c), RLambda (_,Name y,_,t_y,term) + | RProd (_,Name x,_,t_x,c), RProd (_,Name y,_,t_y,term) -> + (* We found a binding position where it differs *) + check_is_hole y t_x; + check_is_hole y t_y; + !diff = None && (diff := Some (x,y,None); aux c term) + | _ -> + compare_rawconstr aux (add_name found) c1 c2 in + if aux iterator subc then + match !diff with + | None -> + let loc1 = loc_of_rawconstr iterator in + let loc2 = loc_of_rawconstr (Option.get !terminator) in + (* Here, we would need a loc made of several parts ... *) + user_err_loc (subtract_loc loc1 loc2,"", + str "Both ends of the recursive pattern are the same.") + | Some (x,y,Some lassoc) -> + let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in + let iterator = + f (if lassoc then subst_rawvars [y,RVar(dummy_loc,x)] iterator + else iterator) in + (* found have been collected by compare_constr *) + found := newfound; + AList (x,y,iterator,f (Option.get !terminator),lassoc) + | Some (x,y,None) -> + let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in + let iterator = f iterator in + (* found have been collected by compare_constr *) + found := newfound; + ABinderList (x,y,iterator,f (Option.get !terminator)) + else + raise Not_found let aconstr_and_vars_of_rawconstr a = - let found = ref [] in - let rec aux = function - | RVar (_,id) -> found := id::!found; AVar id - | RApp (_,f,args) when has_ldots args -> make_aconstr_list f args - | RApp (_,RVar (_,f),[RApp (_,t,[c]);d]) when f = ldots_var -> - (* Special case for alternative (recursive) notation of application *) - let x,y,lassoc = discriminate_patterns found 0 [c] [d] in - found := ldots_var :: !found; assert lassoc; - AList (x,y,AApp (AVar ldots_var,[AVar x]),aux t,lassoc) + let found = ref ([],[],[]) in + let rec aux c = + let keepfound = !found in + (* n^2 complexity but small and done only once per notation *) + try compare_recursive_parts found aux' (split_at_recursive_part c) + with Not_found -> + found := keepfound; + match c with + | RApp (_,RVar (loc,f),[c]) when f = ldots_var -> + (* Fall on the second part of the recursive pattern w/o having + found the first part *) + user_err_loc (loc,"", + str "Cannot find where the recursive pattern starts.") + | c -> + aux' c + and aux' = function + | RVar (_,id) -> add_id found id; AVar id | RApp (_,g,args) -> AApp (aux g, List.map aux args) | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c) | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c) | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c) | RCases (_,sty,rtntypopt,tml,eqnl) -> - let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in + let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in ACases (sty,Option.map aux rtntypopt, List.map (fun (tm,(na,x)) -> add_name found na; @@ -215,7 +310,7 @@ let aconstr_and_vars_of_rawconstr a = add_name found na; AIf (aux c,(na,Option.map aux po),aux b1,aux b2) | RRec (_,fk,idl,dll,tl,bl) -> - Array.iter (fun id -> found := id::!found) idl; + Array.iter (add_id found) idl; let dll = Array.map (List.map (fun (na,bk,oc,b) -> if bk <> Explicit then error "Binders marked as implicit not allowed in notations."; @@ -231,51 +326,61 @@ let aconstr_and_vars_of_rawconstr a = | RDynamic _ | REvar _ -> error "Existential variables not allowed in notations." - (* Recognizing recursive notations *) - and terminator_of_pat f1 ll1 lr1 = function - | RApp (loc,f2,l2) -> - if not (eq_rawconstr f1 f2) then errorlabstrm "" - (strbrk "Cannot recognize the same head to both ends of the recursive pattern."); - let nl = List.length ll1 in - let nr = List.length lr1 in - if List.length l2 <> nl + nr + 1 then - error "Both ends of the recursive pattern have different lengths."; - let ll2,l2' = list_chop nl l2 in - let t = List.hd l2' and lr2 = List.tl l2' in - let x,y,order = discriminate_patterns found nl (ll1@lr1) (ll2@lr2) in - let iter = - if order then RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2) - else RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1) in - (if order then y else x),(if order then x else y), aux iter, aux t, order - | _ -> error "One end of the recursive pattern is not an application." - - and make_aconstr_list f args = - let rec find_patterns acc = function - | RApp(_,RVar (_,a),[c]) :: l when a = ldots_var -> - (* We've found the recursive part *) - let x,y,iter,term,lassoc = terminator_of_pat f (List.rev acc) l c in - AList (x,y,iter,term,lassoc) - | a::l -> find_patterns (a::acc) l - | [] -> error "Ill-formed recursive notation." - in find_patterns [] args - in let t = aux a in (* Side effect *) t, !found -let aconstr_of_rawconstr vars a = - let a,foundvars = aconstr_and_vars_of_rawconstr a in - let check_type x = - if not (List.mem x foundvars) then - error ((string_of_id x)^" is unbound in the right-hand-side.") in - List.iter check_type vars; +let rec list_rev_mem_assoc x = function + | [] -> false + | (_,x')::l -> x = x' || list_rev_mem_assoc x l + +let check_variables vars recvars (found,foundrec,foundrecbinding) = + let useless_vars = List.map snd recvars in + let vars = List.filter (fun (y,_) -> not (List.mem y useless_vars)) vars in + let check_recvar x = + if List.mem x found then + errorlabstrm "" (pr_id x ++ + strbrk " should only be used in the recursive part of a pattern.") in + List.iter (fun (x,y) -> check_recvar x; check_recvar y) + (foundrec@foundrecbinding); + let check_bound x = + if not (List.mem x found) then + if List.mem_assoc x foundrec or List.mem_assoc x foundrecbinding + or list_rev_mem_assoc x foundrec or list_rev_mem_assoc x foundrecbinding + then + error ((string_of_id x)^" should not be bound in a recursive pattern of the right-hand side.") + else + error ((string_of_id x)^" is unbound in the right-hand side.") in + let check_pair s x y where = + if not (List.mem (x,y) where) then + errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++ + str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++ + str " position as part of a recursive pattern.") in + let check_type (x,typ) = + match typ with + | NtnInternTypeConstr -> + begin + try check_pair "term" x (List.assoc x recvars) foundrec + with Not_found -> check_bound x + end + | NtnInternTypeBinder -> + begin + try check_pair "binding" x (List.assoc x recvars) foundrecbinding + with Not_found -> check_bound x + end + | NtnInternTypeIdent -> check_bound x in + List.iter check_type vars + +let aconstr_of_rawconstr vars recvars a = + let a,found = aconstr_and_vars_of_rawconstr a in + check_variables vars recvars found; a (* Substitution of kernel names, avoiding a list of bound identifiers *) let aconstr_of_constr avoiding t = - aconstr_of_rawconstr [] (Detyping.detype false avoiding [] t) + aconstr_of_rawconstr [] [] (Detyping.detype false avoiding [] t) let rec subst_pat subst pat = match pat with @@ -319,6 +424,12 @@ let rec subst_aconstr subst bound raw = if r1' == r1 && r2' == r2 then raw else AProd (n,r1',r2') + | ABinderList (id1,id2,r1,r2) -> + let r1' = subst_aconstr subst bound r1 + and r2' = subst_aconstr subst bound r2 in + if r1' == r1 && r2' == r2 then raw else + ABinderList (id1,id2,r1',r2') + | ALetIn (n,r1,r2) -> let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in @@ -396,7 +507,7 @@ let rec subst_aconstr subst bound raw = ACast (r1',CastCoerce) let subst_interpretation subst (metas,pat) = - let bound = List.map fst (fst metas @ snd metas) in + let bound = List.map fst metas in (metas,subst_aconstr subst bound pat) let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l) @@ -434,7 +545,7 @@ let rec alpha_var id1 id2 = function let alpha_eq_val (x,y) = x = y -let bind_env alp (sigma,sigmalist as fullsigma) var v = +let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v = try let vvar = List.assoc var sigma in if alpha_eq_val (v,vvar) then fullsigma @@ -443,7 +554,10 @@ let bind_env alp (sigma,sigmalist as fullsigma) var v = (* Check that no capture of binding variables occur *) if List.exists (fun (id,_) ->occur_rawconstr id v) alp then raise No_match; (* TODO: handle the case of multiple occs in different scopes *) - ((var,v)::sigma,sigmalist) + ((var,v)::sigma,sigmalist,sigmabinders) + +let bind_binder (sigma,sigmalist,sigmabinders) x bl = + (sigma,sigmalist,(x,List.rev bl)::sigmabinders) let match_fix_kind fk1 fk2 = match (fk1,fk2) with @@ -458,13 +572,9 @@ let match_opt f sigma t1 t2 = match (t1,t2) with | Some t1, Some t2 -> f sigma t1 t2 | _ -> raise No_match -let rawconstr_of_name = function - | Anonymous -> RHole (dummy_loc,Evd.InternalHole) - | Name id -> RVar (dummy_loc,id) - let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with - | (na,Name id2) when List.mem id2 metas -> - alp, bind_env alp sigma id2 (rawconstr_of_name na) + | (Name id1,Name id2) when List.mem id2 (fst metas) -> + alp, bind_env alp sigma id2 (RVar (dummy_loc,id1)) | (Name id1,Name id2) -> (id1,id2)::alp,sigma | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match @@ -482,33 +592,80 @@ let adjust_application_n n loc f l = let l1,l2 = list_chop (List.length l - n) l in if l1 = [] then f,l else RApp (loc,f,l1), l2 -let match_alist match_fun metas sigma l1 l2 x iter termin lassoc = - (* match the iterator at least once *) - let sigmavar,sigmalist = - List.fold_left2 (match_fun (ldots_var::metas)) sigma l1 l2 in - (* Recover the recursive position *) - let rest = List.assoc ldots_var sigmavar in - (* Recover the first element *) - let t1 = List.assoc x sigmavar in - let sigmavar = List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in - (* try to find the remaining elements or the terminator *) - let rec match_alist_tail metas sigma acc rest = +let glue_letin_with_decls = true + +let rec match_iterated_binders islambda decls = function + | RLambda (_,na,bk,t,b) when islambda -> + match_iterated_binders islambda ((na,bk,None,t)::decls) b + | RProd (_,(Name _ as na),bk,t,b) when not islambda -> + match_iterated_binders islambda ((na,bk,None,t)::decls) b + | RLetIn (loc,na,c,b) when glue_letin_with_decls -> + match_iterated_binders islambda + ((na,Explicit (*?*), Some c,RHole(loc,Evd.BinderType na))::decls) b + | b -> (decls,b) + +let remove_sigma x (sigmavar,sigmalist,sigmabinders) = + (List.remove_assoc x sigmavar,sigmalist,sigmabinders) + +let rec match_abinderlist_with_app match_fun metas sigma rest x iter termin = + let rec aux sigma acc rest = try - let sigmavar,sigmalist = match_fun (ldots_var::metas) sigma rest iter in - let rest = List.assoc ldots_var sigmavar in - let t = List.assoc x sigmavar in - let sigmavar = - List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in - match_alist_tail metas (sigmavar,sigmalist) (t::acc) rest - with No_match -> - List.rev acc, match_fun metas (sigmavar,sigmalist) rest termin in - let tl,(sigmavar,sigmalist) = match_alist_tail metas sigma [t1] rest in - (sigmavar, (x,if lassoc then List.rev tl else tl)::sigmalist) - -let rec match_ alp metas sigma a1 a2 = match (a1,a2) with - | r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1 + let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in + let rest = List.assoc ldots_var (pi1 sigma) in + let b = match List.assoc x (pi3 sigma) with [b] -> b | _ ->assert false in + let sigma = remove_sigma x (remove_sigma ldots_var sigma) in + aux sigma (b::acc) rest + with No_match when acc <> [] -> + acc, match_fun metas sigma rest termin in + let bl,sigma = aux sigma [] rest in + bind_binder sigma x bl + +let match_alist match_fun metas sigma rest x iter termin lassoc = + let rec aux sigma acc rest = + try + let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in + let rest = List.assoc ldots_var (pi1 sigma) in + let t = List.assoc x (pi1 sigma) in + let sigma = remove_sigma x (remove_sigma ldots_var sigma) in + aux sigma (t::acc) rest + with No_match when acc <> [] -> + acc, match_fun metas sigma rest termin in + let l,sigma = aux sigma [] rest in + (pi1 sigma, (x,if lassoc then l else List.rev l)::pi2 sigma, pi3 sigma) + +let rec match_ alp (tmetas,blmetas as metas) sigma a1 a2 = match (a1,a2) with + + (* Matching notation variable *) + | r1, AVar id2 when List.mem id2 tmetas -> bind_env alp sigma id2 r1 + + (* Matching recursive notations for terms *) + | r1, AList (x,_,iter,termin,lassoc) -> + match_alist (match_ alp) metas sigma r1 x iter termin lassoc + + (* Matching recursive notations for binders: ad hoc cases supporting let-in *) + | RLambda (_,na1,bk,t1,b1), ABinderList (x,_,ALambda (Name id2,_,b2),termin)-> + let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in + (* TODO: address the possibility that termin is a Lambda itself *) + match_ alp metas (bind_binder sigma x decls) b termin + | RProd (_,na1,bk,t1,b1), ABinderList (x,_,AProd (Name id2,_,b2),termin) + when na1 <> Anonymous -> + let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in + (* TODO: address the possibility that termin is a Prod itself *) + match_ alp metas (bind_binder sigma x decls) b termin + (* Matching recursive notations for binders: general case *) + | r, ABinderList (x,_,iter,termin) -> + match_abinderlist_with_app (match_ alp) metas sigma r x iter termin + + (* Matching individual binders as part of a recursive pattern *) + | RLambda (_,na,bk,t,b1), ALambda (Name id,_,b2) when List.mem id blmetas -> + match_ alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 + | RProd (_,na,bk,t,b1), AProd (Name id,_,b2) + when List.mem id blmetas & na <> Anonymous -> + match_ alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 + + (* Matching compositionally *) | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma - | RRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma + | RRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma | RApp (loc,f1,l1), AApp (f2,l2) -> let n1 = List.length l1 and n2 = List.length l2 in @@ -519,11 +676,6 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with let l11,l12 = list_chop (n1-n2) l1 in RApp (loc,f1,l11),l12, f2,l2 else f1,l1, f2, l2 in List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2 - | RApp (loc,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc) - when List.length l1 >= List.length l2 -> - let f1,l1 = adjust_application_n (List.length l2) loc f1 l1 in - match_alist (match_ alp) - metas sigma (f1::l1) (f2::l2) x iter termin lassoc | RLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) -> match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2 | RProd (_,na1,_,t1,b1), AProd (na2,t2,b2) -> @@ -588,38 +740,36 @@ and match_equations alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) = (alp,sigma) patl1 patl2 in match_ alp metas sigma rhs1 rhs2 -type scope_name = string - -type tmp_scope_name = scope_name - -type subscopes = tmp_scope_name option * scope_name list - -type interpretation = - (* regular vars of notation / recursive parts of notation / body *) - ((identifier * subscopes) list * (identifier * subscopes) list) * aconstr - -let match_aconstr c ((metas_scl,metaslist_scl),pat) = - let vars = List.map fst metas_scl @ List.map fst metaslist_scl in - let subst,substlist = match_ [] vars ([],[]) c pat in +let match_aconstr c (metas,pat) = + let vars = list_split_by (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in + let vars = (List.map fst (fst vars), List.map fst (snd vars)) in + let terms,termlists,binders = match_ [] vars ([],[],[]) c pat in (* Reorder canonically the substitution *) let find x = - try List.assoc x subst + try List.assoc x terms with Not_found -> (* Happens for binders bound to Anonymous *) (* Find a better way to propagate Anonymous... *) RVar (dummy_loc,x) in - List.map (fun (x,scl) -> (find x,scl)) metas_scl, - List.map (fun (x,scl) -> (List.assoc x substlist,scl)) metaslist_scl + List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> + match typ with + | NtnTypeConstr -> + ((find x, scl)::terms',termlists',binders') + | NtnTypeConstrList -> + (terms',(List.assoc x termlists,scl)::termlists',binders') + | NtnTypeBinderList -> + (terms',termlists',(List.assoc x binders,scl)::binders')) + metas ([],[],[]) (* Matching cases pattern *) -let bind_env_cases_pattern (sigma,sigmalist as fullsigma) var v = +let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v = try let vvar = List.assoc var sigma in if v=vvar then fullsigma else raise No_match with Not_found -> (* TODO: handle the case of multiple occs in different scopes *) - (var,v)::sigma,sigmalist + (var,v)::sigma,sigmalist,x let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with | r1, AVar id2 when List.mem id2 metas -> bind_env_cases_pattern sigma id2 r1 @@ -639,26 +789,21 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with (* All parameters must be _ *) List.iter (function AHole _ -> () | _ -> raise No_match) p2; List.fold_left2 (match_cases_pattern metas) sigma args1 args2 - | PatCstr (loc,(ind,_ as r1),args1,_), - AList (x,_,(AApp (ARef (ConstructRef r2),l2) as iter),termin,lassoc) - when r1 = r2 -> - let nparams = Inductive.inductive_params (Global.lookup_inductive ind) in - assert (List.length args1 + nparams = List.length l2); - let (p2,args2) = list_chop nparams l2 in - List.iter (function AHole _ -> () | _ -> raise No_match) p2; - match_alist match_cases_pattern - metas sigma args1 args2 x iter termin lassoc + | r1, AList (x,_,iter,termin,lassoc) -> + match_alist (fun (metas,_) -> match_cases_pattern metas) + (metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc | _ -> raise No_match -let match_aconstr_cases_pattern c ((metas_scl,metaslist_scl),pat) = - let vars = List.map fst metas_scl @ List.map fst metaslist_scl in - let subst,substlist = match_cases_pattern vars ([],[]) c pat in +let match_aconstr_cases_pattern c (metas,pat) = + let vars = List.map fst metas in + let terms,termlists,() = match_cases_pattern vars ([],[],()) c pat in (* Reorder canonically the substitution *) - let find x subst = - try List.assoc x subst - with Not_found -> anomaly "match_aconstr_cases_pattern" in - List.map (fun (x,scl) -> (find x subst,scl)) metas_scl, - List.map (fun (x,scl) -> (find x substlist,scl)) metaslist_scl + List.fold_right (fun (x,(scl,typ)) (terms',termlists') -> + match typ with + | NtnTypeConstr -> ((List.assoc x terms, scl)::terms',termlists') + | NtnTypeConstrList -> (terms',(List.assoc x termlists,scl)::termlists') + | NtnTypeBinderList -> assert false) + metas ([],[]) (**********************************************************************) (*s Concrete syntax for terms *) @@ -675,19 +820,20 @@ type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) type prim_token = Numeral of Bigint.bigint | String of string -type 'a notation_substitution = - 'a list * (* for recursive notations: *) 'a list list - type cases_pattern_expr = | CPatAlias of loc * cases_pattern_expr * identifier | CPatCstr of loc * reference * cases_pattern_expr list | CPatAtom of loc * reference option | CPatOr of loc * cases_pattern_expr list - | CPatNotation of loc * notation * cases_pattern_expr notation_substitution + | CPatNotation of loc * notation * cases_pattern_notation_substitution | CPatPrim of loc * prim_token - | CPatRecord of loc * (reference * cases_pattern_expr) list + | CPatRecord of Util.loc * (reference * cases_pattern_expr) list | CPatDelimiters of loc * string * cases_pattern_expr +and cases_pattern_notation_substitution = + cases_pattern_expr list * (** for constr subterms *) + cases_pattern_expr list list (** for recursive notations *) + type constr_expr = | CRef of reference | CFix of loc * identifier located * fix_expr list @@ -701,18 +847,18 @@ type constr_expr = (constr_expr * explicitation located option) list | CRecord of loc * constr_expr option * (reference * constr_expr) list | CCases of loc * case_style * constr_expr option * - (constr_expr * (name option * constr_expr option)) list * + (constr_expr * (name located option * constr_expr option)) list * (loc * cases_pattern_expr list located list * constr_expr) list - | CLetTuple of loc * name list * (name option * constr_expr option) * + | CLetTuple of loc * name located list * (name located option * constr_expr option) * constr_expr * constr_expr - | CIf of loc * constr_expr * (name option * constr_expr option) + | CIf of loc * constr_expr * (name located option * constr_expr option) * constr_expr * constr_expr | CHole of loc * Evd.hole_kind option | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key * constr_expr list option | CSort of loc * rawsort | CCast of loc * constr_expr * constr_expr cast_type - | CNotation of loc * notation * constr_expr notation_substitution + | CNotation of loc * notation * constr_notation_substitution | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr | CPrim of loc * prim_token | CDelimiters of loc * string * constr_expr @@ -721,14 +867,6 @@ type constr_expr = and fix_expr = identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr -and local_binder = - | LocalRawDef of name located * constr_expr - | LocalRawAssum of name located list * binder_kind * constr_expr - -and typeclass_constraint = name located * binding_kind * constr_expr - -and typeclass_context = typeclass_constraint list - and cofix_expr = identifier located * local_binder list * constr_expr * constr_expr @@ -737,6 +875,19 @@ and recursion_order_expr = | CWfRec of constr_expr | CMeasureRec of constr_expr * constr_expr option (* measure, relation *) +and local_binder = + | LocalRawDef of name located * constr_expr + | LocalRawAssum of name located list * binder_kind * constr_expr + +and constr_notation_substitution = + constr_expr list * (* for constr subterms *) + constr_expr list list * (* for recursive notations *) + local_binder list list (* for binders subexpressions *) + +type typeclass_constraint = name located * binding_kind * constr_expr + +and typeclass_context = typeclass_constraint list + type constr_pattern_expr = constr_expr (***********************) @@ -789,6 +940,15 @@ let cases_pattern_expr_loc = function | CPatPrim (loc,_) -> loc | CPatDelimiters (loc,_,_) -> loc +let local_binder_loc = function + | LocalRawAssum ((loc,_)::_,_,t) + | LocalRawDef ((loc,_),t) -> join_loc loc (constr_loc t) + | LocalRawAssum ([],_,_) -> assert false + +let local_binders_loc bll = + if bll = [] then dummy_loc else + join_loc (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll)) + let occur_var_constr_ref id = function | Ident (loc,id') -> id = id' | Qualid _ -> false @@ -798,7 +958,7 @@ let ids_of_cases_indtype = let rec vars_of = function (* We deal only with the regular cases *) | CApp (_,_,l) -> List.fold_left add_var [] (List.map fst l) - | CNotation (_,_,(l,[])) + | CNotation (_,_,(l,[],[])) (* assume the ntn is applicative and does not instantiate the head !! *) | CAppExpl (_,_,l) -> List.fold_left add_var [] l | CDelimiters(_,_,c) -> vars_of c @@ -809,7 +969,7 @@ let ids_of_cases_tomatch tms = List.fold_right (fun (_,(ona,indnal)) l -> Option.fold_right (fun t -> (@) (ids_of_cases_indtype t)) - indnal (Option.fold_right name_cons ona l)) + indnal (Option.fold_right (down_located name_cons) ona l)) tms [] let is_constructor id = @@ -849,7 +1009,7 @@ let rec fold_local_binders g f n acc b = function f n (fold_local_binders g f n' acc b l) t | LocalRawDef ((_,na),t)::l -> f n (fold_local_binders g f (name_fold g na n) acc b l) t - | _ -> + | [] -> f n acc b let fold_constr_expr_with_binders g f n acc = function @@ -860,7 +1020,11 @@ let fold_constr_expr_with_binders g f n acc = function | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a] | CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b | CCast (loc,a,CastCoerce) -> f n acc a - | CNotation (_,_,(l,ll)) -> List.fold_left (f n) acc (l@List.flatten ll) + | CNotation (_,_,(l,ll,bll)) -> + (* The following is an approximation: we don't know exactly if + an ident is binding nor to which subterms bindings apply *) + let acc = List.fold_left (f n) acc (l@List.flatten ll) in + List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (dummy_loc,None)) bl) acc bll | CGeneralization (_,_,_,c) -> f n acc c | CDelimiters (loc,_,a) -> f n acc a | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ -> @@ -874,11 +1038,12 @@ let fold_constr_expr_with_binders g f n acc = function let ids = ids_of_pattern_list patl in f (Idset.fold g ids n) acc rhs) bl acc | CLetTuple (loc,nal,(ona,po),b,c) -> - let n' = List.fold_right (name_fold g) nal n in - f (Option.fold_right (name_fold g) ona n') (f n acc b) c + let n' = List.fold_right (down_located (name_fold g)) nal n in + f (Option.fold_right (down_located (name_fold g)) ona n') (f n acc b) c | CIf (_,c,(ona,po),b1,b2) -> let acc = f n (f n (f n acc b1) b2) c in - Option.fold_left (f (Option.fold_right (name_fold g) ona n)) acc po + Option.fold_left + (f (Option.fold_right (down_located (name_fold g)) ona n)) acc po | CFix (loc,_,l) -> let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in List.fold_right (fun (_,(_,o),lb,t,c) acc -> @@ -961,21 +1126,29 @@ let coerce_to_name = function (* Interpret the index of a recursion order annotation *) -let index_of_annot bl na = +let split_at_annot bl na = let names = List.map snd (names_of_local_assums bl) in match na with | None -> - if names = [] then error "A fixpoint needs at least one parameter." - else None + if names = [] then error "A fixpoint needs at least one parameter." + else [], bl | Some (loc, id) -> - try Some (list_index0 (Name id) names) - with Not_found -> - user_err_loc(loc,"", - str "No parameter named " ++ Nameops.pr_id id ++ str".") + let rec aux acc = function + | LocalRawAssum (bls, k, t) as x :: rest -> + let l, r = list_split_when (fun (loc, na) -> na = Name id) bls in + if r = [] then aux (x :: acc) rest + else + (List.rev (if l = [] then acc else LocalRawAssum (l, k, t) :: acc), + LocalRawAssum (r, k, t) :: rest) + | LocalRawDef _ as x :: rest -> aux (x :: acc) rest + | [] -> + user_err_loc(loc,"", + str "No parameter named " ++ Nameops.pr_id id ++ str".") + in aux [] bl (* Used in correctness and interface *) -let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e +let map_binder g e nal = List.fold_right (down_located (name_fold g)) nal e let map_binders f g e bl = (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) @@ -1005,8 +1178,10 @@ let map_constr_expr_with_binders g f e = function | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b) | CCast (loc,a,CastConv (k,b)) -> CCast (loc,f e a,CastConv(k, f e b)) | CCast (loc,a,CastCoerce) -> CCast (loc,f e a,CastCoerce) - | CNotation (loc,n,(l,ll)) -> - CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll)) + | CNotation (loc,n,(l,ll,bll)) -> + (* This is an approximation because we don't know what binds what *) + CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll, + List.map (fun bl -> snd (map_local_binders f g e bl)) bll)) | CGeneralization (loc,b,a,c) -> CGeneralization (loc,b,a,f e c) | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a) | CHole _ | CEvar _ | CPatVar _ | CSort _ @@ -1019,11 +1194,11 @@ let map_constr_expr_with_binders g f e = function let po = Option.map (f (List.fold_right g ids e)) rtnpo in CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl) | CLetTuple (loc,nal,(ona,po),b,c) -> - let e' = List.fold_right (name_fold g) nal e in - let e'' = Option.fold_right (name_fold g) ona e in + let e' = List.fold_right (down_located (name_fold g)) nal e in + let e'' = Option.fold_right (down_located (name_fold g)) ona e in CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c) | CIf (loc,c,(ona,po),b1,b2) -> - let e' = Option.fold_right (name_fold g) ona e in + let e' = Option.fold_right (down_located (name_fold g)) ona e in CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2) | CFix (loc,id,dl) -> CFix (loc,id,List.map (fun (id,n,bl,t,d) -> @@ -1067,16 +1242,21 @@ type 'a module_signature = | Check of 'a list (* ... <: T1 <: T2, possibly empty *) (* Returns the ranges of locs of the notation that are not occupied by args *) -(* and which are them occupied by proper symbols of the notation (or spaces) *) +(* and which are then occupied by proper symbols of the notation (or spaces) *) -let locs_of_notation f loc (args,argslist) ntn = +let locs_of_notation loc locs ntn = let (bl,el) = Util.unloc loc in + let locs = List.map Util.unloc locs in let rec aux pos = function | [] -> if pos = el then [] else [(pos,el-1)] - | a::l -> - let ba,ea = Util.unloc (f a) in - if pos = ba then aux ea l else (pos,ba-1)::aux ea l - in aux bl (args@List.flatten argslist) + | (ba,ea)::l ->if pos = ba then aux ea l else (pos,ba-1)::aux ea l + in aux bl (Sort.list (fun l1 l2 -> fst l1 < fst l2) locs) + +let ntn_loc loc (args,argslist,binderslist) = + locs_of_notation loc + (List.map constr_loc (args@List.flatten argslist)@ + List.map local_binders_loc binderslist) -let ntn_loc = locs_of_notation constr_loc -let patntn_loc = locs_of_notation cases_pattern_expr_loc +let patntn_loc loc (args,argslist) = + locs_of_notation loc + (List.map cases_pattern_expr_loc (args@List.flatten argslist)) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 0918a4de..5e49d2ea 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: topconstr.mli 13332 2010-07-26 22:12:43Z msozeau $ i*) (*i*) open Pp @@ -32,6 +32,7 @@ type aconstr = (* Part only in [rawconstr] *) | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr + | ABinderList of identifier * identifier * aconstr * aconstr | ALetIn of name * aconstr * aconstr | ACases of case_style * aconstr option * (aconstr * (name * (inductive * int * name list) option)) list * @@ -46,11 +47,34 @@ type aconstr = | APatVar of patvar | ACast of aconstr * aconstr cast_type +type scope_name = string + +type tmp_scope_name = scope_name + +type subscopes = tmp_scope_name option * scope_name list + +(** Type of the meta-variables of an aconstr: in a recursive pattern x..y, + x carries the sequence of objects bound to the list x..y *) +type notation_var_instance_type = + | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList + +(** Type of variables when interpreting a constr_expr as an aconstr: + in a recursive pattern x..y, both x and y carry the individual type + of each element of the list x..y *) +type notation_var_internalization_type = + | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent + +(** This characterizes to what a notation is interpreted to *) +type interpretation = + (identifier * (subscopes * notation_var_instance_type)) list * aconstr + (**********************************************************************) (* Translate a rawconstr into a notation given the list of variables *) (* bound by the notation; also interpret recursive patterns *) -val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr +val aconstr_of_rawconstr : + (identifier * notation_var_internalization_type) list -> + (identifier * identifier) list -> rawconstr -> aconstr (* Name of the special identifier used to encode recursive notations *) val ldots_var : identifier @@ -68,23 +92,14 @@ val rawconstr_of_aconstr_with_binders : loc -> val rawconstr_of_aconstr : loc -> aconstr -> rawconstr (**********************************************************************) -(* [match_aconstr metas] matches a rawconstr against an aconstr with *) -(* metavariables in [metas]; raise [No_match] if the matching fails *) +(* [match_aconstr] matches a rawconstr against a notation *) +(* interpretation raise [No_match] if the matching fails *) exception No_match -type scope_name = string - -type tmp_scope_name = scope_name - -type subscopes = tmp_scope_name option * scope_name list - -type interpretation = - (* regular vars of notation / recursive parts of notation / body *) - ((identifier * subscopes) list * (identifier * subscopes) list) * aconstr - val match_aconstr : rawconstr -> interpretation -> - (rawconstr * subscopes) list * (rawconstr list * subscopes) list + (rawconstr * subscopes) list * (rawconstr list * subscopes) list * + (rawdecl list * subscopes) list val match_aconstr_cases_pattern : cases_pattern -> interpretation -> (cases_pattern * subscopes) list * (cases_pattern list * subscopes) list @@ -113,19 +128,20 @@ type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) type prim_token = Numeral of Bigint.bigint | String of string -type 'a notation_substitution = - 'a list * (* for recursive notations: *) 'a list list - type cases_pattern_expr = | CPatAlias of loc * cases_pattern_expr * identifier | CPatCstr of loc * reference * cases_pattern_expr list | CPatAtom of loc * reference option | CPatOr of loc * cases_pattern_expr list - | CPatNotation of loc * notation * cases_pattern_expr notation_substitution + | CPatNotation of loc * notation * cases_pattern_notation_substitution | CPatPrim of loc * prim_token | CPatRecord of Util.loc * (reference * cases_pattern_expr) list | CPatDelimiters of loc * string * cases_pattern_expr +and cases_pattern_notation_substitution = + cases_pattern_expr list * (** for constr subterms *) + cases_pattern_expr list list (** for recursive notations *) + type constr_expr = | CRef of reference | CFix of loc * identifier located * fix_expr list @@ -139,18 +155,18 @@ type constr_expr = (constr_expr * explicitation located option) list | CRecord of loc * constr_expr option * (reference * constr_expr) list | CCases of loc * case_style * constr_expr option * - (constr_expr * (name option * constr_expr option)) list * + (constr_expr * (name located option * constr_expr option)) list * (loc * cases_pattern_expr list located list * constr_expr) list - | CLetTuple of loc * name list * (name option * constr_expr option) * + | CLetTuple of loc * name located list * (name located option * constr_expr option) * constr_expr * constr_expr - | CIf of loc * constr_expr * (name option * constr_expr option) + | CIf of loc * constr_expr * (name located option * constr_expr option) * constr_expr * constr_expr | CHole of loc * Evd.hole_kind option | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key * constr_expr list option | CSort of loc * rawsort | CCast of loc * constr_expr * constr_expr cast_type - | CNotation of loc * notation * constr_expr notation_substitution + | CNotation of loc * notation * constr_notation_substitution | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr | CPrim of loc * prim_token | CDelimiters of loc * string * constr_expr @@ -172,6 +188,11 @@ and local_binder = | LocalRawDef of name located * constr_expr | LocalRawAssum of name located list * binder_kind * constr_expr +and constr_notation_substitution = + constr_expr list * (** for constr subterms *) + constr_expr list list * (** for recursive notations *) + local_binder list list (** for binders subexpressions *) + type typeclass_constraint = name located * binding_kind * constr_expr and typeclass_context = typeclass_constraint list @@ -185,6 +206,8 @@ val constr_loc : constr_expr -> loc val cases_pattern_expr_loc : cases_pattern_expr -> loc +val local_binders_loc : local_binder list -> loc + val replace_vars_constr_expr : (identifier * identifier) list -> constr_expr -> constr_expr @@ -208,7 +231,7 @@ val coerce_reference_to_id : reference -> identifier val coerce_to_id : constr_expr -> identifier located val coerce_to_name : constr_expr -> name located -val index_of_annot : local_binder list -> identifier located option -> int option +val split_at_annot : local_binder list -> identifier located option -> local_binder list * local_binder list val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr val prod_constr_expr : constr_expr -> local_binder list -> constr_expr @@ -256,7 +279,6 @@ type 'a module_signature = | Check of 'a list (* ... <: T1 <: T2, possibly empty *) val ntn_loc : - Util.loc -> constr_expr notation_substitution -> string -> (int * int) list + Util.loc -> constr_notation_substitution -> string -> (int * int) list val patntn_loc : - Util.loc -> cases_pattern_expr notation_substitution -> string -> - (int * int) list + Util.loc -> cases_pattern_notation_substitution -> string -> (int * int) list -- cgit v1.2.3