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