X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite%2FgrafiteAstPp.ml;h=18f14c5ce99aefe1f96c1dcf3fc1e3339b9198d1;hb=f68f452173a5077c58f93587faad65fcced77223;hp=6b618c6ac46ad7c2efcc00e75ffedb031147f721;hpb=85cbd6590001b3489d7565eeb5b3c21232a615df;p=helm.git diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 6b618c6ac..18f14c5ce 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -66,17 +66,24 @@ let pp_intros_specs = function let terms_pp ~term_pp terms = String.concat ", " (List.map term_pp terms) +let opt_string_pp = function + | None -> "" + | Some what -> what ^ " " + let rec pp_tactic ~term_pp ~lazy_term_pp = let pp_reduction_kind = pp_reduction_kind ~term_pp in 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 - | Auto _ -> "auto" + | ApplyS (_, term) -> "applyS " ^ term_pp term + | Auto (_,params) -> "auto " ^ + String.concat " " + (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | Assumption _ -> "assumption" | Change (_, where, with_what) -> sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what) - | Clear (_,id) -> sprintf "clear %s" id + | Clear (_,ids) -> sprintf "clear %s" (pp_idents ids) | ClearBody (_,id) -> sprintf "clearbody %s" id | Constructor (_,n) -> "constructor " ^ string_of_int n | Contradiction _ -> "contradiction" @@ -84,14 +91,14 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = "cut " ^ term_pp term ^ (match ident with None -> "" | Some id -> " as " ^ id) | Decompose (_, [], what, names) -> - sprintf "decompose %s%s" what (pp_intros_specs (None, names)) + sprintf "decompose %s%s" (opt_string_pp what) (pp_intros_specs (None, names)) | Decompose (_, types, what, names) -> let to_ident = function | Ident id -> id | Type _ -> assert false in let types = List.rev_map to_ident types in - sprintf "decompose %s %s%s" (pp_idents types) what (pp_intros_specs (None, names)) + sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names)) | Discriminate (_, term) -> "discriminate " ^ term_pp term | Elim (_, term, using, num, idents) -> sprintf "elim " ^ term_pp term ^ @@ -108,7 +115,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = (lazy_term_pp term) (pp_tactic_pattern pattern) | FwdSimpl (_, hyp, idents) -> sprintf "fwd %s%s" hyp - (match idents with [] -> "" | idents -> " " ^ pp_idents idents) + (match idents with [] -> "" | idents -> " as " ^ pp_idents idents) | Generalize (_, pattern, ident) -> sprintf "generalize %s%s" (pp_tactic_pattern pattern) (match ident with None -> "" | Some id -> " as " ^ id) @@ -117,18 +124,19 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Fourier _ -> "fourier" | IdTac _ -> "id" | Injection (_, term) -> "injection " ^ term_pp term - | Intros (_, None, []) -> "intro" + | Intros (_, None, []) -> "intros" | Inversion (_, term) -> "inversion " ^ term_pp term | Intros (_, num, idents) -> sprintf "intros%s%s" (match num with None -> "" | Some num -> " " ^ string_of_int num) (match idents with [] -> "" | idents -> " " ^ pp_idents idents) - | LApply (_, level_opt, terms, term, ident_opt) -> - sprintf "lapply %s%s%s%s" - (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ") + | LApply (_, linear, level_opt, terms, term, ident_opt) -> + sprintf "lapply %s%s%s%s%s" + (if linear then " linear " else "") + (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ") (term_pp term) (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms) - (match ident_opt with None -> "" | Some ident -> " using " ^ ident) + (match ident_opt with None -> "" | Some ident -> " as " ^ ident) | Left _ -> "left" | LetIn (_, term, ident) -> sprintf "let %s in %s" (term_pp term) ident | Reduce (_, kind, pat) -> @@ -168,7 +176,7 @@ let pp_macro ~term_pp = (* Whelp *) | WInstance (_, term) -> "whelp instance " ^ term_pp term | WHint (_, t) -> "whelp hint " ^ term_pp t - | WLocate (_, s) -> "whelp locate " ^ s + | WLocate (_, s) -> "whelp locate \"" ^ s ^ "\"" | WElim (_, t) -> "whelp elim " ^ term_pp t | WMatch (_, term) -> "whelp match " ^ term_pp term (* real macros *) @@ -202,7 +210,7 @@ let pp_coercion uri do_composites = (if do_composites then "compounds" else "no compounds") let pp_command ~obj_pp = function - | Include (_,path) -> "include " ^ path + | Include (_,path) -> "include \"" ^ path ^ "\"" | Qed _ -> "qed" | Drop _ -> "drop" | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value @@ -231,7 +239,8 @@ let rec pp_tactical ~term_pp ~lazy_term_pp = | Semicolon _ -> ";" | Branch _ -> "[" | Shift _ -> "|" - | Pos (_, i) -> sprintf "%d:" i + | Pos (_, i) -> sprintf "%s:" (String.concat "," (List.map string_of_int i)) + | Wildcard _ -> "*:" | Merge _ -> "]" | Focus (_, goals) -> sprintf "focus %s" (String.concat " " (List.map string_of_int goals)) @@ -243,12 +252,12 @@ and pp_tacticals ~term_pp ~lazy_term_pp ~sep tacs = let pp_executable ~term_pp ~lazy_term_pp ~obj_pp = function - | Macro (_, macro) -> pp_macro ~term_pp macro + | Macro (_, macro) -> pp_macro ~term_pp macro ^ "." | Tactical (_, tac, Some punct) -> 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 ~obj_pp cmd ^ "." let pp_comment ~term_pp ~lazy_term_pp ~obj_pp = function @@ -258,5 +267,5 @@ let pp_comment ~term_pp ~lazy_term_pp ~obj_pp = let pp_statement ~term_pp ~lazy_term_pp ~obj_pp = function - | Executable (_, ex) -> pp_executable ~lazy_term_pp ~term_pp ~obj_pp ex + | Executable (_, ex) -> pp_executable ~lazy_term_pp ~term_pp ~obj_pp ex | Comment (_, c) -> pp_comment ~term_pp ~lazy_term_pp ~obj_pp c