diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/astterm.ml | 36 | ||||
| -rw-r--r-- | parsing/astterm.mli | 2 | ||||
| -rw-r--r-- | parsing/coqlib.ml | 1 | ||||
| -rw-r--r-- | parsing/pretty.ml | 1 | ||||
| -rw-r--r-- | parsing/pretty.mli | 8 | ||||
| -rw-r--r-- | parsing/printer.ml | 4 | ||||
| -rw-r--r-- | parsing/termast.ml | 1 | ||||
| -rw-r--r-- | parsing/termast.mli | 2 |
8 files changed, 34 insertions, 21 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index a915148a31..5024d515d7 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -18,7 +18,11 @@ open Pretyping open Evarutil open Ast open Coqast -open Pretype_errors +open Nametab + +type extended_global_reference = + | TrueGlobal of global_reference + | SyntacticDef of section_path (*Takes a list of variables which must not be globalized*) let from_list l = List.fold_right Idset.add l Idset.empty @@ -243,9 +247,8 @@ let ast_to_var (env,impls) (vars1,vars2) loc s = (* This is generic code to deal with globalization *) type 'a globalization_action = { - parse_var : string -> 'a; - parse_ref : global_reference -> 'a; - parse_syn : section_path -> 'a; + parse_var : identifier -> 'a; + parse_ref : extended_global_reference -> 'a; fail : qualid -> 'a * int list; } @@ -253,18 +256,18 @@ let translate_qualid act qid = (* Is it a bound variable? *) try match repr_qualid qid with - | [],s -> act.parse_var (string_of_id s), [] + | [],id -> act.parse_var id, [] | _ -> raise Not_found with Not_found -> (* Is it a global reference? *) try let ref = Nametab.locate qid in - act.parse_ref ref, implicits_of_global ref + act.parse_ref (TrueGlobal ref), implicits_of_global ref with Not_found -> (* Is it a reference to a syntactic definition? *) try let sp = Syntax_def.locate_syntactic_definition qid in - act.parse_syn sp, [] + act.parse_ref (SyntacticDef sp), [] with Not_found -> act.fail qid @@ -274,7 +277,7 @@ let rawconstr_of_var env vars loc s = try ast_to_var env vars loc s with Not_found -> - error_var_not_found_loc loc CCI (id_of_string s) + Pretype_errors.error_var_not_found_loc loc CCI (id_of_string s) let rawconstr_of_qualid env vars loc qid = (* Is it a bound variable? *) @@ -564,7 +567,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar = (* Globalization of AST quotations (mainly used to get statically *) (* bound idents in grammar or pretty-printing rules) *) (**************************************************************************) - +(* (* A brancher ultérieurement sur Termast.ast_of_ref *) let ast_of_ref loc = function | ConstRef sp -> Node (loc, "CONST", [path_section loc sp]) @@ -572,11 +575,19 @@ let ast_of_ref loc = function Node (loc, "MUTCONSTRUCT", [path_section loc sp; num i; num j]) | IndRef (sp, i) -> Node (loc, "MUTIND", [path_section loc sp; num i]) | VarRef sp -> failwith "ast_of_ref: TODO" +*) +let ast_of_ref_loc loc ref = set_loc loc (Termast.ast_of_ref ref) let ast_of_syndef loc sp = Node (loc, "SYNCONST", [path_section loc sp]) -let ast_of_var env ast s = - if isMeta s or Idset.mem (id_of_string s) env then ast +let ast_of_extended_ref_loc loc = function + | TrueGlobal ref -> ast_of_ref_loc loc ref + | SyntacticDef sp -> ast_of_syndef loc sp + +let ast_of_extended_ref = ast_of_extended_ref_loc dummy_loc + +let ast_of_var env ast id = + if isMeta (string_of_id id) or Idset.mem id env then ast else raise Not_found let ast_hole = Node (dummy_loc, "ISEVAR", []) @@ -606,8 +617,7 @@ let ast_adjust_consts sigma = and adjust_qualid env loc ast sp = let act = { parse_var = ast_of_var env ast; - parse_ref = ast_of_ref loc; - parse_syn = ast_of_syndef loc; + parse_ref = ast_of_extended_ref_loc loc; fail = warning_globalize ast } in fst (translate_qualid act sp) diff --git a/parsing/astterm.mli b/parsing/astterm.mli index 613b3c1240..cf2cbfd510 100644 --- a/parsing/astterm.mli +++ b/parsing/astterm.mli @@ -65,7 +65,7 @@ val globalize_ast : Coqast.t -> Coqast.t (* This transforms args of a qualid keyword into a qualified ident *) (* it does no relocation *) -val interp_qualid : Coqast.t list -> qualid +val interp_qualid : Coqast.t list -> Nametab.qualid (* Translation rules from V6 to V7: diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml index b0a7f3a8a2..d7e8efa20f 100644 --- a/parsing/coqlib.ml +++ b/parsing/coqlib.ml @@ -6,6 +6,7 @@ open Names open Term open Declare open Pattern +open Nametab let nat_path = make_path ["Coq";"Init";"Datatypes"] (id_of_string "nat") CCI let myvar_path = diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 34d3d29803..1e45d0ea25 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -15,6 +15,7 @@ open Declare open Impargs open Libobject open Printer +open Nametab let print_basename sp = pr_global (ConstRef sp) diff --git a/parsing/pretty.mli b/parsing/pretty.mli index c224bc20db..7b4ea47e83 100644 --- a/parsing/pretty.mli +++ b/parsing/pretty.mli @@ -21,15 +21,15 @@ val print_context : bool -> Lib.library_segment -> std_ppcmds val print_library_entry : bool -> (section_path * Lib.node) -> std_ppcmds val print_full_context : unit -> std_ppcmds val print_full_context_typ : unit -> std_ppcmds -val print_sec_context : qualid -> std_ppcmds -val print_sec_context_typ : qualid -> std_ppcmds +val print_sec_context : Nametab.qualid -> std_ppcmds +val print_sec_context_typ : Nametab.qualid -> std_ppcmds val print_val : env -> unsafe_judgment -> std_ppcmds val print_type : env -> unsafe_judgment -> std_ppcmds val print_eval : 'a reduction_function -> env -> unsafe_judgment -> std_ppcmds val print_mutual : section_path -> std_ppcmds -val print_name : qualid -> std_ppcmds -val print_opaque_name : qualid -> std_ppcmds +val print_name : Nametab.qualid -> std_ppcmds +val print_opaque_name : Nametab.qualid -> std_ppcmds val print_local_context : unit -> std_ppcmds (*i diff --git a/parsing/printer.ml b/parsing/printer.ml index d0535fbac5..a325f1a8b1 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -21,8 +21,8 @@ let pr_global ref = (* Il est important de laisser le let-in, car les streams s'évaluent paresseusement : il faut forcer l'évaluation pour capturer l'éventuelle levée d'une exception (le cas échoit dans le debugger) *) - let qid = Global.qualid_of_global ref in - [< 'sTR (string_of_qualid qid) >] + let s = Global.string_of_global ref in + [< 'sTR s >] let global_const_name sp = try pr_global (ConstRef sp) diff --git a/parsing/termast.ml b/parsing/termast.ml index 5b0675d979..56f330b749 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -15,6 +15,7 @@ open Coqast open Ast open Rawterm open Pattern +open Nametab (* In this file, we translate rawconstr to ast, in order to print constr *) diff --git a/parsing/termast.mli b/parsing/termast.mli index 1d6ee2208a..35a7349d8f 100644 --- a/parsing/termast.mli +++ b/parsing/termast.mli @@ -27,7 +27,7 @@ val ast_of_existential : env -> existential -> Coqast.t val ast_of_constructor : env -> constructor -> Coqast.t val ast_of_inductive : env -> inductive -> Coqast.t val ast_of_ref : global_reference -> Coqast.t -val ast_of_qualid : qualid -> Coqast.t +val ast_of_qualid : Nametab.qualid -> Coqast.t (* For debugging *) val print_implicits : bool ref |