X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=e022c6f33114c122bac42f2e1ba6e6a99918b3d7;hb=f1fc99e982ca6c9c939504c4dcf773edf582792a;hp=cf9106ea374d44527481c5e12297be63ee52f9f2;hpb=1ca749a387695a5a4abc138a06de496a63abac4a;p=helm.git diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index cf9106ea3..e022c6f33 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -73,6 +73,77 @@ let pp_terms ~term_pp terms = String.concat ", " (List.map term_pp terms) let opt_string_pp = function | None -> "" | Some what -> what ^ " " + +let pp_auto_params ~term_pp (univ, params) = + String.concat " " + (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) ^ + if univ <> [] then + (if params <> [] then " " else "") ^ "by " ^ + String.concat " " (List.map term_pp univ) + else "" +;; + +let pp_just ~term_pp = + function + `Term term -> "exact " ^ term_pp term + | `Auto params -> pp_auto_params ~term_pp params +;; + +let rec pp_ntactic ~map_unicode_to_tex = + let term_pp = CicNotationPp.pp_term in + let lazy_term_pp = fun _ -> assert false in + let pp_tactic_pattern = + pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in + function + | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t + | 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) + | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^ + assert false ^ " " ^ assert false + | NConstructor (_,None,l) -> "@ " ^ + String.concat " " (List.map CicNotationPp.pp_term l) + | NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^ + String.concat " " (List.map CicNotationPp.pp_term l) + | NCase1 (_,n) -> "*" ^ n ^ ":" + | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ + " with " ^ CicNotationPp.pp_term wwhat + | NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t +(*| NDiscriminate (_,t) -> "ndiscriminate " ^ CicNotationPp.pp_term t + | NSubst (_,t) -> "nsubst " ^ CicNotationPp.pp_term t *) + | NDestruct _ -> "ndestruct" + | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^ + assert false ^ " " ^ assert false + | NId _ -> "nid" + | NIntro (_,n) -> "#" ^ n + | NInversion (_,what,where) -> "ninversion " ^ CicNotationPp.pp_term what ^ + assert false ^ " " ^ assert false + | NLApply (_,t) -> "lapply " ^ CicNotationPp.pp_term t + | NRewrite (_,dir,n,where) -> "nrewrite " ^ + (match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^ + " " ^ CicNotationPp.pp_term n ^ " " ^ pp_tactic_pattern where + | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> "TO BE IMPLEMENTED" + | NDot _ -> "##." + | NSemicolon _ -> "##;" + | NBranch _ -> "##[" + | NShift _ -> "##|" + | NPos (_, l) -> "##" ^String.concat "," (List.map string_of_int l)^ ":" + | NPosbyname (_, s) -> "##" ^ s ^ ":" + | 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 = let pp_terms = pp_terms ~term_pp in @@ -99,16 +170,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 ^ - String.concat " " - (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) - | AutoBatch (_,params) -> "auto batch " ^ - String.concat " " - (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) 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) @@ -126,7 +199,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = | Decompose (_, names) -> Printf.sprintf "decompose%s" (pp_intros_specs "names " (None, names)) - | Demodulate _ -> "demodulate" + | Demodulate (_, params) -> "demodulate " ^ pp_auto_params ~term_pp params | Destruct (_, None) -> "destruct" | Destruct (_, Some terms) -> "destruct " ^ pp_terms terms | Elim (_, what, using, pattern, specs) -> @@ -184,17 +257,30 @@ 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 ^ ")" - | RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some (None,term) -> "conclude " ^ term_pp term | Some (Some name,term) -> "obtain (" ^ name ^ ") " ^ term_pp term) ^ "=" ^ term_pp term1 ^ " by " ^ (match term2 with `Auto params -> "_" ^ String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | `Term term2 -> term_pp term2 | `Proof -> "proof") ^ (if cont then " done" else "") + | 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 -> " " + | Some (None,term) -> "conclude " ^ term_pp term + | Some (Some name,term) -> + "obtain (" ^ name ^ ") " ^ term_pp term) + ^ "=" ^ + term_pp term1 ^ + (match term2 with + | `Auto params -> pp_auto_params ~term_pp params + | `Term term2 -> " exact " ^ term_pp term2 + | `Proof -> " proof" + | `SolveWith term -> " using " ^ term_pp term) + ^ (if cont then " done" else "") | Case (_, id, args) -> "case" ^ id ^ String.concat " " @@ -221,16 +307,40 @@ let pp_arg ~term_pp arg = else "(" ^ s ^ ")" -let pp_macro ~term_pp = +let pp_nmacro = function + | NCheck (_, term) -> Printf.sprintf "ncheck %s" (CicNotationPp.pp_term term) + | Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name +;; + +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 + | 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 (* Whelp *) | WInstance (_, term) -> "whelp instance " ^ term_pp term @@ -239,14 +349,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 " ^ - String.concat " " - (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) - | Inline (_, style, suri, prefix) -> - Printf.sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix) + | AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params + | Inline (_, suri, params) -> + Printf.sprintf "inline \"%s\"%s" suri (pp_inline_params params) let pp_associativity = function | Gramext.LeftA -> "left associative" @@ -255,27 +365,46 @@ let pp_associativity = function let pp_precedence i = Printf.sprintf "with precedence %d" i -let pp_dir_opt = function - | None -> "" - | Some `LeftToRight -> "> " - | Some `RightToLeft -> "< " - 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= - Printf.sprintf "coercion %s %d %d (* %s *)" - (UriManager.string_of_uri uri) arity saturations - (if do_composites then "compounds" else "no compounds") +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 + | NDiscriminator (_,_) + | NInverter (_,_,_,_,_) + | NObj (_,_) + | NUnivConstraint (_) -> "not supported" + | NCoercion (_) -> "not supported" + | NQed (_) -> "nqed" + | NCopy (_,name,uri,map) -> + "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ + String.concat " and " + (List.map + (fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b) + map) +;; 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 | 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) -> @@ -291,8 +420,9 @@ let pp_command ~term_pp ~obj_pp = function | None -> "") | Print (_,s) -> "print " ^ s | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value + | Pump (_) -> "not supported" -let pp_punctuation_tactical ~term_pp ~lazy_term_pp = +let pp_punctuation_tactical = function | Dot _ -> "." | Semicolon _ -> ";" @@ -302,7 +432,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)) @@ -311,16 +441,20 @@ 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 ^ "." + | NMacro (_, macro) -> pp_nmacro 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 (_,tacl) -> + String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) tacl) | 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 | 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