X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite%2FgrafiteAstPp.ml;h=547e28b3da0cac759bcd3569f13a29c22625fe1c;hb=afea2be14c1c197e0804e8607fc6dcc49ce46955;hp=55736e862e2cba8aa5ee548a823691af3f7810aa;hpb=6188c48d0ccbe5d8b7dbae9b8ff6de5bf984efa4;p=helm.git diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 55736e862..547e28b3d 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -99,7 +99,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = let types = List.rev_map to_ident types in sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names)) | Demodulate _ -> "demodulate" - | Discriminate (_, term) -> "discriminate " ^ term_pp term + | Destruct (_, term) -> "destruct " ^ term_pp term | Elim (_, term, using, num, idents) -> sprintf "elim " ^ term_pp term ^ (match using with None -> "" | Some term -> " using " ^ term_pp term) @@ -123,7 +123,6 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Fail _ -> "fail" | Fourier _ -> "fourier" | IdTac _ -> "id" - | Injection (_, term) -> "injection " ^ term_pp term | Intros (_, None, []) -> "intros" | Inversion (_, term) -> "inversion " ^ term_pp term | Intros (_, num, idents) -> @@ -152,10 +151,29 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Right _ -> "right" | Ring _ -> "ring" | Split _ -> "split" + | Subst _ -> "subst" | Symmetry _ -> "symmetry" | Transitivity (_, term) -> "transitivity " ^ term_pp term - - let pp_search_kind = function + (* 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 ^ "(" ^ident^ ")" ^ + (match term2 with None -> " " | Some term2 -> term_pp term2) + | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> 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 " ^ term_pp term0 ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ 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 term -> "obtain " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with None -> "_" | Some term2 -> term_pp term2) ^ (match cont with None -> " done" | Some Cic.Anonymous -> "" | Some (Cic.Name id) -> " we proved " ^ id) + | Case (_, id, args) -> + "case" ^ id ^ + String.concat " " + (List.map (function (id,term) -> "(" ^ id ^ ": " ^ term_pp term ^ ")") + args) + + let pp_search_kind = function | `Locate -> "locate" | `Hint -> "hint" | `Match -> "match" @@ -180,9 +198,9 @@ let pp_macro ~term_pp = | WElim (_, t) -> "whelp elim " ^ term_pp t | WMatch (_, term) -> "whelp match " ^ term_pp term (* real macros *) - | Check (_, term) -> sprintf "Check %s" (term_pp term) + | Check (_, term) -> sprintf "check %s" (term_pp term) | Hint _ -> "hint" - | Quit _ -> "Quit" + | Inline (_,suri) -> sprintf "inline %s" suri let pp_associativity = function | Gramext.LeftA -> "left associative" @@ -200,19 +218,30 @@ let pp_default what uris = sprintf "default \"%s\" %s" what (String.concat " " (List.map UriManager.string_of_uri uris)) -let pp_coercion uri do_composites = - sprintf "coercion %s (* %s *)" (UriManager.string_of_uri uri) +let pp_coercion uri do_composites arity = + sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity (if do_composites then "compounds" else "no compounds") -let pp_command ~obj_pp = function +let pp_command ~term_pp ~obj_pp = function + | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i + | Default (_,what,uris) -> pp_default what uris + | Drop _ -> "drop" | Include (_,path) -> "include \"" ^ path ^ "\"" + | Obj (_,obj) -> obj_pp obj | Qed _ -> "qed" - | Drop _ -> "drop" + | Relation (_,id,a,aeq,refl,sym,trans) -> + "relation " ^ term_pp aeq ^ " on " ^ term_pp a ^ + (match refl with + Some r -> " reflexivity proved by " ^ term_pp r + | None -> "") ^ + (match sym with + Some r -> " symmetry proved by " ^ term_pp r + | None -> "") ^ + (match trans with + Some r -> " transitivity proved by " ^ term_pp r + | None -> "") + | Print (_,s) -> "print " ^ s | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value - | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites - | Obj (_,obj) -> obj_pp obj - | Default (_,what,uris) -> - pp_default what uris let rec pp_tactical ~term_pp ~lazy_term_pp = let pp_tactic = pp_tactic ~lazy_term_pp ~term_pp in @@ -229,6 +258,7 @@ let rec pp_tactical ~term_pp ~lazy_term_pp = | First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs) | Try (_, tac) -> "try " ^ pp_tactical ~term_pp ~lazy_term_pp tac | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac) + | Progress (_, tac) -> "progress " ^ pp_tactical ~term_pp ~lazy_term_pp tac | Dot _ -> "." | Semicolon _ -> ";" @@ -252,7 +282,7 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp = pp_tactical ~lazy_term_pp ~term_pp tac ^ pp_tactical ~lazy_term_pp ~term_pp punct | Tactical (_, tac, None) -> pp_tactical ~lazy_term_pp ~term_pp tac - | Command (_, cmd) -> pp_command ~obj_pp cmd ^ "." + | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "." let pp_comment ~term_pp ~lazy_term_pp ~obj_pp = function