diff options
81 files changed, 640 insertions, 683 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 62b8cdcea..299ea8d79 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -21,6 +21,8 @@ open Sign open Environ open Libnames open Impargs +open Constrexpr +open Notation_term open Topconstr open Glob_term open Glob_ops @@ -456,7 +458,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function match t with | PatCstr (loc,_,_,na) -> let p = apply_notation_to_pattern loc - (match_aconstr_cases_pattern t pat) allscopes vars keyrule in + (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias loc p na | PatVar (loc,Anonymous) -> CPatAtom (loc, None) | PatVar (loc,Name id) -> CPatAtom (loc, Some (Ident (loc,id))) @@ -910,7 +912,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | _ -> raise No_match in (* Try matching ... *) let terms,termlists,binders = - match_aconstr !print_universes t pat in + match_notation_constr !print_universes t pat in (* Try availability of interpretation ... *) let e = match keyrule with diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 21c33f3f3..38f8b6579 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -16,7 +16,8 @@ open Libnames open Nametab open Glob_term open Pattern -open Topconstr +open Constrexpr +open Notation_term open Notation open Misctypes diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d125caf54..91e0cf6a1 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -20,6 +20,8 @@ open Glob_ops open Pattern open Pretyping open Cases +open Constrexpr +open Notation_term open Topconstr open Nametab open Notation @@ -254,8 +256,8 @@ let contract_pat_notation ntn (l,ll) = type intern_env = { ids: Names.Idset.t; unb: bool; - tmp_scope: Topconstr.tmp_scope_name option; - scopes: Topconstr.scope_name list; + tmp_scope: Notation_term.tmp_scope_name option; + scopes: Notation_term.scope_name list; impls: internalization_env } (**********************************************************************) @@ -363,7 +365,8 @@ let rec check_capture ty = function let locate_if_isevar loc na = function | GHole _ -> (try match na with - | Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id) + | Name id -> glob_constr_of_notation_constr loc + (Reserve.find_reserved_type id) | Anonymous -> raise Not_found with Not_found -> GHole (loc, Evar_kinds.BinderType na)) | x -> x @@ -530,7 +533,7 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c = let rec aux (terms,binderopt as subst') (renaming,env) c = let subinfos = renaming,{env with tmp_scope = None} in match c with - | AVar id -> + | NVar id -> begin (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) @@ -545,7 +548,7 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c = (* Happens for local notation joint with inductive/fixpoint defs *) GVar (loc,id) end - | AList (x,_,iter,terminator,lassoc) -> + | NList (x,_,iter,terminator,lassoc) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) let (l,(scopt,subscopes)) = List.assoc x termlists in @@ -556,12 +559,12 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c = (if lassoc then List.rev l else l) termin with Not_found -> anomaly "Inconsistent substitution of recursive notation") - | AHole (Evar_kinds.BinderType (Name id as na)) -> + | NHole (Evar_kinds.BinderType (Name id as na)) -> let na = try snd (coerce_to_name (fst (List.assoc id terms))) with Not_found -> na in GHole (loc,Evar_kinds.BinderType na) - | ABinderList (x,_,iter,terminator) -> + | NBinderList (x,_,iter,terminator) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) let (bl,(scopt,subscopes)) = List.assoc x binders in @@ -575,15 +578,15 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c = make_letins letins res with Not_found -> anomaly "Inconsistent substitution of recursive notation") - | AProd (Name id, AHole _, c') when option_mem_assoc id binderopt -> + | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt -> let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in GProd (loc,na,bk,t,make_letins letins (aux subst' infos c')) - | ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt -> + | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt -> let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in GLambda (loc,na,bk,t,make_letins letins (aux subst' infos c')) | t -> - glob_constr_of_aconstr_with_binders loc (traverse_binder subst) - (aux subst') subinfos t + glob_constr_of_notation_constr_with_binders loc + (traverse_binder subst) (aux subst') subinfos t in aux (terms,None) infos c let split_by_type ids = @@ -887,7 +890,7 @@ let chop_params_pattern loc ind args with_letin = let subst_cases_pattern loc alias intern fullsubst env a = let rec aux alias (subst,substlist as fullsubst) = function - | AVar id -> + | NVar id -> begin (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) @@ -905,15 +908,15 @@ let subst_cases_pattern loc alias intern fullsubst env a = [[id],[]], PatVar (loc,Name id) *) end - | ARef (ConstructRef c) -> + | NRef (ConstructRef c) -> ([],[[], PatCstr (loc,c, [], alias)]) - | AApp (ARef (ConstructRef cstr),args) -> + | NApp (NRef (ConstructRef cstr),args) -> let idslpll = List.map (aux Anonymous fullsubst) args in let ids',pll = product_of_cases_patterns [] idslpll in let pl' = List.map (fun (asubst,pl) -> asubst,PatCstr (loc,cstr,chop_params_pattern loc (fst cstr) pl false,alias)) pll in ids', pl' - | AList (x,_,iter,terminator,lassoc) -> + | NList (x,_,iter,terminator,lassoc) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) let (l,(scopt,subscopes)) = List.assoc x substlist in @@ -928,12 +931,12 @@ let subst_cases_pattern loc alias intern fullsubst env a = match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v with Not_found -> anomaly "Inconsistent substitution of recursive notation") - | AHole _ -> ([],[[], PatVar (loc,Anonymous)]) + | NHole _ -> ([],[[], PatVar (loc,Anonymous)]) | t -> error_invalid_pattern_notation loc in aux alias fullsubst a let subst_ind_pattern loc intern_ind_patt intern (subst,_ as fullsubst) env = function - | AVar id -> + | NVar id -> begin (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) @@ -944,9 +947,9 @@ let subst_ind_pattern loc intern_ind_patt intern (subst,_ as fullsubst) env = fu with Not_found -> anomaly ("Unbound pattern notation variable: "^(string_of_id id)) end - | ARef (IndRef c) -> + | NRef (IndRef c) -> false, (c, []) - | AApp (ARef (IndRef ind),args) -> + | NApp (NRef (IndRef ind),args) -> let idslpll = List.map (subst_cases_pattern loc Anonymous intern fullsubst env) args in begin match product_of_cases_patterns [] idslpll with @@ -973,11 +976,11 @@ let find_at_head looked_for add_params ref f pats env = | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with - | ARef g -> + | NRef g -> let cstr = looked_for g in assert (vars=[]); cstr,add_params cstr, pats - | AApp (ARef g,args) -> + | NApp (NRef g,args) -> let cstr = looked_for g in let nvars = List.length vars in if List.length pats < nvars then error_not_enough_arguments loc; @@ -1148,7 +1151,7 @@ let rec intern_cases_pattern genv env (ids,asubst as aliases) pat = in intern_pat env aliases self_patt | CPatCstr (loc, head, pl) -> - if !Topconstr.oldfashion_patterns then + if !oldfashion_patterns then let c,idslpl1,pl2 = mustbe_constructor loc (Some (List.length pl)) head intern_pat pl env in let with_letin = check_constructor_length genv loc c false idslpl1 pl2 in intern_cstr_with_all_args loc c with_letin idslpl1 pl2 @@ -1185,10 +1188,10 @@ let rec intern_cases_pattern genv env (ids,asubst as aliases) pat = intern_pat {env with scopes=find_delimiters_scope loc key::env.scopes; tmp_scope = None} aliases e | CPatAtom (loc, Some head) -> - (match maybe_constructor (if !Topconstr.oldfashion_patterns then Some 0 else None) + (match maybe_constructor (if !oldfashion_patterns then Some 0 else None) head intern_pat env with | ConstrPat (c,idspl) -> - if !Topconstr.oldfashion_patterns then + if !oldfashion_patterns then let with_letin = check_constructor_length genv loc c false idspl [] in intern_cstr_with_all_args loc c with_letin idspl [] else @@ -1463,7 +1466,7 @@ let internalize sigma globalenv env allow_patvar lvar c = (Option.fold_left (fun x (_,y) -> match y with | Name y' -> Idset.add y' x |_ -> x) acc na) inb) Idset.empty tms in (* as, in & return vars *) - let forbidden_vars = Option.cata Topconstr.free_vars_of_constr_expr as_in_vars rtnpo in + let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in let tms,ex_ids,match_from_in = List.fold_right (fun citm (inds,ex_ids,matchs) -> let ((tm,ind),extra_id,match_td) = intern_case_item env forbidden_vars citm in @@ -1782,7 +1785,7 @@ 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_glob_constr c -let interp_aconstr ?(impls=empty_internalization_env) vars recvars a = +let interp_notation_constr ?(impls=empty_internalization_env) 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,typ) -> (id,(ref None,typ))) vars in @@ -1790,7 +1793,7 @@ let interp_aconstr ?(impls=empty_internalization_env) vars recvars a = tmp_scope = None; scopes = []; impls = impls} false (([],[]),vl) a in (* Translate and check that [c] has all its free variables bound in [vars] *) - let a = aconstr_of_glob_constr vars recvars c in + let a = notation_constr_of_glob_constr 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 diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 250871b9e..10fbde605 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -14,7 +14,8 @@ open Environ open Libnames open Glob_term open Pattern -open Topconstr +open Constrexpr +open Notation_term open Termops open Pretyping open Misctypes @@ -52,7 +53,7 @@ type var_internalization_data = (** 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.implicit_status list * (** signature of impargs of the variable *) - scope_name option list (** subscopes of the args of the variable *) + Notation_term.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 = var_internalization_data Idmap.t @@ -175,10 +176,11 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr 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:internalization_env -> +val interp_notation_constr : ?impls:internalization_env -> (identifier * notation_var_internalization_type) list -> (identifier * identifier) list -> constr_expr -> - (identifier * (subscopes * notation_var_internalization_type)) list * aconstr + (identifier * (subscopes * notation_var_internalization_type)) list * + notation_constr (** Globalization options *) val parsing_explicit : bool ref diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 90b56e0a9..59a695ee6 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -34,10 +34,14 @@ val dump_moddef : Pp.loc -> Names.module_path -> string -> unit val dump_modref : Pp.loc -> Names.module_path -> string -> unit val dump_reference : Pp.loc -> string -> string -> string -> unit val dump_libref : Pp.loc -> Names.dir_path -> string -> unit -val dump_notation_location : (int * int) list -> Topconstr.notation -> (Notation.notation_location * Topconstr.scope_name option) -> unit +val dump_notation_location : (int * int) list -> Constrexpr.notation -> + (Notation.notation_location * Notation_term.scope_name option) -> unit val dump_binding : Pp.loc -> Names.Idset.elt -> unit -val dump_notation : Pp.loc * (Topconstr.notation * Notation.notation_location) -> Topconstr.scope_name option -> bool -> unit -val dump_constraint : Topconstr.typeclass_constraint -> bool -> string -> unit +val dump_notation : + Pp.loc * (Constrexpr.notation * Notation.notation_location) -> + Notation_term.scope_name option -> bool -> unit +val dump_constraint : + Constrexpr.typeclass_constraint -> bool -> string -> unit val dump_string : string -> unit diff --git a/interp/genarg.ml b/interp/genarg.ml index 3597879de..bbb4ae0a1 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -13,7 +13,7 @@ open Names open Nameops open Nametab open Glob_term -open Topconstr +open Constrexpr open Term open Evd open Misctypes diff --git a/interp/genarg.mli b/interp/genarg.mli index de1fa0fef..7466ae46f 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -14,7 +14,7 @@ open Libnames open Glob_term open Genredexpr open Pattern -open Topconstr +open Constrexpr open Term open Evd open Misctypes diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 3384d79a5..a39347d55 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -18,7 +18,7 @@ open Mod_subst open Errors open Util open Glob_term -open Topconstr +open Constrexpr open Libnames open Typeclasses open Typeclasses_errors @@ -111,8 +111,8 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l = 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) -> - 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 + Topconstr.fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c + | c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c in aux bound l c let ids_of_names l = @@ -246,7 +246,7 @@ let combine_params avoid fn applied needed = aux (t' :: ids) avoid' app need | (x,_) :: _, [] -> - user_err_loc (constr_loc x,"",str "Typeclass does not expect more arguments") + user_err_loc (Topconstr.constr_loc x,"",str "Typeclass does not expect more arguments") in aux [] avoid applied needed let combine_params_freevar = diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 14a1c630c..3d869a019 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -15,7 +15,7 @@ open Environ open Nametab open Mod_subst open Glob_term -open Topconstr +open Constrexpr open Pp open Libnames open Typeclasses @@ -46,9 +46,9 @@ val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> I val combine_params_freevar : Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) -> - Topconstr.constr_expr * Names.Idset.t + Constrexpr.constr_expr * Names.Idset.t val implicit_application : Idset.t -> ?allow_partial:bool -> (Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) -> - Topconstr.constr_expr * Names.Idset.t) -> + Constrexpr.constr_expr * Names.Idset.t) -> constr_expr -> constr_expr * Idset.t diff --git a/interp/modintern.ml b/interp/modintern.ml index 5dde644b5..18d3a9c1c 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -12,7 +12,7 @@ open Util open Names open Entries open Libnames -open Topconstr +open Constrexpr open Constrintern type module_internalization_error = diff --git a/interp/modintern.mli b/interp/modintern.mli index e808cd980..860f66790 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -12,7 +12,7 @@ open Entries open Pp open Libnames open Names -open Topconstr +open Constrexpr (** Module internalization errors *) diff --git a/interp/notation.ml b/interp/notation.ml index b6496f535..16fdef469 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -16,9 +16,10 @@ open Term open Nametab open Libnames open Summary +open Constrexpr +open Notation_term open Glob_term open Glob_ops -open Topconstr open Ppextend (*i*) @@ -202,12 +203,13 @@ let cases_pattern_key = function | PatCstr (_,ref,_,_) -> RefKey (canonical_gr (ConstructRef ref)) | _ -> Oth -let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *) - | AApp (ARef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) - | AList (_,_,AApp (ARef ref,args),_,_) - | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args) - | ARef ref -> RefKey(canonical_gr ref), None - | AApp (_,args) -> Oth, Some (List.length args) +let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) + | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) + | NList (_,_,NApp (NRef ref,args),_,_) + | NBinderList (_,_,NApp (NRef ref,args),_) -> + RefKey (canonical_gr ref), Some (List.length args) + | NRef ref -> RefKey(canonical_gr ref), None + | NApp (_,args) -> Oth, Some (List.length args) | _ -> Oth, None (**********************************************************************) @@ -321,7 +323,7 @@ let declare_notation_interpretation ntn scopt pat df = if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack let declare_uninterpretation rule (metas,c as pat) = - let (key,n) = aconstr_key c in + let (key,n) = notation_constr_key c in notations_key_table := Gmapl.add key (rule,pat,n) !notations_key_table let rec find_interpretation ntn find = function @@ -349,7 +351,7 @@ let find_prim_token g loc p sc = (* Try for a user-defined numerical notation *) try let (_,c),df = find_notation (notation_of_prim_token p) sc in - g (glob_constr_of_aconstr loc c),df + g (Topconstr.glob_constr_of_notation_constr loc c),df with Not_found -> (* Try for a primitive numerical notation *) let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in @@ -401,9 +403,9 @@ let uninterp_prim_token c = let (sc,numpr,_) = Hashtbl.find prim_token_key_table (glob_prim_constr_key c) in match numpr c with - | None -> raise No_match + | None -> raise Topconstr.No_match | Some n -> (sc,n) - with Not_found -> raise No_match + with Not_found -> raise Topconstr.No_match let uninterp_prim_token_ind_pattern ind args = let ref = IndRef ind in @@ -423,12 +425,12 @@ let uninterp_prim_token_cases_pattern c = try let k = cases_pattern_key c in let (sc,numpr,b) = Hashtbl.find prim_token_key_table k in - if not b then raise No_match; + if not b then raise Topconstr.No_match; let na,c = glob_constr_of_closed_cases_pattern c in match numpr c with - | None -> raise No_match + | None -> raise Topconstr.No_match | Some n -> (na,sc,n) - with Not_found -> raise No_match + with Not_found -> raise Topconstr.No_match let availability_of_prim_token n printer_scope local_scopes = let f scope = @@ -447,7 +449,7 @@ let exists_notation_in_scope scopt ntn r = r' = r with Not_found -> false -let isAVar_or_AHole = function AVar _ | AHole _ -> true | _ -> false +let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) (* Mapping classes to scopes *) @@ -651,7 +653,7 @@ let pr_scope_classes sc = let pr_notation_info prglob ntn c = str "\"" ++ str ntn ++ str "\" := " ++ - prglob (glob_constr_of_aconstr dummy_loc c) + prglob (Topconstr.glob_constr_of_notation_constr dummy_loc c) let pr_named_scope prglob scope sc = (if scope = default_scope then @@ -708,8 +710,8 @@ let browse_notation strict ntn map = let global_reference_of_notation test (ntn,(sc,c,_)) = match c with - | ARef ref when test ref -> Some (ntn,sc,ref) - | AApp (ARef ref, l) when List.for_all isAVar_or_AHole l & test ref -> + | NRef ref when test ref -> Some (ntn,sc,ref) + | NApp (NRef ref, l) when List.for_all isNVar_or_NHole l & test ref -> Some (ntn,sc,ref) | _ -> None diff --git a/interp/notation.mli b/interp/notation.mli index 6eaac73db..d38f3d6bf 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -13,8 +13,9 @@ open Bigint open Names open Nametab open Libnames +open Constrexpr open Glob_term -open Topconstr +open Notation_term open Ppextend (** Notations *) diff --git a/interp/reserve.ml b/interp/reserve.ml index c3cdd3f72..2cfd6f5ea 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -16,7 +16,7 @@ open Nameops open Summary open Libobject open Lib -open Topconstr +open Notation_term open Libnames type key = @@ -26,19 +26,19 @@ type key = let reserve_table = ref Idmap.empty let reserve_revtable = ref Gmapl.empty -let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *) - | AApp (ARef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) - | AList (_,_,AApp (ARef ref,args),_,_) - | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args) - | ARef ref -> RefKey(canonical_gr ref), None +let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) + | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) + | NList (_,_,NApp (NRef ref,args),_,_) + | NBinderList (_,_,NApp (NRef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args) + | NRef ref -> RefKey(canonical_gr ref), None | _ -> Oth, None let cache_reserved_type (_,(id,t)) = - let key = fst (aconstr_key t) in + let key = fst (notation_constr_key t) in reserve_table := Idmap.add id t !reserve_table; reserve_revtable := Gmapl.add key (t,id) !reserve_revtable -let in_reserved : identifier * aconstr -> obj = +let in_reserved : identifier * notation_constr -> obj = declare_object {(default_object "RESERVED-TYPE") with cache_function = cache_reserved_type } @@ -80,8 +80,8 @@ let revert_reserved_type t = let t = Detyping.detype false [] [] t in list_try_find (fun (pat,id) -> - try let _ = match_aconstr false t ([],pat) in Name id - with No_match -> failwith "") l + try let _ = Topconstr.match_notation_constr false t ([],pat) in Name id + with Topconstr.No_match -> failwith "") l with Not_found | Failure _ -> Anonymous let _ = Namegen.set_reserved_typed_name revert_reserved_type @@ -92,7 +92,8 @@ let anonymize_if_reserved na t = match na with | Name id as na -> (try if not !Flags.raw_print & - (try aconstr_of_glob_constr [] [] t = find_reserved_type id + (try Topconstr.notation_constr_of_glob_constr [] [] t + = find_reserved_type id with UserError _ -> false) then GHole (dummy_loc,Evar_kinds.BinderType na) else t diff --git a/interp/reserve.mli b/interp/reserve.mli index f3b9d43a5..d52460b08 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -9,8 +9,8 @@ open Pp open Names open Glob_term -open Topconstr +open Notation_term -val declare_reserved_type : identifier located list -> aconstr -> unit -val find_reserved_type : identifier -> aconstr +val declare_reserved_type : identifier located list -> notation_constr -> unit +val find_reserved_type : identifier ->notation_constr val anonymize_if_reserved : name -> glob_constr -> glob_constr diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 66efe5982..6146bc42e 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -19,13 +19,13 @@ open Names open Libnames open Misctypes open Syntax_def -open Topconstr +open Notation_term let global_of_extended_global = function | TrueGlobal ref -> ref | SynDef kn -> match search_syntactic_definition kn with - | [],ARef ref -> ref + | [],NRef ref -> ref | _ -> raise Not_found let locate_global_with_alias (loc,qid) = diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index eb6f50131..f20d9727d 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -11,7 +11,7 @@ open Util open Pp open Names open Libnames -open Topconstr +open Notation_term open Libobject open Lib open Nameops @@ -38,7 +38,7 @@ let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) = Nametab.push_syndef (Nametab.Until i) sp kn let is_alias_of_already_visible_name sp = function - | _,ARef ref -> + | _,NRef ref -> let (dir,id) = repr_qualid (shortest_qualid_of_global Idset.empty ref) in dir = empty_dirpath && id = basename sp | _ -> @@ -58,7 +58,7 @@ let cache_syntax_constant d = open_syntax_constant 1 d let subst_syntax_constant (subst,(local,pat,onlyparse)) = - (local,subst_interpretation subst pat,onlyparse) + (local,Topconstr.subst_interpretation subst pat,onlyparse) let classify_syntax_constant (local,_,_ as o) = if local then Dispose else Substitute o @@ -71,7 +71,7 @@ let in_syntax_constant : bool * interpretation * bool -> obj = subst_function = subst_syntax_constant; classify_function = classify_syntax_constant } -type syndef_interpretation = (identifier * subscopes) list * aconstr +type syndef_interpretation = (identifier * subscopes) list * notation_constr (* Coercions to the general format of notation that also supports variables bound to list of expressions *) diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 9e15ab970..f0a45389a 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -9,14 +9,14 @@ open Errors open Util open Names -open Topconstr +open Notation_term open Glob_term open Nametab open Libnames (** Syntactic definitions. *) -type syndef_interpretation = (identifier * subscopes) list * aconstr +type syndef_interpretation = (identifier * subscopes) list * notation_constr val declare_syntactic_definition : bool -> identifier -> bool -> syndef_interpretation -> unit diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 9ea6c7e4c..ab603c37d 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -19,56 +19,11 @@ open Term open Mod_subst open Misctypes open Decl_kinds +open Constrexpr +open Notation_term (*i*) (**********************************************************************) -(* This is the subtype of glob_constr allowed in syntactic extensions *) - -(* For AList: first constr is iterator, second is terminator; - first id is where each argument of the list has to be substituted - in iterator and snd id is alternative name just for printing; - boolean is associativity *) - -type aconstr = - (* Part common to glob_constr and cases_pattern *) - | ARef of global_reference - | AVar of identifier - | AApp of aconstr * aconstr list - | AHole of Evar_kinds.t - | AList of identifier * identifier * aconstr * aconstr * bool - (* Part only in glob_constr *) - | 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 * name list) option)) list * - (cases_pattern list * aconstr) list - | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr - | AIf of aconstr * (name * aconstr option) * aconstr * aconstr - | ARec of fix_kind * identifier array * - (name * aconstr option * aconstr) list array * aconstr array * - aconstr array - | ASort of glob_sort - | 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 glob_constr, taking care of binders *) let name_to_ident = function @@ -101,28 +56,28 @@ let rec subst_glob_vars l = function let ldots_var = id_of_string ".." -let glob_constr_of_aconstr_with_binders loc g f e = function - | AVar id -> GVar (loc,id) - | AApp (a,args) -> GApp (loc,f e a, List.map (f e) args) - | AList (x,y,iter,tail,swap) -> +let glob_constr_of_notation_constr_with_binders loc g f e = function + | NVar id -> GVar (loc,id) + | NApp (a,args) -> GApp (loc,f e a, List.map (f e) args) + | NList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in let outerl = (ldots_var,inner)::(if swap then [x,GVar(loc,y)] else []) in subst_glob_vars outerl it - | ABinderList (x,y,iter,tail) -> + | NBinderList (x,y,iter,tail) -> let t = f e tail in let it = f e iter in let innerl = [(ldots_var,t);(x,GVar(loc,y))] in let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in let outerl = [(ldots_var,inner)] in subst_glob_vars outerl it - | ALambda (na,ty,c) -> + | NLambda (na,ty,c) -> let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c) - | AProd (na,ty,c) -> + | NProd (na,ty,c) -> let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c) - | ALetIn (na,b,c) -> + | NLetIn (na,b,c) -> let e',na = g e na in GLetIn (loc,na,f e b,f e' c) - | ACases (sty,rtntypopt,tml,eqnl) -> + | NCases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with | None -> e',None @@ -138,28 +93,28 @@ let glob_constr_of_aconstr_with_binders loc g f e = function list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in (loc,idl,patl,f e rhs)) eqnl in GCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl') - | ALetTuple (nal,(na,po),b,c) -> + | NLetTuple (nal,(na,po),b,c) -> let e',nal = list_fold_map g e nal in let e'',na = g e na in GLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c) - | AIf (c,(na,po),b1,b2) -> + | NIf (c,(na,po),b1,b2) -> let e',na = g e na in GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2) - | ARec (fk,idl,dll,tl,bl) -> + | NRec (fk,idl,dll,tl,bl) -> let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) -> let e,na = g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = array_fold_map (to_id g) e idl in GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) - | ACast (c,k) -> GCast (loc,f e c, Miscops.map_cast_type (f e) k) - | ASort x -> GSort (loc,x) - | AHole x -> GHole (loc,x) - | APatVar n -> GPatVar (loc,(false,n)) - | ARef x -> GRef (loc,x) + | NCast (c,k) -> GCast (loc,f e c, Miscops.map_cast_type (f e) k) + | NSort x -> GSort (loc,x) + | NHole x -> GHole (loc,x) + | NPatVar n -> GPatVar (loc,(false,n)) + | NRef x -> GRef (loc,x) -let rec glob_constr_of_aconstr loc x = +let rec glob_constr_of_notation_constr loc x = let rec aux () x = - glob_constr_of_aconstr_with_binders loc (fun () id -> ((),id)) aux () x + glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x in aux () x (****************************************************************************) @@ -260,17 +215,17 @@ let compare_recursive_parts found f (iterator,subc) = else iterator) in (* found have been collected by compare_constr *) found := newfound; - AList (x,y,iterator,f (Option.get !terminator),lassoc) + NList (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)) + NBinderList (x,y,iterator,f (Option.get !terminator)) else raise Not_found -let aconstr_and_vars_of_glob_constr a = +let notation_constr_and_vars_of_glob_constr a = let found = ref ([],[],[]) in let rec aux c = let keepfound = !found in @@ -287,14 +242,14 @@ let aconstr_and_vars_of_glob_constr a = | c -> aux' c and aux' = function - | GVar (_,id) -> add_id found id; AVar id - | GApp (_,g,args) -> AApp (aux g, List.map aux args) - | GLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c) - | GProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c) - | GLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c) + | GVar (_,id) -> add_id found id; NVar id + | GApp (_,g,args) -> NApp (aux g, List.map aux args) + | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c) + | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c) + | GLetIn (_,na,b,c) -> add_name found na; NLetIn (na,aux b,aux c) | GCases (_,sty,rtntypopt,tml,eqnl) -> let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in - ACases (sty,Option.map aux rtntypopt, + NCases (sty,Option.map aux rtntypopt, List.map (fun (tm,(na,x)) -> add_name found na; Option.iter @@ -304,22 +259,22 @@ let aconstr_and_vars_of_glob_constr a = | GLetTuple (loc,nal,(na,po),b,c) -> add_name found na; List.iter (add_name found) nal; - ALetTuple (nal,(na,Option.map aux po),aux b,aux c) + NLetTuple (nal,(na,Option.map aux po),aux b,aux c) | GIf (loc,c,(na,po),b1,b2) -> add_name found na; - AIf (aux c,(na,Option.map aux po),aux b1,aux b2) + NIf (aux c,(na,Option.map aux po),aux b1,aux b2) | GRec (_,fk,idl,dll,tl,bl) -> 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."; add_name found na; (na,Option.map aux oc,aux b))) dll in - ARec (fk,idl,dll,Array.map aux tl,Array.map aux bl) - | GCast (_,c,k) -> ACast (aux c,Miscops.map_cast_type aux k) - | GSort (_,s) -> ASort s - | GHole (_,w) -> AHole w - | GRef (_,r) -> ARef r - | GPatVar (_,(_,n)) -> APatVar n + NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) + | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k) + | GSort (_,s) -> NSort s + | GHole (_,w) -> NHole w + | GRef (_,r) -> NRef r + | GPatVar (_,(_,n)) -> NPatVar n | GEvar _ -> error "Existential variables not allowed in notations." @@ -369,15 +324,15 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) = | NtnInternTypeIdent -> check_bound x in List.iter check_type vars -let aconstr_of_glob_constr vars recvars a = - let a,found = aconstr_and_vars_of_glob_constr a in +let notation_constr_of_glob_constr vars recvars a = + let a,found = notation_constr_and_vars_of_glob_constr 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_glob_constr [] [] (Detyping.detype false avoiding [] t) +let notation_constr_of_constr avoiding t = + notation_constr_of_glob_constr [] [] (Detyping.detype false avoiding [] t) let rec subst_pat subst pat = match pat with @@ -388,56 +343,56 @@ let rec subst_pat subst pat = if kn' == kn && cpl' == cpl then pat else PatCstr (loc,((kn',i),j),cpl',n) -let rec subst_aconstr subst bound raw = +let rec subst_notation_constr subst bound raw = match raw with - | ARef ref -> + | NRef ref -> let ref',t = subst_global subst ref in if ref' == ref then raw else - aconstr_of_constr bound t + notation_constr_of_constr bound t - | AVar _ -> raw + | NVar _ -> raw - | AApp (r,rl) -> - let r' = subst_aconstr subst bound r - and rl' = list_smartmap (subst_aconstr subst bound) rl in + | NApp (r,rl) -> + let r' = subst_notation_constr subst bound r + and rl' = list_smartmap (subst_notation_constr subst bound) rl in if r' == r && rl' == rl then raw else - AApp(r',rl') + NApp(r',rl') - | AList (id1,id2,r1,r2,b) -> - let r1' = subst_aconstr subst bound r1 - and r2' = subst_aconstr subst bound r2 in + | NList (id1,id2,r1,r2,b) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else - AList (id1,id2,r1',r2',b) + NList (id1,id2,r1',r2',b) - | ALambda (n,r1,r2) -> - let r1' = subst_aconstr subst bound r1 - and r2' = subst_aconstr subst bound r2 in + | NLambda (n,r1,r2) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else - ALambda (n,r1',r2') + NLambda (n,r1',r2') - | AProd (n,r1,r2) -> - let r1' = subst_aconstr subst bound r1 - and r2' = subst_aconstr subst bound r2 in + | NProd (n,r1,r2) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else - AProd (n,r1',r2') + NProd (n,r1',r2') - | ABinderList (id1,id2,r1,r2) -> - let r1' = subst_aconstr subst bound r1 - and r2' = subst_aconstr subst bound r2 in + | NBinderList (id1,id2,r1,r2) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else - ABinderList (id1,id2,r1',r2') + NBinderList (id1,id2,r1',r2') - | ALetIn (n,r1,r2) -> - let r1' = subst_aconstr subst bound r1 - and r2' = subst_aconstr subst bound r2 in + | NLetIn (n,r1,r2) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else - ALetIn (n,r1',r2') + NLetIn (n,r1',r2') - | ACases (sty,rtntypopt,rl,branches) -> - let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt + | NCases (sty,rtntypopt,rl,branches) -> + let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt and rl' = list_smartmap (fun (a,(n,signopt) as x) -> - let a' = subst_aconstr subst bound a in + let a' = subst_notation_constr subst bound a in let signopt' = Option.map (fun ((indkn,i),nal as z) -> let indkn' = subst_ind subst indkn in if indkn == indkn' then z else ((indkn',i),nal)) signopt in @@ -446,62 +401,62 @@ let rec subst_aconstr subst bound raw = and branches' = list_smartmap (fun (cpl,r as branch) -> let cpl' = list_smartmap (subst_pat subst) cpl - and r' = subst_aconstr subst bound r in + and r' = subst_notation_constr subst bound r in if cpl' == cpl && r' == r then branch else (cpl',r')) branches in if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' & rl' == rl && branches' == branches then raw else - ACases (sty,rtntypopt',rl',branches') + NCases (sty,rtntypopt',rl',branches') - | ALetTuple (nal,(na,po),b,c) -> - let po' = Option.smartmap (subst_aconstr subst bound) po - and b' = subst_aconstr subst bound b - and c' = subst_aconstr subst bound c in + | NLetTuple (nal,(na,po),b,c) -> + let po' = Option.smartmap (subst_notation_constr subst bound) po + and b' = subst_notation_constr subst bound b + and c' = subst_notation_constr subst bound c in if po' == po && b' == b && c' == c then raw else - ALetTuple (nal,(na,po'),b',c') + NLetTuple (nal,(na,po'),b',c') - | AIf (c,(na,po),b1,b2) -> - let po' = Option.smartmap (subst_aconstr subst bound) po - and b1' = subst_aconstr subst bound b1 - and b2' = subst_aconstr subst bound b2 - and c' = subst_aconstr subst bound c in + | NIf (c,(na,po),b1,b2) -> + let po' = Option.smartmap (subst_notation_constr subst bound) po + and b1' = subst_notation_constr subst bound b1 + and b2' = subst_notation_constr subst bound b2 + and c' = subst_notation_constr subst bound c in if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else - AIf (c',(na,po'),b1',b2') + NIf (c',(na,po'),b1',b2') - | ARec (fk,idl,dll,tl,bl) -> + | NRec (fk,idl,dll,tl,bl) -> let dll' = array_smartmap (list_smartmap (fun (na,oc,b as x) -> - let oc' = Option.smartmap (subst_aconstr subst bound) oc in - let b' = subst_aconstr subst bound b in + let oc' = Option.smartmap (subst_notation_constr subst bound) oc in + let b' = subst_notation_constr subst bound b in if oc' == oc && b' == b then x else (na,oc',b'))) dll in - let tl' = array_smartmap (subst_aconstr subst bound) tl in - let bl' = array_smartmap (subst_aconstr subst bound) bl in + let tl' = array_smartmap (subst_notation_constr subst bound) tl in + let bl' = array_smartmap (subst_notation_constr subst bound) bl in if dll' == dll && tl' == tl && bl' == bl then raw else - ARec (fk,idl,dll',tl',bl') + NRec (fk,idl,dll',tl',bl') - | APatVar _ | ASort _ -> raw + | NPatVar _ | NSort _ -> raw - | AHole (Evar_kinds.ImplicitArg (ref,i,b)) -> + | NHole (Evar_kinds.ImplicitArg (ref,i,b)) -> let ref',t = subst_global subst ref in if ref' == ref then raw else - AHole (Evar_kinds.InternalHole) - | AHole (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _ + NHole (Evar_kinds.InternalHole) + | NHole (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _ |Evar_kinds.CasesType |Evar_kinds.InternalHole |Evar_kinds.TomatchTypeParameter _ |Evar_kinds.GoalEvar |Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _) -> raw - | ACast (r1,k) -> - let r1' = subst_aconstr subst bound r1 in - let k' = Miscops.smartmap_cast_type (subst_aconstr subst bound) k in - if r1' == r1 && k' == k then raw else ACast(r1',k') + | NCast (r1,k) -> + let r1' = subst_notation_constr subst bound r1 in + let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in + if r1' == r1 && k' == k then raw else NCast(r1',k') let subst_interpretation subst (metas,pat) = let bound = List.map fst metas in - (metas,subst_aconstr subst bound pat) + (metas,subst_notation_constr subst bound pat) -(* Pattern-matching glob_constr and aconstr *) +(* Pattern-matching glob_constr and notation_constr *) let abstract_return_type_context pi mklam tml rtno = Option.map (fun rtn -> @@ -516,9 +471,9 @@ let abstract_return_type_context_glob_constr = (fun na c -> GLambda(dummy_loc,na,Explicit,GHole(dummy_loc,Evar_kinds.InternalHole),c)) -let abstract_return_type_context_aconstr = +let abstract_return_type_context_notation_constr = abstract_return_type_context snd - (fun na c -> ALambda(na,AHole Evar_kinds.InternalHole,c)) + (fun na c -> NLambda(na,NHole Evar_kinds.InternalHole,c)) exception No_match @@ -633,60 +588,60 @@ let rec match_ inner u 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 + | r1, NVar id2 when List.mem id2 tmetas -> bind_env alp sigma id2 r1 (* Matching recursive notations for terms *) - | r1, AList (x,_,iter,termin,lassoc) -> + | r1, NList (x,_,iter,termin,lassoc) -> match_alist (match_hd u alp) metas sigma r1 x iter termin lassoc (* Matching recursive notations for binders: ad hoc cases supporting let-in *) - | GLambda (_,na1,bk,t1,b1), ABinderList (x,_,ALambda (Name id2,_,b2),termin)-> + | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (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_in u alp metas (bind_binder sigma x decls) b termin - | GProd (_,na1,bk,t1,b1), ABinderList (x,_,AProd (Name id2,_,b2),termin) + | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (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_in u alp metas (bind_binder sigma x decls) b termin (* Matching recursive notations for binders: general case *) - | r, ABinderList (x,_,iter,termin) -> + | r, NBinderList (x,_,iter,termin) -> match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin (* Matching individual binders as part of a recursive pattern *) - | GLambda (_,na,bk,t,b1), ALambda (Name id,_,b2) when List.mem id blmetas -> + | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when List.mem id blmetas -> match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 - | GProd (_,na,bk,t,b1), AProd (Name id,_,b2) + | GProd (_,na,bk,t,b1), NProd (Name id,_,b2) when List.mem id blmetas & na <> Anonymous -> match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 (* Matching compositionally *) - | GVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma - | GRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma - | GPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma - | GApp (loc,f1,l1), AApp (f2,l2) -> + | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma + | GRef (_,r1), NRef r2 when (eq_gr r1 r2) -> sigma + | GPatVar (_,(_,n1)), NPatVar n2 when n1=n2 -> sigma + | GApp (loc,f1,l1), NApp (f2,l2) -> let n1 = List.length l1 and n2 = List.length l2 in let f1,l1,f2,l2 = if n1 < n2 then - let l21,l22 = list_chop (n2-n1) l2 in f1,l1, AApp (f2,l21), l22 + let l21,l22 = list_chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22 else if n1 > n2 then let l11,l12 = list_chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2 else f1,l1, f2, l2 in let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in List.fold_left2 (match_ may_use_eta u alp metas) (match_in u alp metas sigma f1 f2) l1 l2 - | GLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) -> + | GLambda (_,na1,_,t1,b1), NLambda (na2,t2,b2) -> match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 - | GProd (_,na1,_,t1,b1), AProd (na2,t2,b2) -> + | GProd (_,na1,_,t1,b1), NProd (na2,t2,b2) -> match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 - | GLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) -> + | GLetIn (_,na1,t1,b1), NLetIn (na2,t2,b2) -> match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 - | GCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2) + | GCases (_,sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2) when sty1 = sty2 & List.length tml1 = List.length tml2 & List.length eqnl1 = List.length eqnl2 -> let rtno1' = abstract_return_type_context_glob_constr tml1 rtno1 in - let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in + let rtno2' = abstract_return_type_context_notation_constr tml2 rtno2 in let sigma = try Option.fold_left2 (match_in u alp metas) sigma rtno1' rtno2' with Option.Heterogeneous -> raise No_match @@ -695,17 +650,17 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = (fun s (tm1,_) (tm2,_) -> match_in u alp metas s tm1 tm2) sigma tml1 tml2 in List.fold_left2 (match_equations u alp metas) sigma eqnl1 eqnl2 - | GLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2) + | GLetTuple (_,nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2) when List.length nal1 = List.length nal2 -> let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in let sigma = match_in u alp metas sigma b1 b2 in let (alp,sigma) = List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in match_in u alp metas sigma c1 c2 - | GIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) -> + | GIf (_,a1,(na1,to1),b1,c1), NIf (a2,(na2,to2),b2,c2) -> let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in List.fold_left2 (match_in u alp metas) sigma [a1;b1;c1] [a2;b2;c2] - | GRec (_,fk1,idl1,dll1,tl1,bl1), ARec (fk2,idl2,dll2,tl2,bl2) + | GRec (_,fk1,idl1,dll1,tl1,bl1), NRec (fk2,idl2,dll2,tl2,bl2) when match_fix_kind fk1 fk2 & Array.length idl1 = Array.length idl2 & array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) dll1 dll2 -> @@ -719,21 +674,21 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = let alp,sigma = array_fold_right2 (fun id1 id2 alsig -> match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in array_fold_left2 (match_in u alp metas) sigma bl1 bl2 - | GCast(_,c1,CastConv t1), ACast (c2,CastConv t2) - | GCast(_,c1,CastVM t1), ACast (c2,CastVM t2) -> + | GCast(_,c1,CastConv t1), NCast (c2,CastConv t2) + | GCast(_,c1,CastVM t1), NCast (c2,CastVM t2) -> match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2 - | GCast(_,c1, CastCoerce), ACast(c2, CastCoerce) -> + | GCast(_,c1, CastCoerce), NCast(c2, CastCoerce) -> match_in u alp metas sigma c1 c2 - | GSort (_,GType _), ASort (GType None) when not u -> sigma - | GSort (_,s1), ASort s2 when s1 = s2 -> sigma - | GPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match - | a, AHole _ -> sigma + | GSort (_,GType _), NSort (GType None) when not u -> sigma + | GSort (_,s1), NSort s2 when s1 = s2 -> sigma + | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match + | a, NHole _ -> sigma (* On the fly eta-expansion so as to use notations of the form "exists x, P x" for "ex P"; expects type not given because don't know otherwise how to ensure it corresponds to a well-typed eta-expansion; ensure at least one constructor is consumed to avoid looping *) - | b1, ALambda (Name id,AHole _,b2) when inner -> + | b1, NLambda (Name id,NHole _,b2) when inner -> let id' = Namegen.next_ident_away id (free_glob_vars b1) in match_in u alp metas (bind_binder sigma id [(Name id',Explicit,None,GHole(dummy_loc,Evar_kinds.BinderType (Name id')))]) @@ -758,7 +713,7 @@ and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) = (alp,sigma) patl1 patl2 in match_in u alp metas sigma rhs1 rhs2 -let match_aconstr u c (metas,pat) = +let match_notation_constr u 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_ false u [] vars ([],[],[]) c pat in @@ -795,11 +750,11 @@ let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v = 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),[] - | PatVar (_,Anonymous), AHole _ -> sigma,[] - | PatCstr (loc,(ind,_ as r1),largs,_), ARef (ConstructRef r2) when r1 = r2 -> + | r1, NVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),[] + | PatVar (_,Anonymous), NHole _ -> sigma,[] + | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when r1 = r2 -> sigma,largs - | PatCstr (loc,(ind,_ as r1),args1,_), AApp (ARef (ConstructRef r2),l2) + | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) when r1 = r2 -> let l1 = add_patterns_for_params (fst r1) args1 in let le2 = List.length l2 in @@ -809,7 +764,7 @@ let rec match_cases_pattern metas sigma a1 a2 = else let l1',more_args = Util.list_chop le2 l1 in (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),more_args - | r1, AList (x,_,iter,termin,lassoc) -> + | r1, NList (x,_,iter,termin,lassoc) -> (match_alist (fun (metas,_) -> match_cases_pattern_no_more_args metas) (metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc),[] | _ -> raise No_match @@ -841,7 +796,7 @@ let reorder_canonically_substitution terms termlists metas = | NtnTypeBinderList -> assert false) metas ([],[]) -let match_aconstr_cases_pattern c (metas,pat) = +let match_notation_constr_cases_pattern c (metas,pat) = let vars = List.map fst metas in let (terms,termlists,()),more_args = match_cases_pattern vars ([],[],()) c pat in reorder_canonically_substitution terms termlists metas,more_args @@ -851,89 +806,6 @@ let match_aconstr_ind_pattern ind args (metas,pat) = let (terms,termlists,()),more_args = match_ind_pattern vars ([],[],()) ind args pat in reorder_canonically_substitution terms termlists metas,more_args -(**********************************************************************) -(*s Concrete syntax for terms *) - -type notation = string - -type explicitation = ExplByPos of int * identifier option | ExplByName of identifier - -type binder_kind = Default of binding_kind | Generalized of binding_kind * binding_kind * bool - -type abstraction_kind = AbsLambda | AbsPi - -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 cases_pattern_expr = - | CPatAlias of loc * cases_pattern_expr * identifier - | CPatCstr of loc * reference * cases_pattern_expr list - | CPatCstrExpl 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_notation_substitution - | CPatPrim of loc * prim_token - | CPatRecord of 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 - | CCoFix of loc * identifier located * cofix_expr list - | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr - | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr - | CLetIn of loc * name located * constr_expr * constr_expr - | CAppExpl of loc * (proj_flag * reference) * constr_expr list - | CApp of loc * (proj_flag * 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 located option * cases_pattern_expr option)) list * - (loc * cases_pattern_expr list located list * constr_expr) list - | CLetTuple of loc * name located list * (name located option * constr_expr option) * - constr_expr * constr_expr - | CIf of loc * constr_expr * (name located option * constr_expr option) - * constr_expr * constr_expr - | CHole of loc * Evar_kinds.t option - | CPatVar of loc * (bool * patvar) - | CEvar of loc * existential_key * constr_expr list option - | CSort of loc * glob_sort - | CCast of loc * constr_expr * constr_expr cast_type - | 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 - -and fix_expr = - identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr - -and cofix_expr = - identifier located * local_binder list * constr_expr * constr_expr - -and recursion_order_expr = - | CStructRec - | 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 let oldfashion_patterns = ref (true) let write_oldfashion_patterns = Goptions.declare_bool_option { diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 101c39eea..760ee14a5 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -15,66 +15,17 @@ open Term open Mod_subst open Misctypes open Decl_kinds +open Constrexpr +open Notation_term -(** Topconstr: definitions of [aconstr] et [constr_expr] *) - -(** {6 aconstr } *) -(** This is the subtype of glob_constr allowed in syntactic extensions - No location since intended to be substituted at any place of a text - Complex expressions such as fixpoints and cofixpoints are excluded, - non global expressions such as existential variables also *) - -type aconstr = - (** Part common to [glob_constr] and [cases_pattern] *) - | ARef of global_reference - | AVar of identifier - | AApp of aconstr * aconstr list - | AHole of Evar_kinds.t - | AList of identifier * identifier * aconstr * aconstr * bool - (** Part only in [glob_constr] *) - | 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 * name list) option)) list * - (cases_pattern list * aconstr) list - | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr - | AIf of aconstr * (name * aconstr option) * aconstr * aconstr - | ARec of fix_kind * identifier array * - (name * aconstr option * aconstr) list array * aconstr array * - aconstr array - | ASort of glob_sort - | 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 +(** Topconstr *) (** Translate a glob_constr into a notation given the list of variables bound by the notation; also interpret recursive patterns *) -val aconstr_of_glob_constr : +val notation_constr_of_glob_constr : (identifier * notation_var_internalization_type) list -> - (identifier * identifier) list -> glob_constr -> aconstr + (identifier * identifier) list -> glob_constr -> notation_constr (** Name of the special identifier used to encode recursive notations *) val ldots_var : identifier @@ -84,23 +35,26 @@ val eq_glob_constr : glob_constr -> glob_constr -> bool (** Re-interpret a notation as a glob_constr, taking care of binders *) -val glob_constr_of_aconstr_with_binders : loc -> +val glob_constr_of_notation_constr_with_binders : loc -> ('a -> name -> 'a * name) -> - ('a -> aconstr -> glob_constr) -> 'a -> aconstr -> glob_constr + ('a -> notation_constr -> glob_constr) -> + 'a -> notation_constr -> glob_constr -val glob_constr_of_aconstr : loc -> aconstr -> glob_constr +val glob_constr_of_notation_constr : loc -> notation_constr -> glob_constr -(** [match_aconstr] matches a glob_constr against a notation interpretation; +(** [match_notation_constr] matches a glob_constr against a notation interpretation; raise [No_match] if the matching fails *) exception No_match -val match_aconstr : bool -> glob_constr -> interpretation -> +val match_notation_constr : bool -> glob_constr -> interpretation -> (glob_constr * subscopes) list * (glob_constr list * subscopes) list * (glob_decl list * subscopes) list -val match_aconstr_cases_pattern : cases_pattern -> interpretation -> - ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (cases_pattern list) +val match_notation_constr_cases_pattern : + cases_pattern -> interpretation -> + ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * + (cases_pattern list) val match_aconstr_ind_pattern : inductive -> cases_pattern list -> interpretation -> ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (cases_pattern list) @@ -109,94 +63,6 @@ val match_aconstr_ind_pattern : inductive -> cases_pattern list -> interpretati val subst_interpretation : substitution -> interpretation -> interpretation -(** {6 Concrete syntax for terms } *) - -type notation = string - -type explicitation = ExplByPos of int * identifier option | ExplByName of identifier - -type binder_kind = - | Default of binding_kind - | Generalized of binding_kind * binding_kind * bool - (** Inner binding, outer bindings, typeclass-specific flag - for implicit generalization of superclasses *) - -type abstraction_kind = AbsLambda | AbsPi - -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 cases_pattern_expr = - | CPatAlias of loc * cases_pattern_expr * identifier - | CPatCstr of loc * reference * cases_pattern_expr list - | CPatCstrExpl 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_notation_substitution - | CPatPrim of loc * prim_token - | CPatRecord of 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 - | CCoFix of loc * identifier located * cofix_expr list - | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr - | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr - | CLetIn of loc * name located * constr_expr * constr_expr - | CAppExpl of loc * (proj_flag * reference) * constr_expr list - | CApp of loc * (proj_flag * 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 located option * cases_pattern_expr option)) list * - (loc * cases_pattern_expr list located list * constr_expr) list - | CLetTuple of loc * name located list * (name located option * constr_expr option) * - constr_expr * constr_expr - | CIf of loc * constr_expr * (name located option * constr_expr option) - * constr_expr * constr_expr - | CHole of loc * Evar_kinds.t option - | CPatVar of loc * (bool * patvar) - | CEvar of loc * existential_key * constr_expr list option - | CSort of loc * glob_sort - | CCast of loc * constr_expr * constr_expr cast_type - | 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 - -and fix_expr = - identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr - -and cofix_expr = - identifier located * local_binder list * constr_expr * constr_expr - -and recursion_order_expr = - | CStructRec - | CWfRec of constr_expr - | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) - -(** Anonymous defs allowed ?? *) -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 - val oldfashion_patterns : bool ref (** Utilities on constr_expr *) @@ -259,17 +125,6 @@ val map_constr_expr_with_binders : (identifier -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) -> 'a -> constr_expr -> constr_expr -(** Concrete syntax for modules and module types *) - -type with_declaration_ast = - | CWith_Module of identifier list located * qualid located - | CWith_Definition of identifier list located * constr_expr - -type module_ast = - | CMident of qualid located - | CMapply of loc * module_ast * module_ast - | CMwith of loc * module_ast * with_declaration_ast - val ntn_loc : loc -> constr_notation_substitution -> string -> (int * int) list val patntn_loc : diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli new file mode 100644 index 000000000..f6d274abb --- /dev/null +++ b/intf/constrexpr.mli @@ -0,0 +1,118 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Names +open Libnames +open Term +open Misctypes +open Decl_kinds + +(** {6 Concrete syntax for terms } *) + +(** [constr_expr] is the abstract syntax tree produced by the parser *) + +type notation = string + +type explicitation = + | ExplByPos of int * identifier option + | ExplByName of identifier + +type binder_kind = + | Default of binding_kind + | Generalized of binding_kind * binding_kind * bool + (** Inner binding, outer bindings, typeclass-specific flag + for implicit generalization of superclasses *) + +type abstraction_kind = AbsLambda | AbsPi + +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 cases_pattern_expr = + | CPatAlias of loc * cases_pattern_expr * identifier + | CPatCstr of loc * reference * cases_pattern_expr list + | CPatCstrExpl 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_notation_substitution + | CPatPrim of loc * prim_token + | CPatRecord of 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 + | CCoFix of loc * identifier located * cofix_expr list + | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr + | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr + | CLetIn of loc * name located * constr_expr * constr_expr + | CAppExpl of loc * (proj_flag * reference) * constr_expr list + | CApp of loc * (proj_flag * 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 located option * cases_pattern_expr option)) list * + (loc * cases_pattern_expr list located list * constr_expr) list + | CLetTuple of loc * name located list * (name located option * constr_expr option) * + constr_expr * constr_expr + | CIf of loc * constr_expr * (name located option * constr_expr option) + * constr_expr * constr_expr + | CHole of loc * Evar_kinds.t option + | CPatVar of loc * (bool * patvar) + | CEvar of loc * existential_key * constr_expr list option + | CSort of loc * glob_sort + | CCast of loc * constr_expr * constr_expr cast_type + | 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 + +and fix_expr = + identifier located * (identifier located option * recursion_order_expr) * + local_binder list * constr_expr * constr_expr + +and cofix_expr = + identifier located * local_binder list * constr_expr * constr_expr + +and recursion_order_expr = + | CStructRec + | CWfRec of constr_expr + | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) + +(** Anonymous defs allowed ?? *) +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 + +(** Concrete syntax for modules and module types *) + +type with_declaration_ast = + | CWith_Module of identifier list located * qualid located + | CWith_Definition of identifier list located * constr_expr + +type module_ast = + | CMident of qualid located + | CMapply of loc * module_ast * module_ast + | CMwith of loc * module_ast * with_declaration_ast diff --git a/intf/notation_term.mli b/intf/notation_term.mli new file mode 100644 index 000000000..2485fd7a6 --- /dev/null +++ b/intf/notation_term.mli @@ -0,0 +1,76 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Term +open Libnames +open Misctypes +open Glob_term + +(** [notation_constr] *) + +(** [notation_constr] is the subtype of [glob_constr] allowed in syntactic + extensions (i.e. notations). + No location since intended to be substituted at any place of a text. + Complex expressions such as fixpoints and cofixpoints are excluded, + as well as non global expressions such as existential variables. *) + +type notation_constr = + (** Part common to [glob_constr] and [cases_pattern] *) + | NRef of global_reference + | NVar of identifier + | NApp of notation_constr * notation_constr list + | NHole of Evar_kinds.t + | NList of identifier * identifier * notation_constr * notation_constr * bool + (** Part only in [glob_constr] *) + | NLambda of name * notation_constr * notation_constr + | NProd of name * notation_constr * notation_constr + | NBinderList of identifier * identifier * notation_constr * notation_constr + | NLetIn of name * notation_constr * notation_constr + | NCases of case_style * notation_constr option * + (notation_constr * (name * (inductive * name list) option)) list * + (cases_pattern list * notation_constr) list + | NLetTuple of name list * (name * notation_constr option) * + notation_constr * notation_constr + | NIf of notation_constr * (name * notation_constr option) * + notation_constr * notation_constr + | NRec of fix_kind * identifier array * + (name * notation_constr option * notation_constr) list array * + notation_constr array * notation_constr array + | NSort of glob_sort + | NPatVar of patvar + | NCast of notation_constr * notation_constr cast_type + +(** Note concerning NList: first constr is iterator, second is terminator; + first id is where each argument of the list has to be substituted + in iterator and snd id is alternative name just for printing; + boolean is associativity *) + +(** Types concerning notations *) + +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 notation_constr: 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 notation_constr: + 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 * + notation_constr diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index d8e340d1e..e70fc1308 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Topconstr +open Constrexpr open Libnames open Nametab open Genredexpr diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index fc3f94920..3223e80b8 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -10,7 +10,8 @@ open Pp open Names open Tacexpr open Misctypes -open Topconstr +open Constrexpr +open Notation_term open Decl_kinds open Libnames diff --git a/library/impargs.ml b/library/impargs.ml index d7d0d4879..707b2f4cb 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -19,7 +19,7 @@ open Libobject open Lib open Nametab open Pp -open Topconstr +open Constrexpr open Termops open Namegen open Decl_kinds @@ -614,7 +614,7 @@ let declare_mib_implicits kn = (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps)) (* Declare manual implicits *) -type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) +type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool) type manual_implicits = manual_explicitation list diff --git a/library/impargs.mli b/library/impargs.mli index 04251f332..57f1ac71e 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -87,7 +87,7 @@ val positions_of_implicits : implicits_list -> int list (** A [manual_explicitation] is a tuple of a positional or named explicitation with maximal insertion, force inference and force usage flags. Forcing usage makes the argument implicit even if the automatic inference considers it not inferable. *) -type manual_explicitation = Topconstr.explicitation * +type manual_explicitation = Constrexpr.explicitation * (maximal_insertion * force_inference * bool) type manual_implicits = manual_explicitation list diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 17a4d98ad..d55363b17 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -13,7 +13,8 @@ open Util open Pcoq open Extend open Ppextend -open Topconstr +open Constrexpr +open Notation_term open Genarg open Libnames open Nameops @@ -108,7 +109,7 @@ let make_constr_action make ([],[],[]) (List.rev pil) let check_cases_pattern_env loc (env,envlist,hasbinders) = - if hasbinders then error_invalid_pattern_notation loc else (env,envlist) + if hasbinders then Topconstr.error_invalid_pattern_notation loc else (env,envlist) let make_cases_pattern_action (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil = diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index c9f92b729..108f39eaa 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -10,7 +10,8 @@ open Compat open Errors open Pp open Names -open Topconstr +open Constrexpr +open Notation_term open Pcoq open Extend open Vernacexpr diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index c8ca6cbab..1bc46f83f 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -14,7 +14,7 @@ open Glob_term open Term open Names open Libnames -open Topconstr +open Constrexpr open Util open Tok open Compat @@ -31,7 +31,9 @@ let _ = List.iter Lexer.add_keyword constr_kw let mk_cast = function (c,(_,None)) -> c - | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv ty) + | (c,(_,Some ty)) -> + let loc = join_loc (Topconstr.constr_loc c) (Topconstr.constr_loc ty) + in CCast(loc, c, CastConv ty) let binders_of_names l = List.map (fun (loc, na) -> @@ -223,13 +225,15 @@ GEXTEND Gram ; binder_constr: [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" -> - mkCProdN loc bl c + Topconstr.mkCProdN loc bl c | lambda; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> - mkCLambdaN loc bl c + Topconstr.mkCLambdaN loc bl c | "let"; id=name; bl = binders; ty = type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - let loc1 = join_loc (local_binders_loc bl) (constr_loc c1) in - CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2) + let loc1 = + join_loc (Topconstr.local_binders_loc bl) (Topconstr.constr_loc c1) + in + CLetIn(loc,id,Topconstr.mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2) | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> let fixp = mk_single_fix fx in let (li,id) = match fixp with @@ -338,7 +342,7 @@ GEXTEND Gram (match p with | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) | _ -> Errors.user_err_loc - (cases_pattern_expr_loc p, "compound_pattern", + (Topconstr.cases_pattern_expr_loc p, "compound_pattern", Pp.str "Constructor expected.")) |"@"; r = Prim.reference; lp = LIST1 NEXT -> CPatCstrExpl (loc, r, lp) ] @@ -391,7 +395,7 @@ GEXTEND Gram | id = name; idl = LIST0 name; bl = binders -> binders_of_names (id::idl) @ bl | id1 = name; ".."; id2 = name -> - [LocalRawAssum ([id1;(loc,Name ldots_var);id2], + [LocalRawAssum ([id1;(loc,Name Topconstr.ldots_var);id2], Default Explicit,CHole (loc,None))] | bl = closed_binder; bl' = binders -> bl@bl' @@ -412,7 +416,7 @@ GEXTEND Gram | "("; id=name; ":="; c=lconstr; ")" -> [LocalRawDef (id,c)] | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv t))] + [LocalRawDef (id,CCast (join_loc (Topconstr.constr_loc t) loc,c, CastConv t))] | "{"; id=name; "}" -> [LocalRawAssum ([id],Default Implicit,CHole (loc, None))] | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 811fd58ff..c8356b603 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -8,7 +8,7 @@ open Pp open Util -open Topconstr +open Constrexpr open Glob_term open Tacexpr open Vernacexpr diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4 index 8ec546ffd..339e0ca16 100644 --- a/parsing/g_obligations.ml4 +++ b/parsing/g_obligations.ml4 @@ -20,6 +20,7 @@ open Nameops open Reduction open Term open Libnames +open Constrexpr open Topconstr (* We define new entries for programs, with the use of this module diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 6edb0bfc1..22a9e0d85 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -11,7 +11,7 @@ open Pp open Tactic open Util open Vernac_ -open Topconstr +open Constrexpr open Vernacexpr open Locality open Prim diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 4c1d747ea..c373371d2 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -13,7 +13,7 @@ open Util open Tacexpr open Genredexpr open Genarg -open Topconstr +open Constrexpr open Libnames open Termops open Tok @@ -129,7 +129,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) = (* Functions overloaded by quotifier *) let induction_arg_of_constr (c,lbind as clbind) = if lbind = NoBindings then - try ElimOnIdent (constr_loc c,snd(coerce_to_id c)) + try ElimOnIdent (Topconstr.constr_loc c,snd(Topconstr.coerce_to_id c)) with _ -> ElimOnConstr clbind else ElimOnConstr clbind @@ -163,7 +163,7 @@ let rec mkCLambdaN_simple_loc loc bll c = let mkCLambdaN_simple bl c = if bl=[] then c else - let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (constr_loc c) in + let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (Topconstr.constr_loc c) in mkCLambdaN_simple_loc loc bl c let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l)) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 83c5e6f31..51088564b 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -12,6 +12,7 @@ open Tok open Errors open Util open Names +open Constrexpr open Topconstr open Extend open Vernacexpr diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index e113bb711..886f91ea0 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -13,7 +13,7 @@ open Glob_term open Extend open Vernacexpr open Genarg -open Topconstr +open Constrexpr open Tacexpr open Libnames open Compat diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 6b2e206b6..d7e968ad4 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -15,6 +15,7 @@ open Names open Nameops open Libnames open Ppextend +open Constrexpr open Topconstr open Term open Pattern @@ -338,7 +339,7 @@ let pr_guard_annot pr_aux bl (n,ro) = match n with | None -> mt () | Some (loc, id) -> - match (ro : Topconstr.recursion_order_expr) with + match (ro : Constrexpr.recursion_order_expr) with | CStructRec -> let names_of_binder = function | LocalRawAssum (nal,_,_) -> nal diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index 390869cf7..88e4e55dc 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -12,7 +12,7 @@ open Term open Libnames open Pcoq open Glob_term -open Topconstr +open Constrexpr open Names open Errors open Util diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 5d03b6028..bbfecac8f 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -13,7 +13,7 @@ open Errors open Util open Tacexpr open Glob_term -open Topconstr +open Constrexpr open Genarg open Libnames open Pattern @@ -294,7 +294,7 @@ let pr_extend prc prlc prtac prpat = let strip_prod_binders_expr n ty = let rec strip_ty acc n ty = match ty with - Topconstr.CProdN(_,bll,a) -> + Constrexpr.CProdN(_,bll,a) -> let nb = List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in let bll = List.map (fun (x, _, y) -> x, y) bll in diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index afcc83c68..7a5c43531 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -11,7 +11,7 @@ open Genarg open Tacexpr open Pretyping open Proof_type -open Topconstr +open Constrexpr open Glob_term open Pattern open Ppextend diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 9f0cc4c03..2cbc0222b 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -22,6 +22,7 @@ open Genarg open Pcoq open Libnames open Ppextend +open Constrexpr open Topconstr open Decl_kinds open Tacinterp @@ -752,7 +753,7 @@ let rec pr_vernac = function ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in pr_raw_tactic_env - (idl @ List.map coerce_reference_to_id + (idl @ List.map Topconstr.coerce_reference_to_id (List.map (fun (x, _, _) -> x) (List.filter (fun (_, redef, _) -> not redef) l))) (Global.env()) body in diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 5dbef1fe5..d90e655b1 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -44,7 +44,7 @@ type object_pr = { print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; print_typed_value_in_env : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds; - print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds; + print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds; } let gallina_print_module = print_module @@ -435,7 +435,7 @@ let gallina_print_constant_with_infos sp = let gallina_print_syntactic_def kn = let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn and (vars,a) = Syntax_def.search_syntactic_definition kn in - let c = Topconstr.glob_constr_of_aconstr dummy_loc a in + let c = Topconstr.glob_constr_of_notation_constr dummy_loc a in hov 2 (hov 4 (str "Notation " ++ pr_qualid qid ++ diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index b3271d141..122da7ebf 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -33,7 +33,8 @@ val print_sec_context_typ : reference -> std_ppcmds val print_judgment : env -> unsafe_judgment -> std_ppcmds val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds val print_eval : - reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds + reduction_function -> env -> Evd.evar_map -> + Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds val print_name : reference or_by_notation -> std_ppcmds val print_opaque_name : reference -> std_ppcmds @@ -68,7 +69,7 @@ type object_pr = { print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; print_typed_value_in_env : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds; - print_eval : reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds + print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds } val set_object_pr : object_pr -> unit diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index a75d1f6cc..cb4fad6f5 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -122,40 +122,40 @@ let mlexpr_of_red_flags { } >> let mlexpr_of_explicitation = function - | Topconstr.ExplByName id -> <:expr< Topconstr.ExplByName $mlexpr_of_ident id$ >> - | Topconstr.ExplByPos (n,_id) -> <:expr< Topconstr.ExplByPos $mlexpr_of_int n$ >> + | Constrexpr.ExplByName id -> <:expr< Constrexpr.ExplByName $mlexpr_of_ident id$ >> + | Constrexpr.ExplByPos (n,_id) -> <:expr< Constrexpr.ExplByPos $mlexpr_of_int n$ >> let mlexpr_of_binding_kind = function | Decl_kinds.Implicit -> <:expr< Decl_kinds.Implicit >> | Decl_kinds.Explicit -> <:expr< Decl_kinds.Explicit >> let mlexpr_of_binder_kind = function - | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >> - | Topconstr.Generalized (b,b',b'') -> - <:expr< Topconstr.TypeClass $mlexpr_of_binding_kind b$ + | Constrexpr.Default b -> <:expr< Constrexpr.Default $mlexpr_of_binding_kind b$ >> + | Constrexpr.Generalized (b,b',b'') -> + <:expr< Constrexpr.TypeClass $mlexpr_of_binding_kind b$ $mlexpr_of_binding_kind b'$ $mlexpr_of_bool b''$ >> let rec mlexpr_of_constr = function - | Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) -> + | Constrexpr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) -> anti loc (string_of_id id) - | Topconstr.CRef r -> <:expr< Topconstr.CRef $mlexpr_of_reference r$ >> - | Topconstr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" - | Topconstr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" - | Topconstr.CProdN (loc,l,a) -> <:expr< Topconstr.CProdN $dloc$ $mlexpr_of_list + | Constrexpr.CRef r -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ >> + | Constrexpr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" + | Constrexpr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" + | Constrexpr.CProdN (loc,l,a) -> <:expr< Constrexpr.CProdN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> - | Topconstr.CLambdaN (loc,l,a) -> <:expr< Topconstr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> - | Topconstr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO" - | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >> - | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >> - | Topconstr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO" - | Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >> - | Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" - | Topconstr.CNotation(_,ntn,(subst,substl,[])) -> - <:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$ + | Constrexpr.CLambdaN (loc,l,a) -> <:expr< Constrexpr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> + | Constrexpr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO" + | Constrexpr.CAppExpl (loc,a,l) -> <:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >> + | Constrexpr.CApp (loc,a,l) -> <:expr< Constrexpr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >> + | Constrexpr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO" + | Constrexpr.CHole (loc, None) -> <:expr< Constrexpr.CHole $dloc$ None >> + | Constrexpr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" + | Constrexpr.CNotation(_,ntn,(subst,substl,[])) -> + <:expr< Constrexpr.CNotation $dloc$ $mlexpr_of_string ntn$ ($mlexpr_of_list mlexpr_of_constr subst$, $mlexpr_of_list (mlexpr_of_list mlexpr_of_constr) substl$,[]) >> - | Topconstr.CPatVar (loc,n) -> - <:expr< Topconstr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >> + | Constrexpr.CPatVar (loc,n) -> + <:expr< Constrexpr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >> | _ -> failwith "mlexpr_of_constr: TODO" let mlexpr_of_occ_constr = diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index e84864f96..78ffda215 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -77,15 +77,15 @@ type ('hyp,'constr,'pat,'tac) gen_proof_instr= type raw_proof_instr = - ((identifier*(Topconstr.constr_expr option)) located, - Topconstr.constr_expr, - Topconstr.cases_pattern_expr, + ((identifier*(Constrexpr.constr_expr option)) located, + Constrexpr.constr_expr, + Constrexpr.cases_pattern_expr, raw_tactic_expr) gen_proof_instr type glob_proof_instr = ((identifier*(Genarg.glob_constr_and_expr option)) located, Genarg.glob_constr_and_expr, - Topconstr.cases_pattern_expr, + Constrexpr.cases_pattern_expr, Tacexpr.glob_tactic_expr) gen_proof_instr type proof_pattern = @@ -94,7 +94,7 @@ type proof_pattern = pat_constr: Term.constr; pat_typ: Term.types; pat_pat: Glob_term.cases_pattern; - pat_expr: Topconstr.cases_pattern_expr} + pat_expr: Constrexpr.cases_pattern_expr} type proof_instr = (Term.constr statement, diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 58111f597..7c097c6d6 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -9,7 +9,7 @@ open Errors open Util open Names -open Topconstr +open Constrexpr open Tacinterp open Tacmach open Decl_expr diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 045678f0c..83beece26 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -192,7 +192,7 @@ GLOBAL: proof_instr; statement : [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c} | i=ident -> {st_label=Anonymous; - st_it=Topconstr.CRef (Libnames.Ident (loc, i))} + st_it=Constrexpr.CRef (Libnames.Ident (loc, i))} | c=constr -> {st_label=Anonymous;st_it=c} ]]; constr_or_thesis : @@ -205,7 +205,7 @@ GLOBAL: proof_instr; | [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot} | i=ident -> {st_label=Anonymous; - st_it=This (Topconstr.CRef (Libnames.Ident (loc, i)))} + st_it=This (Constrexpr.CRef (Libnames.Ident (loc, i)))} | c=constr -> {st_label=Anonymous;st_it=This c} ] ]; diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index aed71c3ae..2047b5326 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -10,7 +10,7 @@ open Util open Term open Names open Pp -open Topconstr +open Constrexpr open Indfun_common open Indfun open Genarg diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index ccf2caaf5..95c6a6d99 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1256,13 +1256,13 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b let rec rebuild_return_type rt = match rt with - | Topconstr.CProdN(loc,n,t') -> - Topconstr.CProdN(loc,n,rebuild_return_type t') - | Topconstr.CLetIn(loc,na,t,t') -> - Topconstr.CLetIn(loc,na,t,rebuild_return_type t') - | _ -> Topconstr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous], - Topconstr.Default Decl_kinds.Explicit,rt], - Topconstr.CSort(dummy_loc,GType None)) + | Constrexpr.CProdN(loc,n,t') -> + Constrexpr.CProdN(loc,n,rebuild_return_type t') + | Constrexpr.CLetIn(loc,na,t,t') -> + Constrexpr.CLetIn(loc,na,t,rebuild_return_type t') + | _ -> Constrexpr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous], + Constrexpr.Default Decl_kinds.Explicit,rt], + Constrexpr.CSort(dummy_loc,GType None)) let do_build_inductive @@ -1302,10 +1302,10 @@ let do_build_inductive (fun (n,t,is_defined) acc -> if is_defined then - Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, + Constrexpr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, acc) else - Topconstr.CProdN + Constrexpr.CProdN (dummy_loc, [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], acc @@ -1368,10 +1368,10 @@ let do_build_inductive (fun (n,t,is_defined) acc -> if is_defined then - Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, + Constrexpr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, acc) else - Topconstr.CProdN + Constrexpr.CProdN (dummy_loc, [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], acc @@ -1390,9 +1390,9 @@ let do_build_inductive (fun (n,t,is_defined) -> if is_defined then - Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t) + Constrexpr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t) else - Topconstr.LocalRawAssum + Constrexpr.LocalRawAssum ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t) ) rels_params diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index 5c91292ba..b8e7b3ab4 100644 --- a/plugins/funind/glob_term_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli @@ -10,7 +10,7 @@ val build_inductive : Names.identifier list -> (* The list of function name *) (Names.name*Glob_term.glob_constr*bool) list list -> (* The list of function args *) - Topconstr.constr_expr list -> (* The list of function returned type *) + Constrexpr.constr_expr list -> (* The list of function returned type *) Glob_term.glob_constr list -> (* the list of body *) unit diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 1c2509f6e..2eb2fb3ed 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -130,8 +130,8 @@ let functional_induction with_clean c princl pat = let rec abstract_glob_constr c = function | [] -> c - | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_glob_constr c bl) - | Topconstr.LocalRawAssum (idl,k,t)::bl -> + | Constrexpr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_glob_constr c bl) + | Constrexpr.LocalRawAssum (idl,k,t)::bl -> List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl (abstract_glob_constr c bl) @@ -220,8 +220,8 @@ let rec is_rec names = let rec local_binders_length = function (* Assume that no `{ ... } contexts occur *) | [] -> 0 - | Topconstr.LocalRawDef _::bl -> 1 + local_binders_length bl - | Topconstr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl + | Constrexpr.LocalRawDef _::bl -> 1 + local_binders_length bl + | Constrexpr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl let prepare_body ((name,_,args,types,_),_) rt = let n = local_binders_length args in @@ -395,7 +395,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas in let unbounded_eq = let f_app_args = - Topconstr.CAppExpl + Constrexpr.CAppExpl (dummy_loc, (None,(Ident (dummy_loc,fname))) , (List.map @@ -407,7 +407,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - Topconstr.CApp (dummy_loc,(None,Topconstr.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))), + Constrexpr.CApp (dummy_loc,(None,Topconstr.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))), [(f_app_args,None);(body,None)]) in let eq = Topconstr.prod_constr_expr unbounded_eq args in @@ -439,7 +439,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> begin match args with - | [Topconstr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x + | [Constrexpr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x | _ -> error "Recursive argument must be specified" end | Some wf_args -> @@ -447,7 +447,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas match List.find (function - | Topconstr.LocalRawAssum(l,k,t) -> + | Constrexpr.LocalRawAssum(l,k,t) -> List.exists (function (_,Name id) -> id = wf_args | _ -> false) l @@ -455,7 +455,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas ) args with - | Topconstr.LocalRawAssum(_,k,t) -> t,wf_args + | Constrexpr.LocalRawAssum(_,k,t) -> t,wf_args | _ -> assert false with Not_found -> assert false in @@ -482,7 +482,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas let b = Names.id_of_string "___b" in Topconstr.mkLambdaC( [dummy_loc,Name a;dummy_loc,Name b], - Topconstr.Default Explicit, + Constrexpr.Default Explicit, wf_arg_type, Topconstr.mkAppC(wf_rel_expr, [ @@ -505,23 +505,23 @@ let decompose_lambda_n_assum_constr_expr = if n = 0 then (List.rev acc,e) else match e with - | Topconstr.CLambdaN(_, [],e') -> decompose_lambda_n_assum_constr_expr acc n e' - | Topconstr.CLambdaN(lambda_loc,(nal,bk,nal_type)::bl,e') -> + | Constrexpr.CLambdaN(_, [],e') -> decompose_lambda_n_assum_constr_expr acc n e' + | Constrexpr.CLambdaN(lambda_loc,(nal,bk,nal_type)::bl,e') -> let nal_length = List.length nal in if nal_length <= n then decompose_lambda_n_assum_constr_expr - (Topconstr.LocalRawAssum(nal,bk,nal_type)::acc) + (Constrexpr.LocalRawAssum(nal,bk,nal_type)::acc) (n - nal_length) - (Topconstr.CLambdaN(lambda_loc,bl,e')) + (Constrexpr.CLambdaN(lambda_loc,bl,e')) else let nal_keep,nal_expr = list_chop n nal in - (List.rev (Topconstr.LocalRawAssum(nal_keep,bk,nal_type)::acc), - Topconstr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e') + (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc), + Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e') ) - | Topconstr.CLetIn(_, na,nav,e') -> + | Constrexpr.CLetIn(_, na,nav,e') -> decompose_lambda_n_assum_constr_expr - (Topconstr.LocalRawDef(na,nav)::acc) (pred n) e' + (Constrexpr.LocalRawDef(na,nav)::acc) (pred n) e' | _ -> error "Not enough product or assumption" in decompose_lambda_n_assum_constr_expr [] @@ -535,29 +535,30 @@ let decompose_prod_n_assum_constr_expr = (List.rev acc,e) else match e with - | Topconstr.CProdN(_, [],e') -> decompose_prod_n_assum_constr_expr acc n e' - | Topconstr.CProdN(lambda_loc,(nal,bk,nal_type)::bl,e') -> + | Constrexpr.CProdN(_, [],e') -> decompose_prod_n_assum_constr_expr acc n e' + | Constrexpr.CProdN(lambda_loc,(nal,bk,nal_type)::bl,e') -> let nal_length = List.length nal in if nal_length <= n then (* let _ = Pp.msgnl (str "first case") in *) decompose_prod_n_assum_constr_expr - (Topconstr.LocalRawAssum(nal,bk,nal_type)::acc) + (Constrexpr.LocalRawAssum(nal,bk,nal_type)::acc) (n - nal_length) - (if bl = [] then e' else (Topconstr.CLambdaN(lambda_loc,bl,e'))) + (if bl = [] then e' else (Constrexpr.CLambdaN(lambda_loc,bl,e'))) else (* let _ = Pp.msgnl (str "second case") in *) let nal_keep,nal_expr = list_chop n nal in - (List.rev (Topconstr.LocalRawAssum(nal_keep,bk,nal_type)::acc), - Topconstr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e') + (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc), + Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e') ) - | Topconstr.CLetIn(_, na,nav,e') -> + | Constrexpr.CLetIn(_, na,nav,e') -> decompose_prod_n_assum_constr_expr - (Topconstr.LocalRawDef(na,nav)::acc) (pred n) e' + (Constrexpr.LocalRawDef(na,nav)::acc) (pred n) e' | _ -> error "Not enough product or assumption" in decompose_prod_n_assum_constr_expr [] +open Constrexpr open Topconstr let rec make_assoc = List.fold_left2 (fun l a b -> @@ -569,10 +570,10 @@ match a, b with let rec rebuild_bl (aux,assoc) bl typ = match bl,typ with | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc) - | (Topconstr.LocalRawAssum(nal,bk,_))::bl',typ -> + | (Constrexpr.LocalRawAssum(nal,bk,_))::bl',typ -> rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ - | (Topconstr.LocalRawDef(na,_))::bl',CLetIn(_,_,nat,typ') -> - rebuild_bl ((Topconstr.LocalRawDef(na,replace_vars_constr_expr assoc nat)::aux),assoc) + | (Constrexpr.LocalRawDef(na,_))::bl',Constrexpr.CLetIn(_,_,nat,typ') -> + rebuild_bl ((Constrexpr.LocalRawDef(na,replace_vars_constr_expr assoc nat)::aux),assoc) bl' typ' | _ -> assert false and rebuild_nal (aux,assoc) bk bl' nal lnal typ = @@ -619,7 +620,7 @@ let do_generate_principle on_error register_built interactive_proof List.iter (fun (_,l) -> if l <> [] then error "Function does not support notations for now") fixpoint_exprl; let _is_struct = match fixpoint_exprl with - | [((_,(wf_x,Topconstr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] -> + | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] -> let ((((_,name),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e @@ -641,7 +642,7 @@ let do_generate_principle on_error register_built interactive_proof if register_built then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook; false - |[((_,(wf_x,Topconstr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] -> + |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] -> let ((((_,name),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e @@ -666,7 +667,7 @@ let do_generate_principle on_error register_built interactive_proof | _ -> List.iter (function ((_na,(_,ord),_args,_body,_type),_not) -> match ord with - | Topconstr.CMeasureRec _ | Topconstr.CWfRec _ -> + | Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _ -> error ("Cannot use mutual definition with well-founded recursion or measure") | _ -> () @@ -757,18 +758,18 @@ let rec add_args id new_args b = | CGeneralization _ -> anomaly "add_args : CGeneralization" | CPrim _ -> b | CDelimiters _ -> anomaly "add_args : CDelimiters" -exception Stop of Topconstr.constr_expr +exception Stop of Constrexpr.constr_expr (* [chop_n_arrow n t] chops the [n] first arrows in [t] - Acts on Topconstr.constr_expr + Acts on Constrexpr.constr_expr *) let rec chop_n_arrow n t = if n <= 0 then t (* If we have already removed all the arrows then return the type *) else (* If not we check the form of [t] *) match t with - | Topconstr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible : + | Constrexpr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible : either we need to discard more than the number of arrows contained in this product declaration then we just recall [chop_n_arrow] on the remaining number of arrow to chop and [t'] we discard it and @@ -787,7 +788,7 @@ let rec chop_n_arrow n t = aux (n - nal_l) nal_ta' else let new_t' = - Topconstr.CProdN(dummy_loc, + Constrexpr.CProdN(dummy_loc, ((snd (list_chop n nal)),k,t'')::nal_ta',t') in raise (Stop new_t') @@ -800,10 +801,10 @@ let rec chop_n_arrow n t = | _ -> anomaly "Not enough products" -let rec get_args b t : Topconstr.local_binder list * - Topconstr.constr_expr * Topconstr.constr_expr = +let rec get_args b t : Constrexpr.local_binder list * + Constrexpr.constr_expr * Constrexpr.constr_expr = match b with - | Topconstr.CLambdaN (loc, (nal_ta), b') -> + | Constrexpr.CLambdaN (loc, (nal_ta), b') -> begin let n = (List.fold_left (fun n (nal,_,_) -> @@ -811,7 +812,7 @@ let rec get_args b t : Topconstr.local_binder list * in let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in (List.map (fun (nal,k,ta) -> - (Topconstr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' + (Constrexpr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' end | _ -> [],b,t @@ -845,7 +846,7 @@ let make_graph (f_ref:global_reference) = let (nal_tas,b,t) = get_args extern_body extern_type in let expr_list = match b with - | Topconstr.CFix(loc,l_id,fixexprl) -> + | Constrexpr.CFix(loc,l_id,fixexprl) -> let l = List.map (fun (id,(n,recexp),bl,t,b) -> @@ -854,8 +855,8 @@ let make_graph (f_ref:global_reference) = List.flatten (List.map (function - | Topconstr.LocalRawDef (na,_)-> [] - | Topconstr.LocalRawAssum (nal,_,_) -> + | Constrexpr.LocalRawDef (na,_)-> [] + | Constrexpr.LocalRawAssum (nal,_,_) -> List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n))) @@ -872,7 +873,7 @@ let make_graph (f_ref:global_reference) = l | _ -> let id = id_of_label (con_label c) in - [((dummy_loc,id),(None,Topconstr.CStructRec),nal_tas,t,Some b),[]] + [((dummy_loc,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in do_generate_principle error_error false false expr_list; (* We register the infos *) diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 0ec5f7bce..4ca23a295 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -13,7 +13,7 @@ open Tactics open Indfun_common open Errors open Util -open Topconstr +open Constrexpr open Vernacexpr open Pp open Names diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index aa4493821..1117e2597 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -10,11 +10,11 @@ val recursive_definition : bool -> Names.identifier -> Constrintern.internalization_env -> - Topconstr.constr_expr -> - Topconstr.constr_expr -> - int -> Topconstr.constr_expr -> (Names.constant -> + Constrexpr.constr_expr -> + Constrexpr.constr_expr -> + int -> Constrexpr.constr_expr -> (Names.constant -> Term.constr option ref -> Names.constant -> - Names.constant -> int -> Term.types -> int -> Term.constr -> 'a) -> Topconstr.constr_expr list -> unit + Names.constant -> int -> Term.types -> int -> Term.constr -> 'a) -> Constrexpr.constr_expr list -> unit diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index a74666fdd..590776760 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -738,11 +738,11 @@ type ring_mod = | Const_tac of cst_tac_spec | Pre_tac of raw_tactic_expr | Post_tac of raw_tactic_expr - | Setoid of Topconstr.constr_expr * Topconstr.constr_expr - | Pow_spec of cst_tac_spec * Topconstr.constr_expr + | Setoid of Constrexpr.constr_expr * Constrexpr.constr_expr + | Pow_spec of cst_tac_spec * Constrexpr.constr_expr (* Syntaxification tactic , correctness lemma *) - | Sign_spec of Topconstr.constr_expr - | Div_spec of Topconstr.constr_expr + | Sign_spec of Constrexpr.constr_expr + | Div_spec of Constrexpr.constr_expr VERNAC ARGUMENT EXTEND ring_mod @@ -1096,7 +1096,7 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi type field_mod = Ring_mod of ring_mod - | Inject of Topconstr.constr_expr + | Inject of Constrexpr.constr_expr VERNAC ARGUMENT EXTEND field_mod | [ ring_mod(m) ] -> [ Ring_mod m ] diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 6429116de..a5ba7e98a 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -15,7 +15,7 @@ open Evd open Environ open Nametab open Mod_subst -open Topconstr +open Constrexpr open Compat open Pp open Util diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 3feb652ae..45857df40 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -14,7 +14,7 @@ open Evd open Environ open Nametab open Mod_subst -open Topconstr +open Constrexpr open Errors open Pp open Libnames diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 8e7c07135..45ec59ef0 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -20,6 +20,6 @@ val w_refine : evar * evar_info -> glob_constr_ltac_closure -> evar_map -> evar_map val instantiate_pf_com : - Evd.evar -> Topconstr.constr_expr -> Evd.evar_map -> Evd.evar_map + Evd.evar -> Constrexpr.constr_expr -> Evd.evar_map -> Evd.evar_map (** the instantiate tactic was moved to [tactics/evar_tactics.ml] *) diff --git a/proofs/goal.mli b/proofs/goal.mli index d67a6b12f..acda9031b 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -55,7 +55,7 @@ val return : 'a -> 'a sensitive (* spiwack: it is a wrapper around [Constrintern.interp_open_constr]. In an ideal world, this could/should be the other way round. As of now, though, it seems at least quite useful to build tactics. *) -val interp_constr : Topconstr.constr_expr -> Term.constr sensitive +val interp_constr : Constrexpr.constr_expr -> Term.constr sensitive (* Type of constr with holes used by refine. *) type refinable diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index a271fb336..9b92893a7 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -162,7 +162,7 @@ val by : tactic -> unit UserError if no proof is focused or if there is no such [n]th existential variable *) -val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit +val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit (** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *) diff --git a/proofs/proof.mli b/proofs/proof.mli index 715b3341b..e162a2aa0 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -187,5 +187,5 @@ module V82 : sig val grab_evars : proof -> unit (* Implements the Existential command *) - val instantiate_evar : int -> Topconstr.constr_expr -> proof -> unit + val instantiate_evar : int -> Constrexpr.constr_expr -> proof -> unit end diff --git a/proofs/proofview.mli b/proofs/proofview.mli index fe24b54b3..1ae5c4fd2 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -210,7 +210,7 @@ module V82 : sig val top_evars : proofview -> Evd.evar list (* Implements the Existential command *) - val instantiate_evar : int -> Topconstr.constr_expr -> proofview -> proofview + val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview (* spiwack: [purify] might be useful while writing tactics manipulating exception explicitely or from the [V82] submodule (neither being advised, though *) diff --git a/tactics/auto.ml b/tactics/auto.ml index f167a91a3..f580f839c 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -825,7 +825,7 @@ let prepare_hint env (sigma,c) = let path_of_constr_expr c = match c with - | Topconstr.CRef r -> (try PathHints [global r] with _ -> PathAny) + | Constrexpr.CRef r -> (try PathHints [global r] with _ -> PathAny) | _ -> PathAny let interp_hints h = diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index 5d3691b54..ee4f38c9d 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -10,7 +10,7 @@ open Tacexpr open Term open Names open Proof_type -open Topconstr +open Constrexpr open Termops open Glob_term open Misctypes diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 21fcc0f5d..fc72bd4e4 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -3,7 +3,7 @@ open Names open Term open Glob_term open Proof_type -open Topconstr +open Constrexpr open Misctypes val lemInv_gen : quantified_hypothesis -> constr -> tactic diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 04a1734fb..4a0d143dc 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -32,7 +32,7 @@ open Hiddentac open Typeclasses open Typeclasses_errors open Classes -open Topconstr +open Constrexpr open Pfedit open Command open Libnames diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 8e68d8e70..88767a363 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -32,6 +32,7 @@ open Proof_type open Refiner open Tacmach open Tactic_debug +open Constrexpr open Topconstr open Term open Termops diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 861dcb97c..35e0c456b 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -16,7 +16,7 @@ open Tactic_debug open Term open Tacexpr open Genarg -open Topconstr +open Constrexpr open Mod_subst open Redexpr open Misctypes diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 40bcb94c9..5cf460366 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -118,7 +118,7 @@ val assumption : tactic val exact_no_check : constr -> tactic val vm_cast_no_check : constr -> tactic val exact_check : constr -> tactic -val exact_proof : Topconstr.constr_expr -> tactic +val exact_proof : Constrexpr.constr_expr -> tactic (** {6 Reduction tactics. } *) diff --git a/toplevel/classes.ml b/toplevel/classes.ml index b3b9efcef..593276589 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -24,7 +24,7 @@ open Typeclasses open Libnames open Constrintern open Glob_term -open Topconstr +open Constrexpr (*i*) open Decl_kinds diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 424645fe8..4ac722eb2 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -14,7 +14,7 @@ open Evd open Environ open Nametab open Mod_subst -open Topconstr +open Constrexpr open Errors open Util open Typeclasses diff --git a/toplevel/command.ml b/toplevel/command.ml index ecc4e6995..a1d6eecf2 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -19,6 +19,7 @@ open Declare open Names open Libnames open Nameops +open Constrexpr open Topconstr open Constrintern open Nametab diff --git a/toplevel/command.mli b/toplevel/command.mli index 3cced65f1..005a4a33a 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -13,7 +13,7 @@ open Entries open Libnames open Tacexpr open Vernacexpr -open Topconstr +open Constrexpr open Decl_kinds open Redexpr open Constrintern diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 00592848f..78aa3fd12 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -29,7 +29,7 @@ open Namegen open Evd open Evarutil open Reductionops -open Topconstr +open Constrexpr open Constrintern open Impargs open Tacticals diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli index 35d6aaa26..1c1465046 100644 --- a/toplevel/lemmas.mli +++ b/toplevel/lemmas.mli @@ -9,7 +9,7 @@ open Names open Term open Decl_kinds -open Topconstr +open Constrexpr open Tacexpr open Vernacexpr open Proof_type diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 54de06c9c..5a305ccc9 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -12,6 +12,8 @@ open Compat open Errors open Util open Names +open Constrexpr +open Notation_term open Topconstr open Ppextend open Extend @@ -842,7 +844,7 @@ let check_rule_productivity l = error "A recursive notation must start with at least one symbol." let is_not_printable = function - | AVar _ -> warning "This notation will not be used for printing as it is bound to a \nsingle variable"; true + | NVar _ -> warning "This notation will not be used for printing as it is bound to a \nsingle variable"; true | _ -> false let find_precedence lev etyps symbols = @@ -1065,7 +1067,7 @@ let add_notation_in_scope local df c mods scope = (* Prepare the interpretation *) let (onlyparse,recvars,mainvars,df') = i_data in let i_vars = make_internalization_vars recvars mainvars i_typs in - let (acvars,ac) = interp_aconstr i_vars recvars c in + let (acvars,ac) = interp_notation_constr i_vars recvars c in let a = (make_interpretation_vars recvars acvars,ac) in let onlyparse = onlyparse or is_not_printable ac in (* Ready to change the global state *) @@ -1086,7 +1088,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) let path = (Lib.library_dp(),Lib.current_dirpath true) in let df' = (make_notation_key symbs,(path,df)) in let i_vars = make_internalization_vars recvars mainvars i_typs in - let (acvars,ac) = interp_aconstr ~impls i_vars recvars c in + let (acvars,ac) = interp_notation_constr ~impls i_vars recvars c in let a = (make_interpretation_vars recvars acvars,ac) in let onlyparse = onlyparse or is_not_printable ac in Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df')); @@ -1191,10 +1193,10 @@ let try_interp_name_alias = function let add_syntactic_definition ident (vars,c) local onlyparse = let vars,pat = - try [], ARef (try_interp_name_alias (vars,c)) + try [], NRef (try_interp_name_alias (vars,c)) with Not_found -> let i_vars = List.map (fun id -> (id,NtnInternTypeConstr)) vars in - let vars,pat = interp_aconstr i_vars [] c in + let vars,pat = interp_notation_constr i_vars [] c in List.map (fun (id,(sc,kind)) -> (id,sc)) vars, pat in let onlyparse = onlyparse or is_not_printable pat in diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index e2a3e33a2..b7651edec 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -15,7 +15,8 @@ open Extend open Tacexpr open Vernacexpr open Notation -open Topconstr +open Constrexpr +open Notation_term val add_token_obj : string -> unit diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index c6bb2c10a..4b26a979d 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -330,10 +330,10 @@ type obligation = type obligations = (obligation array * int) type fixpoint_kind = - | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list + | IsFixpoint of (identifier located option * Constrexpr.recursion_order_expr) list | IsCoFixpoint -type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list +type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list type program_info = { prg_name: identifier; @@ -342,7 +342,7 @@ type program_info = { prg_obligations: obligations; prg_deps : identifier list; prg_fixkind : fixpoint_kind option ; - prg_implicits : (Topconstr.explicitation * (bool * bool * bool)) list; + prg_implicits : (Constrexpr.explicitation * (bool * bool * bool)) list; prg_notations : notations ; prg_kind : definition_kind; prg_reduce : constr -> constr; diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index df093ea43..d052cc441 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -70,21 +70,22 @@ val set_proofs_transparency : bool -> unit (* true = All transparent, false = Op val get_proofs_transparency : unit -> bool val add_definition : Names.identifier -> ?term:Term.constr -> Term.types -> - ?implicits:(Topconstr.explicitation * (bool * bool * bool)) list -> + ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> ?tactic:Proof_type.tactic -> ?reduce:(Term.constr -> Term.constr) -> ?hook:(unit Tacexpr.declaration_hook) -> obligation_info -> progress -type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list +type notations = + (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list type fixpoint_kind = - | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list + | IsFixpoint of (identifier located option * Constrexpr.recursion_order_expr) list | IsCoFixpoint val add_mutual_definitions : (Names.identifier * Term.constr * Term.types * - (Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list -> + (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list -> ?tactic:Proof_type.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(Term.constr -> Term.constr) -> @@ -92,7 +93,7 @@ val add_mutual_definitions : notations -> fixpoint_kind -> unit -val obligation : int * Names.identifier option * Topconstr.constr_expr option -> +val obligation : int * Names.identifier option * Constrexpr.constr_expr option -> Tacexpr.raw_tactic_expr option -> unit val next_obligation : Names.identifier option -> Tacexpr.raw_tactic_expr option -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index c6f620ae5..f4ef35e01 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -25,6 +25,7 @@ open Safe_typing open Decl_kinds open Indtypes open Type_errors +open Constrexpr open Topconstr (********** definition d'un record (structure) **************) diff --git a/toplevel/record.mli b/toplevel/record.mli index 45670f1fa..e2d56cfd8 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -10,7 +10,7 @@ open Names open Term open Sign open Vernacexpr -open Topconstr +open Constrexpr open Impargs open Libnames diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6ac321e43..73c05de3f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -28,7 +28,7 @@ open Libnames open Nametab open Vernacexpr open Decl_kinds -open Topconstr +open Constrexpr open Pretyping open Redexpr open Syntax_def @@ -875,7 +875,7 @@ let vernac_reserve bl = let sb_decl = (fun (idl,c) -> let t = Constrintern.interp_type Evd.empty (Global.env()) c in let t = Detyping.detype false [] [] t in - let t = aconstr_of_glob_constr [] [] t in + let t = Topconstr.notation_constr_of_glob_constr [] [] t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 704f06fb5..2e33f7fd3 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -10,7 +10,7 @@ open Names open Term open Vernacinterp open Vernacexpr -open Topconstr +open Constrexpr open Misctypes (** Vernacular entries *) |