--- /dev/null
+logicalOperations.cmo: proofEngine.cmo
+logicalOperations.cmx: proofEngine.cmx
+sequentPp.cmo: cic2Xml.cmo cic2acic.cmo proofEngine.cmo
+sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx
+gTopLevel.cmo: cic2Xml.cmo cic2acic.cmo logicalOperations.cmo sequentPp.cmo \
+ xml2Gdome.cmo
+gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx sequentPp.cmx \
+ xml2Gdome.cmx
--- /dev/null
+BIN_DIR = /usr/local/bin
+REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \
+ helm-xml gdome_xslt
+PREDICATES =
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
+OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
+OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS)
+OCAMLDEP = ocamldep -pp camlp4o
+
+LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
+LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
+
+all: gTopLevel
+opt: gTopLevel.opt
+
+DEPOBJS = xml2Gdome.ml proofEngine.ml cic2Xml.ml cic2acic.ml \
+ logicalOperations.ml sequentPp.ml gTopLevel.ml
+
+TOPLEVELOBJS = xml2Gdome.cmo proofEngine.cmo cic2Xml.cmo cic2acic.cmo \
+ logicalOperations.cmo sequentPp.cmo gTopLevel.cmo
+
+depend:
+ $(OCAMLDEP) $(DEPOBJS) > .depend
+
+gTopLevel: $(TOPLEVELOBJS) $(LIBRARIES)
+ $(OCAMLC) -linkpkg -o gTopLevel $(TOPLEVELOBJS)
+
+gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT)
+ $(OCAMLOPT) -linkpkg -o gTopLevel.opt $(TOPLEVELOBJS:.cmo=.cmx)
+
+.SUFFIXES: .ml .mli .cmo .cmi .cmx
+.ml.cmo: $(LIBRARIES)
+ $(OCAMLC) -c $<
+.mli.cmi: $(LIBRARIES)
+ $(OCAMLC) -c $<
+.ml.cmx: $(LIBRARIES_OPT)
+ $(OCAMLOPT) -c $<
+
+clean:
+ rm -f *.cm[iox] *.o gTopLevel gTopLevel.opt
+
+install:
+ cp gTopLevel gTopLevel.opt $(BIN_DIR)
+
+uninstall:
+ rm -f $(BIN_DIR)/gTopLevel $(BIN_DIR)/gTopLevel.opt
+
+.PHONY: install uninstall clean
+
+include .depend
--- /dev/null
+
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(*CSC codice cut & paste da cicPp e xmlcommand *)
+
+exception ImpossiblePossible;;
+exception NotImplemented;;
+let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
+
+(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
+let print_term curi =
+ let rec aux =
+ let module C = Cic in
+ let module X = Xml in
+ let module U = UriManager in
+ function
+ C.ARel (id,n,b) ->
+ X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id]
+ | C.AVar (id,uri) ->
+ let vdepth = U.depth_of_uri uri
+ and cdepth = U.depth_of_uri curi in
+ X.xml_empty "VAR"
+ ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
+ (U.name_of_uri uri) ;
+ "id",id]
+ | C.AMeta (id,n) ->
+ X.xml_empty "META" ["no",(string_of_int n) ; "id",id]
+ | C.ASort (id,s) ->
+ let string_of_sort =
+ function
+ C.Prop -> "Prop"
+ | C.Set -> "Set"
+ | C.Type -> "Type"
+ in
+ X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
+ | C.AImplicit _ -> raise NotImplemented
+ | C.AProd (id,C.Anonimous,s,t) ->
+ X.xml_nempty "PROD" ["id",id]
+ [< X.xml_nempty "source" [] (aux s) ;
+ X.xml_nempty "target" [] (aux t)
+ >]
+ | C.AProd (xid,C.Name id,s,t) ->
+ X.xml_nempty "PROD" ["id",xid]
+ [< X.xml_nempty "source" [] (aux s) ;
+ X.xml_nempty "target" ["binder",id] (aux t)
+ >]
+ | C.ACast (id,v,t) ->
+ X.xml_nempty "CAST" ["id",id]
+ [< X.xml_nempty "term" [] (aux v) ;
+ X.xml_nempty "type" [] (aux t)
+ >]
+ | C.ALambda (id,C.Anonimous,s,t) ->
+ X.xml_nempty "LAMBDA" ["id",id]
+ [< X.xml_nempty "source" [] (aux s) ;
+ X.xml_nempty "target" [] (aux t)
+ >]
+ | C.ALambda (xid,C.Name id,s,t) ->
+ X.xml_nempty "LAMBDA" ["id",xid]
+ [< X.xml_nempty "source" [] (aux s) ;
+ X.xml_nempty "target" ["binder",id] (aux t)
+ >]
+ | C.ALetIn (xid,C.Anonimous,s,t) ->
+ assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
+ | C.ALetIn (xid,C.Name id,s,t) ->
+ X.xml_nempty "LETIN" ["id",xid]
+ [< X.xml_nempty "term" [] (aux s) ;
+ X.xml_nempty "letintarget" ["binder",id] (aux t)
+ >]
+ | C.AAppl (id,li) ->
+ X.xml_nempty "APPLY" ["id",id]
+ [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
+ >]
+ | C.AConst (id,uri,_) ->
+ X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id]
+ | C.AAbst (id,uri) -> raise NotImplemented
+ | C.AMutInd (id,uri,_,i) ->
+ X.xml_empty "MUTIND"
+ ["uri", (U.string_of_uri uri) ;
+ "noType",(string_of_int i) ;
+ "id",id]
+ | C.AMutConstruct (id,uri,_,i,j) ->
+ X.xml_empty "MUTCONSTRUCT"
+ ["uri", (U.string_of_uri uri) ;
+ "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
+ "id",id]
+ | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
+ X.xml_nempty "MUTCASE"
+ ["uriType",(U.string_of_uri uri) ;
+ "noType", (string_of_int typeno) ;
+ "id", id]
+ [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
+ X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
+ List.fold_right
+ (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
+ patterns [<>]
+ >]
+ | C.AFix (id, no, funs) ->
+ X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id]
+ [< List.fold_right
+ (fun (fi,ai,ti,bi) i ->
+ [< X.xml_nempty "FixFunction"
+ ["name", fi; "recIndex", (string_of_int ai)]
+ [< X.xml_nempty "type" [] [< aux ti >] ;
+ X.xml_nempty "body" [] [< aux bi >]
+ >] ;
+ i
+ >]
+ ) funs [<>]
+ >]
+ | C.ACoFix (id,no,funs) ->
+ X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id]
+ [< List.fold_right
+ (fun (fi,ti,bi) i ->
+ [< X.xml_nempty "CofixFunction" ["name", fi]
+ [< X.xml_nempty "type" [] [< aux ti >] ;
+ X.xml_nempty "body" [] [< aux bi >]
+ >] ;
+ i
+ >]
+ ) funs [<>]
+ >]
+ in
+ aux
+;;
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+exception NotImplemented;;
+
+let fresh_id ids_to_terms ids_to_father_ids =
+ let id = ref 0 in
+ fun father t ->
+ let res = "i" ^ string_of_int !id in
+ incr id ;
+ Hashtbl.add ids_to_father_ids res father ;
+ Hashtbl.add ids_to_terms res t ;
+ res
+;;
+
+exception NotEnoughElements;;
+exception NameExpected;;
+
+(*CSC: cut&paste da cicPp.ml *)
+(* get_nth l n returns the nth element of the list l if it exists or *)
+(* raises NotEnoughElements if l has less than n elements *)
+let rec get_nth l n =
+ match (n,l) with
+ (1, he::_) -> he
+ | (n, he::tail) when n > 1 -> get_nth tail (n-1)
+ | (_,_) -> raise NotEnoughElements
+;;
+
+let acic_of_cic_env env t =
+ let module C = Cic in
+ let ids_to_terms = Hashtbl.create 503 in
+ let ids_to_father_ids = Hashtbl.create 503 in
+ let fresh_id' = fresh_id ids_to_terms ids_to_father_ids in
+ let rec aux father bs tt =
+ let fresh_id'' = fresh_id' father tt in
+ let aux' = aux (Some fresh_id'') in
+ match tt with
+ C.Rel n ->
+ let id =
+ match get_nth bs n with
+ C.Name s -> s
+ | _ -> raise NameExpected
+ in
+ C.ARel (fresh_id'', n, id)
+ | C.Var uri -> C.AVar (fresh_id'', uri)
+ | C.Meta n -> C.AMeta (fresh_id'', n)
+ | C.Sort s -> C.ASort (fresh_id'', s)
+ | C.Implicit -> C.AImplicit (fresh_id'')
+ | C.Cast (v,t) ->
+ C.ACast (fresh_id'', aux' bs v, aux' bs t)
+ | C.Prod (n,s,t) ->
+ C.AProd (fresh_id'', n, aux' bs s, aux' (n::bs) t)
+ | C.Lambda (n,s,t) ->
+ C.ALambda (fresh_id'',n, aux' bs s, aux' (n::bs) t)
+ | C.LetIn (n,s,t) ->
+ C.ALetIn (fresh_id'', n, aux' bs s, aux' (n::bs) t)
+ | C.Appl l -> C.AAppl (fresh_id'', List.map (aux' bs) l)
+ | C.Const (uri,cn) -> C.AConst (fresh_id'', uri, cn)
+ | C.Abst _ -> raise NotImplemented
+ | C.MutInd (uri,cn,tyno) -> C.AMutInd (fresh_id'', uri, cn, tyno)
+ | C.MutConstruct (uri,cn,tyno,consno) ->
+ C.AMutConstruct (fresh_id'', uri, cn, tyno, consno)
+ | C.MutCase (uri, cn, tyno, outty, term, patterns) ->
+ C.AMutCase (fresh_id'', uri, cn, tyno, aux' bs outty,
+ aux' bs term, List.map (aux' bs) patterns)
+ | C.Fix (funno, funs) ->
+ let names = List.map (fun (name,_,_,_) -> C.Name name) funs in
+ C.AFix (fresh_id'', funno,
+ List.map
+ (fun (name, indidx, ty, bo) ->
+ (name, indidx, aux' bs ty, aux' (names@bs) bo)
+ ) funs
+ )
+ | C.CoFix (funno, funs) ->
+ let names = List.map (fun (name,_,_) -> C.Name name) funs in
+ C.ACoFix (fresh_id'', funno,
+ List.map
+ (fun (name, ty, bo) ->
+ (name, aux' bs ty, aux' (names@bs) bo)
+ ) funs
+ )
+ in
+ aux None env t, ids_to_terms, ids_to_father_ids
+;;
+
+let acic_of_cic = acic_of_cic_env [];;
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 06/01/2002 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+(* GLOBAL CONSTANTS *)
+
+let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
+
+let htmlheader =
+ "<html>" ^
+ " <body bgColor=\"white\">"
+;;
+
+let htmlfooter =
+ " </body>" ^
+ "</html>"
+;;
+
+(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
+
+let htmlheader_and_content = ref htmlheader;;
+
+let filename4uwobo = "/public/sacerdot/prova.xml";;
+
+let current_cic_infos = ref None;;
+
+
+(* MISC FUNCTIONS *)
+
+let domImpl = Gdome.domImplementation ();;
+
+let parseStyle name =
+ let style =
+ domImpl#createDocumentFromURI
+(*
+ ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
+*)
+ ~uri:("styles/" ^ name) ()
+ in
+ Gdome_xslt.processStylesheet style
+;;
+
+let d_c = parseStyle "drop_coercions.xsl";;
+let tc1 = parseStyle "objtheorycontent.xsl";;
+let hc2 = parseStyle "content_to_html.xsl";;
+let l = parseStyle "link.xsl";;
+
+let c1 = parseStyle "rootcontent.xsl";;
+let g = parseStyle "genmmlid.xsl";;
+let c2 = parseStyle "annotatedpres.xsl";;
+
+(*
+let processorURL = "http://phd.cs.unibo.it:8080/helm/servelt/uwobo/";;
+let getterURL = "http://phd.cs.unibo.it:8081/";;
+*)
+let processorURL = "http://localhost:8080/helm/servelt/uwobo/";;
+let getterURL = "http://localhost:8081/";;
+
+let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
+let mml_args =
+ ["processorURL", "'" ^ processorURL ^ "'" ;
+ "getterURL", "'" ^ getterURL ^ "'" ;
+ "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
+ "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
+ "UNICODEvsSYMBOL", "'symbol'" ;
+ "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
+ "encoding", "'iso-8859-1'" ;
+ "media-type", "'text/html'" ;
+ "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
+ "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
+ "naturalLanguage", "'no'" ;
+ "annotations", "'no'" ;
+ "topurl", "'http://phd.cs.unibo.it/helm'" ;
+ "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
+;;
+
+let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
+let sequent_args =
+ ["processorURL", "'" ^ processorURL ^ "'" ;
+ "getterURL", "'" ^ getterURL ^ "'" ;
+ "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
+ "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
+ "UNICODEvsSYMBOL", "'symbol'" ;
+ "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
+ "encoding", "'iso-8859-1'" ;
+ "media-type", "'text/html'" ;
+ "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
+ "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
+ "naturalLanguage", "'no'" ;
+ "annotations", "'no'" ;
+ "topurl", "'http://phd.cs.unibo.it/helm'" ;
+ "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
+;;
+
+let parse_file filename =
+ let inch = open_in filename in
+ let rec read_lines () =
+ try
+ let line = input_line inch in
+ line ^ read_lines ()
+ with
+ End_of_file -> ""
+ in
+ read_lines ()
+;;
+
+let applyStylesheets input styles args =
+ List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
+ input styles
+;;
+
+let mml_of_cic acic =
+prerr_endline "BBB CREAZIONE" ;
+ let xml =
+ Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con") acic
+ in
+ Xml.pp ~quiet:true xml (Some filename4uwobo) ;
+prerr_endline "BBB PARSING" ;
+ let input = domImpl#createDocumentFromURI ~uri:filename4uwobo () in
+prerr_endline "BBB STYLESHEETS" ;
+ let output = applyStylesheets input mml_styles mml_args in
+prerr_endline "BBB RESA" ;
+ignore(domImpl#saveDocumentToFile ~doc:output ~name:"/tmp/xxxyyyzzz" ()) ;
+ output
+;;
+
+
+(* CALLBACKS *)
+
+let exact rendering_window () =
+ let inputt = (rendering_window#inputt : GEdit.text) in
+(*CSC: Gran cut&paste da sotto... *)
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen ^ "\n" in
+ let lexbuf = Lexing.from_string input in
+ try
+ while true do
+ (* Execute the actions *)
+ match CicTextualParser.main CicTextualLexer.token lexbuf with
+ None -> ()
+ | Some expr ->
+ try
+(*??? Ma servira' da qualche parte!
+ let ty = CicTypeChecker.type_of_aux' [] expr in
+*)
+ let (acic, ids_to_terms, ids_to_father_ids) =
+ Cic2acic.acic_of_cic expr
+ in
+(*CSC: chiamare la vera tattica exact qui! *)
+ ()
+ with
+ e ->
+ print_endline ("? " ^ CicPp.ppterm expr) ;
+ raise e
+ done
+ with
+ CicTextualParser0.Eof ->
+ inputt#delete_text 0 inputlen
+(*CSC: fare qualcosa di utile *)
+ | e ->
+ print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
+;;
+
+let proveit rendering_window () =
+ let module G = Gdome in
+ match rendering_window#output#get_selection with
+ Some node ->
+ let xpath =
+ ((node : Gdome.element)#getAttributeNS
+ (*CSC: OCAML DIVERGE
+ ((element : G.element)#getAttributeNS
+ *)
+ ~namespaceURI:helmns
+ ~localName:(G.domString "xref"))#to_string
+ in
+ if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+ else
+ begin
+ match !current_cic_infos with
+ Some (ids_to_terms, ids_to_father_ids) ->
+ let id = xpath in
+ let sequent =
+ LogicalOperations.to_sequent id ids_to_terms ids_to_father_ids
+ in
+ SequentPp.TextualPp.print_sequent sequent ;
+ let sequent_gdome = SequentPp.XmlPp.print_sequent sequent in
+ let sequent_doc =
+ Xml2Gdome.document_of_xml domImpl sequent_gdome
+ in
+ let sequent_mml =
+ applyStylesheets sequent_doc sequent_styles sequent_args
+ in
+ rendering_window#proofw#load_tree ~dom:sequent_mml ;
+ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
+ ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
+ignore(domImpl#saveDocumentToFile ~doc:sequent_mml
+ ~name:"/public/sacerdot/guruguru2" ~indent:true ())
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ end
+ | None -> assert false (* "ERROR: No selection!!!" *)
+;;
+
+let output_html outputhtml msg =
+ htmlheader_and_content := !htmlheader_and_content ^ msg ;
+ outputhtml#source (!htmlheader_and_content ^ htmlfooter)
+;;
+
+let execute rendering_window () =
+ let inputt = (rendering_window#inputt : GEdit.text) in
+ let oldinputt = (rendering_window#oldinputt : GEdit.text) in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let output = (rendering_window#output : GMathView.math_view) in
+ let proofw = (rendering_window#proofw : GMathView.math_view) in
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen ^ "\n" in
+ (* Do something interesting *)
+ let lexbuf = Lexing.from_string input in
+ try
+ while true do
+ (* Execute the actions *)
+ match CicTextualParser.main CicTextualLexer.token lexbuf with
+ None -> ()
+ | Some expr ->
+ try
+ let ty = CicTypeChecker.type_of_aux' [] expr in
+ let whd = CicReduction.whd expr in
+
+ let (acic, ids_to_terms, ids_to_father_ids) =
+ Cic2acic.acic_of_cic expr
+ in
+ let mml = mml_of_cic acic in
+ output#load_tree mml ;
+prerr_endline "BBB FINE RESA" ;
+ current_cic_infos := Some (ids_to_terms,ids_to_father_ids) ;
+print_endline ("? " ^ CicPp.ppterm expr) ;
+print_endline (">> " ^ CicPp.ppterm whd) ;
+print_endline (": " ^ CicPp.ppterm ty) ;
+flush stdout ;
+ with
+ e ->
+ print_endline ("? " ^ CicPp.ppterm expr) ;
+ raise e
+ done
+ with
+ CicTextualParser0.Eof ->
+ inputt#delete_text 0 inputlen ;
+ ignore(oldinputt#insert_text input oldinputt#length) ;
+ | e ->
+ print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
+;;
+
+let choose_selection
+ (mmlwidget : GMathView.math_view) (element : Gdome.element option)
+=
+ let module G = Gdome in
+ let rec aux element =
+ if element#hasAttributeNS
+ ~namespaceURI:helmns
+ ~localName:(G.domString "xref")
+ then
+ mmlwidget#set_selection (Some element)
+ else
+ match element#get_parentNode with
+ None -> assert false
+ (*CSC: OCAML DIVERGES!
+ | Some p -> aux (new G.element_of_node p)
+ *)
+ | Some p -> aux (new Gdome.element_of_node p)
+ in
+ match element with
+ Some x -> aux x
+ | None -> mmlwidget#set_selection None
+;;
+
+(* STUFF TO BUILD THE GTK INTERFACE *)
+
+(* Stuff for the widget settings *)
+
+let export_to_postscript (output : GMathView.math_view) () =
+ output#export_to_postscript ~filename:"output.ps" ();
+;;
+
+let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
+ button_set_kerning button_set_transparency button_export_to_postscript
+ button_t1 ()
+=
+ let is_set = button_t1#active in
+ output#set_font_manager_type
+ (if is_set then `font_manager_t1 else `font_manager_gtk) ;
+ if is_set then
+ begin
+ button_set_anti_aliasing#misc#set_sensitive true ;
+ button_set_kerning#misc#set_sensitive true ;
+ button_set_transparency#misc#set_sensitive true ;
+ button_export_to_postscript#misc#set_sensitive true ;
+ end
+ else
+ begin
+ button_set_anti_aliasing#misc#set_sensitive false ;
+ button_set_kerning#misc#set_sensitive false ;
+ button_set_transparency#misc#set_sensitive false ;
+ button_export_to_postscript#misc#set_sensitive false ;
+ end
+;;
+
+let set_anti_aliasing output button_set_anti_aliasing () =
+ output#set_anti_aliasing button_set_anti_aliasing#active
+;;
+
+let set_kerning output button_set_kerning () =
+ output#set_kerning button_set_kerning#active
+;;
+
+let set_transparency output button_set_transparency () =
+ output#set_transparency button_set_transparency#active
+;;
+
+let changefont output font_size_spinb () =
+ output#set_font_size font_size_spinb#value_as_int
+;;
+
+let set_log_verbosity output log_verbosity_spinb () =
+ output#set_log_verbosity log_verbosity_spinb#value_as_int
+;;
+
+class settings_window (output : GMathView.math_view) sw
+ button_export_to_postscript selection_changed_callback
+=
+ let settings_window = GWindow.window ~title:"GtkMathView settings" () in
+ let vbox =
+ GPack.vbox ~packing:settings_window#add () in
+ let table =
+ GPack.table
+ ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
+ ~border_width:5 ~packing:vbox#add () in
+ let button_t1 =
+ GButton.toggle_button ~label:"activate t1 fonts"
+ ~packing:(table#attach ~left:0 ~top:0) () in
+ let button_set_anti_aliasing =
+ GButton.toggle_button ~label:"set_anti_aliasing"
+ ~packing:(table#attach ~left:0 ~top:1) () in
+ let button_set_kerning =
+ GButton.toggle_button ~label:"set_kerning"
+ ~packing:(table#attach ~left:1 ~top:1) () in
+ let button_set_transparency =
+ GButton.toggle_button ~label:"set_transparency"
+ ~packing:(table#attach ~left:2 ~top:1) () in
+ let table =
+ GPack.table
+ ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
+ ~border_width:5 ~packing:vbox#add () in
+ let font_size_label =
+ GMisc.label ~text:"font size:"
+ ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
+ let font_size_spinb =
+ let sadj =
+ GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
+ in
+ GEdit.spin_button
+ ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
+ let log_verbosity_label =
+ GMisc.label ~text:"log verbosity:"
+ ~packing:(table#attach ~left:0 ~top:1) () in
+ let log_verbosity_spinb =
+ let sadj =
+ GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
+ in
+ GEdit.spin_button
+ ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let closeb =
+ GButton.button ~label:"Close"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+object(self)
+ method show = settings_window#show
+ initializer
+ button_set_anti_aliasing#misc#set_sensitive false ;
+ button_set_kerning#misc#set_sensitive false ;
+ button_set_transparency#misc#set_sensitive false ;
+ (* Signals connection *)
+ ignore(button_t1#connect#clicked
+ (activate_t1 output button_set_anti_aliasing button_set_kerning
+ button_set_transparency button_export_to_postscript button_t1)) ;
+ ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
+ ignore(button_set_anti_aliasing#connect#toggled
+ (set_anti_aliasing output button_set_anti_aliasing));
+ ignore(button_set_kerning#connect#toggled
+ (set_kerning output button_set_kerning)) ;
+ ignore(button_set_transparency#connect#toggled
+ (set_transparency output button_set_transparency)) ;
+ ignore(log_verbosity_spinb#connect#changed
+ (set_log_verbosity output log_verbosity_spinb)) ;
+ ignore(closeb#connect#clicked settings_window#misc#hide)
+end;;
+
+(* Main windows *)
+
+class rendering_window output proofw (label : GMisc.label) =
+ let window =
+ GWindow.window ~title:"MathML viewer" ~border_width:2 () in
+ let hbox0 =
+ GPack.hbox ~packing:window#add () in
+ let vbox =
+ GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
+ let scrolled_window0 =
+ GBin.scrolled_window ~border_width:10
+ ~packing:(vbox#pack ~expand:true ~padding:5) () in
+ let _ = scrolled_window0#add output#coerce in
+ let hbox1 =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let settingsb =
+ GButton.button ~label:"Settings"
+ ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let button_export_to_postscript =
+ GButton.button ~label:"export_to_postscript"
+ ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let closeb =
+ GButton.button ~label:"Close"
+ ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let hbox2 =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let proveitb =
+ GButton.button ~label:"Prove It"
+ ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
+ let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
+ ~packing:(vbox#pack ~padding:5) () in
+ let executeb =
+ GButton.button ~label:"Execute"
+ ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
+ ~packing:(vbox#pack ~padding:5) () in
+ let vbox1 =
+ GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
+ let scrolled_window1 =
+ GBin.scrolled_window ~border_width:10
+ ~packing:(vbox1#pack ~expand:true ~padding:5) () in
+ let _ = scrolled_window1#add proofw#coerce in
+ let hbox3 =
+ GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let exactb =
+ GButton.button ~label:"Exact"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let outputhtml =
+ GHtml.xmhtml
+ ~source:"<html><body bgColor=\"white\"></body></html>"
+ ~width:400 ~height: 200
+ ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
+ ~show:true () in
+object(self)
+ method outputhtml = outputhtml
+ method oldinputt = oldinputt
+ method inputt = inputt
+ method output = (output : GMathView.math_view)
+ method proofw = (proofw : GMathView.math_view)
+ method show () = window#show ()
+ initializer
+ button_export_to_postscript#misc#set_sensitive false ;
+
+ (* signal handlers here *)
+ ignore(output#connect#selection_changed
+ (function elem -> proofw#unload ; choose_selection output elem)) ;
+ ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
+ ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
+ let settings_window = new settings_window output scrolled_window0
+ button_export_to_postscript (choose_selection output) in
+ ignore(settingsb#connect#clicked settings_window#show) ;
+ ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
+ ignore(proveitb#connect#clicked (proveit self)) ;
+ ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
+ ignore(executeb#connect#clicked (execute self)) ;
+ ignore(exactb#connect#clicked (exact self)) ;
+ Logger.log_callback :=
+ (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
+end;;
+
+(* MAIN *)
+
+let initialize_everything () =
+ let module U = Unix in
+ let output = GMathView.math_view ~width:400 ~height:280 ()
+ and proofw = GMathView.math_view ~width:400 ~height:275 ()
+ and label = GMisc.label ~text:"gTopLevel" () in
+ let rendering_window =
+ new rendering_window output proofw label
+ in
+ rendering_window#show () ;
+ GMain.Main.main ()
+;;
+
+let _ =
+ CicCooking.init () ;
+ initialize_everything ()
+;;
--- /dev/null
+let get_parent id ids_to_terms ids_to_father_ids =
+ match Hashtbl.find ids_to_father_ids id with
+ None -> None
+ | Some id -> Some (id, Hashtbl.find ids_to_terms id)
+;;
+
+let get_context ids_to_terms ids_to_father_ids =
+ let module P = ProofEngine in
+ let module C = Cic in
+ let rec aux id =
+ match get_parent id ids_to_terms ids_to_father_ids with
+ None -> []
+ | Some (parentid,parent) ->
+ let term = Hashtbl.find ids_to_terms id in
+ let binding =
+ match parent with
+ C.Rel _
+ | C.Var _
+ | C.Meta _
+ | C.Sort _
+ | C.Implicit
+ | C.Cast _ -> []
+ | C.Prod (n,s,t) when t == term -> [P.Declaration,n,s]
+ | C.Prod _ -> []
+ | C.Lambda (n,s,t) when t == term -> [P.Declaration,n,s]
+ | C.Lambda _ -> []
+ | C.LetIn (n,s,t) when t == term -> [P.Definition,n,s]
+ | C.LetIn _ -> []
+ | C.Appl _
+ | C.Const _ -> []
+ | C.Abst _ -> assert false
+ | C.MutInd _
+ | C.MutConstruct _
+ | C.MutCase _ -> []
+(*CSC: sbagliato: manca il when *)
+ | C.Fix (_,ifl) ->
+ let counter = ref 0 in
+ List.rev_map
+ (function (name,_,ty,bo) ->
+ let res = (P.Definition, C.Name name, C.Fix (!counter,ifl)) in
+ incr counter ;
+ res
+ ) ifl
+ | C.CoFix (_,ifl) ->
+ let counter = ref 0 in
+ List.rev_map
+ (function (name,ty,bo) ->
+ let res = (P.Definition, C.Name name, C.CoFix (!counter,ifl)) in
+ incr counter ;
+ res
+ ) ifl
+ in
+ binding@(aux parentid)
+ in
+ aux
+;;
+
+exception NotImplemented;;
+
+let to_sequent id ids_to_terms ids_to_father_ids =
+ let module P = ProofEngine in
+ let term = Hashtbl.find ids_to_terms id in
+ let context = get_context ids_to_terms ids_to_father_ids id in
+ let type_checker_env_of_context =
+ List.map
+ (function
+ P.Declaration,_,t -> t
+ | P.Definition,_,_ -> raise NotImplemented
+ ) context
+ in
+ let ty = CicTypeChecker.type_of_aux' type_checker_env_of_context term in
+ ((context,ty) : ProofEngine.sequent)
+;;
--- /dev/null
+type binder_type =
+ Declaration
+ | Definition
+;;
+
+type context = (binder_type * Cic.name * Cic.term) list;;
+
+type sequent = context * Cic.term;;
--- /dev/null
+module TextualPp =
+ struct
+ (* It also returns the pretty-printing context! *)
+ let print_context ctx =
+ let module P = ProofEngine in
+ let print_name =
+ function
+ Cic.Name n -> n
+ | Cic.Anonimous -> "_"
+ in
+ List.fold_right
+ (fun i env ->
+ match i with
+ (P.Declaration,n,t) ->
+ print_endline (print_name n ^ ":" ^ CicPp.pp t env) ;
+ flush stdout ;
+ n::env
+ | (P.Definition,n,t) ->
+ print_endline (print_name n ^ ":=" ^ CicPp.pp t env) ;
+ flush stdout ;
+ n::env
+ ) ctx []
+ ;;
+
+ exception NotImplemented;;
+
+ let print_sequent (context,goal) =
+ let module P = ProofEngine in
+ print_newline () ;
+ let pretty_printer_env_of_context =
+ print_context context
+ in
+ print_endline "----------------------" ;
+ print_endline (CicPp.pp goal pretty_printer_env_of_context) ; flush stdout
+ ;;
+ end
+;;
+
+module XmlPp =
+ struct
+ let print_sequent (context,goal) =
+ let module X = Xml in
+ X.xml_nempty "Sequent" []
+ (let final_s,final_env =
+ (List.fold_right
+ (fun (b,n,t) (s,env) ->
+ [< s ;
+ X.xml_nempty
+ (match b with
+ ProofEngine.Definition -> "Definition"
+ | ProofEngine.Declaration -> "Declaration"
+ ) ["name",(match n with Cic.Name n -> n | _ -> assert false)]
+ (Cic2Xml.print_term
+ (UriManager.uri_of_string "cic:/dummy.con")
+ (let (acic,_,_) = Cic2acic.acic_of_cic_env env t in acic)) ;
+ >],(n::env)
+ ) context ([<>],[])
+ )
+ in
+ [< final_s ;
+ Xml.xml_nempty "Goal" []
+ (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
+ (let (acic,_,_) = Cic2acic.acic_of_cic_env final_env goal in acic))
+ >]
+ )
+ ;;
+ end
+;;
--- /dev/null
+let document_of_xml (domImplementation : Gdome.domImplementation) strm =
+ let module G = Gdome in
+ let module X = Xml in
+ let root_name,root_attributes,root_content =
+ match Stream.next strm with
+ X.Empty(n,l) -> n,l,[<>]
+ | X.NEmpty(n,l,c) -> n,l,c
+ | _ -> assert false
+ in
+ let document =
+(*CSC: erroraccio bruttissimo in gmetadom!!! *)
+ new Gdome.document (
+ domImplementation#createDocument ~namespaceURI:None
+ ~qualifiedName:(Gdome.domString root_name) ~doctype:None
+ )
+ in
+ let rec aux (node : Gdome.node) =
+ parser
+ [< 'X.Str a ; s >] ->
+ let textnode = document#createTextNode ~data:(Gdome.domString a) in
+ ignore (node#appendChild ~newChild:(textnode :> Gdome.node)) ;
+ aux node s
+ | [< 'X.Empty(n,l) ; s >] ->
+ let element = document#createElement ~tagName:(Gdome.domString n) in
+ List.iter (function (n,v) -> element#setAttribute
+ ~name:(Gdome.domString n) ~value:(Gdome.domString v)) l ;
+ ignore
+ (node#appendChild ~newChild:(element : Gdome.element :> Gdome.node)) ;
+ aux node s
+ | [< 'X.NEmpty(n,l,c) ; s >] ->
+ let element = document#createElement ~tagName:(Gdome.domString n) in
+ List.iter
+ (function (n,v) ->
+ element#setAttribute ~name:(Gdome.domString n)
+ ~value:(Gdome.domString v)
+ ) l ;
+ ignore (node#appendChild ~newChild:(element :> Gdome.node)) ;
+ aux (element :> Gdome.node) c ;
+ aux node s
+ | [< >] -> ()
+ in
+ let root = document#get_documentElement in
+ List.iter (function (n,v) -> root#setAttribute
+ ~name:(Gdome.domString n) ~value:(Gdome.domString v)) root_attributes ;
+ aux (root : Gdome.element :> Gdome.node) root_content ;
+ document
+;;
projects / helm.git / commitdiff