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
46 let ids_to_hypotheses = Hashtbl.create 11 in
47 let hypotheses_seed = ref 0 in
49 let acic_of_cic_context =
50 Cic2acic.acic_of_cic_context' seed ids_to_terms ids_to_father_ids
51 ids_to_inner_sorts ids_to_inner_types metasenv
55 (fun binding (s,context) ->
56 let hid = "h" ^ string_of_int !hypotheses_seed in
57 Hashtbl.add ids_to_hypotheses hid binding ;
58 incr hypotheses_seed ;
60 (Some (n,(Cic.Def t as b)) as entry)
61 | (Some (n,(Cic.Decl t as b)) as entry) ->
62 let acic = acic_of_cic_context context t in
65 (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
66 ["name",(match n with Cic.Name n -> n | _ -> assert false);
69 (UriManager.uri_of_string "cic:/dummy.con")
70 ids_to_inner_sorts acic)
73 [< s ; X.xml_empty "Hidden" [] >], (None::context)
77 let acic = acic_of_cic_context context goal in
78 X.xml_nempty "Sequent" ["no",string_of_int metano]
80 Xml.xml_nempty "Goal" []
81 (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
82 ids_to_inner_sorts acic)
84 ids_to_terms,ids_to_father_ids,ids_to_hypotheses