diff options
Diffstat (limited to 'plugins')
57 files changed, 857 insertions, 408 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 6f9384941b..d06a241969 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -40,7 +40,7 @@ let start_deriving f suchthat lemma = let f_type = EConstr.Unsafe.to_constr f_type in let ef = EConstr.Unsafe.to_constr ef in let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in - let sigma, suchthat = Constrintern.interp_type_evars env' sigma suchthat in + let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in TCons ( env' , sigma , suchthat , (fun sigma _ -> TNil sigma)))))) in diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index df4b647642..0cdf8fb5d8 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -18,7 +18,7 @@ DECLARE PLUGIN "derive_plugin" { -let classify_derive_command _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) +let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]),VtLater) } diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index b0f6301192..b59e3b608c 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -147,7 +147,7 @@ let check_fix env sg cb i = | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd) | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd) | _ -> raise Impossible) - | Undef _ | OpaqueDef _ -> raise Impossible + | Undef _ | OpaqueDef _ | Primitive _ -> raise Impossible let prec_declaration_equal sg (na1, ca1, ta1) (na2, ca2, ta2) = Array.equal Name.equal na1 na2 && diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 67c605ea1d..204f889f90 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -304,9 +304,9 @@ let rec extract_type env sg db j c args = | (Info, TypeScheme) -> let mlt = extract_type_app env sg db (r, type_sign env sg typ) args in (match (lookup_constant kn env).const_body with - | Undef _ | OpaqueDef _ -> mlt - | Def _ when is_custom (ConstRef kn) -> mlt - | Def lbody -> + | Undef _ | OpaqueDef _ | Primitive _ -> mlt + | Def _ when is_custom (ConstRef kn) -> mlt + | Def lbody -> let newc = applistc (get_body lbody) args in let mlt' = extract_type env sg db j newc [] in (* ML type abbreviations interact badly with Coq *) @@ -318,7 +318,7 @@ let rec extract_type env sg db j c args = | (Info, Default) -> (* Not an ML type, for example [(c:forall X, X->X) Type nat] *) (match (lookup_constant kn env).const_body with - | Undef _ | OpaqueDef _ -> Tunknown (* Brutal approx ... *) + | Undef _ | OpaqueDef _ | Primitive _ -> Tunknown (* Brutal approx ... *) | Def lbody -> (* We try to reduce. *) let newc = applistc (get_body lbody) args in @@ -346,7 +346,7 @@ let rec extract_type env sg db j c args = | (Info, TypeScheme) -> extract_type_app env sg db (r, type_sign env sg ty) args | (Info, Default) -> Tunknown)) - | Cast _ | LetIn _ | Construct _ -> assert false + | Cast _ | LetIn _ | Construct _ | Int _ -> assert false (*s Auxiliary function dealing with type application. Precondition: [r] is a type scheme represented by the signature [s], @@ -564,7 +564,7 @@ and mlt_env env r = match r with | ConstRef kn -> let cb = Environ.lookup_constant kn env in match cb.const_body with - | Undef _ | OpaqueDef _ -> None + | Undef _ | OpaqueDef _ | Primitive _ -> None | Def l_body -> match lookup_typedef kn cb with | Some _ as o -> o @@ -683,6 +683,7 @@ let rec extract_term env sg mle mlt c args = let vty = extract_type env sg [] 0 ty [] in let extract_var mlt = put_magic (mlt,vty) (MLglob (VarRef v)) in extract_app env sg mle mlt extract_var args + | Int i -> assert (args = []); MLuint i | Ind _ | Prod _ | Sort _ -> assert false (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) @@ -1031,6 +1032,55 @@ let extract_fixpoint env sg vkn (fi,ti,ci) = current_fixpoints := []; Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) +(** Because of automatic unboxing the easy way [mk_def c] on the + constant body of primitive projections doesn't work. We pretend + that they are implemented by matches until someone figures out how + to clean it up (test with #4710 when working on this). *) +let fake_match_projection env p = + let ind = Projection.Repr.inductive p in + let proj_arg = Projection.Repr.arg p in + let mib, mip = Inductive.lookup_mind_specif env ind in + let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in + let indu = mkIndU (ind,u) in + let ctx, paramslet = + let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in + let rctx, _ = decompose_prod_assum (Vars.substl subst mip.mind_nf_lc.(0)) in + List.chop mip.mind_consnrealdecls.(0) rctx + in + let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in + let ci = { + ci_ind = ind; + ci_npar = mib.mind_nparams; + ci_cstr_ndecls = mip.mind_consnrealdecls; + ci_cstr_nargs = mip.mind_consnrealargs; + ci_pp_info; + } + in + let x = match mib.mind_record with + | NotRecord | FakeRecord -> assert false + | PrimRecord info -> Name (pi1 info.(snd ind)) + in + let indty = mkApp (indu, Context.Rel.to_extended_vect mkRel 0 paramslet) in + let rec fold arg j subst = function + | [] -> assert false + | LocalAssum (na,ty) :: rem -> + let ty = Vars.substl subst (liftn 1 j ty) in + if arg != proj_arg then + let lab = match na with Name id -> Label.of_id id | Anonymous -> assert false in + let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in + fold (arg+1) (j+1) (mkProj (Projection.make kn false, mkRel 1)::subst) rem + else + let p = mkLambda (x, lift 1 indty, liftn 1 2 ty) in + let branch = lift 1 (it_mkLambda_or_LetIn (mkRel (List.length ctx - (j-1))) ctx) in + let body = mkCase (ci, p, mkRel 1, [|branch|]) in + it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt + | LocalDef (_,c,t) :: rem -> + let c = liftn 1 j c in + let c1 = Vars.substl subst c in + fold arg (j+1) (c1::subst) rem + in + fold 0 1 [] (List.rev ctx) + let extract_constant env kn cb = let sg = Evd.from_env env in let r = ConstRef kn in @@ -1063,15 +1113,12 @@ let extract_constant env kn cb = | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop) | (Info,TypeScheme) -> (match cb.const_body with - | Undef _ -> warn_info (); mk_typ_ax () + | Primitive _ | Undef _ -> warn_info (); mk_typ_ax () | Def c -> (match Recordops.find_primitive_projection kn with | None -> mk_typ (get_body c) | Some p -> - let p = Projection.make p false in - let ind = Projection.inductive p in - let bodies = Inductiveops.legacy_match_projection env ind in - let body = bodies.(Projection.arg p) in + let body = fake_match_projection env p in mk_typ (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; @@ -1079,15 +1126,12 @@ let extract_constant env kn cb = else mk_typ_ax ()) | (Info,Default) -> (match cb.const_body with - | Undef _ -> warn_info (); mk_ax () + | Primitive _ | Undef _ -> warn_info (); mk_ax () | Def c -> (match Recordops.find_primitive_projection kn with | None -> mk_def (get_body c) | Some p -> - let p = Projection.make p false in - let ind = Projection.inductive p in - let bodies = Inductiveops.legacy_match_projection env ind in - let body = bodies.(Projection.arg p) in + let body = fake_match_projection env p in mk_def (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; @@ -1107,7 +1151,7 @@ let extract_constant_spec env kn cb = | (Info, TypeScheme) -> let s,vl = type_sign_vl env sg typ in (match cb.const_body with - | Undef _ | OpaqueDef _ -> Stype (r, vl, None) + | Undef _ | OpaqueDef _ | Primitive _ -> Stype (r, vl, None) | Def body -> let db = db_from_sign s in let body = get_body body in diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 97fe9f24d5..a3cd92d556 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -214,6 +214,8 @@ let rec pp_expr par env args = | MLmagic a -> pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args) | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"") + | MLuint _ -> + pp_par par (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"") and pp_cons_pat par r ppl = pp_par par diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index e43c47d050..f88d29e9ed 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -155,6 +155,10 @@ let rec json_expr env = function ("value", json_expr env a) ] | MLaxiom -> json_dict [("what", json_str "expr:axiom")] + | MLuint i -> json_dict [ + ("what", json_str "expr:int"); + ("int", json_str (Uint63.to_string i)) + ] and json_one_pat env (ids,p,t) = let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [ diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml index ce920ad6a0..b7f80d543b 100644 --- a/plugins/extraction/miniml.ml +++ b/plugins/extraction/miniml.ml @@ -126,6 +126,7 @@ and ml_ast = | MLdummy of kill_reason | MLaxiom | MLmagic of ml_ast + | MLuint of Uint63.t and ml_pattern = | Pcons of GlobRef.t * ml_pattern list diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index ce920ad6a0..9df0f4964e 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -126,6 +126,7 @@ and ml_ast = | MLdummy of kill_reason | MLaxiom | MLmagic of ml_ast + | MLuint of Uint63.t and ml_pattern = | Pcons of GlobRef.t * ml_pattern list diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 9f5c1f1a17..2432887673 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -66,7 +66,8 @@ let rec eq_ml_type t1 t2 = match t1, t2 with | Tdummy k1, Tdummy k2 -> k1 == k2 | Tunknown, Tunknown -> true | Taxiom, Taxiom -> true -| _ -> false +| (Tarr _ | Tglob _ | Tvar _ | Tvar' _ | Tmeta _ | Tdummy _ | Tunknown | Taxiom), _ + -> false and eq_ml_meta m1 m2 = Int.equal m1.id m2.id && Option.equal eq_ml_type m1.contents m2.contents @@ -107,7 +108,7 @@ let rec type_occurs alpha t = | Tmeta {contents=Some u} -> type_occurs alpha u | Tarr (t1, t2) -> type_occurs alpha t1 || type_occurs alpha t2 | Tglob (r,l) -> List.exists (type_occurs alpha) l - | _ -> false + | (Tdummy _ | Tvar _ | Tvar' _ | Taxiom | Tunknown) -> false (*s Most General Unificator *) @@ -310,7 +311,7 @@ let isMLdummy = function MLdummy _ -> true | _ -> false let sign_of_id = function | Dummy -> Kill Kprop - | _ -> Keep + | (Id _ | Tmp _) -> Keep (* Classification of signatures *) @@ -370,7 +371,10 @@ let eq_ml_ident i1 i2 = match i1, i2 with | Dummy, Dummy -> true | Id id1, Id id2 -> Id.equal id1 id2 | Tmp id1, Tmp id2 -> Id.equal id1 id2 -| _ -> false +| Dummy, (Id _ | Tmp _) +| Id _, (Dummy | Tmp _) +| Tmp _, (Dummy | Id _) + -> false let rec eq_ml_ast t1 t2 = match t1, t2 with | MLrel i1, MLrel i2 -> @@ -394,7 +398,8 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with | MLdummy k1, MLdummy k2 -> k1 == k2 | MLaxiom, MLaxiom -> true | MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2 -| _ -> false +| MLuint i1, MLuint i2 -> Uint63.equal i1 i2 +| _, _ -> false and eq_ml_pattern p1 p2 = match p1, p2 with | Pcons (gr1, p1), Pcons (gr2, p2) -> @@ -426,7 +431,7 @@ let ast_iter_rel f = | MLapp (a,l) -> iter n a; List.iter (iter n) l | MLcons (_,_,l) | MLtuple l -> List.iter (iter n) l | MLmagic a -> iter n a - | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> () + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> () in iter 0 (*s Map over asts. *) @@ -445,7 +450,7 @@ let ast_map f = function | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l) | MLtuple l -> MLtuple (List.map f l) | MLmagic a -> MLmagic (f a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ as a -> a (*s Map over asts, with binding depth as parameter. *) @@ -463,7 +468,7 @@ let ast_map_lift f n = function | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l) | MLtuple l -> MLtuple (List.map (f n) l) | MLmagic a -> MLmagic (f n a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ as a -> a (*s Iter over asts. *) @@ -477,7 +482,7 @@ let ast_iter f = function | MLapp (a,l) -> f a; List.iter f l | MLcons (_,_,l) | MLtuple l -> List.iter f l | MLmagic a -> f a - | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> () + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> () (*S Operations concerning De Bruijn indices. *) @@ -513,7 +518,7 @@ let nb_occur_match = | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l | MLmagic a -> nb k a - | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> 0 + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> 0 in nb 1 (* Replace unused variables by _ *) @@ -565,7 +570,7 @@ let dump_unused_vars a = let b' = ren env b in if b' == b then a else MLmagic b' - | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> a + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> a and ren_branch env ((ids,p,b) as tr) = let occs = List.map (fun _ -> ref false) ids in @@ -1398,7 +1403,7 @@ let rec ml_size = function | MLfix(_,_,f) -> ml_size_array f | MLletin (_,_,t) -> ml_size t | MLmagic t -> ml_size t - | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom -> 0 + | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> 0 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index b398bc07a0..654695c232 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -108,7 +108,7 @@ let ast_iter_references do_term do_cons do_type a = Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _ - | MLdummy _ | MLaxiom | MLmagic _ -> () + | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ -> () in iter a let ind_iter_references do_term do_cons do_type kn ind = diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 96d8760404..8940aedd6d 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -310,6 +310,10 @@ let rec pp_expr par env args = apply2 (v 0 (str "match " ++ head ++ str " with" ++ fnl () ++ pp_pat env pv)))) + | MLuint i -> + assert (args=[]); + str "(" ++ str (Uint63.compile i) ++ str ")" + and pp_record_proj par env typ t pv args = (* Can a match be printed as a mere record projection ? *) diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 76a0c74068..6aa3a6220e 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -129,6 +129,8 @@ let rec pp_expr env args = | MLmagic a -> pp_expr env args a | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"") + | MLuint _ -> + paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"") and pp_cons_args env = function | MLcons (_,r,args) when is_coinductive r -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 3b95423067..8da30bd9c9 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -763,12 +763,13 @@ let build_proof end | Cast(t,_,_) -> build_proof do_finalize {dyn_infos with info = t} g - | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> + | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ -> do_finalize dyn_infos g | App(_,_) -> let f,args = decompose_app sigma dyn_infos.info in begin match EConstr.kind sigma f with + | Int _ -> user_err Pp.(str "integer cannot be applied") | App _ -> assert false (* we have collected all the app in decompose_app *) | Proj _ -> assert false (*FIXME*) | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ -> diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 12b68e208c..25a7675113 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -364,7 +364,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = Evd.const_univ_entry ~poly:false evd' in + let univs = Evd.univ_entry ~poly:false evd' in let ce = Declare.definition_entry ~univs value in ignore( Declare.declare_constant diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 8f0440a2a4..c4f8843e51 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -186,7 +186,7 @@ VERNAC COMMAND EXTEND Function (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with | Vernacextend.VtSideff ids, _ when hard -> - Vernacextend.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) + Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) | x -> x } -> { do_generate_principle false (List.map snd recsl) } END diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 4b6caea70d..ba0a3bbb5c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -321,12 +321,10 @@ let build_constructors_of_type ind' argl = construct in let argl = - if List.is_empty argl - then - Array.to_list - (Array.init (cst_narg - npar) (fun _ -> mkGHole ()) - ) - else argl + if List.is_empty argl then + List.make cst_narg (mkGHole ()) + else + List.make npar (mkGHole ()) @ argl in let pat_as_term = mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) @@ -478,7 +476,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt); let open CAst in match DAst.get rt with - | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ -> (* do nothing (except changing type of course) *) mk_result [] rt avoid | GApp(_,_) -> @@ -588,6 +586,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = build_entry_lc env funnames avoid (mkGApp(b,args)) | GRec _ -> user_err Pp.(str "Not handled GRec") | GProd _ -> user_err Pp.(str "Cannot apply a type") + | GInt _ -> user_err Pp.(str "Cannot apply an integer") end (* end of the application treatement *) | GLambda(n,_,t,b) -> @@ -1221,7 +1220,7 @@ 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 = DAst.with_val (function - | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ -> params | GApp(f,args) -> begin match DAst.get f with | GVar relname' when Id.Set.mem relname' relnames -> diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 5b45a8dbed..13ff19a46b 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -106,6 +106,7 @@ let change_vars = | GRec _ -> user_err ?loc Pp.(str "Local (co)fixes are not supported") | GSort _ as x -> x | GHole _ as x -> x + | GInt _ as x -> x | GCast(b,c) -> GCast(change_vars mapping b, Glob_ops.map_cast_type (change_vars mapping) c) @@ -285,6 +286,7 @@ let rec alpha_rt excluded rt = ) | GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ + | GInt _ | GHole _ as rt -> rt | GCast (b,c) -> GCast(alpha_rt excluded b, @@ -344,6 +346,7 @@ let is_free_in id = | GHole _ -> false | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t | GCast (b,CastCoerce) -> is_free_in b + | GInt _ -> false ) x and is_free_in_br {CAst.v=(ids,_,rt)} = (not (Id.List.mem id ids)) && is_free_in rt @@ -434,6 +437,7 @@ let replace_var_by_term x_id term = | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ | GHole _ as rt -> rt + | GInt _ as rt -> rt | GCast(b,c) -> GCast(replace_var_by_pattern b, Glob_ops.map_cast_type replace_var_by_pattern c) @@ -516,7 +520,7 @@ let expand_as = | PatCstr(_,patl,_) -> List.fold_left add_as map patl in let rec expand_as map = DAst.map (function - | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ as rt -> rt | GVar id as rt -> begin try diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 3a04c753ea..42dc66dcf4 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -166,7 +166,7 @@ let build_newrecursive let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evd = Evd.from_env env0 in - let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in let open Context.Named.Declaration in (EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) @@ -201,7 +201,7 @@ let is_rec names = let check_id id names = Id.Set.mem id names in let rec lookup names gt = match DAst.get gt with | GVar(id) -> check_id id names - | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ -> false | GCast(b,_) -> lookup names b | GRec _ -> error "GRec not handled" | GIf(b,_,lhs,rhs) -> diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 38f27f760b..a8517e9ab1 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -306,6 +306,7 @@ let check_not_nested sigma forbidden e = let rec check_not_nested e = match EConstr.kind sigma e with | Rel _ -> () + | Int _ -> () | Var x -> if Id.List.mem x forbidden then user_err ~hdr:"Recdef.check_not_nested" @@ -487,7 +488,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".") end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g - | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> + | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ -> let new_continuation_tac = jinfo.otherS () expr_info continuation_tac in new_continuation_tac expr_info g @@ -1294,6 +1295,7 @@ let is_opaque_constant c = | Declarations.OpaqueDef _ -> Proof_global.Opaque | Declarations.Undef _ -> Proof_global.Opaque | Declarations.Def _ -> Proof_global.Transparent + | Declarations.Primitive _ -> Proof_global.Opaque let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) @@ -1516,10 +1518,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let open CVars in let env = Global.env() in let evd = Evd.from_env env in - let evd, function_type = interp_type_evars env evd type_of_f in + let evd, function_type = interp_type_evars ~program_mode:false env evd type_of_f in let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) - let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in + let evd, ty = interp_type_evars ~program_mode:false env evd ~impls:rec_impls eq in let evd = Evd.minimize_universes evd in let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in @@ -1545,7 +1547,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in + let univs = Evd.univ_entry ~poly:false evd in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res in (* Refresh the global universes, now including those of _F *) diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 47f593ff3e..ffd8b71e5d 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -50,7 +50,8 @@ let with_delayed_uconstr ist c tac = Pretyping.use_typeclasses = false; solve_unification_constraints = true; fail_evar = false; - expand_evars = true + expand_evars = true; + program_mode = false; } in let c = Tacinterp.type_uconstr ~flags ist c in Tacticals.New.tclDELAYEDWITHHOLES false c tac @@ -344,7 +345,9 @@ let constr_flags () = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics (); Pretyping.fail_evar = false; - Pretyping.expand_evars = true } + Pretyping.expand_evars = true; + Pretyping.program_mode = false; +} let refine_tac ist simple with_classes c = Proofview.Goal.enter begin fun gl -> diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 7be8f67616..663537f3e8 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -56,7 +56,8 @@ let eval_uconstrs ist cs = Pretyping.use_typeclasses = false; solve_unification_constraints = true; fail_evar = false; - expand_evars = true + expand_evars = true; + program_mode = false; } in let map c env sigma = c env sigma in List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index d9b19c1ae6..4c24f51b1e 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -58,15 +58,8 @@ let new_entry name = let toplevel_selector = new_entry "vernac:toplevel_selector" let tacdef_body = new_entry "tactic:tacdef_body" -(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for - proof editing and changes nothing else). Then sets it as the default proof mode. *) -let _ = - let mode = { - Proof_global.name = "Classic"; - set = (fun () -> Pvernac.set_command_entry tactic_mode); - reset = (fun () -> Pvernac.(set_command_entry noedit_mode)); - } in - Proof_global.register_proof_mode mode +(* Registers [tactic_mode] as a parser for proof editing *) +let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode (* Hack to parse "[ id" without dropping [ *) let test_bracket_ident = diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 1ea6ff84d4..cdee012a82 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -83,7 +83,7 @@ open Obligations let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac -let classify_obbl _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) +let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater) } diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 31fb1c9abf..db8d1b20d8 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -285,13 +285,13 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF add_morphism_infer atts m n; } | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater } + => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { add_morphism atts [] m s n; } | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater } + => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { add_morphism atts binders m s n; } diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 46ea3819ac..7bf705ffeb 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -287,10 +287,10 @@ GRAMMAR EXTEND Gram [ [ c = smart_global; nl = occs -> { (nl,c) } ] ] ; intropatterns: - [ [ l = LIST0 nonsimple_intropattern -> { l } ] ] + [ [ l = LIST0 intropattern -> { l } ] ] ; ne_intropatterns: - [ [ l = LIST1 nonsimple_intropattern -> { l } ] ] + [ [ l = LIST1 intropattern -> { l } ] ] ; or_and_intropattern: [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> { IntroOrPattern tc } @@ -317,7 +317,7 @@ GRAMMAR EXTEND Gram | "?" -> { IntroAnonymous } | id = ident -> { IntroIdentifier id } ] ] ; - nonsimple_intropattern: + intropattern: [ [ l = simple_intropattern -> { l } | "*" -> { CAst.make ~loc @@ IntroForthcoming true } | "**" -> { CAst.make ~loc @@ IntroForthcoming false } ] ] @@ -534,6 +534,8 @@ GRAMMAR EXTEND Gram { TacAtom (CAst.make ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) } | IDENT "eintros"; pl = ne_intropatterns -> { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,pl)) } + | IDENT "eintros" -> + { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,[CAst.make ~loc @@IntroForthcoming false])) } | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ","; inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (true,false,cl,inhyp)) } diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 4bb52f599a..7da4464e59 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1889,7 +1889,7 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let univs = Evd.const_univ_entry ~poly sigma in + let univs = Evd.univ_entry ~poly sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = @@ -1975,7 +1975,7 @@ let add_morphism_infer atts m n = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in if Lib.is_modtype () then - let uctx = UState.const_univ_entry ~poly:atts.polymorphic uctx in + let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry (None,(instance,uctx),None), @@ -2014,7 +2014,7 @@ let add_morphism atts binders m s n = in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance - (Some (true, CAst.make @@ CRecord [])) + None ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 3e7479903a..30f716d764 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -117,9 +117,14 @@ let combine_appl appl1 appl2 = let of_tacvalue v = in_gen (topwit wit_tacvalue) v let to_tacvalue v = out_gen (topwit wit_tacvalue) v +let log_trace = ref false + +let is_traced () = + !log_trace || !Flags.profile_ltac + (** More naming applications *) let name_vfun appl vle = - if has_type vle (topwit wit_tacvalue) then + if is_traced () && has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with | VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t)) | _ -> vle @@ -137,9 +142,11 @@ type interp_sign = Geninterp.interp_sign = { lfun : value Id.Map.t; extra : TacStore.t } -let extract_trace ist = match TacStore.get ist.extra f_trace with -| None -> [] -| Some l -> l +let extract_trace ist = + if is_traced () then match TacStore.get ist.extra f_trace with + | None -> [] + | Some l -> l + else [] let print_top_val env v = Pptactic.pr_value Pptactic.ltop v @@ -161,8 +168,11 @@ let catch_error call_trace f x = let e = CErrors.push e in catching_error call_trace iraise e +let wrap_error tac k = + if is_traced () then Proofview.tclORELSE tac k else tac + let catch_error_tac call_trace tac = - Proofview.tclORELSE + wrap_error tac (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e)) @@ -203,9 +213,11 @@ let constr_of_id env id = (** Generic arguments : table of interpretation functions *) (* Some of the code further down depends on the fact that push_trace does not modify sigma (the evar map) *) -let push_trace call ist = match TacStore.get ist.extra f_trace with -| None -> Proofview.tclUNIT [call] -| Some trace -> Proofview.tclUNIT (call :: trace) +let push_trace call ist = + if is_traced () then match TacStore.get ist.extra f_trace with + | None -> Proofview.tclUNIT [call] + | Some trace -> Proofview.tclUNIT (call :: trace) + else Proofview.tclUNIT [] let propagate_trace ist loc id v = if has_type v (topwit wit_tacvalue) then @@ -530,7 +542,15 @@ let interp_gen kind ist pattern_mode flags env sigma c = invariant that running the tactic returned by push_trace does not modify sigma. *) let (_, dummy_proofview) = Proofview.init sigma [] in - let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in + + (* Again this is called at times with no open proof! *) + let name, poly = + try + let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in + name, poly + with | Proof_global.NoCurrentProof -> Id.of_string "tacinterp", false + in + let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in let (evd,c) = catch_error trace (understand_ltac flags env sigma vars kind) term in @@ -544,7 +564,9 @@ let constr_flags () = { use_typeclasses = true; solve_unification_constraints = true; fail_evar = true; - expand_evars = true } + expand_evars = true; + program_mode = false; +} (* Interprets a constr; expects evars to be solved *) let interp_constr_gen kind ist env sigma c = @@ -558,19 +580,25 @@ let open_constr_use_classes_flags () = { use_typeclasses = true; solve_unification_constraints = true; fail_evar = false; - expand_evars = true } + expand_evars = true; + program_mode = false; +} let open_constr_no_classes_flags () = { use_typeclasses = false; solve_unification_constraints = true; fail_evar = false; - expand_evars = true } + expand_evars = true; + program_mode = false; +} let pure_open_constr_flags = { use_typeclasses = false; solve_unification_constraints = true; fail_evar = false; - expand_evars = false } + expand_evars = false; + program_mode = false; +} (* Interprets an open constr *) let interp_open_constr ?(expected_type=WithoutTypeConstraint) ?(flags=open_constr_no_classes_flags ()) ist env sigma c = @@ -1247,7 +1275,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = let fold accu (id, v) = Id.Map.add id v accu in let newlfun = List.fold_left fold olfun extfun in if List.is_empty lvar then - begin Proofview.tclORELSE + begin wrap_error begin let ist = { lfun = newlfun; @@ -1407,7 +1435,7 @@ and interp_match_successes lz ist s = (* Interprets the Match expressions *) and interp_match ist lz constr lmr = let (>>=) = Ftactic.bind in - begin Proofview.tclORELSE + begin wrap_error (interp_ltac_constr ist constr) begin function | (e, info) -> @@ -1493,7 +1521,7 @@ and interp_genarg_var_list ist x = (* Interprets tactic expressions : returns a "constr" *) and interp_ltac_constr ist e : EConstr.t Ftactic.t = let (>>=) = Ftactic.bind in - begin Proofview.tclORELSE + begin wrap_error (val_interp ist e) begin function (err, info) -> match err with | Not_found -> @@ -2033,7 +2061,16 @@ let _ = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun = lfun; extra; } in let tac = interp_tactic ist tac in - let name, poly = Id.of_string "ltac_sub", false in + (* XXX: This depends on the global state which is bad; the hooking + mechanism should be modified. *) + let name, poly = + try + let (_, poly, _) = Proof_global.get_current_persistence () in + let name = Proof_global.get_current_proof_name () in + name, poly + with | Proof_global.NoCurrentProof -> + Id.of_string "ltac_gen", false + in let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in (EConstr.of_constr c, sigma) in @@ -2051,4 +2088,13 @@ let () = optread = (fun () -> get_debug () != Tactic_debug.DebugOff); optwrite = vernac_debug } +let () = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "Ltac Backtrace"; + optkey = ["Ltac"; "Backtrace"]; + optread = (fun () -> !log_trace); + optwrite = (fun b -> log_trace := b) } + let () = Hook.set Vernacentries.interp_redexp_hook interp_redexp diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index d4bafe773f..7adae148bd 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -846,7 +846,7 @@ struct match env with | [] -> ([v],n) | e::l -> - if EConstr.eq_constr sigma e v + if EConstr.eq_constr_nounivs sigma e v then (env,n) else let (env,n) = _add l ( n+1) v in diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index c5a09d677e..a964febf9c 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -452,6 +452,7 @@ constructor;red;intros;subst;trivial. Qed. Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)). +Defined. Instance Rri : (Ring (Ro:=Rops)). constructor; @@ -468,6 +469,7 @@ Class can_compute_Z (z : Z) := dummy_can_compute_Z : True. Hint Extern 0 (can_compute_Z ?v) => match isZcst v with true => exact I end : typeclass_instances. Instance reify_IZR z lvar {_ : can_compute_Z z} : reify (PEc z) lvar (IZR z). +Defined. Lemma R_one_zero: 1%R <> 0%R. discrR. @@ -484,6 +486,7 @@ exact Rmult_integral. exact R_one_zero. Defined. Require Import QArith. Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). +Defined. Instance Qri : (Ring (Ro:=Qops)). constructor. diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 94a3d40441..695f000cb1 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -12,6 +12,120 @@ Require Import Arith Max Min BinInt BinNat Znat Nnat. Local Open Scope Z_scope. +(** * [Z.div_mod_to_equations], [Z.quot_rem_to_equations], [Z.to_euclidean_division_equations]: the tactics for preprocessing [Z.div] and [Z.modulo], [Z.quot] and [Z.rem] *) + +(** These tactic use the complete specification of [Z.div] and + [Z.modulo] ([Z.quot] and [Z.rem], respectively) to remove these + functions from the goal without losing information. The + [Z.euclidean_division_equations_cleanup] tactic removes needless + hypotheses, which makes tactics like [nia] run faster. The tactic + [Z.to_euclidean_division_equations] combines the handling of both variants + of division/quotient and modulo/remainder. *) + +Module Z. + Lemma mod_0_r_ext x y : y = 0 -> x mod y = 0. + Proof. intro; subst; destruct x; reflexivity. Qed. + Lemma div_0_r_ext x y : y = 0 -> x / y = 0. + Proof. intro; subst; destruct x; reflexivity. Qed. + + Lemma rem_0_r_ext x y : y = 0 -> Z.rem x y = x. + Proof. intro; subst; destruct x; reflexivity. Qed. + Lemma quot_0_r_ext x y : y = 0 -> Z.quot x y = 0. + Proof. intro; subst; destruct x; reflexivity. Qed. + + Lemma rem_bound_pos_pos x y : 0 < y -> 0 <= x -> 0 <= Z.rem x y < y. + Proof. intros; apply Z.rem_bound_pos; assumption. Qed. + Lemma rem_bound_neg_pos x y : y < 0 -> 0 <= x -> 0 <= Z.rem x y < -y. + Proof. rewrite <- Z.rem_opp_r'; intros; apply Z.rem_bound_pos; rewrite ?Z.opp_pos_neg; assumption. Qed. + Lemma rem_bound_pos_neg x y : 0 < y -> x <= 0 -> -y < Z.rem x y <= 0. + Proof. rewrite <- (Z.opp_involutive x), Z.rem_opp_l', <- Z.opp_lt_mono, and_comm, !Z.opp_nonpos_nonneg; apply rem_bound_pos_pos. Qed. + Lemma rem_bound_neg_neg x y : y < 0 -> x <= 0 -> y < Z.rem x y <= 0. + Proof. rewrite <- (Z.opp_involutive x), <- (Z.opp_involutive y), Z.rem_opp_l', <- Z.opp_lt_mono, and_comm, !Z.opp_nonpos_nonneg, Z.opp_involutive; apply rem_bound_neg_pos. Qed. + + Ltac div_mod_to_equations_generalize x y := + pose proof (Z.div_mod x y); + pose proof (Z.mod_pos_bound x y); + pose proof (Z.mod_neg_bound x y); + pose proof (div_0_r_ext x y); + pose proof (mod_0_r_ext x y); + let q := fresh "q" in + let r := fresh "r" in + set (q := x / y) in *; + set (r := x mod y) in *; + clearbody q r. + Ltac quot_rem_to_equations_generalize x y := + pose proof (Z.quot_rem' x y); + pose proof (rem_bound_pos_pos x y); + pose proof (rem_bound_pos_neg x y); + pose proof (rem_bound_neg_pos x y); + pose proof (rem_bound_neg_neg x y); + pose proof (quot_0_r_ext x y); + pose proof (rem_0_r_ext x y); + let q := fresh "q" in + let r := fresh "r" in + set (q := Z.quot x y) in *; + set (r := Z.rem x y) in *; + clearbody q r. + + Ltac div_mod_to_equations_step := + match goal with + | [ |- context[?x / ?y] ] => div_mod_to_equations_generalize x y + | [ |- context[?x mod ?y] ] => div_mod_to_equations_generalize x y + | [ H : context[?x / ?y] |- _ ] => div_mod_to_equations_generalize x y + | [ H : context[?x mod ?y] |- _ ] => div_mod_to_equations_generalize x y + end. + Ltac quot_rem_to_equations_step := + match goal with + | [ |- context[Z.quot ?x ?y] ] => quot_rem_to_equations_generalize x y + | [ |- context[Z.rem ?x ?y] ] => quot_rem_to_equations_generalize x y + | [ H : context[Z.quot ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y + | [ H : context[Z.rem ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y + end. + Ltac div_mod_to_equations' := repeat div_mod_to_equations_step. + Ltac quot_rem_to_equations' := repeat quot_rem_to_equations_step. + Ltac euclidean_division_equations_cleanup := + repeat match goal with + | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl) + | [ H : ?x <> ?x -> _ |- _ ] => clear H + | [ H : ?x < ?x -> _ |- _ ] => clear H + | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H') + | [ H : ?T -> _, H' : ~?T |- _ ] => clear H + | [ H : ~?T -> _, H' : ?T |- _ ] => clear H + | [ H : ?A -> ?x = ?x -> _ |- _ ] => specialize (fun a => H a eq_refl) + | [ H : ?A -> ?x <> ?x -> _ |- _ ] => clear H + | [ H : ?A -> ?x < ?x -> _ |- _ ] => clear H + | [ H : ?A -> ?B -> _, H' : ?B |- _ ] => specialize (fun a => H a H') + | [ H : ?A -> ?B -> _, H' : ~?B |- _ ] => clear H + | [ H : ?A -> ~?B -> _, H' : ?B |- _ ] => clear H + | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H + | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H + | [ H : ?A -> 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H + | [ H : ?A -> ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H + | [ H : 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H + | [ H : ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H + | [ H : ?A -> 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H + | [ H : ?A -> ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H + | [ H : 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H + | [ H : ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H + | [ H : ?A -> 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H + | [ H : ?A -> ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H + | [ H : 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x (eq_sym pf))) + | [ H : ?A -> 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl 0 x (eq_sym pf))) + | [ H : ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x pf)) + | [ H : ?A -> ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl x 0 pf)) + | [ H : ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H + | [ H : ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H + | [ H : ?A -> ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H + | [ H : ?A -> ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H + | [ H : ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H + | [ H : ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H + | [ H : ?A -> ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H + | [ H : ?A -> ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H + end. + Ltac div_mod_to_equations := div_mod_to_equations'; euclidean_division_equations_cleanup. + Ltac quot_rem_to_equations := quot_rem_to_equations'; euclidean_division_equations_cleanup. + Ltac to_euclidean_division_equations := div_mod_to_equations'; quot_rem_to_equations'; euclidean_division_equations_cleanup. +End Z. (** * zify: the Z-ification tactic *) @@ -411,6 +525,24 @@ Ltac zify_N_op := | |- context [ Z.of_N (N.mul ?a ?b) ] => pose proof (N2Z.is_nonneg (N.mul a b)); rewrite (N2Z.inj_mul a b) in * + (* N.div -> Z.div and a positivity hypothesis *) + | H : context [ Z.of_N (N.div ?a ?b) ] |- _ => + pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in * + | |- context [ Z.of_N (N.div ?a ?b) ] => + pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in * + + (* N.modulo -> Z.rem / Z.modulo and a positivity hypothesis (N.modulo agrees with Z.modulo on everything except 0; so we pose both the non-zero proof for this agreement, but also replace things with [Z.rem]) *) + | H : context [ Z.of_N (N.modulo ?a ?b) ] |- _ => + pose proof (N2Z.is_nonneg (N.modulo a b)); + pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); + pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); + rewrite (N2Z.inj_rem a b) in * + | |- context [ Z.of_N (N.div ?a ?b) ] => + pose proof (N2Z.is_nonneg (N.modulo a b)); + pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); + pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); + rewrite (N2Z.inj_rem a b) in * + (* atoms of type N : we add a positivity condition (if not already there) *) | _ : 0 <= Z.of_N ?a |- _ => hide_Z_of_N a | _ : context [ Z.of_N ?a ] |- _ => pose proof (N2Z.is_nonneg a); hide_Z_of_N a diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 1ca6227f25..aa0370b2ac 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -32,6 +32,7 @@ Lemma Zsth : Equivalence (@eq Z). Proof. exact Z.eq_equiv. Qed. Instance Zops:@Ring_ops Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z). +Defined. Instance Zr: (@Ring _ _ _ _ _ _ _ _ Zops). Proof. diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v index 7958507819..c8d560cfe9 100644 --- a/plugins/setoid_ring/Ncring_tac.v +++ b/plugins/setoid_ring/Ncring_tac.v @@ -27,41 +27,50 @@ Class nth (R:Type) (t:R) (l:list R) (i:nat). Instance Ifind0 (R:Type) (t:R) l : nth t(t::l) 0. +Defined. Instance IfindS (R:Type) (t2 t1:R) l i {_:nth t1 l i} : nth t1 (t2::l) (S i) | 1. +Defined. Class closed (T:Type) (l:list T). Instance Iclosed_nil T : closed (T:=T) nil. +Defined. Instance Iclosed_cons T t (l:list T) {_:closed l} : closed (t::l). +Defined. Class reify (R:Type)`{Rr:Ring (T:=R)} (e:PExpr Z) (lvar:list R) (t:R). Instance reify_zero (R:Type) lvar op `{Ring (T:=R)(ring0:=op)} : reify (ring0:=op)(PEc 0%Z) lvar op. +Defined. Instance reify_one (R:Type) lvar op `{Ring (T:=R)(ring1:=op)} : reify (ring1:=op) (PEc 1%Z) lvar op. +Defined. Instance reifyZ0 (R:Type) lvar `{Ring (T:=R)} : reify (PEc Z0) lvar Z0|11. +Defined. Instance reifyZpos (R:Type) lvar (p:positive) `{Ring (T:=R)} : reify (PEc (Zpos p)) lvar (Zpos p)|11. +Defined. Instance reifyZneg (R:Type) lvar (p:positive) `{Ring (T:=R)} : reify (PEc (Zneg p)) lvar (Zneg p)|11. +Defined. Instance reify_add (R:Type) e1 lvar t1 e2 t2 op @@ -69,6 +78,7 @@ Instance reify_add (R:Type) {_:reify (add:=op) e1 lvar t1} {_:reify (add:=op) e2 lvar t2} : reify (add:=op) (PEadd e1 e2) lvar (op t1 t2). +Defined. Instance reify_mul (R:Type) e1 lvar t1 e2 t2 op @@ -76,6 +86,7 @@ Instance reify_mul (R:Type) {_:reify (mul:=op) e1 lvar t1} {_:reify (mul:=op) e2 lvar t2} : reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2)|10. +Defined. Instance reify_mul_ext (R:Type) `{Ring R} lvar (z:Z) e2 t2 @@ -83,6 +94,7 @@ Instance reify_mul_ext (R:Type) `{Ring R} {_:reify e2 lvar t2} : reify (PEmul (PEc z) e2) lvar (@multiplication Z _ _ z t2)|9. +Defined. Instance reify_sub (R:Type) e1 lvar t1 e2 t2 op @@ -90,24 +102,28 @@ Instance reify_sub (R:Type) {_:reify (sub:=op) e1 lvar t1} {_:reify (sub:=op) e2 lvar t2} : reify (sub:=op) (PEsub e1 e2) lvar (op t1 t2). +Defined. Instance reify_opp (R:Type) e1 lvar t1 op `{Ring (T:=R)(opp:=op)} {_:reify (opp:=op) e1 lvar t1} : reify (opp:=op) (PEopp e1) lvar (op t1). +Defined. Instance reify_pow (R:Type) `{Ring R} e1 lvar t1 n `{Ring (T:=R)} {_:reify e1 lvar t1} : reify (PEpow e1 n) lvar (pow_N t1 n)|1. +Defined. Instance reify_var (R:Type) t lvar i `{nth R t lvar i} `{Rr: Ring (T:=R)} : reify (Rr:= Rr) (PEX Z (Pos.of_succ_nat i))lvar t | 100. +Defined. Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R) (lterm:list R). @@ -115,12 +131,14 @@ Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R) Instance reify_nil (R:Type) lvar `{Rr: Ring (T:=R)} : reifylist (Rr:= Rr) nil lvar (@nil R). +Defined. Instance reify_cons (R:Type) e1 lvar t1 lexpr2 lterm2 `{Rr: Ring (T:=R)} {_:reify (Rr:= Rr) e1 lvar t1} {_:reifylist (Rr:= Rr) lexpr2 lvar lterm2} : reifylist (Rr:= Rr) (e1::lexpr2) lvar (t1::lterm2). +Defined. Definition list_reifyl (R:Type) lexpr lvar lterm `{Rr: Ring (T:=R)} diff --git a/plugins/setoid_ring/Rings_Q.v b/plugins/setoid_ring/Rings_Q.v index ae91ee1664..df3677e1c3 100644 --- a/plugins/setoid_ring/Rings_Q.v +++ b/plugins/setoid_ring/Rings_Q.v @@ -15,6 +15,7 @@ Require Export Integral_domain. Require Import QArith. Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). +Defined. Instance Qri : (Ring (Ro:=Qops)). constructor. diff --git a/plugins/setoid_ring/Rings_R.v b/plugins/setoid_ring/Rings_R.v index 901b36ed3b..fe7558845d 100644 --- a/plugins/setoid_ring/Rings_R.v +++ b/plugins/setoid_ring/Rings_R.v @@ -20,6 +20,7 @@ constructor;red;intros;subst;trivial. Qed. Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)). +Defined. Instance Rri : (Ring (Ro:=Rops)). constructor; diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 65201d922f..3f69701bd3 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -153,7 +153,7 @@ let decl_constant na univs c = let open Constr in let vars = CVars.universes_of_constr c in let univs = UState.restrict_universe_context univs vars in - let univs = Monomorphic_const_entry univs in + let univs = Monomorphic_entry univs in mkConst(declare_constant (Id.of_string na) (DefinitionEntry (definition_entry ~opaque:true ~univs c), IsProof Lemma)) diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index dd2c2d0ba4..0897d3b45b 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -67,7 +67,7 @@ type ssrview = ast_closure_term list type id_block = Prefix of Id.t | SuffixId of Id.t | SuffixNum of int (* Only [One] forces an introduction, possibly reducing the goal. *) -type anon_iter = +type anon_kind = | One of string option (* name hint *) | Drop | All @@ -76,25 +76,23 @@ type anon_iter = type ssripat = | IPatNoop | IPatId of Id.t - | IPatAnon of anon_iter (* inaccessible name *) -(* TODO | IPatClearMark *) - | IPatDispatch of bool (* ssr exception: accept a dispatch on the empty list even when there are subgoals *) * ssripatss_or_block (* (..|..) *) - | IPatCase of (* ipats_mod option * *) ssripatss_or_block (* this is not equivalent to /case /[..|..] if there are already multiple goals *) + | IPatAnon of anon_kind (* inaccessible name *) + | IPatDispatch of ssripatss_or_block (* (..|..) *) + | IPatCase of ssripatss_or_block (* [..|..] *) | IPatInj of ssripatss | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir - | IPatView of bool * ssrview (* {}/view (true if the clear is present) *) + | IPatView of ssrview (* /view *) | IPatClear of ssrclear (* {H1 H2} *) | IPatSimpl of ssrsimpl | IPatAbstractVars of Id.t list | IPatFastNondep - | IPatEqGen of unit Proofview.tactic (* internal use: generation of eqn *) and ssripats = ssripat list and ssripatss = ssripats list and ssripatss_or_block = | Block of id_block | Regular of ssripats list -type ssrhpats = ((ssrclear * ssripats) * ssripats) * ssripats +type ssrhpats = ((ssrclear option * ssripats) * ssripats) * ssripats type ssrhpats_wtransp = bool * ssrhpats (* tac => inpats *) @@ -139,6 +137,9 @@ type 'tac ssrhint = bool * 'tac option list type 'tac fwdbinders = bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)) +type 'tac ffwbinders = + (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)) + type clause = (ssrclear * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 311d912efd..0961edb6cb 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -66,7 +66,7 @@ let check_hyp_exists hyps (SsrHyp(_, id)) = try ignore(Context.Named.lookup id hyps) with Not_found -> errorstrm Pp.(str"No assumption is named " ++ Id.print id) -let test_hypname_exists hyps id = +let test_hyp_exists hyps (SsrHyp(_, id)) = try ignore(Context.Named.lookup id hyps); true with Not_found -> false @@ -243,7 +243,9 @@ let interp_refine ist gl rc = Pretyping.use_typeclasses = true; solve_unification_constraints = true; fail_evar = false; - expand_evars = true } + expand_evars = true; + program_mode = false; + } in let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in (* ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 51116ccd75..e642b5e788 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -29,7 +29,7 @@ val allocc : ssrocc val hyp_id : ssrhyp -> Id.t val hyps_ids : ssrhyps -> Id.t list val check_hyp_exists : ('a, 'b) Context.Named.pt -> ssrhyp -> unit -val test_hypname_exists : ('a, 'b) Context.Named.pt -> Id.t -> bool +val test_hyp_exists : ('a, 'b) Context.Named.pt -> ssrhyp -> bool val check_hyps_uniq : Id.t list -> ssrhyps -> unit val not_section_id : Id.t -> bool val hyp_err : ?loc:Loc.t -> string -> Id.t -> 'a diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 257ecd2a85..8c1363020a 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -94,17 +94,23 @@ let basecuttac name c gl = let introstac ipats = Proofview.V82.of_tactic (tclIPAT ipats) let havetac ist - (transp,((((clr, pats), binders), simpl), (((fk, _), t), hint))) + (transp,((((clr, orig_pats), binders), simpl), (((fk, _), t), hint))) suff namefst gl = let concl = pf_concl gl in + let pats = tclCompileIPats orig_pats in + let binders = tclCompileIPats binders in + let simpl = tclCompileIPats simpl in let skols, pats = - List.partition (function IPatAbstractVars _ -> true | _ -> false) pats in + List.partition (function IOpAbstractVars _ -> true | _ -> false) pats in let itac_mkabs = introstac skols in - let itac_c = introstac (IPatClear clr :: pats) in + let itac_c, clr = + match clr with + | None -> introstac pats, [] + | Some clr -> introstac (tclCompileIPats (IPatClear clr :: orig_pats)), clr in let itac, id, clr = introstac pats, Tacticals.tclIDTAC, old_cleartac clr in let binderstac n = - let rec aux = function 0 -> [] | n -> IPatAnon (One None) :: aux (n-1) in + let rec aux = function 0 -> [] | n -> IOpInaccessible None :: aux (n-1) in Tacticals.tclTHEN (if binders <> [] then introstac (aux n) else Tacticals.tclIDTAC) (introstac binders) in let simpltac = introstac simpl in @@ -160,7 +166,7 @@ let havetac ist gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c | FwdHave, false, false -> let skols = List.flatten (List.map (function - | IPatAbstractVars ids -> ids + | IOpAbstractVars ids -> ids | _ -> assert false) skols) in let skols_args = List.map (fun id -> Ssripats.Internal.examine_abstract (EConstr.mkVar id) gl) skols in @@ -203,10 +209,12 @@ let destProd_or_LetIn sigma c = | _ -> raise DestKO let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = + let clr0 = Option.default [] clr0 in + let pats = tclCompileIPats pats in let mkabs gen = abs_wgen false (fun x -> x) gen in let mkclr gen clrs = clr_of_wgen gen clrs in let mkpats = function - | _, Some ((x, _), _) -> fun pats -> IPatId (hoi_id x) :: pats + | _, Some ((x, _), _) -> fun pats -> IOpId (hoi_id x) :: pats | _ -> fun x -> x in let ct = match Ssrcommon.ssrterm_of_ast_closure_term ct with | (a, (b, Some ct)) -> @@ -265,7 +273,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = if gens = [] then errorstrm(str"gen have requires some generalizations"); let clear0 = old_cleartac clr0 in let id, name_general_hyp, cleanup, pats = match id, pats with - | None, (IPatId id as ip)::pats -> Some id, tacipat [ip], clear0, pats + | None, (IOpId id as ip)::pats -> Some id, tacipat [ip], clear0, pats | None, _ -> None, Tacticals.tclIDTAC, clear0, pats | Some (Some id),_ -> Some id, introid id, clear0, pats | Some _,_ -> @@ -289,6 +297,10 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = (** The "suffice" tactic *) let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) = + let clr = Option.default [] clr in + let pats = tclCompileIPats pats in + let binders = tclCompileIPats binders in + let simpl = tclCompileIPats simpl in let htac = Tacticals.tclTHEN (introstac pats) (hinttac ist true hint) in let c = match Ssrcommon.ssrterm_of_ast_closure_term c with | (a, (b, Some ct)) -> diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index 8a05e25504..35e89dbcea 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -22,7 +22,7 @@ val ssrposetac : Id.t * (ssrfwdfmt * ast_closure_term) -> v82tac val havetac : ist -> bool * - ((((Ssrast.ssrclear * Ssrast.ssripat list) * Ssrast.ssripats) * + ((((Ssrast.ssrclear option * Ssrast.ssripat list) * Ssrast.ssripats) * Ssrast.ssripats) * (((Ssrast.ssrfwdkind * 'a) * ast_closure_term) * (bool * Tacinterp.Value.t option list))) -> @@ -35,7 +35,7 @@ val basecuttac : val wlogtac : Ltac_plugin.Tacinterp.interp_sign -> - ((Ssrast.ssrhyps * Ssrast.ssripats) * 'a) * 'b -> + ((Ssrast.ssrclear option * Ssrast.ssripats) * 'a) * 'b -> (Ssrast.ssrhyps * ((Ssrast.ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) @@ -50,7 +50,7 @@ val wlogtac : val sufftac : Ssrast.ist -> - (((Ssrast.ssrhyps * Ssrast.ssripats) * Ssrast.ssripat list) * + (((Ssrast.ssrclear option * Ssrast.ssripats) * Ssrast.ssripat list) * Ssrast.ssripat list) * (('a * ast_closure_term) * diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index ce81d83661..a8dfd69240 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -19,14 +19,78 @@ open Proofview.Notations open Ssrast +type ssriop = + | IOpId of Names.Id.t + | IOpDrop + | IOpTemporay + | IOpInaccessible of string option + | IOpInaccessibleAll + | IOpAbstractVars of Names.Id.t list + | IOpFastNondep + + | IOpInj of ssriops list + + | IOpDispatchBlock of id_block + | IOpDispatchBranches of ssriops list + + | IOpCaseBlock of id_block + | IOpCaseBranches of ssriops list + + | IOpRewrite of ssrocc * ssrdir + | IOpView of ssrclear option * ssrview (* extra clears to be performed *) + + | IOpClear of ssrclear * ssrhyp option (* must clear, may clear *) + | IOpSimpl of ssrsimpl + + | IOpEqGen of unit Proofview.tactic (* generation of eqn *) + + | IOpNoop + +and ssriops = ssriop list + +let rec pr_ipatop = function + | IOpId id -> Names.Id.print id + | IOpDrop -> Pp.str "_" + | IOpTemporay -> Pp.str "+" + | IOpInaccessible None -> Pp.str "?" + | IOpInaccessible (Some s) -> Pp.str ("?«"^s^"»") + | IOpInaccessibleAll -> Pp.str "*" + | IOpAbstractVars l -> Pp.str ("[:"^String.concat " " (List.map Names.Id.to_string l)^"]") + | IOpFastNondep -> Pp.str ">" + + | IOpInj l -> Pp.(str "[=" ++ ppl l ++ str "]") + + | IOpDispatchBlock b -> Pp.(str"(" ++ Ssrprinters.pr_block b ++ str")") + | IOpDispatchBranches l -> Pp.(str "(" ++ ppl l ++ str ")") + + | IOpCaseBlock b -> Pp.(str"[" ++ Ssrprinters.pr_block b ++ str"]") + | IOpCaseBranches l -> Pp.(str "[" ++ ppl l ++ str "]") + + | IOpRewrite (occ,dir) -> Pp.(Ssrprinters.(pr_occ occ ++ pr_dir dir)) + | IOpView (None,vs) -> Pp.(prlist_with_sep mt (fun c -> str "/" ++ Ssrprinters.pr_ast_closure_term c) vs) + | IOpView (Some cl,vs) -> Pp.(Ssrprinters.pr_clear Pp.spc cl ++ prlist_with_sep mt (fun c -> str "/" ++ Ssrprinters.pr_ast_closure_term c) vs) + + | IOpClear (clmust,clmay) -> + Pp.(Ssrprinters.pr_clear spc clmust ++ + match clmay with + | Some cl -> str "(try " ++ Ssrprinters.pr_clear spc [cl] ++ str")" + | None -> mt ()) + | IOpSimpl s -> Ssrprinters.pr_simpl s + + | IOpEqGen _ -> Pp.str "E:" + | IOpNoop -> Pp.str"-" +and ppl x = Pp.(prlist_with_sep (fun () -> str"|") (prlist_with_sep spc pr_ipatop)) x + + module IpatMachine : sig (* the => tactical. ?eqtac is a tactic to be eventually run * after the first [..] block. first_case_is_dispatch is the * ssr exception to elim: and case: *) val main : ?eqtac:unit tactic -> first_case_is_dispatch:bool -> - ssripats -> unit tactic + ssriops -> unit tactic + val tclCompileIPats : ssripats -> ssriops val tclSEED_SUBGOALS : Names.Name.t list array -> unit tactic -> unit tactic @@ -53,7 +117,7 @@ module State : sig val isNSEED_CONSUME : (Names.Name.t list option -> unit tactic) -> unit tactic (* Some data may expire *) - val isTICK : ssripat -> unit tactic + val isTICK : ssriop -> unit tactic val isPRINT : Proofview.Goal.t -> Pp.t @@ -149,7 +213,7 @@ let isNSEED_CONSUME k = k x) let isTICK = function - | IPatSimpl _ | IPatClear _ -> tclUNIT () + | IOpSimpl _ | IOpClear _ -> tclUNIT () | _ -> tclGET (fun s -> tclSET { s with name_seed = None }) end (* }}} *************************************************************** *) @@ -238,6 +302,13 @@ let tacCHECK_HYPS_EXIST hyps = Goal.enter begin fun gl -> tclUNIT () end +let tacFILTER_HYP_EXIST hyps k = Goal.enter begin fun gl -> + let ctx = Goal.hyps gl in + k (Option.bind hyps (fun h -> + if Ssrcommon.test_hyp_exists ctx h && + Ssrcommon.(not_section_id (hyp_id h)) then Some h else None)) +end + (** [=> []] *****************************************************************) (* calls t1 then t2 on each subgoal passing to t2 the index of the current @@ -286,13 +357,13 @@ let tac_intro_seed interp_ipats fix = Goal.enter begin fun gl -> | Prefix id -> Id.to_string id ^ "?" | SuffixNum n -> "?" ^ string_of_int n | SuffixId id -> "?" ^ Id.to_string id in - IPatAnon (One (Some s)) + IOpInaccessible (Some s) | Name id -> let s = match fix with | Prefix fix -> Id.to_string fix ^ Id.to_string id | SuffixNum n -> Id.to_string id ^ string_of_int n | SuffixId fix -> Id.to_string id ^ Id.to_string fix in - IPatId (Id.of_string s)) seeds in + IOpId (Id.of_string s)) seeds in interp_ipats ipats end end @@ -342,7 +413,7 @@ let tclMK_ABSTRACT_VARS ids = (* Debugging *) let tclLOG p t = tclUNIT () >>= begin fun () -> - Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ Ssrprinters.pr_ipat p)); + Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ pr_ipatop p)); tclUNIT () end <*> Goal.enter begin fun g -> @@ -362,58 +433,74 @@ let tclLOG p t = let notTAC = tclUNIT false +let duplicate_clear = + CWarnings.create ~name:"duplicate-clear" ~category:"ssr" + (fun id -> Pp.(str "Duplicate clear of " ++ Id.print id)) + (* returns true if it was a tactic (eg /ltac:tactic) *) let rec ipat_tac1 ipat : bool tactic = match ipat with - | IPatView (clear_if_id,l) -> + | IOpView (glued_clear,l) -> + let clear_if_id, extra_clear = + match glued_clear with + | None -> false, [] + | Some x -> true, List.map Ssrcommon.hyp_id x in Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id - ~conclusion:(fun ~to_clear:clr -> intro_clear clr) + ~conclusion:(fun ~to_clear:clr -> + let inter = CList.intersect Id.equal clr extra_clear in + List.iter duplicate_clear inter; + let cl = CList.union Id.equal clr extra_clear in + intro_clear cl) - | IPatDispatch(true, Regular [[]]) -> - notTAC - | IPatDispatch(_, Regular ipatss) -> + | IOpDispatchBranches ipatss -> tclDISPATCH (List.map ipat_tac ipatss) <*> notTAC - | IPatDispatch(_,Block id_block) -> + | IOpDispatchBlock id_block -> tac_intro_seed ipat_tac id_block <*> notTAC - - | IPatId id -> Ssrcommon.tclINTRO_ID id <*> notTAC - | IPatFastNondep -> intro_anon_deps <*> notTAC - - | IPatCase (Block id_block) -> + | IOpCaseBlock id_block -> Ssrcommon.tclWITHTOP tac_case <*> tac_intro_seed ipat_tac id_block <*> notTAC - | IPatCase (Regular ipatss) -> + | IOpCaseBranches ipatss -> tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss <*> notTAC - | IPatInj ipatss -> + + | IOpId id -> Ssrcommon.tclINTRO_ID id <*> notTAC + | IOpFastNondep -> intro_anon_deps <*> notTAC + | IOpDrop -> intro_drop <*> notTAC + | IOpInaccessible seed -> Ssrcommon.tclINTRO_ANON ?seed () <*> notTAC + | IOpInaccessibleAll -> intro_anon_all <*> notTAC + | IOpTemporay -> intro_anon_temp <*> notTAC + + | IOpSimpl Nop -> assert false + + | IOpInj ipatss -> tclIORPAT (Ssrcommon.tclWITHTOP (fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t))) ipatss <*> notTAC - | IPatAnon Drop -> intro_drop <*> notTAC - | IPatAnon (One seed) -> Ssrcommon.tclINTRO_ANON ?seed () <*> notTAC - | IPatAnon All -> intro_anon_all <*> notTAC - | IPatAnon Temporary -> intro_anon_temp <*> notTAC - - | IPatNoop -> notTAC - | IPatSimpl Nop -> notTAC - - | IPatClear ids -> - tacCHECK_HYPS_EXIST ids <*> - intro_clear (List.map Ssrcommon.hyp_id ids) <*> + | IOpClear (must,may) -> + tacCHECK_HYPS_EXIST must <*> + tacFILTER_HYP_EXIST may (fun may -> + let must = List.map Ssrcommon.hyp_id must in + let cl = Option.fold_left (fun cls (SsrHyp(_,id)) -> + if CList.mem_f Id.equal id cls then begin + duplicate_clear id; + cls + end else id :: cls) must may in + intro_clear cl) <*> notTAC - | IPatSimpl x -> + | IOpSimpl x -> V82.tactic ~nf_evars:false (Ssrequality.simpltac x) <*> notTAC - | IPatRewrite (occ,dir) -> + | IOpRewrite (occ,dir) -> Ssrcommon.tclWITHTOP (fun x -> V82.tactic ~nf_evars:false (Ssrequality.ipat_rewrite occ dir x)) <*> notTAC - | IPatAbstractVars ids -> tclMK_ABSTRACT_VARS ids <*> notTAC + | IOpAbstractVars ids -> tclMK_ABSTRACT_VARS ids <*> notTAC - | IPatEqGen t -> t <*> notTAC + | IOpEqGen t -> t <*> notTAC + | IOpNoop -> notTAC and ipat_tac pl : unit tactic = match pl with @@ -433,51 +520,88 @@ and tclIORPAT tac = function | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p) and ssr_exception is_on = function - | Some (IPatCase l) when is_on -> Some (IPatDispatch(true, l)) + | Some (IOpCaseBranches [[]]) when is_on -> Some IOpNoop + | Some (IOpCaseBranches l) when is_on -> + Some (IOpDispatchBranches l) + | Some (IOpCaseBlock s) when is_on -> + Some (IOpDispatchBlock s) | x -> x and option_to_list = function None -> [] | Some x -> [x] and split_at_first_case ipats = let rec loop acc = function - | (IPatSimpl _ | IPatClear _) as x :: rest -> loop (x :: acc) rest - | (IPatCase _ | IPatDispatch _) as x :: xs -> CList.rev acc, Some x, xs + | (IOpSimpl _ | IOpClear _) as x :: rest -> loop (x :: acc) rest + | (IOpCaseBlock _ | IOpCaseBranches _ + | IOpDispatchBlock _ | IOpDispatchBranches _) as x :: xs -> + CList.rev acc, Some x, xs | pats -> CList.rev acc, None, pats in loop [] ipats ;; (* Simple pass doing {x}/v -> /v{x} *) -let elaborate_ipats l = +let tclCompileIPats l = let rec elab = function + + | (IPatClear cl) :: (IPatView v) :: rest -> + (IOpView(Some cl,v)) :: elab rest + | (IPatClear cl) :: (IPatId id) :: rest -> + (IOpClear (cl,Some (SsrHyp(None,id)))) :: IOpId id :: elab rest + + (* boring code *) | [] -> [] - | (IPatClear _ as p1) :: (IPatView _ as p2) :: rest -> p2 :: p1 :: elab rest - | IPatDispatch(s, Regular p) :: rest -> IPatDispatch (s, Regular (List.map elab p)) :: elab rest - | IPatCase (Regular p) :: rest -> IPatCase (Regular (List.map elab p)) :: elab rest - | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest - | (IPatEqGen _ | IPatId _ | IPatSimpl _ | IPatClear _ | IPatFastNondep | - IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ | - IPatAbstractVars _ | IPatDispatch(_, Block _) | IPatCase(Block _)) as x :: rest -> x :: elab rest - in - elab l -let main ?eqtac ~first_case_is_dispatch ipats = - let ipats = elaborate_ipats ipats in - let ip_before, case, ip_after = split_at_first_case ipats in + | IPatId id :: rest -> IOpId id :: elab rest + | IPatAnon (One hint) ::rest -> IOpInaccessible hint :: elab rest + | IPatAnon Drop :: rest -> IOpDrop :: elab rest + | IPatAnon All :: rest -> IOpInaccessibleAll :: elab rest + | IPatAnon Temporary :: rest -> IOpTemporay :: elab rest + | IPatAbstractVars vs :: rest -> IOpAbstractVars vs :: elab rest + | IPatFastNondep :: rest -> IOpFastNondep :: elab rest + + | IPatInj pats :: rest -> IOpInj (List.map elab pats) :: elab rest + | IPatRewrite(occ,dir) :: rest -> IOpRewrite(occ,dir) :: elab rest + | IPatView vs :: rest -> IOpView (None,vs) :: elab rest + | IPatSimpl s :: rest -> IOpSimpl s :: elab rest + | IPatClear cl :: rest -> IOpClear (cl,None) :: elab rest + + | IPatCase (Block seed) :: rest -> IOpCaseBlock seed :: elab rest + | IPatCase (Regular bs) :: rest -> IOpCaseBranches (List.map elab bs) :: elab rest + | IPatDispatch (Block seed) :: rest -> IOpDispatchBlock seed :: elab rest + | IPatDispatch (Regular bs) :: rest -> IOpDispatchBranches (List.map elab bs) :: elab rest + | IPatNoop :: rest -> IOpNoop :: elab rest + + in + elab l +;; +let tclCompileIPats l = + Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats input: " ++ + prlist_with_sep spc Ssrprinters.pr_ipat l)); + let ops = tclCompileIPats l in + Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats output: " ++ + prlist_with_sep spc pr_ipatop ops)); + ops + +let main ?eqtac ~first_case_is_dispatch iops = + let ip_before, case, ip_after = split_at_first_case iops in let case = ssr_exception first_case_is_dispatch case in let case = option_to_list case in - let eqtac = option_to_list (Option.map (fun x -> IPatEqGen x) eqtac) in - Ssrcommon.tcl0G ~default:() (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end) + let eqtac = option_to_list (Option.map (fun x -> IOpEqGen x) eqtac) in + let ipats = ip_before @ case @ eqtac @ ip_after in + Ssrcommon.tcl0G ~default:() (ipat_tac ipats <*> intro_end) end (* }}} *) let tclIPAT_EQ eqtac ip = Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); - IpatMachine.main ~eqtac ~first_case_is_dispatch:true ip + IpatMachine.(main ~eqtac ~first_case_is_dispatch:true (tclCompileIPats ip)) let tclIPATssr ip = Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); - IpatMachine.main ~first_case_is_dispatch:true ip + IpatMachine.(main ~first_case_is_dispatch:true (tclCompileIPats ip)) + +let tclCompileIPats = IpatMachine.tclCompileIPats (* Common code to handle generalization lists along with the defective case *) let with_defective maintac deps clr = Goal.enter begin fun g -> @@ -721,12 +845,12 @@ let eqmovetac _ gen = ;; let rec eqmoveipats eqpat = function - | (IPatSimpl _ | IPatClear _ as ipat) :: ipats -> + | (IOpSimpl _ | IOpClear _ as ipat) :: ipats -> ipat :: eqmoveipats eqpat ipats - | (IPatAnon All :: _ | []) as ipats -> - IPatAnon (One None) :: eqpat :: ipats + | (IOpInaccessibleAll :: _ | []) as ipats -> + IOpInaccessible None :: eqpat @ ipats | ipat :: ipats -> - ipat :: eqpat :: ipats + ipat :: eqpat @ ipats let ssrsmovetac = Goal.enter begin fun g -> let sigma, concl = Goal.(sigma g, concl g) in @@ -736,7 +860,6 @@ let ssrsmovetac = Goal.enter begin fun g -> end let tclIPAT ip = - Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); IpatMachine.main ~first_case_is_dispatch:false ip let ssrmovetac = function @@ -748,17 +871,17 @@ let ssrmovetac = function gentac <*> tclLAST_GEN ~to_ind:false lastgen (tacVIEW_THEN_GRAB view ~conclusion) <*> - tclIPAT (IPatClear clr :: ipats) + tclIPAT (IOpClear (clr,None) :: IpatMachine.tclCompileIPats ipats) | _::_ as view, (_, ({ gens = []; clr }, ipats)) -> - tclIPAT (IPatView (false,view) :: IPatClear clr :: ipats) + tclIPAT (IOpView (None,view) :: IOpClear (clr,None) :: IpatMachine.tclCompileIPats ipats) | _, (Some pat, (dgens, ipats)) -> let dgentac = with_dgens dgens eqmovetac in - dgentac <*> tclIPAT (eqmoveipats pat ipats) + dgentac <*> tclIPAT (eqmoveipats (IpatMachine.tclCompileIPats [pat]) (IpatMachine.tclCompileIPats ipats)) | _, (_, ({ gens = (_ :: _ as gens); dgens = []; clr}, ipats)) -> let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) in - gentac <*> tclIPAT ipats + gentac <*> tclIPAT (IpatMachine.tclCompileIPats ipats) | _, (_, ({ clr }, ipats)) -> - Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT ipats] + Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT (IpatMachine.tclCompileIPats ipats)] (** [abstract: absvar gens] **************************************************) let rec is_Evar_or_CastedMeta sigma x = diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli index 89cba4be71..893061b154 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -19,8 +19,44 @@ open Ssrast +(* Atomic operations for the IPat machine. Use this if you are "patching" an + * ipat written by the user, since patching it at he AST level and then + * compiling it may have tricky effects, eg adding a clear in front of a view + * also has the effect of disposing the view (the compilation phase takes care + * of this, by using the compiled ipats you can be more precise *) +type ssriop = + | IOpId of Names.Id.t + | IOpDrop + | IOpTemporay + | IOpInaccessible of string option + | IOpInaccessibleAll + | IOpAbstractVars of Names.Id.t list + | IOpFastNondep + + | IOpInj of ssriops list + + | IOpDispatchBlock of id_block + | IOpDispatchBranches of ssriops list + + | IOpCaseBlock of id_block + | IOpCaseBranches of ssriops list + + | IOpRewrite of ssrocc * ssrdir + | IOpView of ssrclear option * ssrview (* extra clears to be performed *) + + | IOpClear of ssrclear * ssrhyp option + | IOpSimpl of ssrsimpl + + | IOpEqGen of unit Proofview.tactic (* generation of eqn *) + + | IOpNoop + +and ssriops = ssriop list + +val tclCompileIPats : ssripats -> ssriops + (* The => tactical *) -val tclIPAT : ssripats -> unit Proofview.tactic +val tclIPAT : ssriops -> unit Proofview.tactic (* As above but with the SSR exception: first case is dispatch *) val tclIPATssr : ssripats -> unit Proofview.tactic diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 76726009ac..2a2cd73df2 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -591,10 +591,8 @@ END GRAMMAR EXTEND Gram GLOBAL: ssrfwdview; ssrfwdview: [ - [ test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr -> - { [mk_ast_closure_term `None c] } - | test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrfwdview -> - { (mk_ast_closure_term `None c) :: w } ]]; + [ test_not_ssrslashnum; "/"; c = ast_closure_term -> { [c] } + | test_not_ssrslashnum; "/"; c = ast_closure_term; w = ssrfwdview -> { c :: w } ]]; END (* ipats *) @@ -635,11 +633,10 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function | IPatClear clr -> IPatClear (List.map map_ssrhyp clr) | IPatCase (Regular iorpat) -> IPatCase (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)) | IPatCase (Block(hat)) -> IPatCase (Block(map_block map_id hat)) - | IPatDispatch (s, Regular iorpat) -> IPatDispatch (s, Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)) - | IPatDispatch (s, Block (hat)) -> IPatDispatch (s, Block(map_block map_id hat)) + | IPatDispatch (Regular iorpat) -> IPatDispatch (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)) + | IPatDispatch (Block (hat)) -> IPatDispatch (Block(map_block map_id hat)) | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) - | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v) - | IPatEqGen _ -> assert false (*internal usage only *) + | IPatView v -> IPatView (List.map map_ast_closure_term v) and map_block map_id = function | Prefix id -> Prefix (map_id id) | SuffixId id -> SuffixId (map_id id) @@ -715,22 +712,22 @@ let interp_ipat ist gl = if not (ltacvar id) then hyp :: hyps else add_intro_pattern_hyps CAst.(make ?loc (interp_introid ist gl id)) hyps in let clr' = List.fold_right add_hyps clr [] in - check_hyps_uniq [] clr'; IPatClear clr' + check_hyps_uniq [] clr'; + IPatClear clr' | IPatCase(Regular iorpat) -> IPatCase(Regular(List.map (List.map interp) iorpat)) | IPatCase(Block(hat)) -> IPatCase(Block(interp_block hat)) - | IPatDispatch(s,Regular iorpat) -> - IPatDispatch(s,Regular (List.map (List.map interp) iorpat)) - | IPatDispatch(s,Block(hat)) -> IPatDispatch(s,Block(interp_block hat)) + | IPatDispatch(Regular iorpat) -> + IPatDispatch(Regular (List.map (List.map interp) iorpat)) + | IPatDispatch(Block(hat)) -> IPatDispatch(Block(interp_block hat)) | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat) | IPatAbstractVars l -> IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l)) - | IPatView (clr,l) -> IPatView (clr,List.map (fun x -> snd(interp_ast_closure_term ist + | IPatView l -> IPatView (List.map (fun x -> snd(interp_ast_closure_term ist gl x)) l) | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop | IPatFastNondep) as x -> x - | IPatEqGen _ -> assert false (*internal usage only *) in interp @@ -765,10 +762,6 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats } | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, R2L)] | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)] } - | [ ssrdocc(occ) ssrfwdview(v) ] -> { match occ with - | Some [], _ -> [IPatView (true,v)] - | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl;IPatView (false,v)] - | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") } | [ ssrdocc(occ) ] -> { match occ with | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl] | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") } @@ -786,7 +779,7 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats } | [ "-/" integer(n) "/=" ] -> { [IPatNoop;IPatSimpl(SimplCut (n,~-1))] } | [ "-/" integer(n) "/" integer (m) "=" ] -> { [IPatNoop;IPatSimpl(SimplCut(n,m))] } - | [ ssrfwdview(v) ] -> { [IPatView (false,v)] } + | [ ssrfwdview(v) ] -> { [IPatView v] } | [ "[" ":" ident_list(idl) "]" ] -> { [IPatAbstractVars idl] } | [ "[:" ident_list(idl) "]" ] -> { [IPatAbstractVars idl] } END @@ -875,11 +868,12 @@ ARGUMENT EXTEND ssripats_ne TYPED AS ssripat PRINTED BY { pr_ssripats } let check_ssrhpats loc w_binders ipats = let err_loc s = CErrors.user_err ~loc ~hdr:"ssreflect" s in let clr, ipats = + let opt_app = function None -> fun l -> Some l + | Some l1 -> fun l2 -> Some (l1 @ l2) in let rec aux clr = function - | IPatClear cl :: tl -> aux (clr @ cl) tl -(* | IPatSimpl (cl, sim) :: tl -> clr @ cl, IPatSimpl ([], sim) :: tl *) + | IPatClear cl :: tl -> aux (opt_app clr cl) tl | tl -> clr, tl - in aux [] ipats in + in aux None ipats in let simpl, ipats = match List.rev ipats with | IPatSimpl _ as s :: tl -> [s], List.rev tl @@ -903,27 +897,29 @@ let check_ssrhpats loc w_binders ipats = in loop [] ipats in ((clr, ipat), binders), simpl +let pr_clear_opt sep = function None -> mt () | Some x -> pr_clear sep x + let pr_hpats (((clr, ipat), binders), simpl) = - pr_clear mt clr ++ pr_ipats ipat ++ pr_ipats binders ++ pr_ipats simpl + pr_clear_opt mt clr ++ pr_ipats ipat ++ pr_ipats binders ++ pr_ipats simpl let pr_ssrhpats _ _ _ = pr_hpats let pr_ssrhpats_wtransp _ _ _ (_, x) = pr_hpats x } -ARGUMENT EXTEND ssrhpats TYPED AS (((ssrclear * ssripat) * ssripat) * ssripat) +ARGUMENT EXTEND ssrhpats TYPED AS (((ssrclear option * ssripat) * ssripat) * ssripat) PRINTED BY { pr_ssrhpats } | [ ssripats(i) ] -> { check_ssrhpats loc true i } END ARGUMENT EXTEND ssrhpats_wtransp - TYPED AS (bool * (((ssrclear * ssripats) * ssripats) * ssripats)) + TYPED AS (bool * (((ssrclear option * ssripats) * ssripats) * ssripats)) PRINTED BY { pr_ssrhpats_wtransp } | [ ssripats(i) ] -> { false,check_ssrhpats loc true i } | [ ssripats(i) "@" ssripats(j) ] -> { true,check_ssrhpats loc true (i @ j) } END ARGUMENT EXTEND ssrhpats_nobs -TYPED AS (((ssrclear * ssripats) * ssripats) * ssripats) PRINTED BY { pr_ssrhpats } +TYPED AS (((ssrclear option * ssripats) * ssripats) * ssripats) PRINTED BY { pr_ssrhpats } | [ ssripats(i) ] -> { check_ssrhpats loc false i } END @@ -2051,7 +2047,7 @@ END (* We just add a numeric version that clears the n top assumptions. *) TACTIC EXTEND ssrclear - | [ "clear" natural(n) ] -> { tclIPAT (List.init n (fun _ -> IPatAnon Drop)) } + | [ "clear" natural(n) ] -> { tclIPAT (List.init n (fun _ -> IOpDrop)) } END (** The "move" tactic *) @@ -2090,10 +2086,10 @@ let movearg_of_parsed_movearg (v,(eq,(dg,ip))) = TACTIC EXTEND ssrmove | [ "move" ssrmovearg(arg) ssrrpat(pat) ] -> - { ssrmovetac (movearg_of_parsed_movearg arg) <*> tclIPAT [pat] } + { ssrmovetac (movearg_of_parsed_movearg arg) <*> tclIPAT (tclCompileIPats [pat]) } | [ "move" ssrmovearg(arg) ssrclauses(clauses) ] -> { tclCLAUSES (ssrmovetac (movearg_of_parsed_movearg arg)) clauses } -| [ "move" ssrrpat(pat) ] -> { tclIPAT [pat] } +| [ "move" ssrrpat(pat) ] -> { tclIPAT (tclCompileIPats [pat]) } | [ "move" ] -> { ssrsmovetac } END @@ -2632,7 +2628,11 @@ END { -let augment_preclr clr1 (((clr0, x),y),z) = (((clr1 @ clr0, x),y),z) +let augment_preclr clr1 (((clr0, x),y),z) = + let cl = match clr0 with + | None -> if clr1 = [] then None else Some clr1 + | Some clr0 -> Some (clr1 @ clr0) in + (((cl, x),y),z) } diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index a2cbd3c9c8..7844050272 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -32,6 +32,19 @@ type ssrfwdview = ast_closure_term list type ssreqid = ssripat option type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats)) +val wit_ssrseqdir : ssrdir Genarg.uniform_genarg_type +val wit_ssrseqarg : (Tacexpr.raw_tactic_expr ssrseqarg, Tacexpr.glob_tactic_expr ssrseqarg, Geninterp.Val.t ssrseqarg) Genarg.genarg_type + +val wit_ssrintrosarg : + (Tacexpr.raw_tactic_expr * ssripats, + Tacexpr.glob_tactic_expr * ssripats, + Geninterp.Val.t * ssripats) Genarg.genarg_type + +val wit_ssrsufffwd : + (Tacexpr.raw_tactic_expr ffwbinders, + Tacexpr.glob_tactic_expr ffwbinders, + Geninterp.Val.t ffwbinders) Genarg.genarg_type + val wit_ssripatrep : ssripat Genarg.uniform_genarg_type val wit_ssrarg : ssrarg Genarg.uniform_genarg_type val wit_ssrrwargs : ssrrwarg list Genarg.uniform_genarg_type @@ -47,3 +60,43 @@ val wit_ssrhintarg : (Tacexpr.raw_tactic_expr ssrhint, Tacexpr.glob_tactic_expr ssrhint, Tacinterp.Value.t ssrhint) Genarg.genarg_type + +val wit_ssrexactarg : ssrapplyarg Genarg.uniform_genarg_type +val wit_ssrcongrarg : ((int * ssrterm) * cpattern ssragens) Genarg.uniform_genarg_type +val wit_ssrfwdid : Names.Id.t Genarg.uniform_genarg_type + +val wit_ssrsetfwd : + ((ssrfwdfmt * (cpattern * ast_closure_term option)) * ssrdocc) Genarg.uniform_genarg_type + +val wit_ssrdoarg : + (Tacexpr.raw_tactic_expr ssrdoarg, + Tacexpr.glob_tactic_expr ssrdoarg, + Tacinterp.Value.t ssrdoarg) Genarg.genarg_type + +val wit_ssrhint : + (Tacexpr.raw_tactic_expr ssrhint, + Tacexpr.glob_tactic_expr ssrhint, + Tacinterp.Value.t ssrhint) Genarg.genarg_type + +val wit_ssrhpats : ssrhpats Genarg.uniform_genarg_type +val wit_ssrhpats_nobs : ssrhpats Genarg.uniform_genarg_type +val wit_ssrhpats_wtransp : ssrhpats_wtransp Genarg.uniform_genarg_type + +val wit_ssrposefwd : (ssrfwdfmt * ast_closure_term) Genarg.uniform_genarg_type + +val wit_ssrrpat : ssripat Genarg.uniform_genarg_type +val wit_ssrterm : ssrterm Genarg.uniform_genarg_type +val wit_ssrunlockarg : (ssrocc * ssrterm) Genarg.uniform_genarg_type +val wit_ssrunlockargs : (ssrocc * ssrterm) list Genarg.uniform_genarg_type + +val wit_ssrwgen : clause Genarg.uniform_genarg_type +val wit_ssrwlogfwd : (clause list * (ssrfwdfmt * ast_closure_term)) Genarg.uniform_genarg_type + +val wit_ssrfixfwd : (Names.Id.t * (ssrfwdfmt * ast_closure_term)) Genarg.uniform_genarg_type +val wit_ssrfwd : (ssrfwdfmt * ast_closure_term) Genarg.uniform_genarg_type +val wit_ssrfwdfmt : ssrfwdfmt Genarg.uniform_genarg_type + +val wit_ssrcpat : ssripat Genarg.uniform_genarg_type +val wit_ssrdgens : cpattern ssragens Genarg.uniform_genarg_type +val wit_ssrdgens_tl : cpattern ssragens Genarg.uniform_genarg_type +val wit_ssrdir : ssrdir Genarg.uniform_genarg_type diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 898e03b00e..38f5b7d107 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -74,7 +74,7 @@ let pr_occ = function | None -> str "{}" let pr_clear_ne clr = str "{" ++ pr_hyps clr ++ str "}" -let pr_clear sep clr = if clr = [] then mt () else sep () ++ pr_clear_ne clr +let pr_clear sep clr = sep () ++ pr_clear_ne clr let pr_dir = function L2R -> str "->" | R2L -> str "<-" @@ -102,20 +102,18 @@ let rec pr_ipat p = | IPatClear clr -> pr_clear mt clr | IPatCase (Regular iorpat) -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]") | IPatCase (Block m) -> hov 1 (str"[" ++ pr_block m ++ str"]") - | IPatDispatch(_,Regular iorpat) -> hov 1 (str "(" ++ pr_iorpat iorpat ++ str ")") - | IPatDispatch (_,Block m) -> hov 1 (str"(" ++ pr_block m ++ str")") + | IPatDispatch(Regular iorpat) -> hov 1 (str "(" ++ pr_iorpat iorpat ++ str ")") + | IPatDispatch (Block m) -> hov 1 (str"(" ++ pr_block m ++ str")") | IPatInj iorpat -> hov 1 (str "[=" ++ pr_iorpat iorpat ++ str "]") | IPatRewrite (occ, dir) -> pr_occ occ ++ pr_dir dir | IPatAnon All -> str "*" | IPatAnon Drop -> str "_" | IPatAnon (One _) -> str "?" - | IPatView (false,v) -> pr_view2 v - | IPatView (true,v) -> str"{}" ++ pr_view2 v + | IPatView v -> pr_view2 v | IPatAnon Temporary -> str "+" | IPatNoop -> str "-" | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]" | IPatFastNondep -> str">" - | IPatEqGen _ -> str "<tac>" and pr_ipats ipats = pr_list spc pr_ipat ipats and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat and pr_block = function (Prefix id) -> str"^" ++ Id.print id diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 31c360ad6d..5f20ac2705 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -43,6 +43,7 @@ val pr_view2 : ast_closure_term list -> Pp.t val pr_ipat : ssripat -> Pp.t val pr_ipats : ssripats -> Pp.t val pr_iorpat : ssripatss -> Pp.t +val pr_block : id_block -> Pp.t val pr_hyp : ssrhyp -> Pp.t val pr_hyps : ssrhyps -> Pp.t diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 191a4e9a20..d083d34b52 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -596,26 +596,6 @@ VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF Ssrview.AdaptorDb.declare k hints } END -(** Canonical Structure alias *) - -GRAMMAR EXTEND Gram - GLOBAL: gallina_ext; - - gallina_ext: - (* Canonical structure *) - [[ IDENT "Canonical"; qid = Constr.global -> - { Vernacexpr.VernacCanonical (CAst.make @@ AN qid) } - | IDENT "Canonical"; ntn = Prim.by_notation -> - { Vernacexpr.VernacCanonical (CAst.make @@ ByNotation ntn) } - | IDENT "Canonical"; qid = Constr.global; - d = G_vernac.def_body -> - { let s = coerce_reference_to_id qid in - Vernacexpr.VernacDefinition - ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), - ((CAst.make (Name s)),None), d) } - ]]; -END - (** Keyword compatibility fixes. *) (* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *) diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 4816027296..2794696017 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -142,7 +142,7 @@ let intern_constr_expr { Genintern.genv; ltacvars = vars } sigma ce = To allow for t being a notation, like "Notation foo x := ltac:(foo x)", we need to internalize t. *) -let is_tac_in_term ?extra_scope { body; glob_env; interp_env } = +let is_tac_in_term ?extra_scope { annotation; body; glob_env; interp_env } = Goal.(enter_one ~__LOC__ begin fun goal -> let genv = env goal in let sigma = sigma goal in @@ -161,7 +161,7 @@ let is_tac_in_term ?extra_scope { body; glob_env; interp_env } = | Glob_term.GHole (_,_, Some x) when Genarg.has_type x (Genarg.glbwit Tacarg.wit_tactic) -> tclUNIT (`Tac (Genarg.out_gen (Genarg.glbwit Tacarg.wit_tactic) x)) - | _ -> tclUNIT (`Term (interp_env, g)) + | _ -> tclUNIT (`Term (annotation, interp_env, g)) end) (* To inject a constr into a glob_constr we use an Ltac variable *) @@ -207,7 +207,7 @@ let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t let tclADD_CLEAR_IF_ID (env, ist, t) x = Ssrprinters.ppdebug (lazy Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t)); - let hd, _ = EConstr.decompose_app ist t in + let hd, args = EConstr.decompose_app ist t in match EConstr.kind ist hd with | Constr.Var id when Ssrcommon.not_section_id id -> tclUNIT (x, [id]) | _ -> tclUNIT (x,[]) @@ -280,8 +280,9 @@ let interp_view ~clear_if_id ist v p = else tclKeepOpenConstr ot >>= tclPAIR [] (* we store in the state (v top), then (v1 (v2 top))... *) -let pile_up_view ~clear_if_id (ist, v) = +let pile_up_view ~clear_if_id (annotation, ist, v) = let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in + let clear_if_id = clear_if_id && annotation <> `Parens in State.vsPUSH (fun p -> interp_view ~clear_if_id ist v p) let finalize_view s0 ?(simple_types=true) p = diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg index 4ddaeb49fd..d1c7a23e99 100644 --- a/plugins/ssrmatching/g_ssrmatching.mlg +++ b/plugins/ssrmatching/g_ssrmatching.mlg @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) + { open Ltac_plugin diff --git a/plugins/ssrmatching/g_ssrmatching.mli b/plugins/ssrmatching/g_ssrmatching.mli index 588a1a3eac..65ea3f79c8 100644 --- a/plugins/ssrmatching/g_ssrmatching.mli +++ b/plugins/ssrmatching/g_ssrmatching.mli @@ -1,5 +1,14 @@ -(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) open Genarg open Ssrmatching diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index efd65ade15..552a4048b1 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -312,7 +312,8 @@ let iter_constr_LR f c = match kind c with | Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) -> for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done | Proj(_,a) -> f a - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> () + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ + | Int _) -> () (* The comparison used to determine which subterms matches is KEYED *) (* CONVERSION. This looks for convertible terms that either have the same *) diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml deleted file mode 100644 index e34a401c2c..0000000000 --- a/plugins/syntax/int31_syntax.ml +++ /dev/null @@ -1,114 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "int31_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -(* digit-based syntax for int31 *) - -open Bigint -open Names -open Globnames -open Glob_term - -(*** Constants for locating int31 constructors ***) - -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, _) -> GlobRef.equal 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 = - let mp = ModPath.MPdot (ModPath.MPfile (make_dir dir), Label.make modname) - in make_mind mp id - - -(* int31 stuff *) -let int31_module = ["Coq"; "Numbers"; "Cyclic"; "Int31"; "Int31"] -let int31_path = make_path int31_module "int31" -let int31_id = make_mind_mpfile int31_module -let int31_scope = "int31_scope" - -let int31_construct = ConstructRef ((int31_id "int31",0),1) - -let int31_0 = ConstructRef ((int31_id "digits",0),1) -let int31_1 = ConstructRef ((int31_id "digits",0),2) - -(*** Definition of the Non_closed exception, used in the pretty printing ***) -exception Non_closed - -(*** Parsing for int31 in digital notation ***) - -(* 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 = 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 - [] - else - let (q,r) = div2_with_rest n in - (if r then ref_1 else ref_0)::(args (counter-1) q) - in - 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.") - -let interp_int31 ?loc n = - if is_pos_or_zero n then - int31_of_pos_bigint ?loc n - else - error_negative ?loc - -(* Pretty prints an int31 *) - -let bigint_of_int31 = - let rec args_parsing args cur = - match args with - | [] -> 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 - 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 (AnyGlobConstr i) = - try - Some (bigint_of_int31 i) - with Non_closed -> - None - -open Notation - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -(* Actually declares the interpreter for int31 *) - -let _ = - register_bignumeral_interpretation int31_scope (interp_int31,uninterp_int31); - at_declare_ml_module enable_prim_token_interpretation - { pt_local = false; - pt_scope = int31_scope; - pt_interp_info = Uid int31_scope; - pt_required = (int31_path,int31_module); - pt_refs = [int31_construct]; - pt_in_match = true } diff --git a/plugins/syntax/int31_syntax_plugin.mlpack b/plugins/syntax/int31_syntax_plugin.mlpack deleted file mode 100644 index 54a5bc0cd1..0000000000 --- a/plugins/syntax/int31_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Int31_syntax diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml new file mode 100644 index 0000000000..992b7a986b --- /dev/null +++ b/plugins/syntax/int63_syntax.ml @@ -0,0 +1,55 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + + +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "int63_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + +(* digit-based syntax for int63 *) + +open Names +open Libnames + +(*** Constants for locating int63 constructors ***) + +let q_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.Int63.int" +let q_id_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.Int63.id_int" + +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) + +(* int63 stuff *) +let int63_module = ["Coq"; "Numbers"; "Cyclic"; "Int63"; "Int63"] +let int63_path = make_path int63_module "int" +let int63_scope = "int63_scope" + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + +(* Actually declares the interpreter for int63 *) + +let _ = + let open Notation in + at_declare_ml_module + (fun () -> + let id_int63 = Nametab.locate q_id_int63 in + let o = { to_kind = Int63, Direct; + to_ty = id_int63; + of_kind = Int63, Direct; + of_ty = id_int63; + ty_name = q_int63; + warning = Nop } in + enable_prim_token_interpretation + { pt_local = false; + pt_scope = int63_scope; + pt_interp_info = NumeralNotation o; + pt_required = (int63_path, int63_module); + pt_refs = []; + pt_in_match = false }) + () diff --git a/plugins/syntax/int63_syntax_plugin.mlpack b/plugins/syntax/int63_syntax_plugin.mlpack new file mode 100644 index 0000000000..d83d554fe6 --- /dev/null +++ b/plugins/syntax/int63_syntax_plugin.mlpack @@ -0,0 +1 @@ +Int63_syntax diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 470deb4a60..0c6d2ac0d1 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -33,30 +33,49 @@ let get_constructors ind = Array.to_list (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc) -let q_z = qualid_of_string "Coq.Numbers.BinNums.Z" -let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive" -let q_int = qualid_of_string "Coq.Init.Decimal.int" -let q_uint = qualid_of_string "Coq.Init.Decimal.uint" -let q_option = qualid_of_string "Coq.Init.Datatypes.option" +let qualid_of_ref n = + n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty + +let q_option () = qualid_of_ref "core.option.type" let unsafe_locate_ind q = match Nametab.locate q with | IndRef i -> i | _ -> raise Not_found -let locate_ind q = - try unsafe_locate_ind q - with Not_found -> Nametab.error_global_not_found q - let locate_z () = - try - Some { z_ty = unsafe_locate_ind q_z; - pos_ty = unsafe_locate_ind q_positive } - with Not_found -> None + let zn = "num.Z.type" in + let pn = "num.pos.type" in + if Coqlib.has_ref zn && Coqlib.has_ref pn + then + let q_z = qualid_of_ref zn in + let q_pos = qualid_of_ref pn in + Some ({ + z_ty = unsafe_locate_ind q_z; + pos_ty = unsafe_locate_ind q_pos; + }, mkRefC q_z) + else None let locate_int () = - { uint = locate_ind q_uint; - int = locate_ind q_int } + let int = "num.int.type" in + let uint = "num.uint.type" in + if Coqlib.has_ref int && Coqlib.has_ref uint + then + let q_int = qualid_of_ref int in + let q_uint = qualid_of_ref uint in + Some ({ + int = unsafe_locate_ind q_int; + uint = unsafe_locate_ind q_uint; + }, mkRefC q_int, mkRefC q_uint) + else None + +let locate_int63 () = + let int63n = "num.int63.type" in + if Coqlib.has_ref int63n + then + let q_int63 = qualid_of_ref int63n in + Some (mkRefC q_int63) + else None let has_type f ty = let (sigma, env) = Pfedit.get_current_context () in @@ -64,65 +83,65 @@ let has_type f ty = try let _ = Constrintern.interp_constr env sigma c in true with Pretype_errors.PretypeError _ -> false -let type_error_to f ty loadZ = +let type_error_to f ty = CErrors.user_err (pr_qualid f ++ str " should go from Decimal.int to " ++ pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ - fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ - (if loadZ then str " (require BinNums first)." else str ".")) + fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).") -let type_error_of g ty loadZ = +let type_error_of g ty = CErrors.user_err (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ - str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ - (if loadZ then str " (require BinNums first)." else str ".")) + str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).") let vernac_numeral_notation local ty f g scope opts = let int_ty = locate_int () in let z_pos_ty = locate_z () in + let int63_ty = locate_int63 () in let tyc = Smartlocate.global_inductive_with_alias ty in let to_ty = Smartlocate.global_with_alias f in let of_ty = Smartlocate.global_with_alias g in let cty = mkRefC ty in let app x y = mkAppC (x,[y]) in - let cref q = mkRefC q in let arrow x y = mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) in - let cZ = cref q_z in - let cint = cref q_int in - let cuint = cref q_uint in - let coption = cref q_option in - let opt r = app coption r in + let opt r = app (mkRefC (q_option ())) r in let constructors = get_constructors tyc in (* Check the type of f *) let to_kind = - if has_type f (arrow cint cty) then Int int_ty, Direct - else if has_type f (arrow cint (opt cty)) then Int int_ty, Option - else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct - else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option - else - match z_pos_ty with - | Some z_pos_ty -> - if has_type f (arrow cZ cty) then Z z_pos_ty, Direct - else if has_type f (arrow cZ (opt cty)) then Z z_pos_ty, Option - else type_error_to f ty false - | None -> type_error_to f ty true + match int_ty with + | Some (int_ty, cint, _) when has_type f (arrow cint cty) -> Int int_ty, Direct + | Some (int_ty, cint, _) when has_type f (arrow cint (opt cty)) -> Int int_ty, Option + | Some (int_ty, _, cuint) when has_type f (arrow cuint cty) -> UInt int_ty.uint, Direct + | Some (int_ty, _, cuint) when has_type f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option + | _ -> + match z_pos_ty with + | Some (z_pos_ty, cZ) when has_type f (arrow cZ cty) -> Z z_pos_ty, Direct + | Some (z_pos_ty, cZ) when has_type f (arrow cZ (opt cty)) -> Z z_pos_ty, Option + | _ -> + match int63_ty with + | Some cint63 when has_type f (arrow cint63 cty) -> Int63, Direct + | Some cint63 when has_type f (arrow cint63 (opt cty)) -> Int63, Option + | _ -> type_error_to f ty in (* Check the type of g *) let of_kind = - if has_type g (arrow cty cint) then Int int_ty, Direct - else if has_type g (arrow cty (opt cint)) then Int int_ty, Option - else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct - else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option - else - match z_pos_ty with - | Some z_pos_ty -> - if has_type g (arrow cty cZ) then Z z_pos_ty, Direct - else if has_type g (arrow cty (opt cZ)) then Z z_pos_ty, Option - else type_error_of g ty false - | None -> type_error_of g ty true + match int_ty with + | Some (int_ty, cint, _) when has_type g (arrow cty cint) -> Int int_ty, Direct + | Some (int_ty, cint, _) when has_type g (arrow cty (opt cint)) -> Int int_ty, Option + | Some (int_ty, _, cuint) when has_type g (arrow cty cuint) -> UInt int_ty.uint, Direct + | Some (int_ty, _, cuint) when has_type g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option + | _ -> + match z_pos_ty with + | Some (z_pos_ty, cZ) when has_type g (arrow cty cZ) -> Z z_pos_ty, Direct + | Some (z_pos_ty, cZ) when has_type g (arrow cty (opt cZ)) -> Z z_pos_ty, Option + | _ -> + match int63_ty with + | Some cint63 when has_type g (arrow cty cint63) -> Int63, Direct + | Some cint63 when has_type g (arrow cty (opt cint63)) -> Int63, Option + | _ -> type_error_of g ty in let o = { to_kind; to_ty; of_kind; of_ty; ty_name = ty; diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune index 1ab16c700d..aac46338ea 100644 --- a/plugins/syntax/plugin_base.dune +++ b/plugins/syntax/plugin_base.dune @@ -20,8 +20,8 @@ (libraries coq.vernac)) (library - (name int31_syntax_plugin) - (public_name coq.plugins.int31_syntax) - (synopsis "Coq syntax plugin: int31") - (modules int31_syntax) + (name int63_syntax_plugin) + (public_name coq.plugins.int63_syntax) + (synopsis "Coq syntax plugin: int63") + (modules int63_syntax) (libraries coq.vernac)) |