let pres_sequent =
(Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in
let xmlpres = mpres_document pres_sequent in
- (* Xml.pp_to_outchan xmlpres stdout ; *)
- try
- Xml2Gdome.document_of_xml Misc.domImpl xmlpres, (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
- with
- e ->
- prerr_endline ("LUCA: eccezione in document_of_xml " ^ (Printexc.to_string e)) ;
- raise e
+ Xml2Gdome.document_of_xml Misc.domImpl xmlpres,
+ (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
;;
let mml_of_cic_object ~explode_all uri acic
- ids_to_inner_sorts ids_to_inner_types =
- match acic with
- Cic.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
- let time1 = Sys.time () in
- let content =
- Cic2content.annobj2content
- ~ids_to_inner_sorts ~ids_to_inner_types acic in
- (* ContentPp.print_obj content; *)
- let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
- let time2 = Sys.time () in
- (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *)
- let xmlpres = mpres_document pres in
- let time25 = Sys.time () in
- (* alternative: printing to file
- prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2)));
- Xml.pp xmlpres (Some "tmp");
- let time3 = Sys.time () in
- prerr_endline ("FINE valutazione e printing dello stream:" ^ (string_of_float (time3 -. time25)));
- end alternative *)
- (try
- Xml2Gdome.document_of_xml Misc.domImpl xmlpres
- with (GdomeInit.DOMException (_,s)) as e ->
- prerr_endline s; raise e)
- | _ -> assert false
+ ids_to_inner_sorts ids_to_inner_types
+=
+ let content =
+ Cic2content.annobj2content ~ids_to_inner_sorts ~ids_to_inner_types acic
+ in
+ let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
+ let xmlpres = mpres_document pres in
+ Xml2Gdome.document_of_xml Misc.domImpl xmlpres
;;
-(*
-let _ =
- Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount
-;;
-*)
-
| [] -> box
| _ -> Box.H ([], box :: (List.map (fun t -> Box.Text ([], t)) tail))
+let rec find_symbol idref = function
+ | A.AttributedTerm (`Loc _, t) -> find_symbol None t
+ | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
+ | A.Symbol (name, _) -> `Symbol (name, idref)
+ | _ -> `None
+
let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
(t, ids_to_uris)
=
| A.AttributedTerm (`IdRef xref, t) -> bigast2box ~xref ~tail t
| A.Appl [] -> assert false
| A.Appl ((hd::tl) as l) ->
- let rec find_symbol idref = function
- | A.AttributedTerm (`Loc _, t) -> find_symbol None t
- | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
- | A.Symbol (name, _) ->
- (match idref with
- | None -> assert false
- | Some idref -> `Symbol (name, idref))
- | _ -> `None
- in
let aattr = make_attributes [Some "helm","xref"] [xref] in
(match find_symbol None hd with
| `Symbol (name, sxref) ->
- let sattr = make_std_attributes (Some sxref) in
+ let sattr = make_std_attributes sxref in
(try
(let f = Hashtbl.find symbol_table_charcount name in
f tl ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr)
Box.smallskip;
Box.Text([],map_tex unicode "Rightarrow");
Box.smallskip;
- Box.Object([],rhs)]) in
- let plbox = match pl with
- [] -> Box.Text([],"[]")
+ append_tail ~tail (Box.Object([],rhs))]) in
+ let plbox =
+ match pl with
+ [] -> append_tail ~tail (Box.Text([],"[]"))
| r::tl ->
Box.V([],
(make_rule ~tail:[] "[" r) ::
(make_args
- (fun ~tail pat -> make_rule ~tail:[] "|" pat)
+ (fun ~tail pat -> make_rule ~tail "|" pat)
~tail:("]" :: tail)
tl))
in
match ty with
| Some ty ->
[ Box.H([],[Box.Text([],"[");
- ast2box ~tail ty;
+ ast2box ~tail:[] ty;
Box.Text([],"]")]) ]
| None -> []
in
Box.V(make_attributes [Some "helm","xref"] [xref],
ty_box @
[Box.Text([],"match");
- Box.indent (Box.H([],[Box.skip; bigast2box ~tail arg]));
+ Box.indent (Box.H([],[Box.skip; bigast2box ~tail:[] arg]));
Box.Text([],"with");
Box.indent plbox])
else
[Box.H(make_attributes [Some "helm","xref"] [xref],
[Box.Text([],"match");
Box.smallskip;
- ast2box ~tail arg;
+ ast2box ~tail:[] arg;
Box.smallskip;
Box.Text([],"with")]);
Box.indent plbox])
let definitions =
let rec make_defs let_txt = function
[] -> []
- | [(var,s,_)] ->
- make_def let_txt var s "in"
+ | [(var,s,_)] -> make_def let_txt var s "in"
| (var,s,_)::tl ->
(make_def let_txt var s "")@(make_defs "and" tl) in
make_defs "let rec" vars in
| A.UserInput -> P.Mtext([], "")
| A.Appl [] -> assert false
| A.Appl ((hd::tl) as l) ->
- let rec find_symbol idref = function
- | A.AttributedTerm (`Loc _, t) -> find_symbol None t
- | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
- | A.Symbol (name, _) ->
- (match idref with
- | None -> assert false
- | Some idref -> `Symbol (name, idref))
- | term ->
- `None
- in
let aattr = make_attributes [Some "helm","xref"] [xref] in
(match find_symbol None hd with
| `Symbol (name, sxref) ->
- let sattr = make_std_attributes (Some sxref) in
+ let sattr = make_std_attributes sxref in
(try
(let f = Hashtbl.find symbol_table name in
f tl ~priority ~assoc ~ids_to_uris aattr sattr)
let lhs =
P.Mtext([], constr) ::
(List.concat
- (List.map (fun var -> P.smallskip :: make_capture_variable var)
+ (List.map
+ (fun var -> P.smallskip :: make_capture_variable var)
vars))
in
lhs @
add_binary_op "times" 70 (`Ascii "*");
add_binary_op "minus" 60 (`Ascii "-");
add_binary_op "div" 60 (`Ascii "/");
+ add_binary_op "cast" 80 (`Ascii ":");
exception ToDo;;
-let aaa = ref 0
+let counter = ref 0
+
+let conjecture2pres term2pres (id, n, context, ty) =
+ (B.b_h [Some "helm", "xref", id]
+ (((List.map
+ (function
+ | None ->
+ B.b_h []
+ [ B.b_object (p_mi [] "_") ;
+ B.b_object (p_mo [] ":?") ;
+ B.b_object (p_mi [] "_")]
+ | Some (`Declaration d)
+ | Some (`Hypothesis d) ->
+ let { Content.dec_name =
+ dec_name ; Content.dec_type = ty } = d
+ in
+ B.b_h []
+ [ B.b_object
+ (p_mi []
+ (match dec_name with
+ None -> "_"
+ | Some n -> n));
+ B.b_text [] ":";
+ term2pres ty ]
+ | Some (`Definition d) ->
+ let
+ { Content.def_name = def_name ;
+ Content.def_term = bo } = d
+ in
+ B.b_h []
+ [ B.b_object (p_mi []
+ (match def_name with
+ None -> "_"
+ | Some n -> n)) ;
+ B.b_text [] ":=" ;
+ term2pres bo]
+ | Some (`Proof p) ->
+ let proof_name = p.Content.proof_name in
+ B.b_h []
+ [ B.b_object (p_mi []
+ (match proof_name with
+ None -> "_"
+ | Some n -> n)) ;
+ B.b_text [] ":=" ;
+ proof2pres term2pres p])
+ (List.rev context)) @
+ [ B.b_text [] "|-" ;
+ B.b_object (p_mi [] (string_of_int n)) ;
+ B.b_text [] ":" ;
+ term2pres ty ])))
+
+let metasenv2pres term2pres = function
+ | None -> []
+ | Some metasenv' ->
+ (* Conjectures are in their own table to make *)
+ (* diffing the DOM trees easier. *)
+ [B.b_v []
+ ((B.b_text []
+ ("Conjectures:" ^
+ (let _ = incr counter; in (string_of_int !counter)))) ::
+ (List.map (conjecture2pres term2pres) metasenv'))]
+
+let get_name = function
+ | Some s -> s
+ | None -> "_"
+
+let pp_params = function
+ | [] -> ""
+ | params ->
+ " (" ^
+ String.concat " ; " (List.map UriManager.string_of_uri params) ^
+ ")"
let content2pres term2pres (id,params,metasenv,obj) =
- let module K = Content in
- match obj with
- `Def (K.Const,thesis,`Proof p) ->
- B.b_v
- [None,"helm:xref","id"]
- ([B.b_text [] ("UNFINISHED PROOF " ^ id ^"(" ^ String.concat " ; " (List.map UriManager.string_of_uri params)^ ")") ;
- B.b_text [] "THESIS:" ;
- B.indent (term2pres thesis)] @
- (match metasenv with
- None -> []
- | Some metasenv' ->
- (* Conjectures are in their own table to make *)
- (* diffing the DOM trees easier. *)
- (B.b_v []
- ((B.b_text [] ("CONJECTURES:" ^ (let _ = incr aaa; in (string_of_int !aaa))))::
- (List.map
- (function
- (id,n,context,ty) ->
- (B.b_h [Some "helm", "xref", id]
- (((List.map
- (function
- None ->
- B.b_h []
- [ B.b_object (p_mi [] "_") ;
- B.b_object (p_mo [] ":?") ;
- B.b_object (p_mi [] "_")]
- | Some (`Declaration d)
- | Some (`Hypothesis d) ->
- let
- { K.dec_name = dec_name ;
- K.dec_type = ty } = d
- in
- B.b_h []
- [ B.b_object (p_mi []
- (match dec_name with
- None -> "_"
- | Some n -> n)) ;
- B.b_text [] ":" ;
- term2pres ty]
- | Some (`Definition d) ->
- let
- { K.def_name = def_name ;
- K.def_term = bo } = d
- in
- B.b_h []
- [ B.b_object (p_mi []
- (match def_name with
- None -> "_"
- | Some n -> n)) ;
- B.b_text [] ":=" ;
- term2pres bo]
- | Some (`Proof p) ->
- let proof_name = p.K.proof_name in
- B.b_h []
- [ B.b_object (p_mi []
- (match proof_name with
- None -> "_"
- | Some n -> n)) ;
- B.b_text [] ":=" ;
- proof2pres term2pres p]
- ) (List.rev context)) @
- [ B.b_text [] "|-" ;
- B.b_object (p_mi [] (string_of_int n)) ;
- B.b_text [] ":" ;
- term2pres ty ])
- ))
- ) metasenv'))
- )::[proof2pres term2pres p]
- )
- )
- | _ -> raise ToDo
+ match obj with
+ | `Def (Content.Const, thesis, `Proof p) ->
+ let name = get_name p.Content.proof_name in
+ B.b_v
+ [None,"helm:xref","id"]
+ ([ B.b_text [] ("Proof " ^ name ^ pp_params params);
+ B.b_text [] "Thesis:";
+ B.indent (term2pres thesis) ] @
+ metasenv2pres term2pres metasenv @
+ [proof2pres term2pres p])
+ | `Def (_, ty, `Definition body) ->
+ let name = get_name body.Content.def_name in
+ B.b_v
+ [None,"helm:xref","id"]
+ ([B.b_text [] ("Definition " ^ name ^ pp_params params);
+ B.b_text [] "Type:";
+ B.indent (term2pres ty)] @
+ metasenv2pres term2pres metasenv @
+ [term2pres body.Content.def_term])
+ | `Decl (_, `Declaration decl)
+ | `Decl (_, `Hypothesis decl) ->
+ let name = get_name decl.Content.dec_name in
+ B.b_v
+ [None,"helm:xref","id"]
+ ([B.b_text [] ("Axiom " ^ name ^ pp_params params);
+ B.b_text [] "Type:";
+ B.indent (term2pres decl.Content.dec_type)] @
+ metasenv2pres term2pres metasenv)
+ | _ -> raise ToDo
;;
(*
projects / helm.git / commitdiff