X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite%2FgrafiteAstPp.ml;h=f38dbf8597dc3caa309f5fb60c45f30f5dc4d40d;hb=001b43beae9e912a921da426d23c1e437328bb9e;hp=f51cd0bcaf81ba03f5d57d7f51e732d36a78d757;hpb=b309e9baa51822004379ce6364e138e5e803efe4;p=helm.git diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index f51cd0bca..f38dbf859 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -33,7 +33,7 @@ let tactical_terminator = "" let tactic_terminator = tactical_terminator let command_terminator = tactical_terminator -let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" +let pp_idents idents = "(" ^ String.concat " " idents ^ ")" let pp_reduction_kind ~term_pp = function | `Normalize -> "normalize" @@ -44,6 +44,7 @@ let pp_reduction_kind ~term_pp = function | `Whd -> "whd" let pp_tactic_pattern ~term_pp ~lazy_term_pp (what, hyp, goal) = + if what = None && hyp = [] && goal = None then "" else let what_text = match what with | None -> "" @@ -74,7 +75,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = let pp_tactic_pattern = pp_tactic_pattern ~lazy_term_pp ~term_pp in function | Absurd (_, term) -> "absurd" ^ term_pp term - | Apply (_, term) -> "apply " ^ term_pp term + | Apply (_, term) -> "apply (" ^ term_pp term ^ ")" (* FG: rm parentheses *) | ApplyS (_, term, params) -> "applyS " ^ term_pp term ^ String.concat " " @@ -83,6 +84,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | Assumption _ -> "assumption" + | Cases (_, term, idents) -> sprintf "cases " ^ term_pp term ^ + pp_intros_specs (None, idents) | Change (_, where, with_what) -> sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what) | Clear (_,ids) -> sprintf "clear %s" (pp_idents ids) @@ -90,7 +93,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Constructor (_,n) -> "constructor " ^ string_of_int n | Contradiction _ -> "contradiction" | Cut (_, ident, term) -> - "cut " ^ term_pp term ^ + "cut (" ^ term_pp term ^ ")" ^ (* FG: rm parentheses *) (match ident with None -> "" | Some id -> " as " ^ id) | Decompose (_, [], what, names) -> sprintf "decompose %s%s" (opt_string_pp what) (pp_intros_specs (None, names)) @@ -104,7 +107,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Demodulate _ -> "demodulate" | Destruct (_, term) -> "destruct " ^ term_pp term | Elim (_, term, using, num, idents) -> - sprintf "elim " ^ term_pp term ^ + sprintf "elim (" ^ term_pp term ^ ")" ^ (* FG: rm parentheses *) (match using with None -> "" | Some term -> " using " ^ term_pp term) ^ pp_intros_specs (num, idents) | ElimType (_, term, using, num, idents) -> @@ -140,17 +143,21 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms) (match ident_opt with None -> "" | Some ident -> " as " ^ ident) | Left _ -> "left" - | LetIn (_, term, ident) -> sprintf "let %s in %s" (term_pp term) ident + | LetIn (_, term, ident) -> + sprintf "letin %s \\def %s" ident ("(" ^ term_pp term ^ ")") (* FG: rm parentheses *) | Reduce (_, kind, pat) -> sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat) | Reflexivity _ -> "reflexivity" + | Rename (_, froms, tos) -> + sprintf "rename %s as %s" (pp_idents froms) (pp_idents tos) | Replace (_, pattern, t) -> sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t) - | Rewrite (_, pos, t, pattern) -> - sprintf "rewrite %s %s %s" + | Rewrite (_, pos, t, pattern, names) -> + sprintf "rewrite %s %s %s%s" (if pos = `LeftToRight then ">" else "<") - (term_pp t) + ("(" ^ term_pp t ^ ")") (* FG: rm parentheses *) (pp_tactic_pattern pattern) + (if names = [] then "" else " as " ^ pp_idents names) | Right _ -> "right" | Ring _ -> "ring" | Split _ -> "split" @@ -164,6 +171,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | 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^ ")") ^ (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 @@ -193,6 +201,13 @@ let pp_arg ~term_pp arg = let pp_macro ~term_pp = let term_pp = pp_arg ~term_pp in + let style_pp = function + | Declarative -> "" + | Procedural -> "procedural " + in + let prefix_pp prefix = + if prefix = "" then "" else sprintf " \"%s\"" prefix + in function (* Whelp *) | WInstance (_, term) -> "whelp instance " ^ term_pp term @@ -203,8 +218,8 @@ let pp_macro ~term_pp = (* real macros *) | Check (_, term) -> sprintf "check %s" (term_pp term) | Hint _ -> "hint" - | Inline (_, suri, "") -> sprintf "inline \"%s\"" suri - | Inline (_, suri, prefix) -> sprintf "inline \"%s\" \"%s\"" suri prefix + | Inline (_, style, suri, prefix) -> + sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix) let pp_associativity = function | Gramext.LeftA -> "left associative" @@ -291,9 +306,10 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp = let pp_comment ~term_pp ~lazy_term_pp ~obj_pp = function - | Note (_,str) -> sprintf "(* %s *)" str + | Note (_,"") -> sprintf "\n" + | Note (_,str) -> sprintf "(* %s *)\n" str | Code (_,code) -> - sprintf "(** %s. **)" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code) + sprintf "(** %s. **)\n" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code) let pp_statement ~term_pp ~lazy_term_pp ~obj_pp = function