From 8e82c4096357355a148705341742702ff285f72a Mon Sep 17 00:00:00 2001 From: barras Date: Wed, 28 Mar 2001 15:11:26 +0000 Subject: amelioration de la structure des univers elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/astterm.mli | 7 ++++--- parsing/esyntax.ml | 5 +++-- parsing/extend.ml4 | 13 ++++++++----- parsing/extend.mli | 5 ++--- parsing/pcoq.ml4 | 2 ++ parsing/pretty.ml | 12 +++++++----- parsing/pretty.mli | 4 ++-- 7 files changed, 28 insertions(+), 20 deletions(-) (limited to 'parsing') diff --git a/parsing/astterm.mli b/parsing/astterm.mli index 6f7d400fe..744e75fa5 100644 --- a/parsing/astterm.mli +++ b/parsing/astterm.mli @@ -27,9 +27,10 @@ val interp_type : 'a evar_map -> env -> Coqast.t -> types val interp_sort : Coqast.t -> sorts val interp_openconstr : - 'a evar_map -> env -> Coqast.t -> (int * constr) list * constr + 'a evar_map -> env -> Coqast.t -> (existential * constr) list * constr val interp_casted_openconstr : - 'a evar_map -> env -> Coqast.t -> constr -> (int * constr) list * constr + 'a evar_map -> env -> Coqast.t -> constr -> + (existential * constr) list * constr (* [interp_type_with_implicits] extends [interp_type] by allowing implicits arguments in the ``rel'' part of [env]; the extra @@ -54,7 +55,7 @@ val interp_constr_gen : val interp_openconstr_gen : 'a evar_map -> env -> (identifier * constr) list -> (int * constr) list -> Coqast.t -> constr option - -> (int * constr) list * constr + -> (existential * constr) list * constr (*Interprets constr patterns according to a list of instantiations (variables)*) diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml index ba6e8614e..250000b74 100644 --- a/parsing/esyntax.ml +++ b/parsing/esyntax.ml @@ -154,10 +154,11 @@ let print_syntax_entry whatfor sub_pr env se = | PH(e,externpr,reln) -> let printer = match externpr with (* May branch to an other printer *) - | Some (c,entry_prec) -> + | Some c -> (try (* Test for a primitive printer *) (Ppprim.map c) (sub_pr whatfor (Some(rule_prec,reln))) - with Not_found -> token_printer (sub_pr c entry_prec)) + with Not_found -> + token_printer (sub_pr c (Some(rule_prec,reln)))) | None -> token_printer (sub_pr whatfor (Some(rule_prec,reln))) in printer (Ast.pat_sub Ast.dummy_loc env e) diff --git a/parsing/extend.ml4 b/parsing/extend.ml4 index f5969f4b2..d3c0eecba 100644 --- a/parsing/extend.ml4 +++ b/parsing/extend.ml4 @@ -186,8 +186,8 @@ let interp_grammar_command univ astl = (* Converting and checking pretty-printing command *) -type parenRelation = L | E | Any type precedence = int * int * int +type parenRelation = L | E | Any | Prec of precedence let compare_prec (a1,b1,c1) (a2,b2,c2) = match (a1=a2),(b1=b2),(c1=c2) with @@ -200,6 +200,7 @@ let tolerable_prec oparent_prec_reln (_,child_prec) = match oparent_prec_reln with | Some ((_,pprec), L) -> (compare_prec child_prec pprec) < 0 | Some ((_,pprec), E) -> (compare_prec child_prec pprec) <= 0 + | Some (_, Prec level) -> (compare_prec child_prec level) <= 0 | _ -> true type ppbox = @@ -212,7 +213,7 @@ type ppbox = type tolerability = (string * precedence) * parenRelation type unparsing_hunk = - | PH of Ast.pat * (string * tolerability option) option * parenRelation + | PH of Ast.pat * string option * parenRelation | RO of string | UNP_BOX of ppbox * unparsing_hunk list | UNP_BRK of int * int @@ -242,13 +243,15 @@ let prec_of_ast = function | ast -> invalid_arg_loc (Ast.loc ast,"Syntaxext.prec_of_ast") let extern_of_ast loc = function - | [Str(_,ppextern)] -> Some (ppextern,None) - | [Str(_,ppextern);p] -> Some (ppextern,Some ((ppextern,prec_of_ast p),Any)) + | [Str(_,ppextern)] -> (ppextern, Any) + | [Str(_,ppextern);p] -> + (ppextern, Prec (prec_of_ast p)) | _ -> invalid_arg_loc (loc,"Syntaxext.extern_of_ast") let rec unparsing_hunk_of_ast vars = function | Node(_, "PH", [e; Node (loc,"EXTERN", ext_args)]) -> - PH (Ast.val_of_ast vars e, extern_of_ast loc ext_args, Any) + let (ppex, rel) = extern_of_ast loc ext_args in + PH (Ast.val_of_ast vars e, Some ppex, rel) | Node(loc, "PH", [e; Id(_,pr)]) -> let reln = (match pr with diff --git a/parsing/extend.mli b/parsing/extend.mli index 00ffb2097..da77f531d 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -51,8 +51,7 @@ val interp_grammar_command : string -> Coqast.t list -> grammar_command (* Dealing with precedences *) type precedence = int * int * int - -type parenRelation = L | E | Any +type parenRelation = L | E | Any | Prec of precedence (* Checks if the precedence of the parent printer (None means the highest precedence), and the child's one, follow the given @@ -72,7 +71,7 @@ type ppbox = | PpTB type unparsing_hunk = - | PH of Ast.pat * (string * tolerability option) option * parenRelation + | PH of Ast.pat * string option * parenRelation | RO of string | UNP_BOX of ppbox * unparsing_hunk list | UNP_BRK of int * int diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 6792ae044..3b9708dc6 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -414,6 +414,8 @@ open Constr open Tactic open Vernac +(* current file and toplevel/vernac.ml *) + let define_quotation default s e = (if default then GEXTEND Gram diff --git a/parsing/pretty.ml b/parsing/pretty.ml index ef46a0399..ff17c3b74 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -391,15 +391,17 @@ let print_sec_context sec = print_context true (read_sec_context sec) let print_sec_context_typ sec = print_context false (read_sec_context sec) -let print_val env {uj_val=trm;uj_type=typ} = - print_typed_value_in_env env (trm,typ) +let print_judgment env {uj_val=trm;uj_type=typ} = + print_typed_value_in_env env (trm, typ) -let print_type env {uj_val=trm;uj_type=typ} = - print_typed_value_in_env env (trm, type_app (nf_betaiota env Evd.empty) typ) +let print_safe_judgment env j = + let trm = Safe_typing.j_val j in + let typ = Safe_typing.j_type j in + print_typed_value_in_env env (trm, typ) let print_eval red_fun env {uj_val=trm;uj_type=typ} = let ntrm = red_fun env Evd.empty trm in - [< 'sTR " = "; print_type env {uj_val = ntrm; uj_type = typ} >] + [< 'sTR " = "; print_judgment env {uj_val = ntrm; uj_type = typ} >] let print_name qid = try diff --git a/parsing/pretty.mli b/parsing/pretty.mli index c5071367b..c3bf165b1 100644 --- a/parsing/pretty.mli +++ b/parsing/pretty.mli @@ -30,8 +30,8 @@ val print_full_context : unit -> std_ppcmds val print_full_context_typ : unit -> 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_judgment : env -> unsafe_judgment -> std_ppcmds +val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds val print_eval : 'a reduction_function -> env -> unsafe_judgment -> std_ppcmds val print_mutual : section_path -> std_ppcmds -- cgit v1.2.3