X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=df436e7097cefe67fb842f59414a9f3258ad6b12;hb=6a5e51c1cf9a56c74a8b53a9b8bc5aa686c9780e;hp=a98fb8e9d6cd70116d799750b65b06e285ba7bb4;hpb=5649890273cf8e660bba744e84ce5fee1e5efe69;p=helm.git diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index a98fb8e9d..df436e709 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -83,6 +83,12 @@ let pp_auto_params ~term_pp (univ, params) = else "" ;; +let pp_just ~term_pp = + function + `Term term -> "exact " ^ term_pp term + | `Auto params -> pp_auto_params ~term_pp params +;; + let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = let pp_terms = pp_terms ~term_pp in let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in @@ -108,12 +114,14 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = (* First order tactics *) | Absurd (_, term) -> "absurd" ^ term_pp term | Apply (_, term) -> "apply " ^ term_pp term + | ApplyP (_, term) -> "applyP " ^ term_pp term | ApplyS (_, term, params) -> "applyS " ^ term_pp term ^ pp_auto_params ~term_pp params | AutoBatch (_,params) -> "autobatch " ^ pp_auto_params ~term_pp params | Assumption _ -> "assumption" - | Cases (_, term, specs) -> Printf.sprintf "cases " ^ term_pp term ^ + | Cases (_, term, pattern, specs) -> Printf.sprintf "cases " ^ term_pp term ^ + pp_tactic_pattern pattern ^ pp_intros_specs "names " specs | Change (_, where, with_what) -> Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what) @@ -190,16 +198,16 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = (* Tattiche Aggiunte *) | Assume (_, ident , term) -> "assume" ^ ident ^ ":" ^ term_pp term | Suppose (_, term, ident,term1) -> "suppose" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1) - | Bydone (_, term) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "done" - | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^ + | Bydone (_, just) -> pp_just ~term_pp just ^ "done" + | By_just_we_proved (_, just, term1, ident, term2) -> pp_just ~term_pp just ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^ (match term2 with None -> " " | Some term2 -> term_pp term2) | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ (match ident with None -> "" | Some ident -> "(" ^ ident ^ ")") ^ (match term1 with None -> " " | Some term1 -> term_pp term1) | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on" ^ term_pp term ^ "to prove" ^ term_pp term1 | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ term_pp term ^ "to prove" ^ term_pp term1 | Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ term_pp term ^ "(" ^ ident ^ ")" | Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term - | ExistsElim (_, term0, ident, term, ident1, term1) -> "by " ^ (match term0 with None -> "_" | Some term -> term_pp term) ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ lazy_term_pp term1 ^ "(" ^ ident1 ^ ")" - | AndElim (_, term, ident1, term1, ident2, term2) -> "by " ^ term_pp term ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")" + | ExistsElim (_, just, ident, term, ident1, term1) -> pp_just ~term_pp just ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ lazy_term_pp term1 ^ "(" ^ ident1 ^ ")" + | AndElim (_, just, ident1, term1, ident2, term2) -> pp_just ~term_pp just ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")" | RewritingStep (_, term, term1, term2, cont) -> (match term with | None -> " " @@ -250,6 +258,17 @@ let pp_macro ~term_pp = let prefix_pp prefix = if prefix = "" then "" else Printf.sprintf " \"%s\"" prefix in + let flavour_pp = function + | None -> "" + | Some `Definition -> "as definition" + | Some `MutualDefinition -> "as mutual" + | Some `Fact -> "as fact" + | Some `Lemma -> "as lemma" + | Some `Remark -> "as remark" + | Some `Theorem -> "as theorem" + | Some `Variant -> "as variant" + | Some `Axiom -> "as axiom" + in function (* Whelp *) | WInstance (_, term) -> "whelp instance " ^ term_pp term @@ -262,8 +281,8 @@ let pp_macro ~term_pp = | Hint (_, true) -> "hint rewrite" | Hint (_, false) -> "hint" | AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params - | Inline (_, style, suri, prefix) -> - Printf.sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix) + | Inline (_, style, suri, prefix, flavour) -> + Printf.sprintf "inline %s\"%s\"%s%s" (style_pp style) suri (prefix_pp prefix) (flavour_pp flavour) let pp_associativity = function | Gramext.LeftA -> "left associative" @@ -281,15 +300,15 @@ let pp_default what uris = Printf.sprintf "default \"%s\" %s" what (String.concat " " (List.map UriManager.string_of_uri uris)) -let pp_coercion uri do_composites arity saturations= +let pp_coercion ~term_pp t do_composites arity saturations= Printf.sprintf "coercion %s %d %d %s" - (UriManager.string_of_uri uri) arity saturations + (term_pp t) arity saturations (if do_composites then "" else "nocomposites") let pp_command ~term_pp ~obj_pp = function | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri - | Coercion (_, uri, do_composites, i, j) -> - pp_coercion uri do_composites i j + | Coercion (_, t, do_composites, i, j) -> + pp_coercion ~term_pp t do_composites i j | Default (_,what,uris) -> pp_default what uris | Drop _ -> "drop" | Include (_,path) -> "include \"" ^ path ^ "\""