diff options
Diffstat (limited to 'interp')
36 files changed, 596 insertions, 404 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 4bdacda529..21f682ac0e 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -57,26 +57,8 @@ type abstraction_kind = AbsLambda | AbsPi type proj_flag = int option (** [Some n] = proj of the n-th visible argument *) -(** Representation of decimal literals that appear in Coq scripts. - We now use raw strings following the format defined by - [NumTok.t] and a separate sign flag. - - Note that this representation is not unique, due to possible - multiple leading or trailing zeros, and -0 = +0, for instances. - The reason to keep the numeral exactly as it was parsed is that - specific notations can be declared for specific numerals - (e.g. [Notation "0" := False], or [Notation "00" := (nil,nil)], or - [Notation "2e1" := ...]). Those notations, which override the - generic interpretation as numeral, use the same representation of - numeral using the Numeral constructor. So the latter should be able - to record the form of the numeral which exactly matches the - notation. *) - -type sign = SPlus | SMinus -type raw_numeral = NumTok.t - type prim_token = - | Numeral of sign * raw_numeral + | Numeral of NumTok.Signed.t | String of string type instance_expr = Glob_term.glob_level list diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 401853b625..d4369e9bd1 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -48,10 +48,9 @@ let names_of_local_binders bl = are considered different here. *) let prim_token_eq t1 t2 = match t1, t2 with -| Numeral (SPlus,n1), Numeral (SPlus,n2) -| Numeral (SMinus,n1), Numeral (SMinus,n2) -> NumTok.equal n1 n2 +| Numeral n1, Numeral n2 -> NumTok.Signed.equal n1 n2 | String s1, String s2 -> String.equal s1 s2 -| (Numeral ((SPlus|SMinus),_) | String _), _ -> false +| (Numeral _ | String _), _ -> false let explicitation_eq ex1 ex2 = match ex1, ex2 with | ExplByPos (i1, id1), ExplByPos (i2, id2) -> diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index a05a9cb999..edf52c93e8 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 44aacd62d8..7a14ca3e48 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -354,27 +354,21 @@ let drop_implicits_in_patt cst nb_expl args = let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None -let is_zero s = - let rec aux i = - Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1)) - in aux 0 -let is_zero n = is_zero n.NumTok.int && is_zero n.NumTok.frac - let make_notation_gen loc ntn mknot mkprim destprim l bl = match snd ntn,List.map destprim l with (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *) - | "- _", [Some (Numeral (SPlus,p))] when not (is_zero p) -> + | "- _", [Some (Numeral p)] when not (NumTok.Signed.is_zero p) -> assert (bl=[]); mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[]) | _ -> match decompose_notation_key ntn, l with | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] -> - begin match NumTok.of_string x with - | Some n -> mkprim (loc, Numeral (SMinus,n)) + begin match NumTok.Unsigned.parse_string x with + | Some n -> mkprim (loc, Numeral (NumTok.SMinus,n)) | None -> mknot (loc,ntn,l,bl) end | (InConstrEntrySomeLevel,[Terminal x]), [] -> - begin match NumTok.of_string x with - | Some n -> mkprim (loc, Numeral (SPlus,n)) + begin match NumTok.Unsigned.parse_string x with + | Some n -> mkprim (loc, Numeral (NumTok.SPlus,n)) | None -> mknot (loc,ntn,l,bl) end | _ -> mknot (loc,ntn,l,bl) @@ -899,13 +893,10 @@ let extern_float f scopes = else if Float64.is_infinity f then CRef(q_infinity (), None) else if Float64.is_neg_infinity f then CRef(q_neg_infinity (), None) else - let sign = if Float64.sign f then SMinus else SPlus in - let s = Float64.(to_string (abs f)) in - match NumTok.of_string s with - | None -> assert false - | Some n -> - extern_prim_token_delimiter_if_required (Numeral (sign, n)) - "float" "float_scope" scopes + let s = Float64.(to_string f) in + let n = NumTok.Signed.of_string s in + extern_prim_token_delimiter_if_required (Numeral n) + "float" "float_scope" scopes (**********************************************************************) (* mapping glob_constr to constr_expr *) @@ -926,7 +917,7 @@ let extern_ref vars ref us = let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) -let rec extern inctx scopes vars r = +let rec extern inctx ?impargs scopes vars r = match remove_one_coercion inctx (flatten_application r) with | Some (nargs,inctx,r') -> (try extern_notations scopes vars (Some nargs) r @@ -990,10 +981,10 @@ let rec extern inctx scopes vars r = | GLetIn (na,b,t,c) -> CLetIn (make ?loc na,sub_extern false scopes vars b, Option.map (extern_typ scopes vars) t, - extern inctx scopes (add_vname vars na) c) + extern inctx ?impargs scopes (add_vname vars na) c) | GProd (na,bk,t,c) -> - factorize_prod scopes vars na bk t c + factorize_prod ?impargs scopes vars na bk t c | GLambda (na,bk,t,c) -> factorize_lambda inctx scopes vars na bk t c @@ -1085,19 +1076,19 @@ let rec extern inctx scopes vars r = | GInt i -> extern_prim_token_delimiter_if_required - (Numeral (SPlus, NumTok.int (Uint63.to_string i))) + (Numeral (NumTok.Signed.of_int_string (Uint63.to_string i))) "int63" "int63_scope" (snd scopes) | GFloat f -> extern_float f (snd scopes) in insert_coercion coercion (CAst.make ?loc c) -and extern_typ (subentry,(_,scopes)) = - extern true (subentry,(Notation.current_type_scope_name (),scopes)) +and extern_typ ?impargs (subentry,(_,scopes)) = + extern true ?impargs (subentry,(Notation.current_type_scope_name (),scopes)) and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes)) -and factorize_prod scopes vars na bk t c = +and factorize_prod ?impargs scopes vars na bk t c = let implicit_type = is_reserved_type na t in let aty = extern_typ scopes vars t in let vars = add_vname vars na in @@ -1117,7 +1108,13 @@ and factorize_prod scopes vars na bk t c = | _ -> CProdN ([binder],b)) | _ -> assert false) | _, _ -> - let c' = extern_typ scopes vars c in + let impargs_hd, impargs_tl = + match impargs with + | Some [hd] -> Some hd, None + | Some (hd::tl) -> Some hd, Some tl + | _ -> None, None in + let bk = Option.default Explicit impargs_hd in + let c' = extern_typ ?impargs:impargs_tl scopes vars c in match na, c'.v with | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b) when binding_kind_eq bk bk' @@ -1306,8 +1303,8 @@ and extern_notation (custom,scopes as allscopes) vars t rules = let extern_glob_constr vars c = extern false (InConstrEntrySomeLevel,(None,[])) vars c -let extern_glob_type vars c = - extern_typ (InConstrEntrySomeLevel,(None,[])) vars c +let extern_glob_type ?impargs vars c = + extern_typ ?impargs (InConstrEntrySomeLevel,(None,[])) vars c (******************************************************************) (* Main translation function from constr -> constr_expr *) @@ -1320,7 +1317,7 @@ let extern_constr ?lax ?(inctx=false) ?scope env sigma t = let extern_constr_in_scope ?lax ?inctx scope env sigma t = extern_constr ?lax ?inctx ~scope env sigma t -let extern_type ?lax ?(goal_concl_style=false) env sigma t = +let extern_type ?lax ?(goal_concl_style=false) env sigma ?impargs t = (* "goal_concl_style" means do alpha-conversion using the "goal" convention *) (* i.e.: avoid using the names of goal/section/rel variables and the short *) (* names of global definitions of current module when computing names for *) @@ -1330,7 +1327,7 @@ let extern_type ?lax ?(goal_concl_style=false) env sigma t = (* consideration; see namegen.ml for further details *) let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype Detyping.Later ?lax goal_concl_style avoid env sigma t in - extern_glob_type (vars_of_env env) r + extern_glob_type ?impargs (vars_of_env env) r let extern_sort sigma s = extern_glob_sort (detype_sort sigma s) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 0eca287c1d..f85e49d2df 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -25,7 +25,7 @@ open Ltac_pretype val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr -val extern_glob_type : Id.Set.t -> 'a glob_constr_g -> constr_expr +val extern_glob_type : ?impargs:Glob_term.binding_kind list -> Id.Set.t -> 'a glob_constr_g -> constr_expr val extern_constr_pattern : names_context -> Evd.evar_map -> constr_pattern -> constr_expr val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> @@ -42,7 +42,7 @@ val extern_constr : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> val extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid -val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> types -> constr_expr +val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> types -> constr_expr val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> rel_context -> local_binder_expr list diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8a820293a0..905d9f1e5b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -32,6 +32,7 @@ open Notation_ops open Notation open Inductiveops open Context.Rel.Declaration +open NumTok (** constr_expr -> glob_constr translation: - it adds holes for implicit arguments @@ -47,7 +48,7 @@ open Context.Rel.Declaration types and recursive definitions and of projection names in records *) type var_internalization_type = - | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *) + | Inductive | Recursive | Method | Variable @@ -56,9 +57,6 @@ type var_internalization_data = (* type of the "free" variable, for coqdoc, e.g. while typing the constructor of JMeq, "JMeq" behaves as a variable of type Inductive *) var_internalization_type * - (* impargs to automatically add to the variable, e.g. for "JMeq A a B b" - in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) - Id.t list * (* signature of impargs of the variable *) Impargs.implicit_status list * (* subscopes of the args of the variable *) @@ -179,20 +177,9 @@ let parsing_explicit = ref false let empty_internalization_env = Id.Map.empty -let compute_explicitable_implicit imps = function - | Inductive (params,_) -> - (* In inductive types, the parameters are fixed implicit arguments *) - let sub_impl,_ = List.chop (List.length params) imps in - let sub_impl' = List.filter is_status_implicit sub_impl in - List.map name_of_implicit sub_impl' - | Recursive | Method | Variable -> - (* Unable to know in advance what the implicit arguments will be *) - [] - let compute_internalization_data env sigma ty typ impl = let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in - let expls_impl = compute_explicitable_implicit impl ty in - (ty, expls_impl, impl, compute_arguments_scope sigma typ) + (ty, impl, compute_arguments_scope sigma typ) let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty = List.fold_left3 @@ -354,7 +341,7 @@ let impls_binder_list = let impls_type_list n ?(args = []) = let rec aux acc n c = match DAst.get c with | GProd (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c - | _ -> (Variable,[],List.rev acc,[]) + | _ -> (Variable,List.rev acc,[]) in aux args n let impls_term_list n ?(args = []) = @@ -364,7 +351,7 @@ let impls_term_list n ?(args = []) = let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in let n,acc' = List.fold_left (fun (n,acc) (na, bk, _, _) -> (n+1,build_impls n bk na acc)) (n,acc) args.(nb) in aux acc' n bds.(nb) - |_ -> (Variable,[],List.rev acc,[]) + |_ -> (Variable,List.rev acc,[]) in aux args n (* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *) @@ -428,20 +415,6 @@ let locate_if_hole ?loc na c = match DAst.get c with with Not_found -> DAst.make ?loc @@ GHole (Evar_kinds.BinderType na, naming, arg)) | _ -> c -let reset_hidden_inductive_implicit_test env = - { env with impls = Id.Map.map (function - | (Inductive (params,_),b,c,d) -> (Inductive (params,false),b,c,d) - | x -> x) env.impls } - -let check_hidden_implicit_parameters ?loc id impls = - if Id.Map.exists (fun _ -> function - | (Inductive (indparams,check),_,_,_) when check -> Id.List.mem id indparams - | _ -> false) impls - then - user_err ?loc (Id.print id ++ strbrk " is already used as name of " ++ - strbrk "a parameter of the inductive type; bound variables in " ++ - strbrk "the type of a constructor shall use a different name.") - let pure_push_name_env (id,implargs) env = {env with ids = Id.Set.add id env.ids; @@ -455,7 +428,6 @@ let push_name_env ntnvars implargs env = | { loc; v = Anonymous } -> env | { loc; v = Name id } -> - check_hidden_implicit_parameters ?loc id env.impls ; if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var ?loc; set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars; @@ -491,7 +463,7 @@ let intern_generalized_binder intern_type ntnvars let ty' = intern_type {env with ids = ids; unb = true} ty in let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in let env' = List.fold_left - (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x)) + (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[])(*?*) env (make ?loc @@ Name x)) env fvs in let b' = check_implicit_meaningful ?loc b' env in let bl = List.map @@ -558,7 +530,7 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p = user_err ?loc (str "Unsupported nested \"as\" clause."); il,disjpat in - let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars (Variable,[],[],[]) env (make ?loc @@ Name id)) il env in + let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars (Variable,[],[]) env (make ?loc @@ Name id)) il env in let na = alias_of_pat (List.hd disjpat) in let ienv = Name.fold_right Id.Set.remove na env.ids in let id = Namegen.next_name_away_with_default "pat" na ienv in @@ -614,7 +586,7 @@ let intern_generalization intern env ntnvars loc bk ak c = GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc)) in List.fold_right (fun ({loc;v=id} as lid) (env, acc) -> - let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in + let env' = push_name_env ntnvars (Variable,[],[]) env CAst.(make @@ Name id) in (env', abs lid acc)) fvs (env,c) in c' @@ -705,7 +677,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam if onlyident then (* Do not try to interpret a variable as a constructor *) let na = out_patvar pat in - let env = push_name_env ntnvars (Variable,[],[],[]) env (make ?loc:pat.loc na) in + let env = push_name_env ntnvars (Variable,[],[]) env (make ?loc:pat.loc na) in (renaming,env), None, na else (* Interpret as a pattern *) @@ -908,9 +880,6 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = try let pat,(onlyident,scopes) = Id.Map.find id binders in let env = set_env_scopes env scopes in - (* We deactivate impls to avoid the check on hidden parameters *) - (* and since we are only interested in the pattern as a term *) - let env = reset_hidden_inductive_implicit_test env in if onlyident then term_of_name (out_patvar pat) else @@ -1014,7 +983,7 @@ let intern_notation intern env ntnvars loc ntn fullargs = (* Discriminating between bound variables and global references *) let string_of_ty = function - | Inductive _ -> "ind" + | Inductive -> "ind" | Recursive -> "def" | Method -> "meth" | Variable -> "var" @@ -1030,27 +999,25 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = if Id.Map.mem id ntnvars then begin if not (Id.Map.mem id env.impls) then set_var_scope ?loc id true (env.tmp_scope,env.scopes) ntnvars; - gvar (loc,id) us, [], [], [] + gvar (loc,id) us, [], [] end else (* Is [id] registered with implicit arguments *) try - let ty,expl_impls,impls,argsc = Id.Map.find id env.impls in - let expl_impls = List.map - (fun id -> CAst.make ?loc @@ CRef (qualid_of_ident ?loc id,None), Some (make ?loc @@ ExplByName id)) expl_impls in + let ty,impls,argsc = Id.Map.find id env.impls in let tys = string_of_ty ty in Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys; - gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls + gvar (loc,id) us, make_implicits_list impls, argsc with Not_found -> (* Is [id] bound in current term or is an ltac var bound to constr *) if Id.Set.mem id env.ids || Id.Set.mem id ltacvars.ltac_vars then - gvar (loc,id) us, [], [], [] + gvar (loc,id) us, [], [] else if Id.equal id ldots_var (* Is [id] the special variable for recursive notations? *) then if Id.Map.is_empty ntnvars then error_ldots_var ?loc - else gvar (loc,id) us, [], [], [] + else gvar (loc,id) us, [], [] else if Id.Set.mem id ltacvars.ltac_bound then (* Is [id] bound to a free name in ltac (this is an ltac error message) *) user_err ?loc ~hdr:"intern_var" @@ -1066,17 +1033,17 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = let scopes = find_arguments_scope ref in Dumpglob.dump_secvar ?loc id; (* this raises Not_found when not a section variable *) (* Someday we should stop relying on Dumglob raising exceptions *) - DAst.make ?loc @@ GRef (ref, us), impls, scopes, [] + DAst.make ?loc @@ GRef (ref, us), impls, scopes with e when CErrors.noncritical e -> (* [id] a goal variable *) - gvar (loc,id) us, [], [], [] + gvar (loc,id) us, [], [] let find_appl_head_data c = match DAst.get c with | GRef (ref,_) -> let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in - c, impls, scopes, [] + c, impls, scopes | GApp (r, l) -> begin match DAst.get r with | GRef (ref,_) -> @@ -1084,10 +1051,10 @@ let find_appl_head_data c = let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in c, (if n = 0 then [] else List.map (drop_first_implicits n) impls), - List.skipn_at_least n scopes,[] - | _ -> c,[],[],[] + List.skipn_at_least n scopes + | _ -> c,[],[] end - | _ -> c,[],[],[] + | _ -> c,[],[] let error_not_enough_arguments ?loc = user_err ?loc (str "Abbreviation is not applied enough.") @@ -1195,13 +1162,12 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us try let r, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in check_applied_projection isproj realref qid; - let x, imp, scopes, l = find_appl_head_data r in - (x,imp,scopes,l), args2 + find_appl_head_data r, args2 with Not_found -> (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then (* check_applied_projection ?? *) - (gvar (loc,qualid_basename qid) us, [], [], []), args + (gvar (loc,qualid_basename qid) us, [], []), args else Nametab.error_global_not_found qid else let r,realref,args2 = @@ -1209,11 +1175,10 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us with Not_found -> Nametab.error_global_not_found qid in check_applied_projection isproj realref qid; - let x, imp, scopes, l = find_appl_head_data r in - (x,imp,scopes,l), args2 + find_appl_head_data r, args2 let interp_reference vars r = - let (r,_,_,_),_ = + let (r,_,_),_ = intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None) {ids = Id.Set.empty; unb = false ; tmp_scope = None; scopes = []; impls = empty_internalization_env; @@ -1585,12 +1550,6 @@ let alias_of als = match als.alias_ids with *) -let is_zero s = - let rec aux i = - Int.equal (String.length s) i || ((s.[i] == '0' || s.[i] == '_') && aux (i+1)) - in aux 0 -let is_zero n = is_zero n.NumTok.int && is_zero n.NumTok.frac - let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 let product_of_cases_patterns aliases idspl = @@ -1614,11 +1573,11 @@ let rec subst_pat_iterator y t = DAst.(map (function | RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl))) let is_non_zero c = match c with -| { CAst.v = CPrim (Numeral (SPlus, p)) } -> not (is_zero p) +| { CAst.v = CPrim (Numeral p) } -> not (NumTok.Signed.is_zero p) | _ -> false let is_non_zero_pat c = match c with -| { CAst.v = CPatPrim (Numeral (SPlus, p)) } -> not (is_zero p) +| { CAst.v = CPatPrim (Numeral p) } -> not (NumTok.Signed.is_zero p) | _ -> false let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref @@ -1887,18 +1846,6 @@ let intern_ind_pattern genv ntnvars scopes pat = (**********************************************************************) (* Utilities for application *) -let merge_impargs l args = - let test x = function - | (_, Some {v=y}) -> explicitation_eq x y - | _ -> false - in - List.fold_right (fun a l -> - match a with - | (_, Some {v=ExplByName id as x}) when - List.exists (test x) args -> l - | _ -> a::l) - l args - let get_implicit_name n imps = Some (Impargs.name_of_implicit (List.nth imps (n-1))) @@ -1959,11 +1906,11 @@ let extract_explicit_arg imps args = let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let rec intern env = CAst.with_loc_val (fun ?loc -> function | CRef (ref,us) -> - let (c,imp,subscopes,l),_ = + let (c,imp,subscopes),_ = intern_applied_reference ~isproj:None intern env (Environ.named_context_val globalenv) lvar us [] ref in - apply_impargs c env imp subscopes l loc + apply_impargs c env imp subscopes [] loc | CFix ({ CAst.loc = locid; v = iddef}, dl) -> let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in @@ -2058,8 +2005,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a | CNotation (_,ntn,args) -> let c = intern_notation intern env ntnvars loc ntn args in - let x, impl, scopes, l = find_appl_head_data c in - apply_impargs x env impl scopes l loc + let x, impl, scopes = find_appl_head_data c in + apply_impargs x env impl scopes [] loc | CGeneralization (b,a,c) -> intern_generalization intern env ntnvars loc b a c | CPrim p -> @@ -2068,7 +2015,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = intern {env with tmp_scope = None; scopes = find_delimiters_scope ?loc key :: env.scopes} e | CAppExpl ((isproj,ref,us), args) -> - let (f,_,args_scopes,_),args = + let (f,_,args_scopes),args = let args = List.map (fun a -> (a,None)) args in intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv) lvar us args ref @@ -2079,25 +2026,24 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = smart_gapp f loc (intern_args env args_scopes (List.map fst args)) | CApp ((isproj,f), args) -> - let isproj,f,args = match f.CAst.v with - (* Compact notations like "t.(f args') args" *) - | CApp ((Some _ as isproj',f), args') when not (Option.has_some isproj) -> - isproj',f,args'@args - (* Don't compact "(f args') args" to resolve implicits separately *) - | _ -> isproj,f,args in - let (c,impargs,args_scopes,l),args = - match f.CAst.v with - | CRef (ref,us) -> - intern_applied_reference ~isproj intern env - (Environ.named_context_val globalenv) lvar us args ref - | CNotation (_,ntn,ntnargs) -> - assert (Option.is_empty isproj); - let c = intern_notation intern env ntnvars loc ntn ntnargs in - let x, impl, scopes, l = find_appl_head_data c in - (x,impl,scopes,l), args - | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in - apply_impargs c env impargs args_scopes - (merge_impargs l args) loc + let isproj,f,args = match f.CAst.v with + (* Compact notations like "t.(f args') args" *) + | CApp ((Some _ as isproj',f), args') when not (Option.has_some isproj) -> + isproj',f,args'@args + (* Don't compact "(f args') args" to resolve implicits separately *) + | _ -> isproj,f,args in + let (c,impargs,args_scopes),args = + match f.CAst.v with + | CRef (ref,us) -> + intern_applied_reference ~isproj intern env + (Environ.named_context_val globalenv) lvar us args ref + | CNotation (_,ntn,ntnargs) -> + assert (Option.is_empty isproj); + let c = intern_notation intern env ntnvars loc ntn ntnargs in + find_appl_head_data c, args + | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[]), args in + apply_impargs c env impargs args_scopes + args loc | CRecord fs -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in @@ -2138,9 +2084,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = List.rev_append match_td matchs) tms ([],Id.Set.empty,Id.Map.empty,[]) in let env' = Id.Set.fold - (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var)) + (fun var bli -> push_name_env ntnvars (Variable,[],[]) bli (CAst.make @@ Name var)) (Id.Set.union ex_ids as_in_vars) - (reset_hidden_inductive_implicit_test (restart_lambda_binders env)) in + (restart_lambda_binders env) + in (* PatVars before a real pattern do not need to be matched *) let stripped_match_from_in = let rec aux = function @@ -2175,17 +2122,17 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* "in" is None so no match to add *) let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in let p' = Option.map (fun u -> - let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env') + let env'' = push_name_env ntnvars (Variable,[],[]) env' (CAst.make na') in intern_type (slide_binders env'') u) po in DAst.make ?loc @@ GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b', - intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) + intern (List.fold_left (push_name_env ntnvars (Variable,[],[])) env nal) c) | CIf (c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *) let p' = Option.map (fun p -> - let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env) + let env'' = push_name_env ntnvars (Variable,[],[]) env (CAst.make na') in intern_type (slide_binders env'') p) po in DAst.make ?loc @@ @@ -2483,22 +2430,23 @@ let interp_open_constr ?(expected_type=WithoutTypeConstraint) env sigma c = (* Not all evars expected to be resolved and computation of implicit args *) -let interp_constr_evars_gen_impls ?(program_mode=false) env sigma +let interp_constr_evars_gen_impls ?(flags=Pretyping.all_no_fail_flags) env sigma ?(impls=empty_internalization_env) expected_type c = let c = intern_gen expected_type ~impls env sigma c in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in - let flags = { Pretyping.all_no_fail_flags with program_mode } in let sigma, c = understand_tcc ~flags env sigma ~expected_type c in sigma, (c, imps) -let interp_constr_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c = - interp_constr_evars_gen_impls ?program_mode env sigma ~impls WithoutTypeConstraint c +let interp_constr_evars_impls ?(program_mode=false) env sigma ?(impls=empty_internalization_env) c = + let flags = { Pretyping.all_no_fail_flags with program_mode } in + interp_constr_evars_gen_impls ~flags env sigma ~impls WithoutTypeConstraint c -let interp_casted_constr_evars_impls ?program_mode env evdref ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen_impls ?program_mode env evdref ~impls (OfType typ) c +let interp_casted_constr_evars_impls ?(program_mode=false) env evdref ?(impls=empty_internalization_env) c typ = + let flags = { Pretyping.all_no_fail_flags with program_mode } in + interp_constr_evars_gen_impls ~flags env evdref ~impls (OfType typ) c -let interp_type_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c = - interp_constr_evars_gen_impls ?program_mode env sigma ~impls IsType c +let interp_type_evars_impls ?(flags=Pretyping.all_no_fail_flags) env sigma ?(impls=empty_internalization_env) c = + interp_constr_evars_gen_impls ~flags env sigma ~impls IsType c (* Not all evars expected to be resolved, with side-effect on evars *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 670563f02f..9f06f16258 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -38,7 +38,7 @@ open Pretyping of [env] *) type var_internalization_type = - | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *) + | Inductive | Recursive | Method | Variable @@ -48,10 +48,6 @@ type var_internalization_data = (* type of the "free" variable, for coqdoc, e.g. while typing the constructor of JMeq, "JMeq" behaves as a variable of type Inductive *) - Id.t list * - (* impargs to automatically add to the variable, e.g. for "JMeq A a B b" - in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) - Impargs.implicit_status list * (* signature of impargs of the variable *) Notation_term.scope_name option list (* subscopes of the args of the variable *) @@ -132,7 +128,7 @@ val interp_casted_constr_evars_impls : ?program_mode:bool -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> types -> evar_map * (constr * Impargs.manual_implicits) -val interp_type_evars_impls : ?program_mode:bool -> env -> evar_map -> +val interp_type_evars_impls : ?flags:inference_flags -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> evar_map * (types * Impargs.manual_implicits) diff --git a/interp/decls.ml b/interp/decls.ml index d9d33b5e0b..a9f40d7bd6 100644 --- a/interp/decls.ml +++ b/interp/decls.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/decls.mli b/interp/decls.mli index 56866aeb43..57ea678a13 100644 --- a/interp/decls.mli +++ b/interp/decls.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/deprecation.ml b/interp/deprecation.ml index 3b02ba4664..a2408f8091 100644 --- a/interp/deprecation.ml +++ b/interp/deprecation.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/deprecation.mli b/interp/deprecation.mli index f8083c2a5b..60f8eecbbd 100644 --- a/interp/deprecation.mli +++ b/interp/deprecation.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 25a87d5f94..e659a5ac5c 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 2b6a116a01..5409b20472 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/genintern.ml b/interp/genintern.ml index e74f8d5f10..600c82eb2b 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/genintern.mli b/interp/genintern.mli index 5619a7b648..291e829e41 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/impargs.ml b/interp/impargs.ml index 1365b97d82..a1b029c381 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/impargs.mli b/interp/impargs.mli index 65e7fd8aaf..97841b37f2 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index e6f12f7eb2..3d29da025e 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 4f9c47ec36..57db08607a 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/modintern.ml b/interp/modintern.ml index ddf5b2d7b1..ae152e1c1c 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/modintern.mli b/interp/modintern.mli index 72695a680e..443ba03eab 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/notation.ml b/interp/notation.ml index b869cb2a36..6291a88bb0 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -21,6 +21,7 @@ open Notation_term open Glob_term open Glob_ops open Context.Named.Declaration +open NumTok (*i*) @@ -335,7 +336,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) (* Interpreting numbers (not in summary because functional objects) *) type required_module = full_path * string list -type rawnum = Constrexpr.sign * Constrexpr.raw_numeral +type rawnum = NumTok.Signed.t type prim_token_uid = string @@ -358,17 +359,13 @@ module InnerPrimToken = struct | StringInterp f, StringInterp f' -> f == f' | _ -> false - let ofNumeral s n = - let n = String.(concat "" (split_on_char '_' n)) in - match s with - | SPlus -> Bigint.of_string n - | SMinus -> Bigint.neg (Bigint.of_string n) - let do_interp ?loc interp primtok = match primtok, interp with - | Numeral (s,n), RawNumInterp interp -> interp ?loc (s,n) - | Numeral (s,{ NumTok.int = n; frac = ""; exp = "" }), - BigNumInterp interp -> interp ?loc (ofNumeral s n) + | Numeral n, RawNumInterp interp -> interp ?loc n + | Numeral n, BigNumInterp interp -> + (match NumTok.Signed.to_bigint n with + | Some n -> interp ?loc n + | None -> raise Not_found) | String s, StringInterp interp -> interp ?loc s | (Numeral _ | String _), (RawNumInterp _ | BigNumInterp _ | StringInterp _) -> raise Not_found @@ -385,10 +382,7 @@ module InnerPrimToken = struct | _ -> false let mkNumeral n = - if Bigint.is_pos_or_zero n then - Numeral (SPlus,NumTok.int (Bigint.to_string n)) - else - Numeral (SMinus,NumTok.int (Bigint.to_string (Bigint.neg n))) + Numeral (NumTok.Signed.of_bigint n) let mkString = function | None -> None @@ -425,8 +419,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t type numnot_option = | Nop - | Warning of string - | Abstract of string + | Warning of NumTok.UnsignedNat.t + | Abstract of NumTok.UnsignedNat.t type int_ty = { uint : Names.inductive; @@ -567,7 +561,7 @@ let uninterp to_raw o (Glob_term.AnyGlobConstr n) = Some (to_raw (fst o.of_kind, c)) with | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *) - | NotAValidPrimToken -> None (* all other functions except big2raw *) + | NotAValidPrimToken -> None (* all other functions except NumTok.Signed.of_bigint *) end @@ -600,26 +594,6 @@ let warn_abstract_large_num = pr_qualid ty ++ strbrk " are interpreted as applications of " ++ Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".") -(** Comparing two raw numbers (base 10, big-endian, non-negative). - A bit nasty, but not critical: only used to decide when a - number is considered as large (see warnings above). *) - -exception Comp of int - -let rec rawnum_compare s s' = - let l = String.length s and l' = String.length s' in - if l < l' then - rawnum_compare s' s - else - let d = l-l' in - try - for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done; - for i = d to l-1 do - let c = pervasives_compare s.[i] s'.[i-d] in - if c != 0 then raise (Comp c) - done; - 0 - with Comp c -> c - (***********************************************************************) (** ** Conversion between Coq [Decimal.int] and internal raw string *) @@ -634,32 +608,31 @@ let char_of_digit n = assert (2<=n && n<=11); Char.chr (n-2 + Char.code '0') -let coquint_of_rawnum uint str = +let coquint_of_rawnum uint n = let nil = mkConstruct (uint,1) in + match n with None -> nil | Some n -> + let str = NumTok.UnsignedNat.to_string n in let rec do_chars s i acc = if i < 0 then acc - else if s.[i] == '_' then do_chars s (i-1) acc else + else let dg = mkConstruct (uint, digit_of_char s.[i]) in do_chars s (i-1) (mkApp(dg,[|acc|])) in do_chars str (String.length str - 1) nil -let coqint_of_rawnum inds sign str = - let uint = coquint_of_rawnum inds.uint str in +let coqint_of_rawnum inds (sign,n) = + let uint = coquint_of_rawnum inds.uint (Some n) in let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in mkApp (mkConstruct (inds.int, pos_neg), [|uint|]) -let coqdecimal_of_rawnum inds sign n = - let i, f, e = NumTok.(n.int, n.frac, n.exp) in - let i = coqint_of_rawnum inds.int sign i in +let coqdecimal_of_rawnum inds n = + let i, f, e = NumTok.Signed.to_decimal_and_exponent n in + let i = coqint_of_rawnum inds.int i in let f = coquint_of_rawnum inds.int.uint f in - if e = "" then mkApp (mkConstruct (inds.decimal, 1), [|i; f|]) (* Decimal *) - else - let sign, e = match e.[1] with - | '-' -> SMinus, String.sub e 2 (String.length e - 2) - | '+' -> SPlus, String.sub e 2 (String.length e - 2) - | _ -> SPlus, String.sub e 1 (String.length e - 1) in - let e = coqint_of_rawnum inds.int sign e in + match e with + | None -> mkApp (mkConstruct (inds.decimal, 1), [|i; f|]) (* Decimal *) + | Some e -> + let e = coqint_of_rawnum inds.int e in mkApp (mkConstruct (inds.decimal, 2), [|i; f; e|]) (* DecimalExp *) let rawnum_of_coquint c = @@ -680,26 +653,23 @@ let rawnum_of_coquint c = (* To avoid ambiguities between Nil and (D0 Nil), we choose to not display Nil alone as "0" *) raise NotAValidPrimToken - else NumTok.int (Buffer.contents buf) + else NumTok.UnsignedNat.of_string (Buffer.contents buf) let rawnum_of_coqint c = match Constr.kind c with | App (c,[|c'|]) -> (match Constr.kind c with - | Construct ((_,1), _) (* Pos *) -> (SPlus, rawnum_of_coquint c') - | Construct ((_,2), _) (* Neg *) -> (SMinus, rawnum_of_coquint c') + | Construct ((_,1), _) (* Pos *) -> (SPlus,rawnum_of_coquint c') + | Construct ((_,2), _) (* Neg *) -> (SMinus,rawnum_of_coquint c') | _ -> raise NotAValidPrimToken) | _ -> raise NotAValidPrimToken let rawnum_of_decimal c = let of_ife i f e = - let sign, n = rawnum_of_coqint i in - let f = - try (rawnum_of_coquint f).NumTok.int with NotAValidPrimToken -> "" in - let e = match e with None -> "" | Some e -> match rawnum_of_coqint e with - | SPlus, e -> "e+" ^ e.NumTok.int - | SMinus, e -> "e-" ^ e.NumTok.int in - sign,{ n with NumTok.frac = f; exp = e } in + let n = rawnum_of_coqint i in + let f = try Some (rawnum_of_coquint f) with NotAValidPrimToken -> None in + let e = match e with None -> None | Some e -> Some (rawnum_of_coqint e) in + NumTok.Signed.of_decimal_and_exponent n f e in match Constr.kind c with | App (_,[|i; f|]) -> of_ife i f None | App (_,[|i; f; e|]) -> of_ife i f (Some e) @@ -789,43 +759,31 @@ let bigint_of_int63 c = | Int i -> Bigint.of_string (Uint63.to_string i) | _ -> raise NotAValidPrimToken -let big2raw n = - if Bigint.is_pos_or_zero n then - (SPlus, NumTok.int (Bigint.to_string n)) - else - (SMinus, NumTok.int (Bigint.to_string (Bigint.neg n))) - -let raw2big s n = match s with - | SPlus -> Bigint.of_string n - | SMinus -> Bigint.neg (Bigint.of_string n) - let interp o ?loc n = begin match o.warning, n with - | Warning threshold, (SPlus, { NumTok.int = n; frac = ""; exp = "" }) - when rawnum_compare n threshold >= 0 -> + | Warning threshold, n when NumTok.Signed.is_bigger_int_than n threshold -> warn_large_num o.ty_name | _ -> () end; - let c = match fst o.to_kind, n with - | Int int_ty, (s, { NumTok.int = n; frac = ""; exp = "" }) -> - coqint_of_rawnum int_ty s n - | UInt uint_ty, (SPlus, { NumTok.int = n; frac = ""; exp = "" }) -> - coquint_of_rawnum uint_ty n - | Z z_pos_ty, (s, { NumTok.int = n; frac = ""; exp = "" }) -> - z_of_bigint z_pos_ty (raw2big s n) - | Int63, (s, { NumTok.int = n; frac = ""; exp = "" }) -> - interp_int63 ?loc (raw2big s n) + let c = match fst o.to_kind, NumTok.Signed.to_int n with + | Int int_ty, Some n -> + coqint_of_rawnum int_ty n + | UInt uint_ty, Some (SPlus, n) -> + coquint_of_rawnum uint_ty (Some n) + | Z z_pos_ty, Some n -> + z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n) + | Int63, Some n -> + interp_int63 ?loc (NumTok.SignedNat.to_bigint n) | (Int _ | UInt _ | Z _ | Int63), _ -> no_such_prim_token "number" ?loc o.ty_name - | Decimal decimal_ty, (s,n) -> coqdecimal_of_rawnum decimal_ty s n + | Decimal decimal_ty, _ -> coqdecimal_of_rawnum decimal_ty n in let env = Global.env () in let sigma = Evd.from_env env in let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in let to_ty = EConstr.Unsafe.to_constr to_ty in match o.warning, snd o.to_kind with - | Abstract threshold, Direct - when rawnum_compare (snd n).NumTok.int threshold >= 0 -> + | Abstract threshold, Direct when NumTok.Signed.is_bigger_int_than n threshold -> warn_abstract_large_num (o.ty_name,o.to_ty); glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|])) | _ -> @@ -837,10 +795,10 @@ let interp o ?loc n = let uninterp o n = PrimTokenNotation.uninterp begin function - | (Int _, c) -> rawnum_of_coqint c - | (UInt _, c) -> (SPlus, rawnum_of_coquint c) - | (Z _, c) -> big2raw (bigint_of_z c) - | (Int63, c) -> big2raw (bigint_of_int63 c) + | (Int _, c) -> NumTok.Signed.of_int (rawnum_of_coqint c) + | (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c) + | (Z _, c) -> NumTok.Signed.of_bigint (bigint_of_z c) + | (Int63, c) -> NumTok.Signed.of_bigint (bigint_of_int63 c) | (Decimal _, c) -> rawnum_of_decimal c end o n end @@ -1162,8 +1120,8 @@ let find_notation ntn sc = NotationMap.find ntn (find_scope sc).notations let notation_of_prim_token = function - | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n - | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.to_string n + | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n + | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n | String _ -> raise Not_found let find_prim_token check_allowed ?loc p sc = diff --git a/interp/notation.mli b/interp/notation.mli index 26c45d5896..892eba8d11 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -81,7 +81,7 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name type notation_location = (DirPath.t * DirPath.t) * string type required_module = full_path * string list -type rawnum = Constrexpr.sign * Constrexpr.raw_numeral +type rawnum = NumTok.Signed.t (** The unique id string below will be used to refer to a particular registered interpreter/uninterpreter of numeral or string notation. @@ -116,8 +116,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t type numnot_option = | Nop - | Warning of string - | Abstract of string + | Warning of NumTok.UnsignedNat.t + | Abstract of NumTok.UnsignedNat.t type int_ty = { uint : Names.inductive; diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 8f47e9276b..54065e8b35 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 0ef51b65a2..3cc6f82ec8 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/notation_term.ml b/interp/notation_term.ml index c6ddd9ac95..4e9b8bbb17 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/numTok.ml b/interp/numTok.ml index 8f2004b889..e254e9e972 100644 --- a/interp/numTok.ml +++ b/interp/numTok.ml @@ -1,52 +1,250 @@ -type t = { - int : string; - frac : string; - exp : string -} - -let equal n1 n2 = - String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp) - -let int s = { int = s; frac = ""; exp = "" } - -let to_string n = n.int ^ (if n.frac = "" then "" else "." ^ n.frac) ^ n.exp - -let parse = - let buff = ref (Bytes.create 80) in - let store len x = - let open Bytes in - if len >= length !buff then - buff := cat !buff (create (length !buff)); - set !buff len x; - succ len in - let get_buff len = Bytes.sub_string !buff 0 len in - (* reads [0-9_]* *) - let rec number len s = match Stream.peek s with - | Some (('0'..'9' | '_') as c) -> Stream.junk s; number (store len c) s - | _ -> len in - fun s -> - let i = get_buff (number 0 s) in - let f = - match Stream.npeek 2 s with - | '.' :: (('0'..'9' | '_') as c) :: _ -> - Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s) - | _ -> "" in - let e = - match (Stream.npeek 2 s) with - | (('e'|'E') as e) :: ('0'..'9' as c) :: _ -> - Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s) - | (('e'|'E') as e) :: (('+'|'-') as sign) :: _ -> - begin match Stream.npeek 3 s with - | _ :: _ :: ('0'..'9' as c) :: _ -> - Stream.junk s; Stream.junk s; Stream.junk s; - get_buff (number (store (store (store 0 e) sign) c) s) - | _ -> "" - end - | _ -> "" in - { int = i; frac = f; exp = e } - -let of_string s = - if s = "" || s.[0] < '0' || s.[0] > '9' then None else - let strm = Stream.of_string (s ^ " ") in - let n = parse strm in - if Stream.count strm >= String.length s then Some n else None +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \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) *) +(************************************************************************) + +(** We keep the string to preserve the user representation, + e.g. "e"/"E" or the presence of leading 0s, or the presence of a + + in the exponent *) + +module UnsignedNat = +struct + type t = string + let of_string s = + assert (String.length s > 0); + assert (s.[0] >= '0' && s.[0] <= '9'); + s + let to_string s = + String.(concat "" (split_on_char '_' s)) + + let sprint s = s + let print s = Pp.str (sprint s) + + (** Comparing two raw numbers (base 10, big-endian, non-negative). + A bit nasty, but not critical: used e.g. to decide when a number + is considered as large (see threshold warnings in notation.ml). *) + + exception Comp of int + + let rec compare s s' = + let l = String.length s and l' = String.length s' in + if l < l' then - compare s' s + else + let d = l-l' in + try + for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done; + for i = d to l-1 do + let c = Util.pervasives_compare s.[i] s'.[i-d] in + if c != 0 then raise (Comp c) + done; + 0 + with Comp c -> c + + let is_zero s = + compare s "0" = 0 +end + +type sign = SPlus | SMinus + +module SignedNat = +struct + type t = sign * UnsignedNat.t + let of_string s = + assert (String.length s > 0); + let sign,n = + match s.[0] with + | '-' -> (SMinus,String.sub s 1 (String.length s - 1)) + | '+' -> (SPlus,String.sub s 1 (String.length s - 1)) + | _ -> (SPlus,s) in + (sign,UnsignedNat.of_string n) + let to_string (sign,n) = + (match sign with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n + let to_bigint n = Bigint.of_string (to_string n) + let of_bigint n = + let sign, n = if Bigint.is_strictly_neg n then (SMinus, Bigint.neg n) else (SPlus, n) in + (sign, Bigint.to_string n) +end + +module Unsigned = +struct + + type t = { + int : string; (** \[0-9\]\[0-9_\]* *) + frac : string; (** empty or \[0-9_\]+ *) + exp : string (** empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *) + } + + let equal n1 n2 = + String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp) + + let parse = + let buff = ref (Bytes.create 80) in + let store len x = + let open Bytes in + if len >= length !buff then + buff := cat !buff (create (length !buff)); + set !buff len x; + succ len in + let get_buff len = Bytes.sub_string !buff 0 len in + (* reads [0-9_]* *) + let rec number len s = match Stream.peek s with + | Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s + | Some ('_' as c) when len > 0 -> Stream.junk s; number (store len c) s + | _ -> len in + fun s -> + let i = get_buff (number 0 s) in + assert (i <> ""); + let f = + match Stream.npeek 2 s with + | '.' :: (('0'..'9' | '_') as c) :: _ -> + Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s) + | _ -> "" in + let e = + match (Stream.npeek 2 s) with + | (('e'|'E') as e) :: ('0'..'9' as c) :: _ -> + Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s) + | (('e'|'E') as e) :: (('+'|'-') as sign) :: _ -> + begin match Stream.npeek 3 s with + | _ :: _ :: ('0'..'9' as c) :: _ -> + Stream.junk s; Stream.junk s; Stream.junk s; + get_buff (number (store (store (store 0 e) sign) c) s) + | _ -> "" + end + | _ -> "" in + { int = i; frac = f; exp = e } + + let sprint n = + n.int ^ (if n.frac = "" then "" else "." ^ n.frac) ^ n.exp + + let print n = + Pp.str (sprint n) + + let parse_string s = + if s = "" || s.[0] < '0' || s.[0] > '9' then None else + let strm = Stream.of_string (s ^ " ") in + let n = parse strm in + if Stream.count strm >= String.length s then Some n else None + + let of_string s = + match parse_string s with + | None -> assert false + | Some s -> s + + let to_string = + sprint (* We could remove the '_' but not necessary for float_of_string *) + + let to_nat = function + | { int = i; frac = ""; exp = "" } -> Some i + | _ -> None + + let is_nat = function + | { int = _; frac = ""; exp = "" } -> true + | _ -> false + +end + +open Unsigned + +module Signed = +struct + + type t = sign * Unsigned.t + + let equal (s1,n1) (s2,n2) = + s1 = s2 && equal n1 n2 + + let is_zero = function + | (SPlus,{int;frac;exp}) -> UnsignedNat.is_zero int && UnsignedNat.is_zero frac + | _ -> false + + let of_decimal_and_exponent (sign,int) f e = + let exp = match e with Some e -> "e" ^ SignedNat.to_string e | None -> "" in + let frac = match f with Some f -> UnsignedNat.to_string f | None -> "" in + sign, { int; frac; exp } + + let to_decimal_and_exponent (sign, { int; frac; exp }) = + let e = + if exp = "" then None else + Some (match exp.[1] with + | '-' -> SMinus, String.sub exp 2 (String.length exp - 2) + | '+' -> SPlus, String.sub exp 2 (String.length exp - 2) + | _ -> SPlus, String.sub exp 1 (String.length exp - 1)) in + let f = if frac = "" then None else Some frac in + (sign, int), f, e + + let of_nat i = + (SPlus,{ int = i; frac = ""; exp = "" }) + + let of_int (s,i) = + (s,{ int = i; frac = ""; exp = "" }) + + let of_int_string s = of_int (SignedNat.of_string s) + + let to_int = function + | (s, { int = i; frac = ""; exp = "" }) -> Some (s,i) + | _ -> None + + let is_int n = match to_int n with None -> false | Some _ -> true + + let sprint (s,i) = + (match s with SPlus -> "" | SMinus -> "-") ^ Unsigned.sprint i + + let print i = + Pp.str (sprint i) + + let parse_string s = + if s = "" || s = "-" || s = "+" || + (s.[0] < '0' || s.[0] > '9') && ((s.[0] <> '-' && s.[0] <> '+') || s.[1] < '0' || s.[1] > '9') then None else + let strm = Stream.of_string (s ^ " ") in + let sign = match s.[0] with + | '-' -> (Stream.junk strm; SMinus) + | '+' -> (Stream.junk strm; SPlus) + | _ -> SPlus in + let n = parse strm in + if Stream.count strm >= String.length s then Some (sign,n) else None + + let of_string s = + assert (s <> ""); + let sign,u = match s.[0] with + | '-' -> (SMinus, String.sub s 1 (String.length s - 1)) + | '+' -> (SPlus, String.sub s 1 (String.length s - 1)) + | _ -> (SPlus, s) in + (sign, Unsigned.of_string u) + + let to_string (sign,u) = + (match sign with SPlus -> "" | SMinus -> "-") ^ Unsigned.to_string u + + let to_bigint = function + | (sign, { int = n; frac = ""; exp = "" }) -> + Some (SignedNat.to_bigint (sign,UnsignedNat.to_string n)) + | _ -> None + + let of_bigint n = + let sign, int = SignedNat.of_bigint n in + (sign, { int; frac = ""; exp = "" }) + + let to_bigint_and_exponent (s, { int; frac; exp }) = + let s = match s with SPlus -> "" | SMinus -> "-" in + let int = UnsignedNat.to_string int in + let frac = UnsignedNat.to_string frac in + let i = Bigint.of_string (s ^ int ^ frac) in + let e = + let e = if exp = "" then Bigint.zero else match exp.[1] with + | '+' -> Bigint.of_string (UnsignedNat.to_string (String.sub exp 2 (String.length exp - 2))) + | '-' -> Bigint.(neg (of_string (UnsignedNat.to_string (String.sub exp 2 (String.length exp - 2))))) + | _ -> Bigint.of_string (UnsignedNat.to_string (String.sub exp 1 (String.length exp - 1))) in + Bigint.(sub e (of_int (String.length (String.concat "" (String.split_on_char '_' frac))))) in + (i,e) + + let of_bigint_and_exponent i e = + of_decimal_and_exponent (SignedNat.of_bigint i) None (Some (SignedNat.of_bigint e)) + + let is_bigger_int_than (s, { int; frac; exp }) i = + frac = "" && exp = "" && UnsignedNat.compare int i >= 0 + +end diff --git a/interp/numTok.mli b/interp/numTok.mli index 0b6a877cbd..ea289df237 100644 --- a/interp/numTok.mli +++ b/interp/numTok.mli @@ -1,18 +1,132 @@ -type t = { - int : string; (** \[0-9\]\[0-9_\]* *) - frac : string; (** empty or \[0-9_\]+ *) - exp : string (** empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *) -} +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \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) *) +(************************************************************************) -val equal : t -> t -> bool +(** Numerals in different forms: signed or unsigned, possibly with + fractional part and exponent. -(** [int s] amounts to [\{ int = s; frac = ""; exp = "" \}] *) -val int : string -> t + Numerals are represented using raw strings of decimal + literals and a separate sign flag. -val to_string : t -> string + Note that this representation is not unique, due to possible + multiple leading or trailing zeros, and -0 = +0, for instances. + The reason to keep the numeral exactly as it was parsed is that + specific notations can be declared for specific numerals + (e.g. [Notation "0" := False], or [Notation "00" := (nil,nil)], or + [Notation "2e1" := ...]). Those notations override the generic + interpretation as numeral. So, one has to record the form of the + numeral which exactly matches the notation. *) -val of_string : string -> t option +type sign = SPlus | SMinus -(** Precondition: the first char on the stream is a digit (\[0-9\]). - Precondition: at least two extra chars after the numeral to parse. *) -val parse : char Stream.t -> t +(** {6 String representation of a natural number } *) + +module UnsignedNat : +sig + type t + val of_string : string -> t + (** Convert from a non-empty sequence of digits (which may contain "_") *) + + val to_string : t -> string + (** Convert to a non-empty sequence of digit that does not contain "_" *) + + val sprint : t -> string + val print : t -> Pp.t + (** [sprint] and [print] returns the numeral as it was parsed, for printing *) + + val compare : t -> t -> int +end + +(** {6 String representation of a signed natural number } *) + +module SignedNat : +sig + type t = sign * UnsignedNat.t + val of_string : string -> t + (** Convert from a non-empty sequence of digits which may contain "_" *) + + val to_string : t -> string + (** Convert to a non-empty sequence of digit that does not contain "_" *) + + val to_bigint : t -> Bigint.bigint + val of_bigint : Bigint.bigint -> t +end + +(** {6 Unsigned decimal numerals } *) + +module Unsigned : +sig + type t + val equal : t -> t -> bool + val is_nat : t -> bool + val to_nat : t -> string option + + val sprint : t -> string + val print : t -> Pp.t + (** [sprint] and [print] returns the numeral as it was parsed, for printing *) + + val parse : char Stream.t -> t + (** Parse a positive Coq numeral. + Precondition: the first char on the stream is already known to be a digit (\[0-9\]). + Precondition: at least two extra chars after the numeral to parse. + + The recognized syntax is: + - integer part: \[0-9\]\[0-9_\]* + - decimal part: empty or .\[0-9_\]+ + - exponent part: empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *) + + val parse_string : string -> t option + (** Parse the string as a positive Coq numeral, if possible *) + +end + +(** {6 Signed decimal numerals } *) + +module Signed : +sig + type t = sign * Unsigned.t + val equal : t -> t -> bool + val is_zero : t -> bool + val of_nat : UnsignedNat.t -> t + val of_int : SignedNat.t -> t + val to_int : t -> SignedNat.t option + val is_int : t -> bool + + val sprint : t -> string + val print : t -> Pp.t + (** [sprint] and [print] returns the numeral as it was parsed, for printing *) + + val parse_string : string -> t option + (** Parse the string as a signed Coq numeral, if possible *) + + val of_int_string : string -> t + (** Convert from a string in the syntax of OCaml's int/int64 *) + + val of_string : string -> t + (** Convert from a string in the syntax of OCaml's string_of_float *) + + val to_string : t -> string + (** Returns a string in the syntax of OCaml's float_of_string *) + + val of_bigint : Bigint.bigint -> t + val to_bigint : t -> Bigint.bigint option + (** Convert from and to bigint when the denotation of a bigint *) + + val of_decimal_and_exponent : SignedNat.t -> UnsignedNat.t option -> SignedNat.t option -> t + val to_decimal_and_exponent : t -> SignedNat.t * UnsignedNat.t option * SignedNat.t option + (** n, p and q such that the number is n.p*10^q *) + + val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint + val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint -> t + (** n and p such that the number is n*10^p *) + + val is_bigger_int_than : t -> UnsignedNat.t -> bool + (** Test if an integer whose absolute value is bounded *) + +end diff --git a/interp/reserve.ml b/interp/reserve.ml index 4a731e57a3..4418a32645 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/reserve.mli b/interp/reserve.mli index e180fc8071..f40573715a 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 5d36ceca38..98fa71e15d 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index d2770a2e73..9b24a62086 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 555eb34aed..492671fff0 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/stdarg.mli b/interp/stdarg.mli index dffbca0054..35de3693cb 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 9dded8656c..767c69e3b6 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 0065b45b14..8b323462a1 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |