helm/gTopLevel/sequentPp.ml

   1 module TextualPp =
   2  struct
   3   (* It also returns the pretty-printing context! *)
   4   let print_context ctx =
   5    let module P = ProofEngine in
   6     let print_name =
   7      function
   8         Cic.Name n -> n
   9       | Cic.Anonimous -> "_"
  10     in
  11      List.fold_right
  12       (fun i env ->
  13         match i with
  14            (P.Declaration,n,t) ->
  15              print_endline (print_name n ^ ":" ^ CicPp.pp t env) ;
  16              flush stdout ;
  17              n::env
  18          | (P.Definition,n,t) ->
  19              print_endline (print_name n ^ ":=" ^ CicPp.pp t env) ;
  20              flush stdout ;
  21              n::env
  22       ) ctx []
  23   ;;
  24
  25   exception NotImplemented;;
  26
  27   let print_sequent (context,goal) =
  28    let module P = ProofEngine in
  29     print_newline () ;
  30     let pretty_printer_env_of_context =
  31      print_context context
  32     in
  33     print_endline "----------------------" ;
  34     print_endline (CicPp.pp goal pretty_printer_env_of_context) ; flush stdout
  35   ;;
  36  end
  37 ;;
  38
  39 module XmlPp =
  40  struct
  41   let print_sequent (context,goal) =
  42    let module X = Xml in
  43     X.xml_nempty "Sequent" []
  44      (let final_s,final_env =
  45        (List.fold_right
  46          (fun (b,n,t) (s,env) ->
  47            [< s ;
  48               X.xml_nempty
  49                (match b with
  50                    ProofEngine.Definition  -> "Definition"
  51                  | ProofEngine.Declaration -> "Declaration"
  52                ) ["name",(match n with Cic.Name n -> n | _ -> assert false)]
  53                (Cic2Xml.print_term
  54                  (UriManager.uri_of_string "cic:/dummy.con")
  55                  (let (acic,_,_) = Cic2acic.acic_of_cic_env env t in acic)) ;
  56            >],(n::env)
  57          ) context ([<>],[])
  58        )
  59       in
  60        [< final_s ;
  61           Xml.xml_nempty "Goal" []
  62            (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
  63              (let (acic,_,_) = Cic2acic.acic_of_cic_env final_env goal in acic))
  64        >]
  65      )
  66   ;;
  67  end
  68 ;;