X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite%2FgrafiteAstPp.ml;h=8bd5c96f15862677345877c9487e4ce6a96c5501;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=7687bc5222235543bd6da28bd876f6253710b54f;hpb=a58d25c192ff13ecee2cb92f07ee6f1cbe5219b5;p=helm.git diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml index 7687bc522..8bd5c96f1 100644 --- a/helm/ocaml/grafite/grafiteAstPp.ml +++ b/helm/ocaml/grafite/grafiteAstPp.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open GrafiteAst @@ -31,32 +33,30 @@ 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 + | `Demodulate -> "demodulate" | `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 +64,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,32 +94,33 @@ 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" + | Inversion (_, term) -> "inversion " ^ term_pp term | Intros (_, num, idents) -> sprintf "intros%s%s" (match num with None -> "" | Some num -> " " ^ string_of_int num) @@ -122,26 +128,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,50 +156,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) -> - sprintf "alias symbol \"%s\" (instance %d) = \"%s\"" - symb instance desc - | Number_alias (instance,desc) -> - sprintf "alias num (instance %d) = \"%s\"" instance desc - -let pp_argument_pattern = function - | CicNotationPt.IdentArg (eta_depth, name) -> - let eta_buf = Buffer.create 5 in - for i = 1 to eta_depth do - Buffer.add_string eta_buf "\\eta." - done; - sprintf "%s%s" (Buffer.contents eta_buf) name - -let pp_l1_pattern = CicNotationPp.pp_term -let pp_l2_pattern = CicNotationPp.pp_term - let pp_associativity = function | Gramext.LeftA -> "left associative" | Gramext.RightA -> "right associative" @@ -206,48 +185,38 @@ let pp_dir_opt = function | Some `LeftToRight -> "> " | Some `RightToLeft -> "< " -let pp_metadata = - function - | Dependency buri -> sprintf "dependency %s" buri - | Baseuri buri -> sprintf "baseuri %s" buri +let pp_default what uris = + sprintf "default \"%s\" %s" what + (String.concat " " (List.map UriManager.string_of_uri uris)) -let pp_command = function +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 ~obj_pp = function | Include (_,path) -> "include " ^ path | Qed _ -> "qed" | Drop _ -> "drop" | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value - | Coercion (_,term, _do_composites) -> - sprintf "coercion %s" (pp_term_ast term) - | Alias (_,s) -> pp_alias s - | Obj (_,obj) -> CicNotationPp.pp_obj obj + | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites + | Obj (_,obj) -> obj_pp obj | Default (_,what,uris) -> - sprintf "default \"%s\" %s" what - (String.concat " " (List.map UriManager.string_of_uri uris)) - | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) -> - sprintf "interpretation \"%s\" '%s %s = %s" - dsc symbol - (String.concat " " (List.map pp_argument_pattern arg_patterns)) - (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern) - | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) -> - sprintf "notation %s\"%s\" %s %s for %s" - (pp_dir_opt dir_opt) - (pp_l1_pattern l1_pattern) - (pp_associativity assoc) - (pp_precedence prec) - (pp_l2_pattern l2_pattern) - | Metadata (_, m) -> sprintf "metadata %s" (pp_metadata m) - | Render _ - | Dump _ -> assert false (* ZACK: debugging *) + pp_default what uris -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 _ -> "." @@ -261,44 +230,25 @@ let rec pp_tactical = function | Unfocus _ -> "unfocus" | Skip _ -> "skip" -and pp_tacticals ~sep tacs = String.concat sep (List.map pp_tactical tacs) +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_tactical tac = pp_tactical tac -let pp_tactic tac = pp_tactic tac -let pp_command tac = pp_command tac - -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 - -let pp_cic_command = function - | Include (_,path) -> "include " ^ path - | Qed _ -> "qed" - | Drop _ -> "drop" - | Coercion (_,term,_add_composites) -> - sprintf "coercion %s" (CicPp.ppterm term) - | Set _ - | Alias _ - | Default _ - | Render _ - | Dump _ - | Interpretation _ - | Metadata _ - | Notation _ - | Obj _ -> assert false (* not implemented *) - -let pp_dependency = function - | IncludeDep str -> "include \"" ^ str ^ "\"" - | BaseuriDep str -> "set \"baseuri\" \"" ^ str ^ "\"" - | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\"" + | 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