termEditor.cmx: disambiguatingParser.cmx termEditor.cmi
texTermEditor.cmo: disambiguatingParser.cmi texTermEditor.cmi
texTermEditor.cmx: disambiguatingParser.cmx texTermEditor.cmi
-chosenTransformer.cmo: chosenTransformer.cmi
-chosenTransformer.cmx: chosenTransformer.cmi
termViewer.cmo: logicalOperations.cmi termViewer.cmi
termViewer.cmx: logicalOperations.cmx termViewer.cmi
invokeTactics.cmo: logicalOperations.cmi proofEngine.cmi termEditor.cmi \
chosenTermEditor.cmx: termEditor.cmx chosenTermEditor.cmi
helmGtkLogger.cmo: helmGtkLogger.cmi
helmGtkLogger.cmx: helmGtkLogger.cmi
-gTopLevel.cmo: chosenTermEditor.cmi chosenTransformer.cmi \
- disambiguatingParser.cmi hbugs.cmi helmGtkLogger.cmi invokeTactics.cmi \
- logicalOperations.cmi proofEngine.cmi termEditor.cmi termViewer.cmi
-gTopLevel.cmx: chosenTermEditor.cmx chosenTransformer.cmx \
- disambiguatingParser.cmx hbugs.cmx helmGtkLogger.cmx invokeTactics.cmx \
- logicalOperations.cmx proofEngine.cmx termEditor.cmx termViewer.cmx
+gTopLevel.cmo: chosenTermEditor.cmi disambiguatingParser.cmi hbugs.cmi \
+ helmGtkLogger.cmi invokeTactics.cmi logicalOperations.cmi proofEngine.cmi \
+ termEditor.cmi termViewer.cmi
+gTopLevel.cmx: chosenTermEditor.cmx disambiguatingParser.cmx hbugs.cmx \
+ helmGtkLogger.cmx invokeTactics.cmx logicalOperations.cmx proofEngine.cmx \
+ termEditor.cmx termViewer.cmx
regtest.cmo: batchParser.cmi disambiguatingParser.cmi
regtest.cmx: batchParser.cmx disambiguatingParser.cmx
testlibrary.cmo: batchParser.cmi
fi
fi
-AC_ARG_WITH(transformer,
- AS_HELP_STRING([--with-transformer=(xslt|ocaml)],
- [choose mathml transformer (default is ocaml)]),
- [TRANSFORMER=$withval], [TRANSFORMER=ocaml])
-if test $TRANSFORMER = "xslt"; then
- CHOSEN_TRANSFORMER="include ApplyStylesheets"
-else
- if test $TRANSFORMER = "ocaml"; then
- CHOSEN_TRANSFORMER="include ApplyTransformation"
- else
- AC_MSG_ERROR(unknwon transformer $TRANSFORMER)
- fi
-fi
-
if test $TERM_EDITOR = "tex"; then
CHOSEN_TERM_EDITOR="include TexTermEditor"
else
AC_SUBST(OCAMLFIND)
AC_SUBST(CHOSEN_TERM_EDITOR)
AC_SUBST(CHOSEN_TERM_PARSER)
-AC_SUBST(CHOSEN_TRANSFORMER)
AC_OUTPUT([
- chosenTransformer.ml
chosenTermEditor.ml
disambiguatingParser.ml
Makefile
lazy
(let mmlwidget =
TermViewer.sequent_viewer
- ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
+ ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
~packing:scrolled_window#add ~width:400 ~height:280 () in
let expr =
let term = CicUtil.term_of_uri uri in
begin
(*CSC: Wrong: [] is just plainly wrong *)
let proof =
- Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
+ Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[],[])
+ in
let (acic,ids_to_inner_types,ids_to_inner_sorts) =
(rendering_window ())#output#load_proof uri proof
in
pathname_of_annuri (UriManager.buri_of_uri uri)
in
let list_of_universes =
- CicUnivUtils.universes_of_obj uri (Cic.Constant ("",None,ty,[]))
+ CicUnivUtils.universes_of_obj uri
+ (Cic.Constant ("",None,ty,[],[]))
in
let u1_clean = CicUniv.clean_ugraph u1 list_of_universes in
let u2 = CicUniv.fill_empty_nodes_with_uri u1_clean uri in
(* add the object to the env *)
CicEnvironment.add_type_checked_term uri ((
Cic.Constant ((UriManager.name_of_uri uri),
- (Some bo),ty,[])),u2);
+ (Some bo),ty,[],[])),u2);
(* FIXME: the variable list!! *)
prerr_endline "-------------> FINE";
end
(*CSC: Wrong: [] is just plainly wrong *)
let uri = match uri with Some uri -> uri | _ -> assert false in
(uri,
- Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
+ Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[]))
in
ignore (output#load_proof uri currentproof)
with
match ProofEngine.get_proof () with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
- debug_print ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[])));
+ debug_print ("Offending proof: " ^
+ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[],[])));
raise (InvokeTactics.RefreshProofException e)
let set_proof_engine_goal g =
let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in
let proof_file = Helm_registry.get "gtoplevel.proof_file" in
match CicParser.obj_of_xml proof_file_type (Some proof_file) with
- Cic.CurrentProof (_,metasenv,bo,ty,_) ->
+ Cic.CurrentProof (_,metasenv,bo,ty,_,_) ->
typecheck_loaded_proof metasenv bo ty ;
ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty));
refresh_proof output ;
let href = Gdome.domString "href" in
let show_in_show_window_obj uri obj =
try
- let
- (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
- ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
- =
- Cic2acic.acic_object_of_cic_object obj
- in
- let mml =
- ChosenTransformer.mml_of_cic_object
- ~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types
+ let mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_conjectures,
+ ids_to_hypotheses,_,_)) =
+ ApplyTransformation.mml_of_cic_object uri obj
in
window#set_title (UriManager.string_of_uri uri) ;
window#misc#hide () ; window#show () ;
(*CSC: Da finire *)
let params = [] in
let tys = !get_types_and_cons () in
- let obj = Cic.InductiveDefinition(tys,params,!paramsno) in
+ let obj = Cic.InductiveDefinition(tys,params,!paramsno,[]) in
let u =
begin
try
(* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*)
let metasenv,bo,ty =
match fst(CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri ) with
- Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
- | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
+ Cic.Constant (_,Some bo,ty,_,_) -> [],bo,ty
+ | Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> metasenv,bo,ty
| Cic.Constant _
| Cic.Variable _
| Cic.InductiveDefinition _ -> raise NotADefinition
~packing:(vbox#pack ~expand:true ~padding:5) () in
let sequent_viewer =
TermViewer.sequent_viewer
- ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
+ ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
~packing:(scrolled_window#add) ~width:400 ~height:280 () in
object(self)
val mutable term = Cic.Rel 1 (* dummy value *)
~packing:(vbox1#pack ~expand:true ~padding:5) () in
let proofw =
TermViewer.sequent_viewer
- ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
+ ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
~width:400 ~height:275 ~packing:(scrolled_window1#add) () in
let _ = proofw_ref <- Some proofw in
let hbox3 =
~packing:(vbox1#pack ~expand:true ~padding:5) () in
let proofw =
TermViewer.sequent_viewer
- ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
+ ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
~width:400 ~height:275 ~packing:(scrolled_window1#add) () in
object(self)
method proofw = (assert false : TermViewer.sequent_viewer)
factory3#add_item "Reload Stylesheets"
~callback:
(function _ ->
- ChosenTransformer.reload_stylesheets () ;
if ProofEngine.get_proof () <> None then
try
refresh_goals notebook ;
let initialize_everything () =
let output =
TermViewer.proof_viewer
- ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object
+ ~mml_of_cic_object:ApplyTransformation.mml_of_cic_object
~width:350 ~height:280 ()
in
let notebook = new notebook in
let uri = match uri with Some uri -> uri | None -> assert false in
let currentproof =
(*CSC: Wrong: [] is just plainly wrong *)
- Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
+ Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[])
in
let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
type mml_of_cic_sequent =
Cic.metasenv ->
int * Cic.context * Cic.term ->
- Gdome.document *
+ Gdome.document *
+ (Cic.annconjecture *
((Cic.id, Cic.term) Hashtbl.t *
(Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t)
+ (string, Cic.hypothesis) Hashtbl.t *
+ (Cic.id, string) Hashtbl.t))
+
type mml_of_cic_object =
- explode_all:bool ->
UriManager.uri ->
- Cic.annobj ->
- (string, string) Hashtbl.t ->
- (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
-
+ Cic.obj ->
+ Gdome.document *
+ (Cic.annobj *
+ ((Cic.id, Cic.term) Hashtbl.t *
+ (Cic.id, Cic.id option) Hashtbl.t *
+ (Cic.id, Cic.conjecture) Hashtbl.t *
+ (Cic.id, Cic.hypothesis) Hashtbl.t *
+ (Cic.id, string) Hashtbl.t *
+ (Cic.id, Cic2acic.anntypes) Hashtbl.t))
+
(* List utility functions *)
exception Skip;;
method load_sequent metasenv sequent =
(**** SIAM QUI ****)
- let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
+ let sequent_mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)) =
mml_of_cic_sequent metasenv sequent
in
self#load_root ~root:sequent_mml#get_documentElement ;
| None -> assert false (* "ERROR: No selection!!!" *)
method load_proof uri currentproof =
- let
- (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
- ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
- = Cic2acic.acic_object_of_cic_object currentproof
- in
- let mml =
- mml_of_cic_object
- ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
+ let mml,
+ (acic,
+ (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
+ ids_to_hypotheses,ids_to_inner_sorts,ids_to_inner_types)) =
+ mml_of_cic_object uri currentproof
in
current_infos <-
Some
type mml_of_cic_sequent =
Cic.metasenv ->
int * Cic.context * Cic.term ->
- Gdome.document *
+ Gdome.document *
+ (Cic.annconjecture *
((Cic.id, Cic.term) Hashtbl.t *
(Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t)
+ (string, Cic.hypothesis) Hashtbl.t *
+ (Cic.id, string) Hashtbl.t))
+
type mml_of_cic_object =
- explode_all:bool ->
UriManager.uri ->
- Cic.annobj ->
- (string, string) Hashtbl.t ->
- (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
+ Cic.obj ->
+ Gdome.document *
+ (Cic.annobj *
+ ((Cic.id, Cic.term) Hashtbl.t *
+ (Cic.id, Cic.id option) Hashtbl.t *
+ (Cic.id, Cic.conjecture) Hashtbl.t *
+ (Cic.id, Cic.hypothesis) Hashtbl.t *
+ (Cic.id, string) Hashtbl.t *
+ (Cic.id, Cic2acic.anntypes) Hashtbl.t))
(** A widget to render sequents **)
method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) =
let uri = unopt_uri uri_opt in
let obj = cicCurrentProof proof in
- let (mathml, (ids_to_terms, ids_to_father_ids, ids_to_conjectures,
- ids_to_hypotheses)) =
+ let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures,
+ ids_to_hypotheses,_,_))) =
ApplyTransformation.mml_of_cic_object uri obj
in
current_infos <- Some (ids_to_terms, ids_to_father_ids,
in
*)
let sequent = CicUtil.lookup_meta metano metasenv in
- let (mathml, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses)) =
+ let (mathml,(_,(ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_))) =
ApplyTransformation.mml_of_cic_sequent metasenv sequent
in
current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
projects / helm.git / commitdiff