diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-08-29 19:05:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-04 11:28:49 +0200 |
| commit | 1db568d3dc88d538f975377bb4d8d3eecd87872c (patch) | |
| tree | d8e35952cc8f6111875e664d8884dc2c7f908206 | |
| parent | 3072bd9d080984833f5eb007bf15c6e9305619e3 (diff) | |
Making detyping potentially lazy.
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
53 files changed, 1279 insertions, 921 deletions
diff --git a/API/API.mli b/API/API.mli index d1774afe5..02ae86c77 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3072,55 +3072,67 @@ end (* XXX: Located manually from intf *) module Glob_term : sig - type cases_pattern_r = + type 'a cases_pattern_r = | PatVar of Names.Name.t - | PatCstr of Names.constructor * cases_pattern list * Names.Name.t - and cases_pattern = cases_pattern_r CAst.t + | PatCstr of Names.constructor * 'a cases_pattern_g list * Names.Name.t + and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t + type cases_pattern = [ `any ] cases_pattern_g type existential_name = Names.Id.t - type glob_constr_r = + type 'a glob_constr_r = | GRef of Globnames.global_reference * Misctypes.glob_level list option (** An identifier that represents a reference to an object defined either in the (global) environment or in the (local) context. *) | GVar of Names.Id.t (** An identifier that cannot be regarded as "GRef". Bound variables are typically represented this way. *) - | GEvar of existential_name * (Names.Id.t * glob_constr) list + | GEvar of existential_name * (Names.Id.t * 'a glob_constr_g) list | GPatVar of Evar_kinds.matching_var_kind - | GApp of glob_constr * glob_constr list - | GLambda of Names.Name.t * Decl_kinds.binding_kind * glob_constr * glob_constr - | GProd of Names.Name.t * Decl_kinds.binding_kind * glob_constr * glob_constr - | GLetIn of Names.Name.t * glob_constr * glob_constr option * glob_constr - | GCases of Term.case_style * glob_constr option * tomatch_tuples * cases_clauses - | GLetTuple of Names.Name.t list * (Names.Name.t * glob_constr option) * glob_constr * glob_constr - | GIf of glob_constr * (Names.Name.t * glob_constr option) * glob_constr * glob_constr - | GRec of fix_kind * Names.Id.t array * glob_decl list array * - glob_constr array * glob_constr array + | GApp of 'a glob_constr_g * 'a glob_constr_g list + | GLambda of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g + | GProd of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g + | GLetIn of Names.Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g + | GCases of Term.case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g + | GLetTuple of Names.Name.t list * (Names.Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g + | GIf of 'a glob_constr_g * (Names.Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g + | GRec of 'a fix_kind_g * Names.Id.t array * 'a glob_decl_g list array * + 'a glob_constr_g array * 'a glob_constr_g array | GSort of Misctypes.glob_sort | GHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option - | GCast of glob_constr * glob_constr Misctypes.cast_type + | GCast of 'a glob_constr_g * 'a glob_constr_g Misctypes.cast_type - and glob_constr = glob_constr_r CAst.t + and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t - and glob_decl = Names.Name.t * Decl_kinds.binding_kind * glob_constr option * glob_constr + and 'a glob_decl_g = Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g option * 'a glob_constr_g - and fix_recursion_order = + and 'a fix_recursion_order_g = | GStructRec - | GWfRec of glob_constr - | GMeasureRec of glob_constr * glob_constr option + | GWfRec of 'a glob_constr_g + | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option - and fix_kind = - | GFix of ((int option * fix_recursion_order) array * int) + and 'a fix_kind_g = + | GFix of ((int option * 'a fix_recursion_order_g) array * int) | GCoFix of int - and predicate_pattern = + and 'a predicate_pattern_g = Names.Name.t * (Names.inductive * Names.Name.t list) Loc.located option - and tomatch_tuple = (glob_constr * predicate_pattern) + and 'a tomatch_tuple_g = ('a glob_constr_g * 'a predicate_pattern_g) - and tomatch_tuples = tomatch_tuple list + and 'a tomatch_tuples_g = 'a tomatch_tuple_g list - and cases_clause = (Names.Id.t list * cases_pattern list * glob_constr) Loc.located - and cases_clauses = cases_clause list + and 'a cases_clause_g = (Names.Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) Loc.located + and 'a cases_clauses_g = 'a cases_clause_g list + + type glob_constr = [ `any ] glob_constr_g + type tomatch_tuple = [ `any ] tomatch_tuple_g + type tomatch_tuples = [ `any ] tomatch_tuples_g + type cases_clause = [ `any ] cases_clause_g + type cases_clauses = [ `any ] cases_clauses_g + type glob_decl = [ `any ] glob_decl_g + type fix_kind = [ `any ] fix_kind_g + type predicate_pattern = [ `any ] predicate_pattern_g + type any_glob_constr = + | AnyGlobConstr : 'r glob_constr_g -> any_glob_constr (** A globalised term together with a closure representing the value of its free variables. Intended for use when these variables are taken @@ -3980,11 +3992,14 @@ end module Detyping : sig + type 'a delay = + | Now : 'a delay + | Later : [ `thunk ] delay val print_universes : bool ref val print_evar_arguments : bool ref - val detype : ?lax:bool -> bool -> Names.Id.t list -> Environ.env -> Evd.evar_map -> EConstr.constr -> Glob_term.glob_constr + val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.t list -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g val subst_glob_constr : Mod_subst.substitution -> Glob_term.glob_constr -> Glob_term.glob_constr - val set_detype_anonymous : (?loc:Loc.t -> int -> Glob_term.glob_constr) -> unit + val set_detype_anonymous : (?loc:Loc.t -> int -> Names.Id.t) -> unit end module Indrec : @@ -4181,7 +4196,7 @@ sig type cases_pattern_status = bool type required_module = Libnames.full_path * string list type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> Glob_term.glob_constr - type 'a prim_token_uninterpreter = Glob_term.glob_constr list * (Glob_term.glob_constr -> 'a option) * cases_pattern_status + type 'a prim_token_uninterpreter = Glob_term.glob_constr list * (Glob_term.any_glob_constr -> 'a option) * cases_pattern_status type delimiters = string type local_scopes = Notation_term.tmp_scope_name option * Notation_term.scope_name list type notation_location = (Names.DirPath.t * Names.DirPath.t) * string diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 4b3b44875..26901ac43 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -125,5 +125,5 @@ ######################################################################## # Bignums ######################################################################## -: ${bignums_CI_BRANCH:=master} -: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git} +: ${bignums_CI_BRANCH:=fix-thunk-printer} +: ${bignums_CI_GITURL:=https://github.com/ppedrot/bignums.git} diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e85415bed..f5eff693f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -298,7 +298,7 @@ let add_patt_for_params ind l = let add_cpatt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ PatVar Anonymous) l + Util.List.addn (Inductiveops.inductive_nparamdecls ind) (DAst.make @@ PatVar Anonymous) l let drop_implicits_in_patt cst nb_expl args = let impl_st = (implicits_of_global cst) in @@ -376,6 +376,10 @@ let pattern_printable_in_both_syntax (ind,_ as c) = (List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args) ) impl_st +let lift f c = + let loc = c.CAst.loc in + CAst.make ?loc (f ?loc (DAst.get c)) + (* Better to use extern_glob_constr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = try @@ -392,7 +396,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = extern_notation_pattern scopes vars pat (uninterp_cases_pattern_notations pat) with No_match -> - CAst.map_with_loc (fun ?loc -> function + lift (fun ?loc -> function | PatVar (Name id) -> CPatAtom (Some (Ident (loc,id))) | PatVar (Anonymous) -> CPatAtom None | PatCstr(cstrsp,args,na) -> @@ -482,7 +486,7 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function try if is_inactive_rule keyrule then raise No_match; let loc = t.loc in - match t.v with + match DAst.get t with | PatCstr (cstr,_,na) -> let p = apply_notation_to_pattern ?loc (ConstructRef cstr) (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in @@ -645,8 +649,12 @@ let extern_args extern env args = let map (arg, argscopes) = lazy (extern argscopes env arg) in List.map map args -let match_coercion_app = function - | {loc; v = GApp ({ v = GRef (r,_) },args)} -> Some (loc, r, 0, args) +let match_coercion_app c = match DAst.get c with + | GApp (r, args) -> + begin match DAst.get r with + | GRef (r,_) -> Some (c.CAst.loc, r, 0, args) + | _ -> None + end | _ -> None let rec remove_coercions inctx c = @@ -668,14 +676,20 @@ let rec remove_coercions inctx c = been confused with ordinary application or would have need a surrounding context and the coercion to funclass would have been made explicit to match *) - if List.is_empty l then a' else CAst.make ?loc @@ GApp (a',l) + if List.is_empty l then a' else DAst.make ?loc @@ GApp (a',l) | _ -> c with Not_found -> c) | _ -> c -let rec flatten_application = function - | {loc; v = GApp ({ v = GApp(a,l')},l)} -> flatten_application (CAst.make ?loc @@ GApp (a,l'@l)) - | a -> a +let rec flatten_application c = match DAst.get c with + | GApp (f, l) -> + begin match DAst.get f with + | GApp(a,l') -> + let loc = c.CAst.loc in + flatten_application (DAst.make ?loc @@ GApp (a,l'@l)) + | _ -> c + end + | a -> c (**********************************************************************) (* mapping glob_constr to numerals (in presence of coercions, choose the *) @@ -702,10 +716,12 @@ let extern_optimal_prim_token scopes r r' = let extended_glob_local_binder_of_decl loc = function | (p,bk,None,t) -> GLocalAssum (p,bk,t) - | (p,bk,Some x, { v = GHole ( _, Misctypes.IntroAnonymous, None) } ) -> GLocalDef (p,bk,x,None) - | (p,bk,Some x,t) -> GLocalDef (p,bk,x,Some t) + | (p,bk,Some x, t) -> + match DAst.get t with + | GHole (_, Misctypes.IntroAnonymous, None) -> GLocalDef (p,bk,x,None) + | _ -> GLocalDef (p,bk,x,Some t) -let extended_glob_local_binder_of_decl ?loc u = CAst.make ?loc (extended_glob_local_binder_of_decl loc u) +let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u) (**********************************************************************) (* mapping glob_constr to constr_expr *) @@ -730,7 +746,7 @@ let rec extern inctx scopes vars r = let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation scopes vars r'' (uninterp_notations r'') - with No_match -> CAst.map_with_loc (fun ?loc -> function + with No_match -> lift (fun ?loc -> function | GRef (ref,us) -> extern_global (select_stronger_impargs (implicits_of_global ref)) (extern_reference ?loc vars ref) (extern_universes us) @@ -749,8 +765,9 @@ let rec extern inctx scopes vars r = | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[])) | GApp (f,args) -> - (match f with - | {loc = rloc; v = GRef (ref,us) } -> + (match DAst.get f with + | GRef (ref,us) -> + let rloc = f.CAst.loc in let subscopes = find_arguments_scope ref in let args = fill_arg_scopes args subscopes (snd scopes) in begin @@ -825,8 +842,8 @@ let rec extern inctx scopes vars r = (cases_predicate_names tml) vars in let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> - let na' = match na,tm with - | Anonymous, { v = GVar id } -> + let na' = match na, DAst.get tm with + | Anonymous, GVar id -> begin match rtntypopt with | None -> None | Some ntn -> @@ -835,12 +852,12 @@ let rec extern inctx scopes vars r = else None end | Anonymous, _ -> None - | Name id, { v = GVar id' } when Id.equal id id' -> None + | Name id, GVar id' when Id.equal id id' -> None | Name _, _ -> Some (Loc.tag na) in (sub_extern false scopes vars tm, na', Option.map (fun (loc,(ind,nal)) -> - let args = List.map (fun x -> CAst.make @@ PatVar x) nal in + let args = List.map (fun x -> DAst.make @@ PatVar x) nal in let fullargs = add_cpatt_for_params ind args in extern_ind_pattern_in_scope scopes vars ind fullargs ) x)) @@ -931,14 +948,16 @@ and factorize_lambda inctx scopes vars na bk aty c = and extern_local_binder scopes vars = function [] -> ([],[],[]) - | { v = GLocalDef (na,bk,bd,ty)}::l -> + | b :: l -> + match DAst.get b with + | GLocalDef (na,bk,bd,ty) -> let (assums,ids,l) = extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in (assums,na::ids, CLocalDef((Loc.tag na), extern false scopes vars bd, Option.map (extern false scopes vars) ty) :: l) - | { v = GLocalAssum (na,bk,ty)}::l -> + | GLocalAssum (na,bk,ty) -> let ty = extern_typ scopes vars ty in (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) @@ -951,7 +970,7 @@ and extern_local_binder scopes vars = function (na::assums,na::ids, CLocalAssum([(Loc.tag na)],Default bk,ty) :: l)) - | { v = GLocalPattern ((p,_),_,bk,ty)}::l -> + | GLocalPattern ((p,_),_,bk,ty) -> let ty = if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in let p = extern_cases_pattern vars p in @@ -969,12 +988,12 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function try if is_inactive_rule keyrule then raise No_match; (* Adjusts to the number of arguments expected by the notation *) - let (t,args,argsscopes,argsimpls) = match t.v ,n with + let (t,args,argsscopes,argsimpls) = match DAst.get t ,n with | GApp (f,args), Some n when List.length args >= n -> let args1, args2 = List.chop n args in let subscopes, impls = - match f.v with + match DAst.get f with | GRef (ref,us) -> let subscopes = try List.skipn n (find_arguments_scope ref) @@ -987,15 +1006,19 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function subscopes,impls | _ -> [], [] in - (if Int.equal n 0 then f else CAst.make @@ GApp (f,args1)), + (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)), args2, subscopes, impls - | GApp ({ v = GRef (ref,us) } as f, args), None -> + | GApp (f, args), None -> + begin match DAst.get f with + | GRef (ref,us) -> let subscopes = find_arguments_scope ref in let impls = select_impargs_size (List.length args) (implicits_of_global ref) in f, args, subscopes, impls - | GRef (ref,us), Some 0 -> CAst.make @@ GApp (t,[]), [], [], [] + | _ -> t, [], [], [] + end + | GRef (ref,us), Some 0 -> DAst.make @@ GApp (t,[]), [], [], [] | _, None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) @@ -1065,7 +1088,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t = (* those goal/section/rel variables that occurs in the subterm under *) (* consideration; see namegen.ml for further details *) let avoid = if goal_concl_style then ids_of_context env else [] in - let r = Detyping.detype ~lax:lax goal_concl_style avoid env sigma t in + let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in let vars = vars_of_env env in extern false (scopt,[]) vars r @@ -1077,7 +1100,7 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t = let extern_type goal_concl_style env sigma t = let avoid = if goal_concl_style then ids_of_context env else [] in - let r = Detyping.detype goal_concl_style avoid env sigma t in + let r = Detyping.detype Detyping.Later goal_concl_style avoid env sigma t in extern_glob_type (vars_of_env env) r let extern_sort sigma s = extern_glob_sort (detype_sort sigma s) @@ -1095,9 +1118,9 @@ let extern_closed_glob ?lax goal_concl_style env sigma t = let any_any_branch = (* | _ => _ *) - Loc.tag ([],[CAst.make @@ PatVar Anonymous], CAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) + Loc.tag ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) -let rec glob_of_pat env sigma pat = CAst.make @@ match pat with +let rec glob_of_pat env sigma pat = DAst.make @@ match pat with | PRef ref -> GRef (ref,None) | PVar id -> GVar id | PEvar (evk,l) -> @@ -1117,12 +1140,12 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with GVar id | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n) - | PProj (p,c) -> GApp (CAst.make @@ GRef (ConstRef (Projection.constant p),None), + | PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None), [glob_of_pat env sigma c]) | PApp (f,args) -> GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args) | PSoApp (n,args) -> - GApp (CAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n), + GApp (DAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n), List.map (glob_of_pat env sigma) args) | PProd (na,t,c) -> GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) @@ -1154,15 +1177,15 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.") in GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat) - | PFix f -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))).v (** FIXME bad env *) - | PCoFix c -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))).v + | PFix f -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *) + | PCoFix c -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))) | PSort s -> GSort s let extern_constr_pattern env sigma pat = extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat) let extern_rel_context where env sigma sign = - let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in + let a = detype_rel_context Detyping.Later where [] (names_of_rel_context env,env) sigma sign in let vars = vars_of_env env in let a = List.map (extended_glob_local_binder_of_decl) a in pi3 (extern_local_binder (None,[]) vars a) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index ffa891c50..593580fb7 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -23,9 +23,9 @@ open Misctypes (** Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing *) -val extern_cases_pattern : Id.Set.t -> cases_pattern -> cases_pattern_expr -val extern_glob_constr : Id.Set.t -> glob_constr -> constr_expr -val extern_glob_type : Id.Set.t -> glob_constr -> constr_expr +val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr +val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr +val extern_glob_type : Id.Set.t -> 'a glob_constr_g -> constr_expr val extern_constr_pattern : names_context -> Evd.evar_map -> constr_pattern -> constr_expr val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob_constr -> constr_expr diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e465677cd..6f7c6c827 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -15,7 +15,6 @@ open Namegen open Libnames open Globnames open Impargs -open CAst open Glob_term open Glob_ops open Patternops @@ -306,12 +305,12 @@ let reset_tmp_scope env = {env with tmp_scope = None} let rec it_mkGProd ?loc env body = match env with - (loc2, (na, bk, t)) :: tl -> it_mkGProd ?loc:loc2 tl (CAst.make ?loc:(Loc.merge_opt loc loc2) @@ GProd (na, bk, t, body)) + (loc2, (na, bk, t)) :: tl -> it_mkGProd ?loc:loc2 tl (DAst.make ?loc:(Loc.merge_opt loc loc2) @@ GProd (na, bk, t, body)) | [] -> body let rec it_mkGLambda ?loc env body = match env with - (loc2, (na, bk, t)) :: tl -> it_mkGLambda ?loc:loc2 tl (CAst.make ?loc:(Loc.merge_opt loc loc2) @@ GLambda (na, bk, t, body)) + (loc2, (na, bk, t)) :: tl -> it_mkGLambda ?loc:loc2 tl (DAst.make ?loc:(Loc.merge_opt loc loc2) @@ GLambda (na, bk, t, body)) | [] -> body (**********************************************************************) @@ -323,15 +322,15 @@ let build_impls = function |Explicit -> fun _ -> None let impls_type_list ?(args = []) = - let rec aux acc = function - | { v = GProd (na,bk,_,c) } -> aux ((build_impls bk na)::acc) c + let rec aux acc c = match DAst.get c with + | GProd (na,bk,_,c) -> aux ((build_impls bk na)::acc) c | _ -> (Variable,[],List.append args (List.rev acc),[]) in aux [] let impls_term_list ?(args = []) = - let rec aux acc = function - | { v = GLambda (na,bk,_,c) } -> aux ((build_impls bk na)::acc) c - | { v = GRec (fix_kind, nas, args, tys, bds) } -> + let rec aux acc c = match DAst.get c with + | GLambda (na,bk,_,c) -> aux ((build_impls bk na)::acc) c + | GRec (fix_kind, nas, args, tys, bds) -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in let acc' = List.fold_left (fun a (na, bk, _, _) -> (build_impls bk na)::a) acc args.(nb) in aux acc' bds.(nb) @@ -347,14 +346,14 @@ let rec check_capture ty = function | [] -> () -let locate_if_hole ?loc na = function - | { v = GHole (_,naming,arg) } -> +let locate_if_hole ?loc na c = match DAst.get c with + | GHole (_,naming,arg) -> (try match na with | Name id -> glob_constr_of_notation_constr ?loc (Reserve.find_reserved_type id) | Anonymous -> raise Not_found - with Not_found -> CAst.make ?loc @@ GHole (Evar_kinds.BinderType na, naming, arg)) - | x -> x + with Not_found -> DAst.make ?loc @@ GHole (Evar_kinds.BinderType na, naming, arg)) + | _ -> c let reset_hidden_inductive_implicit_test env = { env with impls = Id.Map.map (function @@ -400,7 +399,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar env fvs in let bl = List.map (fun (loc, id) -> - (loc, (Name id, b, CAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) + (loc, (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) fvs in let na = match na with @@ -433,11 +432,11 @@ let intern_assumption intern lvar env nal bk ty = let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in env, b -let glob_local_binder_of_extended = CAst.with_loc_val (fun ?loc -> function +let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function | GLocalAssum (na,bk,t) -> (na,bk,None,t) | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t) | GLocalDef (na,bk,c,None) -> - let t = CAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in + let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in (na,bk,Some c,t) | GLocalPattern (_,_,_,_) -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.") @@ -448,13 +447,13 @@ let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd" let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function | CLocalAssum(nal,bk,ty) -> let env, bl' = intern_assumption intern lvar env nal bk ty in - let bl' = List.map (fun (loc,(na,c,t)) -> CAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in + let bl' = List.map (fun (loc,(na,c,t)) -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in env, bl' @ bl | CLocalDef((loc,na as locna),def,ty) -> let term = intern env def in let ty = Option.map (intern env) ty in (push_name_env lvar (impls_term_list term) env locna, - (CAst.make ?loc @@ GLocalDef (na,Explicit,term,ty)) :: bl) + (DAst.make ?loc @@ GLocalDef (na,Explicit,term,ty)) :: bl) | CLocalPattern (loc,(p,ty)) -> let tyc = match ty with @@ -476,7 +475,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio let bk = Default Explicit in let _, bl' = intern_assumption intern lvar env [na] bk tyc in let _,(_,bk,t) = List.hd bl' in - (env, (CAst.make ?loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl) + (env, (DAst.make ?loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl) let intern_generalization intern env lvar loc bk ak c = let c = intern {env with unb = true} c in @@ -499,12 +498,12 @@ let intern_generalization intern env lvar loc bk ak c = in if pi then (fun (loc', id) acc -> - CAst.make ?loc:(Loc.merge_opt loc' loc) @@ - GProd (Name id, bk, CAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) + DAst.make ?loc:(Loc.merge_opt loc' loc) @@ + GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) else (fun (loc', id) acc -> - CAst.make ?loc:(Loc.merge_opt loc' loc) @@ - GLambda (Name id, bk, CAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) + DAst.make ?loc:(Loc.merge_opt loc' loc) @@ + GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) in List.fold_right (fun (loc, id as lid) (env, acc) -> let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in @@ -558,27 +557,34 @@ let make_letins = (fun a c -> match a with | loc, LPLetIn (na,b,t) -> - CAst.make ?loc @@ GLetIn(na,b,t,c) + DAst.make ?loc @@ GLetIn(na,b,t,c) | loc, LPCases ((cp,il),id) -> - let tt = (CAst.make ?loc @@ GVar id, (Name id,None)) in - CAst.make ?loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))])) + let tt = (DAst.make ?loc @@ GVar id, (Name id,None)) in + DAst.make ?loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))])) -let rec subordinate_letins letins = function +let rec subordinate_letins letins l = match l with + | bnd :: l -> + let loc = bnd.CAst.loc in + begin match DAst.get bnd with (* binders come in reverse order; the non-let are returned in reverse order together *) (* with the subordinated let-in in writing order *) - | { loc; v = GLocalDef (na,_,b,t) }::l -> + | GLocalDef (na,_,b,t) -> subordinate_letins ((Loc.tag ?loc @@ LPLetIn (na,b,t))::letins) l - | { loc; v = GLocalAssum (na,bk,t)}::l -> + | GLocalAssum (na,bk,t) -> let letins',rest = subordinate_letins [] l in letins',((loc,(na,bk,t)),letins)::rest - | { loc; v = GLocalPattern (u,id,bk,t)} :: l -> + | GLocalPattern (u,id,bk,t) -> subordinate_letins ((Loc.tag ?loc @@ LPCases (u,id))::letins) - ([CAst.make ?loc @@ GLocalAssum (Name id,bk,t)] @ l) + ([DAst.make ?loc @@ GLocalAssum (Name id,bk,t)] @ l) + end | [] -> letins,[] +let dmap_with_loc f n = + CAst.map_with_loc (fun ?loc c -> f ?loc (DAst.get_thunk c)) n + let terms_of_binders bl = - let rec term_of_pat pt = CAst.map_with_loc (fun ?loc -> function + let rec term_of_pat pt = dmap_with_loc (fun ?loc -> function | PatVar (Name id) -> CRef (Ident (loc,id), None) | PatVar (Anonymous) -> user_err Pp.(str "Cannot turn \"_\" into a term.") | PatCstr (c,l,_) -> @@ -586,12 +592,16 @@ let terms_of_binders bl = let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in - let rec extract_variables = function - | {loc; v = GLocalAssum (Name id,_,_)}::l -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l - | {loc; v = GLocalDef (Name id,_,_,_)}::l -> extract_variables l - | {loc; v = GLocalDef (Anonymous,_,_,_)}::l - | {loc; v = GLocalAssum (Anonymous,_,_)}::l -> user_err Pp.(str "Cannot turn \"_\" into a term.") - | {loc; v = GLocalPattern ((u,_),_,_,_)}::l -> term_of_pat u :: extract_variables l + let rec extract_variables l = match l with + | bnd :: l -> + let loc = bnd.CAst.loc in + begin match DAst.get bnd with + | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l + | GLocalDef (Name id,_,_,_) -> extract_variables l + | GLocalDef (Anonymous,_,_,_) + | GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.") + | GLocalPattern ((u,_),_,_,_) -> term_of_pat u :: extract_variables l + end | [] -> [] in extract_variables bl @@ -647,7 +657,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = let bindings = Id.Map.map mk_env terms in Some (Genintern.generic_substitute_notation bindings arg) in - CAst.make ?loc @@ GHole (knd, naming, arg) + DAst.make ?loc @@ GHole (knd, naming, arg) | NBinderList (x,y,iter,terminator) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) @@ -665,22 +675,22 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = let a,letins = snd (Option.get binderopt) in let e = make_letins letins (aux subst' infos c') in let (_loc,(na,bk,t)) = a in - CAst.make ?loc @@ GProd (na,bk,t,e) + DAst.make ?loc @@ GProd (na,bk,t,e) | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt -> let a,letins = snd (Option.get binderopt) in let (_loc,(na,bk,t)) = a in - CAst.make ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c')) + DAst.make ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c')) (* Two special cases to keep binder name synchronous with BinderType *) | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c') when Name.equal na na' -> let subinfos,na = traverse_binder subst avoid subinfos na in - let ty = CAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in - CAst.make ?loc @@ GProd (na,Explicit,ty,aux subst' subinfos c') + let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in + DAst.make ?loc @@ GProd (na,Explicit,ty,aux subst' subinfos c') | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c') when Name.equal na na' -> let subinfos,na = traverse_binder subst avoid subinfos na in - let ty = CAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in - CAst.make ?loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c') + let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in + DAst.make ?loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c') | t -> glob_constr_of_notation_constr_with_binders ?loc (traverse_binder subst avoid) (aux subst') subinfos t @@ -692,7 +702,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = intern {env with tmp_scope = scopt; scopes = subscopes @ env.scopes} a with Not_found -> - CAst.make ?loc ( + DAst.make ?loc ( try GVar (Id.Map.find id renaming) with Not_found -> @@ -732,7 +742,7 @@ let string_of_ty = function | Variable -> "var" let gvar (loc, id) us = match us with -| None -> CAst.make ?loc @@ GVar id +| None -> DAst.make ?loc @@ GVar id | Some _ -> user_err ?loc (str "Variable " ++ pr_id id ++ str " cannot have a universe instance") @@ -774,24 +784,27 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us = let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in Dumpglob.dump_reference ?loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var"; - CAst.make ?loc @@ GRef (ref, us), impls, scopes, [] + DAst.make ?loc @@ GRef (ref, us), impls, scopes, [] with e when CErrors.noncritical e -> (* [id] a goal variable *) gvar (loc,id) us, [], [], [] let find_appl_head_data c = - match c.v with + match DAst.get c with | GRef (ref,_) -> let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in c, impls, scopes, [] - | GApp ({ v = GRef (ref,_) },l) - when l != [] -> + | GApp (r, l) -> + begin match DAst.get r with + | GRef (ref,_) when l != [] -> let n = List.length l in let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in c, List.map (drop_first_implicits n) impls, List.skipn_at_least n scopes,[] + | _ -> c,[],[],[] + end | _ -> c,[],[],[] let error_not_enough_arguments ?loc = @@ -824,7 +837,7 @@ let intern_reference ref = (* Is it a global reference or a syntactic definition? *) let intern_qualid loc qid intern env lvar us args = match intern_extended_global_of_qualid (loc,qid) with - | TrueGlobal ref -> (CAst.make ?loc @@ GRef (ref, us)), true, args + | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args | SynDef sp -> let (ids,c) = Syntax_def.search_syntactic_definition sp in let nids = List.length ids in @@ -836,23 +849,32 @@ let intern_qualid loc qid intern env lvar us args = let infos = (Id.Map.empty, env) in let projapp = match c with NRef _ -> true | _ -> false in let c = instantiate_notation_constr loc intern lvar subst infos c in - let c = match us, c with - | None, _ -> c - | Some _, { loc; v = GRef (ref, None) } -> CAst.make ?loc @@ GRef (ref, us) - | Some _, { loc; v = GApp ({ loc = loc' ; v = GRef (ref, None) }, arg) } -> - CAst.make ?loc @@ GApp (CAst.make ?loc:loc' @@ GRef (ref, us), arg) - | Some _, _ -> + let loc = c.CAst.loc in + let err () = user_err ?loc (str "Notation " ++ pr_qualid qid - ++ str " cannot have a universe instance," - ++ str " its expanded head does not start with a reference") + ++ str " cannot have a universe instance," + ++ str " its expanded head does not start with a reference") + in + let c = match us, DAst.get c with + | None, _ -> c + | Some _, GRef (ref, None) -> DAst.make ?loc @@ GRef (ref, us) + | Some _, GApp (r, arg) -> + let loc' = r.CAst.loc in + begin match DAst.get r with + | GRef (ref, None) -> + DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg) + | _ -> err () + end + | Some _, _ -> err () in c, projapp, args2 (* Rule out section vars since these should have been found by intern_var *) let intern_non_secvar_qualid loc qid intern env lvar us args = - match intern_qualid loc qid intern env lvar us args with - | { v = GRef (VarRef _, _) },_,_ -> raise Not_found - | r -> r + let c, _, _ as r = intern_qualid loc qid intern env lvar us args in + match DAst.get c with + | GRef (VarRef _, _) -> raise Not_found + | _ -> r let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function | Qualid (loc, qid) -> @@ -888,14 +910,14 @@ let interp_reference vars r = (** {5 Cases } *) (** Private internalization patterns *) -type raw_cases_pattern_expr_r = - | RCPatAlias of raw_cases_pattern_expr * Id.t +type 'a raw_cases_pattern_expr_r = + | RCPatAlias of 'a raw_cases_pattern_expr * Id.t | RCPatCstr of Globnames.global_reference - * raw_cases_pattern_expr list * raw_cases_pattern_expr list + * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *) | RCPatAtom of Id.t option - | RCPatOr of raw_cases_pattern_expr list -and raw_cases_pattern_expr = raw_cases_pattern_expr_r CAst.t + | RCPatOr of 'a raw_cases_pattern_expr list +and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t (** {6 Elementary bricks } *) let apply_scope_env env = function @@ -977,7 +999,7 @@ let insert_local_defs_in_pattern (ind,j) l = let (decls,_) = decompose_prod_assum typi in let rec aux decls args = match decls, args with - | Context.Rel.Declaration.LocalDef _ :: decls, args -> (CAst.make @@ RCPatAtom None) :: aux decls args + | Context.Rel.Declaration.LocalDef _ :: decls, args -> (DAst.make @@ RCPatAtom None) :: aux decls args | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *) | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args | _ -> assert false in @@ -1013,10 +1035,10 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i)))) ,l) |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp - then let (b,out) = aux i (q,[]) in (b,(CAst.make @@ RCPatAtom None)::out) + then let (b,out) = aux i (q,[]) in (b,(DAst.make @@ RCPatAtom None)::out) else fail (remaining_args (len_pl1+i) il) |imp::q,(hh::tt as l) -> if is_status_implicit imp - then let (b,out) = aux i (q,l) in (b,(CAst.make @@ RCPatAtom(None))::out) + then let (b,out) = aux i (q,l) in (b,(DAst.make @@ RCPatAtom(None))::out) else let (b,out) = aux (succ i) (q,tt) in (b,hh::out) in aux 0 (impl_list,pl2) @@ -1041,8 +1063,9 @@ let chop_params_pattern loc ind args with_letin = else Inductiveops.inductive_nparams ind in assert (nparams <= List.length args); let params,args = List.chop nparams args in - List.iter (function { v = PatVar Anonymous } -> () - | { loc; v = PatVar _ } | { loc; v = PatCstr(_,_,_) } -> error_parameter_not_implicit ?loc) params; + List.iter (fun c -> match DAst.get c with + | PatVar Anonymous -> () + | PatVar _ | PatCstr(_,_,_) -> error_parameter_not_implicit ?loc:c.CAst.loc) params; args let find_constructor loc add_params ref = @@ -1062,7 +1085,7 @@ let find_constructor loc add_params ref = then Inductiveops.inductive_nparamdecls ind else Inductiveops.inductive_nparams ind in - List.make nb ([], [(Id.Map.empty, CAst.make @@ PatVar Anonymous)]) + List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)]) | None -> [] let find_pattern_variable = function @@ -1235,15 +1258,23 @@ let product_of_cases_patterns aliases idspl = List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl))) idspl (aliases.alias_ids,[aliases.alias_map,[]]) -let rec subst_pat_iterator y t = CAst.(map (function +let rec subst_pat_iterator y t = DAst.(map (function | RCPatAtom id as p -> - begin match id with Some x when Id.equal x y -> t.v | _ -> p end + begin match id with Some x when Id.equal x y -> DAst.get t | _ -> p end | RCPatCstr (id,l1,l2) -> RCPatCstr (id,List.map (subst_pat_iterator y t) l1, List.map (subst_pat_iterator y t) l2) | RCPatAlias (p,a) -> RCPatAlias (subst_pat_iterator y t p,a) | RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl))) +let is_non_zero c = match c with +| { CAst.v = CPrim (Numeral (p, true)) } -> not (is_zero p) +| _ -> false + +let is_non_zero_pat c = match c with +| { CAst.v = CPatPrim (Numeral (p, true)) } -> not (is_zero p) +| _ -> false + let drop_notations_pattern looked_for genv = (* At toplevel, Constructors and Inductives are accepted, in recursive calls only constructor are allowed *) @@ -1258,11 +1289,16 @@ let drop_notations_pattern looked_for genv = if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found in (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) - let rec rcp_of_glob x = CAst.(map (function + let rec rcp_of_glob x = DAst.(map (function | GVar id -> RCPatAtom (Some id) | GHole (_,_,_) -> RCPatAtom (None) | GRef (g,_) -> RCPatCstr (g,[],[]) - | GApp ({ v = GRef (g,_) }, l) -> RCPatCstr (g, List.map rcp_of_glob l,[]) + | GApp (r, l) -> + begin match DAst.get r with + | GRef (g,_) -> RCPatCstr (g, List.map rcp_of_glob l,[]) + | _ -> + CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr.") + end | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x in let rec drop_syndef top scopes re pats = @@ -1303,25 +1339,25 @@ let drop_notations_pattern looked_for genv = let open CAst in let loc = pt.loc in match pt.v with - | CPatAlias (p, id) -> CAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id) + | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id) | CPatRecord l -> let sorted_fields = sort_fields ~complete:false loc l (fun _idx -> CAst.make ?loc @@ CPatAtom None) in begin match sorted_fields with - | None -> CAst.make ?loc @@ RCPatAtom None + | None -> DAst.make ?loc @@ RCPatAtom None | Some (n, head, pl) -> let pl = if !asymmetric_patterns then pl else let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in List.rev_append pars pl in match drop_syndef top scopes head pl with - | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr(a, b, c) + | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end | CPatCstr (head, None, pl) -> begin match drop_syndef top scopes head pl with - | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr(a, b, c) + | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end | CPatCstr (r, Some expl_pl, pl) -> @@ -1330,14 +1366,14 @@ let drop_notations_pattern looked_for genv = raise (InternalizationError (loc,NotAConstructor r)) in if expl_pl == [] then (* Convention: (@r) deactivates all further implicit arguments and scopes *) - CAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, []) + DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, []) else (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *) (* but not scopes in expl_pl *) let (argscs1,_) = find_remaining_scopes expl_pl pl g in - CAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) - | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral (p,true)) }],[]),[]) - when not (is_zero p) -> + DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) + | CPatNotation ("- _",([a],[]),[]) when is_non_zero_pat a -> + let p = match a.CAst.v with CPatPrim (Numeral (p, _)) -> p | _ -> assert false in let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (p,false)) scopes in rcp_of_glob pat | CPatNotation ("( _ )",([a],[]),[]) -> @@ -1358,11 +1394,11 @@ let drop_notations_pattern looked_for genv = | CPatAtom Some id -> begin match drop_syndef top scopes id [] with - | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr (a, b, c) - | None -> CAst.make ?loc @@ RCPatAtom (Some (find_pattern_variable id)) + | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c) + | None -> DAst.make ?loc @@ RCPatAtom (Some (find_pattern_variable id)) end - | CPatAtom None -> CAst.make ?loc @@ RCPatAtom None - | CPatOr pl -> CAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl) + | CPatAtom None -> DAst.make ?loc @@ RCPatAtom None + | CPatOr pl -> DAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl) | CPatCast (_,_) -> (* We raise an error if the pattern contains a cast, due to current restrictions on casts in patterns. Cast in patterns @@ -1389,19 +1425,19 @@ let drop_notations_pattern looked_for genv = let (a,(scopt,subscopes)) = Id.Map.find id subst in in_pat top (scopt,subscopes@snd scopes) a with Not_found -> - if Id.equal id ldots_var then CAst.make ?loc @@ RCPatAtom (Some id) else + if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some id) else anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".") end | NRef g -> ensure_kind top loc g; let (_,argscs) = find_remaining_scopes [] args g in - CAst.make ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args) + DAst.make ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args) | NApp (NRef g,pl) -> ensure_kind top loc g; let (argscs1,argscs2) = find_remaining_scopes pl args g in let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in let pl = add_local_defs_and_check_length loc genv g pl args in - CAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, []) + DAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, []) | NList (x,y,iter,terminator,lassoc) -> if not (List.is_empty args) then user_err ?loc (strbrk "Application of arguments to a recursive notation not supported in patterns."); @@ -1418,7 +1454,7 @@ let drop_notations_pattern looked_for genv = anomaly (Pp.str "Inconsistent substitution of recursive notation.")) | NHole _ -> let () = assert (List.is_empty args) in - CAst.make ?loc @@ RCPatAtom None + DAst.make ?loc @@ RCPatAtom None | t -> error_invalid_pattern_notation ?loc () in in_pat true @@ -1427,10 +1463,10 @@ let rec intern_pat genv aliases pat = let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in let (ids',pll) = product_of_cases_patterns aliases (idslpl1@idslpl2) in let pl' = List.map (fun (asubst,pl) -> - (asubst, CAst.make ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in + (asubst, DAst.make ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in ids',pl' in let loc = CAst.(pat.loc) in - match CAst.(pat.v) with + match DAst.get pat with | RCPatAlias (p, id) -> let aliases' = merge_aliases aliases id in intern_pat genv aliases' p @@ -1448,10 +1484,10 @@ let rec intern_pat genv aliases pat = intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2) | RCPatAtom (Some id) -> let aliases = merge_aliases aliases id in - (aliases.alias_ids,[aliases.alias_map, CAst.make ?loc @@ PatVar (alias_of aliases)]) + (aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)]) | RCPatAtom (None) -> let { alias_ids = ids; alias_map = asubst; } = aliases in - (ids, [asubst, CAst.make ?loc @@ PatVar (alias_of aliases)]) + (ids, [asubst, DAst.make ?loc @@ PatVar (alias_of aliases)]) | RCPatOr pl -> assert (not (List.is_empty pl)); let pl' = List.map (intern_pat genv aliases) pl in @@ -1475,7 +1511,7 @@ let intern_ind_pattern genv scopes pat = with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc in let loc = no_not.CAst.loc in - match no_not.CAst.v with + match DAst.get no_not with | RCPatCstr (head, expl_pl, pl) -> let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in let with_letin, pl2 = add_implicits_check_ind_length genv loc c @@ -1506,9 +1542,18 @@ let merge_impargs l args = let get_implicit_name n imps = Some (Impargs.name_of_implicit (List.nth imps (n-1))) -let set_hole_implicit i b = function - | {loc; v = GRef (r,_) } | { v = GApp ({loc; v = GRef (r,_)},_) } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) - | {loc; v = GVar id } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None) +let set_hole_implicit i b c = + let loc = c.CAst.loc in + match DAst.get c with + | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) + | GApp (r, _) -> + let loc = r.CAst.loc in + begin match DAst.get r with + | GRef (r, _) -> + Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) + | _ -> anomaly (Pp.str "Only refs have implicits.") + end + | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits.") let exists_implicit_name id = @@ -1574,7 +1619,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let before, after = split_at_annot bl n in let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in let ro = f (intern env') in - let n' = Option.map (fun _ -> List.count (function | { v = GLocalAssum _ } -> true + let n' = Option.map (fun _ -> List.count (fun c -> match DAst.get c with + | GLocalAssum _ -> true | _ -> false (* remove let-ins *)) rbefore) n in n', ro, List.fold_left intern_local_binder (env',rbefore) after @@ -1597,7 +1643,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = push_name_env ntnvars (impls_type_list ~args:fix_args tyi) en (Loc.tag @@ Name name)) 0 env' lf in (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in - CAst.make ?loc @@ + DAst.make ?loc @@ GRec (GFix (Array.map (fun (ro,_,_,_) -> ro) idl,n), Array.of_list lf, @@ -1624,7 +1670,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = push_name_env ntnvars (impls_type_list ~args:cofix_args tyi) en (Loc.tag @@ Name name)) 0 env' lf in (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in - CAst.make ?loc @@ + DAst.make ?loc @@ GRec (GCoFix n, Array.of_list lf, Array.map (fun (bl,_,_) -> bl) idl, @@ -1641,11 +1687,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CLetIn (na,c1,t,c2) -> let inc1 = intern (reset_tmp_scope env) c1 in let int = Option.map (intern_type env) t in - CAst.make ?loc @@ + DAst.make ?loc @@ GLetIn (snd na, inc1, int, intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) - | CNotation ("- _",([{ CAst.v = CPrim (Numeral (p,true)) }],[],[])) - when not (is_zero p) -> + | CNotation ("- _", ([a],[],[])) when is_non_zero a -> + let p = match a.CAst.v with CPrim (Numeral (p, _)) -> p | _ -> assert false in intern env (CAst.make ?loc @@ CPrim (Numeral (p,false))) | CNotation ("( _ )",([a],[],[])) -> intern env a | CNotation (ntn,args) -> @@ -1664,13 +1710,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = lvar us args ref in (* Rem: GApp(_,f,[]) stands for @f *) - CAst.make ?loc @@ + DAst.make ?loc @@ GApp (f, intern_args env args_scopes (List.map fst args)) | CApp ((isproj,f), args) -> - let f,args = match f with + let f,args = match f.CAst.v with (* Compact notations like "t.(f args') args" *) - | { CAst.v = CApp ((Some _,f), args') } when not (Option.has_some isproj) -> + | CApp ((Some _,f), args') when not (Option.has_some isproj) -> f,args'@args (* Don't compact "(f args') args" to resolve implicits separately *) | _ -> f,args in @@ -1719,9 +1765,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in (* PatVars before a real pattern do not need to be matched *) let stripped_match_from_in = + let is_patvar c = match DAst.get c with + | PatVar _ -> true + | _ -> false + in let rec aux = function | [] -> [] - | (_, { v = PatVar _}) :: q -> aux q + | (_, c) :: q when is_patvar c -> aux q | l -> l in aux match_from_in in let rtnpo = match stripped_match_from_in with @@ -1730,20 +1780,20 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* Build a return predicate by expansion of the patterns of the "in" clause *) let thevars, thepats = List.split l in let sub_rtn = (* Some (GSort (Loc.ghost,GType None)) *) None in - let sub_tms = List.map (fun id -> (CAst.make @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in + let sub_tms = List.map (fun id -> (DAst.make @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in let main_sub_eqn = Loc.tag @@ ([],thepats, (* "|p1,..,pn" *) Option.cata (intern_type env') - (CAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None)) + (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None)) rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in let catch_all_sub_eqn = if List.for_all (irrefutable globalenv) thepats then [] else - [Loc.tag @@ ([],List.make (List.length thepats) (CAst.make @@ PatVar Anonymous), (* "|_,..,_" *) - CAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in - Some (CAst.make @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) + [Loc.tag @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *) + DAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in + Some (DAst.make @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in - CAst.make ?loc @@ + DAst.make ?loc @@ GCases (sty, rtnpo, tms, List.flatten eqns') | CLetTuple (nal, (na,po), b, c) -> let env' = reset_tmp_scope env in @@ -1753,7 +1803,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env') (Loc.tag na') in intern_type env'' u) po in - CAst.make ?loc @@ + DAst.make ?loc @@ GLetTuple (List.map snd nal, (na', p'), b', intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) | CIf (c, (na,po), b1, b2) -> @@ -1763,7 +1813,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env) (Loc.tag na') in intern_type env'' p) po in - CAst.make ?loc @@ + DAst.make ?loc @@ GIf (c', (na', p'), intern env b1, intern env b2) | CHole (k, naming, solve) -> let k = match k with @@ -1791,28 +1841,28 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let (_, glb) = Genintern.generic_intern ist gen in Some glb in - CAst.make ?loc @@ + DAst.make ?loc @@ GHole (k, naming, solve) (* Parsing pattern variables *) | CPatVar n when pattern_mode -> - CAst.make ?loc @@ + DAst.make ?loc @@ GPatVar (Evar_kinds.SecondOrderPatVar n) | CEvar (n, []) when pattern_mode -> - CAst.make ?loc @@ + DAst.make ?loc @@ GPatVar (Evar_kinds.FirstOrderPatVar n) (* end *) (* Parsing existential variables *) | CEvar (n, l) -> - CAst.make ?loc @@ + DAst.make ?loc @@ GEvar (n, List.map (on_snd (intern env)) l) | CPatVar _ -> raise (InternalizationError (loc,IllegalMetavariable)) (* end *) | CSort s -> - CAst.make ?loc @@ + DAst.make ?loc @@ GSort s | CCast (c1, c2) -> - CAst.make ?loc @@ + DAst.make ?loc @@ GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2) ) and intern_type env = intern (set_type_scope env) @@ -1850,9 +1900,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* the "match" part *) let tm' = intern env tm in (* the "as" part *) - let extra_id,na = match tm', na with - | {loc; v = GVar id}, None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id) - | {loc; v = GRef (VarRef id, _)}, None -> Some id,(loc,Name id) + let extra_id,na = + let loc = tm'.CAst.loc in + match DAst.get tm', na with + | GVar id, None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id) + | GRef (VarRef id, _), None -> Some id,(loc,Name id) | _, None -> None,(Loc.tag Anonymous) | _, Some (loc,na) -> None,(loc,na) in (* the "in" part *) @@ -1871,21 +1923,25 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let rec canonize_args case_rel_ctxt arg_pats forbidden_names match_acc var_acc = let add_name l = function | _,Anonymous -> l - | loc,(Name y as x) -> (y, CAst.make ?loc @@ PatVar x) :: l in + | loc,(Name y as x) -> (y, DAst.make ?loc @@ PatVar x) :: l in match case_rel_ctxt,arg_pats with (* LetIn in the rel_context *) | LocalDef _ :: t, l when not with_letin -> canonize_args t l forbidden_names match_acc ((Loc.tag Anonymous)::var_acc) | [],[] -> (add_name match_acc na, var_acc) - | _::t, { loc; v = PatVar x}::tt -> - canonize_args t tt forbidden_names - (add_name match_acc (loc,x)) ((loc,x)::var_acc) | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt -> - let fresh = - Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in - canonize_args t tt (fresh::forbidden_names) - ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc) + begin match DAst.get c with + | PatVar x -> + let loc = c.CAst.loc in + canonize_args t tt forbidden_names + (add_name match_acc (loc,x)) ((loc,x)::var_acc) + | _ -> + let fresh = + Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in + canonize_args t tt (fresh::forbidden_names) + ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc) + end | _ -> assert false in let _,args_rel = List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in @@ -1924,7 +1980,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* with implicit arguments if maximal insertion is set *) [] else - (CAst.map_from_loc (fun ?loc (a,b,c) -> GHole(a,b,c)) + (DAst.map_from_loc (fun ?loc (a,b,c) -> GHole(a,b,c)) (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) ) :: aux (n+1) impl' subscopes' eargs rargs end @@ -1950,9 +2006,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = and smart_gapp f loc = function | [] -> f - | l -> match f with - | { loc = loc'; v = GApp (g, args) } -> CAst.make ?loc:(Loc.merge_opt loc' loc) @@ GApp (g, args@l) - | _ -> CAst.make ?loc:(Loc.merge_opt (loc_of_glob_constr f) loc) @@ GApp (f, l) + | l -> + let loc' = f.CAst.loc in + match DAst.get f with + | GApp (g, args) -> DAst.make ?loc:(Loc.merge_opt loc' loc) @@ GApp (g, args@l) + | _ -> DAst.make ?loc:(Loc.merge_opt (loc_of_glob_constr f) loc) @@ GApp (f, l) and intern_args env subscopes = function | [] -> [] diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index e498d979d..cae67c3e7 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -119,13 +119,14 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li in aux bound l binders let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) = - let rec vars bound vs t = match t with - | { loc; CAst.v = GVar id } -> + let rec vars bound vs c = match DAst.get c with + | GVar id -> + let loc = c.CAst.loc in if is_freevar bound (Global.env ()) id then if Id.List.mem_assoc_sym id vs then vs else (Loc.tag ?loc id) :: vs else vs - | c -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c + | _ -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c in fun rt -> let vars = List.rev (vars bound [] rt) in List.iter (fun (loc, id) -> @@ -253,11 +254,11 @@ let implicits_of_glob_constr ?(with_products=true) l = (ExplByPos (i, name), (true, true, true)) :: l | _ -> l in - let rec aux i { loc; CAst.v = c } = + let rec aux i c = let abs na bk b = add_impl i na bk (aux (succ i) b) in - match c with + match DAst.get c with | GProd (na, bk, t, b) -> if with_products then abs na bk b else diff --git a/interp/notation.ml b/interp/notation.ml index c373faf68..176ac3bf6 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -265,19 +265,28 @@ let keymap_find key map = (* Scopes table : interpretation -> scope_name *) let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) -let prim_token_key_table = ref KeyMap.empty - -let glob_prim_constr_key = function - | { CAst.v = GApp ({ CAst.v = GRef (ref,_) } ,_) } | { CAst.v = GRef (ref,_) } -> RefKey (canonical_gr ref) +let prim_token_key_table = ref (KeyMap.empty : (string * (any_glob_constr -> prim_token option) * bool) KeyMap.t) + +let glob_prim_constr_key c = match DAst.get c with + | GRef (ref, _) -> RefKey (canonical_gr ref) + | GApp (c, _) -> + begin match DAst.get c with + | GRef (ref, _) -> RefKey (canonical_gr ref) + | _ -> Oth + end | _ -> Oth -let glob_constr_keys = function - | { CAst.v = GApp ({ CAst.v = GRef (ref,_) },_) } -> [RefKey (canonical_gr ref); Oth] - | { CAst.v = GRef (ref,_) } -> [RefKey (canonical_gr ref)] +let glob_constr_keys c = match DAst.get c with + | GApp (c, _) -> + begin match DAst.get c with + | GRef (ref, _) -> [RefKey (canonical_gr ref); Oth] + | _ -> [Oth] + end + | GRef (ref,_) -> [RefKey (canonical_gr ref)] | _ -> [Oth] -let cases_pattern_key = function - | { CAst.v = PatCstr (ref,_,_) } -> RefKey (canonical_gr (ConstructRef ref)) +let cases_pattern_key c = match DAst.get c with + | PatCstr (ref,_,_) -> RefKey (canonical_gr (ConstructRef ref)) | _ -> Oth let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) @@ -300,7 +309,7 @@ type 'a prim_token_interpreter = type cases_pattern_status = bool (* true = use prim token in patterns *) type 'a prim_token_uninterpreter = - glob_constr list * (glob_constr -> 'a option) * cases_pattern_status + glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status type internal_prim_token_interpreter = ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr) @@ -496,11 +505,15 @@ let interp_prim_token_gen ?loc g p local_scopes = let interp_prim_token ?loc = interp_prim_token_gen ?loc (fun _ -> ()) -let rec check_allowed_ref_in_pat looked_for = CAst.(with_val (function +let rec check_allowed_ref_in_pat looked_for = DAst.(with_val (function | GVar _ | GHole _ -> () | GRef (g,_) -> looked_for g - | GApp ({ v = GRef (g,_) },l) -> - looked_for g; List.iter (check_allowed_ref_in_pat looked_for) l + | GApp (f, l) -> + begin match DAst.get f with + | GRef (g, _) -> + looked_for g; List.iter (check_allowed_ref_in_pat looked_for) l + | _ -> raise Not_found + end | _ -> raise Not_found)) let interp_prim_token_cases_pattern_expr ?loc looked_for p = @@ -532,7 +545,7 @@ let uninterp_prim_token c = try let (sc,numpr,_) = KeyMap.find (glob_prim_constr_key c) !prim_token_key_table in - match numpr c with + match numpr (AnyGlobConstr c) with | None -> raise Notation_ops.No_match | Some n -> (sc,n) with Not_found -> raise Notation_ops.No_match @@ -545,8 +558,8 @@ let uninterp_prim_token_ind_pattern ind args = if not b then raise Notation_ops.No_match; let args' = List.map (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in - let ref = CAst.make @@ GRef (ref,None) in - match numpr (CAst.make @@ GApp (ref,args')) with + let ref = DAst.make @@ GRef (ref,None) in + match numpr (AnyGlobConstr (DAst.make @@ GApp (ref,args'))) with | None -> raise Notation_ops.No_match | Some n -> (sc,n) with Not_found -> raise Notation_ops.No_match @@ -557,7 +570,7 @@ let uninterp_prim_token_cases_pattern c = let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in if not b then raise Notation_ops.No_match; let na,c = glob_constr_of_closed_cases_pattern c in - match numpr c with + match numpr (AnyGlobConstr c) with | None -> raise Notation_ops.No_match | Some n -> (na,sc,n) with Not_found -> raise Notation_ops.No_match diff --git a/interp/notation.mli b/interp/notation.mli index f9f247fe1..75c8d5aa5 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -70,7 +70,7 @@ type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr type 'a prim_token_uninterpreter = - glob_constr list * (glob_constr -> 'a option) * cases_pattern_status + glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign @@ -96,9 +96,9 @@ val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (global_reference -> un raise [No_match] if no such token *) val uninterp_prim_token : - glob_constr -> scope_name * prim_token + 'a glob_constr_g -> scope_name * prim_token val uninterp_prim_token_cases_pattern : - cases_pattern -> Name.t * scope_name * prim_token + 'a cases_pattern_g -> Name.t * scope_name * prim_token val uninterp_prim_token_ind_pattern : inductive -> cases_pattern list -> scope_name * prim_token @@ -124,8 +124,8 @@ val interp_notation : ?loc:Loc.t -> notation -> local_scopes -> type notation_rule = interp_rule * interpretation * int option (** Return the possible notations for a given term *) -val uninterp_notations : glob_constr -> notation_rule list -val uninterp_cases_pattern_notations : cases_pattern -> notation_rule list +val uninterp_notations : 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list val uninterp_ind_pattern_notations : inductive -> notation_rule list (** Test if a notation is available in the scopes diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 565a7e642..034116731 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -99,43 +99,43 @@ let name_to_ident = function let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na -let rec cases_pattern_fold_map ?loc g e = CAst.with_val (function +let rec cases_pattern_fold_map ?loc g e = DAst.with_val (function | PatVar na -> - let e',na' = g e na in e', CAst.make ?loc @@ PatVar na' + let e',na' = g e na in e', DAst.make ?loc @@ PatVar na' | PatCstr (cstr,patl,na) -> let e',na' = g e na in let e',patl' = List.fold_left_map (cases_pattern_fold_map ?loc g) e patl in - e', CAst.make ?loc @@ PatCstr (cstr,patl',na') + e', DAst.make ?loc @@ PatCstr (cstr,patl',na') ) let subst_binder_type_vars l = function | Evar_kinds.BinderType (Name id) -> let id = - try match Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id + try match DAst.get (Id.List.assoc id l) with GVar id' -> id' | _ -> id with Not_found -> id in Evar_kinds.BinderType (Name id) | e -> e -let rec subst_glob_vars l gc = CAst.map (function - | GVar id as r -> (try (Id.List.assoc id l).CAst.v with Not_found -> r) +let rec subst_glob_vars l gc = DAst.map (function + | GVar id as r -> (try DAst.get (Id.List.assoc id l) with Not_found -> r) | GProd (Name id,bk,t,c) -> let id = - try match Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id + try match DAst.get (Id.List.assoc id l) with GVar id' -> id' | _ -> id with Not_found -> id in GProd (Name id,bk,subst_glob_vars l t,subst_glob_vars l c) | GLambda (Name id,bk,t,c) -> let id = - try match Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id + try match DAst.get (Id.List.assoc id l) with GVar id' -> id' | _ -> id with Not_found -> id in GLambda (Name id,bk,subst_glob_vars l t,subst_glob_vars l c) | GHole (x,naming,arg) -> GHole (subst_binder_type_vars l x,naming,arg) - | _ -> (map_glob_constr (subst_glob_vars l) gc).CAst.v (* assume: id is not binding *) + | _ -> DAst.get (map_glob_constr (subst_glob_vars l) gc) (* assume: id is not binding *) ) gc let ldots_var = Id.of_string ".." let glob_constr_of_notation_constr_with_binders ?loc g f e nc = - let lt x = CAst.make ?loc x in lt @@ match nc with + let lt x = DAst.make ?loc x in lt @@ match nc with | NVar id -> GVar id | NApp (a,args) -> GApp (f e a, List.map (f e) args) | NList (x,y,iter,tail,swap) -> @@ -143,13 +143,13 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in let inner = lt @@ GApp (lt @@ GVar (ldots_var),[subst_glob_vars innerl it]) in let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in - (subst_glob_vars outerl it).CAst.v + DAst.get (subst_glob_vars outerl it) | NBinderList (x,y,iter,tail) -> let t = f e tail in let it = f e iter in let innerl = [(ldots_var,t);(x, lt @@ GVar y)] in let inner = lt @@ GApp (lt @@ GVar ldots_var,[subst_glob_vars innerl it]) in let outerl = [(ldots_var,inner)] in - (subst_glob_vars outerl it).CAst.v + DAst.get (subst_glob_vars outerl it) | NLambda (na,ty,c) -> let e',na = g e na in GLambda (na,Explicit,f e ty,f e' c) | NProd (na,ty,c) -> @@ -201,28 +201,34 @@ let glob_constr_of_notation_constr ?loc x = let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r) let add_name r = function Anonymous -> () | Name id -> add_id r id +let is_gvar id c = match DAst.get c with +| GVar id' -> Id.equal id id' +| _ -> false + let split_at_recursive_part c = let sub = ref None in - let open CAst in - let rec aux = function - | { loc = loc0; v = GApp ({ loc; v = GVar v },c::l) } when Id.equal v ldots_var -> (* *) + let rec aux c = + let loc0 = c.CAst.loc in + match DAst.get c with + | GApp (f, c::l) when is_gvar ldots_var f -> (* *) + let loc = f.CAst.loc in begin match !sub with | None -> let () = sub := Some c in begin match l with - | [] -> CAst.make ?loc @@ GVar ldots_var - | _ :: _ -> CAst.make ?loc:loc0 @@ GApp (CAst.make ?loc @@ GVar ldots_var, l) + | [] -> DAst.make ?loc @@ GVar ldots_var + | _ :: _ -> DAst.make ?loc:loc0 @@ GApp (DAst.make ?loc @@ GVar ldots_var, l) end | Some _ -> (* Not narrowed enough to find only one recursive part *) raise Not_found end - | c -> map_glob_constr aux c in + | _ -> map_glob_constr aux c in let outer_iterator = aux c in match !sub with | None -> (* No recursive pattern found *) raise Not_found | Some c -> - match outer_iterator.v with + match DAst.get outer_iterator with | GVar v when Id.equal v ldots_var -> (* Not enough context *) raise Not_found | _ -> outer_iterator, c @@ -231,7 +237,7 @@ let subtract_loc loc1 loc2 = let l2 = fst (Option.cata Loc.unloc (0,0) loc2) in Some (Loc.make_loc (l1,l2-1)) -let check_is_hole id = function { CAst.v = GHole _ } -> () | t -> +let check_is_hole id t = match DAst.get t with GHole _ -> () | _ -> user_err ?loc:(loc_of_glob_constr t) (strbrk "In recursive notation with binders, " ++ pr_id id ++ strbrk " is expected to come without type.") @@ -243,21 +249,24 @@ type recursive_pattern_kind = | RecursiveBinders of glob_constr * glob_constr let compare_recursive_parts found f f' (iterator,subc) = - let open CAst in let diff = ref None in let terminator = ref None in - let rec aux c1 c2 = match c1.v, c2.v with + let rec aux c1 c2 = match DAst.get c1, DAst.get c2 with | GVar v, term when Id.equal v ldots_var -> (* We found the pattern *) assert (match !terminator with None -> true | Some _ -> false); terminator := Some c2; true - | GApp ({ v = GVar v },l1), GApp (term, l2) when Id.equal v ldots_var -> + | GApp (f,l1), GApp (term, l2) -> + begin match DAst.get f with + | GVar v when Id.equal v ldots_var -> (* We found the pattern, but there are extra arguments *) (* (this allows e.g. alternative (recursive) notation of application) *) assert (match !terminator with None -> true | Some _ -> false); terminator := Some term; List.for_all2eq aux l1 l2 + | _ -> mk_glob_constr_eq aux c1 c2 + end | GVar x, GVar y when not (Id.equal x y) -> (* We found the position where it differs *) let lassoc = match !terminator with None -> false | Some _ -> true in @@ -301,13 +310,13 @@ let compare_recursive_parts found f f' (iterator,subc) = (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in let iterator = f' (if lassoc then iterator - else subst_glob_vars [x, CAst.make @@ GVar y] iterator) in + else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in (* found have been collected by compare_constr *) found := newfound; NList (x,y,iterator,f (Option.get !terminator),lassoc) | Some (x,y,RecursiveBinders (t_x,t_y)) -> let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in - let iterator = f' (subst_glob_vars [x, CAst.make @@ GVar y] iterator) in + let iterator = f' (subst_glob_vars [x, DAst.make @@ GVar y] iterator) in (* found have been collected by compare_constr *) found := newfound; check_is_hole x t_x; @@ -325,15 +334,20 @@ let notation_constr_and_vars_of_glob_constr a = try compare_recursive_parts found aux aux' (split_at_recursive_part c) with Not_found -> found := keepfound; - match c.CAst.v with - | GApp ({ CAst.v = GVar f; loc},[c]) when Id.equal f ldots_var -> + match DAst.get c with + | GApp (t, [_]) -> + begin match DAst.get t with + | GVar f when Id.equal f ldots_var -> (* Fall on the second part of the recursive pattern w/o having found the first part *) + let loc = t.CAst.loc in user_err ?loc (str "Cannot find where the recursive pattern starts.") + | _ -> aux' c + end | _c -> aux' c - and aux' x = CAst.with_val (function + and aux' x = DAst.with_val (function | 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) @@ -433,7 +447,7 @@ let notation_constr_of_glob_constr nenv a = let notation_constr_of_constr avoiding t = let t = EConstr.of_constr t in - let t = Detyping.detype false avoiding (Global.env()) Evd.empty t in + let t = Detyping.detype Detyping.Now false avoiding (Global.env()) Evd.empty t in let nenv = { ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; @@ -441,13 +455,13 @@ let notation_constr_of_constr avoiding t = notation_constr_of_glob_constr nenv t let rec subst_pat subst pat = - match pat.CAst.v with + match DAst.get pat with | PatVar _ -> pat | PatCstr (((kn,i),j),cpl,n) -> let kn' = subst_mind subst kn and cpl' = List.smartmap (subst_pat subst) cpl in if kn' == kn && cpl' == cpl then pat else - CAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n) + DAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n) let rec subst_notation_constr subst bound raw = match raw with @@ -576,14 +590,14 @@ let abstract_return_type_context pi mklam tml rtno = List.fold_right mklam nal rtn) rtno -let abstract_return_type_context_glob_constr = +let abstract_return_type_context_glob_constr tml rtn = abstract_return_type_context (fun (_,(_,nal)) -> nal) - (fun na c -> CAst.make @@ - GLambda(na,Explicit,CAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) + (fun na c -> DAst.make @@ + GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) tml rtn -let abstract_return_type_context_notation_constr = +let abstract_return_type_context_notation_constr tml rtn = abstract_return_type_context snd - (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c)) + (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c)) tml rtn let is_term_meta id metas = try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false @@ -651,19 +665,23 @@ let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v = let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl = (terms,onlybinders,termlists,(x,bl)::binderlists) -let rec pat_binder_of_term t = CAst.map (function +let rec pat_binder_of_term t = DAst.map (function | GVar id -> PatVar (Name id) - | GApp ({ CAst.v = GRef (ConstructRef cstr,_)}, l) -> + | GApp (t, l) -> + begin match DAst.get t with + | GRef (ConstructRef cstr,_) -> let nparams = Inductiveops.inductive_nparams (fst cstr) in let _,l = List.chop nparams l in PatCstr (cstr, List.map pat_binder_of_term l, Anonymous) + | _ -> raise No_match + end | _ -> raise No_match ) t let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v = try let v' = Id.List.assoc var terms in - match CAst.(v.v, v'.v) with + match DAst.get v, DAst.get v' with | GHole _, _ -> sigma | _, GHole _ -> let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in @@ -677,7 +695,7 @@ let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var try let vl' = Id.List.assoc var termlists in let unify_term v v' = - match CAst.(v.v, v'.v) with + match DAst.get v, DAst.get v' with | GHole _, _ -> v' | _, GHole _ -> v | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v' else raise No_match in @@ -693,8 +711,8 @@ let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id = try - match Id.List.assoc var terms with - | { CAst.v = GVar id' } -> + match DAst.get (Id.List.assoc var terms) with + | GVar id' -> (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), sigma | _ -> anomaly (str "A term which can be a binder has to be a variable.") @@ -702,7 +720,7 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig (* The matching against a term allowing to find the instance has not been found yet *) (* If it will be a different name, we shall unfortunately fail *) (* TODO: look at the consequences for alp *) - alp, add_env alp sigma var (CAst.make @@ GVar id) + alp, add_env alp sigma var (DAst.make @@ GVar id) let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id = try @@ -729,17 +747,19 @@ let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var else (fst alp,(id1,id2)::snd alp),sigma with Not_found -> alp, add_binding_env alp sigma var v -let rec map_cases_pattern_name_left f = CAst.map (function +let rec map_cases_pattern_name_left f = DAst.map (function | PatVar na -> PatVar (f na) | PatCstr (c,l,na) -> PatCstr (c,List.map_left (map_cases_pattern_name_left f) l,f na) ) -let rec fold_cases_pattern_eq f x p p' = let open CAst in match p, p' with - | { loc; v = PatVar na}, { v = PatVar na' } -> let x,na = f x na na' in x, CAst.make ?loc @@ PatVar na - | { loc; v = PatCstr (c,l,na)}, { v = PatCstr (c',l',na') } when eq_constructor c c' -> +let rec fold_cases_pattern_eq f x p p' = + let loc = p.CAst.loc in + match DAst.get p, DAst.get p' with + | PatVar na, PatVar na' -> let x,na = f x na na' in x, DAst.make ?loc @@ PatVar na + | PatCstr (c,l,na), PatCstr (c',l',na') when eq_constructor c c' -> let x,l = fold_cases_pattern_list_eq f x l l' in let x,na = f x na na' in - x, CAst.make ?loc @@ PatCstr (c,l,na) + x, DAst.make ?loc @@ PatCstr (c,l,na) | _ -> failwith "Not equal" and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with @@ -750,7 +770,7 @@ and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with x, p :: pl | _ -> assert false -let rec cases_pattern_eq p1 p2 = match CAst.(p1.v, p2.v) with +let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with | PatVar na1, PatVar na2 -> Name.equal na1 na2 | PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && @@ -771,7 +791,7 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) let unify_pat alp p p' = try fold_cases_pattern_eq unify_name alp p p' with Failure _ -> raise No_match in let unify_term alp v v' = - match CAst.(v.v, v'.v) with + match DAst.get v, DAst.get v' with | GHole _, _ -> v' | _, GHole _ -> v | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in @@ -783,16 +803,16 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in let unify_binder alp b b' = let loc, loc' = CAst.(b.loc, b'.loc) in - match CAst.(b.v, b'.v) with + match DAst.get b, DAst.get b' with | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') -> let alp, na = unify_name alp na na' in - alp, CAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t') + alp, DAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t') | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') -> let alp, na = unify_name alp na na' in - alp, CAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t') + alp, DAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t') | GLocalPattern ((p,ids),id,bk,t), GLocalPattern ((p',_),_,bk',t') -> let alp, p = unify_pat alp p p' in - alp, CAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t') + alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t') | _ -> raise No_match in let rec unify alp bl bl' = match bl, bl' with @@ -819,19 +839,22 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v let unify_pat p p' = if cases_pattern_eq (map_cases_pattern_name_left (name_app (rename_var (snd alp))) p) p' then p' else raise No_match in - let unify_term_binder c = CAst.(map (fun b' -> - match c, b' with - | { v = GVar id}, GLocalAssum (na', bk', t') -> + let unify_term_binder c = DAst.(map (fun b' -> + match DAst.get c, b' with + | GVar id, GLocalAssum (na', bk', t') -> GLocalAssum (unify_id id na', bk', t') - | c, GLocalPattern ((p',ids), id, bk', t') -> + | _, GLocalPattern ((p',ids), id, bk', t') -> let p = pat_binder_of_term c in GLocalPattern ((unify_pat p p',ids), id, bk', t') | _ -> raise No_match )) in let rec unify cl bl' = match cl, bl' with | [], [] -> [] - | c :: cl, { CAst.v = GLocalDef ( _, _, _, t) } :: bl' -> unify cl bl' - | c :: cl, b' :: bl' -> unify_term_binder c b' :: unify cl bl' + | c :: cl, b' :: bl' -> + begin match DAst.get b' with + | GLocalDef ( _, _, _, t) -> unify cl bl' + | _ -> unify_term_binder c b' :: unify cl bl' + end | _ -> raise No_match in let bl = unify cl bl' in let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in @@ -872,7 +895,7 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | _ -> raise No_match let rec match_cases_pattern_binders metas acc pat1 pat2 = - match CAst.(pat1.v, pat2.v) with + match DAst.get pat1, DAst.get pat2 with | PatVar na1, PatVar na2 -> match_names metas acc na1 na2 | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2) when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) -> @@ -882,21 +905,29 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 = let glue_letin_with_decls = true -let rec match_iterated_binders islambda decls bi = CAst.(with_loc_val (fun ?loc -> function - | GLambda (Name p,bk,t, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b))])}) - when islambda && Id.equal p e -> - match_iterated_binders islambda ((CAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b - | GLambda (na,bk,t,b) when islambda -> - match_iterated_binders islambda ((CAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b - | GProd (Name p,bk,t, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b))]) } ) - when not islambda && Id.equal p e -> - match_iterated_binders islambda ((CAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b - | GProd ((Name _ as na),bk,t,b) when not islambda -> - match_iterated_binders islambda ((CAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b +let rec match_iterated_binders islambda decls bi = DAst.(with_loc_val (fun ?loc -> function + | GLambda (na,bk,t,b) as b0 -> + begin match na, DAst.get b with + | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))]) + when islambda && is_gvar p e -> + match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b + | _, _ when islambda -> + match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b + | _ -> (decls, DAst.make ?loc b0) + end + | GProd (na,bk,t,b) as b0 -> + begin match na, DAst.get b with + | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))]) + when not islambda && is_gvar p e -> + match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b + | Name _, _ when not islambda -> + match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b + | _ -> (decls, DAst.make ?loc b0) + end | GLetIn (na,c,t,b) when glue_letin_with_decls -> match_iterated_binders islambda - ((CAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b - | b -> (decls, CAst.make ?loc b) + ((DAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b + | b -> (decls, DAst.make ?loc b) )) bi let remove_sigma x (terms,onlybinders,termlists,binderlists) = @@ -948,7 +979,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin lassoc = else bind_termlist_env alp sigma x l -let does_not_come_from_already_eta_expanded_var = +let does_not_come_from_already_eta_expanded_var glob = (* This is hack to avoid looping on a rule with rhs of the form *) (* "?f (fun ?x => ?g)" since otherwise, matching "F H" expands in *) (* "F (fun x => H x)" and "H x" is recursively matched against the same *) @@ -958,12 +989,14 @@ let does_not_come_from_already_eta_expanded_var = (* The following test is then an approximation of what can be done *) (* optimally (whether other looping situations can occur remains to be *) (* checked). *) - function { CAst.v = GVar _ } -> false | _ -> true + match DAst.get glob with GVar _ -> false | _ -> true + +let is_var c = match DAst.get c with GVar _ -> true | _ -> false let rec match_ inner u alp metas sigma a1 a2 = let open CAst in let loc = a1.loc in - match a1.v, a2 with + match DAst.get a1, a2 with (* Matching notation variable *) | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1 | GVar id1, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1 @@ -973,50 +1006,62 @@ let rec match_ inner u alp metas sigma a1 a2 = | r1, NList (x,y,iter,termin,lassoc) -> match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin lassoc - (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *) - | GLambda (Name p,bk,t1, { v = GCases (LetPatternStyle,None,[({ v = GVar e},_)],[(_,(ids,[cp],b1))])}), - NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e -> - let (decls,b) = match_iterated_binders true [CAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in + | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin) -> + begin match na1, DAst.get b1, iter with + (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *) + | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _) when is_gvar p e -> + let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin - - (* Matching recursive notations for binders: ad hoc cases supporting let-in *) - | GLambda (na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)-> - let (decls,b) = match_iterated_binders true [CAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in + (* Matching recursive notations for binders: ad hoc cases supporting let-in *) + | _, _, NLambda (Name _,_,_) -> + let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in (* TODO: address the possibility that termin is a Lambda itself *) let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin + (* Matching recursive notations for binders: general case *) + | _, _, _ -> + match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin + end - (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *) - | GProd (Name p,bk,t1, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b1))]) } ), - NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e -> - let (decls,b) = match_iterated_binders true [CAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in + | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin) -> + (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *) + begin match na1, DAst.get b1, iter, termin with + | Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _ when is_gvar p e -> + let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin - - | GProd (na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin) - when na1 != Anonymous -> - let (decls,b) = match_iterated_binders false [CAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in + | _, _, NProd (Name _,_,_), _ when na1 != Anonymous -> + let (decls,b) = match_iterated_binders false [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in (* TODO: address the possibility that termin is a Prod itself *) let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin + (* Matching recursive notations for binders: general case *) + | _, _, _, _ -> + match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin + end + (* Matching recursive notations for binders: general case *) | _r, NBinderList (x,y,iter,termin) -> - match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin + match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin (* Matching individual binders as part of a recursive pattern *) - | GLambda (Name p,bk,t, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b1))])}), - NLambda (Name id,_,b2) - when is_bindinglist_meta id metas -> - let alp,sigma = bind_bindinglist_env alp sigma id [CAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in + | GLambda (na1, bk, t1, b1), NLambda (na2, t2, b2) -> + begin match na1, DAst.get b1, na2 with + | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id + when is_var e && is_bindinglist_meta id metas -> + let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] in match_in u alp metas sigma b1 b2 - | GLambda (na,bk,t,b1), NLambda (Name id,_,b2) - when is_bindinglist_meta id metas -> - let alp,sigma = bind_bindinglist_env alp sigma id [CAst.make ?loc @@ GLocalAssum (na,bk,t)] in + | _, _, Name id when is_bindinglist_meta id metas -> + let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] in match_in u alp metas sigma b1 b2 + | _ -> + match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 + end + | GProd (na,bk,t,b1), NProd (Name id,_,b2) when is_bindinglist_meta id metas && na != Anonymous -> - let alp,sigma = bind_bindinglist_env alp sigma id [CAst.make ?loc @@ GLocalAssum (na,bk,t)] in + let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na,bk,t)] in match_in u alp metas sigma b1 b2 (* Matching compositionally *) @@ -1028,13 +1073,11 @@ let rec match_ inner u alp metas sigma a1 a2 = if n1 < n2 then 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 CAst.make ?loc @@ GApp (f1,l11),l12, f2,l2 + let l11,l12 = List.chop (n1-n2) l1 in DAst.make ?loc @@ GApp (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), 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), NProd (na2,t2,b2) -> match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 | GLetIn (na1,b1,_,c1), NLetIn (na2,b2,None,c2) @@ -1101,17 +1144,17 @@ let rec match_ inner u alp metas sigma a1 a2 = let avoid = free_glob_vars a1 @ (* as in Namegen: *) glob_visible_short_qualid a1 in let id' = Namegen.next_ident_away id avoid in - let t1 = CAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in + let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in let sigma = match t2 with | NHole _ -> sigma | NVar id2 -> bind_term_env alp sigma id2 t1 | _ -> assert false in let (alp,sigma) = if is_bindinglist_meta id metas then - bind_bindinglist_env alp sigma id [CAst.make @@ GLocalAssum (Name id',Explicit,t1)] + bind_bindinglist_env alp sigma id [DAst.make @@ GLocalAssum (Name id',Explicit,t1)] else match_names metas (alp,sigma) (Name id') na in - match_in u alp metas sigma (mkGApp a1 (CAst.make @@ GVar id')) b2 + match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2 | (GRec _ | GEvar _), _ | _,_ -> raise No_match @@ -1132,7 +1175,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 term_of_binder bi = CAst.make @@ match bi with +let term_of_binder bi = DAst.make @@ match bi with | Name id -> GVar id | Anonymous -> GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) @@ -1145,7 +1188,7 @@ let match_notation_constr u c (metas,pat) = with Not_found -> (* Happens for binders bound to Anonymous *) (* Find a better way to propagate Anonymous... *) - CAst.make @@GVar x in + DAst.make @@GVar x in List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> match typ with | NtnTypeConstr -> @@ -1185,8 +1228,7 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc = (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists) let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = - let open CAst in - match a1.v, a2 with + match DAst.get a1, a2 with | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) | PatVar Anonymous, NHole _ -> sigma,(0,[]) | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 3154fd7ad..0904a4ea3 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -47,19 +47,19 @@ val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_const exception No_match -val match_notation_constr : bool -> glob_constr -> interpretation -> - (glob_constr * subscopes) list * (glob_constr list * subscopes) list * - (extended_glob_local_binder list * subscopes) list +val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> + ('a glob_constr_g * subscopes) list * ('a glob_constr_g list * subscopes) list * + ('a extended_glob_local_binder_g list * subscopes) list val match_notation_constr_cases_pattern : - cases_pattern -> interpretation -> - ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * - (int * cases_pattern list) + 'a cases_pattern_g -> interpretation -> + (('a cases_pattern_g * subscopes) list * ('a cases_pattern_g list * subscopes) list) * + (int * 'a cases_pattern_g list) val match_notation_constr_ind_pattern : - inductive -> cases_pattern list -> interpretation -> - ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * - (int * cases_pattern list) + inductive -> 'a cases_pattern_g list -> interpretation -> + (('a cases_pattern_g * subscopes) list * ('a cases_pattern_g list * subscopes) list) * + (int * 'a cases_pattern_g list) (** {5 Matching a notation pattern against a [glob_constr]} *) diff --git a/interp/reserve.ml b/interp/reserve.ml index b05f05283..a1e5bd0ea 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -110,7 +110,7 @@ let revert_reserved_type t = let t = EConstr.Unsafe.to_constr t in let reserved = KeyMap.find (constr_key t) !reserve_revtable in let t = EConstr.of_constr t in - let t = Detyping.detype false [] (Global.env()) Evd.empty t in + let t = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _] then I've introduced a bug... *) let filter _ pat = diff --git a/intf/glob_term.ml b/intf/glob_term.ml index dd122b972..757ba5786 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -24,66 +24,82 @@ type existential_name = Id.t (** The kind of patterns that occurs in "match ... with ... end" locs here refers to the ident's location, not whole pat *) -type cases_pattern_r = +type 'a cases_pattern_r = | PatVar of Name.t - | PatCstr of constructor * cases_pattern list * Name.t + | PatCstr of constructor * 'a cases_pattern_g list * Name.t (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) -and cases_pattern = cases_pattern_r CAst.t +and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t + +type cases_pattern = [ `any ] cases_pattern_g (** Representation of an internalized (or in other words globalized) term. *) -type glob_constr_r = +type 'a glob_constr_r = | GRef of global_reference * glob_level list option (** An identifier that represents a reference to an object defined either in the (global) environment or in the (local) context. *) | GVar of Id.t (** An identifier that cannot be regarded as "GRef". Bound variables are typically represented this way. *) - | GEvar of existential_name * (Id.t * glob_constr) list + | GEvar of existential_name * (Id.t * 'a glob_constr_g) list | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *) - | GApp of glob_constr * glob_constr list - | GLambda of Name.t * binding_kind * glob_constr * glob_constr - | GProd of Name.t * binding_kind * glob_constr * glob_constr - | GLetIn of Name.t * glob_constr * glob_constr option * glob_constr - | GCases of case_style * glob_constr option * tomatch_tuples * cases_clauses + | GApp of 'a glob_constr_g * 'a glob_constr_g list + | GLambda of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g + | GProd of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g + | GLetIn of Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g + | GCases of case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g (** [GCases(style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) - | GLetTuple of Name.t list * (Name.t * glob_constr option) * glob_constr * glob_constr - | GIf of glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr - | GRec of fix_kind * Id.t array * glob_decl list array * - glob_constr array * glob_constr array + | GLetTuple of Name.t list * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g + | GIf of 'a glob_constr_g * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g + | GRec of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array * + 'a glob_constr_g array * 'a glob_constr_g array | GSort of glob_sort | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option - | GCast of glob_constr * glob_constr cast_type -and glob_constr = glob_constr_r CAst.t + | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type +and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t -and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr +and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g -and fix_recursion_order = +and 'a fix_recursion_order_g = | GStructRec - | GWfRec of glob_constr - | GMeasureRec of glob_constr * glob_constr option + | GWfRec of 'a glob_constr_g + | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option -and fix_kind = - | GFix of ((int option * fix_recursion_order) array * int) +and 'a fix_kind_g = + | GFix of ((int option * 'a fix_recursion_order_g) array * int) | GCoFix of int -and predicate_pattern = +and 'a predicate_pattern_g = Name.t * (inductive * Name.t list) Loc.located option (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *) -and tomatch_tuple = (glob_constr * predicate_pattern) +and 'a tomatch_tuple_g = ('a glob_constr_g * 'a predicate_pattern_g) -and tomatch_tuples = tomatch_tuple list +and 'a tomatch_tuples_g = 'a tomatch_tuple_g list -and cases_clause = (Id.t list * cases_pattern list * glob_constr) Loc.located +and 'a cases_clause_g = (Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) Loc.located (** [(p,il,cl,t)] = "|'cl' => 't'". Precondition: the free variables of [t] are members of [il]. *) -and cases_clauses = cases_clause list - -type extended_glob_local_binder_r = - | GLocalAssum of Name.t * binding_kind * glob_constr - | GLocalDef of Name.t * binding_kind * glob_constr * glob_constr option - | GLocalPattern of (cases_pattern * Id.t list) * Id.t * binding_kind * glob_constr -and extended_glob_local_binder = extended_glob_local_binder_r CAst.t +and 'a cases_clauses_g = 'a cases_clause_g list + +type glob_constr = [ `any ] glob_constr_g +type tomatch_tuple = [ `any ] tomatch_tuple_g +type tomatch_tuples = [ `any ] tomatch_tuples_g +type cases_clause = [ `any ] cases_clause_g +type cases_clauses = [ `any ] cases_clauses_g +type glob_decl = [ `any ] glob_decl_g +type fix_kind = [ `any ] fix_kind_g +type predicate_pattern = [ `any ] predicate_pattern_g +type fix_recursion_order = [ `any ] fix_recursion_order_g + +type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr + +type 'a extended_glob_local_binder_r = + | GLocalAssum of Name.t * binding_kind * 'a glob_constr_g + | GLocalDef of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option + | GLocalPattern of ('a cases_pattern_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g +and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t + +type extended_glob_local_binder = [ `any ] extended_glob_local_binder_g (** A globalised term together with a closure representing the value of its free variables. Intended for use when these variables are taken diff --git a/lib/clib.mllib b/lib/clib.mllib index d5c938fe5..5c1f7d9af 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -19,6 +19,7 @@ Flags Control Loc CAst +DAst CList CString Deque diff --git a/lib/dAst.ml b/lib/dAst.ml new file mode 100644 index 000000000..0fe323d01 --- /dev/null +++ b/lib/dAst.ml @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open CAst + +type ('a, _) thunk = +| Value : 'a -> ('a, 'b) thunk +| Thunk : 'a Lazy.t -> ('a, [ `thunk ]) thunk + +type ('a, 'b) t = ('a, 'b) thunk CAst.t + +let map_thunk (type s) f : (_, s) thunk -> (_, s) thunk = function +| Value x -> Value (f x) +| Thunk k -> Thunk (lazy (f (Lazy.force k))) + +let get_thunk (type s) : ('a, s) thunk -> 'a = function +| Value x -> x +| Thunk k -> Lazy.force k + +let get x = get_thunk x.v + +let make ?loc v = CAst.make ?loc (Value v) + +let delay ?loc v = CAst.make ?loc (Thunk (Lazy.from_fun v)) + +let map f n = CAst.map (fun x -> map_thunk f x) n + +let map_with_loc f n = + CAst.map_with_loc (fun ?loc x -> map_thunk (fun x -> f ?loc x) x) n + +let map_from_loc f (loc, x) = + make ?loc (f ?loc x) + +let with_val f n = f (get n) + +let with_loc_val f n = f ?loc:n.CAst.loc (get n) diff --git a/lib/dAst.mli b/lib/dAst.mli new file mode 100644 index 000000000..5b51677fc --- /dev/null +++ b/lib/dAst.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Lazy AST node wrapper. Only used for [glob_constr] as of today. *) + +type ('a, _) thunk = +| Value : 'a -> ('a, 'b) thunk +| Thunk : 'a Lazy.t -> ('a, [ `thunk ]) thunk + +type ('a, 'b) t = ('a, 'b) thunk CAst.t + +val get : ('a, 'b) t -> 'a +val get_thunk : ('a, 'b) thunk -> 'a + +val make : ?loc:Loc.t -> 'a -> ('a, 'b) t +val delay : ?loc:Loc.t -> (unit -> 'a) -> ('a, [ `thunk ]) t + +val map : ('a -> 'b) -> ('a, 'c) t -> ('b, 'c) t +val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> ('a, 'c) t -> ('b, 'c) t +val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> ('b, 'c) t + +val with_val : ('a -> 'b) -> ('a, 'c) t -> 'b +val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> ('a, 'c) t -> 'b diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 5a4c52456..fca7d9851 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -442,11 +442,11 @@ let cc_tactic depth additionnal_terms = let open Glob_term in let env = Proofview.Goal.env gl in let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in - let hole = CAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in + let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in let pr_missing (c, missing) = - let c = Detyping.detype ~lax:true false [] env sigma c in + let c = Detyping.detype Detyping.Now ~lax:true false [] env sigma c in let holes = List.init missing (fun _ -> hole) in - Printer.pr_glob_constr_env env (CAst.make @@ GApp (c, holes)) + Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes)) in Feedback.msg_info (Pp.str "Goal is solvable by congruence but some arguments are missing."); diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 8cf5e8442..7087a195e 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -34,10 +34,10 @@ type glob_context = (binder_type*glob_constr) list let rec solve_trivial_holes pat_as_term e = - match pat_as_term.CAst.v,e.CAst.v with + match DAst.get pat_as_term, DAst.get e with | GHole _,_ -> e | GApp(fp,argsp),GApp(fe,argse) when glob_constr_eq fp fe -> - CAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse)) + DAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse)) | _,_ -> pat_as_term (* @@ -361,7 +361,7 @@ let add_pat_variables pat typ env : Environ.env = let rec add_pat_variables env pat typ : Environ.env = observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); - match pat.CAst.v with + match DAst.get pat with | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env | PatCstr(c,patl,na) -> let Inductiveops.IndType(indf,indargs) = @@ -411,7 +411,7 @@ let add_pat_variables pat typ env : Environ.env = -let rec pattern_to_term_and_type env typ = CAst.with_val (function +let rec pattern_to_term_and_type env typ = DAst.with_val (function | PatVar Anonymous -> assert false | PatVar (Name id) -> mkGVar id @@ -434,7 +434,7 @@ let rec pattern_to_term_and_type env typ = CAst.with_val (function Array.to_list (Array.init (cst_narg - List.length patternl) - (fun i -> Detyping.detype false [] env (Evd.from_env env) (EConstr.of_constr csta.(i))) + (fun i -> Detyping.detype Detyping.Now false [] env (Evd.from_env env) (EConstr.of_constr csta.(i))) ) in let patl_as_term = @@ -480,7 +480,7 @@ let rec pattern_to_term_and_type env typ = CAst.with_val (function let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = observe (str " Entering : " ++ Printer.pr_glob_constr rt); let open CAst in - match rt.v with + match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> (* do nothing (except changing type of course) *) mk_result [] rt avoid @@ -496,13 +496,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = (mk_result [] [] avoid) in begin - match f.v with + match DAst.get f with | GLambda _ -> let rec aux t l = match l with | [] -> t - | u::l -> CAst.make @@ - match t.v with + | u::l -> DAst.make @@ + match DAst.get t with | GLambda(na,_,nat,b) -> GLetIn(na,u,None,aux b l) | _ -> @@ -519,7 +519,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in - let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in + let res_raw_type = Detyping.detype Detyping.Now false [] env (Evd.from_env env) rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in let res_rt = mkGVar res in @@ -564,7 +564,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_b = replace_var_by_term id - (CAst.make @@ GVar id) + (DAst.make @@ GVar id) b in (Name new_id,new_b,new_avoid) @@ -626,7 +626,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = then the one corresponding to the value [t] and combine the two result *) - let v = match typ with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in + let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let v_res = build_entry_lc env funnames avoid v in let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in @@ -773,7 +773,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id) in let raw_typ_of_id = - Detyping.detype false [] + Detyping.detype Detyping.Now false [] env_with_pat_ids (Evd.from_env env) typ_of_id in mkGProd (Name id,raw_typ_of_id,acc)) @@ -819,7 +819,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve (fun pat e typ_as_constr -> let this_pat_ids = ids_of_pat pat in let typ_as_constr = EConstr.of_constr typ_as_constr in - let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in + let typ = Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_as_constr in let pat_as_term = pattern_to_term pat in (* removing trivial holes *) let pat_as_term = solve_trivial_holes pat_as_term e in @@ -833,7 +833,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve then (Prod (Name id), let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in let raw_typ_of_id = - Detyping.detype false [] new_env (Evd.from_env env) typ_of_id + Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_of_id in raw_typ_of_id )::acc @@ -875,15 +875,23 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve { brl'_res with result = this_branch_res@brl'_res.result } -let is_res id = - try +let is_res r = match DAst.get r with +| GVar id -> + begin try String.equal (String.sub (Id.to_string id) 0 4) "_res" - with Invalid_argument _ -> false + with Invalid_argument _ -> false end +| _ -> false +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false +let is_gvar c = match DAst.get c with +| GVar id -> true +| _ -> false let same_raw_term rt1 rt2 = - match CAst.(rt1.v, rt2.v) with + match DAst.get rt1, DAst.get rt2 with | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2 | GHole _, GHole _ -> true | _ -> false @@ -917,23 +925,24 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = observe (str "rebuilding : " ++ pr_glob_constr rt); let open Context.Rel.Declaration in let open CAst in - match rt.v with + match DAst.get rt with | GProd(n,k,t,b) -> let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t::crossed_types in begin - match t with - | { v = GApp(({ v = GVar res_id } as res_rt),args') } when is_res res_id -> + match DAst.get t with + | GApp(res_rt ,args') when is_res res_rt -> begin - match args' with - | { v = GVar this_relname }::args' -> + let arg = List.hd args' in + match DAst.get arg with + | GVar this_relname -> (*i The next call to mk_rel_id is valid since we are constructing the graph Ensures by: obvious i*) let new_t = - mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt]) + mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt]) in let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in let new_env = Environ.push_rel (LocalAssum (n,t')) env in @@ -948,9 +957,13 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> (* the first args is the name of the function! *) assert false end - | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty; { loc = loc3; v = GVar id};rt]) } - when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + | GApp(eq_as_ref,[ty; id ;rt]) + when is_gvar id && is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> + let loc1 = rt.CAst.loc in + let loc2 = eq_as_ref.CAst.loc in + let loc3 = id.CAst.loc in + let id = match DAst.get id with GVar id -> id | _ -> assert false in begin try observe (str "computing new type for eq : " ++ pr_glob_constr rt); @@ -985,10 +998,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let params,arg' = ((Util.List.chop nparam args')) in - let rt_typ = CAst.make @@ - GApp(CAst.make @@ GRef (Globnames.IndRef (fst ind),None), + let rt_typ = DAst.make @@ + GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None), (List.map - (fun p -> Detyping.detype false [] + (fun p -> Detyping.detype Detyping.Now false [] env (Evd.from_env env) (EConstr.of_constr p)) params)@(Array.to_list (Array.make @@ -996,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (mkGHole ())))) in let eq' = - CAst.make ?loc:loc1 @@ GApp(CAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;CAst.make ?loc:loc3 @@ GVar id;rt_typ;rt]) + DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt]) in observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in @@ -1015,12 +1028,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match na with | Anonymous -> acc | Name id' -> - (id',Detyping.detype false [] + (id',Detyping.detype Detyping.Now false [] env (Evd.from_env env) arg)::acc else if isVar var_as_constr - then (destVar var_as_constr,Detyping.detype false [] + then (destVar var_as_constr,Detyping.detype Detyping.Now false [] env (Evd.from_env env) arg)::acc @@ -1065,8 +1078,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGProd(n,t,new_b),id_to_exclude else new_b, Id.Set.add id id_to_exclude *) - | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty;rt1;rt2]) } - when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + | GApp(eq_as_ref,[ty;rt1;rt2]) + when is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin try @@ -1077,7 +1090,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = List.fold_left (fun acc (lhs,rhs) -> mkGProd(Anonymous, - mkGApp(mkGRef(eq_as_ref),[mkGHole ();lhs;rhs]),acc) + mkGApp(mkGRef(Lazy.force Coqlib.coq_eq_ref),[mkGHole ();lhs;rhs]),acc) ) b l @@ -1135,14 +1148,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = then new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) else - CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude + DAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude | _ -> anomaly (Pp.str "Should not have an anonymous function here.") (* We have renamed all the anonymous functions during alpha_renaming phase *) end | GLetIn(n,v,t,b) -> begin - let t = match t with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in + let t = match t with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in @@ -1158,7 +1171,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match n with | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args -> new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) - | _ -> CAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *) + | _ -> DAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *) Id.Set.filter not_free_in_t id_to_exclude end | GLetTuple(nal,(na,rto),t,b) -> @@ -1184,7 +1197,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* | Name id when Id.Set.mem id id_to_exclude -> *) (* new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *) (* | _ -> *) - CAst.make @@ GLetTuple(nal,(na,None),t,new_b), + DAst.make @@ GLetTuple(nal,(na,None),t,new_b), Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude') end @@ -1210,12 +1223,15 @@ let rebuild_cons env nb_args relname args crossed_types rt = TODO: Find a valid way to deal with implicit arguments here! *) -let rec compute_cst_params relnames params gt = CAst.with_val (function +let rec compute_cst_params relnames params gt = DAst.with_val (function | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params - | GApp({ CAst.v = GVar relname' },rtl) when Id.Set.mem relname' relnames -> - compute_cst_params_from_app [] (params,rtl) | GApp(f,args) -> + begin match DAst.get f with + | GVar relname' when Id.Set.mem relname' relnames -> + compute_cst_params_from_app [] (params,args) + | _ -> List.fold_left (compute_cst_params relnames) params (f::args) + end | GLambda(_,_,t,b) | GProd(_,_,t,b) | GLetTuple(_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b @@ -1232,10 +1248,10 @@ let rec compute_cst_params relnames params gt = CAst.with_val (function raise (UserError(Some "compute_cst_params", str "Not handled case")) ) gt and compute_cst_params_from_app acc (params,rtl) = + let is_gid id c = match DAst.get c with GVar id' -> Id.equal id id' | _ -> false in match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) - | ((Name id,_,None) as param)::params', { CAst.v = GVar id' }::rtl' - when Id.compare id id' == 0 -> + | ((Name id,_,None) as param)::params', c::rtl' when is_gid id c -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 003bb4e30..02ee56ac5 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -10,36 +10,36 @@ open Misctypes Some basic functions to rebuild glob_constr In each of them the location is Loc.ghost *) -let mkGRef ref = CAst.make @@ GRef(ref,None) -let mkGVar id = CAst.make @@ GVar(id) -let mkGApp(rt,rtl) = CAst.make @@ GApp(rt,rtl) -let mkGLambda(n,t,b) = CAst.make @@ GLambda(n,Explicit,t,b) -let mkGProd(n,t,b) = CAst.make @@ GProd(n,Explicit,t,b) -let mkGLetIn(n,b,t,c) = CAst.make @@ GLetIn(n,b,t,c) -let mkGCases(rto,l,brl) = CAst.make @@ GCases(Term.RegularStyle,rto,l,brl) -let mkGSort s = CAst.make @@ GSort(s) -let mkGHole () = CAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) -let mkGCast(b,t) = CAst.make @@ GCast(b,CastConv t) +let mkGRef ref = DAst.make @@ GRef(ref,None) +let mkGVar id = DAst.make @@ GVar(id) +let mkGApp(rt,rtl) = DAst.make @@ GApp(rt,rtl) +let mkGLambda(n,t,b) = DAst.make @@ GLambda(n,Explicit,t,b) +let mkGProd(n,t,b) = DAst.make @@ GProd(n,Explicit,t,b) +let mkGLetIn(n,b,t,c) = DAst.make @@ GLetIn(n,b,t,c) +let mkGCases(rto,l,brl) = DAst.make @@ GCases(Term.RegularStyle,rto,l,brl) +let mkGSort s = DAst.make @@ GSort(s) +let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) +let mkGCast(b,t) = DAst.make @@ GCast(b,CastConv t) (* Some basic functions to decompose glob_constrs These are analogous to the ones constrs *) let glob_decompose_prod = - let rec glob_decompose_prod args = function - | { CAst.v = GProd(n,k,t,b) } -> + let rec glob_decompose_prod args c = match DAst.get c with + | GProd(n,k,t,b) -> glob_decompose_prod ((n,t)::args) b - | rt -> args,rt + | _ -> args,c in glob_decompose_prod [] let glob_decompose_prod_or_letin = - let rec glob_decompose_prod args = function - | { CAst.v = GProd(n,k,t,b) } -> + let rec glob_decompose_prod args rt = match DAst.get rt with + | GProd(n,k,t,b) -> glob_decompose_prod ((n,None,Some t)::args) b - | { CAst.v = GLetIn(n,b,t,c) } -> + | GLetIn(n,b,t,c) -> glob_decompose_prod ((n,Some b,t)::args) c - | rt -> args,rt + | _ -> args,rt in glob_decompose_prod [] @@ -58,10 +58,10 @@ let glob_decompose_prod_n n = let rec glob_decompose_prod i args c = if i<=0 then args,c else - match c with - | { CAst.v = GProd(n,_,t,b) } -> + match DAst.get c with + | GProd(n,_,t,b) -> glob_decompose_prod (i-1) ((n,t)::args) b - | rt -> args,rt + | _ -> args,c in glob_decompose_prod n [] @@ -70,12 +70,12 @@ let glob_decompose_prod_or_letin_n n = let rec glob_decompose_prod i args c = if i<=0 then args,c else - match c with - | { CAst.v = GProd(n,_,t,b) } -> + match DAst.get c with + | GProd(n,_,t,b) -> glob_decompose_prod (i-1) ((n,None,Some t)::args) b - | { CAst.v = GLetIn(n,b,t,c) } -> + | GLetIn(n,b,t,c) -> glob_decompose_prod (i-1) ((n,Some b,t)::args) c - | rt -> args,rt + | _ -> args,c in glob_decompose_prod n [] @@ -83,10 +83,10 @@ let glob_decompose_prod_or_letin_n n = let glob_decompose_app = let rec decompose_rapp acc rt = (* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *) - match rt with - | { CAst.v = GApp(rt,rtl) } -> + match DAst.get rt with + | GApp(rt,rtl) -> decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt - | rt -> rt,List.rev acc + | _ -> rt,List.rev acc in decompose_rapp [] @@ -120,7 +120,7 @@ let remove_name_from_mapping mapping na = let change_vars = let rec change_vars mapping rt = - CAst.map_with_loc (fun ?loc -> function + DAst.map_with_loc (fun ?loc -> function | GRef _ as x -> x | GVar id -> let new_id = @@ -191,15 +191,15 @@ let change_vars = let rec alpha_pat excluded pat = let loc = pat.CAst.loc in - match pat.CAst.v with + match DAst.get pat with | PatVar Anonymous -> let new_id = Indfun_common.fresh_id excluded "_x" in - (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty + (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty | PatVar(Name id) -> if Id.List.mem id excluded then let new_id = Namegen.next_ident_away id excluded in - (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded), + (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded), (Id.Map.add id new_id Id.Map.empty) else pat, excluded,Id.Map.empty | PatCstr(constr,patl,na) -> @@ -219,7 +219,7 @@ let rec alpha_pat excluded pat = ([],new_excluded,map) patl in - (CAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map + (DAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map let alpha_patl excluded patl = let patl,new_excluded,map = @@ -238,7 +238,7 @@ let alpha_patl excluded patl = let raw_get_pattern_id pat acc = let rec get_pattern_id pat = - match pat.CAst.v with + match DAst.get pat with | PatVar(Anonymous) -> assert false | PatVar(Name id) -> [id] @@ -257,8 +257,8 @@ let get_pattern_id pat = raw_get_pattern_id pat [] let rec alpha_rt excluded rt = let loc = rt.CAst.loc in - let new_rt = CAst.make ?loc @@ - match rt.CAst.v with + let new_rt = DAst.make ?loc @@ + match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt | GLambda(Anonymous,k,t,b) -> let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in @@ -377,7 +377,7 @@ and alpha_br excluded (loc,(ids,patl,res)) = [is_free_in id rt] checks if [id] is a free variable in [rt] *) let is_free_in id = - let rec is_free_in x = CAst.with_loc_val (fun ?loc -> function + let rec is_free_in x = DAst.with_loc_val (fun ?loc -> function | GRef _ -> false | GVar id' -> Id.compare id' id == 0 | GEvar _ -> false @@ -421,7 +421,7 @@ let is_free_in id = -let rec pattern_to_term pt = CAst.with_val (function +let rec pattern_to_term pt = DAst.with_val (function | PatVar Anonymous -> assert false | PatVar(Name id) -> mkGVar id @@ -448,8 +448,8 @@ let rec pattern_to_term pt = CAst.with_val (function let replace_var_by_term x_id term = - let rec replace_var_by_pattern x = CAst.map (function - | GVar id when Id.compare id x_id == 0 -> term.CAst.v + let rec replace_var_by_pattern x = DAst.map (function + | GVar id when Id.compare id x_id == 0 -> DAst.get term | GRef _ | GVar _ | GEvar _ @@ -522,11 +522,10 @@ exception NotUnifiable let rec are_unifiable_aux = function | [] -> () - | eq::eqs -> - let open CAst in - match eq with - | { v = PatVar _ },_ | _, { v = PatVar _ } -> are_unifiable_aux eqs - | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } -> + | (l, r) ::eqs -> + match DAst.get l, DAst.get r with + | PatVar _ ,_ | _, PatVar _-> are_unifiable_aux eqs + | PatCstr(constructor1,cpl1,_), PatCstr(constructor2,cpl2,_) -> if not (eq_constructor constructor2 constructor1) then raise NotUnifiable else @@ -545,11 +544,10 @@ let are_unifiable pat1 pat2 = let rec eq_cases_pattern_aux = function | [] -> () - | eq::eqs -> - let open CAst in - match eq with - | { v = PatVar _ }, { v = PatVar _ } -> eq_cases_pattern_aux eqs - | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } -> + | (l, r) ::eqs -> + match DAst.get l, DAst.get r with + | PatVar _, PatVar _ -> eq_cases_pattern_aux eqs + | PatCstr(constructor1,cpl1,_), PatCstr(constructor2,cpl2,_) -> if not (eq_constructor constructor2 constructor1) then raise NotUnifiable else @@ -569,7 +567,7 @@ let eq_cases_pattern pat1 pat2 = let ids_of_pat = - let rec ids_of_pat ids = CAst.with_val (function + let rec ids_of_pat ids = DAst.with_val (function | PatVar Anonymous -> ids | PatVar(Name id) -> Id.Set.add id ids | PatCstr(_,patl,_) -> List.fold_left ids_of_pat ids patl @@ -583,9 +581,9 @@ let id_of_name = function (* TODO: finish Rec caes *) let ids_of_glob_constr c = - let rec ids_of_glob_constr acc {loc; CAst.v = c} = + let rec ids_of_glob_constr acc c = let idof = id_of_name in - match c with + match DAst.get c with | GVar id -> id::acc | GApp (g,args) -> ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc @@ -610,7 +608,7 @@ let ids_of_glob_constr c = let zeta_normalize = - let rec zeta_normalize_term x = CAst.map (function + let rec zeta_normalize_term x = DAst.map (function | GRef _ | GVar _ | GEvar _ @@ -632,9 +630,9 @@ let zeta_normalize = zeta_normalize_term b ) | GLetIn(Name id,def,typ,b) -> - (zeta_normalize_term (replace_var_by_term id def b)).CAst.v + DAst.get (zeta_normalize_term (replace_var_by_term id def b)) | GLetIn(Anonymous,def,typ,b) -> - (zeta_normalize_term b).CAst.v + DAst.get (zeta_normalize_term b) | GLetTuple(nal,(na,rto),def,b) -> GLetTuple(nal, (na,Option.map zeta_normalize_term rto), @@ -670,19 +668,19 @@ let zeta_normalize = let expand_as = - let rec add_as map ({loc; CAst.v = pat } as rt) = - match pat with + let rec add_as map rt = + match DAst.get rt with | PatVar _ -> map | PatCstr(_,patl,Name id) -> Id.Map.add id (pattern_to_term rt) (List.fold_left add_as map patl) | PatCstr(_,patl,_) -> List.fold_left add_as map patl in - let rec expand_as map = CAst.map (function + let rec expand_as map = DAst.map (function | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt | GVar id as rt -> begin try - (Id.Map.find id map).CAst.v + DAst.get (Id.Map.find id map) with Not_found -> rt end | GApp(f,args) -> GApp(expand_as map f,List.map (expand_as map) args) @@ -723,7 +721,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas (* then we map [rt] to replace the implicit holes by their values *) let rec change rt = - match rt.CAst.v with + match DAst.get rt with | GHole(ImplicitArg(grk,pk,bk),_,_) -> (* we only want to deal with implicit arguments *) ( try (* we scan the new evar map to find the evar corresponding to this hole (by looking the source *) @@ -743,7 +741,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype false [] env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c)) | Evar_empty -> rt (* the hole was not solved : we do nothing *) ) | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *) @@ -765,7 +763,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype false [] env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c)) | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *) in res diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 8769f5668..dab094f91 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -191,7 +191,7 @@ let error msg = user_err Pp.(str msg) let is_rec names = let names = List.fold_right Id.Set.add names Id.Set.empty in let check_id id names = Id.Set.mem id names in - let rec lookup names gt = match gt.CAst.v with + let rec lookup names gt = match DAst.get gt with | GVar(id) -> check_id id names | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false | GCast(b,_) -> lookup names b diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index f4f9ba2bb..5f4d514f3 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -66,7 +66,7 @@ let chop_rlambda_n = if n == 0 then List.rev acc,rt else - match rt.CAst.v with + match DAst.get rt with | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> @@ -80,7 +80,7 @@ let chop_rprod_n = if n == 0 then List.rev acc,rt else - match rt.CAst.v with + match DAst.get rt with | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 3ae922190..96200a98a 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -64,8 +64,8 @@ let string_of_name = id_of_name %> Id.to_string (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) let isVarf f x = - match x with - | { CAst.v = GVar x } -> Id.equal x f + match DAst.get x with + | GVar x -> Id.equal x f | _ -> false (** [ident_global_exist id] returns true if identifier [id] is linked @@ -491,38 +491,38 @@ exception NoMerge let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in - match CAst.(c1.v, c2.v) with + match DAst.get c1, DAst.get c2 with | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> let _ = prstr "\nICI1!\n" in let args = filter_shift_stable lnk (arr1 @ arr2) in - CAst.make @@ GApp ((CAst.make @@ GVar shift.ident) , args) + DAst.make @@ GApp ((DAst.make @@ GVar shift.ident) , args) | GApp(f1, arr1), GApp(f2,arr2) -> raise NoMerge | GLetIn(nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2!\n" in let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in - CAst.make @@ GLetIn(nme,bdy,typ,newtrm) + DAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _, GLetIn(nme,bdy,typ,trm) -> let _ = prstr "\nICI3!\n" in let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in - CAst.make @@ GLetIn(nme,bdy,typ,newtrm) + DAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4!\n" in raise NoMerge let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in - match CAst.(c1.v, c2.v) with + match DAst.get c1, DAst.get c2 with | GApp(f1, arr1), GApp(f2,arr2) -> let args = filter_shift_stable lnk (arr1 @ arr2) in - CAst.make @@ GApp (CAst.make @@ GVar shift.ident, args) + DAst.make @@ GApp (DAst.make @@ GVar shift.ident, args) (* FIXME: what if the function appears in the body of the let? *) | GLetIn(nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2 '!\n" in let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in - CAst.make @@ GLetIn(nme,bdy,typ,newtrm) + DAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _, GLetIn(nme,bdy,typ,trm) -> let _ = prstr "\nICI3 '!\n" in let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in - CAst.make @@ GLetIn(nme,bdy,typ,newtrm) + DAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge @@ -533,16 +533,18 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let rec merge_rec_hyps shift accrec (ltyp:(Name.t * glob_constr option * glob_constr option) list) filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list = + let is_app c = match DAst.get c with GApp _ -> true | _ -> false in let mergeonehyp t reldecl = match reldecl with - | (nme,x,Some ({ CAst.v = GApp(i,args)} as ind)) + | (nme,x,Some ind) when is_app ind -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable) | (nme,Some _,None) -> error "letins with recursive calls not treated yet" | (nme,None,Some _) -> assert false | (nme,None,None) | (nme,Some _,Some _) -> assert false in + let is_app c = match DAst.get c with GApp (f, _) -> isVarf ind2name f | _ -> false in match ltyp with | [] -> [] - | (nme,None,Some ({ CAst. v = GApp(f, largs) } as t)) :: lt when isVarf ind2name f -> + | (nme,None,Some t) :: lt when is_app t -> let rechyps = List.map (mergeonehyp t) accrec in rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable @@ -553,12 +555,13 @@ let build_suppl_reccall (accrec:(Name.t * glob_constr) list) concl2 shift = let find_app (nme:Id.t) ltyp = + let is_app c = match DAst.get c with GApp (f, _) -> isVarf nme f | _ -> false in try ignore (List.map (fun x -> match x with - | _,None,Some { CAst.v = GApp(f,_)} when isVarf nme f -> raise (Found 0) + | _,None,Some c when is_app c -> raise (Found 0) | _ -> ()) ltyp); false @@ -617,7 +620,7 @@ let rec merge_types shift accrec1 rechyps , concl | (nme,None, Some t1)as e ::lt1 -> - (match t1.CAst.v with + (match DAst.get t1 with | GApp(f,carr) when isVarf ind1name f -> merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2 | _ -> @@ -764,7 +767,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) (* first replace rel 1 by a varname *) let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in let substindtyp = EConstr.of_constr substindtyp in - Detyping.detype false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in + Detyping.detype Detyping.Now false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in let lcstr1: glob_constr list = Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in (* add to avoid all indentifiers of lcstr1 *) @@ -848,8 +851,8 @@ let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = match rdecl with | LocalAssum (nme,t) -> let t = EConstr.of_constr t in - let traw = Detyping.detype false [] (Global.env()) Evd.empty t in - CAst.make @@ GProd (nme,Explicit,traw,t2) + let traw = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in + DAst.make @@ GProd (nme,Explicit,traw,t2) | LocalDef _ -> assert false diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d3eccb58d..41a10cba3 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -190,15 +190,15 @@ let (value_f:Term.constr list -> global_reference -> Term.constr) = in let env = Environ.push_rel_context context (Global.env ()) in let glob_body = - CAst.make @@ + DAst.make @@ GCases (RegularStyle,None, - [CAst.make @@ GApp(CAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> CAst.make @@ GVar x_id) rev_x_id_l), + [DAst.make @@ GApp(DAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> DAst.make @@ GVar x_id) rev_x_id_l), (Anonymous,None)], - [Loc.tag ([v_id], [CAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), - [CAst.make @@ PatVar(Name v_id); CAst.make @@ PatVar Anonymous], + [Loc.tag ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), + [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous], Anonymous)], - CAst.make @@ GVar v_id)]) + DAst.make @@ GVar v_id)]) in let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index b847aadf2..99e444010 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -626,19 +626,19 @@ END let subst_var_with_hole occ tid t = let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in let locref = ref 0 in - let rec substrec = function - | { CAst.v = GVar id } as x -> + let rec substrec x = match DAst.get x with + | GVar id -> if Id.equal id tid then (decr occref; if Int.equal !occref 0 then x else (incr locref; - CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ + DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous), Misctypes.IntroAnonymous, None))) else x - | c -> map_glob_constr_left_to_right substrec c in + | _ -> map_glob_constr_left_to_right substrec x in let t' = substrec t in if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t' @@ -646,15 +646,15 @@ let subst_var_with_hole occ tid t = let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in - let rec substrec = function - | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) } -> + let rec substrec c = match DAst.get c with + | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) -> decr occref; if Int.equal !occref 0 then tc else (incr locref; - CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ + DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s)) - | c -> map_glob_constr_left_to_right substrec c + | _ -> map_glob_constr_left_to_right substrec c in substrec t @@ -666,8 +666,8 @@ let hResolve id c occ t = let env = Termops.clear_named_body id (Proofview.Goal.env gl) in let concl = Proofview.Goal.concl gl in let env_ids = Termops.ids_of_context env in - let c_raw = Detyping.detype true env_ids env sigma c in - let t_raw = Detyping.detype true env_ids env sigma t in + let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in + let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in let rec resolve_hole t_hole = try Pretyping.understand env sigma t_hole diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index c874f8d5a..c22e68323 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -123,7 +123,7 @@ END let clsubstitute o c = Proofview.Goal.enter begin fun gl -> - let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in + let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in let hyps = Tacmach.New.pf_ids_of_hyps gl in Tacticals.New.tclMAP (fun cl -> diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index cb7d9b9c0..f4e3ba633 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1040,7 +1040,7 @@ type 'a extra_genarg_printer = let strip_prod_binders_glob_constr n (ty,_) = let rec strip_ty acc n ty = if Int.equal n 0 then (List.rev acc, (ty,None)) else - match ty.CAst.v with + match DAst.get ty with Glob_term.GProd(na,Explicit,a,b) -> strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 0554d4364..fc6ee6aab 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -106,12 +106,12 @@ let intern_ltac_variable ist = function let intern_constr_reference strict ist = function | Ident (_,id) as r when not strict && find_hyp id ist -> - (CAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None)) + (DAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None)) | Ident (_,id) as r when find_var id ist -> - (CAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None)) + (DAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None)) | r -> let loc,_ as lqid = qualid_of_reference r in - CAst.make @@ GRef (locate_global_with_alias lqid,None), + DAst.make @@ GRef (locate_global_with_alias lqid,None), if strict then None else Some (CAst.make @@ CRef (r,None)) (* Internalize an isolated reference in position of tactic *) @@ -264,9 +264,10 @@ let intern_destruction_arg ist = function | clear,ElimOnIdent (loc,id) -> if !strict_check then (* If in a defined tactic, no intros-until *) - match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with - | {loc; CAst.v = GVar id}, _ -> clear,ElimOnIdent (loc,id) - | c -> clear,ElimOnConstr (c,NoBindings) + let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in + match DAst.get c with + | GVar id -> clear,ElimOnIdent (c.CAst.loc,id) + | _ -> clear,ElimOnConstr ((c, p), NoBindings) else clear,ElimOnIdent (loc,id) @@ -348,7 +349,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = ltac_extra = ist.extra; } in let c = Constrintern.interp_reference sign r in - match c.CAst.v with + match DAst.get c with | GRef (r,None) -> Inl (ArgArg (evaluable_of_global_reference ist.genv r,None)) | GVar id -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 2a1e2b682..8fa95ffb0 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -679,8 +679,8 @@ let interp_typed_pattern ist env sigma (_,c,_) = (* Interprets a constr expression *) let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = - try match dest_fun x with - | { CAst.v = GVar id }, _ -> + try match DAst.get (fst (dest_fun x)) with + | GVar id -> let v = Id.Map.find id ist.lfun in sigma, List.map inj_fun (coerce_to_constr_list env v) | _ -> @@ -1043,7 +1043,7 @@ let interp_destruction_arg ist gl arg = if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (loc,id) else - let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in + let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in let f env sigma = let (sigma,c) = interp_open_constr ist env sigma c in (sigma, (c,NoBindings)) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 0f996c65a..d0fe1f957 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -131,7 +131,7 @@ let closed_term_ast l = let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in TacFun([Name(Id.of_string"t")], TacML(Loc.tag (tacname, - [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (CAst.make @@ GVar(Id.of_string"t"),None)); + [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None)); TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index cc0e86684..c29a1fe7c 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -42,10 +42,10 @@ let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) = | Some ghyps -> let clr' = snd (interp_hyps ist gl ghyps) @ clr in if k <> xNoFlag then clr', rcs' else - let open CAst in - match rc with - | { loc; v = GVar id } when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs' - | { loc; v = GRef (VarRef id, _) } when not_section_id id -> + let loc = rc.CAst.loc in + match DAst.get rc with + | GVar id when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs' + | GRef (VarRef id, _) when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs' | _ -> clr', rcs' @@ -68,9 +68,8 @@ let pf_match = pf_apply (fun e s c t -> understand_tcc e s ~expected_type:t c) let apply_rconstr ?ist t gl = (* ppdebug(lazy(str"sigma@apply_rconstr=" ++ pr_evar_map None (project gl))); *) - let open CAst in - let n = match ist, t with - | None, { v = GVar id | GRef (VarRef id,_) } -> pf_nbargs gl (EConstr.mkVar id) + let n = match ist, DAst.get t with + | None, (GVar id | GRef (VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id) | Some ist, _ -> interp_nbargs ist gl t | _ -> anomaly "apply_rconstr without ist and not RVar" in let mkRlemma i = mkRApp t (mkRHoles i) in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 799e969ae..cf5fdf318 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -176,24 +176,26 @@ open Globnames open Misctypes open Decl_kinds -let mkRHole = CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None) +let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None) let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else [] -let rec isRHoles = function { CAst.v = GHole _ } :: cl -> isRHoles cl | cl -> cl = [] -let mkRApp f args = if args = [] then f else CAst.make @@ GApp (f, args) -let mkRVar id = CAst.make @@ GRef (VarRef id,None) -let mkRltacVar id = CAst.make @@ GVar (id) -let mkRCast rc rt = CAst.make @@ GCast (rc, CastConv rt) -let mkRType = CAst.make @@ GSort (GType []) -let mkRProp = CAst.make @@ GSort (GProp) -let mkRArrow rt1 rt2 = CAst.make @@ GProd (Anonymous, Explicit, rt1, rt2) -let mkRConstruct c = CAst.make @@ GRef (ConstructRef c,None) -let mkRInd mind = CAst.make @@ GRef (IndRef mind,None) -let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t) +let rec isRHoles cl = match cl with +| [] -> true +| c :: l -> match DAst.get c with GHole _ -> isRHoles l | _ -> false +let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) +let mkRVar id = DAst.make @@ GRef (VarRef id,None) +let mkRltacVar id = DAst.make @@ GVar (id) +let mkRCast rc rt = DAst.make @@ GCast (rc, CastConv rt) +let mkRType = DAst.make @@ GSort (GType []) +let mkRProp = DAst.make @@ GSort (GProp) +let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2) +let mkRConstruct c = DAst.make @@ GRef (ConstructRef c,None) +let mkRInd mind = DAst.make @@ GRef (IndRef mind,None) +let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t) let rec mkRnat n = - if n <= 0 then CAst.make @@ GRef (Coqlib.glob_O, None) else - mkRApp (CAst.make @@ GRef (Coqlib.glob_S, None)) [mkRnat (n - 1)] + if n <= 0 then DAst.make @@ GRef (Coqlib.glob_O, None) else + mkRApp (DAst.make @@ GRef (Coqlib.glob_S, None)) [mkRnat (n - 1)] let glob_constr ist genv = function | _, Some ce -> @@ -710,7 +712,7 @@ let mkSsrRef name = try locate_reference (ssrqid name) with Not_found -> try locate_reference (ssrtopqid name) with Not_found -> CErrors.user_err (Pp.str "Small scale reflection library not loaded") -let mkSsrRRef name = (CAst.make @@ GRef (mkSsrRef name,None)), None +let mkSsrRRef name = (DAst.make @@ GRef (mkSsrRef name,None)), None let mkSsrConst name env sigma = EConstr.fresh_global env sigma (mkSsrRef name) let pf_mkSsrConst name gl = @@ -845,10 +847,10 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty = let n_binders = ref 0 in let ty = match ty with | a, (t, None) -> - let rec force_type ty = CAst.(map (function + let rec force_type ty = DAst.(map (function | GProd (x, k, s, t) -> incr n_binders; GProd (x, k, s, force_type t) | GLetIn (x, v, oty, t) -> incr n_binders; GLetIn (x, v, oty, force_type t) - | _ -> (mkRCast ty mkRType).v)) ty in + | _ -> DAst.get (mkRCast ty mkRType))) ty in a, (force_type t, None) | _, (_, Some ty) -> let rec force_type ty = CAst.(map (function diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index ab6a60f4e..8b69c3435 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -129,7 +129,7 @@ let newssrcongrtac arg ist gl = let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in pf_saturate gl (EConstr.of_constr eq) 3 in tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args)) - (fun ty -> congrtac (arg, Detyping.detype false [] (pf_env gl) (project gl) ty) ist) + (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) ty) ist) (fun () -> let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in let arrow = EConstr.mkArrow lhs (EConstr.Vars.lift 1 rhs) in diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 8e6329a15..d01bdc1b9 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -184,9 +184,13 @@ let havetac ist mkt ct, mkt cty, mkt (mkCHole None), loc | _, (_, Some ct) -> mkt ct, mkt (mkCHole None), mkt (mkCHole None), None - | _, ({ loc; v = GCast (ct, CastConv cty) }, None) -> - mkl ct, mkl cty, mkl mkRHole, loc - | _, (t, None) -> mkl t, mkl mkRHole, mkl mkRHole, None in + | _, (t, None) -> + begin match DAst.get t with + | GCast (ct, CastConv cty) -> + mkl ct, mkl cty, mkl mkRHole, t.CAst.loc + | _ -> mkl t, mkl mkRHole, mkl mkRHole, None + end + in let gl, cut, sol, itac1, itac2 = match fk, namefst, suff with | FwdHave, true, true -> @@ -323,11 +327,18 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = let mkpats = function | _, Some ((x, _), _) -> fun pats -> IPatId (hoi_id x) :: pats | _ -> fun x -> x in - let open CAst in let ct = match ct with - | (a, (b, Some { v = CCast (_, CastConv cty)})) -> a, (b, Some cty) - | (a, ({ v = GCast (_, CastConv cty) }, None)) -> a, (cty, None) - | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" in + | (a, (b, Some ct)) -> + begin match ct.CAst.v with + | CCast (_, CastConv cty) -> a, (b, Some cty) + | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" + end + | (a, (t, None)) -> + begin match DAst.get t with + | GCast (_, CastConv cty) -> a, (cty, None) + | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" + end + in let cut_implies_goal = not (suff || ghave <> `NoGen) in let c, args, ct, gl = let gens = List.filter (function _, Some _ -> true | _ -> false) gens in @@ -398,11 +409,18 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) = let htac = Tacticals.tclTHEN (introstac ~ist pats) (hinttac ist true hint) in - let open CAst in let c = match c with - | (a, (b, Some { v = CCast (_, CastConv cty)})) -> a, (b, Some cty) - | (a, ({ v = GCast (_, CastConv cty) }, None)) -> a, (cty, None) - | _ -> anomaly "suff: ssr cast hole deleted by typecheck" in + | (a, (b, Some ct)) -> + begin match ct.CAst.v with + | CCast (_, CastConv cty) -> a, (b, Some cty) + | _ -> anomaly "suff: ssr cast hole deleted by typecheck" + end + | (a, (t, None)) -> + begin match DAst.get t with + | GCast (_, CastConv cty) -> a, (cty, None) + | _ -> anomaly "suff: ssr cast hole deleted by typecheck" + end + in let ctac gl = let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in basecuttac "ssr_suff" ty gl in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index db1981228..060225dab 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -342,7 +342,7 @@ let interp_index ist gl idx = | None -> begin match Tacinterp.Value.to_constr v with | Some c -> - let rc = Detyping.detype false [] (pf_env gl) (project gl) c in + let rc = Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) c in begin match Notation.uninterp_prim_token rc with | _, Constrexpr.Numeral (s,b) -> let n = int_of_string s in if b then n else -n @@ -1062,32 +1062,32 @@ let rec format_glob_decl h0 d0 = match h0, d0 with Bdef (x, None, v) :: format_glob_decl [] d | _, [] -> [] -let rec format_glob_constr h0 c0 = let open CAst in match h0, c0 with - | BFvar :: h, { v = GLambda (x, _, _, c) } -> +let rec format_glob_constr h0 c0 = match h0, DAst.get c0 with + | BFvar :: h, GLambda (x, _, _, c) -> let bs, c' = format_glob_constr h c in Bvar x :: bs, c' - | BFdecl 1 :: h, { v = GLambda (x, _, t, c) } -> + | BFdecl 1 :: h, GLambda (x, _, t, c) -> let bs, c' = format_glob_constr h c in Bdecl ([x], t) :: bs, c' - | BFdecl n :: h, { v = GLambda (x, _, t, c) } when n > 1 -> + | BFdecl n :: h, GLambda (x, _, t, c) when n > 1 -> begin match format_glob_constr (BFdecl (n - 1) :: h) c with | Bdecl (xs, _) :: bs, c' -> Bdecl (x :: xs, t) :: bs, c' | _ -> [Bdecl ([x], t)], c end - | BFdef :: h, { v = GLetIn(x, v, oty, c) } -> + | BFdef :: h, GLetIn(x, v, oty, c) -> let bs, c' = format_glob_constr h c in Bdef (x, oty, v) :: bs, c' - | [BFcast], { v = GCast (c, CastConv t) } -> + | [BFcast], GCast (c, CastConv t) -> [Bcast t], c - | BFrec (has_str, has_cast) :: h, { v = GRec (f, _, bl, t, c) } + | BFrec (has_str, has_cast) :: h, GRec (f, _, bl, t, c) when Array.length c = 1 -> let bs = format_glob_decl h bl.(0) in let bstr = match has_str, f with | true, GFix ([|Some i, GStructRec|], _) -> mkBstruct i bs | _ -> [] in bs @ bstr @ (if has_cast then [Bcast t.(0)] else []), c.(0) - | _, c -> - [], c + | _, _ -> + [], c0 (** Forward chaining argument *) diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 9c59d83d4..507b4631b 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -292,7 +292,7 @@ let interp_search_notation ?loc tag okey = err (pr_ntn ntn ++ str " is an n-ary notation"); let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in let rec sub () = function - | NVar x when List.mem_assoc x nvars -> CAst.make ?loc @@ GPatVar (FirstOrderPatVar x) + | NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x) | c -> glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), x) sub () c in let _, npat = Patternops.pattern_of_glob_constr (sub () body) in @@ -467,10 +467,10 @@ let pr_raw_ssrhintref prc _ _ = let open CAst in function prc c ++ str "|" ++ int (List.length args) | c -> prc c -let pr_rawhintref = let open CAst in function - | { v = GApp (f, args) } when isRHoles args -> +let pr_rawhintref c = match DAst.get c with + | GApp (f, args) when isRHoles args -> pr_glob_constr f ++ str "|" ++ int (List.length args) - | c -> pr_glob_constr c + | _ -> pr_glob_constr c let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 338ecccc2..61b65e347 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -59,13 +59,13 @@ let glob_view_hints lvh = let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh)) -let interp_view ist si env sigma gv v rid = - let open CAst in - match v with - | { v = GApp ( { v = GHole _ } , rargs); loc } -> - let rv = make ?loc @@ GApp (rid, rargs) in +let interp_view ist si env sigma gv rv rid = + match DAst.get rv with + | GApp (h, rargs) when (match DAst.get h with GHole _ -> true | _ -> false) -> + let loc = rv.CAst.loc in + let rv = DAst.make ?loc @@ GApp (rid, rargs) in snd (interp_open_constr ist (re_sig si sigma) (rv, None)) - | rv -> + | _ -> let interp rc rargs = interp_open_constr ist (re_sig si sigma) (mkRApp rc rargs, None) in let rec simple_view rargs n = diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index f6300ab7e..2e5522b83 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -134,6 +134,10 @@ let dC t = CastConv t let isCVar = function { CAst.v = CRef (Ident _, _) } -> true | _ -> false let destCVar = function { CAst.v = CRef (Ident (_, id), _) } -> id | _ -> CErrors.anomaly (str"not a CRef.") +let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _) -> true | _ -> false +let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c) + | _ -> CErrors.anomaly (str "not a GLambda") +let isGHole c = match DAst.get c with GHole _ -> true | _ -> false let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ CLambdaN ([[Loc.tag ?loc name], Default Explicit, ty], t) @@ -141,10 +145,10 @@ let mkCLetIn ?loc name bo t = CAst.make ?loc @@ CLetIn ((Loc.tag ?loc name), bo, None, t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty) (** Constructors for rawconstr *) -let mkRHole = CAst.make @@ GHole (InternalHole, IntroAnonymous, None) -let mkRApp f args = if args = [] then f else CAst.make @@ GApp (f, args) -let mkRCast rc rt = CAst.make @@ GCast (rc, dC rt) -let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t) +let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None) +let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) +let mkRCast rc rt = DAst.make @@ GCast (rc, dC rt) +let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t) (* ssrterm conbinators *) let combineCG t1 t2 f g = match t1, t2 with @@ -980,11 +984,10 @@ let pr_rpattern = pr_pattern type pattern = Evd.evar_map * (constr, constr) ssrpattern - -let id_of_cpattern = let open CAst in function - | _,(_,Some { v = CRef (Ident (_, x), _) } ) -> Some x - | _,(_,Some { v = CAppExpl ((_, Ident (_, x), _), []) } ) -> Some x - | _,({ v = GRef (VarRef x, _)} ,None) -> Some x +let id_of_cpattern (_, (c1, c2)) = let open CAst in match DAst.get c1, c2 with + | _, Some { v = CRef (Ident (_, x), _) } -> Some x + | _, Some { v = CAppExpl ((_, Ident (_, x), _), []) } -> Some x + | GRef (VarRef x, _), None -> Some x | _ -> None let id_of_Cterm t = match id_of_cpattern t with | Some x -> x @@ -1082,10 +1085,11 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = let eAsXInT e x t = E_As_X_In_T(e,x,t) in let mkG ?(k=' ') x = k,(x,None) in let decode ist t ?reccall f g = - let open CAst in - try match (pf_intern_term ist gl t) with - | { v = GCast({ v = GHole _},CastConv({ v = GLambda(Name x,_,_,c)})) } -> f x (' ',(c,None)) - | { v = GVar id } + try match DAst.get (pf_intern_term ist gl t) with + | GCast(t,CastConv c) when isGHole t && isGLambda c-> + let (x, c) = destGLambda c in + f x (' ',(c,None)) + | GVar id when Id.Map.mem id ist.lfun && not(Option.is_empty reccall) && not(Option.is_empty wit_ssrpatternarg) -> @@ -1126,19 +1130,27 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = thin name sigma e) sigma new_evars in sigma in - let red = let rec decode_red (ist,red) = let open CAst in match red with - | T(k,({ v = GCast ({ v = GHole _ },CastConv({ v = GLambda (Name id,_,_,t)}))},None)) - when let id = Id.to_string id in let len = String.length id in + let red = let rec decode_red (ist,red) = match red with + | T(k,(t,None)) -> + begin match DAst.get t with + | GCast (c,CastConv t) + when isGHole c && + let (id, t) = destGLambda t in + let id = Id.to_string id in let len = String.length id in (len > 8 && String.sub id 0 8 = "_ssrpat_") -> + let (id, t) = destGLambda t in let id = Id.to_string id in let len = String.length id in - (match String.sub id 8 (len - 8), t with - | "In", { v = GApp( _, [t]) } -> decodeG t xInT (fun x -> T x) - | "In", { v = GApp( _, [e; t]) } -> decodeG t (eInXInT (mkG e)) (bad_enc id) - | "In", { v = GApp( _, [e; t; e_in_t]) } -> + (match String.sub id 8 (len - 8), DAst.get t with + | "In", GApp( _, [t]) -> decodeG t xInT (fun x -> T x) + | "In", GApp( _, [e; t]) -> decodeG t (eInXInT (mkG e)) (bad_enc id) + | "In", GApp( _, [e; t; e_in_t]) -> decodeG t (eInXInT (mkG e)) (fun _ -> decodeG e_in_t xInT (fun _ -> assert false)) - | "As", { v = GApp(_, [e; t]) } -> decodeG t (eAsXInT (mkG e)) (bad_enc id) + | "As", GApp(_, [e; t]) -> decodeG t (eAsXInT (mkG e)) (bad_enc id) | _ -> bad_enc id ()) + | _ -> + decode ist ~reccall:decode_red (k, (t, None)) xInT (fun x -> T x) + end | T t -> decode ist ~reccall:decode_red t xInT (fun x -> T x) | In_T t -> decode ist t inXInT inT | X_In_T (e,t) -> decode ist t (eInXInT e) (fun x -> xInT (id_of_Cterm e) x) @@ -1163,7 +1175,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); let mkXLetIn ?loc x (a,(g,c)) = match c with | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)) - | None -> a,(CAst.make ?loc @@ GLetIn (x, CAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in + | None -> a,(DAst.make ?loc @@ GLetIn (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in match red with | T t -> let sigma, t = interp_term ist gl t in sigma, T t | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t @@ -1336,10 +1348,10 @@ let pf_fill_occ_term gl occ t = let cl,(_,t) = fill_occ_term env concl occ sigma0 t in cl, t -let cpattern_of_id id = ' ', (CAst.make @@ GRef (VarRef id, None), None) +let cpattern_of_id id = ' ', (DAst.make @@ GRef (VarRef id, None), None) -let is_wildcard : cpattern -> bool = function - | _,(_,Some { CAst.v = CHole _ } | { CAst.v = GHole _ } ,None) -> true +let is_wildcard ((_, (l, r)) : cpattern) : bool = match DAst.get l, r with + | _, Some { CAst.v = CHole _ } | GHole _, None -> true | _ -> false (* "ssrpattern" *) diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index c41ec39cb..b299ff853 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -25,6 +25,10 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + let ascii_module = ["Coq";"Strings";"Ascii"] let ascii_path = make_path ascii_module "ascii" @@ -42,9 +46,9 @@ let interp_ascii ?loc p = let rec aux n p = if Int.equal n 0 then [] else let mp = p mod 2 in - (CAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None)) + (DAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None)) :: (aux (n-1) (p/2)) in - CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) + DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) let interp_ascii_string ?loc s = let p = @@ -60,12 +64,12 @@ let interp_ascii_string ?loc s = let uninterp_ascii r = let rec uninterp_bool_list n = function | [] when Int.equal n 0 -> 0 - | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r glob_true -> 1+2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r glob_false -> 2*(uninterp_bool_list (n-1) l) | _ -> raise Non_closed_ascii in try - let aux = function - | { CAst.v = GApp ({ CAst.v = GRef (k,_)},l) } when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l + let aux c = match DAst.get c with + | GApp (r, l) when is_gr r (force glob_Ascii) -> uninterp_bool_list 8 l | _ -> raise Non_closed_ascii in Some (aux r) with @@ -75,10 +79,10 @@ let make_ascii_string n = if n>=32 && n<=126 then String.make 1 (char_of_int n) else Printf.sprintf "%03d" n -let uninterp_ascii_string r = Option.map make_ascii_string (uninterp_ascii r) +let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r) let _ = Notation.declare_string_interpreter "char_scope" (ascii_path,ascii_module) interp_ascii_string - ([CAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) + ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml index af64b1479..0dff047a3 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -23,6 +23,10 @@ open Glob_term let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + let make_mind mp id = Names.MutInd.make2 mp (Label.make id) let make_mind_mpfile dir id = make_mind (ModPath.MPfile (make_dir dir)) id let make_mind_mpdot dir modname id = @@ -49,9 +53,9 @@ exception Non_closed (* parses a *non-negative* integer (from bigint.ml) into an int31 wraps modulo 2^31 *) let int31_of_pos_bigint ?loc n = - let ref_construct = CAst.make ?loc (GRef (int31_construct, None)) in - let ref_0 = CAst.make ?loc (GRef (int31_0, None)) in - let ref_1 = CAst.make ?loc (GRef (int31_1, None)) in + let ref_construct = DAst.make ?loc (GRef (int31_construct, None)) in + let ref_0 = DAst.make ?loc (GRef (int31_0, None)) in + let ref_1 = DAst.make ?loc (GRef (int31_1, None)) in let rec args counter n = if counter <= 0 then [] @@ -59,7 +63,7 @@ let int31_of_pos_bigint ?loc n = let (q,r) = div2_with_rest n in (if r then ref_1 else ref_0)::(args (counter-1) q) in - CAst.make ?loc (GApp (ref_construct, List.rev (args 31 n))) + DAst.make ?loc (GApp (ref_construct, List.rev (args 31 n))) let error_negative ?loc = CErrors.user_err ?loc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.") @@ -76,15 +80,15 @@ let bigint_of_int31 = let rec args_parsing args cur = match args with | [] -> cur - | { CAst.v = GRef (b,_) }::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur) - | { CAst.v = GRef (b,_) }::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur)) + | r::l when is_gr r int31_0 -> args_parsing l (mult_2 cur) + | r::l when is_gr r int31_1 -> args_parsing l (add_1 (mult_2 cur)) | _ -> raise Non_closed in - function - | { CAst.v = GApp ({ CAst.v = GRef (c, _) }, args) } when eq_gr c int31_construct -> args_parsing args zero + fun c -> match DAst.get c with + | GApp (r, args) when is_gr r int31_construct -> args_parsing args zero | _ -> raise Non_closed -let uninterp_int31 i = +let uninterp_int31 (AnyGlobConstr i) = try Some (bigint_of_int31 i) with Non_closed -> @@ -94,6 +98,6 @@ let uninterp_int31 i = let _ = Notation.declare_numeral_interpreter int31_scope (int31_path, int31_module) interp_int31 - ([CAst.make (GRef (int31_construct, None))], + ([DAst.make (GRef (int31_construct, None))], uninterp_int31, true) diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 524a5c522..2f9870cf9 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -37,11 +37,11 @@ let warn_large_nat = let nat_of_int ?loc n = if is_pos_or_zero n then begin if less_than threshold n then warn_large_nat (); - let ref_O = CAst.make ?loc @@ GRef (glob_O, None) in - let ref_S = CAst.make ?loc @@ GRef (glob_S, None) in + let ref_O = DAst.make ?loc @@ GRef (glob_O, None) in + let ref_S = DAst.make ?loc @@ GRef (glob_S, None) in let rec mk_nat acc n = if n <> zero then - mk_nat (CAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) + mk_nat (DAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) else acc in @@ -56,13 +56,17 @@ let nat_of_int ?loc n = exception Non_closed_number -let rec int_of_nat x = CAst.with_val (function - | GApp ({ CAst.v = GRef (s,_) } ,[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) +let rec int_of_nat x = DAst.with_val (function + | GApp (r, [a]) -> + begin match DAst.get r with + | GRef (s,_) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) + | _ -> raise Non_closed_number + end | GRef (z,_) when Globnames.eq_gr z glob_O -> zero | _ -> raise Non_closed_number ) x -let uninterp_nat p = +let uninterp_nat (AnyGlobConstr p) = try Some (int_of_nat p) with @@ -75,4 +79,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,datatypes_module_name) nat_of_int - ([CAst.make @@ GRef (glob_S,None); CAst.make @@ GRef (glob_O,None)], uninterp_nat, true) + ([DAst.make @@ GRef (glob_S,None); DAst.make @@ GRef (glob_O,None)], uninterp_nat, true) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 06117de79..88ff38c6d 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -27,6 +27,10 @@ let binnums = ["Coq";"Numbers";"BinNums"] let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + let positive_path = make_path binnums "positive" (* TODO: temporary hack *) @@ -42,13 +46,13 @@ let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH let pos_of_bignat ?loc x = - let ref_xI = CAst.make @@ GRef (glob_xI, None) in - let ref_xH = CAst.make @@ GRef (glob_xH, None) in - let ref_xO = CAst.make @@ GRef (glob_xO, None) in + let ref_xI = DAst.make @@ GRef (glob_xI, None) in + let ref_xH = DAst.make @@ GRef (glob_xH, None) in + let ref_xO = DAst.make @@ GRef (glob_xO, None) in let rec pos_of x = match div2_with_rest x with - | (q,false) -> CAst.make @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> CAst.make @@ GApp (ref_xI,[pos_of q]) + | (q,false) -> DAst.make @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q]) | (q,true) -> ref_xH in pos_of x @@ -57,10 +61,10 @@ let pos_of_bignat ?loc x = (* Printing positive via scopes *) (**********************************************************************) -let rec bignat_of_pos = function - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) - | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_xH -> Bigint.one +let rec bignat_of_pos c = match DAst.get c with + | GApp (r, [a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) + | GApp (r, [a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) + | GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one | _ -> raise Non_closed_number (**********************************************************************) @@ -81,18 +85,18 @@ let z_of_int ?loc n = if not (Bigint.equal n zero) then let sgn, n = if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - CAst.make @@ GApp(CAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n]) + DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n]) else - CAst.make @@ GRef (glob_ZERO, None) + DAst.make @@ GRef (glob_ZERO, None) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) -let bigint_of_z = function - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_POS -> bignat_of_pos a - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) - | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_ZERO -> Bigint.zero +let bigint_of_z c = match DAst.get c with + | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a + | GApp (r,[a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) + | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number (**********************************************************************) @@ -108,18 +112,18 @@ let make_path dir id = Globnames.encode_con dir (Id.of_string id) let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR") let r_of_int ?loc z = - CAst.make @@ GApp (CAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z]) + DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z]) (**********************************************************************) (* Printing R via scopes *) (**********************************************************************) -let bigint_of_r = function - | { CAst.v = GApp ({ CAst.v = GRef (o,_) }, [a]) } when Globnames.eq_gr o glob_IZR -> +let bigint_of_r c = match DAst.get c with + | GApp (r, [a]) when is_gr r glob_IZR -> bigint_of_z a | _ -> raise Non_closed_number -let uninterp_r p = +let uninterp_r (AnyGlobConstr p) = try Some (bigint_of_r p) with Non_closed_number -> @@ -128,6 +132,6 @@ let uninterp_r p = let _ = Notation.declare_numeral_interpreter "R_scope" (r_path,["Coq";"Reals";"Rdefinitions"]) r_of_int - ([CAst.make @@ GRef (glob_IZR, None)], + ([DAst.make @@ GRef (glob_IZR, None)], uninterp_r, false) diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index b7f13b040..cc82fc94c 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -31,25 +31,29 @@ let make_reference id = find_reference "String interpretation" string_module id let glob_String = lazy (make_reference "String") let glob_EmptyString = lazy (make_reference "EmptyString") +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + open Lazy let interp_string ?loc s = let le = String.length s in let rec aux n = - if n = le then CAst.make ?loc @@ GRef (force glob_EmptyString, None) else - CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef (force glob_String, None), + if n = le then DAst.make ?loc @@ GRef (force glob_EmptyString, None) else + DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef (force glob_String, None), [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)]) in aux 0 -let uninterp_string r = +let uninterp_string (AnyGlobConstr r) = try let b = Buffer.create 16 in - let rec aux = function - | { CAst.v = GApp ({ CAst.v = GRef (k,_) },[a;s]) } when eq_gr k (force glob_String) -> + let rec aux c = match DAst.get c with + | GApp (k,[a;s]) when is_gr k (force glob_String) -> (match uninterp_ascii a with | Some c -> Buffer.add_char b (Char.chr c); aux s | _ -> raise Non_closed_string) - | { CAst.v = GRef (z,_) } when eq_gr z (force glob_EmptyString) -> + | GRef (z,_) when eq_gr z (force glob_EmptyString) -> Some (Buffer.contents b) | _ -> raise Non_closed_string @@ -61,6 +65,6 @@ let _ = Notation.declare_string_interpreter "string_scope" (string_path,["Coq";"Strings";"String"]) interp_string - ([CAst.make @@ GRef (static_glob_String,None); - CAst.make @@ GRef (static_glob_EmptyString,None)], + ([DAst.make @@ GRef (static_glob_String,None); + DAst.make @@ GRef (static_glob_EmptyString,None)], uninterp_string, true) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index af3df2889..0d743a2b5 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -45,13 +45,13 @@ let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH let pos_of_bignat ?loc x = - let ref_xI = CAst.make ?loc @@ GRef (glob_xI, None) in - let ref_xH = CAst.make ?loc @@ GRef (glob_xH, None) in - let ref_xO = CAst.make ?loc @@ GRef (glob_xO, None) in + let ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in + let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in + let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in let rec pos_of x = match div2_with_rest x with - | (q,false) -> CAst.make ?loc @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> CAst.make ?loc @@ GApp (ref_xI,[pos_of q]) + | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q]) | (q,true) -> ref_xH in pos_of x @@ -68,14 +68,18 @@ let interp_positive ?loc n = (* Printing positive via scopes *) (**********************************************************************) -let rec bignat_of_pos x = CAst.with_val (function - | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) - | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + +let rec bignat_of_pos x = DAst.with_val (function + | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) + | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) | GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one | _ -> raise Non_closed_number ) x -let uninterp_positive p = +let uninterp_positive (AnyGlobConstr p) = try Some (bignat_of_pos p) with Non_closed_number -> @@ -88,9 +92,9 @@ let uninterp_positive p = let _ = Notation.declare_numeral_interpreter "positive_scope" (positive_path,binnums) interp_positive - ([CAst.make @@ GRef (glob_xI, None); - CAst.make @@ GRef (glob_xO, None); - CAst.make @@ GRef (glob_xH, None)], + ([DAst.make @@ GRef (glob_xI, None); + DAst.make @@ GRef (glob_xO, None); + DAst.make @@ GRef (glob_xH, None)], uninterp_positive, true) @@ -107,9 +111,9 @@ let glob_Npos = ConstructRef path_of_Npos let n_path = make_path binnums "N" -let n_of_binnat ?loc pos_or_neg n = CAst.make ?loc @@ +let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@ if not (Bigint.equal n zero) then - GApp(CAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) + GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) else GRef(glob_N0, None) @@ -124,13 +128,13 @@ let n_of_int ?loc n = (* Printing N via scopes *) (**********************************************************************) -let bignat_of_n = CAst.with_val (function - | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a +let bignat_of_n n = DAst.with_val (function + | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a | GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero | _ -> raise Non_closed_number - ) + ) n -let uninterp_n p = +let uninterp_n (AnyGlobConstr p) = try Some (bignat_of_n p) with Non_closed_number -> None @@ -140,8 +144,8 @@ let uninterp_n p = let _ = Notation.declare_numeral_interpreter "N_scope" (n_path,binnums) n_of_int - ([CAst.make @@ GRef (glob_N0, None); - CAst.make @@ GRef (glob_Npos, None)], + ([DAst.make @@ GRef (glob_N0, None); + DAst.make @@ GRef (glob_Npos, None)], uninterp_n, true) @@ -163,22 +167,22 @@ let z_of_int ?loc n = if not (Bigint.equal n zero) then let sgn, n = if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - CAst.make ?loc @@ GApp(CAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) + DAst.make ?loc @@ GApp(DAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) else - CAst.make ?loc @@ GRef(glob_ZERO, None) + DAst.make ?loc @@ GRef(glob_ZERO, None) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) -let bigint_of_z = CAst.with_val (function - | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a - | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) +let bigint_of_z z = DAst.with_val (function + | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a + | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number - ) + ) z -let uninterp_z p = +let uninterp_z (AnyGlobConstr p) = try Some (bigint_of_z p) with Non_closed_number -> None @@ -189,8 +193,8 @@ let uninterp_z p = let _ = Notation.declare_numeral_interpreter "Z_scope" (z_path,binnums) z_of_int - ([CAst.make @@ GRef (glob_ZERO, None); - CAst.make @@ GRef (glob_POS, None); - CAst.make @@ GRef (glob_NEG, None)], + ([DAst.make @@ GRef (glob_ZERO, None); + DAst.make @@ GRef (glob_POS, None); + DAst.make @@ GRef (glob_NEG, None)], uninterp_z, true) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 63775d737..7455587c0 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -94,7 +94,7 @@ let msg_may_need_inversion () = (* Utils *) let make_anonymous_patvars n = - List.make n (CAst.make @@ PatVar Anonymous) + List.make n (DAst.make @@ PatVar Anonymous) (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *) @@ -177,7 +177,7 @@ and build_glob_pattern args = function | Top -> args | MakeConstructor (pci, rh) -> glob_pattern_of_partial_history - [CAst.make @@ PatCstr (pci, args, Anonymous)] rh + [DAst.make @@ PatCstr (pci, args, Anonymous)] rh let complete_history = glob_pattern_of_partial_history [] @@ -187,12 +187,12 @@ let pop_history_pattern = function | Continuation (0, l, Top) -> Result (List.rev l) | Continuation (0, l, MakeConstructor (pci, rh)) -> - feed_history (CAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh + feed_history (DAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh | _ -> anomaly (Pp.str "Constructor not yet filled with its arguments.") let pop_history h = - feed_history (CAst.make @@ PatVar Anonymous) h + feed_history (DAst.make @@ PatVar Anonymous) h (* Builds a continuation expecting [n] arguments and building [ci] applied to this [n] arguments *) @@ -273,8 +273,10 @@ type 'a pattern_matching_problem = let rec find_row_ind = function [] -> None - | { CAst.v = PatVar _ } :: l -> find_row_ind l - | { CAst.v = PatCstr(c,_,_) ; loc } :: _ -> Some (loc,c) + | p :: l -> + match DAst.get p with + | PatVar _ -> find_row_ind l + | PatCstr(c,_,_) -> Some (p.CAst.loc,c) let inductive_template evdref env tmloc ind = let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in @@ -348,7 +350,7 @@ let find_tomatch_tycon evdref env loc = function empty_tycon,None let make_return_predicate_ltac_lvar sigma na tm c lvar = - match na, tm.CAst.v with + match na, DAst.get tm with | Name id, (GVar id' | GRef (Globnames.VarRef id', _)) when Id.equal id id' -> if Id.Map.mem id lvar.ltac_genargs then let ltac_genargs = Id.Map.remove id lvar.ltac_genargs in @@ -447,7 +449,7 @@ let current_pattern eqn = | pat::_ -> pat | [] -> anomaly (Pp.str "Empty list of patterns.") -let alias_of_pat = CAst.with_val (function +let alias_of_pat = DAst.with_val (function | PatVar name -> name | PatCstr(_,_,name) -> name ) @@ -493,13 +495,14 @@ let rec adjust_local_defs ?loc = function | (pat :: pats, LocalAssum _ :: decls) -> pat :: adjust_local_defs ?loc (pats,decls) | (pats, LocalDef _ :: decls) -> - (CAst.make ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls) + (DAst.make ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls) | [], [] -> [] | _ -> raise NotAdjustable -let check_and_adjust_constructor env ind cstrs = function - | { CAst.v = PatVar _ } as pat -> pat - | { CAst.v = PatCstr (((_,i) as cstr),args,alias) ; loc } as pat -> +let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with + | PatVar _ -> pat + | PatCstr (((_,i) as cstr),args,alias) -> + let loc = pat.CAst.loc in (* Check it is constructor of the right type *) let ind' = inductive_of_constructor cstr in if eq_ind ind' ind then @@ -510,7 +513,7 @@ let check_and_adjust_constructor env ind cstrs = function else try let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args) - in CAst.make ?loc @@ PatCstr (cstr, args', alias) + in DAst.make ?loc @@ PatCstr (cstr, args', alias) with NotAdjustable -> error_wrong_numarg_constructor ?loc env cstr nb_args_constr else @@ -522,9 +525,12 @@ let check_and_adjust_constructor env ind cstrs = function let check_all_variables env sigma typ mat = List.iter - (fun eqn -> match current_pattern eqn with - | { CAst.v = PatVar id } -> () - | { CAst.v = PatCstr (cstr_sp,_,_); loc } -> + (fun eqn -> + let pat = current_pattern eqn in + match DAst.get pat with + | PatVar id -> () + | PatCstr (cstr_sp,_,_) -> + let loc = pat.CAst.loc in error_bad_pattern ?loc env sigma cstr_sp typ) mat @@ -549,9 +555,9 @@ let occur_in_rhs na rhs = | Anonymous -> false | Name id -> Id.List.mem id rhs.rhs_vars -let is_dep_patt_in eqn = function - | { CAst.v = PatVar name } -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs - | { CAst.v = PatCstr _ } -> true +let is_dep_patt_in eqn pat = match DAst.get pat with + | PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs + | PatCstr _ -> true let mk_dep_patt_row (pats,_,eqn) = List.map (is_dep_patt_in eqn) pats @@ -771,7 +777,7 @@ let recover_and_adjust_alias_names names sign = | x::names, LocalAssum (_,t)::sign -> (x, LocalAssum (alias_of_pat x,t)) :: aux (names,sign) | names, (LocalDef (na,_,_) as decl)::sign -> - (CAst.make @@ PatVar na, decl) :: aux (names,sign) + (DAst.make @@ PatVar na, decl) :: aux (names,sign) | _ -> assert false in List.split (aux (names,sign)) @@ -987,7 +993,7 @@ let use_unit_judge evd = evd', j let add_assert_false_case pb tomatch = - let pats = List.map (fun _ -> CAst.make @@ PatVar Anonymous) tomatch in + let pats = List.map (fun _ -> DAst.make @@ PatVar Anonymous) tomatch in let aliasnames = List.map_filter (function Alias _ | NonDepAlias -> Some Anonymous | _ -> None) tomatch in @@ -1184,9 +1190,9 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs = (************************************************************************) (* Sorting equations by constructor *) -let rec irrefutable env = function - | { CAst.v = PatVar name } -> true - | { CAst.v = PatCstr (cstr,args,_) } -> +let rec irrefutable env pat = match DAst.get pat with + | PatVar name -> true + | PatCstr (cstr,args,_) -> let ind = inductive_of_constructor cstr in let (_,mip) = Inductive.lookup_mind_specif env ind in let one_constr = Int.equal (Array.length mip.mind_user_lc) 1 in @@ -1206,15 +1212,15 @@ let group_equations pb ind current cstrs mat = (fun eqn () -> let rest = remove_current_pattern eqn in let pat = current_pattern eqn in - match check_and_adjust_constructor pb.env ind cstrs pat with - | { CAst.v = PatVar name } -> + match DAst.get (check_and_adjust_constructor pb.env ind cstrs pat) with + | PatVar name -> (* This is a default clause that we expand *) for i=1 to Array.length cstrs do let args = make_anonymous_patvars cstrs.(i-1).cs_nargs in brs.(i-1) <- (args, name, rest) :: brs.(i-1) done; if !only_default == None then only_default := Some true - | { CAst.v = PatCstr (((_,i)),args,name) ; loc } -> + | PatCstr (((_,i)),args,name) -> (* This is a regular clause *) only_default := Some false; brs.(i-1) <- (args, name, rest) :: brs.(i-1)) mat () in @@ -1745,16 +1751,16 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = let build_inversion_problem loc env sigma tms t = let make_patvar t (subst,avoid) = let id = next_name_away (named_hd env sigma t Anonymous) avoid in - CAst.make @@ PatVar (Name id), ((id,t)::subst, id::avoid) in + DAst.make @@ PatVar (Name id), ((id,t)::subst, id::avoid) in let rec reveal_pattern t (subst,avoid as acc) = match EConstr.kind sigma (whd_all env sigma t) with - | Construct (cstr,u) -> CAst.make (PatCstr (cstr,[],Anonymous)), acc + | Construct (cstr,u) -> DAst.make (PatCstr (cstr,[],Anonymous)), acc | App (f,v) when isConstruct sigma f -> let cstr,u = destConstruct sigma f in let n = constructor_nrealargs_env env cstr in let l = List.lastn n (Array.to_list v) in let l,acc = List.fold_right_map reveal_pattern l acc in - CAst.make (PatCstr (cstr,l,Anonymous)), acc + DAst.make (PatCstr (cstr,l,Anonymous)), acc | _ -> make_patvar t acc in let rec aux n env acc_sign tms acc = match tms with @@ -1830,7 +1836,7 @@ let build_inversion_problem loc env sigma tms t = (* No need for a catch all clause *) [] else - [ { patterns = List.map (fun _ -> CAst.make @@ PatVar Anonymous) patl; + [ { patterns = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl; alias_stack = []; eqn_loc = None; used = ref false; @@ -2094,14 +2100,14 @@ let mk_JMeq evdref typ x typ' y = let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] -let hole na = CAst.make @@ +let hole na = DAst.make @@ GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na), Misctypes.IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = let rec typ env (ty, realargs) pat avoid = let loc = pat.CAst.loc in - match pat.CAst.v with + match DAst.get pat with | PatVar name -> let name, avoid = match name with Name n -> name, avoid @@ -2109,7 +2115,7 @@ let constr_of_pat env evdref arsign pat avoid = let previd, id = prime avoid (Name (Id.of_string "wildcard")) in Name id, id :: avoid in - ((CAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, + ((DAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid) | PatCstr (((_, i) as cstr),args,alias) -> let cind = inductive_of_constructor cstr in @@ -2140,7 +2146,7 @@ let constr_of_pat env evdref arsign pat avoid = in let args = List.rev args in let patargs = List.rev patargs in - let pat' = CAst.make ?loc @@ PatCstr (cstr, patargs, alias) in + let pat' = DAst.make ?loc @@ PatCstr (cstr, patargs, alias) in let cstr = mkConstructU (on_snd EInstance.make ci.cs_cstr) in let app = applist (cstr, List.map (lift (List.length sign)) params) in let app = applist (app, args) in @@ -2196,18 +2202,18 @@ let vars_of_ctx sigma ctx = match decl with | LocalDef (na,t',t) when is_topvar sigma t' -> prev, - (CAst.make @@ GApp ( - (CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), - [hole na; CAst.make @@ GVar prev])) :: vars + (DAst.make @@ GApp ( + (DAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), + [hole na; DAst.make @@ GVar prev])) :: vars | _ -> match RelDecl.get_name decl with Anonymous -> invalid_arg "vars_of_ctx" - | Name n -> n, (CAst.make @@ GVar n) :: vars) + | Name n -> n, (DAst.make @@ GVar n) :: vars) ctx (Id.of_string "vars_of_ctx_error", []) in List.rev y let rec is_included x y = - match CAst.(x.v, y.v) with + match DAst.get x, DAst.get y with | PatVar _, _ -> true | _, PatVar _ -> true | PatCstr ((_, i), args, alias), PatCstr ((_, i'), args', alias') -> @@ -2325,13 +2331,13 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in let branch = - let bref = CAst.make @@ GVar branch_name in + let bref = DAst.make @@ GVar branch_name in match vars_of_ctx !evdref rhs_rels with [] -> bref - | l -> CAst.make @@ GApp (bref, l) + | l -> DAst.make @@ GApp (bref, l) in let branch = match ineqs with - Some _ -> CAst.make @@ GApp (branch, [ hole Anonymous ]) + Some _ -> DAst.make @@ GApp (branch, [ hole Anonymous ]) | None -> branch in incr i; diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 535a62046..fc0a650bc 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -77,8 +77,8 @@ let apply_pattern_coercion ?loc pat p = List.fold_left (fun pat (co,n) -> let f i = - if i<n then (CAst.make ?loc @@ Glob_term.PatVar Anonymous) else pat in - CAst.make ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous)) + if i<n then (DAst.make ?loc @@ Glob_term.PatVar Anonymous) else pat in + DAst.make ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous)) pat p (* raise Not_found if no coercion found *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index b9cb7ba1b..1eb22cdb8 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -28,6 +28,10 @@ open Misctypes open Decl_kinds open Context.Named.Declaration +type _ delay = +| Now : 'a delay +| Later : [ `thunk ] delay + (** Should we keep details of universes during detyping ? *) let print_universes = Flags.univ_print @@ -277,7 +281,7 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c = (avoid', add_name_opt na' body t env) sigma c let rec build_tree na isgoal e sigma ci cl = - let mkpat n rhs pl = CAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in + let mkpat n rhs pl = DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in let cnl = ci.ci_pp_info.cstr_tags in let cna = ci.ci_cstr_nargs in List.flatten @@ -300,7 +304,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with List.map (fun (hd,rest) -> pat::hd,rest) lines) clauses) | _ -> - let pat = CAst.make @@ PatVar(update_name sigma na rhs) in + let pat = DAst.make @@ PatVar(update_name sigma na rhs) in let mat = align_tree nal isgoal rhs sigma in List.map (fun (hd,rest) -> pat::hd,rest) mat @@ -323,7 +327,7 @@ let is_nondep_branch sigma c l = let extract_nondep_branches test c b l = let rec strip l r = - match r.CAst.v, l with + match DAst.get r, l with | r', [] -> r | GLambda (_,_,_,t), false::l -> strip l t | GLetIn (_,_,_,t), true::l -> strip l t @@ -333,7 +337,7 @@ let extract_nondep_branches test c b l = let it_destRLambda_or_LetIn_names l c = let rec aux l nal c = - match c.CAst.v, l with + match DAst.get c, l with | _, [] -> (List.rev nal,c) | GLambda (na,_,_,c), false::l -> aux l (na::nal) c | GLetIn (na,_,_,c), true::l -> aux l (na::nal) c @@ -347,11 +351,11 @@ let it_destRLambda_or_LetIn_names l c = x in let x = next (free_glob_vars c) in - let a = CAst.make @@ GVar x in + let a = DAst.make @@ GVar x in aux l (Name x :: nal) - (match c with - | { loc; CAst.v = GApp (p,l) } -> CAst.make ?loc @@ GApp (p,l@[a]) - | _ -> CAst.make @@ GApp (c,[a])) + (match DAst.get c with + | GApp (p,l) -> DAst.make ?loc:c.CAst.loc @@ GApp (p,l@[a]) + | _ -> DAst.make @@ GApp (c,[a])) in aux l [] c let detype_case computable detype detype_eqns testdep avoid data p c bl = @@ -367,7 +371,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | None -> Anonymous, None, None | Some p -> let nl,typ = it_destRLambda_or_LetIn_names k p in - let n,typ = match typ.CAst.v with + let n,typ = match DAst.get typ with | GLambda (x,_,t,c) -> x, c | _ -> Anonymous, typ in let aliastyp = @@ -437,12 +441,20 @@ let detype_instance sigma l = if Univ.Instance.is_empty l then None else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l))) -let rec detype flags avoid env sigma t = CAst.make @@ +let delay (type a) (d : a delay) (f : a delay -> _ -> _ -> _ -> _ -> _ -> a glob_constr_r) flags env avoid sigma t : a glob_constr_g = + match d with + | Now -> DAst.make (f d flags env avoid sigma t) + | Later -> DAst.delay (fun () -> f d flags env avoid sigma t) + +let rec detype d flags avoid env sigma t = + delay d detype_r flags avoid env sigma t + +and detype_r d flags avoid env sigma t = match EConstr.kind sigma (collapse_appl sigma t) with | Rel n -> (try match lookup_name_of_rel n (fst env) with | Name id -> GVar id - | Anonymous -> (!detype_anonymous n).CAst.v + | Anonymous -> GVar (!detype_anonymous n) with Not_found -> let s = "_UNBOUND_REL_"^(string_of_int n) in GVar (Id.of_string s)) @@ -455,44 +467,44 @@ let rec detype flags avoid env sigma t = CAst.make @@ with Not_found -> GVar id) | Sort s -> GSort (detype_sort sigma (ESorts.kind sigma s)) | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> - (detype flags avoid env sigma c1).CAst.v + DAst.get (detype d flags avoid env sigma c1) | Cast (c1,k,c2) -> - let d1 = detype flags avoid env sigma c1 in - let d2 = detype flags avoid env sigma c2 in + let d1 = detype d flags avoid env sigma c1 in + let d2 = detype d flags avoid env sigma c2 in let cast = match k with | VMcast -> CastVM d2 | NATIVEcast -> CastNative d2 | _ -> CastConv d2 in GCast(d1,cast) - | Prod (na,ty,c) -> detype_binder flags BProd avoid env sigma na None ty c - | Lambda (na,ty,c) -> detype_binder flags BLambda avoid env sigma na None ty c - | LetIn (na,b,ty,c) -> detype_binder flags BLetIn avoid env sigma na (Some b) ty c + | Prod (na,ty,c) -> detype_binder d flags BProd avoid env sigma na None ty c + | Lambda (na,ty,c) -> detype_binder d flags BLambda avoid env sigma na None ty c + | LetIn (na,b,ty,c) -> detype_binder d flags BLetIn avoid env sigma na (Some b) ty c | App (f,args) -> let mkapp f' args' = - match f'.CAst.v with + match DAst.get f' with | GApp (f',args'') -> GApp (f',args''@args') | _ -> GApp (f',args') in - mkapp (detype flags avoid env sigma f) - (Array.map_to_list (detype flags avoid env sigma) args) + mkapp (detype d flags avoid env sigma f) + (Array.map_to_list (detype d flags avoid env sigma) args) | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u) | Proj (p,c) -> let noparams () = let pb = Environ.lookup_projection p (snd env) in let pars = pb.Declarations.proj_npars in - let hole = CAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in + let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in let args = List.make pars hole in - GApp (CAst.make @@ GRef (ConstRef (Projection.constant p), None), - (args @ [detype flags avoid env sigma c])) + GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), + (args @ [detype d flags avoid env sigma c])) in if fst flags || !Flags.in_debugger || !Flags.in_toplevel then try noparams () with _ -> (* lax mode, used by debug printers only *) - GApp (CAst.make @@ GRef (ConstRef (Projection.constant p), None), - [detype flags avoid env sigma c]) + GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), + [detype d flags avoid env sigma c]) else if print_primproj_compatibility () && Projection.unfolded p then (** Print the compatibility match version *) @@ -509,12 +521,12 @@ let rec detype flags avoid env sigma t = CAst.make @@ substl (c :: List.rev args) body' with Retyping.RetypeError _ | Not_found -> anomaly (str"Cannot detype an unfolded primitive projection.") - in (detype flags avoid env sigma c').CAst.v + in DAst.get (detype d flags avoid env sigma c') else if print_primproj_params () then try let c = Retyping.expand_projection (snd env) sigma p c [] in - (detype flags avoid env sigma c).CAst.v + DAst.get (detype d flags avoid env sigma c) with Retyping.RetypeError _ -> noparams () else noparams () @@ -542,23 +554,23 @@ let rec detype flags avoid env sigma t = CAst.make @@ (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl) in GEvar (id, - List.map (on_snd (detype flags avoid env sigma)) l) + List.map (on_snd (detype d flags avoid env sigma)) l) | Ind (ind_sp,u) -> GRef (IndRef ind_sp, detype_instance sigma u) | Construct (cstr_sp,u) -> GRef (ConstructRef cstr_sp, detype_instance sigma u) | Case (ci,p,c,bl) -> let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in - detype_case comp (detype flags avoid env sigma) - (detype_eqns flags avoid env sigma ci comp) + detype_case comp (detype d flags avoid env sigma) + (detype_eqns d flags avoid env sigma ci comp) (is_nondep_branch sigma) avoid (ci.ci_ind,ci.ci_pp_info.style, ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags) (Some p) c bl - | Fix (nvn,recdef) -> detype_fix flags avoid env sigma nvn recdef - | CoFix (n,recdef) -> detype_cofix flags avoid env sigma n recdef + | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef + | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef -and detype_fix flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = +and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = let def_avoid, def_env, lfi = Array.fold_left2 (fun (avoid, env, l) na ty -> @@ -567,14 +579,14 @@ and detype_fix flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = (avoid, env, []) names tys in let n = Array.length tys in let v = Array.map3 - (fun c t i -> share_names flags (i+1) [] def_avoid def_env sigma c (lift n t)) + (fun c t i -> share_names d flags (i+1) [] def_avoid def_env sigma c (lift n t)) bodies tys vn in GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) -and detype_cofix flags avoid env sigma n (names,tys,bodies) = +and detype_cofix d flags avoid env sigma n (names,tys,bodies) = let def_avoid, def_env, lfi = Array.fold_left2 (fun (avoid, env, l) na ty -> @@ -583,14 +595,14 @@ and detype_cofix flags avoid env sigma n (names,tys,bodies) = (avoid, env, []) names tys in let ntys = Array.length tys in let v = Array.map2 - (fun c t -> share_names flags 0 [] def_avoid def_env sigma c (lift ntys t)) + (fun c t -> share_names d flags 0 [] def_avoid def_env sigma c (lift ntys t)) bodies tys in GRec(GCoFix n,Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) -and share_names flags n l avoid env sigma c t = +and share_names d flags n l avoid env sigma c t = match EConstr.kind sigma c, EConstr.kind sigma t with (* factorize even when not necessary to have better presentation *) | Lambda (na,t,c), Prod (na',t',c') -> @@ -598,59 +610,59 @@ and share_names flags n l avoid env sigma c t = Name _, _ -> na | _, Name _ -> na' | _ -> na in - let t' = detype flags avoid env sigma t in + let t' = detype d flags avoid env sigma t in let id = next_name_away na avoid in let avoid = id::avoid and env = add_name (Name id) None t env in - share_names flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' + share_names d flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' (* May occur for fix built interactively *) | LetIn (na,b,t',c), _ when n > 0 -> - let t'' = detype flags avoid env sigma t' in - let b' = detype flags avoid env sigma b in + let t'' = detype d flags avoid env sigma t' in + let b' = detype d flags avoid env sigma b in let id = next_name_away na avoid in let avoid = id::avoid and env = add_name (Name id) (Some b) t' env in - share_names flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) + share_names d flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) (* Only if built with the f/n notation or w/o let-expansion in types *) | _, LetIn (_,b,_,t) when n > 0 -> - share_names flags n l avoid env sigma c (subst1 b t) + share_names d flags n l avoid env sigma c (subst1 b t) (* If it is an open proof: we cheat and eta-expand *) | _, Prod (na',t',c') when n > 0 -> - let t'' = detype flags avoid env sigma t' in + let t'' = detype d flags avoid env sigma t' in let id = next_name_away na' avoid in let avoid = id::avoid and env = add_name (Name id) None t' env in let appc = mkApp (lift 1 c,[|mkRel 1|]) in - share_names flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' + share_names d flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); - let c = detype flags avoid env sigma c in - let t = detype flags avoid env sigma t in + let c = detype d flags avoid env sigma c in + let t = detype d flags avoid env sigma t in (List.rev l,c,t) -and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl = +and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl = try if !Flags.raw_print || not (reverse_matching ()) then raise Exit; let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in - List.map (fun (pat,((avoid,env),c)) -> Loc.tag ([],[pat],detype flags avoid env sigma c)) + List.map (fun (pat,((avoid,env),c)) -> Loc.tag ([],[pat],detype d flags avoid env sigma c)) mat with e when CErrors.noncritical e -> Array.to_list - (Array.map3 (detype_eqn flags avoid env sigma) constructs consnargsl bl) + (Array.map3 (detype_eqn d flags avoid env sigma) constructs consnargsl bl) -and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch = +and detype_eqn d (lax,isgoal as flags) avoid env sigma constr construct_nargs branch = let make_pat x avoid env b body ty ids = if force_wildcard () && noccurn sigma 1 b then - CAst.make @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids + DAst.make @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids else let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in let na,avoid' = compute_displayed_name_in sigma flag avoid x b in - CAst.make (PatVar na),avoid',(add_name na body ty env),add_vname ids na + DAst.make (PatVar na),avoid',(add_name na body ty env),add_vname ids na in let rec buildrec ids patlist avoid env l b = match EConstr.kind sigma b, l with | _, [] -> Loc.tag @@ (Id.Set.elements ids, - [CAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)], - detype flags avoid env sigma b) + [DAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)], + detype d flags avoid env sigma b) | Lambda (x,t,b), false::l -> let pat,new_avoid,new_env,new_ids = make_pat x avoid env b None t ids in buildrec new_ids (pat::patlist) new_avoid new_env l b @@ -663,7 +675,7 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran buildrec ids patlist avoid env l c | _, true::l -> - let pat = CAst.make @@ PatVar Anonymous in + let pat = DAst.make @@ PatVar Anonymous in buildrec ids (pat::patlist) avoid env l b | _, false::l -> @@ -678,23 +690,23 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran in buildrec Id.Set.empty [] avoid env construct_nargs branch -and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = +and detype_binder d (lax,isgoal as flags) bk avoid env sigma na body ty c = let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in let na',avoid' = match bk with | BLetIn -> compute_displayed_let_name_in sigma flag avoid na c | _ -> compute_displayed_name_in sigma flag avoid na c in - let r = detype flags avoid' (add_name na' body ty env) sigma c in + let r = detype d flags avoid' (add_name na' body ty env) sigma c in match bk with - | BProd -> GProd (na',Explicit,detype (lax,false) avoid env sigma ty, r) - | BLambda -> GLambda (na',Explicit,detype (lax,false) avoid env sigma ty, r) + | BProd -> GProd (na',Explicit,detype d (lax,false) avoid env sigma ty, r) + | BLambda -> GLambda (na',Explicit,detype d (lax,false) avoid env sigma ty, r) | BLetIn -> - let c = detype (lax,false) avoid env sigma (Option.get body) in + let c = detype d (lax,false) avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in - let t = if s != InProp && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in + let t = if s != InProp && not !Flags.raw_print then None else Some (detype d (lax,false) avoid env sigma ty) in GLetIn (na', c, t, r) -let detype_rel_context ?(lax=false) where avoid env sigma sign = +let detype_rel_context d ?(lax=false) where avoid env sigma sign = let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in let rec aux avoid env = function | [] -> [] @@ -716,15 +728,18 @@ let detype_rel_context ?(lax=false) where avoid env sigma sign = | LocalAssum _ -> None | LocalDef (_,b,_) -> Some b in - let b' = Option.map (detype (lax,false) avoid env sigma) b in - let t' = detype (lax,false) avoid env sigma t in + let b' = Option.map (detype d (lax,false) avoid env sigma) b in + let t' = detype d (lax,false) avoid env sigma t in (na',Explicit,b',t') :: aux avoid' (add_name na' b t env) rest in aux avoid env (List.rev sign) let detype_names isgoal avoid nenv env sigma t = - detype (false,isgoal) avoid (nenv,env) sigma t -let detype ?(lax=false) isgoal avoid env sigma t = - detype (lax,isgoal) avoid (names_of_rel_context env, env) sigma t + detype Now (false,isgoal) avoid (nenv,env) sigma t +let detype d ?(lax=false) isgoal avoid env sigma t = + detype d (lax,isgoal) avoid (names_of_rel_context env, env) sigma t + +let detype_rel_context d ?lax where avoid env sigma sign = + detype_rel_context d ?lax where avoid env sigma sign let detype_closed_glob ?lax isgoal avoid env sigma t = let open Context.Rel.Declaration in @@ -736,7 +751,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = | Name id -> Name (convert_id cl id) | Anonymous -> Anonymous in - let rec detype_closed_glob cl cg : Glob_term.glob_constr = CAst.map (function + let rec detype_closed_glob cl cg : Glob_term.glob_constr = DAst.map (function | GVar id -> (* if [id] is bound to a name. *) begin try @@ -750,11 +765,11 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = [Printer.pr_constr_under_binders_env] does. *) let assums = List.map (fun id -> LocalAssum (Name id,(* dummy *) mkProp)) b in let env = push_rel_context assums env in - (detype ?lax isgoal avoid env sigma c).CAst.v + DAst.get (detype Now ?lax isgoal avoid env sigma c) (* if [id] is bound to a [closed_glob_constr]. *) with Not_found -> try let {closure;term} = Id.Map.find id cl.untyped in - (detype_closed_glob closure term).CAst.v + DAst.get (detype_closed_glob closure term) (* Otherwise [id] stands for itself *) with Not_found -> GVar id @@ -781,7 +796,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = in GCases(sty,po,tml,eqns) | c -> - (Glob_ops.map_glob_constr (detype_closed_glob cl) cg).CAst.v + DAst.get (Glob_ops.map_glob_constr (detype_closed_glob cl) cg) ) cg in detype_closed_glob t.closure t.term @@ -789,7 +804,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = (**********************************************************************) (* Module substitution: relies on detyping *) -let rec subst_cases_pattern subst = CAst.map (function +let rec subst_cases_pattern subst = DAst.map (function | PatVar _ as pat -> pat | PatCstr (((kn,i),j),cpl,n) as pat -> let kn' = subst_mind subst kn @@ -800,11 +815,11 @@ let rec subst_cases_pattern subst = CAst.map (function let (f_subst_genarg, subst_genarg_hook) = Hook.make () -let rec subst_glob_constr subst = CAst.map (function +let rec subst_glob_constr subst = DAst.map (function | GRef (ref,u) as raw -> let ref',t = subst_global subst ref in if ref' == ref then raw else - (detype false [] (Global.env()) Evd.empty (EConstr.of_constr t)).CAst.v + DAst.get (detype Now false [] (Global.env()) Evd.empty (EConstr.of_constr t)) | GSort _ | GVar _ @@ -905,8 +920,8 @@ let rec subst_glob_constr subst = CAst.map (function let simple_cases_matrix_of_branches ind brs = List.map (fun (i,n,b) -> let nal,c = it_destRLambda_or_LetIn_names n b in - let mkPatVar na = CAst.make @@ PatVar na in - let p = CAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in + let mkPatVar na = DAst.make @@ PatVar na in + let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in let ids = List.map_filter Nameops.Name.to_option nal in Loc.tag @@ (ids,[p],c)) brs diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 59f3f967d..67c852af3 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -16,6 +16,10 @@ open Mod_subst open Misctypes open Evd +type _ delay = +| Now : 'a delay +| Later : [ `thunk ] delay + (** Should we keep details of universes during detyping ? *) val print_universes : bool ref @@ -33,12 +37,12 @@ val subst_glob_constr : substitution -> glob_constr -> glob_constr val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> constr -> glob_constr -val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob_constr +val detype : 'a delay -> ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> 'a glob_constr_g val detype_sort : evar_map -> sorts -> glob_sort -val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> - evar_map -> rel_context -> glob_decl list +val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> + evar_map -> rel_context -> 'a glob_decl_g list val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr @@ -47,7 +51,7 @@ val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option (* XXX: This is a hack and should go away *) -val set_detype_anonymous : (?loc:Loc.t -> int -> glob_constr) -> unit +val set_detype_anonymous : (?loc:Loc.t -> int -> Id.t) -> unit val force_wildcard : unit -> bool val synthetize_type : unit -> bool diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index b94228e75..c40a24e3b 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -23,8 +23,8 @@ let cases_predicate_names tml = | (tm,(na,None)) -> [na] | (tm,(na,Some (_,(_,nal)))) -> na::nal) tml) -let mkGApp ?loc p t = CAst.make ?loc @@ - match p.CAst.v with +let mkGApp ?loc p t = DAst.make ?loc @@ + match DAst.get p with | GApp (f,l) -> GApp (f,l@[t]) | _ -> GApp (p,[t]) @@ -46,7 +46,7 @@ let case_style_eq s1 s2 = match s1, s2 with | RegularStyle, RegularStyle -> true | (LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle), _ -> false -let rec cases_pattern_eq { CAst.v = p1} { CAst.v = p2 } = match p1, p2 with +let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with | PatVar na1, PatVar na2 -> Name.equal na1 na2 | PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && @@ -98,7 +98,7 @@ let fix_kind_eq f k1 k2 = match k1, k2 with let instance_eq f (x1,c1) (x2,c2) = Id.equal x1 x2 && f c1 c2 -let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with +let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 | GVar id1, GVar id2 -> Id.equal id1 id2 | GEvar (id1, arg1), GEvar (id2, arg2) -> @@ -137,7 +137,7 @@ let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c -let map_glob_constr_left_to_right f = CAst.map (function +let map_glob_constr_left_to_right f = DAst.map (function | GApp (g,args) -> let comp1 = f g in let comp2 = Util.List.map_left f args in @@ -186,7 +186,7 @@ let map_glob_constr = map_glob_constr_left_to_right let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt -let fold_glob_constr f acc = CAst.with_val (function +let fold_glob_constr f acc = DAst.with_val (function | GVar _ -> acc | GApp (c,args) -> List.fold_left f (f acc c) args | GLambda (_,_,b,c) | GProd (_,_,b,c) -> @@ -217,7 +217,7 @@ let fold_glob_constr f acc = CAst.with_val (function let fold_return_type_with_binders f g v acc (na,tyopt) = Option.fold_left (f (Name.fold_right g na v)) acc tyopt -let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function +let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function | GVar _ -> acc | GApp (c,args) -> List.fold_left (f v) (f v acc c) args | GLambda (na,_,b,c) | GProd (na,_,b,c) -> @@ -256,10 +256,9 @@ let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function let iter_glob_constr f = fold_glob_constr (fun () -> f) () let occur_glob_constr id = - let open CAst in - let rec occur barred acc = function - | { loc ; v = GVar id' } -> Id.equal id id' - | c -> + let rec occur barred acc c = match DAst.get c with + | GVar id' -> Id.equal id id' + | _ -> (* [g] looks if [id] appears in a binding position, in which case, we don't have to look in the corresponding subterm *) let g id' barred = barred || Id.equal id id' in @@ -268,21 +267,20 @@ let occur_glob_constr id = occur false false let free_glob_vars = - let open CAst in - let rec vars bound vs = function - | { loc ; v = GVar id' } -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs - | c -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in + let rec vars bound vs c = match DAst.get c with + | GVar id' -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs + | _ -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in fun rt -> let vs = vars Id.Set.empty Id.Set.empty rt in Id.Set.elements vs let glob_visible_short_qualid c = - let rec aux acc = function - | { CAst.v = GRef (c,_) } -> + let rec aux acc c = match DAst.get c with + | GRef (c,_) -> let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in let dir,id = Libnames.repr_qualid qualid in if DirPath.is_empty dir then id :: acc else acc - | c -> + | _ -> fold_glob_constr aux acc c in aux [] c @@ -326,7 +324,7 @@ let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple = if r == inp then x else c,(f na, r) -let rec map_case_pattern_binders f = CAst.map (function +let rec map_case_pattern_binders f = DAst.map (function | PatVar na as x -> let r = f na in if r == na then x @@ -396,7 +394,9 @@ let rename_var l id = if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming else id -let rec rename_glob_vars l c = CAst.map_with_loc (fun ?loc -> function +let force c = DAst.make ?loc:c.CAst.loc (DAst.get c) + +let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function | GVar id as r -> let id' = rename_var l id in if id == id' then r else GVar id' @@ -436,13 +436,13 @@ let rec rename_glob_vars l c = CAst.map_with_loc (fun ?loc -> function test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls, Array.map (rename_glob_vars l) bs, Array.map (rename_glob_vars l) ts) - | _ -> (map_glob_constr (rename_glob_vars l) c).CAst.v + | _ -> DAst.get (map_glob_constr (rename_glob_vars l) c) ) c (**********************************************************************) (* Conversion from glob_constr to cases pattern, if possible *) -let rec cases_pattern_of_glob_constr na = CAst.map (function +let rec cases_pattern_of_glob_constr na = DAst.map (function | GVar id -> begin match na with | Name _ -> @@ -452,8 +452,12 @@ let rec cases_pattern_of_glob_constr na = CAst.map (function end | GHole (_,_,_) -> PatVar na | GRef (ConstructRef cstr,_) -> PatCstr (cstr,[],na) - | GApp ( { CAst.v = GRef (ConstructRef cstr,_) }, l) -> + | GApp (c, l) -> + begin match DAst.get c with + | GRef (ConstructRef cstr,_) -> PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) + | _ -> raise Not_found + end | _ -> raise Not_found ) @@ -469,7 +473,7 @@ let drop_local_defs typi args = | [], [] -> [] | Rel.Declaration.LocalDef _ :: decls, pat :: args -> begin - match pat.CAst.v with + match DAst.get pat with | PatVar Anonymous -> aux decls args | _ -> raise Not_found (* The pattern is used, one cannot drop it *) end @@ -487,21 +491,22 @@ let add_patterns_for_params_remove_local_defs (ind,j) l = let typi = mip.mind_nf_lc.(j-1) in let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in drop_local_defs typi l in - Util.List.addn nparams (CAst.make @@ PatVar Anonymous) l + Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l (* Turn a closed cases pattern into a glob_constr *) -let rec glob_constr_of_closed_cases_pattern_aux x = CAst.map_with_loc (fun ?loc -> function +let rec glob_constr_of_closed_cases_pattern_aux x = DAst.map_with_loc (fun ?loc -> function | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None) | PatCstr (cstr,l,Anonymous) -> - let ref = CAst.make ?loc @@ GRef (ConstructRef cstr,None) in + let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in let l = add_patterns_for_params_remove_local_defs cstr l in GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l) | _ -> raise Not_found ) x -let glob_constr_of_closed_cases_pattern = function - | { CAst.loc ; v = PatCstr (cstr,l,na) } -> - na,glob_constr_of_closed_cases_pattern_aux (CAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) +let glob_constr_of_closed_cases_pattern p = match DAst.get p with + | PatCstr (cstr,l,na) -> + let loc = p.CAst.loc in + na,glob_constr_of_closed_cases_pattern_aux (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) | _ -> raise Not_found diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index bd9e111f5..bacc8fbe4 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -11,21 +11,21 @@ open Glob_term (** Equalities *) -val cases_pattern_eq : cases_pattern -> cases_pattern -> bool +val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool val cast_type_eq : ('a -> 'a -> bool) -> 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool -val glob_constr_eq : glob_constr -> glob_constr -> bool +val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool (** Operations on [glob_constr] *) -val cases_pattern_loc : cases_pattern -> Loc.t option +val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option -val cases_predicate_names : tomatch_tuples -> Name.t list +val cases_predicate_names : 'a tomatch_tuples_g -> Name.t list (** Apply one argument to a glob_constr *) -val mkGApp : ?loc:Loc.t -> glob_constr -> glob_constr -> glob_constr +val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g -> 'a glob_constr_g val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr @@ -42,12 +42,12 @@ val mk_glob_constr_eq : (glob_constr -> glob_constr -> bool) -> val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit -val occur_glob_constr : Id.t -> glob_constr -> bool -val free_glob_vars : glob_constr -> Id.t list +val occur_glob_constr : Id.t -> 'a glob_constr_g -> bool +val free_glob_vars : 'a glob_constr_g -> Id.t list val bound_glob_vars : glob_constr -> Id.Set.t (* Obsolete *) -val loc_of_glob_constr : glob_constr -> Loc.t option -val glob_visible_short_qualid : glob_constr -> Id.t list +val loc_of_glob_constr : 'a glob_constr_g -> Loc.t option +val glob_visible_short_qualid : 'a glob_constr_g -> Id.t list (* Renaming free variables using a renaming map; fails with [UnsoundRenaming] if applying the renaming would introduce @@ -57,7 +57,7 @@ val glob_visible_short_qualid : glob_constr -> Id.t list exception UnsoundRenaming val rename_var : (Id.t * Id.t) list -> Id.t -> Id.t -val rename_glob_vars : (Id.t * Id.t) list -> glob_constr -> glob_constr +val rename_glob_vars : (Id.t * Id.t) list -> 'a glob_constr_g -> 'a glob_constr_g (** [map_pattern_binders f m c] applies [f] to all the binding names in a pattern-matching expression ({!Glob_term.GCases}) represented @@ -80,9 +80,9 @@ val map_pattern : (glob_constr -> glob_constr) -> @raise Not_found if translation is impossible *) val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern -val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr +val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob_constr_g -val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list +val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name val empty_lvar : Glob_term.ltac_var_map diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 5826cc135..3b3ad021e 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -326,7 +326,7 @@ let warn_cast_in_pattern = CWarnings.create ~name:"cast-in-pattern" ~category:"automation" (fun () -> Pp.strbrk "Casts are ignored in patterns") -let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function +let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function | GVar id -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) @@ -335,11 +335,14 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function | GRef (gr,_) -> PRef (canonical_gr gr) (* Hack to avoid rewriting a complete interpretation of patterns *) - | GApp ({ CAst.v = GPatVar (Evar_kinds.SecondOrderPatVar n) }, cl) -> + | GApp (c, cl) -> + begin match DAst.get c with + | GPatVar (Evar_kinds.SecondOrderPatVar n) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) - | GApp (c,cl) -> + | _ -> PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) + end | GLambda (na,bk,c1,c2) -> Name.iter (fun n -> metas := n::!metas) na; PLambda (na, pat_of_raw metas vars c1, @@ -364,8 +367,8 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (nal,(_,None),b,c) -> - let mkGLambda na c = CAst.make ?loc @@ - GLambda (na,Explicit, CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in + let mkGLambda na c = DAst.make ?loc @@ + GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in let c = List.fold_right mkGLambda nal c in let cip = { cip_style = LetStyle; @@ -377,8 +380,12 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function PCase (cip, PMeta None, pat_of_raw metas vars b, [0,tags,pat_of_raw metas vars c]) | GCases (sty,p,[c,(na,indnames)],brs) -> + let get_ind p = match DAst.get p with + | PatCstr((ind,_),_,_) -> Some ind + | _ -> None + in let get_ind = function - | (_,(_,[{ CAst.v = PatCstr((ind,_),_,_) }],_))::_ -> Some ind + | (_,(_,[p],_))::_ -> get_ind p | _ -> None in let ind_tags,ind = match indnames with @@ -391,8 +398,11 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function | Some p, Some (_,(_,nal)) -> let nvars = na :: List.rev nal @ vars in rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) - | (None | Some { CAst.v = GHole _}), _ -> PMeta None + | None, _ -> PMeta None | Some p, None -> + match DAst.get p with + | GHole _ -> PMeta None + | _ -> user_err ?loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in let info = @@ -410,30 +420,36 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function ) and pats_of_glob_branches loc metas vars ind brs = - let get_arg = function - | { CAst.v = PatVar na } -> + let get_arg p = match DAst.get p with + | PatVar na -> Name.iter (fun n -> metas := n::!metas) na; na - | { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.") + | PatCstr(_,_,_) -> err ?loc:p.CAst.loc (Pp.str "Non supported pattern.") in let rec get_pat indexes = function | [] -> false, [] - | [(_,(_,[{ CAst.v = PatVar Anonymous }], { CAst.v = GHole _}))] -> true, [] (* ends with _ => _ *) - | (_,(_,[{ CAst.v = PatCstr((indsp,j),lv,_) }],br)) :: brs -> - let () = match ind with - | Some sp when eq_ind sp indsp -> () + | (loc',(_,[p], br)) :: brs -> + begin match DAst.get p, DAst.get br, brs with + | PatVar Anonymous, GHole _, [] -> + true, [] (* ends with _ => _ *) + | PatCstr((indsp,j),lv,_), _, _ -> + let () = match ind with + | Some sp when eq_ind sp indsp -> () + | _ -> + err ?loc (Pp.str "All constructors must be in the same inductive type.") + in + if Int.Set.mem (j-1) indexes then + err ?loc + (str "No unique branch for " ++ int j ++ str"-th constructor."); + let lna = List.map get_arg lv in + let vars' = List.rev lna @ vars in + let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in + let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in + let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in + ext, ((j-1, tags, pat) :: pats) | _ -> - err ?loc (Pp.str "All constructors must be in the same inductive type.") - in - if Int.Set.mem (j-1) indexes then - err ?loc - (str "No unique branch for " ++ int j ++ str"-th constructor."); - let lna = List.map get_arg lv in - let vars' = List.rev lna @ vars in - let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in - let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in - let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in - ext, ((j-1, tags, pat) :: pats) + err ?loc:loc' (Pp.str "Non supported pattern.") + end | (loc,(_,_,_)) :: _ -> err ?loc (Pp.str "Non supported pattern.") in get_pat Int.Set.empty brs diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 40b8bcad9..79d2c3333 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -572,7 +572,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pretype = pretype k0 resolve_tc in let open Context.Rel.Declaration in let loc = t.CAst.loc in - match t.CAst.v with + match DAst.get t with | GRef (ref,u) -> inh_conv_coerce_to_tycon ?loc env evdref (pretype_ref ?loc evdref env ref u) @@ -1100,8 +1100,9 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = Array.map_of_list snd subst (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) -and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function - | { loc; CAst.v = GHole (knd, naming, None) } -> +and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match DAst.get c with + | GHole (knd, naming, None) -> + let loc = loc_of_glob_constr c in let rec is_Type c = match EConstr.kind !evdref c with | Sort s -> begin match ESorts.kind !evdref s with @@ -1134,7 +1135,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s); utj_type = s}) - | c -> + | _ -> let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in let tj = evd_comb1 (Coercion.inh_coerce_to_sort ?loc env.ExtraEnv.env) evdref j in diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index b057cf72b..75fae6647 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -252,16 +252,16 @@ open Decl_kinds open Evar_kinds let mkPattern c = snd (Patternops.pattern_of_glob_constr c) -let mkGApp f args = CAst.make @@ GApp (f, args) -let mkGHole = CAst.make @@ +let mkGApp f args = DAst.make @@ GApp (f, args) +let mkGHole = DAst.make @@ GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None) -let mkGProd id c1 c2 = CAst.make @@ +let mkGProd id c1 c2 = DAst.make @@ GProd (Name (Id.of_string id), Explicit, c1, c2) -let mkGArrow c1 c2 = CAst.make @@ +let mkGArrow c1 c2 = DAst.make @@ GProd (Anonymous, Explicit, c1, c2) -let mkGVar id = CAst.make @@ GVar (Id.of_string id) -let mkGPatVar id = CAst.make @@ GPatVar(Evar_kinds.FirstOrderPatVar (Id.of_string id)) -let mkGRef r = CAst.make @@ GRef (Lazy.force r, None) +let mkGVar id = DAst.make @@ GVar (Id.of_string id) +let mkGPatVar id = DAst.make @@ GPatVar(Evar_kinds.FirstOrderPatVar (Id.of_string id)) +let mkGRef r = DAst.make @@ GRef (Lazy.force r, None) let mkGAppRef r args = mkGApp (mkGRef r) args (** forall x : _, _ x x *) diff --git a/vernac/command.ml b/vernac/command.ml index 0d6fd24cd..32ab5401a 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -367,7 +367,7 @@ let prepare_param = function let rec check_anonymous_type ind = let open Glob_term in - match ind.CAst.v with + match DAst.get ind with | GSort (GType []) -> true | GProd ( _, _, _, e) | GLetIn (_, _, _, e) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 8738e58e8..d2ba9eb1c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1230,7 +1230,7 @@ let vernac_reserve bl = let env = Global.env() in let sigma = Evd.from_env env in let t,ctx = Constrintern.interp_type env sigma c in - let t = Detyping.detype false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in + let t = Detyping.detype Detyping.Now false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl |