diff options
Diffstat (limited to 'parsing/ppdecl_proof.ml')
| -rw-r--r-- | parsing/ppdecl_proof.ml | 122 |
1 files changed, 61 insertions, 61 deletions
diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml index 3b9a002f..abcbedfa 100644 --- a/parsing/ppdecl_proof.ml +++ b/parsing/ppdecl_proof.ml @@ -6,45 +6,45 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppdecl_proof.ml 10739 2008-04-01 14:45:20Z herbelin $ *) +(* $Id$ *) -open Util +open Util open Pp open Decl_expr -open Names +open Names open Nameops let pr_constr = Printer.pr_constr_env let pr_tac = Pptactic.pr_glob_tactic -let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr +let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr let pr_label = function Anonymous -> mt () - | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () + | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () let pr_justification_items env = function Some [] -> mt () - | Some (_::_ as l) -> - spc () ++ str "by" ++ spc () ++ + | Some (_::_ as l) -> + spc () ++ str "by" ++ spc () ++ prlist_with_sep (fun () -> str ",") (pr_constr env) l | None -> spc () ++ str "by *" let pr_justification_method env = function None -> mt () - | Some tac -> + | Some tac -> spc () ++ str "using" ++ spc () ++ pr_tac env tac -let pr_statement pr_it env st = +let pr_statement pr_it env st = pr_label st.st_label ++ pr_it env st.st_it let pr_or_thesis pr_this env = function Thesis Plain -> str "thesis" - | Thesis (For id) -> - str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id + | Thesis (For id) -> + str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id | This c -> pr_this env c -let pr_cut pr_it env c = - hov 1 (pr_it env c.cut_stat) ++ +let pr_cut pr_it env c = + hov 1 (pr_it env c.cut_stat) ++ pr_justification_items env c.cut_by ++ pr_justification_method env c.cut_using @@ -54,45 +54,45 @@ let type_or_thesis = function let _I x = x -let rec print_hyps pconstr gtyp env sep _be _have hyps = +let rec print_hyps pconstr gtyp env sep _be _have hyps = let pr_sep = if sep then str "and" ++ spc () else mt () in - match hyps with - (Hvar _ ::_) as rest -> - spc () ++ pr_sep ++ str _have ++ + match hyps with + (Hvar _ ::_) as rest -> + spc () ++ pr_sep ++ str _have ++ print_vars pconstr gtyp env false _be _have rest - | Hprop st :: rest -> + | Hprop st :: rest -> begin let nenv = match st.st_label with Anonymous -> env | Name id -> Environ.push_named (id,None,gtyp st.st_it) env in - spc() ++ pr_sep ++ pr_statement pconstr env st ++ + spc() ++ pr_sep ++ pr_statement pconstr env st ++ print_hyps pconstr gtyp nenv true _be _have rest end | [] -> mt () and print_vars pconstr gtyp env sep _be _have vars = match vars with - Hvar st :: rest -> + Hvar st :: rest -> begin - let nenv = + let nenv = match st.st_label with Anonymous -> anomaly "anonymous variable" | Name id -> Environ.push_named (id,None,st.st_it) env in - let pr_sep = if sep then pr_coma () else mt () in + let pr_sep = if sep then pr_comma () else mt () in spc() ++ pr_sep ++ pr_statement pr_constr env st ++ print_vars pconstr gtyp nenv true _be _have rest end | (Hprop _ :: _) as rest -> - let _st = if _be then - str "be such that" - else + let _st = if _be then + str "be such that" + else str "such that" in spc() ++ _st ++ print_hyps pconstr gtyp env false _be _have rest | [] -> mt () -let pr_suffices_clause env (hyps,c) = +let pr_suffices_clause env (hyps,c) = print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++ str "to show" ++ spc () ++ pr_or_thesis pr_constr env c @@ -110,68 +110,68 @@ let pr_side = function let rec pr_bare_proof_instr _then _thus env = function | Pescape -> str "escape" - | Pthen i -> pr_bare_proof_instr true _thus env i - | Pthus i -> pr_bare_proof_instr _then true env i + | Pthen i -> pr_bare_proof_instr true _thus env i + | Pthus i -> pr_bare_proof_instr _then true env i | Phence i -> pr_bare_proof_instr true true env i - | Pcut c -> + | Pcut c -> begin match _then,_thus with - false,false -> str "have" ++ spc () ++ + false,false -> str "have" ++ spc () ++ pr_cut (pr_statement (pr_or_thesis pr_constr)) env c - | false,true -> str "thus" ++ spc () ++ + | false,true -> str "thus" ++ spc () ++ pr_cut (pr_statement (pr_or_thesis pr_constr)) env c | true,false -> str "then" ++ spc () ++ pr_cut (pr_statement (pr_or_thesis pr_constr)) env c - | true,true -> str "hence" ++ spc () ++ + | true,true -> str "hence" ++ spc () ++ pr_cut (pr_statement (pr_or_thesis pr_constr)) env c end | Psuffices c -> - str "suffices" ++ pr_cut pr_suffices_clause env c + str "suffices" ++ pr_cut pr_suffices_clause env c | Prew (sid,c) -> (if _thus then str "thus" else str " ") ++ spc () ++ pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c - | Passume hyps -> + | Passume hyps -> str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps - | Plet hyps -> + | Plet hyps -> str "let" ++ print_vars pr_constr _I env false true "let" hyps | Pclaim st -> str "claim" ++ spc () ++ pr_statement pr_constr env st | Pfocus st -> str "focus on" ++ spc () ++ pr_statement pr_constr env st | Pconsider (id,hyps) -> - str "consider" ++ print_vars pr_constr _I env false false "consider" hyps - ++ spc () ++ str "from " ++ pr_constr env id + str "consider" ++ print_vars pr_constr _I env false false "consider" hyps + ++ spc () ++ str "from " ++ pr_constr env id | Pgiven hyps -> str "given" ++ print_vars pr_constr _I env false false "given" hyps - | Ptake witl -> - str "take" ++ spc () ++ - prlist_with_sep pr_coma (pr_constr env) witl + | Ptake witl -> + str "take" ++ spc () ++ + prlist_with_sep pr_comma (pr_constr env) witl | Pdefine (id,args,body) -> - str "define" ++ spc () ++ pr_id id ++ spc () ++ - prlist_with_sep spc - (fun st -> str "(" ++ - pr_statement pr_constr env st ++ str ")") args ++ spc () ++ - str "as" ++ (pr_constr env body) - | Pcast (id,typ) -> - str "reconsider" ++ spc () ++ - pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++ - str "as" ++ spc () ++ (pr_constr env typ) - | Psuppose hyps -> - str "suppose" ++ + str "define" ++ spc () ++ pr_id id ++ spc () ++ + prlist_with_sep spc + (fun st -> str "(" ++ + pr_statement pr_constr env st ++ str ")") args ++ spc () ++ + str "as" ++ (pr_constr env body) + | Pcast (id,typ) -> + str "reconsider" ++ spc () ++ + pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++ + str "as" ++ spc () ++ (pr_constr env typ) + | Psuppose hyps -> + str "suppose" ++ print_hyps pr_constr _I env false false "we have" hyps | Pcase (params,pat,hyps) -> str "suppose it is" ++ spc () ++ pr_pat pat ++ - (if params = [] then mt () else - (spc () ++ str "with" ++ spc () ++ - prlist_with_sep spc - (fun st -> str "(" ++ - pr_statement pr_constr env st ++ str ")") params ++ spc ())) + (if params = [] then mt () else + (spc () ++ str "with" ++ spc () ++ + prlist_with_sep spc + (fun st -> str "(" ++ + pr_statement pr_constr env st ++ str ")") params ++ spc ())) ++ - (if hyps = [] then mt () else - (spc () ++ str "and" ++ + (if hyps = [] then mt () else + (spc () ++ str "and" ++ print_hyps (pr_or_thesis pr_constr) type_or_thesis env false false "we have" hyps)) - | Pper (et,c) -> + | Pper (et,c) -> str "per" ++ spc () ++ pr_elim_type et ++ spc () ++ pr_casee env c | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et @@ -184,7 +184,7 @@ let pr_emph = function | 3 -> str "*** " | _ -> anomaly "unknown emphasis" -let pr_proof_instr env instr = - pr_emph instr.emph ++ spc () ++ +let pr_proof_instr env instr = + pr_emph instr.emph ++ spc () ++ pr_bare_proof_instr false false env instr.instr |