diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 61 |
1 files changed, 29 insertions, 32 deletions
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) |