3 (* It also returns the pretty-printing context! *)
4 let print_context ctx =
11 (fun i (output,context) ->
12 let (newoutput,context') =
14 Some (n,Cic.Decl t) ->
15 print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context
16 | Some (n,Cic.Def t) ->
17 print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context
19 "_ ?= _\n", None::context
21 output^newoutput,context'
25 exception NotImplemented;;
27 let print_sequent (metano,context,goal) =
28 let module P = ProofEngine in
30 let (output,pretty_printer_context_of_context) = print_context context in
32 "---------------------- ?" ^ string_of_int metano ^ "\n" ^
33 CicPp.pp goal pretty_printer_context_of_context
40 let print_sequent metasenv (metano,context,goal) =
42 let ids_to_terms = Hashtbl.create 503 in
43 let ids_to_father_ids = Hashtbl.create 503 in
44 let ids_to_inner_sorts = Hashtbl.create 503 in
45 let ids_to_inner_types = Hashtbl.create 503 in
47 let acic_of_cic_context =
48 Cic2acic.acic_of_cic_context' seed ids_to_terms ids_to_father_ids
49 ids_to_inner_sorts ids_to_inner_types metasenv
53 (fun binding (s,context) ->
55 (Some (n,(Cic.Def t as b)) as entry)
56 | (Some (n,(Cic.Decl t as b)) as entry) ->
57 let acic = acic_of_cic_context context t in
60 (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
61 ["name",(match n with Cic.Name n -> n | _ -> assert false)]
63 (UriManager.uri_of_string "cic:/dummy.con")
64 ids_to_inner_sorts acic)
67 [< s ; X.xml_empty "Hidden" [] >], (None::context)
71 let acic = acic_of_cic_context context goal in
72 X.xml_nempty "Sequent" ["no",string_of_int metano]
74 Xml.xml_nempty "Goal" []
75 (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
76 ids_to_inner_sorts acic)
78 ids_to_terms,ids_to_father_ids