diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr.ml | 12 | ||||
| -rw-r--r-- | interp/constrexpr_ops.ml | 5 | ||||
| -rw-r--r-- | interp/constrextern.ml | 2 | ||||
| -rw-r--r-- | interp/constrintern.ml | 10 | ||||
| -rw-r--r-- | interp/constrintern.mli | 14 | ||||
| -rw-r--r-- | interp/declare.ml | 40 | ||||
| -rw-r--r-- | interp/dumpglob.mli | 1 | ||||
| -rw-r--r-- | interp/impargs.ml | 2 | ||||
| -rw-r--r-- | interp/impargs.mli | 1 | ||||
| -rw-r--r-- | interp/notation.ml | 287 | ||||
| -rw-r--r-- | interp/notation.mli | 26 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 12 | ||||
| -rw-r--r-- | interp/notation_term.ml | 4 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 7 | ||||
| -rw-r--r-- | interp/syntax_def.mli | 3 |
15 files changed, 282 insertions, 144 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 77d612cfd9..757d186c8b 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -80,8 +80,8 @@ type cases_pattern_expr_r = and cases_pattern_expr = cases_pattern_expr_r CAst.t and cases_pattern_notation_substitution = - cases_pattern_expr list * (** for constr subterms *) - cases_pattern_expr list list (** for recursive notations *) + cases_pattern_expr list * (* for constr subterms *) + cases_pattern_expr list list (* for recursive notations *) and constr_expr_r = | CRef of qualid * instance_expr option @@ -142,10 +142,10 @@ and local_binder_expr = | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t and constr_notation_substitution = - constr_expr list * (** for constr subterms *) - constr_expr list list * (** for recursive notations *) - cases_pattern_expr list * (** for binders *) - local_binder_expr list list (** for binder lists (recursive notations) *) + constr_expr list * (* for constr subterms *) + constr_expr list list * (* for recursive notations *) + cases_pattern_expr list * (* for binders *) + local_binder_expr list list (* for binder lists (recursive notations) *) type constr_pattern_expr = constr_expr diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 3a4969a3ee..3a5af1dd5f 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -140,7 +140,7 @@ let rec constr_expr_eq e1 e2 = in List.equal field_eq l1 l2 | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) -> - (** Don't care about the case_style *) + (* Don't care about the case_style *) Option.equal constr_expr_eq r1 r2 && List.equal case_expr_eq a1 a2 && List.equal branch_expr_eq brl1 brl2 @@ -220,7 +220,7 @@ and local_binder_eq l1 l2 = match l1, l2 with | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> - (** Don't care about the [binder_kind] *) + (* Don't care about the [binder_kind] *) List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false @@ -258,7 +258,6 @@ let local_binders_loc bll = match bll with | h :: l -> Loc.merge_opt (local_binder_loc h) (local_binder_loc (List.last bll)) (** Folds and maps *) - let is_constructor id = try Globnames.isConstructRef (Smartlocate.global_of_extended_global diff --git a/interp/constrextern.ml b/interp/constrextern.ml index fba03b9de9..0d0b6158d9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -960,7 +960,7 @@ let rec extern inctx (custom,scopes as allscopes) vars r = | GSort s -> CSort (extern_glob_sort s) - | GHole (e,naming,_) -> CHole (Some e, naming, None) (** TODO: extern tactics. *) + | GHole (e,naming,_) -> CHole (Some e, naming, None) (* TODO: extern tactics. *) | GCast (c, c') -> CCast (sub_extern true scopes vars c, diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6313f2d7ba..7aa85a0810 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1507,7 +1507,7 @@ let drop_notations_pattern looked_for genv = let test_kind top = if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found in - (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) + (* [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) let rec rcp_of_glob scopes x = DAst.(map (function | GVar id -> RCPatAtom (Some (CAst.make ?loc:x.loc id,scopes)) | GHole (_,_,_) -> RCPatAtom (None) @@ -1527,8 +1527,8 @@ let drop_notations_pattern looked_for genv = try match Nametab.locate_extended qid with | SynDef sp -> - let (vars,a) = Syntax_def.search_syntactic_definition sp in - (match a with + let filter (vars,a) = + try match a with | NRef g -> (* Convention: do not deactivate implicit arguments and scopes for further arguments *) test_kind top g; @@ -1549,7 +1549,9 @@ let drop_notations_pattern looked_for genv = let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in let (_,argscs) = find_remaining_scopes pats1 pats2 g in Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2) - | _ -> raise Not_found) + | _ -> raise Not_found + with Not_found -> None in + Syntax_def.search_filtered_syntactic_definition filter sp | TrueGlobal g -> test_kind top g; Dumpglob.add_glob ?loc:qid.loc g; diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 035e4bc644..61acd09d65 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -45,13 +45,15 @@ type var_internalization_type = type var_internalization_data = var_internalization_type * - (** type of the "free" variable, for coqdoc, e.g. while typing the - constructor of JMeq, "JMeq" behaves as a variable of type Inductive *) + (* 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 *) + (* 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 *) (** A map of free variables to their implicit arguments and scopes *) type internalization_env = var_internalization_data Id.Map.t diff --git a/interp/declare.ml b/interp/declare.ml index 1e972d3e35..6778fa1e7a 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -56,7 +56,7 @@ let load_constant i ((sp,kn), obj) = (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn), obj) = - (** Never open a local definition *) + (* Never open a local definition *) if obj.cst_locl then () else let con = Global.constant_of_delta_kn kn in @@ -166,9 +166,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e export_seff || not de.const_entry_opaque || is_poly de -> - (** This globally defines the side-effects in the environment. We mark - exported constants as being side-effect not to redeclare them at - caching time. *) + (* This globally defines the side-effects in the environment. We mark + exported constants as being side-effect not to redeclare them at + caching time. *) let de, export = Global.export_private_constants ~in_section de in export, ConstantEntry (PureEntry, DefinitionEntry de) | _ -> [], ConstantEntry (EffectEntry, cd) @@ -191,7 +191,6 @@ let declare_definition ?(internal=UserIndividualRequest) (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of section variables and local definitions *) - type section_variable_entry = | SectionLocalDef of Safe_typing.private_constants definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) @@ -214,16 +213,16 @@ let cache_variable ((sp,_),o) = | SectionLocalDef (de) -> let (de, eff) = Global.export_private_constants ~in_section:true de in let () = List.iter register_side_effect eff in - (** The body should already have been forced upstream because it is a - section-local definition, but it's not enforced by typing *) + (* The body should already have been forced upstream because it is a + section-local definition, but it's not enforced by typing *) let (body, uctx), () = Future.force de.const_entry_body in let poly, univs = match de.const_entry_universes with | Monomorphic_const_entry uctx -> false, uctx | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in let univs = Univ.ContextSet.union uctx univs in - (** We must declare the universe constraints before type-checking the - term. *) + (* We must declare the universe constraints before type-checking the + term. *) let () = Global.push_context_set (not poly) univs in let se = { secdef_body = body; @@ -262,7 +261,6 @@ let declare_variable id obj = oname (** Declaration of inductive blocks *) - let declare_inductive_argument_scopes kn mie = List.iteri (fun i {mind_entry_consnames=lc} -> Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i)); @@ -360,7 +358,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter let id = Label.to_id label in let univs = match univs with | Monomorphic_ind_entry _ -> - (** Global constraints already defined through the inductive *) + (* Global constraints already defined through the inductive *) Monomorphic_const_entry Univ.ContextSet.empty | Polymorphic_ind_entry (nas, ctx) -> Polymorphic_const_entry (nas, ctx) @@ -447,11 +445,9 @@ let assumption_message id = (** Monomorphic universes need to survive sections. *) let input_universe_context : Univ.ContextSet.t -> Libobject.obj = - declare_object - { (default_object "Monomorphic section universes") with - cache_function = (fun (na, uctx) -> Global.push_context_set false uctx); - discharge_function = (fun (_, x) -> Some x); - classify_function = (fun a -> Dispose) } + declare_object @@ local_object "Monomorphic section universes" + ~cache:(fun (na, uctx) -> Global.push_context_set false uctx) + ~discharge:(fun (_, x) -> Some x) let declare_universe_context poly ctx = if poly then @@ -469,7 +465,7 @@ type universe_source = | QualifiedUniv of Id.t (* global universe introduced by some global value *) | UnqualifiedUniv (* other global universe *) -type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list +type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list let check_exists sp = if Nametab.exists_universe sp then @@ -511,7 +507,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj = load_function = load_univ_names; open_function = open_univ_names; discharge_function = discharge_univ_names; - subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a); + subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a); classify_function = (fun a -> Substitute a) } let declare_univ_binders gr pl = @@ -540,12 +536,8 @@ let do_universe poly l = user_err ~hdr:"Constraint" (str"Cannot declare polymorphic universes outside sections") in - let l = - List.map (fun {CAst.v=id} -> - let lev = UnivGen.new_univ_id () in - (id, lev)) l - in - let ctx = List.fold_left (fun ctx (_,(dp,i)) -> Univ.LSet.add (Univ.Level.make dp i) ctx) + let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in + let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) Univ.LSet.empty l, Univ.Constraint.empty in let () = declare_universe_context poly ctx in diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 931d05a975..554da7603f 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -18,6 +18,7 @@ val dump : unit -> bool val noglob : unit -> unit val dump_into_file : string -> unit (** special handling of "stdout" *) + val dump_to_dotglob : unit -> unit val feedback_glob : unit -> unit diff --git a/interp/impargs.ml b/interp/impargs.ml index d024a9e808..8a89bcdf26 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -448,7 +448,7 @@ let compute_mib_implicits flags kn = Array.to_list (Array.mapi (* No need to lift, arities contain no de Bruijn *) (fun i mip -> - (** No need to care about constraints here *) + (* No need to care about constraints here *) let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty)) mib.mind_packets) in diff --git a/interp/impargs.mli b/interp/impargs.mli index ea5aa90f68..4afc2af5e9 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -65,6 +65,7 @@ type implicit_explanation = operational only if [conclusion_matters] is true. *) type maximal_insertion = bool (** true = maximal contextual insertion *) + type force_inference = bool (** true = always infer, never turn into evar/subgoal *) type implicit_status = (Id.t * implicit_explanation * diff --git a/interp/notation.ml b/interp/notation.ml index 0af75b5bfa..c866929234 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -308,7 +308,7 @@ let declare_delimiters scope key = | None -> scope_map := String.Map.add scope newsc !scope_map | Some oldkey when String.equal oldkey key -> () | Some oldkey -> - (** FIXME: implement multikey scopes? *) + (* FIXME: implement multikey scopes? *) Flags.if_verbose Feedback.msg_info (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope); scope_map := String.Map.add scope newsc !scope_map @@ -530,11 +530,11 @@ let prim_token_uninterpreters = (*******************************************************) (* Numeral notation interpretation *) -type numeral_notation_error = +type prim_token_notation_error = | UnexpectedTerm of Constr.t | UnexpectedNonOptionTerm of Constr.t -exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error +exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_token_notation_error type numnot_option = | Nop @@ -554,20 +554,26 @@ type target_kind = | UInt of Names.inductive (* Coq.Init.Decimal.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) +type string_target_kind = + | ListByte + | Byte + type option_kind = Option | Direct -type conversion_kind = target_kind * option_kind +type 'target conversion_kind = 'target * option_kind -type numeral_notation_obj = - { to_kind : conversion_kind; +type ('target, 'warning) prim_token_notation_obj = + { to_kind : 'target conversion_kind; to_ty : GlobRef.t; - of_kind : conversion_kind; + of_kind : 'target conversion_kind; of_ty : GlobRef.t; - num_ty : Libnames.qualid; (* for warnings / error messages *) - warning : numnot_option } + ty_name : Libnames.qualid; (* for warnings / error messages *) + warning : 'warning } -module Numeral = struct -(** * Numeral notation *) +type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj +type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj +module PrimTokenNotation = struct +(** * Code shared between Numeral notation and String notation *) (** Reduction The constr [c] below isn't necessarily well-typed, since we @@ -596,7 +602,69 @@ let eval_constr env sigma (c : Constr.t) = let eval_constr_app env sigma c1 c2 = eval_constr env sigma (mkApp (c1,[| c2 |])) -exception NotANumber +exception NotAValidPrimToken + +(** The uninterp function below work at the level of [glob_constr] + which is too low for us here. So here's a crude conversion back + to [constr] for the subset that concerns us. *) + +let rec constr_of_glob env sigma g = match DAst.get g with + | Glob_term.GRef (ConstructRef c, _) -> + let sigma,c = Evd.fresh_constructor_instance env sigma c in + sigma,mkConstructU c + | Glob_term.GApp (gc, gcl) -> + let sigma,c = constr_of_glob env sigma gc in + let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in + sigma,mkApp (c, Array.of_list cl) + | _ -> + raise NotAValidPrimToken + +let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with + | App (c, ca) -> + let c = glob_of_constr token_kind ?loc env sigma c in + let cel = List.map (glob_of_constr token_kind ?loc env sigma) (Array.to_list ca) in + DAst.make ?loc (Glob_term.GApp (c, cel)) + | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None)) + | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None)) + | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None)) + | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None)) + | _ -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedTerm c)) + +let no_such_prim_token uninterpreted_token_kind ?loc ty = + CErrors.user_err ?loc + (str ("Cannot interpret this "^uninterpreted_token_kind^" as a value of type ") ++ + pr_qualid ty) + +let interp_option uninterpreted_token_kind token_kind ty ?loc env sigma c = + match Constr.kind c with + | App (_Some, [| _; c |]) -> glob_of_constr token_kind ?loc env sigma c + | App (_None, [| _ |]) -> no_such_prim_token uninterpreted_token_kind ?loc ty + | x -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedNonOptionTerm c)) + +let uninterp_option c = + match Constr.kind c with + | App (_Some, [| _; x |]) -> x + | _ -> raise NotAValidPrimToken + +let uninterp to_raw o (Glob_term.AnyGlobConstr n) = + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in + let of_ty = EConstr.Unsafe.to_constr of_ty in + try + let sigma,n = constr_of_glob env sigma n in + let c = eval_constr_app env sigma of_ty n in + let c = if snd o.of_kind == Direct then c else uninterp_option c in + 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 *) + +end + +module Numeral = struct +(** * Numeral notation *) +open PrimTokenNotation let warn_large_num = CWarnings.create ~name:"large-number" ~category:"numbers" @@ -670,15 +738,15 @@ let rawnum_of_coquint c = | Construct ((_,n), _) (* D0 to D9 *) -> let () = Buffer.add_char buf (char_of_digit n) in of_uint_loop a buf - | _ -> raise NotANumber) - | _ -> raise NotANumber + | _ -> raise NotAValidPrimToken) + | _ -> raise NotAValidPrimToken in let buf = Buffer.create 64 in let () = of_uint_loop c buf in if Int.equal (Buffer.length buf) 0 then (* To avoid ambiguities between Nil and (D0 Nil), we choose to not display Nil alone as "0" *) - raise NotANumber + raise NotAValidPrimToken else Buffer.contents buf let rawnum_of_coqint c = @@ -687,8 +755,8 @@ let rawnum_of_coqint c = (match Constr.kind c with | Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true) | Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false) - | _ -> raise NotANumber) - | _ -> raise NotANumber + | _ -> raise NotAValidPrimToken) + | _ -> raise NotAValidPrimToken (***********************************************************************) @@ -718,9 +786,9 @@ let rec bigint_of_pos c = match Constr.kind c with | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d) | n -> assert false (* no other constructor of type positive *) end - | x -> raise NotANumber + | x -> raise NotAValidPrimToken end - | x -> raise NotANumber + | x -> raise NotAValidPrimToken (** Now, [Z] from/to bigint *) @@ -745,51 +813,9 @@ let bigint_of_z z = match Constr.kind z with | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d) | n -> assert false (* no other constructor of type Z *) end - | _ -> raise NotANumber + | _ -> raise NotAValidPrimToken end - | _ -> raise NotANumber - -(** The uninterp function below work at the level of [glob_constr] - which is too low for us here. So here's a crude conversion back - to [constr] for the subset that concerns us. *) - -let rec constr_of_glob env sigma g = match DAst.get g with - | Glob_term.GRef (ConstructRef c, _) -> - let sigma,c = Evd.fresh_constructor_instance env sigma c in - sigma,mkConstructU c - | Glob_term.GApp (gc, gcl) -> - let sigma,c = constr_of_glob env sigma gc in - let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in - sigma,mkApp (c, Array.of_list cl) - | _ -> - raise NotANumber - -let rec glob_of_constr ?loc env sigma c = match Constr.kind c with - | App (c, ca) -> - let c = glob_of_constr ?loc env sigma c in - let cel = List.map (glob_of_constr ?loc env sigma) (Array.to_list ca) in - DAst.make ?loc (Glob_term.GApp (c, cel)) - | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None)) - | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None)) - | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None)) - | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None)) - | _ -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedTerm c)) - -let no_such_number ?loc ty = - CErrors.user_err ?loc - (str "Cannot interpret this number as a value of type " ++ - pr_qualid ty) - -let interp_option ty ?loc env sigma c = - match Constr.kind c with - | App (_Some, [| _; c |]) -> glob_of_constr ?loc env sigma c - | App (_None, [| _ |]) -> no_such_number ?loc ty - | x -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedNonOptionTerm c)) - -let uninterp_option c = - match Constr.kind c with - | App (_Some, [| _; x |]) -> x - | _ -> raise NotANumber + | _ -> raise NotAValidPrimToken let big2raw n = if Bigint.is_pos_or_zero n then (Bigint.to_string n, true) @@ -801,13 +827,13 @@ let raw2big (n,s) = let interp o ?loc n = begin match o.warning with | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 -> - warn_large_num o.num_ty + warn_large_num o.ty_name | _ -> () end; let c = match fst o.to_kind with | Int int_ty -> coqint_of_rawnum int_ty n | UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n) - | UInt _ (* n <= 0 *) -> no_such_number ?loc o.num_ty + | UInt _ (* n <= 0 *) -> no_such_prim_token "number" ?loc o.ty_name | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n) in let env = Global.env () in @@ -816,30 +842,120 @@ let interp o ?loc n = let to_ty = EConstr.Unsafe.to_constr to_ty in match o.warning, snd o.to_kind with | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 -> - warn_abstract_large_num (o.num_ty,o.to_ty); - glob_of_constr ?loc env sigma (mkApp (to_ty,[|c|])) + warn_abstract_large_num (o.ty_name,o.to_ty); + glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|])) | _ -> let res = eval_constr_app env sigma to_ty c in match snd o.to_kind with - | Direct -> glob_of_constr ?loc env sigma res - | Option -> interp_option o.num_ty ?loc env sigma res + | Direct -> glob_of_constr "numeral" ?loc env sigma res + | Option -> interp_option "number" "numeral" o.ty_name ?loc env sigma res + +let uninterp o n = + PrimTokenNotation.uninterp + begin function + | (Int _, c) -> rawnum_of_coqint c + | (UInt _, c) -> (rawnum_of_coquint c, true) + | (Z _, c) -> big2raw (bigint_of_z c) + end o n +end + +module Strings = struct +(** * String notation *) +open PrimTokenNotation + +let qualid_of_ref n = + n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty + +let q_list () = qualid_of_ref "core.list.type" +let q_byte () = qualid_of_ref "core.byte.type" + +let unsafe_locate_ind q = + match Nametab.locate q with + | IndRef i -> i + | _ -> raise Not_found + +let locate_list () = unsafe_locate_ind (q_list ()) +let locate_byte () = unsafe_locate_ind (q_byte ()) + +(***********************************************************************) + +(** ** Conversion between Coq [list Byte.byte] and internal raw string *) + +let coqbyte_of_char_code byte c = + mkConstruct (byte, 1 + c) + +let coqbyte_of_string ?loc byte s = + let p = + if Int.equal (String.length s) 1 then int_of_char s.[0] + else + if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] + then int_of_string s + else + user_err ?loc ~hdr:"coqbyte_of_string" + (str "Expects a single character or a three-digits ascii code.") in + coqbyte_of_char_code byte p + +let coqbyte_of_char byte c = coqbyte_of_char_code byte (Char.code c) + +let make_ascii_string n = + if n>=32 && n<=126 then String.make 1 (char_of_int n) + else Printf.sprintf "%03d" n + +let char_code_of_coqbyte c = + match Constr.kind c with + | Construct ((_,c), _) -> c - 1 + | _ -> raise NotAValidPrimToken + +let string_of_coqbyte c = make_ascii_string (char_code_of_coqbyte c) + +let coqlist_byte_of_string byte_ty list_ty str = + let cbyte = mkInd byte_ty in + let nil = mkApp (mkConstruct (list_ty, 1), [|cbyte|]) in + let cons x xs = mkApp (mkConstruct (list_ty, 2), [|cbyte; x; xs|]) in + let rec do_chars s i acc = + if i < 0 then acc + else + let b = coqbyte_of_char byte_ty s.[i] in + do_chars s (i-1) (cons b acc) + in + do_chars str (String.length str - 1) nil + +(* N.B. We rely on the fact that [nil] is the first constructor and [cons] is the second constructor, for [list] *) +let string_of_coqlist_byte c = + let rec of_coqlist_byte_loop c buf = + match Constr.kind c with + | App (_nil, [|_ty|]) -> () + | App (_cons, [|_ty;b;c|]) -> + let () = Buffer.add_char buf (Char.chr (char_code_of_coqbyte b)) in + of_coqlist_byte_loop c buf + | _ -> raise NotAValidPrimToken + in + let buf = Buffer.create 64 in + let () = of_coqlist_byte_loop c buf in + Buffer.contents buf -let uninterp o (Glob_term.AnyGlobConstr n) = +let interp o ?loc n = + let byte_ty = locate_byte () in + let list_ty = locate_list () in + let c = match fst o.to_kind with + | ListByte -> coqlist_byte_of_string byte_ty list_ty n + | Byte -> coqbyte_of_string ?loc byte_ty n + in let env = Global.env () in let sigma = Evd.from_env env in - let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in - let of_ty = EConstr.Unsafe.to_constr of_ty in - try - let sigma,n = constr_of_glob env sigma n in - let c = eval_constr_app env sigma of_ty n in - let c = if snd o.of_kind == Direct then c else uninterp_option c in - match fst o.of_kind with - | Int _ -> Some (rawnum_of_coqint c) - | UInt _ -> Some (rawnum_of_coquint c, true) - | Z _ -> Some (big2raw (bigint_of_z c)) - with - | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *) - | NotANumber -> None (* all other functions except big2raw *) + let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in + let to_ty = EConstr.Unsafe.to_constr to_ty in + let res = eval_constr_app env sigma to_ty c in + match snd o.to_kind with + | Direct -> glob_of_constr "string" ?loc env sigma res + | Option -> interp_option "string" "string" o.ty_name ?loc env sigma res + +let uninterp o n = + PrimTokenNotation.uninterp + begin function + | (ListByte, c) -> string_of_coqlist_byte c + | (Byte, c) -> string_of_coqbyte c + end o n end (* A [prim_token_infos], which is synchronized with the document @@ -853,6 +969,7 @@ end type prim_token_interp_info = Uid of prim_token_uid | NumeralNotation of numeral_notation_obj + | StringNotation of string_notation_obj type prim_token_infos = { pt_local : bool; (** Is this interpretation local? *) @@ -1081,6 +1198,7 @@ let find_prim_token check_allowed ?loc p sc = let interp = match info with | Uid uid -> Hashtbl.find prim_token_interpreters uid | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o) + | StringNotation o -> InnerPrimToken.StringInterp (Strings.interp o) in let pat = InnerPrimToken.do_interp ?loc interp p in check_allowed pat; @@ -1270,6 +1388,7 @@ let uninterp_prim_token c = let uninterp = match info with | Uid uid -> Hashtbl.find prim_token_uninterpreters uid | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o) + | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o) in match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with | None -> raise Notation_ops.No_match @@ -1289,6 +1408,8 @@ let availability_of_prim_token n printer_scope local_scopes = match n, uid with | Numeral _, NumeralNotation _ -> true | _, NumeralNotation _ -> false + | String _, StringNotation _ -> true + | _, StringNotation _ -> false | _, Uid uid -> let interp = Hashtbl.find prim_token_interpreters uid in match n, interp with diff --git a/interp/notation.mli b/interp/notation.mli index 3480d1c8f2..75034cad70 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -54,7 +54,7 @@ val scope_is_open : scope_name -> bool (** Open scope *) val open_close_scope : - (** locality *) bool * (* open *) bool * scope_name -> unit + (* locality *) bool * (* open *) bool * scope_name -> unit (** Extend a list of scopes *) val empty_scope_stack : scopes @@ -104,11 +104,11 @@ val register_string_interpretation : (** * Numeral notation *) -type numeral_notation_error = +type prim_token_notation_error = | UnexpectedTerm of Constr.t | UnexpectedNonOptionTerm of Constr.t -exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error +exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_token_notation_error type numnot_option = | Nop @@ -128,20 +128,28 @@ type target_kind = | UInt of Names.inductive (* Coq.Init.Decimal.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) +type string_target_kind = + | ListByte + | Byte + type option_kind = Option | Direct -type conversion_kind = target_kind * option_kind +type 'target conversion_kind = 'target * option_kind -type numeral_notation_obj = - { to_kind : conversion_kind; +type ('target, 'warning) prim_token_notation_obj = + { to_kind : 'target conversion_kind; to_ty : GlobRef.t; - of_kind : conversion_kind; + of_kind : 'target conversion_kind; of_ty : GlobRef.t; - num_ty : Libnames.qualid; (* for warnings / error messages *) - warning : numnot_option } + ty_name : Libnames.qualid; (* for warnings / error messages *) + warning : 'warning } + +type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj +type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj type prim_token_interp_info = Uid of prim_token_uid | NumeralNotation of numeral_notation_obj + | StringNotation of string_notation_obj type prim_token_infos = { pt_local : bool; (** Is this interpretation local? *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7a525f84a5..8d225fe683 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -37,7 +37,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | _ -> false) | NApp (t1, a1), NApp (t2, a2) -> (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2 -| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *) +| NHole (_, _, _), NHole (_, _, _) -> true (* FIXME? *) | NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) -> Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 && b1 == b2 @@ -51,7 +51,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) -> Name.equal na1 na2 && eq_notation_constr vars b1 b2 && Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 -| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *) +| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *) let eqpat (p1, t1) (p2, t2) = List.equal cases_pattern_eq p1 p2 && (eq_notation_constr vars) t1 t2 @@ -75,7 +75,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with Option.equal (eq_notation_constr vars) o1 o2 && (eq_notation_constr vars) u1 u2 && (eq_notation_constr vars) r1 r2 -| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *) +| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *) let eq (na1, o1, t1) (na2, o2, t2) = Name.equal na1 na2 && Option.equal (eq_notation_constr vars) o1 o2 && @@ -530,8 +530,10 @@ let rec subst_notation_constr subst bound raw = match raw with | NRef ref -> let ref',t = subst_global subst ref in - if ref' == ref then raw else - fst (notation_constr_of_constr bound t) + if ref' == ref then raw else (match t with + | None -> NRef ref' + | Some t -> + fst (notation_constr_of_constr bound t.Univ.univ_abstracted_value)) | NVar _ -> raw diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 5fb0ca1b43..0ef1f267f6 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -20,13 +20,13 @@ open Glob_term as well as non global expressions such as existential variables. *) type notation_constr = - (** Part common to [glob_constr] and [cases_pattern] *) + (* Part common to [glob_constr] and [cases_pattern] *) | NRef of GlobRef.t | NVar of Id.t | NApp of notation_constr * notation_constr list | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool - (** Part only in [glob_constr] *) + (* Part only in [glob_constr] *) | NLambda of Name.t * notation_constr * notation_constr | NProd of Name.t * notation_constr * notation_constr | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index b73d238c22..49273c4146 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -105,3 +105,10 @@ let search_syntactic_definition ?loc kn = let def = out_pat pat in verbose_compat ?loc kn def v; def + +let search_filtered_syntactic_definition ?loc filter kn = + let pat,v = KNmap.find kn !syntax_table in + let def = out_pat pat in + let res = filter def in + (match res with Some _ -> verbose_compat ?loc kn def v | None -> ()); + res diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index c5b6655ff8..77873f8f67 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -19,3 +19,6 @@ val declare_syntactic_definition : bool -> Id.t -> Flags.compat_version option -> syndef_interpretation -> unit val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation + +val search_filtered_syntactic_definition : ?loc:Loc.t -> + (syndef_interpretation -> 'a option) -> KerName.t -> 'a option |