summaryrefslogtreecommitdiff
path: root/parsing/pptactic.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pptactic.ml')
-rw-r--r--parsing/pptactic.ml59
1 files changed, 32 insertions, 27 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 6a7ae9bc..3b433498 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pptactic.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: pptactic.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
open Pp
open Names
@@ -21,6 +21,7 @@ open Pattern
open Ppextend
open Ppconstr
open Printer
+open Termops
let pr_global x = Nametab.pr_global_env Idset.empty x
@@ -79,7 +80,7 @@ let pr_and_short_name pr (c,_) = pr c
let pr_or_by_notation f = function
| AN v -> f v
- | ByNotation (_,s) -> str s
+ | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
let pr_located pr (loc,x) = pr x
@@ -122,10 +123,6 @@ let pr_with_constr prc = function
| None -> mt ()
| Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
-let pr_with_names = function
- | None -> mt ()
- | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
-
let rec pr_message_token prid = function
| MsgString s -> qs s
| MsgInt n -> int n
@@ -140,6 +137,8 @@ let out_bindings = function
| ExplicitBindings l -> ExplicitBindings (List.map (fun (loc,id,c) -> (loc,id,snd c)) l)
| NoBindings -> NoBindings
+let if_pattern_ident b pr c = (if b then str "?" else mt()) ++ pr c
+
let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argument) =
match Genarg.genarg_tag x with
| BoolArgType -> str (if out_gen rawwit_bool x then "true" else "false")
@@ -148,7 +147,7 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu
| StringArgType -> str "\"" ++ str (out_gen rawwit_string x) ++ str "\""
| PreIdentArgType -> str (out_gen rawwit_pre_ident x)
| IntroPatternArgType -> pr_intro_pattern (out_gen rawwit_intro_pattern x)
- | IdentArgType -> pr_id (out_gen rawwit_ident x)
+ | IdentArgType b -> if_pattern_ident b pr_id (out_gen rawwit_ident x)
| VarArgType -> pr_located pr_id (out_gen rawwit_var x)
| RefArgType -> prref (out_gen rawwit_ref x)
| SortArgType -> pr_rawsort (out_gen rawwit_sort x)
@@ -179,7 +178,7 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu
x)
| ExtraArgType s ->
try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x
- with Not_found -> str " [no printer for " ++ str s ++ str "] "
+ with Not_found -> str "[no printer for " ++ str s ++ str "]"
let rec pr_glob_generic prc prlc prtac x =
@@ -190,7 +189,7 @@ let rec pr_glob_generic prc prlc prtac x =
| StringArgType -> str "\"" ++ str (out_gen globwit_string x) ++ str "\""
| PreIdentArgType -> str (out_gen globwit_pre_ident x)
| IntroPatternArgType -> pr_intro_pattern (out_gen globwit_intro_pattern x)
- | IdentArgType -> pr_id (out_gen globwit_ident x)
+ | IdentArgType b -> if_pattern_ident b pr_id (out_gen globwit_ident x)
| VarArgType -> pr_located pr_id (out_gen globwit_var x)
| RefArgType -> pr_or_var (pr_located pr_global) (out_gen globwit_ref x)
| SortArgType -> pr_rawsort (out_gen globwit_sort x)
@@ -224,7 +223,7 @@ let rec pr_glob_generic prc prlc prtac x =
x)
| ExtraArgType s ->
try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x
- with Not_found -> str "[no printer for " ++ str s ++ str "] "
+ with Not_found -> str "[no printer for " ++ str s ++ str "]"
open Closure
@@ -236,7 +235,7 @@ let rec pr_generic prc prlc prtac x =
| StringArgType -> str "\"" ++ str (out_gen wit_string x) ++ str "\""
| PreIdentArgType -> str (out_gen wit_pre_ident x)
| IntroPatternArgType -> pr_intro_pattern (out_gen wit_intro_pattern x)
- | IdentArgType -> pr_id (out_gen wit_ident x)
+ | IdentArgType b -> if_pattern_ident b pr_id (out_gen wit_ident x)
| VarArgType -> pr_id (out_gen wit_var x)
| RefArgType -> pr_global (out_gen wit_ref x)
| SortArgType -> pr_sort (out_gen wit_sort x)
@@ -326,9 +325,6 @@ let pr_evaluable_reference_env env = function
| EvalConstRef sp ->
Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.ConstRef sp)
-let pr_inductive env ind =
- Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.IndRef ind)
-
let pr_quantified_hypothesis = function
| AnonHyp n -> int n
| NamedHyp id -> pr_id id
@@ -376,9 +372,9 @@ let pr_with_inversion_names = function
| None -> mt ()
| Some ipat -> pr_as_intro_pattern ipat
-let pr_with_names = function
- | _,IntroAnonymous -> mt ()
- | ipat -> pr_as_intro_pattern ipat
+let pr_as_ipat = function
+ | None -> mt ()
+ | Some ipat -> pr_as_intro_pattern ipat
let pr_as_name = function
| Anonymous -> mt ()
@@ -397,7 +393,7 @@ let pr_assertion _prlc prc ipat c = match ipat with
spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
*)
| ipat ->
- spc() ++ prc c ++ pr_with_names ipat
+ spc() ++ prc c ++ pr_as_ipat ipat
let pr_assumption prlc prc ipat c = match ipat with
(* Use this "optimisation" or use only the general case ?
@@ -405,7 +401,7 @@ let pr_assumption prlc prc ipat c = match ipat with
spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
*)
| ipat ->
- spc() ++ prc c ++ pr_with_names ipat
+ spc() ++ prc c ++ pr_as_ipat ipat
let pr_by_tactic prt = function
| TacId [] -> mt ()
@@ -426,6 +422,10 @@ let pr_simple_clause pr_id = function
| [] -> mt ()
| l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
+let pr_in_hyp_as pr_id = function
+ | None -> mt ()
+ | Some (id,ipat) -> pr_simple_clause pr_id [id] ++ pr_as_ipat ipat
+
let pr_clauses pr_id = function
| { onhyps=None; concl_occs=occs } ->
if occs = no_occurrences_expr then pr_in (str " * |-")
@@ -468,12 +468,16 @@ let pr_lazy lz = if lz then str "lazy" else mt ()
let pr_match_pattern pr_pat = function
| Term a -> pr_pat a
- | Subterm (None,a) -> str "context [" ++ pr_pat a ++ str "]"
- | Subterm (Some id,a) ->
- str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+ | Subterm (b,None,a) -> (if b then str"appcontext [" else str "context [") ++ pr_pat a ++ str "]"
+ | Subterm (b,Some id,a) ->
+ (if b then str"appcontext " else str "context ") ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
-let pr_match_hyps pr_pat (Hyp (nal,mp)) =
- pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
+let pr_match_hyps pr_pat = function
+ | Hyp (nal,mp) ->
+ pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
+ | Def (nal,mv,mp) ->
+ pr_lname nal ++ str ":=" ++ pr_match_pattern pr_pat mv
+ ++ str ":" ++ pr_match_pattern pr_pat mp
let pr_match_rule m pr pr_pat = function
| Pat ([],mp,t) when m ->
@@ -695,10 +699,11 @@ and pr_atom1 = function
| TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
| TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
| TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c)
- | TacApply (a,ev,cb) ->
+ | TacApply (a,ev,cb,inhyp) ->
hov 1 ((if a then mt() else str "simple ") ++
str (with_evars ev "apply") ++ spc () ++
- prlist_with_sep pr_coma pr_with_bindings cb)
+ prlist_with_sep pr_coma pr_with_bindings cb ++
+ pr_in_hyp_as pr_ident inhyp)
| TacElim (ev,cb,cbo) ->
hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++
pr_opt pr_eliminator cbo)
@@ -1019,7 +1024,7 @@ let rec raw_printers =
(pr_raw_tactic_level,
drop_env pr_constr_expr,
drop_env pr_lconstr_expr,
- pr_lpattern_expr,
+ pr_lconstr_pattern_expr,
drop_env (pr_or_by_notation pr_reference),
drop_env (pr_or_by_notation pr_reference),
pr_reference,
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-05 19:34:15 +0000