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 binding (s,env) ->
  55            let b,n,t,cicbinding =
  56             match binding with
  57                ProofEngine.Definition  (n,t) -> "Def", n, t,Cic.Def t
  58              | ProofEngine.Declaration (n,t) -> "Decl", n, t, Cic.Decl t
  59            in
  60             let acic = acic_of_cic_env env t in
  61              [< s ;
  62                 X.xml_nempty b
  63                  ["name",(match n with Cic.Name n -> n | _ -> assert false)]
  64                  (Cic2Xml.print_term
  65                    (UriManager.uri_of_string "cic:/dummy.con")
  66                    ids_to_inner_sorts acic)
  67              >],((n,cicbinding)::env)
  68          ) context ([<>],[])
  69        )
  70       in
  71        let acic = acic_of_cic_env final_env goal in
  72         X.xml_nempty "Sequent" []
  73          [< final_s ;
  74             Xml.xml_nempty "Goal" []
  75              (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
  76                ids_to_inner_sorts acic)
  77          >],
  78          ids_to_terms,ids_to_father_ids
  79   ;;
  80  end
  81 ;;