aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/esyntax.ml24
-rw-r--r--parsing/printer.ml18
-rw-r--r--parsing/termast.ml41
-rw-r--r--parsing/termast.mli1
-rwxr-xr-xsyntax/PPConstr.v9
5 files changed, 62 insertions, 31 deletions
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index c5be89d926..ef9b4feecc 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -17,13 +17,20 @@ open Extend
type key =
| Cst of string list (* keys for global constants rules *)
+ | Ind of string list * int
+ | Cstr of (string list * int) * int
| Nod of string (* keys for other constructed asts rules *)
| Oth (* key for other syntax rules *)
| All (* key for catch-all rules (i.e. with a pattern such as $x .. *)
let ast_keys = function
- | Node(_,"APPLIST",(Node(_,"CONST",(Path (_,sl,_))::_))::_) ->
+ | Node(_,"APPLIST", Node(_,"CONST", [Path (_,sl,_)]) ::_) ->
[Cst sl; Nod "APPLIST"; All]
+ | Node(_,"APPLIST", Node(_,"MUTIND", [Path (_,sl,_); Num (_,tyi)]) ::_) ->
+ [Ind (sl,tyi); Nod "APPLIST"; All]
+ | Node(_,"APPLIST", Node(_,"MUTCONSTRUCT",
+ [Path (_,sl,_); Num (_,tyi); Num (_,i)]) ::_) ->
+ [Cstr ((sl,tyi),i); Nod "APPLIST"; All]
| Node(_,s,_) -> [Nod s; All]
| _ -> [Oth; All]
@@ -31,8 +38,19 @@ let spat_key astp =
match astp with
| Pnode("APPLIST",
Pcons(Pnode("CONST",
- Pcons(Pquote(Path (_,sl,s)),_)),
- _)) -> Cst sl
+ Pcons(Pquote(Path (_,sl,s)),_)), _))
+ -> Cst sl
+ | Pnode("APPLIST",
+ Pcons(Pnode("MUTIND",
+ Pcons(Pquote(Path (_,sl,s)),
+ Pcons(Pquote(Num (_,tyi)),_))), _))
+ -> Ind (sl,tyi)
+ | Pnode("APPLIST",
+ Pcons(Pnode("MUTCONSTRUCT",
+ Pcons(Pquote(Path (_,sl,s)),
+ Pcons(Pquote(Num (_,tyi)),
+ Pcons(Pquote(Num (_,i)),_)))), _))
+ -> Cstr ((sl,tyi),i)
| Pnode(na,_) -> Nod na
| Pquote ast -> List.hd (ast_keys ast)
| Pmeta _ -> All
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 5fa57bd39e..bad9c38667 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -16,23 +16,37 @@ let emacs_str s = if !Options.print_emacs then s else ""
let dfltpr ast = [< 'sTR"#GENTERM " ; Ast.print_ast ast >];;
-(*
let section_path sl s =
let sl = List.rev sl in
make_path (List.tl sl) (id_of_string (List.hd sl)) (kind_of_string s)
+(*
let pr_global k oper =
let id = id_of_global oper in
[< 'sTR (string_of_id id) >]
*)
+let pr_qualified_path sp id =
+ if Nametab.sp_of_id (kind_of_path sp) id = sp then [<'sTR(string_of_id id)>]
+ else [<'sTR(string_of_path (make_path (dirpath sp) id (kind_of_path sp)))>]
+
let globpr gt = match gt with
| Nvar(_,s) -> [< 'sTR s >]
+ | Node(_,"EVAR", [Num (_,ev)]) -> [< 'sTR ("?" ^ (string_of_int ev)) >]
+ | Node(_,"CONST",[Path(_,sl,s)]) ->
+ let sp = section_path sl s in
+ pr_qualified_path sp (basename (section_path sl s))
+ | Node(_,"MUTIND",[Path(_,sl,s); Num(_,tyi)]) ->
+ let sp = section_path sl s in
+ pr_qualified_path sp (Global.id_of_global (MutInd (sp,tyi)))
+ | Node(_,"MUTCONSTRUCT",[Path(_,sl,s); Num(_,tyi); Num(_,i)]) ->
+ let sp = section_path sl s in
+ pr_qualified_path sp (Global.id_of_global (MutConstruct ((sp,tyi),i)))
(*
| Node(_,"EVAR", (Num (_,ev))::_) ->
if !print_arguments then dfltpr gt
else pr_existential (ev,[])
- | Node(_,"CONST",(Path(_,sl,s))::_) ->
+ | Node(_,"CONST"),(Path(_,sl,s))::_) ->
if !print_arguments then dfltpr gt
else pr_constant (section_path sl s,[])
| Node(_,"MUTIND",(Path(_,sl,s))::(Num(_,tyi))::_) ->
diff --git a/parsing/termast.ml b/parsing/termast.ml
index f92f9cef42..f4b7071932 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -24,6 +24,9 @@ open Pattern
(* This governs printing of local context of references *)
let print_arguments = ref false
+(* If true, prints local context of evars, whatever print_arguments *)
+let print_evar_arguments = ref false
+
(* This forces printing of cast nodes *)
let print_casts = ref false
@@ -83,44 +86,32 @@ let stringopt_of_name = function
| Name id -> Some (string_of_id id)
| Anonymous -> None
-let ast_of_qualified sp id =
- if Nametab.sp_of_id (kind_of_path sp) id = sp then nvar (string_of_id id)
- else nvar (string_of_path sp)
-
let ast_of_constant_ref (sp,ids) =
- if !print_arguments then
- ope("CONST", (path_section dummy_loc sp)::(List.map ast_of_ident ids))
- else
- try ast_of_qualified sp (basename sp)
- with Not_found -> nvar (string_of_path sp) (* May happen while debugging *)
+ let a = ope("CONST", [path_section dummy_loc sp]) in
+ if !print_arguments then ope("INSTANCE",a::(List.map ast_of_ident ids))
+ else a
let ast_of_constant (ev,ids) = ast_of_constant_ref (ev,ids_of_ctxt ids)
let ast_of_existential_ref (ev,ids) =
- if !print_arguments then
- ope("EVAR", (num ev)::(List.map ast_of_ident ids))
- else nvar ("?" ^ string_of_int ev)
+ let a = ope("EVAR", [num ev]) in
+ if !print_arguments or !print_evar_arguments then
+ ope("INSTANCE",a::(List.map ast_of_ident ids))
+ else a
let ast_of_existential (ev,ids) = ast_of_existential_ref (ev,ids_of_ctxt ids)
let ast_of_constructor_ref (((sp,tyi),n) as cstr_sp,ids) =
- if !print_arguments then
- ope("MUTCONSTRUCT",
- (path_section dummy_loc sp)::(num tyi)::(num n)
- ::(List.map ast_of_ident ids))
- else
- try ast_of_qualified sp (Global.id_of_global (MutConstruct cstr_sp))
- with Not_found -> nvar (string_of_path sp) (* May happen while debugging *)
+ let a = ope("MUTCONSTRUCT",[path_section dummy_loc sp; num tyi; num n]) in
+ if !print_arguments then ope("INSTANCE",a::(List.map ast_of_ident ids))
+ else a
let ast_of_constructor (ev,ids) = ast_of_constructor_ref (ev,ids_of_ctxt ids)
let ast_of_inductive_ref ((sp,tyi) as ind_sp,ids) =
- if !print_arguments then
- ope("MUTIND",
- (path_section dummy_loc sp)::(num tyi)::(List.map ast_of_ident ids))
- else
- try ast_of_qualified sp (Global.id_of_global (MutInd ind_sp))
- with Not_found -> nvar (string_of_path sp) (* May happen while debugging *)
+ let a = ope("MUTIND", [path_section dummy_loc sp; num tyi]) in
+ if !print_arguments then ope("INSTANCE",a::(List.map ast_of_ident ids))
+ else a
let ast_of_inductive (ev,ctxt) = ast_of_inductive_ref (ev,ids_of_ctxt ctxt)
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 064dc8c25b..e0b8069d93 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -34,6 +34,7 @@ val ast_of_inductive : inductive -> Coqast.t
val print_implicits : bool ref
val print_casts : bool ref
val print_arguments : bool ref
+val print_evar_arguments : bool ref
val print_coercions : bool ref
val with_casts : ('a -> 'b) -> 'a -> 'b
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index 4980afd587..ad74cd462e 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -35,12 +35,19 @@ Syntax constr
| type [(TYPE)] -> ["Type"]
| type_sp [(TYPE ($PATH $sp) ($NUM $n))] -> ["Type"]
(* Note: Atomic constants (Nvar, CONST, MUTIND, MUTCONSTRUCT) are printed in
- typing/printer to deal with the duality CCI/FW *)
+ Printer to know if they must be qualified or not (and previously to
+ deal with the duality CCI/FW) *)
| evar [<< ? >>] -> ["?"]
| meta [(META ($NUM $n))] -> [ "?" $n ]
| implicit [(IMPLICIT)] -> ["<Implicit>"]
| indice [(REL ($NUM $n))] -> ["<Unbound ref: " $n ">"]
+ | instantiation [(INSTANCE $a ($LIST $l))] ->
+ [ $a "{" (CONTEXT ($LIST $l)) "}"]
+ | instantiation_nil [(CONTEXT)] -> [ ]
+ | instantiation_one [(CONTEXT $a)] -> [ $a ]
+ | instantiation_many [(CONTEXT $a $b ($LIST $l))] ->
+ [ (CONTEXT $b ($LIST $l)) ";" $a ]
;
(* Things parsed in command1 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:52:35 +0000