X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=cdf90c5b989883ff54a2e98d6a4c7e6c527901e8;hb=637114791874df9ebc4e0f0936513c71886a913f;hp=a98fb8e9d6cd70116d799750b65b06e285ba7bb4;hpb=5649890273cf8e660bba744e84ce5fee1e5efe69;p=helm.git diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index a98fb8e9d..cdf90c5b9 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -83,6 +83,27 @@ let pp_auto_params ~term_pp (univ, params) = else "" ;; +let pp_just ~term_pp = + function + `Term term -> "exact " ^ term_pp term + | `Auto params -> pp_auto_params ~term_pp params +;; + +let 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 + | NCase1 (_,n) -> "*" ^ n ^ ":" + | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ + " with " ^ CicNotationPp.pp_term wwhat + | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^ + assert false ^ " " ^ assert false + | NId _ -> "nid" + | NIntro (_,n) -> "#" ^ n + | NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false + | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ | NAuto _ -> assert false +;; + let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = let pp_terms = pp_terms ~term_pp in let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in @@ -108,13 +129,18 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = (* First order tactics *) | Absurd (_, term) -> "absurd" ^ term_pp term | Apply (_, term) -> "apply " ^ term_pp term + | ApplyRule (_, term) -> "apply rule " ^ term_pp term + | ApplyP (_, term) -> "applyP " ^ term_pp term | ApplyS (_, term, params) -> "applyS " ^ term_pp term ^ pp_auto_params ~term_pp params | AutoBatch (_,params) -> "autobatch " ^ pp_auto_params ~term_pp params | Assumption _ -> "assumption" - | Cases (_, term, specs) -> Printf.sprintf "cases " ^ term_pp term ^ - pp_intros_specs "names " specs + | Cases (_, term, pattern, specs) -> + Printf.sprintf "cases %s %s%s" + (term_pp term) + (pp_tactic_pattern pattern) + (pp_intros_specs "names " specs) | Change (_, where, with_what) -> Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what) | Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids) @@ -190,16 +216,16 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = (* 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 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^ + | Bydone (_, just) -> pp_just ~term_pp just ^ "done" + | By_just_we_proved (_, just, term1, ident, term2) -> pp_just ~term_pp just ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^ (match term2 with None -> " " | Some term2 -> term_pp term2) | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ (match ident with None -> "" | Some ident -> "(" ^ ident ^ ")") ^ (match term1 with None -> " " | Some term1 -> term_pp term1) | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on" ^ term_pp term ^ "to prove" ^ 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 " ^ (match term0 with None -> "_" | Some term -> term_pp term) ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ lazy_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 ^ ")" + | ExistsElim (_, just, ident, term, ident1, term1) -> pp_just ~term_pp just ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ lazy_term_pp term1 ^ "(" ^ ident1 ^ ")" + | AndElim (_, just, ident1, term1, ident2, term2) -> pp_just ~term_pp just ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")" | RewritingStep (_, term, term1, term2, cont) -> (match term with | None -> " " @@ -240,16 +266,34 @@ let pp_arg ~term_pp arg = else "(" ^ s ^ ")" -let pp_macro ~term_pp = +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 + let flavour_pp = function + | `Definition -> "definition" + | `Fact -> "fact" + | `Lemma -> "lemma" + | `Remark -> "remark" + | `Theorem -> "theorem" + | `Variant -> "variant" + | `Axiom -> "axiom" + | `MutualDefinition -> assert false in - let prefix_pp prefix = - if prefix = "" then "" else Printf.sprintf " \"%s\"" prefix + let pp_inline_params l = + let pp_param = function + | IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\"" + | IPAs flavour -> flavour_pp flavour + | IPProcedural -> "procedural" + | IPNoDefaults -> "nodefaults" + | IPDepth depth -> "depth = " ^ string_of_int depth + | IPLevel level -> "level = " ^ string_of_int level + | IPComments -> "comments" + | IPCoercions -> "coercions" + | IPDebug debug -> "debug = " ^ string_of_int debug + 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 (* Whelp *) | WInstance (_, term) -> "whelp instance " ^ term_pp term @@ -258,12 +302,14 @@ let pp_macro ~term_pp = | WElim (_, t) -> "whelp elim " ^ term_pp t | WMatch (_, term) -> "whelp match " ^ term_pp term (* real macros *) + | Eval (_, kind, term) -> + Printf.sprintf "eval %s on %s" (pp_reduction_kind kind) (term_pp term) | Check (_, term) -> Printf.sprintf "check %s" (term_pp term) | Hint (_, true) -> "hint rewrite" | Hint (_, false) -> "hint" | AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params - | Inline (_, style, suri, prefix) -> - Printf.sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix) + | Inline (_, suri, params) -> + Printf.sprintf "inline \"%s\"%s" suri (pp_inline_params params) let pp_associativity = function | Gramext.LeftA -> "left associative" @@ -281,18 +327,26 @@ let pp_default what uris = Printf.sprintf "default \"%s\" %s" what (String.concat " " (List.map UriManager.string_of_uri uris)) -let pp_coercion uri do_composites arity saturations= +let pp_coercion ~term_pp t do_composites arity saturations= Printf.sprintf "coercion %s %d %d %s" - (UriManager.string_of_uri uri) arity saturations + (term_pp t) arity saturations (if do_composites then "" else "nocomposites") let pp_command ~term_pp ~obj_pp = function | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri - | Coercion (_, uri, do_composites, i, j) -> - pp_coercion uri do_composites i j + | 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 + | Inverter (_,n,ty,params) -> + "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params + | UnificationHint (_,t, n) -> + "unification hint " ^ string_of_int n ^ " " ^ term_pp t | Default (_,what,uris) -> pp_default what uris | Drop _ -> "drop" - | Include (_,path) -> "include \"" ^ path ^ "\"" + | Include (_,true,path) -> "include \"" ^ path ^ "\"" + | Include (_,false,path) -> "include source \"" ^ path ^ "\"" | Obj (_,obj) -> obj_pp obj | Qed _ -> "qed" | Relation (_,id,a,aeq,refl,sym,trans) -> @@ -308,8 +362,12 @@ 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" + | NUnivConstraint (_) -> "not supported" + | NQed (_) -> "not supported" + | Pump (_) -> "not supported" -let pp_punctuation_tactical ~term_pp ~lazy_term_pp = +let pp_punctuation_tactical = function | Dot _ -> "." | Semicolon _ -> ";" @@ -319,7 +377,7 @@ let pp_punctuation_tactical ~term_pp ~lazy_term_pp = | Wildcard _ -> "*:" | Merge _ -> "]" -let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp = +let pp_non_punctuation_tactical = function | Focus (_, goals) -> Printf.sprintf "focus %s" (String.concat " " (List.map string_of_int goals)) @@ -328,15 +386,21 @@ let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp = let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = function - | Macro (_, macro) -> pp_macro ~term_pp macro ^ "." + | Macro (_, macro) -> pp_macro ~term_pp ~lazy_term_pp macro ^ "." | Tactic (_, Some tac, punct) -> - pp_tactic ~map_unicode_to_tex ~lazy_term_pp ~term_pp tac - ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct + pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp tac + ^ pp_punctuation_tactical punct | Tactic (_, None, punct) -> - pp_punctuation_tactical ~lazy_term_pp ~term_pp punct + pp_punctuation_tactical punct + | NTactic (_,tac, punct) -> + pp_ntactic ~map_unicode_to_tex tac + ^ pp_punctuation_tactical punct | NonPunctuationTactical (_, tac, punct) -> - pp_non_punctuation_tactical ~lazy_term_pp ~term_pp tac - ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct + pp_non_punctuation_tactical tac + ^ pp_punctuation_tactical punct + | NNonPunctuationTactical (_, tac, punct) -> + pp_non_punctuation_tactical tac + ^ pp_punctuation_tactical punct | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "." let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =