]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/sequentPp.ml
cicReductionNaif.ml was left out from the commit that introduced explicit
[helm.git] / 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 ;;