From e43b1768d0f8399f426b92f4dfe31955daceb1a4 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 16 Feb 2018 01:02:17 +0100 Subject: Primitive integers This work makes it possible to take advantage of a compact representation for integers in the entire system, as opposed to only in some reduction machines. It is useful for heavily computational applications, where even constructing terms is not possible without such a representation. Concretely, it replaces part of the retroknowledge machinery with a primitive construction for integers in terms, and introduces a kind of FFI which maps constants to operators (on integers). Properties of these operators are expressed as explicit axioms, whereas they were hidden in the retroknowledge-based approach. This has been presented at the Coq workshop and some Coq Working Groups, and has been used by various groups for STM trace checking, computational analysis, etc. Contributions by Guillaume Bertholon and Pierre Roux Co-authored-by: Benjamin Grégoire Co-authored-by: Vincent Laporte --- plugins/extraction/extract_env.ml | 2 +- plugins/extraction/extraction.ml | 19 +++-- plugins/extraction/haskell.ml | 2 + plugins/extraction/json.ml | 4 + plugins/extraction/miniml.ml | 1 + plugins/extraction/miniml.mli | 1 + plugins/extraction/mlutil.ml | 29 ++++--- plugins/extraction/modutil.ml | 2 +- plugins/extraction/ocaml.ml | 4 + plugins/extraction/scheme.ml | 2 + plugins/funind/functional_principles_proofs.ml | 3 +- plugins/funind/glob_term_to_relation.ml | 5 +- plugins/funind/glob_termops.ml | 6 +- plugins/funind/indfun.ml | 2 +- plugins/funind/recdef.ml | 4 +- plugins/ssrmatching/ssrmatching.ml | 3 +- plugins/syntax/int31_syntax.ml | 114 ------------------------- plugins/syntax/int31_syntax_plugin.mlpack | 1 - plugins/syntax/int63_syntax.ml | 55 ++++++++++++ plugins/syntax/int63_syntax_plugin.mlpack | 1 + plugins/syntax/numeral.ml | 21 ++++- plugins/syntax/plugin_base.dune | 8 +- 22 files changed, 138 insertions(+), 151 deletions(-) delete mode 100644 plugins/syntax/int31_syntax.ml delete mode 100644 plugins/syntax/int31_syntax_plugin.mlpack create mode 100644 plugins/syntax/int63_syntax.ml create mode 100644 plugins/syntax/int63_syntax_plugin.mlpack (limited to 'plugins') 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..c15486ea10 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] *) @@ -1063,7 +1064,7 @@ 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) @@ -1079,7 +1080,7 @@ 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) @@ -1107,7 +1108,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/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 4b6caea70d..02964d7ba5 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -478,7 +478,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 +588,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 +1222,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..d9b0330e2b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -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..1b5286dce4 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); *) 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 *) -(* 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 *) +(* 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 ea564ae2ba..0c6d2ac0d1 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -69,6 +69,14 @@ let locate_int () = }, 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 let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in @@ -79,17 +87,18 @@ 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 (you may need to require BinNums or Decimal first).") + 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 = 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 (you may need to require BinNums or Decimal first).") + 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 @@ -111,6 +120,10 @@ let vernac_numeral_notation local ty f g scope opts = 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 *) @@ -124,6 +137,10 @@ let vernac_numeral_notation local ty f g scope opts = 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; 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)) -- cgit v1.2.3