From 55ba0a660f91e491e904dad63b14ddf2bcc2754d Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 12 Dec 2005 16:00:38 +0000 Subject: [PATCH] abstracted pretty printers over inner pretty printing units (terms, lazy terms, and objects) --- helm/ocaml/grafite/cicNotation.mli | 2 +- helm/ocaml/grafite/grafiteAst.ml | 10 +- helm/ocaml/grafite/grafiteAstPp.ml | 189 +++++++++++--------------- helm/ocaml/grafite/grafiteAstPp.mli | 53 +++++--- helm/ocaml/grafite/grafiteMarshal.ml | 9 +- helm/ocaml/grafite/grafiteMarshal.mli | 2 +- 6 files changed, 128 insertions(+), 137 deletions(-) diff --git a/helm/ocaml/grafite/cicNotation.mli b/helm/ocaml/grafite/cicNotation.mli index 41b775562..9eb98c1d3 100644 --- a/helm/ocaml/grafite/cicNotation.mli +++ b/helm/ocaml/grafite/cicNotation.mli @@ -26,7 +26,7 @@ type notation_id val process_notation: - ('a, 'b) GrafiteAst.command -> ('a, 'b) GrafiteAst.command * notation_id list + 'obj GrafiteAst.command -> 'obj GrafiteAst.command * notation_id list val remove_notation: notation_id -> unit diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml index 3d176fbe5..e1ae5865d 100644 --- a/helm/ocaml/grafite/grafiteAst.ml +++ b/helm/ocaml/grafite/grafiteAst.ml @@ -28,7 +28,7 @@ type direction = [ `LeftToRight | `RightToLeft ] type loc = CicNotationPt.location type ('term, 'lazy_term, 'ident) pattern = - 'lazy_term option * ('ident * 'term) list * 'term + 'lazy_term option * ('ident * 'term) list * 'term option type ('term, 'ident) type_spec = | Ident of 'ident @@ -114,9 +114,9 @@ type alias_spec = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 4 +let magic = 5 -type ('term,'obj) command = +type 'obj command = | Default of loc * string * UriManager.uri list | Include of loc * string | Set of loc * string * string @@ -125,7 +125,7 @@ type ('term,'obj) command = (** name. * Name is needed when theorem was started without providing a name *) - | Coercion of loc * 'term * bool (* add composites *) + | Coercion of loc * UriManager.uri * bool (* add composites *) | Alias of loc * alias_spec (** parameters, name, type, fields *) | Obj of loc * 'obj @@ -175,7 +175,7 @@ let is_punctuation = | _ -> false type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code = - | Command of loc * ('term,'obj) command + | Command of loc * 'obj command | Macro of loc * 'term macro | Tactical of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical * ('term, 'lazy_term, 'reduction, 'ident) tactical option(* punctuation *) diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml index dac1d6e05..617a6d563 100644 --- a/helm/ocaml/grafite/grafiteAstPp.ml +++ b/helm/ocaml/grafite/grafiteAstPp.ml @@ -31,32 +31,29 @@ let tactical_terminator = "" let tactic_terminator = tactical_terminator let command_terminator = tactical_terminator -let pp_term_ast term = CicNotationPp.pp_term term -let pp_term_cic term = CicPp.ppterm term - let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" -let pp_terms_ast terms = String.concat ", " (List.map pp_term_ast terms) - -let pp_reduction_kind = function +let pp_reduction_kind ~term_pp = function | `Normalize -> "normalize" | `Reduce -> "reduce" | `Simpl -> "simplify" - | `Unfold (Some t) -> "unfold " ^ pp_term_ast t + | `Unfold (Some t) -> "unfold " ^ term_pp t | `Unfold None -> "unfold" | `Whd -> "whd" - -let pp_pattern (t, hyp, goal) = - let pp_hyp_pattern l = - String.concat "; " - (List.map (fun (name, p) -> sprintf "%s : %s" name (pp_term_ast p)) l) in - let pp_t t = - match t with - None -> "" - | Some t -> pp_term_ast t - in - pp_t t ^ " in " ^ pp_hyp_pattern hyp ^ " \\vdash " ^ pp_term_ast goal +let pp_tactic_pattern ~term_pp ~lazy_term_pp (what, hyp, goal) = + let what_text = + match what with + | None -> "" + | Some t -> sprintf "in match (%s) " (lazy_term_pp t) in + let hyp_text = + String.concat " " + (List.map (fun (name, p) -> sprintf "%s:(%s)" name (term_pp p)) hyp) in + let goal_text = + match goal with + | None -> "" + | Some t -> sprintf "\\vdash (%s)" (term_pp t) in + sprintf "%sin %s%s" what_text hyp_text goal_text let pp_intros_specs = function | None, [] -> "" @@ -64,20 +61,25 @@ let pp_intros_specs = function | None, idents -> Printf.sprintf " names %s" (pp_idents idents) | Some num, idents -> Printf.sprintf " names %i %s" num (pp_idents idents) -let rec pp_tactic = function - | Absurd (_, term) -> "absurd" ^ pp_term_ast term - | Apply (_, term) -> "apply " ^ pp_term_ast term +let terms_pp ~term_pp terms = String.concat ", " (List.map term_pp terms) + +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" | Assumption _ -> "assumption" | Change (_, where, with_what) -> - sprintf "change %s with %s" (pp_pattern where) (pp_term_ast with_what) + sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what) | Clear (_,id) -> sprintf "clear %s" id | ClearBody (_,id) -> sprintf "clearbody %s" id - | Compare (_,term) -> "compare " ^ pp_term_ast term + | Compare (_,term) -> "compare " ^ term_pp term | Constructor (_,n) -> "constructor " ^ string_of_int n | Contradiction _ -> "contradiction" | Cut (_, ident, term) -> - "cut " ^ pp_term_ast term ^ + "cut " ^ term_pp term ^ (match ident with None -> "" | Some id -> " as " ^ id) | DecideEquality _ -> "decide equality" | Decompose (_, [], what, names) -> @@ -89,31 +91,31 @@ let rec pp_tactic = function in let types = List.rev_map to_ident types in sprintf "decompose %s %s%s" (pp_idents types) what (pp_intros_specs (None, names)) - | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term + | Discriminate (_, term) -> "discriminate " ^ term_pp term | Elim (_, term, using, num, idents) -> - sprintf "elim " ^ pp_term_ast term ^ - (match using with None -> "" | Some term -> " using " ^ pp_term_ast term) + sprintf "elim " ^ term_pp term ^ + (match using with None -> "" | Some term -> " using " ^ term_pp term) ^ pp_intros_specs (num, idents) | ElimType (_, term, using, num, idents) -> - sprintf "elim type " ^ pp_term_ast term ^ - (match using with None -> "" | Some term -> " using " ^ pp_term_ast term) + sprintf "elim type " ^ term_pp term ^ + (match using with None -> "" | Some term -> " using " ^ term_pp term) ^ pp_intros_specs (num, idents) - | Exact (_, term) -> "exact " ^ pp_term_ast term + | Exact (_, term) -> "exact " ^ term_pp term | Exists _ -> "exists" | Fold (_, kind, term, pattern) -> sprintf "fold %s %s %s" (pp_reduction_kind kind) - (pp_term_ast term) (pp_pattern pattern) + (lazy_term_pp term) (pp_tactic_pattern pattern) | FwdSimpl (_, hyp, idents) -> sprintf "fwd %s%s" hyp (match idents with [] -> "" | idents -> " " ^ pp_idents idents) | Generalize (_, pattern, ident) -> - sprintf "generalize %s%s" (pp_pattern pattern) + sprintf "generalize %s%s" (pp_tactic_pattern pattern) (match ident with None -> "" | Some id -> " as " ^ id) | Goal (_, n) -> "goal " ^ string_of_int n | Fail _ -> "fail" | Fourier _ -> "fourier" | IdTac _ -> "id" - | Injection (_, term) -> "injection " ^ pp_term_ast term + | Injection (_, term) -> "injection " ^ term_pp term | Intros (_, None, []) -> "intro" | Intros (_, num, idents) -> sprintf "intros%s%s" @@ -122,26 +124,26 @@ let rec pp_tactic = function | 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 ^ " ") - (pp_term_ast term) - (match terms with [] -> "" | _ -> " to " ^ pp_terms_ast terms) + (term_pp term) + (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms) (match ident_opt with None -> "" | Some ident -> " using " ^ ident) | Left _ -> "left" - | LetIn (_, term, ident) -> sprintf "let %s in %s" (pp_term_ast term) ident + | LetIn (_, term, ident) -> sprintf "let %s in %s" (term_pp term) ident | Reduce (_, kind, pat) -> - sprintf "%s %s" (pp_reduction_kind kind) (pp_pattern pat) + sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat) | Reflexivity _ -> "reflexivity" | Replace (_, pattern, t) -> - sprintf "replace %s with %s" (pp_pattern pattern) (pp_term_ast t) + sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t) | Rewrite (_, pos, t, pattern) -> sprintf "rewrite %s %s %s" (if pos = `LeftToRight then ">" else "<") - (pp_term_ast t) - (pp_pattern pattern) + (term_pp t) + (pp_tactic_pattern pattern) | Right _ -> "right" | Ring _ -> "ring" | Split _ -> "split" | Symmetry _ -> "symmetry" - | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term + | Transitivity (_, term) -> "transitivity " ^ term_pp term let pp_search_kind = function | `Locate -> "locate" @@ -150,31 +152,23 @@ let pp_search_kind = function | `Elim -> "elim" | `Instance -> "instance" -let pp_macro pp_term = function +let pp_macro ~term_pp = function (* Whelp *) - | WInstance (_, term) -> "whelp instance " ^ pp_term term - | WHint (_, t) -> "whelp hint " ^ pp_term t + | WInstance (_, term) -> "whelp instance " ^ term_pp term + | WHint (_, t) -> "whelp hint " ^ term_pp t | WLocate (_, s) -> "whelp locate " ^ s - | WElim (_, t) -> "whelp elim " ^ pp_term t - | WMatch (_, term) -> "whelp match " ^ pp_term term + | WElim (_, t) -> "whelp elim " ^ term_pp t + | WMatch (_, term) -> "whelp match " ^ term_pp term (* real macros *) -(* | Abort _ -> "Abort" *) - | Check (_, term) -> sprintf "Check %s" (pp_term term) + | Check (_, term) -> sprintf "Check %s" (term_pp term) | Hint _ -> "hint" -(* | Redo (_, None) -> "Redo" - | Redo (_, Some n) -> sprintf "Redo %d" n *) | Search_pat (_, kind, pat) -> sprintf "search %s \"%s\"" (pp_search_kind kind) pat | Search_term (_, kind, term) -> - sprintf "search %s %s" (pp_search_kind kind) (pp_term term) -(* | Undo (_, None) -> "Undo" - | Undo (_, Some n) -> sprintf "Undo %d" n *) + sprintf "search %s %s" (pp_search_kind kind) (term_pp term) | Print (_, name) -> sprintf "Print \"%s\"" name | Quit _ -> "Quit" -let pp_macro_ast = pp_macro pp_term_ast -let pp_macro_cic = pp_macro pp_term_cic - let pp_alias = function | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri | Symbol_alias (symb, instance, desc) -> @@ -224,23 +218,18 @@ let pp_notation dir_opt l1_pattern assoc prec l2_pattern = (pp_precedence prec) (pp_l2_pattern l2_pattern) -let pp_coercion_ast term do_composites = - sprintf "coercion %s (* %s *)" (pp_term_ast term) - (if do_composites then "compounds" else "no compounds") - -let pp_coercion_cic term do_composites = - sprintf "coercion %s (* %s *)" (pp_term_cic term) +let pp_coercion uri do_composites = + sprintf "coercion %s (* %s *)" (UriManager.string_of_uri uri) (if do_composites then "compounds" else "no compounds") -let pp_command = function +let pp_command ~obj_pp = function | Include (_,path) -> "include " ^ path | Qed _ -> "qed" | Drop _ -> "drop" | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value - | Coercion (_,term, do_composites) -> - pp_coercion_ast term do_composites + | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites | Alias (_,s) -> pp_alias s - | Obj (_,obj) -> CicNotationPp.pp_obj obj + | Obj (_,obj) -> obj_pp obj | Default (_,what,uris) -> pp_default what uris | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) -> @@ -250,15 +239,20 @@ let pp_command = function | Render _ | Dump _ -> assert false (* ZACK: debugging *) -let rec pp_tactical = function +let rec pp_tactical ~term_pp ~lazy_term_pp = + let pp_tactic = pp_tactic ~lazy_term_pp ~term_pp in + let pp_tacticals = pp_tacticals ~lazy_term_pp ~term_pp in + function | Tactic (_, tac) -> pp_tactic tac - | Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac) - | Repeat (_, tac) -> "repeat " ^ pp_tactical tac + | Do (_, count, tac) -> + sprintf "do %d %s" count (pp_tactical ~term_pp ~lazy_term_pp tac) + | Repeat (_, tac) -> "repeat " ^ pp_tactical ~term_pp ~lazy_term_pp tac | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs | Then (_, tac, tacs) -> - sprintf "%s; [%s]" (pp_tactical tac) (pp_tacticals ~sep:" | " tacs) + sprintf "%s; [%s]" (pp_tactical ~term_pp ~lazy_term_pp tac) + (pp_tacticals ~sep:" | " tacs) | First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs) - | Try (_, tac) -> "try " ^ pp_tactical tac + | Try (_, tac) -> "try " ^ pp_tactical ~term_pp ~lazy_term_pp tac | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac) | Dot _ -> "." @@ -272,46 +266,29 @@ let rec pp_tactical = function | Unfocus _ -> "unfocus" | Skip _ -> "skip" -and pp_tacticals ~sep tacs = String.concat sep (List.map pp_tactical tacs) - -let pp_tactical tac = pp_tactical tac -let pp_tactic tac = pp_tactic tac -let pp_command tac = pp_command tac +and pp_tacticals ~term_pp ~lazy_term_pp ~sep tacs = + String.concat sep (List.map (pp_tactical~lazy_term_pp ~term_pp) tacs) -let pp_executable = function - | Macro (_,x) -> pp_macro_ast x - | Tactical (_, tac, Some punct) -> pp_tactical tac ^ pp_tactical punct - | Tactical (_, tac, None) -> pp_tactical tac - | Command (_,x) -> pp_command x +let pp_executable ~term_pp ~lazy_term_pp ~obj_pp = + function + | 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 -let pp_comment = function +let pp_comment ~term_pp ~lazy_term_pp ~obj_pp = + function | Note (_,str) -> sprintf "(* %s *)" str - | Code (_,code) -> sprintf "(** %s. **)" (pp_executable code) - -let pp_statement = function - | Executable (_, ex) -> pp_executable ex - | Comment (_, c) -> pp_comment c - + | Code (_,code) -> + sprintf "(** %s. **)" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code) +let pp_statement ~term_pp ~lazy_term_pp ~obj_pp = + function + | Executable (_, ex) -> pp_executable ~lazy_term_pp ~term_pp ~obj_pp ex + | Comment (_, c) -> pp_comment ~term_pp ~lazy_term_pp ~obj_pp c -let pp_cic_command = function - | Include (_,path) -> "include " ^ path - | Qed _ -> "qed" - | Drop _ -> "drop" - | Coercion (_,term, do_composites) -> - pp_coercion_cic term do_composites - | Obj (_,obj) -> CicPp.ppobj obj - | Set _-> assert false (* not implemented *) - | Alias (_, alias) -> pp_alias alias - | Default (_,what,uris) -> - pp_default what uris - | Render _ -> assert false (* not implemented *) - | Dump _ -> assert false (* not implemented *) - | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) -> - pp_interpretation dsc symbol arg_patterns cic_appl_pattern - | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) -> - pp_notation dir_opt l1_pattern assoc prec l2_pattern - let pp_dependency = function | IncludeDep str -> "include \"" ^ str ^ "\"" | BaseuriDep str -> "set \"baseuri\" \"" ^ str ^ "\"" diff --git a/helm/ocaml/grafite/grafiteAstPp.mli b/helm/ocaml/grafite/grafiteAstPp.mli index 1ecfb4352..80d2174f7 100644 --- a/helm/ocaml/grafite/grafiteAstPp.mli +++ b/helm/ocaml/grafite/grafiteAstPp.mli @@ -24,43 +24,56 @@ *) val pp_tactic: - (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string) + term_pp:('term -> string) -> + lazy_term_pp:('lazy_term -> string) -> + ('term, 'lazy_term, 'term GrafiteAst.reduction, string) GrafiteAst.tactic -> string -val pp_command: - (CicNotationPt.term,CicNotationPt.obj) GrafiteAst.command -> string -val pp_macro: ('a -> string) -> 'a GrafiteAst.macro -> string +val pp_tactic_pattern: + term_pp:('term -> string) -> + lazy_term_pp:('lazy_term -> string) -> + ('term, 'lazy_term, string) GrafiteAst.pattern -> + string + +val pp_reduction_kind: + term_pp:('a -> string) -> + 'a GrafiteAst.reduction -> + string + +val pp_command: obj_pp:('obj -> string) -> 'obj GrafiteAst.command -> string +val pp_macro: term_pp:('term -> string) -> 'term GrafiteAst.macro -> string +val pp_alias: GrafiteAst.alias_spec -> string +val pp_dependency: GrafiteAst.dependency -> string val pp_comment: - (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, - CicNotationPt.obj, string) + term_pp:('term -> string) -> + lazy_term_pp:('lazy_term -> string) -> + obj_pp:('obj -> string) -> + ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string) GrafiteAst.comment -> string val pp_executable: - (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, - CicNotationPt.obj, string) + term_pp:('term -> string) -> + lazy_term_pp:('lazy_term -> string) -> + obj_pp:('obj -> string) -> + ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string) GrafiteAst.code -> string val pp_statement: - (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, - CicNotationPt.obj, string) + term_pp:('term -> string) -> + lazy_term_pp:('lazy_term -> string) -> + obj_pp:('obj -> string) -> + ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string) GrafiteAst.statement -> string -val pp_macro_ast: CicNotationPt.term GrafiteAst.macro -> string -val pp_macro_cic: Cic.term GrafiteAst.macro -> string - val pp_tactical: - (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string) + term_pp:('term -> string) -> + lazy_term_pp:('lazy_term -> string) -> + ('term, 'lazy_term, 'term GrafiteAst.reduction, string) GrafiteAst.tactical -> string -val pp_alias: GrafiteAst.alias_spec -> string - -val pp_cic_command: (Cic.term,Cic.obj) GrafiteAst.command -> string - -val pp_dependency: GrafiteAst.dependency -> string - diff --git a/helm/ocaml/grafite/grafiteMarshal.ml b/helm/ocaml/grafite/grafiteMarshal.ml index 8b4f8858b..8c6928b7b 100644 --- a/helm/ocaml/grafite/grafiteMarshal.ml +++ b/helm/ocaml/grafite/grafiteMarshal.ml @@ -27,7 +27,7 @@ exception Checksum_failure of string exception Corrupt_moo of string exception Version_mismatch of string -type ast_command = (Cic.term, Cic.obj) GrafiteAst.command +type ast_command = Cic.obj GrafiteAst.command type moo = ast_command list let marshal_flags = [] @@ -50,13 +50,14 @@ let rehash_cmd_uris = in let appl_pattern = aux cic_appl_pattern in GrafiteAst.Interpretation (loc, dsc, args, appl_pattern) - | GrafiteAst.Coercion (loc, term, close) -> - GrafiteAst.Coercion (loc, CicUtil.rehash_term term, close) + | GrafiteAst.Coercion (loc, uri, close) -> + GrafiteAst.Coercion (loc, rehash_uri uri, close) | GrafiteAst.Notation _ | GrafiteAst.Alias _ as cmd -> cmd | cmd -> prerr_endline "Found a command not expected in a .moo:"; - prerr_endline (GrafiteAstPp.pp_cic_command cmd); + let obj_pp _ = assert false in + prerr_endline (GrafiteAstPp.pp_command ~obj_pp cmd); assert false (** .moo file format diff --git a/helm/ocaml/grafite/grafiteMarshal.mli b/helm/ocaml/grafite/grafiteMarshal.mli index 9be797a44..4b49cfc41 100644 --- a/helm/ocaml/grafite/grafiteMarshal.mli +++ b/helm/ocaml/grafite/grafiteMarshal.mli @@ -28,7 +28,7 @@ exception Checksum_failure of string exception Corrupt_moo of string exception Version_mismatch of string -type ast_command = (Cic.term, Cic.obj) GrafiteAst.command +type ast_command = Cic.obj GrafiteAst.command type moo = ast_command list val save_moo: fname:string -> moo -> unit -- 2.39.2