From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- interp/constrextern.ml | 54 +++++----- interp/constrintern.ml | 154 ++++++++++++++++++--------- interp/constrintern.mli | 19 +++- interp/notation.ml | 31 +++--- interp/notation.mli | 17 +-- interp/topconstr.ml | 269 ++++++++++++++++++++++++++++++------------------ interp/topconstr.mli | 59 +++++++---- 7 files changed, 389 insertions(+), 214 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 570d113d..ffedcfff 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrextern.ml 8997 2006-07-03 16:40:20Z herbelin $ *) +(* $Id: constrextern.ml 9226 2006-10-09 16:11:01Z herbelin $ *) (*i*) open Pp @@ -295,9 +295,6 @@ let same_rawconstr c d = (**********************************************************************) (* mapping patterns to cases_pattern_expr *) -let make_current_scopes (scopt,scopes) = - option_fold_right push_scope scopt scopes - let has_curly_brackets ntn = String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or String.sub ntn (String.length ntn - 6) 6 = " { _ }" or @@ -401,14 +398,14 @@ let match_aconstr_cases_pattern c (metas_scl,pat) = List.map (fun (x,scl) -> (find x subst,scl)) metas_scl (* Better to use extern_rawconstr composed with injection/retraction ?? *) -let rec extern_cases_pattern_in_scope scopes vars pat = +let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = try if !Options.raw_print or !print_no_symbol then raise No_match; let (na,sc,p) = uninterp_prim_token_cases_pattern pat in - match availability_of_prim_token sc (make_current_scopes scopes) with + match availability_of_prim_token sc scopes with | None -> raise No_match | Some key -> - let loc = pattern_loc pat in + let loc = cases_pattern_loc pat in insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na with No_match -> try @@ -440,17 +437,15 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function (* Try availability of interpretation ... *) match keyrule with | NotationRule (sc,ntn) -> - let scopes' = make_current_scopes (tmp_scope, scopes) in - (match availability_of_notation (sc,ntn) scopes' with + (match availability_of_notation (sc,ntn) allscopes with (* Uninterpretation is not allowed in current context *) | None -> raise No_match (* Uninterpretation is allowed in current context *) | Some (scopt,key) -> - let scopes = make_current_scopes (scopt, scopes) in + let scopes' = option_cons scopt scopes in let l = List.map (fun (c,(scopt,scl)) -> - extern_cases_pattern_in_scope - (scopt,List.fold_right push_scope scl scopes) vars c) + extern_cases_pattern_in_scope (scopt,scl@scopes') vars c) subst in insert_pat_delimiters loc (make_pat_notation loc ntn l) key) | SynDefRule kn -> @@ -460,7 +455,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function No_match -> extern_symbol_pattern allscopes vars t rules let extern_cases_pattern vars p = - extern_cases_pattern_in_scope (None,Notation.current_scopes()) vars p + extern_cases_pattern_in_scope (None,[]) vars p (**********************************************************************) (* Externalising applications *) @@ -607,7 +602,7 @@ let rec share_fix_binders n rbl ty def = let extern_possible_prim_token scopes r = try let (sc,n) = uninterp_prim_token r in - match availability_of_prim_token sc (make_current_scopes scopes) with + match availability_of_prim_token sc scopes with | None -> None | Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key) with No_match -> @@ -754,11 +749,16 @@ let rec extern inctx scopes vars r = | RDynamic (loc,d) -> CDynamic (loc,d) -and extern_typ (_,scopes) = extern true (Some Notation.type_scope,scopes) +and extern_typ (_,scopes) = + extern true (Some Notation.type_scope,scopes) and sub_extern inctx (_,scopes) = extern inctx (None,scopes) -and factorize_prod scopes vars aty = function +and factorize_prod scopes vars aty c = + try + if !Options.raw_print or !print_no_symbol then raise No_match; + ([],extern_symbol scopes vars c (uninterp_notations c)) + with No_match -> match c with | RProd (loc,(Name id as na),ty,c) when same aty (extern_typ scopes vars (anonymize_if_reserved na ty)) & not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *) @@ -766,7 +766,11 @@ and factorize_prod scopes vars aty = function ((loc,Name id)::nal,c) | c -> ([],extern_typ scopes vars c) -and factorize_lambda inctx scopes vars aty = function +and factorize_lambda inctx scopes vars aty c = + try + if !Options.raw_print or !print_no_symbol then raise No_match; + ([],extern_symbol scopes vars c (uninterp_notations c)) + with No_match -> match c with | RLambda (loc,na,ty,c) when same aty (extern_typ scopes vars (anonymize_if_reserved na ty)) & not (occur_name na aty) (* To avoid na in ty' escapes scope *) @@ -817,17 +821,16 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function let e = match keyrule with | NotationRule (sc,ntn) -> - let scopes' = make_current_scopes (tmp_scope, scopes) in - (match availability_of_notation (sc,ntn) scopes' with + (match availability_of_notation (sc,ntn) allscopes with (* Uninterpretation is not allowed in current context *) | None -> raise No_match (* Uninterpretation is allowed in current context *) | Some (scopt,key) -> - let scopes = make_current_scopes (scopt, scopes) in + let scopes' = option_cons scopt scopes in let l = List.map (fun (c,(scopt,scl)) -> extern (* assuming no overloading: *) true - (scopt,List.fold_right push_scope scl scopes) vars c) + (scopt,scl@scopes') vars c) subst in insert_delimiters (make_notation loc ntn l) key) | SynDefRule kn -> @@ -847,10 +850,10 @@ and extern_recursion_order scopes vars = function let extern_rawconstr vars c = - extern false (None,Notation.current_scopes()) vars c + extern false (None,[]) vars c let extern_rawtype vars c = - extern_typ (None,Notation.current_scopes()) vars c + extern_typ (None,[]) vars c (******************************************************************) (* Main translation function from constr -> constr_expr *) @@ -861,7 +864,7 @@ let extern_constr_gen at_top scopt env t = let avoid = if at_top then ids_of_context env else [] in let r = Detyping.detype at_top avoid (names_of_rel_context env) t in let vars = vars_of_env env in - extern (not at_top) (scopt,Notation.current_scopes()) vars r + extern (not at_top) (scopt,[]) vars r let extern_constr_in_scope at_top scope env t = extern_constr_gen at_top (Some scope) env t @@ -962,5 +965,4 @@ and raw_of_eqn env constr construct_nargs branch = buildrec [] [] env construct_nargs branch let extern_constr_pattern env pat = - extern true (None,Notation.current_scopes()) Idset.empty - (raw_of_pat env pat) + extern true (None,[]) Idset.empty (raw_of_pat env pat) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 355bac1d..d09430dc 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrintern.ml 8997 2006-07-03 16:40:20Z herbelin $ *) +(* $Id: constrintern.ml 9226 2006-10-09 16:11:01Z herbelin $ *) open Pp open Util @@ -118,6 +118,11 @@ let error_bad_inductive_type loc = user_err_loc (loc,"",str "This should be an inductive type applied to names or \"_\"") +let error_inductive_parameter_not_implicit loc = + user_err_loc (loc,"", str + ("The parameters of inductive types do not bind in\n"^ + "the 'return' clauses; they must be replaced by '_' in the 'in' clauses.")) + (**********************************************************************) (* Dump of globalization (to be used by coqdoc) *) let token_number = ref 0 @@ -151,7 +156,7 @@ let loc_of_notation f loc args ntn = else snd (unloc (f (List.hd args))) let ntn_loc = loc_of_notation constr_loc -let patntn_loc = loc_of_notation cases_pattern_loc +let patntn_loc = loc_of_notation cases_pattern_expr_loc let dump_notation_location pos ((path,df),sc) = let rec next growing = @@ -216,7 +221,7 @@ let contract_pat_notation ntn l = (**********************************************************************) (* Remembering the parsing scope of variables in notations *) -let make_current_scope (scopt,scopes) = option_cons scopt scopes +let make_current_scope (tmp_scope,scopes) = option_cons tmp_scope scopes let set_var_scope loc id (_,scopt,scopes) varscopes = let idscopes = List.assoc id varscopes in @@ -356,8 +361,8 @@ let rec has_duplicate = function | x::l -> if List.mem x l then (Some x) else has_duplicate l let loc_of_lhs lhs = - join_loc (cases_pattern_loc (List.hd (List.hd lhs))) - (cases_pattern_loc (list_last (list_last lhs))) + join_loc (cases_pattern_expr_loc (List.hd (List.hd lhs))) + (cases_pattern_expr_loc (list_last (list_last lhs))) let check_linearity lhs ids = match has_duplicate ids with @@ -553,16 +558,15 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope = intern_cases_pattern genv scopes aliases tmp_scope a | CPatNotation (loc, ntn, args) -> let ntn,args = contract_pat_notation ntn args in - let scopes = option_cons tmp_scope scopes in - let ((ids,c),df) = Notation.interp_notation loc ntn scopes in + let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in if !dump then dump_notation_location (patntn_loc loc args ntn) df; let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in subst_cases_pattern loc aliases (intern_cases_pattern genv) subst scopes c | CPatPrim (loc, p) -> - let scopes = option_cons tmp_scope scopes in let a = alias_of aliases in - let (c,df) = Notation.interp_prim_token_cases_pattern loc p a scopes in + let (c,df) = Notation.interp_prim_token_cases_pattern loc p a + (tmp_scope,scopes) in if !dump then dump_notation_location (fst (unloc loc)) df; (ids,[subst,c]) | CPatDelimiters (loc, key, e) -> @@ -689,15 +693,20 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Syntax extensions *) -let traverse_binder subst id (ids,tmpsc,scopes as env) = +let traverse_binder subst (renaming,(ids,tmpsc,scopes as env)) id = try - (* Binders bound in the notation are consider first-order object *) - (* and binders not bound in the notation do not capture variables *) - (* outside the notation *) + (* Binders bound in the notation are considered first-order objects *) let _,id' = coerce_to_id (fst (List.assoc id subst)) in - id', (Idset.add id' ids,tmpsc,scopes) + (renaming,(Idset.add id' ids,tmpsc,scopes)), id' with Not_found -> - id, env + (* 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.map snd renaming in + let fvs = List.flatten (List.map Idset.elements fvs1) @ fvs2 in + let id' = next_ident_away id fvs in + let renaming' = if id=id' then renaming else (id,id')::renaming in + (renaming',env), id' let decode_constrlist_value = function | CAppExpl (_,_,l) -> l @@ -707,7 +716,7 @@ 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 (ids,_,scopes as _env) = +let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) = function | AVar id -> begin @@ -716,6 +725,9 @@ let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as _env) = try let (a,(scopt,subscopes)) = List.assoc id subst in interp (ids,scopt,subscopes@scopes) a + with Not_found -> + try + RVar (loc,List.assoc id renaming) with Not_found -> (* Happens for local notation joint with inductive/fixpoint defs *) RVar (loc,id) @@ -725,28 +737,28 @@ let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as _env) = (* All elements of the list are in scopes (scopt,subscopes) *) let (a,(scopt,subscopes)) = List.assoc x subst in let termin = - subst_aconstr_in_rawconstr loc interp subst (ids,None,scopes) - terminator in + subst_aconstr_in_rawconstr loc interp subst + (renaming,(ids,None,scopes)) terminator in let l = decode_constrlist_value a in List.fold_right (fun a t -> subst_iterator ldots_var t (subst_aconstr_in_rawconstr loc interp ((x,(a,(scopt,subscopes)))::subst) - (ids,None,scopes) iter)) + (renaming,(ids,None,scopes)) iter)) (if lassoc then List.rev l else l) termin with Not_found -> anomaly "Inconsistent substitution of recursive notation") | t -> rawconstr_of_aconstr_with_binders loc (traverse_binder subst) - (subst_aconstr_in_rawconstr loc interp subst) (ids,None,scopes) t + (subst_aconstr_in_rawconstr loc interp subst) + (renaming,(ids,None,scopes)) t let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args = let ntn,args = contract_notation ntn args in - let scopes = option_cons tmp_scope scopes in - let ((ids,c),df) = Notation.interp_notation loc ntn scopes in + let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in if !dump then dump_notation_location (ntn_loc loc args ntn) df; let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in - subst_aconstr_in_rawconstr loc intern subst env c + subst_aconstr_in_rawconstr loc intern subst ([],env) c let set_type_scope (ids,tmp_scope,scopes) = (ids,Some Notation.type_scope,scopes) @@ -844,8 +856,7 @@ let internalise sigma globalenv env allow_soapp lvar c = | CNotation (loc,ntn,args) -> intern_notation intern env loc ntn args | CPrim (loc, p) -> - let scopes = option_cons tmp_scope scopes in - let c,df = Notation.interp_prim_token loc p scopes in + let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in if !dump then dump_notation_location (fst (unloc loc)) df; c | CDelimiters (loc, key, e) -> @@ -913,8 +924,7 @@ let internalise sigma globalenv env allow_soapp lvar c = | CDynamic (loc,d) -> RDynamic (loc,d) - and intern_type (ids,_,scopes) = - intern (ids,Some Notation.type_scope,scopes) + and intern_type env = intern (set_type_scope env) and intern_local_binder ((ids,ts,sc as env),bl) = function | LocalRawAssum(nal,ty) -> @@ -961,29 +971,25 @@ let internalise sigma globalenv env allow_soapp lvar c = let tm' = intern env tm in let ids,typ = match t with | Some t -> - let tids = names_of_cases_indtype t in + let tids = ids_of_cases_indtype t in let tids = List.fold_right Idset.add tids Idset.empty in let t = intern_type (tids,None,scopes) t in - let (_,_,_,nal as indsign) = - match t with - | RRef (loc,IndRef ind) -> (loc,ind,0,[]) - | RApp (loc,RRef (_,IndRef ind),l) -> - let nparams, nrealargs = inductive_nargs globalenv ind in - let nindargs = nparams + nrealargs in - if List.length l <> nindargs then - error_wrong_numarg_inductive_loc loc globalenv ind nindargs; - let nal = List.map (function - | RHole _ -> Anonymous - | RVar (_,id) -> 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 - user_err_loc (loc,"", - str "The parameters of inductive type must be implicit"); - (loc,ind,nparams,realnal) - | _ -> error_bad_inductive_type (loc_of_rawconstr t) in - nal, Some indsign + let loc,ind,l = match t with + | RRef (loc,IndRef ind) -> (loc,ind,[]) + | RApp (loc,RRef (_,IndRef ind),l) -> (loc,ind,l) + | _ -> error_bad_inductive_type (loc_of_rawconstr t) in + let nparams, nrealargs = inductive_nargs globalenv ind in + let nindargs = nparams + nrealargs in + if List.length l <> nindargs then + error_wrong_numarg_inductive_loc loc globalenv ind nindargs; + let nal = List.map (function + | RHole loc -> Anonymous + | RVar (_,id) -> 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 + error_inductive_parameter_not_implicit loc; + realnal, Some (loc,ind,nparams,realnal) | None -> [], None in let na = match tm', na with @@ -1067,12 +1073,21 @@ let extract_ids env = let intern_gen isarity sigma env ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) c = - let tmp_scope = if isarity then Some Notation.type_scope else None in + let tmp_scope = + if isarity then Some Notation.type_scope else None in internalise sigma env (extract_ids env, tmp_scope,[]) allow_soapp (ltacvars,Environ.named_context env, [], impls) c let intern_constr sigma env c = intern_gen false sigma env c +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) + + let intern_ltac isarity ltacvars sigma env c = intern_gen isarity sigma env ~ltacvars:ltacvars c @@ -1100,6 +1115,21 @@ let interp_open_constr sigma env c = let interp_constr_judgment sigma env c = Default.understand_judgment sigma env (intern_constr sigma env c) + +let interp_constr_evars_gen isevars env ?(impls=([],[])) kind c = + Default.understand_tcc_evars isevars env kind + (intern_gen (kind=IsType) ~impls (Evd.evars_of !isevars) env c) + +let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ = + interp_constr_evars_gen isevars env ~impls (OfType (Some typ)) c + +let interp_type_evars isevars env ?(impls=([],[])) c = + interp_constr_evars_gen isevars env IsType ~impls c + +let interp_constr_judgment_evars isevars env c = + Default.understand_judgment_tcc isevars env + (intern_constr (Evd.evars_of !isevars) env c) + type ltac_sign = identifier list * unbound_ltac_var_map let interp_constrpattern sigma env c = @@ -1123,7 +1153,13 @@ let interp_aconstr impls vars a = let interp_binder sigma env na t = let t = intern_gen true sigma env t in - Default.understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t) + let t' = locate_if_isevar (loc_of_rawconstr t) na t in + Default.understand_type sigma env t' + +let interp_binder_evars isevars env na t = + let t = intern_gen true (Evd.evars_of !isevars) env t in + let t' = locate_if_isevar (loc_of_rawconstr t) na t in + Default.understand_tcc_evars isevars env IsType t' open Environ open Term @@ -1146,6 +1182,24 @@ let interp_context sigma env params = (push_rel d env,d::params)) (env,[]) params +let interp_context_evars isevars env params = + List.fold_left + (fun (env,params) d -> match d with + | LocalRawAssum ([_,na],(CHole _ as t)) -> + let t = interp_binder_evars isevars env na t in + let d = (na,None,t) in + (push_rel d env, d::params) + | LocalRawAssum (nal,t) -> + let t = interp_type_evars isevars env t in + let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in + let ctx = List.rev ctx in + (push_rel_context ctx env, ctx@params) + | LocalRawDef ((_,na),c) -> + let c = interp_constr_judgment_evars isevars env c in + let d = (na, Some c.uj_val, c.uj_type) in + (push_rel d env,d::params)) + (env,[]) params + (**********************************************************************) (* Locating reference, possibly via an abbreviation *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index cdd87a7c..d88a058d 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: constrintern.mli 7732 2005-12-26 13:51:24Z herbelin $ i*) +(*i $Id: constrintern.mli 9154 2006-09-20 17:18:18Z corbinea $ i*) (*i*) open Names @@ -55,6 +55,14 @@ val intern_gen : bool -> evar_map -> env -> ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign -> constr_expr -> rawconstr +val intern_pattern : env -> cases_pattern_expr -> + Names.identifier list * + ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list + +val intern_pattern : env -> cases_pattern_expr -> + Names.identifier list * + ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list + (*s Composing internalisation with pretyping *) (* Main interpretation function *) @@ -76,6 +84,12 @@ val interp_type : evar_map -> env -> ?impls:full_implicits_env -> val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr +val interp_casted_constr_evars : evar_defs ref -> env -> + ?impls:full_implicits_env -> constr_expr -> types -> constr + +val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env -> + constr_expr -> types + (*s Build a judgment *) val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment @@ -95,6 +109,9 @@ val interp_binder : evar_map -> env -> name -> constr_expr -> types val interp_context : evar_map -> env -> local_binder list -> env * rel_context +val interp_context_evars : + evar_defs ref -> env -> local_binder list -> env * rel_context + (* Locating references of constructions, possibly via a syntactic definition *) val locate_reference : qualid -> global_reference diff --git a/interp/notation.ml b/interp/notation.ml index 7e101784..5b6692e9 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: notation.ml 8752 2006-04-27 19:37:33Z herbelin $ *) +(* $Id: notation.ml 9258 2006-10-23 07:15:04Z courtieu $ *) (*i*) open Util @@ -130,6 +130,11 @@ let push_scope sc scopes = Scope sc :: scopes let push_scopes = List.fold_right push_scope +type local_scopes = tmp_scope_name option * scope_name list + +let make_current_scopes (tmp_scope,scopes) = + option_fold_right push_scope tmp_scope (push_scopes scopes !scope_stack) + (**********************************************************************) (* Delimiters *) @@ -146,7 +151,7 @@ let declare_delimiters scope key = scope_map := Gmap.add scope sc !scope_map; if Gmap.mem key !delimiters_map then begin let oldsc = Gmap.find key !delimiters_map in - Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc) + Options.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc) end; delimiters_map := Gmap.add key scope !delimiters_map @@ -295,8 +300,8 @@ let declare_notation_interpretation ntn scopt pat df = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in if Gmap.mem ntn sc.notations && Options.is_verbose () then - warning ("Notation "^ntn^" was already used"^ - (if scopt = None then "" else " in scope "^scope)); + msg_warning (str ("Notation "^ntn^" was already used"^ + (if scopt = None then "" else " in scope "^scope))); let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in scope_map := Gmap.add scope sc !scope_map; if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack @@ -336,9 +341,9 @@ let find_prim_token g loc p sc = check_required_module loc sc spdir; g (interp ()), (dirpath (fst spdir),"") -let interp_prim_token_gen g loc p scopes = - let all_scopes = push_scopes scopes !scope_stack in - try find_interpretation (find_prim_token g loc p) all_scopes +let interp_prim_token_gen g loc p local_scopes = + let scopes = make_current_scopes local_scopes in + try find_interpretation (find_prim_token g loc p) scopes with Not_found -> user_err_loc (loc,"interp_prim_token", (match p with @@ -351,8 +356,9 @@ let interp_prim_token = let interp_prim_token_cases_pattern loc p name = interp_prim_token_gen (cases_pattern_of_rawconstr name) loc p -let rec interp_notation loc ntn scopes = - try find_interpretation (find_notation ntn) (push_scopes scopes !scope_stack) +let rec interp_notation loc ntn local_scopes = + let scopes = make_current_scopes local_scopes in + try find_interpretation (find_notation ntn) scopes with Not_found -> user_err_loc (loc,"",str ("Unknown interpretation for notation \""^ntn^"\"")) @@ -366,7 +372,7 @@ let uninterp_cases_pattern_notations c = let availability_of_notation (ntn_scope,ntn) scopes = let f scope = Gmap.mem ntn (Gmap.find scope !scope_map).notations in - find_without_delimiters f (ntn_scope,Some ntn) scopes + find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes) let uninterp_prim_token c = try @@ -387,8 +393,9 @@ let uninterp_prim_token_cases_pattern c = | Some n -> (na,sc,n) with Not_found -> raise No_match -let availability_of_prim_token printer_scope scopes = +let availability_of_prim_token printer_scope local_scopes = let f scope = Hashtbl.mem prim_token_interpreter_tab scope in + let scopes = make_current_scopes local_scopes in option_map snd (find_without_delimiters f (Some printer_scope,None) scopes) (* Miscellaneous *) @@ -494,7 +501,7 @@ let make_notation_key symbols = let decompose_notation_key s = let len = String.length s in let rec decomp_ntn dirs n = - if n>=len then dirs else + if n>=len then List.rev dirs else let pos = try String.index_from s n ' ' diff --git a/interp/notation.mli b/interp/notation.mli index 32ec7a96..840274c5 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: notation.mli 7984 2006-02-04 20:14:55Z herbelin $ i*) +(*i $Id: notation.mli 9208 2006-10-05 07:45:01Z herbelin $ i*) (*i*) open Util @@ -32,12 +32,15 @@ type delimiters = string type scope type scopes (* = [scope_name list] *) +type local_scopes = tmp_scope_name option * scope_name list + val type_scope : scope_name val declare_scope : scope_name -> unit +val current_scopes : unit -> scopes + (* Open scope *) -val current_scopes : unit -> scopes val open_close_scope : (* locality *) bool * (* open *) bool * scope_name -> unit @@ -76,10 +79,10 @@ val declare_string_interpreter : scope_name -> required_module -> (* Return the [term]/[cases_pattern] bound to a primitive token in a given scope context*) -val interp_prim_token : loc -> prim_token -> scope_name list -> +val interp_prim_token : loc -> prim_token -> local_scopes -> rawconstr * (notation_location * scope_name option) val interp_prim_token_cases_pattern : loc -> prim_token -> name -> - scope_name list -> cases_pattern * (notation_location * scope_name option) + local_scopes -> cases_pattern * (notation_location * scope_name option) (* Return the primitive token associated to a [term]/[cases_pattern]; raise [No_match] if no such token *) @@ -90,7 +93,7 @@ val uninterp_prim_token_cases_pattern : cases_pattern -> name * scope_name * prim_token val availability_of_prim_token : - scope_name -> scopes -> delimiters option option + scope_name -> local_scopes -> delimiters option option (*s Declare and interpret back and forth a notation *) @@ -105,7 +108,7 @@ val declare_notation_interpretation : notation -> scope_name option -> val declare_uninterpretation : interp_rule -> interpretation -> unit (* Return the interpretation bound to a notation *) -val interp_notation : loc -> notation -> scope_name list -> +val interp_notation : loc -> notation -> local_scopes -> interpretation * (notation_location * scope_name option) (* Return the possible notations for a given term *) @@ -117,7 +120,7 @@ val uninterp_cases_pattern_notations : cases_pattern -> (* Test if a notation is available in the scopes *) (* context [scopes]; if available, the result is not None; the first *) (* argument is itself not None if a delimiters is needed *) -val availability_of_notation : scope_name option * notation -> scopes -> +val availability_of_notation : scope_name option * notation -> local_scopes -> (scope_name option * delimiters option) option (*s Declare and test the level of a (possibly uninterpreted) notation *) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index f3099346..936b6830 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: topconstr.ml 9032 2006-07-07 16:30:34Z herbelin $ *) +(* $Id: topconstr.ml 9226 2006-10-09 16:11:01Z herbelin $ *) (*i*) open Pp @@ -39,17 +39,24 @@ type aconstr = | ALetIn of name * aconstr * aconstr | ACases of aconstr option * (aconstr * (name * (inductive * int * name list) option)) list * - (identifier list * cases_pattern list * aconstr) list + (cases_pattern list * aconstr) list | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr | AIf of aconstr * (name * aconstr option) * aconstr * aconstr | ASort of rawsort | AHole of Evd.hole_kind | APatVar of patvar | ACast of aconstr * cast_type * aconstr - -let name_app f e = function - | Name id -> let (id, e) = f id e in (e, Name id) - | Anonymous -> e,Anonymous + +(**********************************************************************) +(* Re-interpret a notation as a rawconstr, taking care of binders *) + +let rec cases_pattern_fold_map loc g e = function + | PatVar (_,na) -> + let e',na' = name_fold_map g e na in e', PatVar (loc,na') + | PatCstr (_,cstr,patl,na) -> + let e',na' = name_fold_map g e na in + let e',patl' = list_fold_map (cases_pattern_fold_map loc g) e patl in + e', PatCstr (loc,cstr,patl',na') let rec subst_rawvars l = function | RVar (_,id) as r -> (try List.assoc id l with Not_found -> r) @@ -67,32 +74,33 @@ let rawconstr_of_aconstr_with_binders loc g f e = function let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in subst_rawvars outerl it | ALambda (na,ty,c) -> - let e,na = name_app g e na in RLambda (loc,na,f e ty,f e c) + let e,na = name_fold_map g e na in RLambda (loc,na,f e ty,f e c) | AProd (na,ty,c) -> - let e,na = name_app g e na in RProd (loc,na,f e ty,f e c) + let e,na = name_fold_map g e na in RProd (loc,na,f e ty,f e c) | ALetIn (na,b,c) -> - let e,na = name_app g e na in RLetIn (loc,na,f e b,f e c) + let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c) | ACases (rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with | None -> e',None | Some (ind,npar,nal) -> let e',nal' = List.fold_right (fun na (e',nal) -> - let e',na' = name_app g e' na in e',na'::nal) nal (e',[]) in + let e',na' = name_fold_map g e' na in e',na'::nal) nal (e',[]) in e',Some (loc,ind,npar,nal') in - let e',na' = name_app g e' na in + let e',na' = name_fold_map g e' na in (e',(f e tm,(na',t'))::tml')) tml (e,[]) in - let fold id (idl,e) = let (id,e) = g id e in (id::idl,e) in - let eqnl' = List.map (fun (idl,pat,rhs) -> - let (idl,e) = List.fold_right fold idl ([],e) in - (loc,idl,pat,f e rhs)) eqnl in + let fold (idl,e) id = let (e,id) = g e id in ((id::idl,e),id) in + let eqnl' = List.map (fun (patl,rhs) -> + let ((idl,e),patl) = + list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in + (loc,idl,patl,f e rhs)) eqnl in RCases (loc,option_map (f e') rtntypopt,tml',eqnl') | ALetTuple (nal,(na,po),b,c) -> - let e,nal = list_fold_map (name_app g) e nal in - let e,na = name_app g e na in + let e,nal = list_fold_map (name_fold_map g) e nal in + let e,na = name_fold_map g e na in RLetTuple (loc,nal,(na,option_map (f e) po),f e b,f e c) | AIf (c,(na,po),b1,b2) -> - let e,na = name_app g e na in + let e,na = name_fold_map g e na in RIf (loc,f e c,(na,option_map (f e) po),f e b1,f e b2) | ACast (c,k,t) -> RCast (loc,f e c, k,f e t) | ASort x -> RSort (loc,x) @@ -102,17 +110,11 @@ let rawconstr_of_aconstr_with_binders loc g f e = function let rec rawconstr_of_aconstr loc x = let rec aux () x = - rawconstr_of_aconstr_with_binders loc (fun id () -> (id,())) aux () x + rawconstr_of_aconstr_with_binders loc (fun () id -> ((),id)) aux () x in aux () x -let rec subst_pat subst pat = - match pat with - | PatVar _ -> pat - | PatCstr (loc,((kn,i),j),cpl,n) -> - let kn' = subst_kn subst kn - and cpl' = list_smartmap (subst_pat subst) cpl in - if kn' == kn && cpl' == cpl then pat else - PatCstr (loc,((kn',i),j),cpl',n) +(****************************************************************************) +(* Translating a rawconstr into a notation, interpreting recursive patterns *) let add_name r = function | Anonymous -> () @@ -179,9 +181,7 @@ let aconstr_and_vars_of_rawconstr a = | RProd (_,na,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 (_,rtntypopt,tml,eqnl) -> - let f (_,idl,pat,rhs) = - found := idl@(!found); - (idl,pat,aux rhs) in + let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in ACases (option_map aux rtntypopt, List.map (fun (tm,(na,x)) -> add_name found na; @@ -246,9 +246,20 @@ let aconstr_of_rawconstr vars a = List.iter check_type vars; 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) +let rec subst_pat subst pat = + match pat with + | PatVar _ -> pat + | PatCstr (loc,((kn,i),j),cpl,n) -> + let kn' = subst_kn subst kn + and cpl' = list_smartmap (subst_pat subst) cpl in + if kn' == kn && cpl' == cpl then pat else + PatCstr (loc,((kn',i),j),cpl',n) + let rec subst_aconstr subst bound raw = match raw with | ARef ref -> @@ -265,22 +276,26 @@ let rec subst_aconstr subst bound raw = AApp(r',rl') | AList (id1,id2,r1,r2,b) -> - let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in + let r1' = subst_aconstr subst bound r1 + and r2' = subst_aconstr subst bound r2 in if r1' == r1 && r2' == r2 then raw else AList (id1,id2,r1',r2',b) | ALambda (n,r1,r2) -> - let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in + let r1' = subst_aconstr subst bound r1 + and r2' = subst_aconstr subst bound r2 in if r1' == r1 && r2' == r2 then raw else ALambda (n,r1',r2') | AProd (n,r1,r2) -> - let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in + let r1' = subst_aconstr subst bound r1 + and r2' = subst_aconstr subst bound r2 in if r1' == r1 && r2' == r2 then raw else AProd (n,r1',r2') | ALetIn (n,r1,r2) -> - let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in + let r1' = subst_aconstr subst bound r1 + and r2' = subst_aconstr subst bound r2 in if r1' == r1 && r2' == r2 then raw else ALetIn (n,r1',r2') @@ -295,11 +310,11 @@ let rec subst_aconstr subst bound raw = if a' == a && signopt' == signopt then x else (a',(n,signopt'))) rl and branches' = list_smartmap - (fun (idl,cpl,r as branch) -> + (fun (cpl,r as branch) -> let cpl' = list_smartmap (subst_pat subst) cpl and r' = subst_aconstr subst bound r in if cpl' == cpl && r' == r then branch else - (idl,cpl',r')) + (cpl',r')) branches in if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' & @@ -331,7 +346,8 @@ let rec subst_aconstr subst bound raw = Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw | ACast (r1,k,r2) -> - let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in + let r1' = subst_aconstr subst bound r1 + and r2' = subst_aconstr subst bound r2 in if r1' == r1 && r2' == r2 then raw else ACast (r1',k,r2') @@ -394,6 +410,15 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match +let rec match_cases_pattern metas acc pat1 pat2 = + match (pat1,pat2) with + | PatVar (_,na1), PatVar (_,na2) -> match_names metas acc na1 na2 + | PatCstr (_,c1,patl1,na1), PatCstr (_,c2,patl2,na2) + when c1 = c2 & List.length patl1 = List.length patl2 -> + List.fold_left2 (match_cases_pattern metas) + (match_names metas acc na1 na2) patl1 patl2 + | _ -> raise No_match + 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 | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma @@ -411,7 +436,8 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with | RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) -> match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2 | RCases (_,rtno1,tml1,eqnl1), ACases (rtno2,tml2,eqnl2) - when List.length tml1 = List.length tml2 -> + when List.length tml1 = List.length tml2 + & List.length eqnl1 = List.length eqnl2 -> let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in let sigma = option_fold_left2 (match_ alp metas) sigma rtno1' rtno2' in @@ -461,15 +487,19 @@ and match_binders alp metas na1 na2 sigma b1 b2 = let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in match_ alp metas sigma b1 b2 -and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) = - if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then - match_ alp metas sigma rhs1 rhs2 - else raise No_match +and match_equations alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) = + (* patl1 and patl2 have the same length because they respectively + correspond to some tml1 and tml2 that have the same length *) + let (alp,sigma) = + List.fold_left2 (match_cases_pattern metas) (alp,sigma) patl1 patl2 in + match_ alp metas sigma rhs1 rhs2 type scope_name = string +type tmp_scope_name = scope_name + type interpretation = - (identifier * (scope_name option * scope_name list)) list * aconstr + (identifier * (tmp_scope_name option * scope_name list)) list * aconstr let match_aconstr c (metas_scl,pat) = let subst = match_ [] (List.map fst metas_scl) [] c pat in @@ -592,7 +622,7 @@ let constr_loc = function | CDelimiters (loc,_,_) -> loc | CDynamic _ -> dummy_loc -let cases_pattern_loc = function +let cases_pattern_expr_loc = function | CPatAlias (loc,_,_) -> loc | CPatCstr (loc,_,_) -> loc | CPatAtom (loc,_) -> loc @@ -605,35 +635,98 @@ let occur_var_constr_ref id = function | Ident (loc,id') -> id = id' | Qualid _ -> false -let rec occur_var_constr_expr id = function - | CRef r -> occur_var_constr_ref id r - | CArrow (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b - | CAppExpl (loc,(_,r),l) -> - occur_var_constr_ref id r or List.exists (occur_var_constr_expr id) l - | CApp (loc,(_,f),l) -> - occur_var_constr_expr id f or - List.exists (fun (a,_) -> occur_var_constr_expr id a) l - | CProdN (_,l,b) -> occur_var_binders id b l - | CLambdaN (_,l,b) -> occur_var_binders id b l - | CLetIn (_,na,a,b) -> occur_var_binders id b [[na],a] - | CCast (loc,a,_,b) -> - occur_var_constr_expr id a or occur_var_constr_expr id b - | CNotation (_,_,l) -> List.exists (occur_var_constr_expr id) l - | CDelimiters (loc,_,a) -> occur_var_constr_expr id a - | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ -> false - | CCases (loc,_,_,_) - | CLetTuple (loc,_,_,_,_) - | CIf (loc,_,_,_,_) - | CFix (loc,_,_) +let ids_of_cases_indtype = + let add_var ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in + 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) + (* assume the ntn is applicative and does not instantiate the head !! *) + | CAppExpl (_,_,l) -> List.fold_left add_var [] l + | CDelimiters(_,_,c) -> vars_of c + | _ -> [] in + vars_of + +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)) + tms [] + +let is_constructor id = + try ignore (Nametab.extended_locate (make_short_qualid id)); true + with Not_found -> true + +let rec cases_pattern_fold_names f a = function + | CPatAlias (_,pat,id) -> f id a + | CPatCstr (_,_,patl) | CPatOr (_,patl) | CPatNotation (_,_,patl) -> + List.fold_left (cases_pattern_fold_names f) a patl + | CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat + | CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a + | CPatPrim _ | CPatAtom _ -> a + +let ids_of_pattern_list = + List.fold_left (List.fold_left (cases_pattern_fold_names Idset.add)) + Idset.empty + +let rec fold_constr_expr_binders g f n acc b = function + | (nal,t)::l -> + let nal = snd (List.split nal) in + let n' = List.fold_right (name_fold g) nal n in + f n (fold_constr_expr_binders g f n' acc b l) t + | [] -> + f n acc b + +let rec fold_local_binders g f n acc b = function + | LocalRawAssum (nal,t)::l -> + let nal = snd (List.split nal) in + let n' = List.fold_right (name_fold g) nal n in + 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 + | CArrow (loc,a,b) -> f n (f n acc a) b + | CAppExpl (loc,(_,_),l) -> List.fold_left (f n) acc l + | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) + | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l + | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],a] + | CCast (loc,a,_,b) -> f n (f n acc a) b + | CNotation (_,_,l) -> List.fold_left (f n) acc l + | CDelimiters (loc,_,a) -> f n acc a + | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ -> + acc + | CCases (loc,rtnpo,al,bl) -> + let ids = ids_of_cases_tomatch al in + let acc = option_fold_left (f (List.fold_right g ids n)) acc rtnpo in + let acc = List.fold_left (f n) acc (List.map fst al) in + List.fold_right (fun (loc,patl,rhs) acc -> + 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 + | 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 + | CFix (loc,_,l) -> + let n' = List.fold_right (fun (id,_,_,_,_) -> g id) l n in + List.fold_right (fun (_,(_,o),lb,t,c) acc -> + fold_local_binders g f n' + (fold_local_binders g f n acc t lb) c lb) l acc | CCoFix (loc,_,_) -> - Pp.warning "Capture check in multiple binders not done"; false + Pp.warning "Capture check in multiple binders not done"; acc + +let free_vars_of_constr_expr c = + let rec aux bdvars l = function + | CRef (Ident (_,id)) -> if List.mem id bdvars then l else Idset.add id l + | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c + in aux [] Idset.empty c -and occur_var_binders id b = function - | (idl,a)::l -> - occur_var_constr_expr id a or - (not (List.mem (Name id) (snd (List.split idl))) - & occur_var_binders id b l) - | [] -> occur_var_constr_expr id b +let occur_var_constr_expr id c = Idset.mem id (free_vars_of_constr_expr c) let mkIdentC id = CRef (Ident (dummy_loc, id)) let mkRefC r = CRef r @@ -665,19 +758,6 @@ let coerce_to_id = function (* Used in correctness and interface *) - -let names_of_cases_indtype = - let add_var ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in - 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) - (* assume the ntn is applicative and does not instantiate the head !! *) - | CAppExpl (_,_,l) -> List.fold_left add_var [] l - | CDelimiters(_,_,c) -> vars_of c - | _ -> [] in - vars_of - let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e let map_binders f g e bl = @@ -696,7 +776,7 @@ let map_local_binders f g e bl = let (e,rbl) = List.fold_left h (e,[]) bl in (e, List.rev rbl) -let map_constr_expr_with_binders f g e = function +let map_constr_expr_with_binders g f e = function | CArrow (loc,a,b) -> CArrow (loc,f e a,f e b) | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l) | CApp (loc,(p,a),l) -> @@ -714,18 +794,9 @@ let map_constr_expr_with_binders f g e = function | CCases (loc,rtnpo,a,bl) -> (* TODO: apply g on the binding variables in pat... *) let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in - let e' = - List.fold_right - (fun (tm,(na,indnal)) e -> - option_fold_right - (fun t -> - let ids = names_of_cases_indtype t in - List.fold_right g ids) - indnal (option_fold_right (name_fold g) na e)) - a e - in - CCases (loc,option_map (f e') rtnpo, - List.map (fun (tm,x) -> (f e tm,x)) a,bl) + let ids = ids_of_cases_tomatch a in + let po = option_map (f (List.fold_right g ids e)) rtnpo in + CCases (loc, 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 @@ -753,8 +824,8 @@ let map_constr_expr_with_binders f g e = function let rec replace_vars_constr_expr l = function | CRef (Ident (loc,id)) as x -> (try CRef (Ident (loc,List.assoc id l)) with Not_found -> x) - | c -> map_constr_expr_with_binders replace_vars_constr_expr - (fun id l -> List.remove_assoc id l) l c + | c -> map_constr_expr_with_binders List.remove_assoc + replace_vars_constr_expr l c (**********************************************************************) (* Concrete syntax for modules and modules types *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 51853089..131e4170 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: topconstr.mli 9032 2006-07-07 16:30:34Z herbelin $ i*) +(*i $Id: topconstr.mli 9226 2006-10-09 16:11:01Z herbelin $ i*) (*i*) open Pp @@ -35,7 +35,7 @@ type aconstr = | ALetIn of name * aconstr * aconstr | ACases of aconstr option * (aconstr * (name * (inductive * int * name list) option)) list * - (identifier list * cases_pattern list * aconstr) list + (cases_pattern list * aconstr) list | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr | AIf of aconstr * (name * aconstr option) * aconstr * aconstr | ASort of rawsort @@ -43,30 +43,50 @@ type aconstr = | APatVar of patvar | ACast of aconstr * cast_type * 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 + +(* Name of the special identifier used to encode recursive notations *) +val ldots_var : identifier + +(* Equality of rawconstr (warning: only partially implemented) *) +val eq_rawconstr : rawconstr -> rawconstr -> bool + +(**********************************************************************) +(* Re-interpret a notation as a rawconstr, taking care of binders *) + val rawconstr_of_aconstr_with_binders : loc -> - (identifier -> 'a -> identifier * 'a) -> + ('a -> identifier -> 'a * identifier) -> ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr val rawconstr_of_aconstr : loc -> aconstr -> rawconstr -val subst_aconstr : substitution -> Names.identifier list -> aconstr -> aconstr +(**********************************************************************) +(* Substitution of kernel names, avoiding a list of bound identifiers *) -val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr +val subst_aconstr : substitution -> identifier list -> aconstr -> aconstr -val eq_rawconstr : rawconstr -> rawconstr -> bool +(**********************************************************************) +(* [match_aconstr metas] matches a rawconstr against an aconstr with *) +(* metavariables in [metas]; raise [No_match] if the matching fails *) -(* [match_aconstr metas] match a rawconstr against an aconstr with - metavariables in [metas]; it raises [No_match] if the matching fails *) exception No_match type scope_name = string + +type tmp_scope_name = scope_name + type interpretation = - (identifier * (scope_name option * scope_name list)) list * aconstr + (identifier * (tmp_scope_name option * scope_name list)) list * aconstr val match_aconstr : rawconstr -> interpretation -> - (rawconstr * (scope_name option * scope_name list)) list + (rawconstr * (tmp_scope_name option * scope_name list)) list -(*s Concrete syntax for terms *) +(**********************************************************************) +(*s Concrete syntax for terms *) type notation = string @@ -128,18 +148,21 @@ and local_binder = | LocalRawDef of name located * constr_expr | LocalRawAssum of name located list * constr_expr +(**********************************************************************) +(* Utilities on constr_expr *) val constr_loc : constr_expr -> loc -val cases_pattern_loc : cases_pattern_expr -> loc +val cases_pattern_expr_loc : cases_pattern_expr -> loc val replace_vars_constr_expr : (identifier * identifier) list -> constr_expr -> constr_expr +val free_vars_of_constr_expr : constr_expr -> Idset.t val occur_var_constr_expr : identifier -> constr_expr -> bool (* Specific function for interning "in indtype" syntax of "match" *) -val names_of_cases_indtype : constr_expr -> identifier list +val ids_of_cases_indtype : constr_expr -> identifier list val mkIdentC : identifier -> constr_expr val mkRefC : reference -> constr_expr @@ -172,10 +195,11 @@ val names_of_local_binders : local_binder list -> name located list (* in pattern-matching clauses and in binders of the form [x,y:T(x)] *) val map_constr_expr_with_binders : - ('a -> constr_expr -> constr_expr) -> - (identifier -> 'a -> 'a) -> 'a -> constr_expr -> constr_expr + (identifier -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) -> + 'a -> constr_expr -> constr_expr -(* Concrete syntax for modules and modules types *) +(**********************************************************************) +(* Concrete syntax for modules and module types *) type with_declaration_ast = | CWith_Module of identifier list located * qualid located @@ -188,6 +212,3 @@ type module_type_ast = type module_ast = | CMEident of qualid located | CMEapply of module_ast * module_ast - -(* Special identifier to encode recursive notations *) -val ldots_var : identifier -- cgit v1.2.3