diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pptactic.ml | 25 | ||||
| -rw-r--r-- | parsing/pptactic.mli | 11 | ||||
| -rw-r--r-- | parsing/printer.ml | 6 | ||||
| -rw-r--r-- | parsing/printer.mli | 6 |
4 files changed, 36 insertions, 12 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index b6c38cf93..d4fa5163e 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -133,6 +133,11 @@ let rec pr_message_token prid = function let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s) +let out_bindings = function + | ImplicitBindings l -> ImplicitBindings (List.map snd l) + | ExplicitBindings l -> ExplicitBindings (List.map (fun (loc,id,c) -> (loc,id,snd c)) l) + | NoBindings -> NoBindings + let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argument) = match Genarg.genarg_tag x with | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false") @@ -244,10 +249,12 @@ let rec pr_generic prc prlc prtac x = pr_arg (pr_red_expr (prc,prlc,pr_evaluable_reference)) (out_gen wit_red_expr x) | OpenConstrArgType b -> pr_arg prc (snd (out_gen (wit_open_constr_gen b) x)) - | ConstrWithBindingsArgType -> - pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x) + | ConstrWithBindingsArgType -> + let (c,b) = out_gen wit_constr_with_bindings x in + pr_arg (pr_with_bindings prc prlc) (c,out_bindings b) | BindingsArgType -> - pr_arg (pr_bindings_no_with prc prlc) (out_gen wit_bindings x) + pr_arg (pr_bindings_no_with prc prlc) + (out_bindings (out_gen wit_bindings x)) | List0ArgType _ -> hov 0 (fold_list0 (fun x a -> pr_generic prc prlc prtac x ++ a) x (mt())) | List1ArgType _ -> @@ -283,7 +290,7 @@ let pr_raw_extend prc prlc prtac = let pr_glob_extend prc prlc prtac = pr_extend_gen (pr_glob_generic prc prlc prtac) let pr_extend prc prlc prtac = - pr_extend_gen (pr_generic prc prlc prtac) + pr_extend_gen (pr_generic (fun c -> prc (Evd.empty,c)) (fun c -> prlc (Evd.empty,c)) prtac) (**********************************************************************) (* The tactic printer *) @@ -966,12 +973,12 @@ let strip_prod_binders_rawterm n (ty,_) = | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty -let strip_prod_binders_constr n ty = +let strip_prod_binders_constr n (sigma,ty) = let rec strip_ty acc n ty = - if n=0 then (List.rev acc, ty) else + if n=0 then (List.rev acc, (sigma,ty)) else match Term.kind_of_term ty with Term.Prod(na,a,b) -> - strip_ty (([dummy_loc,na],a)::acc) (n-1) b + strip_ty (([dummy_loc,na],(sigma,a))::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty @@ -1017,8 +1024,8 @@ and pr_glob_match_rule env t = let typed_printers = (pr_glob_tactic_level, - pr_constr_env, - pr_lconstr_env, + pr_open_constr_env, + pr_open_lconstr_env, pr_lconstr_pattern, pr_evaluable_reference_env, pr_inductive, diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index cfa035b16..31a626cea 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -17,6 +17,7 @@ open Topconstr open Rawterm open Ppextend open Environ +open Evd val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds @@ -45,7 +46,7 @@ type 'a extra_genarg_printer = val declare_extra_genarg_pprule : ('c raw_abstract_argument_type * 'c raw_extra_genarg_printer) -> ('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) -> - ('b closed_abstract_argument_type * 'b extra_genarg_printer) -> unit + ('b typed_abstract_argument_type * 'b extra_genarg_printer) -> unit type grammar_terminals = string option list @@ -73,9 +74,9 @@ val pr_glob_extend: string -> glob_generic_argument list -> std_ppcmds val pr_extend : - (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> + (open_constr -> std_ppcmds) -> (open_constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> int -> - string -> closed_generic_argument list -> std_ppcmds + string -> typed_generic_argument list -> std_ppcmds val pr_raw_tactic : env -> raw_tactic_expr -> std_ppcmds @@ -88,3 +89,7 @@ val pr_tactic : env -> Proof_type.tactic_expr -> std_ppcmds val pr_hintbases : string list option -> std_ppcmds val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds + +val pr_bindings : + ('constr -> std_ppcmds) -> + ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds diff --git a/parsing/printer.ml b/parsing/printer.ml index df078f302..307e0af23 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -48,10 +48,16 @@ let pr_lconstr_env_at_top env = pr_lconstr_core true env let pr_lconstr_env env = pr_lconstr_core false env let pr_constr_env env = pr_constr_core false env +let pr_open_lconstr_env env (_,c) = pr_lconstr_env env c +let pr_open_constr_env env (_,c) = pr_constr_env env c + (* NB do not remove the eta-redexes! Global.env() has side-effects... *) let pr_lconstr t = pr_lconstr_env (Global.env()) t let pr_constr t = pr_constr_env (Global.env()) t +let pr_open_lconstr (_,c) = pr_lconstr c +let pr_open_constr (_,c) = pr_constr c + let pr_type_core at_top env t = pr_constr_expr (extern_type at_top env t) let pr_ltype_core at_top env t = diff --git a/parsing/printer.mli b/parsing/printer.mli index 4e09e0251..1f3f2b0fb 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -35,6 +35,12 @@ val pr_lconstr : constr -> std_ppcmds val pr_constr_env : env -> constr -> std_ppcmds val pr_constr : constr -> std_ppcmds +val pr_open_constr_env : env -> open_constr -> std_ppcmds +val pr_open_constr : open_constr -> std_ppcmds + +val pr_open_lconstr_env : env -> open_constr -> std_ppcmds +val pr_open_lconstr : open_constr -> std_ppcmds + val pr_ltype_env_at_top : env -> types -> std_ppcmds val pr_ltype_env : env -> types -> std_ppcmds val pr_ltype : types -> std_ppcmds |