X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=9fa1d05b62e5fdfaddac84da415b57845e51b310;hb=fd93fa0155994b70482e0f07d8e45c238cce835d;hp=fd3c444b9d26e009e55b23453949e60bd1df5ebe;hpb=81d0d5a3aad863b991996c008f5c19076e771dbb;p=helm.git diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index fd3c444b9..9fa1d05b6 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -73,6 +73,21 @@ let pp_terms ~term_pp terms = String.concat ", " (List.map term_pp terms) let opt_string_pp = function | None -> "" | Some what -> what ^ " " + +let pp_auto_params ~term_pp (univ, params) = + String.concat " " + (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) ^ + if univ <> [] then + (if params <> [] then " " else "") ^ "by " ^ + String.concat " " (List.map term_pp univ) + 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 @@ -100,12 +115,9 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = | Absurd (_, term) -> "absurd" ^ term_pp term | Apply (_, term) -> "apply " ^ term_pp term | ApplyS (_, term, params) -> - "applyS " ^ term_pp term ^ - String.concat " " - (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) - | AutoBatch (_,params) -> "auto batch " ^ - String.concat " " - (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) 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 ^ pp_intros_specs "names " specs @@ -126,7 +138,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = | Decompose (_, names) -> Printf.sprintf "decompose%s" (pp_intros_specs "names " (None, names)) - | Demodulate _ -> "demodulate" + | Demodulate (_, params) -> "demodulate " ^ pp_auto_params ~term_pp params | Destruct (_, None) -> "destruct" | Destruct (_, Some terms) -> "destruct " ^ pp_terms terms | Elim (_, what, using, pattern, specs) -> @@ -184,17 +196,30 @@ 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 ^ ")" - | RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some (None,term) -> "conclude " ^ term_pp term | Some (Some name,term) -> "obtain (" ^ name ^ ") " ^ term_pp term) ^ "=" ^ term_pp term1 ^ " by " ^ (match term2 with `Auto params -> "_" ^ String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | `Term term2 -> term_pp term2 | `Proof -> "proof") ^ (if cont then " done" else "") + | 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 -> " " + | Some (None,term) -> "conclude " ^ term_pp term + | Some (Some name,term) -> + "obtain (" ^ name ^ ") " ^ term_pp term) + ^ "=" ^ + term_pp term1 ^ + (match term2 with + | `Auto params -> pp_auto_params ~term_pp params + | `Term term2 -> " exact " ^ term_pp term2 + | `Proof -> " proof" + | `SolveWith term -> " using " ^ term_pp term) + ^ (if cont then " done" else "") | Case (_, id, args) -> "case" ^ id ^ String.concat " " @@ -242,9 +267,7 @@ let pp_macro ~term_pp = | Check (_, term) -> Printf.sprintf "check %s" (term_pp term) | Hint (_, true) -> "hint rewrite" | Hint (_, false) -> "hint" - | AutoInteractive (_,params) -> "auto " ^ - String.concat " " - (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) + | 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)