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