Quelle number_string.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq 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)         *)
(************************************************************************)

open Pp
open Util
open Names
open Libnames
open Glob_term
open Notation

module CSet = CSet.Make (Constr)
module CMap = CMap.Make (Constr)

let mkRef env sigma g =
  let sigma, c = Evd.fresh_global env sigma g in
  sigma, EConstr.Unsafe.to_constr c

let gref q = DAst.make (GRef (q,None))

(** * Number notation *)

type number_string_via = qualid * (bool * qualid * qualid) list
type number_option =
  | After of numnot_option
  | Via of number_string_via

let warn_abstract_large_num_no_op =
  CWarnings.create ~name:"abstract-large-number-no-op" ~category:CWarnings.CoreCategories.numbers
    (fun f ->
      strbrk "The 'abstract after' directive has no effect when " ++
      strbrk "the parsing function (" ++
      Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++
      strbrk "option type.")

let get_constructors ind =
  let mib,oib = Global.lookup_inductive ind in
  let mc = oib.Declarations.mind_consnames in
  Array.to_list
    (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc)

let unsafe_ref_ind q =
  match q with
  | GlobRef.IndRef i -> i
  | _ -> raise Not_found

type 'kind target = {
  kind : 'kind;
  typ : glob_constr;
}

let locate_z () =
  let zn = "num.Z.type" in
  let pn = "num.pos.type" in
  match Rocqlib.lib_ref zn, Rocqlib.lib_ref pn with
  | exception Rocqlib.NotFoundRef _ -> []
  | q_z, q_pos ->
    let z_ty = { z_ty = unsafe_ref_ind q_z; pos_ty = unsafe_ref_ind q_pos; } in
    [ { kind = Z z_ty; typ = gref q_z }; ]

let locate_number () =
  let dint = "num.int.type" in
  let duint = "num.uint.type" in
  let dec = "num.decimal.type" in
  let hint = "num.hexadecimal_int.type" in
  let huint = "num.hexadecimal_uint.type" in
  let hex = "num.hexadecimal.type" in
  let int = "num.num_int.type" in
  let uint = "num.num_uint.type" in
  let num = "num.number.type" in
  match Rocqlib.lib_ref dint, Rocqlib.lib_ref duint, Rocqlib.lib_ref dec
        , Rocqlib.lib_ref hint, Rocqlib.lib_ref huint, Rocqlib.lib_ref hex
        , Rocqlib.lib_ref int, Rocqlib.lib_ref uint, Rocqlib.lib_ref num
  with
  | exception Rocqlib.NotFoundRef _ -> []
  | q_dint, q_duint, q_dec, q_hint, q_huint, q_hex, q_int, q_uint, q_num ->
    let int_ty = {
      dec_int = unsafe_ref_ind q_dint;
      dec_uint = unsafe_ref_ind q_duint;
      hex_int = unsafe_ref_ind q_hint;
      hex_uint = unsafe_ref_ind q_huint;
      int = unsafe_ref_ind q_int;
      uint = unsafe_ref_ind q_uint;
    } in
    let num_ty = {
      int = int_ty;
      decimal = unsafe_ref_ind q_dec;
      hexadecimal = unsafe_ref_ind q_hex;
      number = unsafe_ref_ind q_num;
    } in
    [ { kind = Int int_ty; typ = gref q_int };
      { kind = UInt int_ty; typ = gref q_uint };
      { kind = Number num_ty; typ = gref q_num };
    ]

let locate_int63 () =
  let pos_neg_int63n = "num.int63.pos_neg_int63" in
  match Rocqlib.lib_ref pos_neg_int63n with
  | exception Rocqlib.NotFoundRef _ -> []
  | pos_neg_int63 ->
    [ { kind = Int63 {pos_neg_int63_ty = unsafe_ref_ind pos_neg_int63}; typ = gref pos_neg_int63 }; ]

let locate_float () =
  let floatn = "num.float.type" in
  match Rocqlib.lib_ref floatn with
  | exception Rocqlib.NotFoundRef _ -> []
  | q_float ->
    [ { kind = Float64; typ = gref q_float }; ]

let has_type env sigma f ty =
  let c = DAst.make @@ GCast (f, Some Constr.DEFAULTcast, ty) in
  let flags = Pretyping.{ all_and_fail_flags with use_coercions = false } in
  try let _ = Pretyping.understand ~flags env sigma c in true
  with Pretype_errors.PretypeError _ -> false

let q_option () = Rocqlib.lib_ref_opt "core.option.type"

let q_result () = Rocqlib.lib_ref_opt "core.result.type"

let is_to_target env sigma f cty {kind; typ} =
  let (>>?) opt f = match opt with
    | None -> false
    | Some x -> f x
  in
  let arrow x y =
    DAst.make @@ GProd (Anonymous,None,Glob_term.Explicit, x, y)
  in
  let app x y = DAst.make @@ GApp (gref x,[y]) in
  let app2 x y z = DAst.make @@ GApp (gref x,[y;z]) in
  let ghole = DAst.make @@ GHole GInternalHole in
  if has_type env sigma f (arrow typ cty) then
    Some (kind, Direct)
  else if q_option() >>? fun q_opt -> has_type env sigma f (arrow typ (app q_opt cty)) then
    Some (kind, Option)
  else if q_result() >>? fun q_result -> has_type env sigma f (arrow typ (app2 q_result cty ghole)) then
    Some (kind, Error)
  else None

let is_from_target env sigma g cty {kind; typ} =
  let (>>?) opt f = match opt with
    | None -> false
    | Some x -> f x
  in
  let arrow x y =
    DAst.make @@ GProd (Anonymous,None,Glob_term.Explicit, x, y)
  in
  let app x y = DAst.make @@ GApp (gref x,[y]) in
  let app2 x y z = DAst.make @@ GApp (gref x,[y;z]) in
  let ghole = DAst.make @@ GHole GInternalHole in
  if has_type env sigma g (arrow cty typ) then
    Some (kind, Direct)
  else if q_option() >>? fun q_opt -> has_type env sigma g (arrow cty (app q_opt typ)) then
    Some (kind, Option)
  else if q_result() >>? fun q_result -> has_type env sigma g (arrow cty (app2 q_result typ ghole)) then
    Some (kind, Error)
  else None

let type_error_to f ty =
  let ppty = pr_qualid ty in
  CErrors.user_err
    (pr_qualid f ++ str " should go from Number.int to " ++
     ppty ++ str " or (option " ++ ppty ++ str "), or (result " ++ ppty ++ str " _)." ++
     fnl () ++ strbrk "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or PrimFloat.float or Number.number could be used (you may need to require BinNums or Number or PrimInt63 or PrimFloat first).")

let type_error_of g ty =
  CErrors.user_err
    (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
     str " to Number.int or (option Number.int), or (result Number.int _)." ++ fnl () ++
     strbrk "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or PrimFloat.float or Number.number could be used (you may need to require BinNums or Number or PrimInt63 or PrimFloat first).")

let error_params ind =
  CErrors.user_err
    (str "Wrong number of parameters for inductive" ++ spc ()
     ++ Printer.pr_global (GlobRef.IndRef ind) ++ str ".")

let remapping_error ?loc ty ty' ty'' =
  CErrors.user_err ?loc
    (Printer.pr_global ty
     ++ str " was already mapped to" ++ spc () ++ Printer.pr_global ty'
     ++ str " and cannot be remapped to" ++ spc () ++ Printer.pr_global ty''
     ++ str ".")

let error_missing c =
  CErrors.user_err
    (str "Missing mapping for constructor " ++ Printer.pr_global c ++ str ".")

let warn_via_remapping =
  CWarnings.create ~name:"via-type-remapping" ~category:CWarnings.CoreCategories.numbers
    (fun (env, sigma, ty, ty', ty'') ->
      let constr = Printer.pr_constr_env env sigma in
      constr ty ++ str " was already mapped to" ++ spc () ++ constr ty'
      ++ str ", mapping it also to" ++ spc () ++ constr ty''
      ++ str " might yield ill typed terms when using the notation.")

let warn_via_type_mismatch =
  CWarnings.create ~name:"via-type-mismatch" ~category:CWarnings.CoreCategories.numbers
    (fun (env, sigma, g, g', exp, actual) ->
      let constr = Printer.pr_constr_env env sigma in
      str "Type of" ++ spc() ++ Printer.pr_global g
      ++ str " seems incompatible with the type of" ++ spc ()
      ++ Printer.pr_global g' ++ str "." ++ spc ()
      ++ str "Expected type is: " ++ constr exp ++ spc ()
      ++ str "instead of " ++ constr actual ++ str "." ++ spc ()
      ++ str "This might yield ill typed terms when using the notation.")

let multiple_via_error () =
  CErrors.user_err (Pp.str "Multiple 'via' options.")

let multiple_after_error () =
  CErrors.user_err (Pp.str "Multiple 'warning after' or 'abstract after' options.")

let via_abstract_error () =
  CErrors.user_err (Pp.str "'via' and 'abstract' cannot be used together.")

let locate_global_sort_inductive_or_constant env sigma qid =
  let locate_sort qid =
    match Nametab.locate_extended qid with
    | Globnames.TrueGlobal _ -> raise Not_found
    | Globnames.Abbrev kn ->
    match Abbreviation.search_abbreviation kn with
    | [], Notation_term.NSort r ->
       let sigma,c = Glob_ops.fresh_glob_sort_in_quality sigma r in
       let c = EConstr.ESorts.kind sigma c in
       sigma, Constr.mkSort c
    | _ -> raise Not_found in
  try locate_sort qid
  with Not_found ->
    let g = Smartlocate.global_with_alias qid in
    let () = match g with
      | IndRef _ | ConstRef _ -> ()
      | VarRef _ | ConstructRef _ ->
        CErrors.user_err Pp.(pr_qualid qid ++ spc() ++ str "is not an inductive type or a constant.")
    in
    mkRef env sigma g

let locate_global_constructor_inductive_or_constant env sigma qid =
  let g = Smartlocate.global_with_alias qid in
  let () = match g with
    | ConstructRef _ | IndRef _ | ConstRef _ -> ()
    | VarRef _ -> CErrors.user_err Pp.(pr_qualid qid ++ spc() ++ str "is a section variable.")
  in
  let sigma, c = mkRef env sigma g in
  sigma, g, c

(* [get_type env sigma c] retrieves the type of [c] and returns a pair
   [l, t] such that [c : l_0 -> ... -> l_n -> t]. *)
let get_type env sigma c =
  (* inspired from [compute_implicit_names] in "interp/impargs.ml" *)
  let rec aux env acc t =
    let t = Reductionops.whd_all env sigma t in
    match EConstr.kind sigma t with
    | Constr.Prod (na, a, b) ->
       let a = Reductionops.whd_all env sigma a in
       let rel = Context.Rel.Declaration.LocalAssum (na, a) in
       aux (EConstr.push_rel rel env) ((na, a) :: acc) b
    | _ -> List.rev acc, t in
  let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in
  let l, t = aux env [] t in
  List.map (fun (na, a) -> EConstr.Unsafe.to_binder_annot na, EConstr.Unsafe.to_constr a) l,
  EConstr.Unsafe.to_constr t

(* [elaborate_to_post_params env sigma ty_ind params] builds the
   [to_post] translation (c.f., interp/notation.mli) for the numeral
   notation to parse/print type [ty_ind]. This translation is the
   identity ([ToPostCopy]) except that it checks ([ToPostCheck]) that
   the parameters of the inductive type [ty_ind] match the ones given
   in [params]. *)
let elaborate_to_post_params env sigma ty_ind params =
  let to_post_for_constructor indc =
    let sigma, c = match indc with
      | GlobRef.ConstructRef _ -> mkRef env sigma indc
      | _ -> assert false in  (* c.f. get_constructors *)
    let args, t = get_type env sigma c in
    let params_indc = match Constr.kind t with
      | Constr.App (_, a) -> Array.to_list a | _ -> [] in
    let sz = List.length args in
    let a = Array.make sz ToPostCopy in
    if List.length params <> List.length params_indc then error_params ty_ind;
    List.iter2 (fun param param_indc ->
        match param, Constr.kind param_indc with
        | Some p, Constr.Rel i when i <= sz -> a.(sz - i) <- ToPostCheck p
        | _ -> ())
      params params_indc;
    indc, indc, Array.to_list a in
  let pt_refs = get_constructors ty_ind in
  let to_post_0 = List.map to_post_for_constructor pt_refs in
  let to_post =
    let only_copy (_, _, args) = List.for_all ((=) ToPostCopy) args in
    if (List.for_all only_copy to_post_0) then [||] else [|to_post_0|] in
  to_post, pt_refs

(* [elaborate_to_post_via env sigma ty_name ty_ind l] builds the [to_post]
   translation (c.f., interp/notation.mli) for the number notation to
   parse/print type [ty_name] through the inductive [ty_ind] according
   to the pairs [constant, constructor] in the list [l]. *)
let elaborate_to_post_via env sigma ty_name ty_ind l =
  let sigma, ty_name =
    locate_global_sort_inductive_or_constant env sigma ty_name in
  let sigma, ty_ind = mkRef env sigma (IndRef ty_ind) in
  (* Retrieve constants and constructors mappings and their type.
     For each constant [cnst] and inductive constructor [indc] in [l], retrieve:
     * its location: [lcnst] and [lindc]
     * its GlobRef: [cnst] and [indc]
     * its type: [tcnst] and [tindc] (decomposed in product by [get_type] above)
     * [impls] are the implicit arguments of [cnst] *)
  let sigma, l =
    let read sigma (consider_implicits, cnst, indc) =
      let lcnst, lindc = cnst.CAst.loc, indc.CAst.loc in
      let sigma, cnst, ccnst = locate_global_constructor_inductive_or_constant env sigma cnst in
      let indc = GlobRef.ConstructRef (Smartlocate.global_constructor_with_alias indc) in
      let sigma, cindc = mkRef env sigma indc in
      let get_type_wo_params c =
        (* ignore parameters of inductive types *)
        let rm_params c = match Constr.kind c with
          | Constr.App (c, _) when Constr.isInd c -> c
          | _ -> c in
        let lc, tc = get_type env sigma c in
        List.map (fun (n, c) -> n, rm_params c) lc, rm_params tc in
      let tcnst, tindc = get_type_wo_params ccnst, get_type_wo_params cindc in
      let impls =
        if not consider_implicits then [] else
          Impargs.(select_stronger_impargs (implicits_of_global cnst)) in
      sigma, (lcnst, cnst, tcnst, lindc, indc, tindc, impls) in
    List.fold_left_map read sigma l
  in
  let eq_indc indc (_, _, _, _, indc', _, _) = Environ.QGlobRef.equal env indc indc' in
  (* Collect all inductive types involved.
     That is [ty_ind] and all final codomains of [tindc] above. *)
  let inds =
    List.fold_left (fun s (_, _, _, _, _, tindc, _) -> CSet.add (snd tindc) s)
      (CSet.singleton ty_ind) l in
  (* And for each inductive, retrieve its constructors. *)
  let constructors =
    CSet.fold (fun ind m ->
        let inductive, _ = Constr.destInd ind in
        CMap.add ind (get_constructors inductive) m)
      inds CMap.empty in
  (* Error if one [constructor] in some inductive in [inds]
     doesn't appear exactly once in [l] *)
  let _ : _ list = (* check_for duplicate constructor and error *)
    List.fold_left (fun already_seen (_, cnst, _, loc, indc, _, _) ->
        try
          let cnst' = List.assoc_f (fun c1 c2 -> Environ.QGlobRef.equal env c1 c2) indc already_seen in
          remapping_error ?loc indc cnst' cnst
        with Not_found -> (indc, cnst) :: already_seen)
    [] l in
  let () = (* check for missing constructor and error *)
    CMap.iter (fun _ ctors ->
        List.iter (fun cstr ->
            if not (List.exists (eq_indc cstr) l) then error_missing cstr)
          ctors)
      constructors in
  (* Perform some checks on types and warn if they look strange.
     These checks are neither sound nor complete, so we only warn. *)
  let () =
    (* associate inductives to types, and check that this mapping is one to one
       and maps [ty_ind] to [ty_name] *)
    let ind2ty, ty2ind =
      let add loc ckey cval m =
        match CMap.find_opt ckey m with
        | None -> CMap.add ckey cval m
        | Some old_cval ->
           if not (Constr.eq_constr_nounivs old_cval cval) then
             warn_via_remapping ?loc (env, sigma, ckey, old_cval, cval);
           m in
      List.fold_left
        (fun (ind2ty, ty2ind) (lcnst, _, (_, tcnst), lindc, _, (_, tindc), _) ->
          add lcnst tindc tcnst ind2ty, add lindc tcnst tindc ty2ind)
        CMap.(singleton ty_ind ty_name, singleton ty_name ty_ind) l in
    (* check that type of constants and constructors mapped in [l]
       match modulo [ind2ty] *)
    let rm_impls impls (l, t) =
      let rec aux impls l = match impls, l with
        | Some _ :: impls, _ :: b -> aux impls b
        | None :: impls, (n, a) :: b -> (n, a) :: aux impls b
        | _ -> l in
      aux impls l, t in
    let replace m (l, t) =
      let apply_m c = try CMap.find c m with Not_found -> c in
      List.fold_right (fun (na, a) b -> Constr.mkProd (na, (apply_m a), b))
        l (apply_m t) in
    List.iter (fun (_, cnst, tcnst, loc, indc, tindc, impls) ->
        let tcnst = rm_impls impls tcnst in
        let tcnst' = replace CMap.empty tcnst in
        if not (Constr.eq_constr_nounivs tcnst' (replace ind2ty tindc)) then
          let actual = replace CMap.empty tindc in
          let expected = replace ty2ind tcnst in
          warn_via_type_mismatch ?loc (env, sigma, indc, cnst, expected, actual))
      l in
  (* Associate an index to each inductive, starting from 0 for [ty_ind]. *)
  let ind2num, num2ind, nb_ind =
    CMap.fold (fun ind _ (ind2num, num2ind, i) ->
        CMap.add ind i ind2num, Int.Map.add i ind num2ind, i + 1)
      (CMap.remove ty_ind constructors)
      (CMap.singleton ty_ind 0, Int.Map.singleton 0 ty_ind, 1) in
  (* Finally elaborate [to_post] *)
  let to_post =
    let rec map_prod impls tindc = match impls with
      | (Some _ as i) :: impls -> ToPostHole (Impargs.name_of_implicit i) :: map_prod impls tindc
      | _ ->
         match tindc with
         | [] -> []
         | (_, a) :: b ->
            let t = match CMap.find_opt a ind2num with
              | Some i -> ToPostAs i
              | None -> ToPostCopy in
            let impls = match impls with [] -> [] | _ :: t -> t in
            t :: map_prod impls b in
    Array.init nb_ind (fun i ->
        List.map (fun indc ->
            let _, cnst, _, _, _, tindc, impls = List.find (eq_indc indc) l in
            indc, cnst, map_prod impls (fst tindc))
          (CMap.find (Int.Map.find i num2ind) constructors)) in
  (* and use constants mapped to constructors of [ty_ind] as triggers. *)
  let pt_refs = List.map (fun (_, cnst, _) -> cnst) (to_post.(0)) in
  to_post, pt_refs

type target_type =
  | TargetInd of (inductive * Constr.t option list)
  | TargetPrim of GlobRef.t * GlobRef.t list * required_module

let locate_global_inductive_with_params allow_params qid =
  if not allow_params then raise Not_found else
    match Nametab.locate_extended qid with
    | Globnames.TrueGlobal _ -> raise Not_found
    | Globnames.Abbrev kn ->
    match Abbreviation.search_abbreviation kn with
    | [], Notation_term.(NApp (NRef (GlobRef.IndRef i,None), l)) ->
       i,
       List.map (function
           | Notation_term.NHole _ -> None
           | n ->
              let g = Notation_ops.glob_constr_of_notation_constr n in
              let c, _ =
                let env = Global.env () in
                let sigma = Evd.from_env env in
                Pretyping.understand env sigma g in
              Some (EConstr.Unsafe.to_constr c)) l
    | _ -> raise Not_found

let locate_global_inductive_or_int63_or_float env allow_params qid =
  try TargetInd (locate_global_inductive_with_params allow_params qid)
  with Not_found ->
    let int63n = "num.int63.type" in
    let int63c = "num.int63.wrap_int" in
    let int63w = "num.int63.int_wrapper" in
    let floatn = "num.float.type" in
    let floatc = "num.float.wrap_float" in
    let floatw = "num.float.float_wrapper" in
    if allow_params && Rocqlib.check_ref int63n (Smartlocate.global_with_alias qid)
    then TargetPrim (Rocqlib.lib_ref int63w, [Rocqlib.lib_ref int63c],
                     (Nametab.path_of_global (Rocqlib.lib_ref int63n), []))
    else if allow_params && Rocqlib.check_ref floatn (Smartlocate.global_with_alias qid)
    then TargetPrim (Rocqlib.lib_ref floatw, [Rocqlib.lib_ref floatc],
                     (Nametab.path_of_global (Rocqlib.lib_ref floatn), []))
    else TargetInd (Smartlocate.global_inductive_with_alias qid, [])

let intern_cref env sigma r =
  Constrintern.intern_constr env sigma (CAst.make @@ Constrexpr.CAppExpl ((r,None),[]))

let vernac_number_notation local ty f g opts scope =
  let rec parse_opts = function
    | [] -> None, Nop
    | h :: opts ->
       let via, opts = parse_opts opts in
       let via = match h, via with
         | Via _, Some _ -> multiple_via_error ()
         | Via v, None -> Some v
         | _ -> via in
       let opts = match h, opts with
         | After _, (Warning _ | Abstract _) -> multiple_after_error ()
         | After a, Nop -> a
         | _ -> opts in
       via, opts in
  let via, opts = parse_opts opts in
  (match via, opts with Some _, Abstract _ -> via_abstract_error () | _ -> ());
  let env = Global.env () in
  let sigma = Evd.from_env env in
  let targets = List.concat [
      locate_number ();
      locate_z ();
      locate_int63 ();
      locate_float ();
    ]
  in
  let ty_name = ty in
  let ty, via =
    match via with None -> ty, via | Some (ty', a) -> ty', Some (ty, a) in
  let tyc_params = locate_global_inductive_or_int63_or_float env (via = None) ty in
  let to_ty = Smartlocate.global_with_alias f in
  let of_ty = Smartlocate.global_with_alias g in
  let cty = intern_cref env sigma ty in
  let f_name, f = f, intern_cref env sigma f in
  let g_name, g = g, intern_cref env sigma g in
  (* Check the type of f *)
  let to_kind =
    match List.find_map (fun target -> is_to_target env sigma f cty target) targets with
    | Some v -> v
    | None -> type_error_to f_name ty
  in
  (* Check the type of g *)
  let cty = match tyc_params with TargetPrim (c, _, _) -> gref c | TargetInd _ -> cty in
  let of_kind =
    match List.find_map (fun target -> is_from_target env sigma g cty target) targets with
    | Some v -> v
    | None -> type_error_of g_name ty
  in
  let to_post, pt_required, pt_refs = match tyc_params with
    | TargetPrim (_, refs, path) -> [||], path, refs
    | TargetInd (tyc, params) ->
       let to_post, pt_refs =
         match via with
         | None -> elaborate_to_post_params env sigma tyc params
         | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in
       to_post, (Nametab.path_of_global (GlobRef.IndRef tyc), []), pt_refs in
  let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name;
            warning = opts }
  in
  (match opts, to_kind with
   | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty
   | _ -> ());
  let i =
       { pt_local = local;
         pt_scope = scope;
         pt_interp_info = NumberNotation o;
         pt_required;
         pt_refs;
         pt_in_match = true }
  in
  enable_prim_token_interpretation i

(** * String notation *)

let locate_global_inductive_or_pstring env allow_params qid =
  try TargetInd (locate_global_inductive_with_params allow_params qid)
  with Not_found ->
    let pstringn = "strings.pstring.type" in
    let pstringc = "strings.pstring.wrap_string" in
    let pstringw = "strings.pstring.string_wrapper" in
    if allow_params && Rocqlib.check_ref pstringn (Smartlocate.global_with_alias qid)
    then TargetPrim (Rocqlib.lib_ref pstringw, [Rocqlib.lib_ref pstringc],
                     (Nametab.path_of_global (Rocqlib.lib_ref pstringn), []))
    else TargetInd (Smartlocate.global_inductive_with_alias qid, [])

let locate_pstring () =
  match Rocqlib.lib_ref_opt "strings.pstring.type" with
  | None -> []
  | Some q_pstring ->
    [ { kind = PString; typ = gref q_pstring }; ]

let locate_bytestring () =
  match Rocqlib.lib_ref_opt "core.byte.type" with
  | None -> []
  | Some q_byte ->
    let byte_target = { kind = Byte; typ = gref q_byte } in
    match Rocqlib.lib_ref_opt "core.list.type" with
    | None -> [ byte_target ]
    | Some q_list ->
      let app x y = DAst.make @@ GApp (x,[y]) in
      [ { kind = ListByte; typ = app (gref q_list) (gref q_byte) };
        byte_target;
      ]

let type_error_to f ty =
  let ppty = pr_qualid ty in
  CErrors.user_err
    (pr_qualid f ++ str " should go from Byte.byte, (list Byte.byte), or PrimString.string to " ++
     ppty ++ str " or (option " ++ ppty ++ str "), or (result " ++ ppty ++ str " _).")

let type_error_of g ty =
  CErrors.user_err
    (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
     strbrk " to T or (option T) or (result T _), where T is either Byte.byte, (list Byte.byte), or PrimString.string.")

let vernac_string_notation local ty f g via scope =
  let env = Global.env () in
  let sigma = Evd.from_env env in
  let targets = List.concat [
      locate_pstring ();
      locate_bytestring ();
    ]
  in
  let ty_name = ty in
  let ty, via =
    match via with None -> ty, via | Some (ty', a) -> ty', Some (ty, a) in
  let tyc_params = locate_global_inductive_or_pstring env (via = None) ty in
  let to_ty = Smartlocate.global_with_alias f in
  let of_ty = Smartlocate.global_with_alias g in
  let f_name, f = f, intern_cref env sigma f in
  let g_name, g = g, intern_cref env sigma g in
  let cty = intern_cref env sigma ty in
  (* Check the type of f *)
  let to_kind =
    match List.find_map (fun target -> is_to_target env sigma f cty target) targets with
    | Some v -> v
    | None -> type_error_to f_name ty
  in
  (* Check the type of g *)
  let of_kind =
    match List.find_map (fun target -> is_from_target env sigma g cty target) targets with
    | Some v -> v
    | None -> type_error_of g_name ty
  in
  let to_post, pt_required, pt_refs = match tyc_params with
    | TargetPrim (_, refs, path) -> [||], path, refs
    | TargetInd (tyc, params) ->
       let to_post, pt_refs =
         match via with
         | None -> elaborate_to_post_params env sigma tyc params
         | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in
       to_post, (Nametab.path_of_global (GlobRef.IndRef tyc), []), pt_refs in
  let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name; warning = () } in
  let i =
       { pt_local = local;
         pt_scope = scope;
         pt_interp_info = StringNotation o;
         pt_required;
         pt_refs;
         pt_in_match = true }
  in
  enable_prim_token_interpretation i

quality100%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.