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 metasenv (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            let (acic,_,_,ids_to_inner_sorts,_) =
  48             Cic2acic.acic_of_cic_env metasenv env t
  49            in
  50             [< s ;
  51                X.xml_nempty
  52                 (match b with
  53                     ProofEngine.Definition  -> "Def"
  54                   | ProofEngine.Declaration -> "Decl"
  55                 ) ["name",(match n with Cic.Name n -> n | _ -> assert false)]
  56                 (Cic2Xml.print_term
  57                   (UriManager.uri_of_string "cic:/dummy.con")
  58                   ids_to_inner_sorts acic)
  59             >],((n,t)::env) (* CSC: sbagliato!!! Giusto solo se Declaration! *)
  60          ) context ([<>],[])
  61        )
  62       in
  63        let (acic,_,_,ids_to_inner_sorts,_) =
  64         Cic2acic.acic_of_cic_env metasenv final_env goal
  65        in
  66         [< final_s ;
  67            Xml.xml_nempty "Goal" []
  68             (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
  69               ids_to_inner_sorts acic)
  70         >]
  71      )
  72   ;;
  73  end
  74 ;;