X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=2cd7a4f4fcddfee286d115b84ff79c5a18cee9ad;hb=72cd94b68037956a70b98cfa54f316fd54e52bae;hp=22e4cbe09e19348aab695521a9947693bcfdaf4a;hpb=4b6193be548c96964beee706b75a06e269eed88d;p=helm.git diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 22e4cbe09..2cd7a4f4f 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -89,7 +89,7 @@ let pp_just ~term_pp = | `Auto params -> pp_auto_params ~term_pp params ;; -let pp_ntactic ~map_unicode_to_tex = function +let rec pp_ntactic ~map_unicode_to_tex = function | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^ assert false ^ " " ^ assert false @@ -100,6 +100,30 @@ let pp_ntactic ~map_unicode_to_tex = function assert false ^ " " ^ assert false | NId _ -> "nid" | NIntro (_,n) -> "#" ^ n + | NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false + | NAuto (_,(l,flgs)) -> + "nauto" ^ + (if l <> [] then (" by " ^ + (String.concat "," (List.map CicNotationPp.pp_term l))) else "") ^ + String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs) + | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> assert false + | NDot _ -> "##." + | NSemicolon _ -> "##;" + | NBranch _ -> "##[" + | NShift _ -> "##|" + | NPos (_, l) -> "##" ^String.concat "," (List.map string_of_int l)^ ":" + | NWildcard _ -> "##*:" + | NMerge _ -> "##]" + | NFocus (_,l) -> + Printf.sprintf "##focus %s" + (String.concat " " (List.map string_of_int l)) + | NUnfocus _ -> "##unfocus" + | NSkip _ -> "##skip" + | NTry (_,tac) -> "ntry " ^ pp_ntactic ~map_unicode_to_tex tac + | NAssumption _ -> "nassumption" + | NBlock (_,l) -> + "(" ^ String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) l)^ ")" + | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic ~map_unicode_to_tex t ;; let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = @@ -266,24 +290,31 @@ let pp_arg ~term_pp arg = let pp_macro ~term_pp ~lazy_term_pp = let term_pp = pp_arg ~term_pp in - let style_pp = function - | Declarative -> "" - | Procedural None -> "procedural " - | Procedural (Some i) -> Printf.sprintf "procedural %u " i - in - let prefix_pp prefix = - if prefix = "" then "" else Printf.sprintf " \"%s\"" prefix - in let flavour_pp = function - | None -> "" - | Some `Definition -> " as definition" - | Some `MutualDefinition -> " as mutual" - | Some `Fact -> " as fact" - | Some `Lemma -> " as lemma" - | Some `Remark -> " as remark" - | Some `Theorem -> " as theorem" - | Some `Variant -> " as variant" - | Some `Axiom -> " as axiom" + | `Definition -> "definition" + | `Fact -> "fact" + | `Lemma -> "lemma" + | `Remark -> "remark" + | `Theorem -> "theorem" + | `Variant -> "variant" + | `Axiom -> "axiom" + | `MutualDefinition -> assert false + in + let pp_inline_params l = + let pp_param = function + | IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\"" + | IPAs flavour -> flavour_pp flavour + | IPCoercions -> "coercions" + | IPDebug debug -> "debug = " ^ string_of_int debug + | IPProcedural -> "procedural" + | IPNoDefaults -> "nodefaults" + | IPDepth depth -> "depth = " ^ string_of_int depth + | IPLevel level -> "level = " ^ string_of_int level + | IPComments -> "comments" + | IPCR -> "cr" + in + let s = String.concat " " (List.map pp_param l) in + if s = "" then s else " " ^ s in let pp_reduction_kind = pp_reduction_kind ~term_pp:lazy_term_pp in function @@ -300,8 +331,8 @@ let pp_macro ~term_pp ~lazy_term_pp = | Hint (_, true) -> "hint rewrite" | Hint (_, false) -> "hint" | AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params - | Inline (_, style, suri, prefix, flavour) -> - Printf.sprintf "inline %s\"%s\"%s%s" (style_pp style) suri (prefix_pp prefix) (flavour_pp flavour) + | Inline (_, suri, params) -> + Printf.sprintf "inline \"%s\"%s" suri (pp_inline_params params) let pp_associativity = function | Gramext.LeftA -> "left associative" @@ -323,18 +354,29 @@ let pp_coercion ~term_pp t do_composites arity saturations= Printf.sprintf "coercion %s %d %d %s" (term_pp t) arity saturations (if do_composites then "" else "nocomposites") + +let pp_ncommand = function + | UnificationHint (_,t, n) -> + "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t + | NObj (_,_) + | NUnivConstraint (_) -> "not supported" + | NCoercion (_) -> "not supported" + | NQed (_) -> "nqed" let pp_command ~term_pp ~obj_pp = function | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri + | Select (_,uri) -> "Selecting " ^ UriManager.string_of_uri uri | Coercion (_, t, do_composites, i, j) -> pp_coercion ~term_pp t do_composites i j | PreferCoercion (_,t) -> "prefer coercion " ^ term_pp t - | UnificationHint (_,t, n) -> - "unification hint " ^ string_of_int n ^ " " ^ term_pp t + | Inverter (_,n,ty,params) -> + "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params | Default (_,what,uris) -> pp_default what uris | Drop _ -> "drop" - | Include (_,path) -> "include \"" ^ path ^ "\"" + | Include (_,true,`OldAndNew,path) -> "include \"" ^ path ^ "\"" + | Include (_,false,`OldAndNew,path) -> "include source \"" ^ path ^ "\"" + | Include (_,_,`New,path) -> "RECURSIVELY INCLUDING " ^ path | Obj (_,obj) -> obj_pp obj | Qed _ -> "qed" | Relation (_,id,a,aeq,refl,sym,trans) -> @@ -350,7 +392,7 @@ let pp_command ~term_pp ~obj_pp = function | None -> "") | Print (_,s) -> "print " ^ s | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value - | NObj (_,o) -> "not supported" + | Pump (_) -> "not supported" let pp_punctuation_tactical = function @@ -377,13 +419,13 @@ let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = ^ pp_punctuation_tactical punct | Tactic (_, None, punct) -> pp_punctuation_tactical punct - | NTactic (_,tac, punct) -> - pp_ntactic ~map_unicode_to_tex tac - ^ pp_punctuation_tactical punct + | NTactic (_,tacl) -> + String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) tacl) | NonPunctuationTactical (_, tac, punct) -> pp_non_punctuation_tactical tac ^ pp_punctuation_tactical punct | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "." + | NCommand (_, cmd) -> pp_ncommand cmd ^ "." let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = function