diff options
Diffstat (limited to 'translate/pptacticnew.ml')
| -rw-r--r-- | translate/pptacticnew.ml | 612 |
1 files changed, 266 insertions, 346 deletions
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 1cab30aa0..b80ae29d6 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -11,33 +11,17 @@ open Pp open Names open Nameops +open Environ open Util open Extend -open Ppconstr +open Ppextend +open Ppconstrnew open Tacexpr open Rawterm open Topconstr open Genarg open Libnames -(* Extensions *) -let prtac_tab = Hashtbl.create 17 - -let declare_extra_tactic_pprule s f g = - Hashtbl.add prtac_tab s (f,g) - -let genarg_pprule = ref Stringmap.empty - -let declare_extra_genarg_pprule (rawwit, f) (wit, g) = - let s = match unquote wit with - | ExtraArgType s -> s - | _ -> error - "Can declare a pretty-printing rule only for extra argument types" - in - let f x = f (out_gen rawwit x) in - let g x = g (out_gen wit x) in - genarg_pprule := Stringmap.add s (f,g) !genarg_pprule - (* [pr_rawtac] is here to cheat with ML typing system, gen_tactic_expr is polymorphic but with some occurrences of its instance raw_tactic_expr in it; then pr_tactic should be @@ -47,10 +31,10 @@ let declare_extra_genarg_pprule (rawwit, f) (wit, g) = let pr_rawtac = ref (fun _ -> failwith "Printer for raw tactic expr is not defined" - : raw_tactic_expr -> std_ppcmds) + : env -> raw_tactic_expr -> std_ppcmds) let pr_rawtac0 = ref (fun _ -> failwith "Printer for raw tactic expr is not defined" - : raw_tactic_expr -> std_ppcmds) + : env -> raw_tactic_expr -> std_ppcmds) let pr_arg pr x = spc () ++ pr x @@ -66,8 +50,6 @@ let pr_or_meta pr = function | AI x -> pr x | _ -> failwith "pr_hyp_location: unexpected quotation meta-variable" -let pr_casted_open_constr = pr_constr - let pr_quantified_hypothesis = function | AnonHyp n -> int n | NamedHyp id -> pr_id id @@ -78,16 +60,24 @@ let pr_binding prc = function | NamedHyp id, c -> hov 1 (pr_id id ++ str ":=" ++ cut () ++ prc c) | AnonHyp n, c -> hov 1 (int n ++ str ":=" ++ cut () ++ prc c) -let pr_bindings prc = function +let pr_esubst prc l = + let pr_qhyp = function + (_,AnonHyp n,c) -> int n ++ str":=" ++ prc c + | (_,NamedHyp id,c) -> pr_id id ++ str":=" ++ prc c in + prlist_with_sep spc pr_qhyp l + +let pr_bindings_gen for_ex prc = function | ImplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - prlist_with_sep spc prc l + spc () ++ (if for_ex then mt() else str "with ") ++ + hv 0 (prlist_with_sep spc prc l) | ExplicitBindings l -> - str"TODO" (* brk (1,1) ++ str "with" ++ brk (1,1) ++ - prlist_with_sep spc (pr_binding prc) l *) + spc () ++ (if for_ex then mt() else str "with ") ++ + hv 0 (pr_esubst prc l) | NoBindings -> mt () -let pr_with_bindings prc (c,bl) = prc c ++ hv 0 (pr_bindings prc bl) +let pr_bindings prc = pr_bindings_gen false prc + +let pr_with_bindings prc (c,bl) = prc c ++ pr_bindings prc bl let pr_with_names = function | [] -> mt () @@ -106,7 +96,7 @@ let rec pr_intro_pattern = function let pr_hyp_location pr_id = function | InHyp id -> spc () ++ pr_id id - | InHypType id -> spc () ++ str "(Type of " ++ pr_id id ++ str ")" + | InHypType id -> spc () ++ str "(type of " ++ pr_id id ++ str ")" let pr_clause pr_id = function | [] -> mt () @@ -138,30 +128,35 @@ let pr_match_hyps = function let pr_match_rule m pr = function | Pat ([],mp,t) when m -> str "[" ++ pr_match_pattern mp ++ str "]" - ++ spc () ++ str "->" ++ brk (1,2) ++ pr t + ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t | Pat (rl,mp,t) -> - str "[" ++ prlist_with_sep pr_semicolon pr_match_hyps rl ++ spc () ++ - str "|-" ++ spc () ++ pr_match_pattern mp ++ spc () ++ str "]" ++ - spc () ++ str "->" ++ brk (1,2) ++ pr t - | All t -> str "_" ++ spc () ++ str "->" ++ brk (1,2) ++ pr t + str "[" ++ prlist_with_sep (fun () -> str",") pr_match_hyps rl ++ + spc () ++ str "|-" ++ spc () ++ pr_match_pattern mp ++ spc () ++ + str "] =>" ++ brk (1,4) ++ pr t + | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t let pr_funvar = function | None -> spc () ++ str "()" | Some id -> spc () ++ pr_id id let pr_let_clause k pr = function - | ((_,id),None,t) -> hv 0(str k ++ pr_id id ++ str " =" ++ brk (1,1) ++ pr t) - | ((_,id),Some c,t) -> str "TODO(LETCLAUSE)" + | ((_,id),None,t) -> + hov 0 (str k ++ pr_id id ++ str " :=" ++ brk (1,1) ++ + pr (TacArg t)) + | ((_,id),Some c,t) -> + hv 0 (str k ++ pr_id id ++ str" :" ++ brk(1,2) ++ + pr_may_eval pr_constr pr_constr c ++ + str " :=" ++ brk (1,1) ++ pr (TacArg t)) let pr_let_clauses pr = function | hd::tl -> hv 0 (pr_let_clause "let " pr hd ++ spc () ++ - prlist_with_sep spc (pr_let_clause "and " pr) tl) + prlist_with_sep spc (pr_let_clause "with " pr) tl) | [] -> anomaly "LetIn must declare at least one binding" let pr_rec_clause pr ((_,id),(l,t)) = - pr_id id ++ prlist pr_funvar l ++ str "->" ++ spc () ++ pr t + pr_id id ++ prlist pr_funvar l ++ str "=>" ++ spc () ++ pr t let pr_rec_clauses pr l = prlist_with_sep (fun () -> fnl () ++ str "and ") (pr_rec_clause pr) l @@ -170,7 +165,7 @@ let pr_hintbases = function | None -> spc () ++ str "with *" | Some [] -> mt () | Some l -> - spc () ++ str "with" ++ hv 0 (prlist (fun s -> spc () ++ str s) l) + spc () ++ hov 2 (str "with" ++ prlist (fun s -> spc () ++ str s) l) let pr_autoarg_adding = function | [] -> mt () @@ -186,410 +181,335 @@ let pr_autoarg_usingTDB = function | true -> spc () ++ str "Using TDB" | false -> mt () -let rec pr_rawgen prtac x = - match Genarg.genarg_tag x with - | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false") - | IntArgType -> pr_arg int (out_gen rawwit_int x) - | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen rawwit_int_or_var x) - | StringArgType -> spc () ++ str "\"" ++ str (out_gen rawwit_string x) ++ str "\"" - | PreIdentArgType -> pr_arg str (out_gen rawwit_pre_ident x) - | IdentArgType -> pr_arg pr_id (out_gen rawwit_ident x) - | RefArgType -> pr_arg pr_reference (out_gen rawwit_ref x) - | SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x) - | ConstrArgType -> pr_arg pr_constr (out_gen rawwit_constr x) - | ConstrMayEvalArgType -> - pr_arg (pr_may_eval pr_constr) (out_gen rawwit_constr_may_eval x) - | QuantHypArgType -> - pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x) - | RedExprArgType -> - pr_arg (pr_red_expr (pr_constr,pr_metanum pr_reference)) (out_gen rawwit_red_expr x) - | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x) - | CastedOpenConstrArgType -> - pr_arg pr_casted_open_constr (out_gen rawwit_casted_open_constr x) - | ConstrWithBindingsArgType -> - pr_arg (pr_with_bindings pr_constr) - (out_gen rawwit_constr_with_bindings x) - | List0ArgType _ -> - hov 0 (fold_list0 (fun x a -> pr_rawgen prtac x ++ a) x (mt())) - | List1ArgType _ -> - hov 0 (fold_list1 (fun x a -> pr_rawgen prtac x ++ a) x (mt())) - | OptArgType _ -> hov 0 (fold_opt (pr_rawgen prtac) (mt()) x) - | PairArgType _ -> - hov 0 - (fold_pair - (fun a b -> pr_rawgen prtac a ++ spc () ++ pr_rawgen prtac b) - x) - | ExtraArgType s -> - try fst (Stringmap.find s !genarg_pprule) x - with Not_found -> str " [no printer for " ++ str s ++ str "] " - -let rec pr_raw_tacarg_using_rule pr_gen = function - | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_raw_tacarg_using_rule pr_gen (l,al) - | Egrammar.TacNonTerm _ :: l, a :: al -> pr_gen a ++ pr_raw_tacarg_using_rule pr_gen (l,al) - | [], [] -> mt () - | _ -> failwith "Inconsistent arguments of extended tactic" - -let pr_raw_extend prt s l = - try - let (s,pl) = fst (Hashtbl.find prtac_tab s) l in - str s ++ pr_raw_tacarg_using_rule (pr_rawgen prt) (pl,l) - with Not_found -> - str "TODO(" ++ str s ++ prlist (pr_rawgen prt) l ++ str ")" - open Closure -let pr_evaluable_reference = function +let pr_evaluable_reference vars = function | EvalVarRef id -> pr_id id - | EvalConstRef sp -> pr_global (Libnames.ConstRef sp) - -let pr_inductive ind = pr_global (Libnames.IndRef ind) - -let rec pr_generic prtac x = - match Genarg.genarg_tag x with - | BoolArgType -> pr_arg str (if out_gen wit_bool x then "true" else "false") - | IntArgType -> pr_arg int (out_gen wit_int x) - | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen wit_int_or_var x) - | StringArgType -> spc () ++ str "\"" ++ str (out_gen wit_string x) ++ str "\"" - | PreIdentArgType -> pr_arg str (out_gen wit_pre_ident x) - | IdentArgType -> pr_arg pr_id (out_gen wit_ident x) - | RefArgType -> pr_arg pr_global (out_gen wit_ref x) - | SortArgType -> pr_arg Printer.prterm (Term.mkSort (out_gen wit_sort x)) - | ConstrArgType -> pr_arg Printer.prterm (out_gen wit_constr x) - | ConstrMayEvalArgType -> - pr_arg Printer.prterm (out_gen wit_constr_may_eval x) - | QuantHypArgType -> - pr_arg pr_quantified_hypothesis (out_gen wit_quant_hyp x) - | RedExprArgType -> - pr_arg (pr_red_expr (Printer.prterm,pr_evaluable_reference)) (out_gen wit_red_expr x) - | TacticArgType -> pr_arg prtac (out_gen wit_tactic x) - | CastedOpenConstrArgType -> - pr_arg Printer.prterm (snd (out_gen wit_casted_open_constr x)) - | ConstrWithBindingsArgType -> - pr_arg (pr_with_bindings Printer.prterm) - (out_gen wit_constr_with_bindings x) - | List0ArgType _ -> - hov 0 (fold_list0 (fun x a -> pr_generic prtac x ++ a) x (mt())) - | List1ArgType _ -> - hov 0 (fold_list1 (fun x a -> pr_generic prtac x ++ a) x (mt())) - | OptArgType _ -> hov 0 (fold_opt (pr_generic prtac) (mt()) x) - | PairArgType _ -> - hov 0 - (fold_pair - (fun a b -> pr_generic prtac a ++ spc () ++ pr_generic prtac b) - x) - | ExtraArgType s -> - try snd (Stringmap.find s !genarg_pprule) x - with Not_found -> str "[no printer for " ++ str s ++ str "]" - -let rec pr_tacarg_using_rule prt = function - | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule prt (l,al) - | Egrammar.TacNonTerm _ :: l, a :: al -> pr_generic prt a ++ pr_tacarg_using_rule prt (l,al) - | [], [] -> mt () - | _ -> failwith "Inconsistent arguments of extended tactic" - -let pr_extend prt s l = - try - let (s,pl) = snd (Hashtbl.find prtac_tab s) l in - str s ++ pr_tacarg_using_rule prt (pl,l) - with Not_found -> - str s ++ prlist (pr_generic prt) l - -let make_pr_tac (pr_constr,pr_cst,pr_ind,pr_ident,pr_extend) = - -let pr_bindings = pr_bindings pr_constr in -let pr_with_bindings = pr_with_bindings pr_constr in -let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in -let pr_constrarg c = spc () ++ pr_constr c in + | EvalConstRef sp -> pr_global vars (Libnames.ConstRef sp) + +let pr_inductive vars ind = pr_global vars (Libnames.IndRef ind) + +let make_pr_tac (pr_constr,pr_lconstr,pr_cst,pr_ind,pr_ident,pr_extend) = + +let pr_bindings env = pr_bindings (pr_constr env) in +let pr_ex_bindings env = pr_bindings_gen true (pr_constr env) in +let pr_with_bindings env = pr_with_bindings (pr_constr env) in +let pr_eliminator env cb = str "using" ++ pr_arg (pr_with_bindings env) cb in +let pr_constrarg env c = spc () ++ pr_constr env c in +let pr_lconstrarg env c = spc () ++ pr_lconstr env c in let pr_intarg n = spc () ++ int n in (* Printing tactics as arguments *) -let rec pr_atom0 = function - | TacIntroPattern [] -> str "Intros" - | TacIntroMove (None,None) -> str "Intro" - | TacAssumption -> str "Assumption" - | TacAnyConstructor None -> str "Constructor" - | TacTrivial (Some []) -> str "Trivial" - | TacAuto (None,Some []) -> str "Auto" - | TacAutoTDB None -> str "AutoTDB" - | TacDestructConcl -> str "DConcl" - | TacReflexivity -> str "Reflexivity" - | TacSymmetry -> str "Symmetry" - | t -> str "(" ++ pr_atom1 t ++ str ")" +let rec pr_atom0 env = function + | TacIntroPattern [] -> str "intros" + | TacIntroMove (None,None) -> str "intro" + | TacAssumption -> str "assumption" + | TacAnyConstructor None -> str "constructor" + | TacTrivial (Some []) -> str "trivial" + | TacAuto (None,Some []) -> str "auto" + | TacAutoTDB None -> str "autotdb" + | TacDestructConcl -> str "dconcl" + | TacReflexivity -> str "reflexivity" + | TacSymmetry -> str "symmetry" + | t -> str "(" ++ pr_atom1 env t ++ str ")" (* Main tactic printer *) -and pr_atom1 = function - | TacExtend (_,s,l) -> pr_extend !pr_rawtac s l - | TacAlias (s,l,_) -> pr_extend !pr_rawtac s (List.map snd l) +and pr_atom1 env = function + | TacExtend (_,s,l) -> + pr_extend (Ppconstrnew.pr_constr_env env) (!pr_rawtac env) s l + | TacAlias (s,l,_) -> + pr_extend (Ppconstrnew.pr_constr_env env) (!pr_rawtac env) s + (List.map snd l) (* Basic tactics *) - | TacIntroPattern [] as t -> pr_atom0 t + | TacIntroPattern [] as t -> pr_atom0 env t | TacIntroPattern (_::_ as p) -> - hov 1 (str "Intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p) + hov 1 (str "intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p) | TacIntrosUntil h -> - hv 1 (str "Intros until" ++ pr_arg pr_quantified_hypothesis h) - | TacIntroMove (None,None) as t -> pr_atom0 t - | TacIntroMove (Some id1,None) -> str "Intro " ++ pr_id id1 + hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h) + | TacIntroMove (None,None) as t -> pr_atom0 env t + | TacIntroMove (Some id1,None) -> str "intro " ++ pr_id id1 | TacIntroMove (ido1,Some (_,id2)) -> hov 1 - (str "Intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++ pr_id id2) - | TacAssumption as t -> pr_atom0 t - | TacExact c -> hov 1 (str "Exact" ++ pr_arg pr_constr c) - | TacApply cb -> hov 1 (str "Apply" ++ spc () ++ pr_with_bindings cb) + (str "intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++ pr_id id2) + | TacAssumption as t -> pr_atom0 env t + | TacExact c -> hov 1 (str "exact" ++ pr_lconstrarg env c) + | TacApply cb -> hov 1 (str "apply " ++ pr_with_bindings env cb) | TacElim (cb,cbo) -> - hov 1 (str "Elim" ++ pr_arg pr_with_bindings cb ++ - pr_opt pr_eliminator cbo) - | TacElimType c -> hov 1 (str "ElimType" ++ pr_arg pr_constr c) - | TacCase cb -> hov 1 (str "Case" ++ spc () ++ pr_with_bindings cb) - | TacCaseType c -> hov 1 (str "CaseType" ++ pr_arg pr_constr c) - | TacFix (ido,n) -> hov 1 (str "Fix" ++ pr_opt pr_id ido ++ pr_intarg n) + hov 1 (str "elim" ++ pr_arg (pr_with_bindings env) cb ++ + pr_opt (pr_eliminator env) cbo) + | TacElimType c -> hov 1 (str "elimtype" ++ pr_lconstrarg env c) + | TacCase cb -> hov 1 (str "case" ++ spc () ++ pr_with_bindings env cb) + | TacCaseType c -> hov 1 (str "CaseType" ++ pr_lconstrarg env c) + | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n) | TacMutualFix (id,n,l) -> - hov 1 (str "Cofix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc () ++ + hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc () ++ hov 0 (str "with" ++ brk (1,1) ++ prlist_with_sep spc (fun (id,n,c) -> - spc () ++ pr_id id ++ pr_intarg n ++ pr_arg pr_constr c) + spc () ++ pr_id id ++ pr_intarg n ++ pr_constrarg env c) l)) - | TacCofix ido -> hov 1 (str "Cofix" ++ pr_opt pr_id ido) + | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido) | TacMutualCofix (id,l) -> - hov 1 (str "Cofix" ++ spc () ++ pr_id id ++ spc () ++ + hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc () ++ hov 0 (str "with" ++ brk (1,1) ++ - prlist (fun (id,c) -> spc () ++ pr_id id ++ pr_arg pr_constr c) + prlist (fun (id,c) -> spc () ++ pr_id id ++ pr_constrarg env c) l)) - | TacCut c -> hov 1 (str "Cut" ++ pr_arg pr_constr c) + | TacCut c -> hov 1 (str "cut" ++ pr_lconstrarg env c) | TacTrueCut (None,c) -> - hov 1 (str "Assert" ++ pr_arg pr_constr c) + hov 1 (str "assert" ++ pr_lconstrarg env c) | TacTrueCut (Some id,c) -> - hov 1 (str "Assert" ++ spc () ++ pr_id id ++ str ":" ++ pr_constr c) + hov 1 (str "assert" ++ spc () ++ pr_id id ++ str ":" ++ + pr_lconstr env c) | TacForward (false,na,c) -> - hov 1 (str "Assert" ++ pr_arg pr_name na ++ str ":=" ++ pr_constr c) + hov 1 (str "assert" ++ pr_arg pr_name na ++ str ":=" ++ + pr_lconstr env c) | TacForward (true,na,c) -> - hov 1 (str "Pose" ++ pr_arg pr_name na ++ str ":=" ++ pr_constr c) + hov 1 (str "pose" ++ pr_arg pr_name na ++ str ":=" ++ + pr_lconstr env c) | TacGeneralize l -> - hov 1 (str "Generalize" ++ spc () ++ prlist_with_sep spc pr_constr l) + hov 1 (str "generalize" ++ spc () ++ + prlist_with_sep spc (pr_constr env) l) | TacGeneralizeDep c -> - hov 1 (str "Generalize" ++ spc () ++ str "Dependent" ++ spc () ++ - pr_constr c) + hov 1 (str "generalize" ++ spc () ++ str "dependent" ++ + pr_lconstrarg env c) | TacLetTac (id,c,cl) -> - hov 1 (str "LetTac" ++ spc () ++ pr_id id ++ str ":=" ++ - pr_constr c ++ pr_clause_pattern pr_ident cl) + hov 1 (str "lettac" ++ spc () ++ pr_id id ++ str ":=" ++ + pr_constr env c ++ pr_clause_pattern pr_ident cl) | TacInstantiate (n,c) -> - hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c) + hov 1 (str "instantiate" ++ pr_arg int n ++ pr_lconstrarg env c) (* Derived basic tactics *) | TacOldInduction h -> - hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h) + hov 1 (str "induction" ++ pr_arg pr_quantified_hypothesis h) | TacNewInduction (h,e,ids) -> - hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h ++ - pr_opt pr_eliminator e ++ pr_with_names ids) + hov 1 (str "newinduction" ++ spc () ++ + pr_induction_arg (pr_lconstr env) h ++ + pr_opt (pr_eliminator env) e ++ pr_with_names ids) | TacOldDestruct h -> - hov 1 (str "Destruct" ++ pr_arg pr_quantified_hypothesis h) + hov 1 (str "destruct" ++ pr_arg pr_quantified_hypothesis h) | TacNewDestruct (h,e,ids) -> - hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h ++ - pr_opt pr_eliminator e ++ pr_with_names ids) + hov 1 (str "newdestruct" ++ spc () ++ + pr_induction_arg (pr_lconstr env) h ++ + pr_opt (pr_eliminator env) e ++ pr_with_names ids) | TacDoubleInduction (h1,h2) -> hov 1 - (str "Double Induction" ++ + (str "double induction" ++ pr_arg pr_quantified_hypothesis h1 ++ pr_arg pr_quantified_hypothesis h2) | TacDecomposeAnd c -> - hov 1 (str "Decompose Record" ++ pr_arg pr_constr c) + hov 1 (str "decompose record" ++ pr_lconstrarg env c) | TacDecomposeOr c -> - hov 1 (str "Decompose Sum" ++ pr_arg pr_constr c) + hov 1 (str "decompose sum" ++ pr_lconstrarg env c) | TacDecompose (l,c) -> - hov 1 (str "Decompose" ++ spc () ++ - hov 0 (str "[" ++ prlist_with_sep spc (pr_metanum pr_ind) l - ++ str "]")) + let vars = Termops.vars_of_env env in + hov 1 (str "decompose" ++ spc () ++ + hov 0 (str "[" ++ prlist_with_sep spc (pr_metanum (pr_ind vars)) l + ++ str "]" ++ pr_lconstrarg env c)) | TacSpecialize (n,c) -> - hov 1 (str "Specialize" ++ pr_opt int n ++ pr_with_bindings c) + hov 1 (str "specialize " ++ pr_opt int n ++ pr_with_bindings env c) | TacLApply c -> - hov 1 (str "LApply" ++ pr_constr c) + hov 1 (str "lapply" ++ pr_lconstrarg env c) (* Automation tactics *) - | TacTrivial (Some []) as x -> pr_atom0 x - | TacTrivial db -> hov 0 (str "Trivial" ++ pr_hintbases db) - | TacAuto (None,Some []) as x -> pr_atom0 x - | TacAuto (n,db) -> hov 0 (str "Auto" ++ pr_opt int n ++ pr_hintbases db) - | TacAutoTDB None as x -> pr_atom0 x - | TacAutoTDB (Some n) -> hov 0 (str "AutoTDB" ++ spc () ++ int n) - | TacDestructHyp (true,(_,id)) -> hov 0 (str "CDHyp" ++ spc () ++ pr_id id) - | TacDestructHyp (false,(_,id)) -> hov 0 (str "DHyp" ++ spc () ++ pr_id id) - | TacDestructConcl as x -> pr_atom0 x + | TacTrivial (Some []) as x -> pr_atom0 env x + | TacTrivial db -> hov 0 (str "trivial" ++ pr_hintbases db) + | TacAuto (None,Some []) as x -> pr_atom0 env x + | TacAuto (n,db) -> hov 0 (str "auto" ++ pr_opt int n ++ pr_hintbases db) + | TacAutoTDB None as x -> pr_atom0 env x + | TacAutoTDB (Some n) -> hov 0 (str "autotdb" ++ spc () ++ int n) + | TacDestructHyp (true,(_,id)) -> hov 0 (str "cdhyp" ++ spc () ++ pr_id id) + | TacDestructHyp (false,(_,id)) -> hov 0 (str "dhyp" ++ spc () ++ pr_id id) + | TacDestructConcl as x -> pr_atom0 env x | TacSuperAuto (n,l,b1,b2) -> - hov 1 (str "SuperAuto" ++ pr_opt int n ++ pr_autoarg_adding l ++ + hov 1 (str "superauto" ++ pr_opt int n ++ pr_autoarg_adding l ++ pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2) | TacDAuto (n,p) -> - hov 1 (str "Auto" ++ pr_opt int n ++ str "Decomp" ++ pr_opt int p) + hov 1 (str "auto" ++ pr_opt int n ++ str "decomp" ++ pr_opt int p) (* Context management *) | TacClear l -> - hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l) + hov 1 (str "clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l) | TacClearBody l -> - hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l) + hov 1 (str "clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l) | TacMove (b,(_,id1),(_,id2)) -> (* Rem: only b = true is available for users *) assert b; hov 1 - (str "Move" ++ brk (1,1) ++ pr_id id1 ++ spc () ++ + (str "move" ++ brk (1,1) ++ pr_id id1 ++ spc () ++ str "after" ++ brk (1,1) ++ pr_id id2) | TacRename ((_,id1),(_,id2)) -> hov 1 - (str "Rename" ++ brk (1,1) ++ pr_id id1 ++ spc () ++ + (str "rename" ++ brk (1,1) ++ pr_id id1 ++ spc () ++ str "into" ++ brk (1,1) ++ pr_id id2) (* Constructors *) - | TacLeft l -> hov 1 (str "Left" ++ pr_bindings l) - | TacRight l -> hov 1 (str "Right" ++ pr_bindings l) - | TacSplit l -> hov 1 (str "Split" ++ pr_bindings l) + | TacLeft l -> hov 1 (str "left" ++ pr_bindings env l) + | TacRight l -> hov 1 (str "right" ++ pr_bindings env l) + | TacSplit (false,l) -> hov 1 (str "split" ++ pr_bindings env l) + | TacSplit (true,l) -> hov 1 (str "exists" ++ pr_ex_bindings env l) | TacAnyConstructor (Some t) -> - hov 1 (str "Constructor" ++ pr_arg !pr_rawtac0 t) - | TacAnyConstructor None as t -> pr_atom0 t + hov 1 (str "constructor" ++ pr_arg (!pr_rawtac0 env) t) + | TacAnyConstructor None as t -> pr_atom0 env t | TacConstructor (n,l) -> - hov 1 (str "Constructor" ++ pr_or_meta pr_intarg n ++ pr_bindings l) + hov 1 (str "constructor" ++ pr_or_meta pr_intarg n ++ + pr_bindings env l) (* Conversion *) | TacReduce (r,h) -> - hov 1 (pr_red_expr (pr_constr,pr_cst) r ++ pr_clause pr_ident h) - | TacChange (_,c,h) -> (* A Verifier *) - hov 1 (str "Change" ++ brk (1,1) ++ pr_constr c ++ pr_clause pr_ident h) + hov 1 (pr_red_expr (pr_constr env,pr_lconstr env,pr_cst) r ++ + pr_clause pr_ident h) + | TacChange (occ,c,h) -> (* A Verifier *) + hov 1 (str "change" ++ brk (1,1) ++ + (match occ with + None -> mt() + | Some(ocl,c1) -> + hov 1 (prlist (fun i -> int i ++ spc()) ocl ++ + pr_constr env c1) ++ spc() ++ str "with ") ++ + pr_constr env c ++ pr_clause pr_ident h) (* Equivalence relations *) - | (TacReflexivity | TacSymmetry) as x -> pr_atom0 x - | TacTransitivity c -> str "Transitivity" ++ pr_arg pr_constr c - -and pr_tactic_seq_body tl = + | (TacReflexivity | TacSymmetry) as x -> pr_atom0 env x + | TacTransitivity c -> str "transitivity" ++ pr_lconstrarg env c in + +let ltop = (5,E) in +let lseq = 5 in +let ltactical = 3 in +let lorelse = 2 in +let llet = 1 in +let lfun = 1 in +let labstract = 1 in +let lmatch = 1 in +let latom = 0 in +let lcall = 1 in +let leval = 1 in +let ltatom = 1 in + +let pr_seq_body pr tl = hv 0 (str "[ " ++ - prlist_with_sep (fun () -> spc () ++ str "| ") prtac tl ++ str " ]") - - (* Strictly closed atomic tactic expressions *) -and pr0 = function - | TacFirst tl -> str "First" ++ spc () ++ pr_tactic_seq_body tl - | TacSolve tl -> str "Solve" ++ spc () ++ pr_tactic_seq_body tl - | TacId -> str "Idtac" - | TacFail 0 -> str "Fail" - | TacAtom (_,t) -> pr_atom0 t - | TacArg c -> pr_tacarg c - | t -> str "(" ++ prtac t ++ str ")" - - (* Semi-closed atomic tactic expressions *) -and pr1 = function - | TacAtom (_,t) -> pr_atom1 t - | TacFail n -> str "Fail " ++ int n - | t -> pr0 t - - (* Orelse tactic expressions (printed as if parsed associating on the right - though the semantics is purely associative) *) -and pr2 = function - | TacOrelse (t1,t2) -> - hov 1 (pr1 t1 ++ str " Orelse" ++ brk (1,1) ++ pr3 t2) - | t -> pr1 t - - (* Non closed prefix tactic expressions *) -and pr3 = function - | TacTry t -> hov 1 (str "Try" ++ spc () ++ pr3 t) - | TacDo (n,t) -> hov 1 (str "Do " ++ int n ++ spc () ++ pr3 t) - | TacRepeat t -> hov 1 (str "Repeat" ++ spc () ++ pr3 t) - | TacProgress t -> hov 1 (str "Progress" ++ spc () ++ pr3 t) - | TacInfo t -> hov 1 (str "Info" ++ spc () ++ pr3 t) - | t -> pr2 t - -and pr4 = function - | t -> pr3 t - - (* THEN and THENS tactic expressions (printed as if parsed - associating on the left though the semantics is purely associative) *) -and pr5 = function - | TacThens (t,tl) -> - hov 1 (pr5 t ++ spc () ++ str "&" ++ spc () ++ pr_tactic_seq_body tl) - | TacThen (t1,t2) -> - hov 1 (pr5 t1 ++ spc () ++ str "&" ++ spc () ++ pr4 t2) - | t -> pr4 t - - (* Ltac tactic expressions *) -and pr6 = function - |(TacAtom _ - | TacThen _ - | TacThens _ - | TacFirst _ - | TacSolve _ - | TacTry _ - | TacOrelse _ - | TacDo _ - | TacRepeat _ - | TacProgress _ - | TacId - | TacFail _ - | TacInfo _) as t -> pr5 t - - | TacAbstract (t,None) -> str "Abstract " ++ pr6 t + prlist_with_sep (fun () -> spc () ++ str "| ") (pr ltop) tl ++ + str " ]") in + +let rec pr_tac env inherited tac = + let (strm,prec) = match tac with + | TacAbstract (t,None) -> + str "abstract " ++ pr_tac env (labstract,E) t, labstract | TacAbstract (t,Some s) -> hov 0 - (str "Abstract " ++ pr6 t ++ spc () ++ str "using" ++ spc () ++ pr_id s) + (str "abstract " ++ pr_tac env ltop t ++ spc () ++ + str "using " ++ pr_id s), + labstract | TacLetRecIn (l,t) -> hv 0 - (str "let rec " ++ pr_rec_clauses prtac l ++ - spc () ++ str "in" ++ fnl () ++ prtac t) + (str "let rec " ++ pr_rec_clauses (pr_tac env ltop) l ++ str " in" ++ + fnl () ++ pr_tac env (llet,E) t), + llet | TacLetIn (llc,u) -> v 0 - (hv 0 (pr_let_clauses pr_tacarg0 llc ++ spc () ++ str "in") ++ fnl () ++ prtac u) - | TacLetCut llc -> - pr_let_clauses pr_tacarg0 - (List.map (fun (id,c,t) -> ((dummy_loc,id),Some c,t)) llc) - ++ fnl () + (hv 0 (pr_let_clauses (pr_tac env ltop) llc ++ str " in") ++ + fnl () ++ pr_tac env (llet,E) u), + llet + | TacLetCut llc -> assert false | TacMatch (t,lrul) -> - hov 0 (str "match" ++ spc () ++ pr_may_eval Ppconstr.pr_constr t ++ spc() - ++ str "with" + hov 0 (str "match " ++ + pr_may_eval (Ppconstrnew.pr_constr_env env) + (Ppconstrnew.pr_lconstr_env env) t + ++ str " with" ++ prlist - (fun r -> fnl () ++ str "|" ++ spc () ++ pr_match_rule true prtac r) - lrul) + (fun r -> fnl () ++ str "| " ++ + pr_match_rule true (pr_tac env ltop) r) + lrul + ++ fnl() ++ str "end"), + lmatch | TacMatchContext (lr,lrul) -> hov 0 ( - str (if lr then "Match Reverse Context With" else "Match Context With") + str (if lr then "match reverse context with" else "match context with") ++ prlist - (fun r -> fnl () ++ str "|" ++ spc () ++ pr_match_rule false prtac r) - lrul) + (fun r -> fnl () ++ str "| " ++ + pr_match_rule false (pr_tac env ltop) r) + lrul + ++ fnl() ++ str "end"), + lmatch | TacFun (lvar,body) -> - hov 0 (str "fun" ++ - prlist pr_funvar lvar ++ spc () ++ str "->" ++ spc () ++ prtac body) - | TacArg c -> pr_tacarg c + hov 2 (str "fun" ++ + prlist pr_funvar lvar ++ str " =>" ++ spc () ++ + pr_tac env (lfun,E) body), + lfun + | TacThens (t,tl) -> + hov 1 (pr_tac env (lseq,E) t ++ str " &" ++ spc () ++ + pr_seq_body (pr_tac env) tl), + lseq + | TacThen (t1,t2) -> + hov 1 (pr_tac env (lseq,E) t1 ++ str " &" ++ spc () ++ + pr_tac env (lseq,L) t2), + lseq + | TacTry t -> + hov 1 (str "try" ++ spc () ++ pr_tac env (ltactical,E) t), + ltactical + | TacDo (n,t) -> + hov 1 (str "do " ++ int n ++ spc () ++ pr_tac env (ltactical,E) t), + ltactical + | TacRepeat t -> + hov 1 (str "repeat" ++ spc () ++ pr_tac env (ltactical,E) t), + ltactical + | TacProgress t -> + hov 1 (str "progress" ++ spc () ++ pr_tac env (ltactical,E) t), + ltactical + | TacInfo t -> + hov 1 (str "info" ++ spc () ++ pr_tac env (ltactical,E) t), + ltactical + | TacOrelse (t1,t2) -> + hov 1 (pr_tac env (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++ + pr_tac env (lorelse,E) t2), + lorelse + | TacFail 0 -> str "fail", latom + | TacFail n -> str "fail " ++ int n, latom + | TacFirst tl -> + str "first" ++ spc () ++ pr_seq_body (pr_tac env) tl, llet + | TacSolve tl -> + str "solve" ++ spc () ++ pr_seq_body (pr_tac env) tl, llet + | TacId -> str "idtac", latom + | TacAtom (_,t) -> hov 1 (pr_atom1 env t), ltatom + | TacArg(Tacexp e) -> !pr_rawtac0 env e, latom + | TacArg(ConstrMayEval (ConstrTerm c)) -> str "'" ++ pr_constr env c, latom + | TacArg(ConstrMayEval c) -> + pr_may_eval (pr_constr env) (pr_lconstr env) c, leval + | TacArg(Integer n) -> int n, latom + | TacArg(TacCall(_,f,l)) -> + hov 1 (pr_reference f ++ spc () ++ + prlist_with_sep spc (pr_tacarg env) l), + lcall + | TacArg a -> pr_tacarg env a, latom + in + if prec_less prec inherited then strm + else str"(" ++ strm ++ str")" -and pr_tacarg0 = function +and pr_tacarg env = function | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>") | MetaNumArg (_,n) -> str ("?" ^ string_of_int n ) | MetaIdArg (_,s) -> str ("$" ^ s) | TacVoid -> str "()" | Reference r -> pr_reference r - | ConstrMayEval (ConstrTerm c) -> str "'" ++ pr_constr c - | ConstrMayEval c -> pr_may_eval pr_constr c - | Integer n -> int n - | (TacCall _ | Tacexp _) as t -> str "(" ++ pr_tacarg1 t ++ str ")" - -and pr_tacarg1 = function - | TacCall (_,f,l) -> - hov 0 (pr_reference f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l) - | Tacexp t -> !pr_rawtac t - | t -> pr_tacarg0 t + | ConstrMayEval (ConstrTerm c) -> pr_constr env c + | (ConstrMayEval _|TacCall _|Tacexp _|Integer _) as a -> + str "'" ++ pr_tac env (latom,E) (TacArg a) -and pr_tacarg x = pr_tacarg1 x - -and prtac x = pr6 x - -in (prtac,pr0,pr_match_rule) +in ((fun env -> pr_tac env ltop), + (fun env -> pr_tac env (latom,E)), + pr_match_rule) let (pr_raw_tactic,pr_raw_tactic0,pr_match_rule) = make_pr_tac - (Ppconstrnew.pr_constr, + (Ppconstrnew.pr_constr_env, + Ppconstrnew.pr_lconstr_env, pr_metanum pr_reference, - pr_reference, + (fun _ -> pr_reference), pr_or_meta (fun (loc,id) -> pr_id id), - pr_raw_extend) + Pptactic.pr_raw_extend) let _ = pr_rawtac := pr_raw_tactic let _ = pr_rawtac0 := pr_raw_tactic0 -let (pr_tactic,_,_) = - make_pr_tac - (Printer.prterm, - pr_evaluable_reference, - pr_inductive, - pr_id, - pr_extend) +let pr_gen env = + Pptactic.pr_rawgen (Ppconstrnew.pr_constr_env env) + (pr_raw_tactic env) |