X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=5f89df9d6ebca083064425ca71598719650905b0;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=ba9f87abd2bd6c777efd8894a7ef4d32179db7b6;hpb=640de42807566c08248ade7cfc92851bebc31d74;p=helm.git diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index ba9f87abd..5f89df9d6 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -77,10 +77,10 @@ let opt_string_pp = function 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 "" + match univ with + | None -> "" + | Some l -> (if params <> [] then " " else "") ^ "by " ^ + String.concat " " (List.map term_pp l) ;; let pp_just ~term_pp = @@ -89,24 +89,63 @@ 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 = + 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 + | NSmartApply (_,t) -> "fixme" + | NAuto (_,(None,flgs)) -> + "nautobatch" ^ + String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs) + | NAuto (_,(Some l,flgs)) -> + "nautobatch" ^ " by " ^ + (String.concat "," (List.map CicNotationPp.pp_term l)) ^ + 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 (_,dom,skip) -> "ndestruct ..." | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^ 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 + | 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 = @@ -271,6 +310,11 @@ let pp_arg ~term_pp arg = else "(" ^ s ^ ")" +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 flavour_pp = function @@ -324,11 +368,6 @@ 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)) @@ -337,6 +376,23 @@ 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 ~obj_pp = function + | UnificationHint (_,t, n) -> + "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t + | NDiscriminator (_,_) + | NInverter (_,_,_,_,_) + | NUnivConstraint (_) -> "not supported" + | NCoercion (_) -> "not supported" + | NObj (_,obj) -> obj_pp obj + | 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 @@ -347,12 +403,11 @@ let pp_command ~term_pp ~obj_pp = function "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 (_,true,path) -> "include \"" ^ path ^ "\"" - | Include (_,false,path) -> "include source \"" ^ 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) -> @@ -368,9 +423,6 @@ let pp_command ~term_pp ~obj_pp = function | None -> "") | Print (_,s) -> "print " ^ s | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value - | NObj (_,_) - | NUnivConstraint (_) -> "not supported" - | NQed (_) -> "nqed" | Pump (_) -> "not supported" let pp_punctuation_tactical = @@ -392,22 +444,22 @@ let pp_non_punctuation_tactical = let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = function + | 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 ~term_pp ~lazy_term_pp tac ^ 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 - | NNonPunctuationTactical (_, tac, punct) -> - pp_non_punctuation_tactical tac - ^ pp_punctuation_tactical punct | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "." + | NCommand (_, cmd) -> + let obj_pp = Obj.magic obj_pp in + pp_ncommand ~obj_pp cmd ^ "." let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = function