From 86122a3ce11bdf45ecb93f8f7efaffa49bd31fa2 Mon Sep 17 00:00:00 2001 From: no author Date: Fri, 25 Oct 2002 15:14:18 +0000 Subject: [PATCH] This commit was manufactured by cvs2svn to create branch 'V7_3_new_exportation'. --- helm/gTopLevel/.depend | 55 + helm/gTopLevel/Makefile | 64 + helm/gTopLevel/esempi/fourier.cic | 8 + helm/gTopLevel/esempi/rewrite.cic | 5 + helm/gTopLevel/fourierR.ml | 1228 ++++++++++++ helm/gTopLevel/fourierR.mli | 2 + helm/gTopLevel/gTopLevel.ml | 1653 +++++++++++++++++ helm/gTopLevel/mQueryGenerator.ml | 228 +++ helm/gTopLevel/mQueryGenerator.mli | 55 + helm/gTopLevel/proofEngine.ml | 277 +++ helm/gTopLevel/proofEngine.mli | 61 + helm/gTopLevel/proofEngineReduction.ml | 678 +++++++ helm/gTopLevel/proofEngineReduction.mli | 45 + helm/gTopLevel/topLevel/topLevel.ml | 208 +++ helm/ocaml/.cvsignore | 19 + .../cic_proof_checking/cicEnvironment.mli | 69 + helm/ocaml/cic_proof_checking/cicPp.ml | 260 +++ helm/ocaml/mathql/.depend | 8 + helm/ocaml/mathql/Makefile | 16 + helm/ocaml/mathql/mQueryTLexer.mll | 104 ++ helm/ocaml/mathql/mQueryTParser.mly | 189 ++ helm/ocaml/mathql/mQueryUtil.ml | 124 ++ helm/ocaml/mathql/mQueryUtil.mli | 49 + helm/ocaml/mathql/mathQL.ml | 100 + helm/ocaml/mathql_interpreter/.depend | 22 + helm/ocaml/mathql_interpreter/Makefile | 15 + helm/ocaml/mathql_interpreter/context.ml | 30 + helm/ocaml/mathql_interpreter/dbconn.ml | 74 + helm/ocaml/mathql_interpreter/dbconn.mli | 28 + helm/ocaml/mathql_interpreter/diff.ml | 98 + helm/ocaml/mathql_interpreter/diff.mli | 27 + helm/ocaml/mathql_interpreter/func.ml | 56 + helm/ocaml/mathql_interpreter/func.mli | 26 + helm/ocaml/mathql_interpreter/intersect.ml | 75 + helm/ocaml/mathql_interpreter/intersect.mli | 30 + helm/ocaml/mathql_interpreter/meet.ml | 34 + helm/ocaml/mathql_interpreter/meet.mli | 27 + helm/ocaml/mathql_interpreter/mqint.ml | 213 +++ helm/ocaml/mathql_interpreter/mqint.mli | 46 + helm/ocaml/mathql_interpreter/relation.ml | 149 ++ helm/ocaml/mathql_interpreter/relation.mli | 30 + helm/ocaml/mathql_interpreter/select.ml | 153 ++ helm/ocaml/mathql_interpreter/sortedby.ml | 62 + helm/ocaml/mathql_interpreter/sub.ml | 34 + helm/ocaml/mathql_interpreter/sub.mli | 27 + helm/ocaml/mathql_interpreter/union.ml | 52 + helm/ocaml/mathql_interpreter/union.mli | 27 + helm/on-line/xslt/ls2html.xsl | 158 ++ 48 files changed, 6998 insertions(+) create mode 100644 helm/gTopLevel/.depend create mode 100644 helm/gTopLevel/Makefile create mode 100644 helm/gTopLevel/esempi/fourier.cic create mode 100644 helm/gTopLevel/esempi/rewrite.cic create mode 100644 helm/gTopLevel/fourierR.ml create mode 100644 helm/gTopLevel/fourierR.mli create mode 100644 helm/gTopLevel/gTopLevel.ml create mode 100644 helm/gTopLevel/mQueryGenerator.ml create mode 100644 helm/gTopLevel/mQueryGenerator.mli create mode 100644 helm/gTopLevel/proofEngine.ml create mode 100644 helm/gTopLevel/proofEngine.mli create mode 100644 helm/gTopLevel/proofEngineReduction.ml create mode 100644 helm/gTopLevel/proofEngineReduction.mli create mode 100644 helm/gTopLevel/topLevel/topLevel.ml create mode 100644 helm/ocaml/.cvsignore create mode 100644 helm/ocaml/cic_proof_checking/cicEnvironment.mli create mode 100644 helm/ocaml/cic_proof_checking/cicPp.ml create mode 100644 helm/ocaml/mathql/.depend create mode 100644 helm/ocaml/mathql/Makefile create mode 100644 helm/ocaml/mathql/mQueryTLexer.mll create mode 100644 helm/ocaml/mathql/mQueryTParser.mly create mode 100644 helm/ocaml/mathql/mQueryUtil.ml create mode 100644 helm/ocaml/mathql/mQueryUtil.mli create mode 100644 helm/ocaml/mathql/mathQL.ml create mode 100644 helm/ocaml/mathql_interpreter/.depend create mode 100644 helm/ocaml/mathql_interpreter/Makefile create mode 100644 helm/ocaml/mathql_interpreter/context.ml create mode 100644 helm/ocaml/mathql_interpreter/dbconn.ml create mode 100644 helm/ocaml/mathql_interpreter/dbconn.mli create mode 100644 helm/ocaml/mathql_interpreter/diff.ml create mode 100644 helm/ocaml/mathql_interpreter/diff.mli create mode 100644 helm/ocaml/mathql_interpreter/func.ml create mode 100644 helm/ocaml/mathql_interpreter/func.mli create mode 100644 helm/ocaml/mathql_interpreter/intersect.ml create mode 100644 helm/ocaml/mathql_interpreter/intersect.mli create mode 100644 helm/ocaml/mathql_interpreter/meet.ml create mode 100644 helm/ocaml/mathql_interpreter/meet.mli create mode 100644 helm/ocaml/mathql_interpreter/mqint.ml create mode 100644 helm/ocaml/mathql_interpreter/mqint.mli create mode 100644 helm/ocaml/mathql_interpreter/relation.ml create mode 100644 helm/ocaml/mathql_interpreter/relation.mli create mode 100644 helm/ocaml/mathql_interpreter/select.ml create mode 100644 helm/ocaml/mathql_interpreter/sortedby.ml create mode 100644 helm/ocaml/mathql_interpreter/sub.ml create mode 100644 helm/ocaml/mathql_interpreter/sub.mli create mode 100644 helm/ocaml/mathql_interpreter/union.ml create mode 100644 helm/ocaml/mathql_interpreter/union.mli create mode 100644 helm/on-line/xslt/ls2html.xsl diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend new file mode 100644 index 000000000..2b88f0c85 --- /dev/null +++ b/helm/gTopLevel/.depend @@ -0,0 +1,55 @@ +xml2Gdome.cmo: xml2Gdome.cmi +xml2Gdome.cmx: xml2Gdome.cmi +proofEngineHelpers.cmo: proofEngineHelpers.cmi +proofEngineHelpers.cmx: proofEngineHelpers.cmi +proofEngineReduction.cmo: proofEngineReduction.cmi +proofEngineReduction.cmx: proofEngineReduction.cmi +proofEngineStructuralRules.cmo: proofEngineTypes.cmo \ + proofEngineStructuralRules.cmi +proofEngineStructuralRules.cmx: proofEngineTypes.cmx \ + proofEngineStructuralRules.cmi +proofEngineStructuralRules.cmi: proofEngineTypes.cmo +primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \ + proofEngineTypes.cmo primitiveTactics.cmi +primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ + proofEngineTypes.cmx primitiveTactics.cmi +primitiveTactics.cmi: proofEngineTypes.cmo +tacticals.cmo: primitiveTactics.cmi proofEngineTypes.cmo tacticals.cmi +tacticals.cmx: primitiveTactics.cmx proofEngineTypes.cmx tacticals.cmi +tacticals.cmi: proofEngineTypes.cmo +ring.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \ + proofEngineTypes.cmo tacticals.cmi ring.cmi +ring.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \ + proofEngineTypes.cmx tacticals.cmx ring.cmi +ring.cmi: proofEngineTypes.cmo +fourierR.cmo: fourier.cmo primitiveTactics.cmi proofEngineHelpers.cmi \ + proofEngineReduction.cmi proofEngineTypes.cmo ring.cmi tacticals.cmi \ + fourierR.cmi +fourierR.cmx: fourier.cmx primitiveTactics.cmx proofEngineHelpers.cmx \ + proofEngineReduction.cmx proofEngineTypes.cmx ring.cmx tacticals.cmx \ + fourierR.cmi +fourierR.cmi: proofEngineTypes.cmo +proofEngine.cmo: fourierR.cmi primitiveTactics.cmi proofEngineHelpers.cmi \ + proofEngineReduction.cmi proofEngineStructuralRules.cmi \ + proofEngineTypes.cmo ring.cmi proofEngine.cmi +proofEngine.cmx: fourierR.cmx primitiveTactics.cmx proofEngineHelpers.cmx \ + proofEngineReduction.cmx proofEngineStructuralRules.cmx \ + proofEngineTypes.cmx ring.cmx proofEngine.cmi +proofEngine.cmi: proofEngineTypes.cmo +doubleTypeInference.cmo: doubleTypeInference.cmi +doubleTypeInference.cmx: doubleTypeInference.cmi +cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi +cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi +cic2Xml.cmo: cic2acic.cmi cic2Xml.cmi +cic2Xml.cmx: cic2acic.cmx cic2Xml.cmi +cic2Xml.cmi: cic2acic.cmi +logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi +logicalOperations.cmx: proofEngine.cmx logicalOperations.cmi +sequentPp.cmo: cic2Xml.cmi cic2acic.cmi proofEngine.cmi sequentPp.cmi +sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx sequentPp.cmi +mQueryGenerator.cmo: mQueryGenerator.cmi +mQueryGenerator.cmx: mQueryGenerator.cmi +gTopLevel.cmo: cic2Xml.cmi cic2acic.cmi logicalOperations.cmi \ + mQueryGenerator.cmi proofEngine.cmi sequentPp.cmi xml2Gdome.cmi +gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx \ + mQueryGenerator.cmx proofEngine.cmx sequentPp.cmx xml2Gdome.cmx diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile new file mode 100644 index 000000000..403b8b180 --- /dev/null +++ b/helm/gTopLevel/Makefile @@ -0,0 +1,64 @@ +BIN_DIR = /usr/local/bin +REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \ + helm-xml gdome2-xslt helm-cic_unification helm-mathql \ + helm-mathql_interpreter +PREDICATES = "gnome,init" +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 xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \ + proofEngineReduction.ml proofEngineReduction.mli \ + proofEngineStructuralRules.ml proofEngineStructuralRules.mli \ + primitiveTactics.ml primitiveTactics.mli tacticals.ml tacticals.mli \ + ring.ml ring.mli fourier.ml fourierR.ml fourierR.mli\ + proofEngine.ml proofEngine.mli \ + doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \ + cic2acic.mli cic2Xml.ml cic2Xml.mli logicalOperations.ml \ + logicalOperations.mli sequentPp.ml sequentPp.mli mQueryGenerator.mli \ + mQueryGenerator.ml gTopLevel.ml + +TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \ + proofEngineReduction.cmo proofEngineStructuralRules.cmo \ + primitiveTactics.cmo tacticals.cmo ring.cmo \ + fourier.cmo fourierR.cmo proofEngine.cmo \ + doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \ + logicalOperations.cmo sequentPp.cmo mQueryGenerator.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 diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic new file mode 100644 index 000000000..cae3925a7 --- /dev/null +++ b/helm/gTopLevel/esempi/fourier.cic @@ -0,0 +1,8 @@ +alias Rge /Coq/Reals/Rdefinitions/Rge.con +alias Rle /Coq/Reals/Rdefinitions/Rle.con +alias Rplus /Coq/Reals/Rdefinitions/Rplus.con +alias Rminus /Coq/Reals/Rdefinitions/Rminus.con +alias R1 /Coq/Reals/Rdefinitions/R1.con +alias R /Coq/Reals/Rdefinitions/R.con + +!x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1)) diff --git a/helm/gTopLevel/esempi/rewrite.cic b/helm/gTopLevel/esempi/rewrite.cic new file mode 100644 index 000000000..ff2b92e52 --- /dev/null +++ b/helm/gTopLevel/esempi/rewrite.cic @@ -0,0 +1,5 @@ +!v:nat.(eq nat -> nat -> nat \x:nat.\y:nat.(plus y v) \x:nat.\y:nat.O) + +Fare cut di: + (eq nat -> nat \w:nat.(plus w v) \w:nat.(plus (plus w w) v)) +e poi riscriverlo diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml new file mode 100644 index 000000000..0dd76f89a --- /dev/null +++ b/helm/gTopLevel/fourierR.ml @@ -0,0 +1,1228 @@ +(* Copyright (C) 2002, 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/. + *) + + +(******************** OTHER USEFUL TACTICS **********************) + +let rewrite_tac ~term:equality ~status:(proof,goal) = + let module C = Cic in + let module U = UriManager in + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let eq_ind_r,ty,t1,t2 = + match CicTypeChecker.type_of_aux' metasenv context equality with + C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind") -> + let eq_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0) + in + eq_ind_r,ty,t1,t2 + | C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") -> + let eqT_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",0) + in + eqT_ind_r,ty,t1,t2 + | _ -> + raise + (ProofEngineTypes.Fail + "Rewrite: the argument is not a proof of an equality") + in + let pred = + let gty' = CicSubstitution.lift 1 gty in + let t1' = CicSubstitution.lift 1 t1 in + let gty'' = + ProofEngineReduction.replace_lifting + ~equality: + (ProofEngineReduction.syntactic_equality ~alpha_equivalence:true) + ~what:t1' ~with_what:(C.Rel 1) ~where:gty' + in + C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') + in +prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in + + let (proof',goals) = + PrimitiveTactics.exact_tac + ~term:(C.Appl + [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) + ~status:((curi,metasenv',pbo,pty),goal) + in + assert (List.length goals = 0) ; + (proof',[fresh_meta]) +;; + + + +let simpl_tac ~status:(proof,goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + +prerr_endline("simpl_tac su "^CicPp.ppterm ty); + + let new_ty = ProofEngineReduction.simpl context ty in + +prerr_endline("ritorna "^CicPp.ppterm new_ty); + + let new_metasenv = + List.map + (function + (n,_,_) when n = metano -> (metano,context,new_ty) + | _ as t -> t + ) metasenv + in + (curi,new_metasenv,pbo,pty), [metano] + +;; + +let rewrite_simpl_tac ~term ~status = + + Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:simpl_tac ~status + +;; + +(******************** THE FOURIER TACTIC ***********************) + +(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients +des inéquations et équations sont entiers. En attendant la tactique Field. +*) + +open Fourier + + +let debug x = print_string ("____ "^x) ; flush stdout;; + +let debug_pcontext x = + let str = ref "" in + List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^ + a ^ " " | _ ->()) x ; + debug ("contesto : "^ (!str) ^ "\n") +;; + +(****************************************************************************** +Operations on linear combinations. + +Opérations sur les combinaisons linéaires affines. +La partie homogène d'une combinaison linéaire est en fait une table de hash +qui donne le coefficient d'un terme du calcul des constructions, +qui est zéro si le terme n'y est pas. +*) + + + +(** + The type for linear combinations +*) +type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational} +;; + +(** + @return an empty flin +*) +let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0} +;; + +(** + @param f a flin + @param x a Cic.term + @return the rational associated with x (coefficient) +*) +let flin_coef f x = + try + (Hashtbl.find f.fhom x) + with + _ -> r0 +;; + +(** + Adds c to the coefficient of x + @param f a flin + @param x a Cic.term + @param c a rational + @return the new flin +*) +let flin_add f x c = + let cx = flin_coef f x in + Hashtbl.remove f.fhom x; + Hashtbl.add f.fhom x (rplus cx c); + f +;; +(** + Adds c to f.fcste + @param f a flin + @param c a rational + @return the new flin +*) +let flin_add_cste f c = + {fhom=f.fhom; + fcste=rplus f.fcste c} +;; + +(** + @return a empty flin with r1 in fcste +*) +let flin_one () = flin_add_cste (flin_zero()) r1;; + +(** + Adds two flin +*) +let flin_plus f1 f2 = + let f3 = flin_zero() in + Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; + Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom; + flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste; +;; + +(** + Substracts two flin +*) +let flin_minus f1 f2 = + let f3 = flin_zero() in + Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; + Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom; + flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste); +;; + +(** + @return f times a +*) +let flin_emult a f = + let f2 = flin_zero() in + Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom; + flin_add_cste f2 (rmult a f.fcste); +;; + + +(*****************************************************************************) + + +(** + @param t a term + @return proiection on string of t +*) +let rec string_of_term t = + match t with + Cic.Cast (t1,t2) -> string_of_term t1 + |Cic.Const (u,boh) -> UriManager.string_of_uri u + |Cic.Var (u) -> UriManager.string_of_uri u + | _ -> "not_of_constant" +;; + +(* coq wrapper +let string_of_constr = string_of_term +;; +*) + +(** + @param t a term + @raise Failure if conversion is impossible + @return rational proiection of t +*) +let rec rational_of_term t = + (* fun to apply f to the first and second rational-term of l *) + let rat_of_binop f l = + let a = List.hd l and + b = List.hd(List.tl l) in + f (rational_of_term a) (rational_of_term b) + in + (* as before, but f is unary *) + let rat_of_unop f l = + f (rational_of_term (List.hd l)) + in + match t with + | Cic.Cast (t1,t2) -> (rational_of_term t1) + | Cic.Appl (t1::next) -> + (match t1 with + Cic.Const (u,boh) -> + (match (UriManager.string_of_uri u) with + "cic:/Coq/Reals/Rdefinitions/Ropp.con" -> + rat_of_unop rop next + |"cic:/Coq/Reals/Rdefinitions/Rinv.con" -> + rat_of_unop rinv next + |"cic:/Coq/Reals/Rdefinitions/Rmult.con" -> + rat_of_binop rmult next + |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" -> + rat_of_binop rdiv next + |"cic:/Coq/Reals/Rdefinitions/Rplus.con" -> + rat_of_binop rplus next + |"cic:/Coq/Reals/Rdefinitions/Rminus.con" -> + rat_of_binop rminus next + | _ -> failwith "not a rational") + | _ -> failwith "not a rational") + | Cic.Const (u,boh) -> + (match (UriManager.string_of_uri u) with + "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1 + |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0 + | _ -> failwith "not a rational") + | _ -> failwith "not a rational" +;; + +(* coq wrapper +let rational_of_const = rational_of_term;; +*) + + +let rec flin_of_term t = + let fl_of_binop f l = + let a = List.hd l and + b = List.hd(List.tl l) in + f (flin_of_term a) (flin_of_term b) + in + try( + match t with + | Cic.Cast (t1,t2) -> (flin_of_term t1) + | Cic.Appl (t1::next) -> + begin + match t1 with + Cic.Const (u,boh) -> + begin + match (UriManager.string_of_uri u) with + "cic:/Coq/Reals/Rdefinitions/Ropp.con" -> + flin_emult (rop r1) (flin_of_term (List.hd next)) + |"cic:/Coq/Reals/Rdefinitions/Rplus.con"-> + fl_of_binop flin_plus next + |"cic:/Coq/Reals/Rdefinitions/Rminus.con"-> + fl_of_binop flin_minus next + |"cic:/Coq/Reals/Rdefinitions/Rmult.con"-> + begin + let arg1 = (List.hd next) and + arg2 = (List.hd(List.tl next)) + in + try + begin + let a = rational_of_term arg1 in + try + begin + let b = (rational_of_term arg2) in + (flin_add_cste (flin_zero()) (rmult a b)) + end + with + _ -> (flin_add (flin_zero()) arg2 a) + end + with + _-> (flin_add(flin_zero()) arg1 (rational_of_term arg2)) + end + |"cic:/Coq/Reals/Rdefinitions/Rinv.con"-> + let a=(rational_of_term (List.hd next)) in + flin_add_cste (flin_zero()) (rinv a) + |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"-> + begin + let b=(rational_of_term (List.hd(List.tl next))) in + try + begin + let a = (rational_of_term (List.hd next)) in + (flin_add_cste (flin_zero()) (rdiv a b)) + end + with + _-> (flin_add (flin_zero()) (List.hd next) (rinv b)) + end + |_->assert false + end + |_ -> assert false + end + | Cic.Const (u,boh) -> + begin + match (UriManager.string_of_uri u) with + "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one () + |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero () + |_-> assert false + end + |_-> assert false) + with _ -> flin_add (flin_zero()) t r1 +;; + +(* coq wrapper +let flin_of_constr = flin_of_term;; +*) + +(** + Translates a flin to (c,x) list + @param f a flin + @return something like (c1,x1)::(c2,x2)::...::(cn,xn) +*) +let flin_to_alist f = + let res=ref [] in + Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f; + !res +;; + +(* Représentation des hypothèses qui sont des inéquations ou des équations. +*) + +(** + The structure for ineq +*) +type hineq={hname:Cic.term; (* le nom de l'hypothèse *) + htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *) + hleft:Cic.term; + hright:Cic.term; + hflin:flin; + hstrict:bool} +;; + +(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0 +*) + +let ineq1_of_term (h,t) = + match t with (* match t *) + Cic.Appl (t1::next) -> + let arg1= List.hd next in + let arg2= List.hd(List.tl next) in + (match t1 with (* match t1 *) + Cic.Const (u,boh) -> + (match UriManager.string_of_uri u with (* match u *) + "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> + [{hname=h; + htype="Rlt"; + hleft=arg1; + hright=arg2; + hflin= flin_minus (flin_of_term arg1) + (flin_of_term arg2); + hstrict=true}] + |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> + [{hname=h; + htype="Rgt"; + hleft=arg2; + hright=arg1; + hflin= flin_minus (flin_of_term arg2) + (flin_of_term arg1); + hstrict=true}] + |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> + [{hname=h; + htype="Rle"; + hleft=arg1; + hright=arg2; + hflin= flin_minus (flin_of_term arg1) + (flin_of_term arg2); + hstrict=false}] + |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> + [{hname=h; + htype="Rge"; + hleft=arg2; + hright=arg1; + hflin= flin_minus (flin_of_term arg2) + (flin_of_term arg1); + hstrict=false}] + |_->assert false)(* match u *) + | Cic.MutInd (u,i,o) -> + (match UriManager.string_of_uri u with + "cic:/Coq/Init/Logic_Type/eqT.con" -> + let t0= arg1 in + let arg1= arg2 in + let arg2= List.hd(List.tl (List.tl next)) in + (match t0 with + Cic.Const (u,boh) -> + (match UriManager.string_of_uri u with + "cic:/Coq/Reals/Rdefinitions/R.con"-> + [{hname=h; + htype="eqTLR"; + hleft=arg1; + hright=arg2; + hflin= flin_minus (flin_of_term arg1) + (flin_of_term arg2); + hstrict=false}; + {hname=h; + htype="eqTRL"; + hleft=arg2; + hright=arg1; + hflin= flin_minus (flin_of_term arg2) + (flin_of_term arg1); + hstrict=false}] + |_-> assert false) + |_-> assert false) + |_-> assert false) + |_-> assert false)(* match t1 *) + |_-> assert false (* match t *) +;; +(* coq wrapper +let ineq1_of_constr = ineq1_of_term;; +*) + +(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq) +*) + +let rec print_rl l = + match l with + []-> () + | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next +;; + +let rec print_sys l = + match l with + [] -> () + | (a,b)::next -> (print_rl a; + print_string (if b=true then "strict\n"else"\n"); + print_sys next) + ;; + +(*let print_hash h = + Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h +;;*) + +let fourier_lineq lineq1 = + let nvar=ref (-1) in + let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *) + List.iter (fun f -> + Hashtbl.iter (fun x c -> + try (Hashtbl.find hvar x;()) + with _-> nvar:=(!nvar)+1; + Hashtbl.add hvar x (!nvar)) + f.hflin.fhom) + lineq1; + (*print_hash hvar;*) + debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n"); + let sys= List.map (fun h-> + let v=Array.create ((!nvar)+1) r0 in + Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c) + h.hflin.fhom; + ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict)) + lineq1 in + debug ("chiamo unsolvable sul sistema di "^ + string_of_int (List.length sys) ^"\n"); + print_sys sys; + unsolvable sys +;; + +(***************************************************************************** +Construction de la preuve en cas de succès de la méthode de Fourier, +i.e. on obtient une contradiction. +*) + + +let _eqT = Cic.MutInd(UriManager.uri_of_string + "cic:/Coq/Init/Logic_Type/eqT.ind") 0 0 ;; +let _False = Cic.MutInd (UriManager.uri_of_string + "cic:/Coq/Init/Logic/False.ind") 0 0 ;; +let _not = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Init/Logic/not.con") 0;; +let _R0 = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;; +let _R1 = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;; +let _R = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;; +let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;; +let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;; +let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;; +let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;; +let _Rfourier_le=Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;; +let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") 0 ;; +let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;; +let _Rfourier_lt=Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;; +let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") 0 ;; +let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;; +let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;; +let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;; +let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;; +let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;; +let _Rinv = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;; +let _Rinv_R1 = Cic.Const(UriManager.uri_of_string + "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;; +let _Rle = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;; +let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;; +let _Rle_not_lt = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;; +let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;; +let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;; +let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;; +let _Rlt = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;; +let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;; +let _Rlt_not_le = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;; +let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;; +let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;; +let _Rminus = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;; +let _Rmult = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;; +let _Rnot_le_le =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;; +let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;; +let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;; +let _Ropp = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;; +let _Rplus = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;; +let _sym_eqT = Cic.Const(UriManager.uri_of_string + "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;; + +(******************************************************************************) + +let is_int x = (x.den)=1 +;; + +(* fraction = couple (num,den) *) +let rec rational_to_fraction x= (x.num,x.den) +;; + +(* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1))) +*) + +let rec int_to_real_aux n = + match n with + 0 -> _R0 (* o forse R0 + R0 ????? *) + | 1 -> _R1 + | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ] +;; + + +let int_to_real n = + let x = int_to_real_aux (abs n) in + if n < 0 then + Cic.Appl [ _Ropp ; x ] + else + x +;; + + +(* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1))) +*) + +let rational_to_real x = + let (n,d)=rational_to_fraction x in + Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ] +;; + +(* preuve que 0 m=goal) metasenv in + debug ("th = "^ CicPp.ppterm t ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); + in + let tacn=ref + (fun ~status -> pall "n0" ~status _Rlt_zero_1 ; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in + let tacd=ref + (fun ~status -> pall "d0" ~status _Rlt_zero_1 ; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in + + + for i=1 to n-1 do + tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i) + ~status _Rlt_zero_pos_plus1; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) + ~continuation:!tacn); + done; + for i=1 to d-1 do + tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d" + ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac + ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd); + done; + + + +debug("TAC ZERO INF POS\n"); + +(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) + ~continuations:[ + !tacn ; + !tacd ] + ~status) +;; + + + +(* preuve que 0<=n*1/d +*) + +let tac_zero_infeq_pos gl (n,d) ~status = + (*let cste = pf_parse_constr gl in*) + debug("inizio tac_zero_infeq_pos\n"); + let tacn = ref + (if n=0 then + (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero ) + else + (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ) + ) + in + let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in + for i=1 to n-1 do + tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); + done; + for i=1 to d-1 do + tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); + done; + let r = + (Tacticals.thens ~start:(PrimitiveTactics.apply_tac + ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in + debug("fine tac_zero_infeq_pos\n"); + r +;; + + + +(* preuve que 0<(-n)*(1/d) => False +*) + +let tac_zero_inf_false gl (n,d) ~status= + debug("inizio tac_zero_inf_false\n"); + if n=0 then + (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in + debug("fine\n"); + r) + else + (debug "2\n";let r = (Tacticals.then_ ~start:( + fun ~status:(proof,goal as status) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in + debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with " + ^ CicPp.ppterm ty ^"\n"); + let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in + debug("!!!!!!!!!2\n"); + r + ) + ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in + debug("fine\n"); + r + ) +;; + +(* preuve que 0<=(-n)*(1/d) => False +*) + +let tac_zero_infeq_false gl (n,d) ~status= +debug("stat tac_zero_infeq_false"); +let r = + (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) + ~continuation:(tac_zero_inf_pos (-n,d))) ~status in + debug("stat tac_zero_infeq_false"); + r +;; + + +(* *********** ********** ******** ??????????????? *********** **************) + +let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,t)::metasenv in + let proof' = curi,metasenv',pbo,pty in + let proof'',goals = + PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta + (fresh_meta,irl),t))::al)) ~status:(proof',goal) + in + proof'',fresh_meta::goals +;; + + + + + +let my_cut ~term:c ~status:(proof,goal)= + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,c)::metasenv in + let proof' = curi,metasenv',pbo,pty in + let proof'',goals = + apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c, + CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] + ~status:(proof',goal) + in + (* We permute the generated goals to be consistent with Coq *) + match goals with + [] -> assert false + | he::tl -> proof'',he::fresh_meta::tl +;; + + +let exact = PrimitiveTactics.exact_tac;; + +let tac_use h ~status:(proof,goal as status) = +debug("Inizio TC_USE\n"); +let curi,metasenv,pbo,pty = proof in +let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in +debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); +debug ("ty = "^ CicPp.ppterm ty^"\n"); + +let res = +match h.htype with + "Rlt" -> exact ~term:h.hname ~status + |"Rle" -> exact ~term:h.hname ~status + |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_gt_to_lt) + ~continuation:(exact ~term:h.hname)) ~status + |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_ge_to_le) + ~continuation:(exact ~term:h.hname)) ~status + |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_eqLR_to_le) + ~continuation:(exact ~term:h.hname)) ~status + |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_eqRL_to_le) + ~continuation:(exact ~term:h.hname)) ~status + |_->assert false +in +debug("Fine TAC_USE\n"); +res +;; + + + +let is_ineq (h,t) = + match t with + Cic.Appl ( Cic.Const(u,boh)::next) -> + (match (UriManager.string_of_uri u) with + "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true + |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true + |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true + |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true + |"cic:/Coq/Init/Logic_Type/eqT.con" -> + (match (List.hd next) with + Cic.Const (uri,_) when + UriManager.string_of_uri uri = + "cic:/Coq/Reals/Rdefinitions/R.con" -> true + | _ -> false) + |_->false) + |_->false +;; + +let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;; + +let mkAppL a = + Cic.Appl(Array.to_list a) +;; + +(* Résolution d'inéquations linéaires dans R *) +let rec strip_outer_cast c = match c with + | Cic.Cast (c,_) -> strip_outer_cast c + | _ -> c +;; + +let find_in_context id context = + let rec find_in_context_aux c n = + match c with + [] -> failwith (id^" not found in context") + | a::next -> (match a with + Some (Cic.Name(name),_) when name = id -> n + (*? magari al posto di _ qualcosaltro?*) + | _ -> find_in_context_aux next (n+1)) + in + find_in_context_aux context 1 +;; + +(* mi sembra quadratico *) +let rec filter_real_hyp context cont = + match context with + [] -> [] + | Some(Cic.Name(h),Cic.Decl(t))::next -> ( + let n = find_in_context h cont in + [(Cic.Rel(n),t)] @ filter_real_hyp next cont) + | a::next -> debug(" no\n"); filter_real_hyp next cont +;; + +(* lifts everithing at the conclusion level *) +let rec superlift c n= + match c with + [] -> [] + | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl( + CicSubstitution.lift n a))] @ superlift next (n+1) + | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def( + CicSubstitution.lift n a))] @ superlift next (n+1) + | _::next -> superlift next (n+1) (*?? ??*) + +;; + +let equality_replace a b ~status = +debug("inizio EQ\n"); + let module C = Cic in + let proof,goal = status in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in +debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl))); + let (proof,goals) = + rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) + ~status:((curi,metasenv',pbo,pty),goal) + in + let new_goals = fresh_meta::goals in +debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " + ^string_of_int( List.length goals)^"+ meta\n"); + (proof,new_goals) +;; + +let tcl_fail a ~status:(proof,goal) = + match a with + 1 -> raise (ProofEngineTypes.Fail "fail-tactical") + |_-> (proof,[goal]) +;; + + +let assumption_tac ~status:(proof,goal)= + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let num = ref 0 in + let tac_list = List.map + ( fun x -> num := !num + 1; + match x with + Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num))) + | _ -> ("fake",tcl_fail 1) + ) + context + in + Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal) +;; + +(* !!!!! fix !!!!!!!!!! *) +let contradiction_tac ~status:(proof,goal)= + Tacticals.then_ + ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) + ~continuation:(Tacticals.then_ + ~start:(Ring.elim_type_tac ~term:_False) + ~continuation:(assumption_tac)) + ~status:(proof,goal) +;; + +(* ********************* TATTICA ******************************** *) + +let rec fourier ~status:(s_proof,s_goal)= + let s_curi,s_metasenv,s_pbo,s_pty = s_proof in + let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal) + s_metasenv in + + debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n"); + debug_pcontext s_context; + + let fhyp = String.copy "new_hyp_for_fourier" in + +(* here we need to negate the thesis, but to do this we need to apply the right +theoreme,so let's parse our thesis *) + + let th_to_appl = ref _Rfourier_not_le_gt in + (match s_ty with + Cic.Appl ( Cic.Const(u,boh)::args) -> + (match UriManager.string_of_uri u with + "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl := + _Rfourier_not_ge_lt + |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl := + _Rfourier_not_gt_le + |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl := + _Rfourier_not_le_gt + |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl := + _Rfourier_not_lt_ge + |_-> failwith "fourier can't be applyed") + |_-> failwith "fourier can't be applyed"); + (* fix maybe strip_outer_cast goes here?? *) + + (* now let's change our thesis applying the th and put it with hp *) + + let proof,gl = Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) + ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp) + ~status:(s_proof,s_goal) in + let goal = if List.length gl = 1 then List.hd gl + else failwith "a new goal" in + + debug ("port la tesi sopra e la nego. contesto :\n"); + debug_pcontext s_context; + + (* now we have all the right environment *) + + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + + + (* now we want to convert hp to inequations, but first we must lift + everyting to thesis level, so that a variable has the save Rel(n) + in each hp ( needed by ineq1_of_term ) *) + + (* ? fix if None ?????*) + (* fix change superlift with a real name *) + + let l_context = superlift context 1 in + let hyps = filter_real_hyp l_context l_context in + + debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n"); + + let lineq =ref [] in + + (* transform hyps into inequations *) + + List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq)) + with _-> ()) + hyps; + + + debug ("applico fourier a "^ string_of_int (List.length !lineq)^ + " disequazioni\n"); + + let res=fourier_lineq (!lineq) in + let tac=ref Ring.id_tac in + if res=[] then + (print_string "Tactic Fourier fails.\n";flush stdout; + failwith "fourier_tac fails") + else + ( + match res with (*match res*) + [(cres,sres,lc)]-> + + (* in lc we have the coefficient to "reduce" the system *) + + print_string "Fourier's method can prove the goal...\n";flush stdout; + + debug "I coeff di moltiplicazione rit sono: "; + + let lutil=ref [] in + List.iter + (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil); + (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *)) + ) + (List.combine (!lineq) lc); + + print_string (" quindi lutil e' lunga "^ + string_of_int (List.length (!lutil))^"\n"); + + (* on construit la combinaison linéaire des inéquation *) + + (match (!lutil) with (*match (!lutil) *) + (h1,c1)::lutil -> + debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n"; + + let s=ref (h1.hstrict) in + + + let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in + let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in + + List.iter (fun (h,c) -> + s:=(!s)||(h.hstrict); + t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl + [_Rmult;rational_to_real c;h.hleft ] ]); + t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl + [_Rmult;rational_to_real c;h.hright] ])) + lutil; + + let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in + let tc=rational_to_real cres in + + +(* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *) + + debug "inizio a costruire tac1\n"; + Fourier.print_rational(c1); + + let tac1=ref ( fun ~status -> + if h1.hstrict then + (Tacticals.thens + ~start:( + fun ~status -> + debug ("inizio t1 strict\n"); + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find + (function (m,_,_) -> m=goal) metasenv in + debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); + PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status) + ~continuations:[tac_use h1;tac_zero_inf_pos + (rational_to_fraction c1)] + ~status + ) + else + (Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le) + ~continuations:[tac_use h1;tac_zero_inf_pos + (rational_to_fraction c1)] ~status + ) + ) + + in + s:=h1.hstrict; + List.iter (fun (h,c) -> + (if (!s) then + (if h.hstrict then + (debug("tac1 1\n"); + tac1:=(Tacticals.thens + ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_lt_lt) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + else + (debug("tac1 2\n"); + Fourier.print_rational(c1); + tac1:=(Tacticals.thens + ~start:( + fun ~status -> + debug("INIZIO TAC 1 2\n"); + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) + metasenv in + debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); + PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + ) + else + (if h.hstrict then + (debug("tac1 3\n"); + tac1:=(Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + else + (debug("tac1 4\n"); + tac1:=(Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + ) + ); + s:=(!s)||(h.hstrict)) lutil;(*end List.iter*) + + let tac2 = + if sres then + tac_zero_inf_false goal (rational_to_fraction cres) + else + tac_zero_infeq_false goal (rational_to_fraction cres) + in + tac:=(Tacticals.thens + ~start:(my_cut ~term:ineq) + ~continuations:[Tacticals.then_ + ~start:(fun ~status:(proof,goal as status) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) + metasenv in + PrimitiveTactics.change_tac ~what:ty + ~with_what:(Cic.Appl [ _not; ineq]) ~status) + ~continuation:(Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term: + (if sres then _Rnot_lt_lt else _Rnot_le_le)) + ~continuation:(Tacticals.thens + ~start:( + fun ~status -> + let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc + ~status + in + (match r with (p,gl) -> + debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" )); + r) + ~continuations:[(Tacticals.thens + ~start:( + fun ~status -> + let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in + (match r with (p,gl) -> + debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" )); + r) + ~continuations: + [PrimitiveTactics.apply_tac ~term:_Rinv_R1 +(* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno + di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i + parametri della equality_replace vengono passati al contrario? Oppure la + tattica usa i parametri al contrario? + ~continuations:[Tacticals.then_ + ~start:( + fun ~status:(proof,goal as status) -> + debug("ECCOCI\n"); + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m= + goal) metasenv in + debug("ty = "^CicPp.ppterm ty^"\n"); + let r = PrimitiveTactics.apply_tac ~term:_sym_eqT + ~status in + debug("fine ECCOCI\n"); + r) + ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1) +*) + ;Tacticals.try_tactics + ~tactics:[ "ring", (fun ~status -> + debug("begin RING\n"); + let r = Ring.ring_tac ~status in + debug ("end RING\n"); + r) + ; "id", Ring.id_tac] + ]) +(* CSC: NOW THE BUG IS HERE: tac2 DOES NOT WORK ANY MORE *) + ;tac2])) + ;!tac1]);(*end tac:=*) + tac:=(Tacticals.thens + ~start:(PrimitiveTactics.cut_tac ~term:_False) + ~continuations:[Tacticals.then_ + ~start:(PrimitiveTactics.intros_tac ~name:"??") + ~continuation:contradiction_tac + ;!tac]) + + + |_-> assert false)(*match (!lutil) *) + |_-> assert false); (*match res*) + debug ("finalmente applico tac\n"); + (!tac ~status:(proof,goal)) +;; + +let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);; + + diff --git a/helm/gTopLevel/fourierR.mli b/helm/gTopLevel/fourierR.mli new file mode 100644 index 000000000..fbd55e685 --- /dev/null +++ b/helm/gTopLevel/fourierR.mli @@ -0,0 +1,2 @@ +val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic +val fourier_tac: ProofEngineTypes.tactic diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml new file mode 100644 index 000000000..83d959ca3 --- /dev/null +++ b/helm/gTopLevel/gTopLevel.ml @@ -0,0 +1,1653 @@ +(* Copyright (C) 2000-2002, 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 *) +(* 06/01/2002 *) +(* *) +(* *) +(******************************************************************************) + + +(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *) +let wrong_xpointer_format_from_wrong_xpointer_format' uri = + try + let index_sharp = String.index uri '#' in + let index_rest = index_sharp + 10 in + let baseuri = String.sub uri 0 index_sharp in + let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in + baseuri ^ "#" ^ rest + with Not_found -> uri +;; + +(* GLOBAL CONSTANTS *) + +let helmns = Gdome.domString "http://www.cs.unibo.it/helm";; + +let htmlheader = + "" ^ + " " +;; + +let htmlfooter = + " " ^ + "" +;; + +(* +let prooffile = "/home/tassi/miohelm/tmp/currentproof";; +*) +let prooffile = "/public/sacerdot/currentproof";; +(*CSC: the getter should handle the innertypes, not the FS *) +(* +let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; +*) +let innertypesfile = "/public/sacerdot/innertypes";; + +(* GLOBAL REFERENCES (USED BY CALLBACKS) *) + +let htmlheader_and_content = ref htmlheader;; + +let current_cic_infos = ref None;; +let current_goal_infos = ref None;; +let current_scratch_infos = ref None;; + +(* COMMAND LINE OPTIONS *) + +let usedb = ref true + +let argspec = + [ + "-nodb", Arg.Clear usedb, "disable use of MathQL DB" + ] +in +Arg.parse argspec ignore "" + + +(* 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 getterURL = Configuration.getter_url;; +let processorURL = Configuration.processor_url;; + +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", "'yes'" ; + "annotations", "'no'" ; + "explodeall", "'true()'" ; + "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'" ; + "explodeall", "'true()'" ; + "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_object uri annobj ids_to_inner_sorts ids_to_inner_types = + let xml = + Cic2Xml.print_object uri ~ids_to_inner_sorts annobj + in + let xmlinnertypes = + Cic2Xml.print_inner_types uri ~ids_to_inner_sorts + ~ids_to_inner_types + in + let input = Xml2Gdome.document_of_xml domImpl xml in +(*CSC: We save the innertypes to disk so that we can retrieve them in the *) +(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *) +(*CSC: local. *) + Xml.pp xmlinnertypes (Some innertypesfile) ; + let output = applyStylesheets input mml_styles mml_args in + output +;; + + +(* CALLBACKS *) + +exception RefreshSequentException of exn;; +exception RefreshProofException of exn;; + +let refresh_proof (output : GMathView.math_view) = + try + let uri,currentproof = + match !ProofEngine.proof with + None -> assert false + | Some (uri,metasenv,bo,ty) -> + uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty)) + in + 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 uri acic ids_to_inner_sorts ids_to_inner_types + in + output#load_tree mml ; + current_cic_infos := + Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) + with + e -> + match !ProofEngine.proof with + None -> assert false + | Some (uri,metasenv,bo,ty) -> +prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty))) ; flush stderr ; + raise (RefreshProofException e) +;; + +let refresh_sequent (proofw : GMathView.math_view) = + try + match !ProofEngine.goal with + None -> proofw#unload + | Some metano -> + let metasenv = + match !ProofEngine.proof with + None -> assert false + | Some (_,metasenv,_,_) -> metasenv + in + let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in + let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses = + SequentPp.XmlPp.print_sequent metasenv currentsequent + in + let sequent_doc = + Xml2Gdome.document_of_xml domImpl sequent_gdome + in + let sequent_mml = + applyStylesheets sequent_doc sequent_styles sequent_args + in + proofw#load_tree ~dom:sequent_mml ; + current_goal_infos := + Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) + with + e -> +let metano = + match !ProofEngine.goal with + None -> assert false + | Some m -> m +in +let metasenv = + match !ProofEngine.proof with + None -> assert false + | Some (_,metasenv,_,_) -> metasenv +in +let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in +prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ; + raise (RefreshSequentException e) +;; + +(* +ignore(domImpl#saveDocumentToFile ~doc:sequent_doc + ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ; +*) + +let mml_of_cic_term metano term = + let metasenv = + match !ProofEngine.proof with + None -> [] + | Some (_,metasenv,_,_) -> metasenv + in + let context = + match !ProofEngine.goal with + None -> [] + | Some metano -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=metano) metasenv + in + canonical_context + in + let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses = + SequentPp.XmlPp.print_sequent metasenv (metano,context,term) + in + let sequent_doc = + Xml2Gdome.document_of_xml domImpl sequent_gdome + in + let res = + applyStylesheets sequent_doc sequent_styles sequent_args ; + in + current_scratch_infos := + Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ; + res +;; + +let output_html outputhtml msg = + htmlheader_and_content := !htmlheader_and_content ^ msg ; + outputhtml#source (!htmlheader_and_content ^ htmlfooter) ; + outputhtml#set_topline (-1) +;; + +(***********************) +(* TACTICS *) +(***********************) + +let call_tactic tactic rendering_window () = + let proofw = (rendering_window#proofw : GMathView.math_view) in + let output = (rendering_window#output : GMathView.math_view) in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + begin + try + tactic () ; + refresh_sequent proofw ; + refresh_proof output + with + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw ; + refresh_proof output + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + end +;; + +let call_tactic_with_input tactic rendering_window () = + let proofw = (rendering_window#proofw : GMathView.math_view) in + let output = (rendering_window#output : GMathView.math_view) in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let inputt = (rendering_window#inputt : GEdit.text) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal 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 + let curi = + match !ProofEngine.proof with + None -> assert false + | Some (curi,_,_,_) -> curi + in + let uri,metasenv,bo,ty = + match !ProofEngine.proof with + None -> assert false + | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty + in + let context = + List.map + (function + Some (n,_) -> Some n + | None -> None) + (match !ProofEngine.goal with + None -> assert false + | Some metano -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=metano) metasenv + in + canonical_context + ) + in + try + while true do + match + CicTextualParserContext.main + curi context metasenv CicTextualLexer.token lexbuf + with + None -> () + | Some (metasenv',expr) -> + ProofEngine.proof := Some (uri,metasenv',bo,ty) ; + tactic expr ; + refresh_sequent proofw ; + refresh_proof output + done + with + CicTextualParser0.Eof -> + inputt#delete_text 0 inputlen + | RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw ; + refresh_proof output + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; +;; + +let call_tactic_with_goal_input tactic rendering_window () = + let module L = LogicalOperations in + let module G = Gdome in + let proofw = (rendering_window#proofw : GMathView.math_view) in + let output = (rendering_window#output : GMathView.math_view) in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + match proofw#get_selection with + Some node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:helmns + ~localName:(G.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + begin + try + match !current_goal_infos with + Some (ids_to_terms, ids_to_father_ids,_) -> + let id = xpath in + tactic (Hashtbl.find ids_to_terms id) ; + refresh_sequent rendering_window#proofw ; + refresh_proof rendering_window#output + | None -> assert false (* "ERROR: No current term!!!" *) + with + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw ; + refresh_proof output + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + end + | None -> + output_html outputhtml + ("

No term selected

") +;; + +let call_tactic_with_input_and_goal_input tactic rendering_window () = + let module L = LogicalOperations in + let module G = Gdome in + let proofw = (rendering_window#proofw : GMathView.math_view) in + let output = (rendering_window#output : GMathView.math_view) in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let inputt = (rendering_window#inputt : GEdit.text) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + match proofw#get_selection with + Some node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:helmns + ~localName:(G.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + begin + try + match !current_goal_infos with + Some (ids_to_terms, ids_to_father_ids,_) -> + let id = xpath in + (* Let's parse the input *) + let inputlen = inputt#length in + let input = inputt#get_chars 0 inputlen ^ "\n" in + let lexbuf = Lexing.from_string input in + let curi = + match !ProofEngine.proof with + None -> assert false + | Some (curi,_,_,_) -> curi + in + let uri,metasenv,bo,ty = + match !ProofEngine.proof with + None -> assert false + | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty + in + let context = + List.map + (function + Some (n,_) -> Some n + | None -> None) + (match !ProofEngine.goal with + None -> assert false + | Some metano -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=metano) metasenv + in + canonical_context + ) + in + begin + try + while true do + match + CicTextualParserContext.main curi context metasenv + CicTextualLexer.token lexbuf + with + None -> () + | Some (metasenv',expr) -> + ProofEngine.proof := Some (uri,metasenv',bo,ty) ; + tactic ~goal_input:(Hashtbl.find ids_to_terms id) + ~input:expr ; + refresh_sequent proofw ; + refresh_proof output + done + with + CicTextualParser0.Eof -> + inputt#delete_text 0 inputlen + end + | None -> assert false (* "ERROR: No current term!!!" *) + with + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw ; + refresh_proof output + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + end + | None -> + output_html outputhtml + ("

No term selected

") +;; + +let call_tactic_with_goal_input_in_scratch tactic scratch_window () = + let module L = LogicalOperations in + let module G = Gdome in + let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in + let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + match mmlwidget#get_selection with + Some node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:helmns + ~localName:(G.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + begin + try + match !current_scratch_infos with + (* term is the whole goal in the scratch_area *) + Some (term,ids_to_terms, ids_to_father_ids,_) -> + let id = xpath in + let expr = tactic term (Hashtbl.find ids_to_terms id) in + let mml = mml_of_cic_term 111 expr in + scratch_window#show () ; + scratch_window#mmlwidget#load_tree ~dom:mml + | None -> assert false (* "ERROR: No current term!!!" *) + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") + end + | None -> + output_html outputhtml + ("

No term selected

") +;; + +let call_tactic_with_hypothesis_input tactic rendering_window () = + let module L = LogicalOperations in + let module G = Gdome in + let proofw = (rendering_window#proofw : GMathView.math_view) in + let output = (rendering_window#output : GMathView.math_view) in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + match proofw#get_selection with + Some node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:helmns + ~localName:(G.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + begin + try + match !current_goal_infos with + Some (_,_,ids_to_hypotheses) -> + let id = xpath in + tactic (Hashtbl.find ids_to_hypotheses id) ; + refresh_sequent rendering_window#proofw ; + refresh_proof rendering_window#output + | None -> assert false (* "ERROR: No current term!!!" *) + with + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw ; + refresh_proof output + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + end + | None -> + output_html outputhtml + ("

No term selected

") +;; + + +let intros rendering_window = call_tactic ProofEngine.intros rendering_window;; +let exact rendering_window = + call_tactic_with_input ProofEngine.exact rendering_window +;; +let apply rendering_window = + call_tactic_with_input ProofEngine.apply rendering_window +;; +let elimintrossimpl rendering_window = + call_tactic_with_input ProofEngine.elim_intros_simpl rendering_window +;; +let elimtype rendering_window = + call_tactic_with_input ProofEngine.elim_type rendering_window +;; +let whd rendering_window = + call_tactic_with_goal_input ProofEngine.whd rendering_window +;; +let reduce rendering_window = + call_tactic_with_goal_input ProofEngine.reduce rendering_window +;; +let simpl rendering_window = + call_tactic_with_goal_input ProofEngine.simpl rendering_window +;; +let fold rendering_window = + call_tactic_with_input ProofEngine.fold rendering_window +;; +let cut rendering_window = + call_tactic_with_input ProofEngine.cut rendering_window +;; +let change rendering_window = + call_tactic_with_input_and_goal_input ProofEngine.change rendering_window +;; +let letin rendering_window = + call_tactic_with_input ProofEngine.letin rendering_window +;; +let ring rendering_window = call_tactic ProofEngine.ring rendering_window;; +let clearbody rendering_window = + call_tactic_with_hypothesis_input ProofEngine.clearbody rendering_window +;; +let clear rendering_window = + call_tactic_with_hypothesis_input ProofEngine.clear rendering_window +;; +let fourier rendering_window = + call_tactic ProofEngine.fourier rendering_window +;; +let rewritesimpl rendering_window = + call_tactic_with_input ProofEngine.rewrite_simpl rendering_window +;; + + + +let whd_in_scratch scratch_window = + call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch + scratch_window +;; +let reduce_in_scratch scratch_window = + call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch + scratch_window +;; +let simpl_in_scratch scratch_window = + call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch + scratch_window +;; + + + +(**********************) +(* END OF TACTICS *) +(**********************) + +exception OpenConjecturesStillThere;; +exception WrongProof;; + +let qed rendering_window () = + match !ProofEngine.proof with + None -> assert false + | Some (uri,[],bo,ty) -> + if + CicReduction.are_convertible [] + (CicTypeChecker.type_of_aux' [] [] bo) ty + then + begin + (*CSC: Wrong: [] is just plainly wrong *) + let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in + 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 proof + in + let mml = + mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types + in + (rendering_window#output : GMathView.math_view)#load_tree mml ; + current_cic_infos := + Some + (ids_to_terms,ids_to_father_ids,ids_to_conjectures, + ids_to_hypotheses) + end + else + raise WrongProof + | _ -> raise OpenConjecturesStillThere +;; + +(*???? +let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";; +*) +let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";; + +let save rendering_window () = + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + match !ProofEngine.proof with + None -> assert false + | Some (uri, metasenv, bo, ty) -> + let currentproof = + Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty) + in + let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) = + Cic2acic.acic_object_of_cic_object currentproof + in + let xml = Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof in + let xml' = + [< Xml.xml_cdata "\n" ; + Xml.xml_cdata + ("\n\n") ; + xml + >] + in + Xml.pp ~quiet:true xml' (Some prooffile) ; + output_html outputhtml + ("

Current proof saved to " ^ + prooffile ^ "

") +;; + +(* Used to typecheck the loaded proofs *) +let typecheck_loaded_proof metasenv bo ty = + let module T = CicTypeChecker in + (*CSC: bisogna controllare anche il metasenv!!! *) + ignore (T.type_of_aux' metasenv [] ty) ; + ignore (T.type_of_aux' metasenv [] bo) +;; + +let load rendering_window () = + 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 + try + let uri = UriManager.uri_of_string "cic:/dummy.con" in + match CicParser.obj_of_xml prooffile uri with + Cic.CurrentProof (_,metasenv,bo,ty) -> + typecheck_loaded_proof metasenv bo ty ; + ProofEngine.proof := + Some (uri, metasenv, bo, ty) ; + ProofEngine.goal := + (match metasenv with + [] -> None + | (metano,_,_)::_ -> Some metano + ) ; + refresh_proof output ; + refresh_sequent proofw ; + output_html outputhtml + ("

Current proof loaded from " ^ + prooffile ^ "

") + | _ -> assert false + with + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; +;; + +let proveit rendering_window () = + let module L = LogicalOperations in + let module G = Gdome in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) 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 + try + match !current_cic_infos with + Some (ids_to_terms, ids_to_father_ids, _, _) -> + let id = xpath in + L.to_sequent id ids_to_terms ids_to_father_ids ; + refresh_proof rendering_window#output ; + refresh_sequent rendering_window#proofw + | None -> assert false (* "ERROR: No current term!!!" *) + with + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") + end + | None -> assert false (* "ERROR: No selection!!!" *) +;; + +let focus rendering_window () = + let module L = LogicalOperations in + let module G = Gdome in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) 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 + try + match !current_cic_infos with + Some (ids_to_terms, ids_to_father_ids, _, _) -> + let id = xpath in + L.focus id ids_to_terms ids_to_father_ids ; + refresh_sequent rendering_window#proofw + | None -> assert false (* "ERROR: No current term!!!" *) + with + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") + end + | None -> assert false (* "ERROR: No selection!!!" *) +;; + +exception NoPrevGoal;; +exception NoNextGoal;; + +let prevgoal metasenv metano = + let rec aux = + function + [] -> assert false + | [(m,_,_)] -> raise NoPrevGoal + | (n,_,_)::(m,_,_)::_ when m=metano -> n + | _::tl -> aux tl + in + aux metasenv +;; + +let nextgoal metasenv metano = + let rec aux = + function + [] -> assert false + | [(m,_,_)] when m = metano -> raise NoNextGoal + | (m,_,_)::(n,_,_)::_ when m=metano -> n + | _::tl -> aux tl + in + aux metasenv +;; + +let prev_or_next_goal select_goal rendering_window () = + let module L = LogicalOperations in + let module G = Gdome in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let metasenv = + match !ProofEngine.proof with + None -> assert false + | Some (_,metasenv,_,_) -> metasenv + in + let metano = + match !ProofEngine.goal with + None -> assert false + | Some m -> m + in + try + ProofEngine.goal := Some (select_goal metasenv metano) ; + refresh_sequent rendering_window#proofw + with + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") +;; + +exception NotADefinition;; + +let open_ 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 + try + let uri = UriManager.uri_of_string ("cic:" ^ input) in + CicTypeChecker.typecheck uri ; + let metasenv,bo,ty = + match CicEnvironment.get_cooked_obj uri 0 with + Cic.Definition (_,bo,ty,_) -> [],bo,ty + | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty + | Cic.Axiom _ + | Cic.Variable _ + | Cic.InductiveDefinition _ -> raise NotADefinition + in + ProofEngine.proof := + Some (uri, metasenv, bo, ty) ; + ProofEngine.goal := None ; + refresh_sequent proofw ; + refresh_proof output ; + inputt#delete_text 0 inputlen ; + ignore(oldinputt#insert_text input oldinputt#length) + with + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; +;; + +let state 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 -> + let _ = CicTypeChecker.type_of_aux' [] [] expr in + ProofEngine.proof := + Some (UriManager.uri_of_string "cic:/dummy.con", + [1,[],expr], Cic.Meta (1,[]), expr) ; + ProofEngine.goal := Some 1 ; + refresh_sequent proofw ; + refresh_proof output ; + done + with + CicTextualParser0.Eof -> + inputt#delete_text 0 inputlen ; + ignore(oldinputt#insert_text input oldinputt#length) + | RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; +;; + +let check rendering_window scratch_window () = + let inputt = (rendering_window#inputt : 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 + let curi,metasenv = + match !ProofEngine.proof with + None -> UriManager.uri_of_string "cic:/dummy.con", [] + | Some (curi,metasenv,_,_) -> curi,metasenv + in + let context,names_context = + let context = + match !ProofEngine.goal with + None -> [] + | Some metano -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=metano) metasenv + in + canonical_context + in + context, + List.map + (function + Some (n,_) -> Some n + | None -> None + ) context + in + (* Do something interesting *) + let lexbuf = Lexing.from_string input in + try + while true do + (* Execute the actions *) + match + CicTextualParserContext.main curi names_context metasenv + CicTextualLexer.token lexbuf + with + None -> () + | Some (metasenv',expr) -> + try + let ty = CicTypeChecker.type_of_aux' metasenv' context expr in + let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in + scratch_window#show () ; + scratch_window#mmlwidget#load_tree ~dom:mml + with + e -> + print_endline ("? " ^ CicPp.ppterm expr) ; + raise e + done + with + CicTextualParser0.Eof -> () + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; +;; + +exception NoObjectsLocated;; + +let user_uri_choice uris = + let uri = + match uris with + [] -> raise NoObjectsLocated + | [uri] -> uri + | uris -> + let choice = + GToolbox.question_box ~title:"Ambiguous result." + ~buttons:uris ~default:1 + "Ambiguous result. Please, choose one." + in + List.nth uris (choice-1) + in + String.sub uri 4 (String.length uri - 4) +;; + +(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *) +let get_last_query = + let query = ref "" in + MQueryGenerator.set_confirm_query + (function q -> query := MQueryUtil.text_of_query q ; true) ; + function result -> !query ^ "

Result:

" ^ MQueryUtil.text_of_result result "
" +;; + +let locate rendering_window () = + let inputt = (rendering_window#inputt : GEdit.text) in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let inputlen = inputt#length in + let input = inputt#get_chars 0 inputlen in + try + match Str.split (Str.regexp "[ \t]+") input with + [] -> () + | head :: tail -> + inputt#delete_text 0 inputlen ; + let result = MQueryGenerator.locate head in + let uris = + List.map + (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) + result in + let html = ("

Locate Query: 

" ^ get_last_query result ^ "
") in + output_html outputhtml html ; + let uri' = user_uri_choice uris in + ignore ((inputt#insert_text uri') ~pos:0) + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") +;; + +let backward rendering_window () = + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let inputt = (rendering_window#inputt : GEdit.text) in + let inputlen = inputt#length in + let input = inputt#get_chars 0 inputlen in + let level = int_of_string input in + let metasenv = + match !ProofEngine.proof with + None -> assert false + | Some (_,metasenv,_,_) -> metasenv + in + try + match !ProofEngine.goal with + None -> () + | Some metano -> + let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in + let result = MQueryGenerator.backward metasenv ey ty level in + let uris = + List.map + (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) + result in + let html = + "

Backward Query:

" ^ + "

Levels:

" ^ + MQueryGenerator.string_of_levels (MQueryGenerator.levels_of_term metasenv ey ty) "
" ^ + " 
" ^ get_last_query result ^ "
" in + output_html outputhtml html ; + let uri' = user_uri_choice uris in + inputt#delete_text 0 inputlen ; + ignore ((inputt#insert_text uri') ~pos:0) + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") +;; + +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;; + +(* Scratch window *) + +class scratch_window outputhtml = + let window = + GWindow.window ~title:"MathML viewer" ~border_width:2 () in + let vbox = + GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let whdb = + GButton.button ~label:"Whd" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let reduceb = + GButton.button ~label:"Reduce" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let simplb = + GButton.button ~label:"Simpl" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 + ~packing:(vbox#pack ~expand:true ~padding:5) () in + let mmlwidget = + GMathView.math_view + ~packing:(scrolled_window#add) ~width:400 ~height:280 () in +object(self) + method outputhtml = outputhtml + method mmlwidget = mmlwidget + method show () = window#misc#hide () ; window#show () + initializer + ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ; + ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ; + ignore(whdb#connect#clicked (whd_in_scratch self)) ; + ignore(reduceb#connect#clicked (reduce_in_scratch self)) ; + ignore(simplb#connect#clicked (simpl_in_scratch self)) +end;; + +(* Main window *) + +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 qedb = + GButton.button ~label:"Qed" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let saveb = + GButton.button ~label:"Save" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let loadb = + GButton.button ~label:"Load" + ~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 focusb = + GButton.button ~label:"Focus" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let prevgoalb = + GButton.button ~label:"<" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let nextgoalb = + GButton.button ~label:">" + ~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 hbox4 = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let stateb = + GButton.button ~label:"State" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let openb = + GButton.button ~label:"Open" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let checkb = + GButton.button ~label:"Check" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let locateb = + GButton.button ~label:"Locate" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let backwardb = + GButton.button ~label:"Backward" + ~packing:(hbox4#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 introsb = + GButton.button ~label:"Intros" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let applyb = + GButton.button ~label:"Apply" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let elimintrossimplb = + GButton.button ~label:"ElimIntrosSimpl" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let elimtypeb = + GButton.button ~label:"ElimType" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let whdb = + GButton.button ~label:"Whd" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let reduceb = + GButton.button ~label:"Reduce" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let simplb = + GButton.button ~label:"Simpl" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let foldb = + GButton.button ~label:"Fold" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let cutb = + GButton.button ~label:"Cut" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let changeb = + GButton.button ~label:"Change" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let hbox4 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in + let letinb = + GButton.button ~label:"Let ... In" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let ringb = + GButton.button ~label:"Ring" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let clearbodyb = + GButton.button ~label:"ClearBody" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let clearb = + GButton.button ~label:"Clear" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let fourierb = + GButton.button ~label:"Fourier" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let rewritesimplb = + GButton.button ~label:"RewriteSimpl ->" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let outputhtml = + GHtml.xmhtml + ~source:"" + ~width:400 ~height: 200 + ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) + ~show:true () in + let scratch_window = new scratch_window outputhtml 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(qedb#connect#clicked (qed self)) ; + ignore(saveb#connect#clicked (save self)) ; + ignore(loadb#connect#clicked (load self)) ; + ignore(proveitb#connect#clicked (proveit self)) ; + ignore(focusb#connect#clicked (focus self)) ; + ignore(prevgoalb#connect#clicked (prev_or_next_goal prevgoal self)) ; + ignore(nextgoalb#connect#clicked (prev_or_next_goal nextgoal self)) ; + ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; + ignore(stateb#connect#clicked (state self)) ; + ignore(openb#connect#clicked (open_ self)) ; + ignore(checkb#connect#clicked (check self scratch_window)) ; + ignore(locateb#connect#clicked (locate self)) ; + ignore(backwardb#connect#clicked (backward self)) ; + ignore(exactb#connect#clicked (exact self)) ; + ignore(applyb#connect#clicked (apply self)) ; + ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ; + ignore(elimtypeb#connect#clicked (elimtype self)) ; + ignore(whdb#connect#clicked (whd self)) ; + ignore(reduceb#connect#clicked (reduce self)) ; + ignore(simplb#connect#clicked (simpl self)) ; + ignore(foldb#connect#clicked (fold self)) ; + ignore(cutb#connect#clicked (cut self)) ; + ignore(changeb#connect#clicked (change self)) ; + ignore(letinb#connect#clicked (letin self)) ; + ignore(ringb#connect#clicked (ring self)) ; + ignore(clearbodyb#connect#clicked (clearbody self)) ; + ignore(clearb#connect#clicked (clear self)) ; + ignore(fourierb#connect#clicked (fourier self)) ; + ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ; + ignore(introsb#connect#clicked (intros self)) ; + Logger.log_callback := + (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) +end;; + +(* MAIN *) + +let rendering_window = ref None;; + +let initialize_everything () = + let module U = Unix in + let output = GMathView.math_view ~width:350 ~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 := Some rendering_window' ; + rendering_window'#show () ; + GMain.Main.main () +;; + +let _ = + CicCooking.init () ; + if !usedb then + begin + Mqint.init "host=mowgli.cs.unibo.it dbname=helm user=helm" ; + CicTextualParser0.set_locate_object + (function id -> + let result = MQueryGenerator.locate id in + let uris = + List.map + (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) + result in + let html = ("

Locate Query: 

" ^ get_last_query result ^ "
") in + begin + match !rendering_window with + None -> assert false + | Some rw -> output_html rw#outputhtml html ; + end ; + let uri = + match uris with + [] -> + (match + (GToolbox.input_string ~title:"Unknown input" + ("No URI matching \"" ^ id ^ "\" found. Please enter its URI")) + with + None -> None + | Some uri -> Some ("cic:" ^ uri) + ) + | [uri] -> Some uri + | _ -> + let choice = + GToolbox.question_box ~title:"Ambiguous input." + ~buttons:uris ~default:1 "Ambiguous input. Please, choose one." + in + if choice > 0 then + Some (List.nth uris (choice - 1)) + else + (* No choice from the user *) + None + in + match uri with + Some uri' -> + (* Constant *) + if String.sub uri' (String.length uri' - 4) 4 = ".con" then +(*CSC: what cooking number? Here I always use 0, which may be bugged *) + Some (Cic.Const (UriManager.uri_of_string uri',0)) + else + (try + (* Inductive Type *) + let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in +(*CSC: what cooking number? Here I always use 0, which may be bugged *) + Some (Cic.MutInd (uri'',0,typeno)) + with + _ -> + (* Constructor of an Inductive Type *) + let uri'',typeno,consno = + CicTextualLexer.indconuri_of_uri uri' + in +(*CSC: what cooking number? Here I always use 0, which may be bugged *) + Some (Cic.MutConstruct (uri'',0,typeno,consno)) + ) + | None -> None + ) + end ; + ignore (GtkMain.Main.init ()) ; + initialize_everything () ; + if !usedb then Mqint.close (); +;; diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml new file mode 100644 index 000000000..4deaf8c7a --- /dev/null +++ b/helm/gTopLevel/mQueryGenerator.ml @@ -0,0 +1,228 @@ +(* 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 *) +(* *) +(* Ferruccio Guidi *) +(* 30/04/2002 *) +(* *) +(* *) +(******************************************************************************) + +(* level managing functions *************************************************) + +type levels_spec = (string * bool * int) list + +let levels_of_term metasenv context term = + let module TC = CicTypeChecker in + let module Red = CicReduction in + let module Util = MQueryUtil in + let degree t = + let rec degree_aux = function + | Cic.Sort _ -> 1 + | Cic.Cast (u, _) -> degree_aux u + | Cic.Prod (_, _, t) -> degree_aux t + | _ -> 2 + in + let u = TC.type_of_aux' metasenv context t in + degree_aux (Red.whd context u) + in + let entry_eq (s1, b1, v1) (s2, b2, v2) = + s1 = s2 && b1 = b2 + in + let rec entry_in e = function + | [] -> [e] + | head :: tail -> + head :: if entry_eq head e then tail else entry_in e tail + in + let inspect_uri main l uri tc v term = + let d = degree term in + entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l + in + let rec inspect_term main l v term = match term with + | Cic.Rel _ -> l + | Cic.Meta (_, _) -> l + | Cic.Sort _ -> l + | Cic.Implicit -> l + | Cic.Var u -> inspect_uri main l u [] v term + | Cic.Const (u, _) -> inspect_uri main l u [] v term + | Cic.MutInd (u, _, t) -> inspect_uri main l u [t] v term + | Cic.MutConstruct (u, _, t, c) -> inspect_uri main l u [t; c] v term + | Cic.Cast (uu, _) -> + inspect_term main l v uu + | Cic.Prod (_, uu, tt) -> + let luu = inspect_term false l (v + 1) uu in + inspect_term main luu (v + 1) tt + | Cic.Lambda (_, uu, tt) -> + let luu = inspect_term false l (v + 1) uu in + inspect_term false luu (v + 1) tt + | Cic.LetIn (_, uu, tt) -> + let luu = inspect_term false l (v + 1) uu in + inspect_term false luu (v + 1) tt + | Cic.Appl m -> inspect_list main l true v m + | Cic.MutCase (u, _, t, tt, uu, m) -> + let lu = inspect_uri main l u [t] (v + 1) term in + let ltt = inspect_term false lu (v + 1) tt in + let luu = inspect_term false ltt (v + 1) uu in + inspect_list main luu false (v + 1) m + | Cic.Fix (_, m) -> inspect_ind l (v + 1) m + | Cic.CoFix (_, m) -> inspect_coind l (v + 1) m + and inspect_list main l head v = function + | [] -> l + | tt :: m -> + let ltt = inspect_term main l (if head then v else v + 1) tt in + inspect_list false ltt false v m + and inspect_ind l v = function + | [] -> l + | (_, _, tt, uu) :: m -> + let ltt = inspect_term false l v tt in + let luu = inspect_term false ltt v uu in + inspect_ind luu v m + and inspect_coind l v = function + | [] -> l + | (_, tt, uu) :: m -> + let ltt = inspect_term false l v tt in + let luu = inspect_term false ltt v uu in + inspect_coind luu v m + in + let rec inspect_backbone = function + | Cic.Cast (uu, _) -> inspect_backbone uu + | Cic.Prod (_, _, tt) -> inspect_backbone tt + | Cic.LetIn (_, uu, tt) -> inspect_backbone tt + | t -> inspect_term true [] 0 t + in + inspect_backbone term + +let string_of_levels l sep = + let entry_out (s, b, v) = + let pos = if b then " HEAD: " else " TAIL: " in + string_of_int v ^ pos ^ s ^ sep + in + let rec levels_out = function + | [] -> "" + | head :: tail -> entry_out head ^ levels_out tail + in + levels_out l + +(* Query issuing functions **************************************************) + +exception Discard + +let nl = "

\n" + +let query_num = ref 1 + +let log_file = ref "" + +let confirm_query = ref (fun _ -> true) + +let info = ref [] + +let set_log_file f = + log_file := f + +let set_confirm_query f = + confirm_query := f + +let get_query_info () = ! info + +let execute_query query = + let module Util = MQueryUtil in + let mode = [Open_wronly; Open_append; Open_creat; Open_text] in + let perm = 64 * 6 + 8 * 6 + 4 in + let time () = + let lt = Unix.localtime (Unix.time ()) in + "NEW LOG: " ^ + string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^ + string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^ + string_of_int (lt.Unix.tm_year + 1900) ^ " " ^ + string_of_int (lt.Unix.tm_hour) ^ ":" ^ + string_of_int (lt.Unix.tm_min) ^ ":" ^ + string_of_int (lt.Unix.tm_sec) + in + let log q r = + let och = open_out_gen mode perm ! log_file in + if ! query_num = 1 then output_string och (time () ^ nl); + let str = "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^ + "Result:" ^ nl ^ Util.text_of_result r nl in + output_string och str; + flush och + in + let execute q = + let r = Mqint.execute q in + if ! log_file <> "" then log q r; + info := string_of_int ! query_num :: ! info; + incr query_num; + r + in + if ! confirm_query query then execute query else raise Discard + +(* Query building functions ************************************************) + +let locate s = + let module M = MathQL in + let q = M.Ref (M.Fun "reference" (M.Const [s])) in + execute_query q + +let backward e c t level = + let module M = MathQL in + let v_pos = M.Const ["MainConclusion"; "InConclusion"] in + let q_where = M.Sub (M.RefOf ( + M.Select ("uri", + M.Relation (M.ExactOp, ["refObj"], M.RVar "uri0", ["pos"]), + M.Ex ["uri"] (M.Meet (M.VVar "positions", M.Record ("uri", "pos"))) + )), M.VVar "universe" + ) + in + let uri_of_entry (r, b, v) = r in + let rec restrict level = function + | [] -> [] + | (u, b, v) :: tail -> + if v <= level then (u, b, v) :: restrict level tail + else restrict level tail + in + let build_select (r, b, v) = + let pos = if b then "MainConclusion" else "InConclusion" in + M.Select ("uri", + M.Relation (M.ExactOp, ["backPointer"], M.Ref (M.Const [r]), ["pos"]), + M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", "pos"))) + ) + in + let rec build_intersect = function + | [] -> M.Pattern (M.Const [".*"]) + | [hd] -> build_select hd + | hd :: tl -> M.Intersect (build_select hd, build_intersect tl) + in + let levels = levels_of_term e c t in + let rest = restrict level levels in + info := [string_of_int (List.length rest)]; + let q_in = build_intersect rest in + let q_select = M.Select ("uri0", q_in, q_where) in + let universe = M.Const (List.map uri_of_entry levels) in + let q_let_u = M.LetVVar ("universe", universe, q_select) in + let q_let_p = M.LetVVar ("positions", v_pos, q_let_u) in + execute_query q_let_p diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli new file mode 100644 index 000000000..57137974f --- /dev/null +++ b/helm/gTopLevel/mQueryGenerator.mli @@ -0,0 +1,55 @@ +(* 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 *) +(* *) +(* Ferruccio Guidi *) +(* 30/04/2002 *) +(* *) +(* *) +(******************************************************************************) + +exception Discard + +type levels_spec = (string * bool * int) list + +val levels_of_term : Cic.metasenv -> Cic.context -> Cic.term -> levels_spec + +val string_of_levels : levels_spec -> string -> string + +val set_log_file : string -> unit + +(* the callback function must return false iff the query must be skipped *) +val set_confirm_query : (MathQL.query -> bool) -> unit + +val execute_query : MathQL.query -> MathQL.result + +val locate : string -> MathQL.result + +val backward : Cic.metasenv -> Cic.context -> Cic.term -> int -> MathQL.result + +val get_query_info : unit -> string list diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml new file mode 100644 index 000000000..5f0ba8aaa --- /dev/null +++ b/helm/gTopLevel/proofEngine.ml @@ -0,0 +1,277 @@ +(* 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/. + *) + +open ProofEngineHelpers +open ProofEngineTypes + + (* proof assistant status *) + +let proof = ref (None : proof option) +let goal = ref (None : goal option) + +let apply_tactic ~tactic:tactic = + match !proof,!goal with + None,_ + | _,None -> assert false + | Some proof', Some goal' -> + let (newproof, newgoals) = tactic ~status:(proof', goal') in + proof := Some newproof; + goal := + (match newgoals, newproof with + goal::_, _ -> Some goal + | [], (_,(goal,_,_)::_,_,_) -> + (* the tactic left no open goal ; let's choose the first open goal *) +(*CSC: here we could implement and use a proof-tree like notion... *) + Some goal + | _, _ -> None) + +(* metas_in_term term *) +(* Returns the ordered list of the metas that occur in [term]. *) +(* Duplicates are removed. The implementation is not very efficient. *) +let metas_in_term term = + let module C = Cic in + let rec aux = + function + C.Rel _ + | C.Var _ -> [] + | C.Meta (n,_) -> [n] + | C.Sort _ + | C.Implicit -> [] + | C.Cast (te,ty) -> (aux te) @ (aux ty) + | C.Prod (_,s,t) -> (aux s) @ (aux t) + | C.Lambda (_,s,t) -> (aux s) @ (aux t) + | C.LetIn (_,s,t) -> (aux s) @ (aux t) + | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l + | C.Const _ + | C.MutInd _ + | C.MutConstruct _ -> [] + | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + (aux outt) @ (aux t) @ + (List.fold_left (fun i t -> i @ (aux t)) [] pl) + | C.Fix (i,fl) -> + List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl + | C.CoFix (i,fl) -> + List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl + in + let metas = aux term in + let rec elim_duplicates = + function + [] -> [] + | he::tl -> + he::(elim_duplicates (List.filter (function el -> he <> el) tl)) + in + elim_duplicates metas + +(* perforate context term ty *) +(* replaces the term [term] in the proof with a new metavariable whose type *) +(* is [ty]. [context] must be the context of [term] in the whole proof. This *) +(* could be easily computed; so the only reasons to have it as an argument *) +(* are efficiency reasons. *) +let perforate context term ty = + let module C = Cic in + match !proof with + None -> assert false + | Some (uri,metasenv,bo,gty as proof') -> + let newmeta = new_meta proof' in + (* We push the new meta at the end of the list for pretty-printing *) + (* purposes: in this way metas are ordered. *) + let metasenv' = metasenv@[newmeta,context,ty] in + let irl = identity_relocation_list_for_metavariable context in +(*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*) + let bo' = + ProofEngineReduction.replace (==) term (C.Meta (newmeta,irl)) bo + in + (* It may be possible that some metavariables occurred only in *) + (* the term we are perforating and they now occurs no more. We *) + (* get rid of them, collecting the really useful metavariables *) + (* in metasenv''. *) +(*CSC: Bug: una meta potrebbe non comparire in bo', ma comparire nel tipo *) +(*CSC: di una metavariabile che compare in bo'!!!!!!! *) + let newmetas = metas_in_term bo' in + let metasenv'' = + List.filter (function (n,_,_) -> List.mem n newmetas) metasenv' + in + proof := Some (uri,metasenv'',bo',gty) ; + goal := Some newmeta + + +(************************************************************) +(* Some easy tactics. *) +(************************************************************) + +(*CSC: generatore di nomi? Chiedere il nome? *) +let fresh_name = + let next_fresh_index = ref 0 +in + function () -> + incr next_fresh_index ; + "fresh_name" ^ string_of_int !next_fresh_index + +let reduction_tactic reduction_function term = + let curi,metasenv,pbo,pty = + match !proof with + None -> assert false + | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty + in + let metano,context,ty = + match !goal with + None -> assert false + | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv + in + (* We don't know if [term] is a subterm of [ty] or a subterm of *) + (* the type of one metavariable. So we replace it everywhere. *) + (*CSC: Il vero problema e' che non sapendo dove sia il term non *) + (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *) + (*CSC: e' meglio prima cercare il termine e scoprirne il *) + (*CSC: contesto, poi ridurre e infine rimpiazzare. *) + let replace context where= +(*CSC: Per il momento se la riduzione fallisce significa solamente che *) +(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *) +(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *) + try + let term' = reduction_function context term in + ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term' + ~where:where + with + _ -> where + in + let ty' = replace context ty in + let context' = + List.fold_right + (fun entry context -> + match entry with + Some (name,Cic.Def t) -> + (Some (name,Cic.Def (replace context t)))::context + | Some (name,Cic.Decl t) -> + (Some (name,Cic.Decl (replace context t)))::context + | None -> None::context + ) context [] + in + let metasenv' = + List.map + (function + (n,_,_) when n = metano -> (metano,context',ty') + | _ as t -> t + ) metasenv + in + proof := Some (curi,metasenv',pbo,pty) ; + goal := Some metano + +(* Reduces [term] using [reduction_function] in the current scratch goal [ty] *) +let reduction_tactic_in_scratch reduction_function term ty = + let metasenv = + match !proof with + None -> [] + | Some (_,metasenv,_,_) -> metasenv + in + let metano,context,_ = + match !goal with + None -> assert false + | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv + in + let term' = reduction_function context term in + ProofEngineReduction.replace + ~equality:(==) ~what:term ~with_what:term' ~where:ty + +let whd = reduction_tactic CicReduction.whd +let reduce = reduction_tactic ProofEngineReduction.reduce +let simpl = reduction_tactic ProofEngineReduction.simpl + +let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd +let reduce_in_scratch = + reduction_tactic_in_scratch ProofEngineReduction.reduce +let simpl_in_scratch = + reduction_tactic_in_scratch ProofEngineReduction.simpl + +(* It is just the opposite of whd. The code should probably be merged. *) +let fold term = + let curi,metasenv,pbo,pty = + match !proof with + None -> assert false + | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty + in + let metano,context,ty = + match !goal with + None -> assert false + | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv + in + let term' = CicReduction.whd context term in + (* We don't know if [term] is a subterm of [ty] or a subterm of *) + (* the type of one metavariable. So we replace it everywhere. *) + (*CSC: ma si potrebbe ovviare al problema. Ma non credo *) + (*CSC: che si guadagni nulla in fatto di efficienza. *) + let replace = + ProofEngineReduction.replace + ~equality: + (ProofEngineReduction.syntactic_equality ~alpha_equivalence:false) + ~what:term' ~with_what:term + in + let ty' = replace ty in + let context' = + List.map + (function + Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t)) + | Some (n,Cic.Def t) -> Some (n,Cic.Def (replace t)) + | None -> None + ) context + in + let metasenv' = + List.map + (function + (n,_,_) when n = metano -> (metano,context',ty') + | _ as t -> t + ) metasenv + in + proof := Some (curi,metasenv',pbo,pty) ; + goal := Some metano + +(************************************************************) +(* Tactics defined elsewhere *) +(************************************************************) + + (* primitive tactics *) + +let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term) +let intros () = + apply_tactic (PrimitiveTactics.intros_tac ~name:(fresh_name ())) +let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term) +let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term) +let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term) +let elim_intros_simpl term = + apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term) +let change ~goal_input:what ~input:with_what = + apply_tactic (PrimitiveTactics.change_tac ~what ~with_what) + + (* structural tactics *) + +let clearbody hyp = apply_tactic (ProofEngineStructuralRules.clearbody ~hyp) +let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp) + + (* other tactics *) + +let elim_type term = apply_tactic (Ring.elim_type_tac ~term) +let ring () = apply_tactic Ring.ring_tac +let fourier () = apply_tactic FourierR.fourier_tac +let rewrite_simpl term = apply_tactic (FourierR.rewrite_simpl_tac ~term) diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli new file mode 100644 index 000000000..f5c31067f --- /dev/null +++ b/helm/gTopLevel/proofEngine.mli @@ -0,0 +1,61 @@ +(* Copyright (C) 2002, 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/. + *) + + (* proof engine status *) +val proof : ProofEngineTypes.proof option ref +val goal : ProofEngineTypes.goal option ref + + (* start a new goal undoing part of the proof *) +val perforate : Cic.context -> Cic.term -> Cic.term -> unit + + (* reduction tactics *) +val whd : Cic.term -> unit +val reduce : Cic.term -> unit +val simpl : Cic.term -> unit +val fold : Cic.term -> unit + + (* scratch area reduction tactics *) +val whd_in_scratch : Cic.term -> Cic.term -> Cic.term +val reduce_in_scratch : Cic.term -> Cic.term -> Cic.term +val simpl_in_scratch : Cic.term -> Cic.term -> Cic.term + + (* "primitive" tactics *) +val apply : Cic.term -> unit +val intros : unit -> unit +val cut : Cic.term -> unit +val letin : Cic.term -> unit +val exact : Cic.term -> unit +val elim_intros_simpl : Cic.term -> unit +val change : goal_input:Cic.term -> input:Cic.term -> unit + + (* structural tactics *) +val clearbody : Cic.hypothesis -> unit +val clear : Cic.hypothesis -> unit + + (* other tactics *) +val elim_type : Cic.term -> unit +val ring : unit -> unit +val fourier : unit -> unit +val rewrite_simpl : Cic.term -> unit diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml new file mode 100644 index 000000000..bb724fc75 --- /dev/null +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -0,0 +1,678 @@ +(* Copyright (C) 2002, 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 *) +(* 12/04/2002 *) +(* *) +(* *) +(******************************************************************************) + + +(* The code of this module is derived from the code of CicReduction *) + +exception Impossible of int;; +exception ReferenceToDefinition;; +exception ReferenceToAxiom;; +exception ReferenceToVariable;; +exception ReferenceToCurrentProof;; +exception ReferenceToInductiveDefinition;; +exception WrongUriToInductiveDefinition;; +exception RelToHiddenHypothesis;; + +(* syntactic_equality up to cookingsno for uris *) +(* (which is often syntactically irrilevant) *) +let syntactic_equality ~alpha_equivalence = + let module C = Cic in + let rec aux t t' = + if t = t' then true + else + match t,t' with + C.Rel _, C.Rel _ + | C.Var _, C.Var _ + | C.Meta _, C.Meta _ + | C.Sort _, C.Sort _ + | C.Implicit, C.Implicit -> false (* we already know that t != t' *) + | C.Cast (te,ty), C.Cast (te',ty') -> + aux te te' && aux ty ty' + | C.Prod (n,s,t), C.Prod (n',s',t') -> + (alpha_equivalence || n = n') && aux s s' && aux t t' + | C.Lambda (n,s,t), C.Lambda (n',s',t') -> + (alpha_equivalence || n = n') && aux s s' && aux t t' + | C.LetIn (n,s,t), C.LetIn(n',s',t') -> + (alpha_equivalence || n = n') && aux s s' && aux t t' + | C.Appl l, C.Appl l' -> + (try + List.fold_left2 + (fun b t1 t2 -> b && aux t1 t2) true l l' + with + Invalid_argument _ -> false) + | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri' + | C.MutInd (uri,_,i), C.MutInd (uri',_,i') -> + UriManager.eq uri uri' && i = i' + | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') -> + UriManager.eq uri uri' && i = i' && j = j' + | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') -> + UriManager.eq sp sp' && i = i' && + aux outt outt' && aux t t' && + (try + List.fold_left2 + (fun b t1 t2 -> b && aux t1 t2) true pl pl' + with + Invalid_argument _ -> false) + | C.Fix (i,fl), C.Fix (i',fl') -> + i = i' && + (try + List.fold_left2 + (fun b (name,i,ty,bo) (name',i',ty',bo') -> + b && (alpha_equivalence || name = name') && i = i' && + aux ty ty' && aux bo bo') true fl fl' + with + Invalid_argument _ -> false) + | C.CoFix (i,fl), C.CoFix (i',fl') -> + i = i' && + (try + List.fold_left2 + (fun b (name,ty,bo) (name',ty',bo') -> + b && (alpha_equivalence || name = name') && + aux ty ty' && aux bo bo') true fl fl' + with + Invalid_argument _ -> false) + | _,_ -> false + in + aux +;; + +(* "textual" replacement of a subterm with another one *) +let replace ~equality ~what ~with_what ~where = + let module C = Cic in + let rec aux = + function + t when (equality t what) -> with_what + | C.Rel _ as t -> t + | C.Var _ as t -> t + | C.Meta _ as t -> t + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (aux te, aux ty) + | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t) + | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t) + | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t) + | C.Appl l -> + (* Invariant enforced: no application of an application *) + (match List.map aux l with + (C.Appl l')::tl -> C.Appl (l'@tl) + | l' -> C.Appl l') + | C.Const _ as t -> t + | C.MutInd _ as t -> t + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + C.MutCase (sp,cookingsno,i,aux outt, aux t, + List.map aux pl) + | C.Fix (i,fl) -> + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, aux ty, aux bo)) + fl + in + C.CoFix (i, substitutedfl) + in + aux where +;; + +(* replaces in a term a term with another one. *) +(* Lifting are performed as usual. *) +let replace_lifting ~equality ~what ~with_what ~where = + let rec substaux k what = + let module C = Cic in + let module S = CicSubstitution in + function + t when (equality t what) -> S.lift (k-1) with_what + | C.Rel n as t -> t + | C.Var _ as t -> t + | C.Meta (i, l) as t -> + let l' = + List.map + (function + None -> None + | Some t -> Some (substaux k what t) + ) l + in + C.Meta(i,l') + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty) + | C.Prod (n,s,t) -> + C.Prod (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t) + | C.Lambda (n,s,t) -> + C.Lambda (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t) + | C.LetIn (n,s,t) -> + C.LetIn (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t) + | C.Appl (he::tl) -> + (* Invariant: no Appl applied to another Appl *) + let tl' = List.map (substaux k what) tl in + begin + match substaux k what he with + C.Appl l -> C.Appl (l@tl') + | _ as he' -> C.Appl (he'::tl') + end + | C.Appl _ -> assert false + | C.Const _ as t -> t + | C.MutInd _ as t -> t + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + C.MutCase (sp,cookingsno,i,substaux k what outt, substaux k what t, + List.map (substaux k what) pl) + | C.Fix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> + (name, i, substaux k what ty, substaux (k+len) (S.lift len what) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> + (name, substaux k what ty, substaux (k+len) (S.lift len what) bo)) + fl + in + C.CoFix (i, substitutedfl) + in + substaux 1 what where +;; + +(* Takes a well-typed term and fully reduces it. *) +(*CSC: It does not perform reduction in a Case *) +let reduce context = + let rec reduceaux context l = + let module C = Cic in + let module S = CicSubstitution in + function + C.Rel n as t -> + (match List.nth context (n-1) with + Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l) + | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo) + | None -> raise RelToHiddenHypothesis + ) + | C.Var uri as t -> + (match CicEnvironment.get_cooked_obj uri 0 with + C.Definition _ -> raise ReferenceToDefinition + | C.Axiom _ -> raise ReferenceToAxiom + | C.CurrentProof _ -> raise ReferenceToCurrentProof + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l) + | C.Variable (_,Some body,_) -> reduceaux context l body + ) + | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) + | C.Sort _ as t -> t (* l should be empty *) + | C.Implicit as t -> t + | C.Cast (te,ty) -> + C.Cast (reduceaux context l te, reduceaux context l ty) + | C.Prod (name,s,t) -> + assert (l = []) ; + C.Prod (name, + reduceaux context [] s, + reduceaux ((Some (name,C.Decl s))::context) [] t) + | C.Lambda (name,s,t) -> + (match l with + [] -> + C.Lambda (name, + reduceaux context [] s, + reduceaux ((Some (name,C.Decl s))::context) [] t) + | he::tl -> reduceaux context tl (S.subst he t) + (* when name is Anonimous the substitution should be superfluous *) + ) + | C.LetIn (n,s,t) -> + reduceaux context l (S.subst (reduceaux context [] s) t) + | C.Appl (he::tl) -> + let tl' = List.map (reduceaux context []) tl in + reduceaux context (tl'@l) he + | C.Appl [] -> raise (Impossible 1) + | C.Const (uri,cookingsno) as t -> + (match CicEnvironment.get_cooked_obj uri cookingsno with + C.Definition (_,body,_,_) -> reduceaux context l body + | C.Axiom _ -> if l = [] then t else C.Appl (t::l) + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof (_,_,body,_) -> reduceaux context l body + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l) + | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l) + | C.MutCase (mutind,cookingsno,i,outtype,term,pl) -> + let decofix = + function + C.CoFix (i,fl) as t -> + let tys = + List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl + in + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + reduceaux (tys@context) [] body' + | C.Appl (C.CoFix (i,fl) :: tl) -> + let tys = + List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl + in + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + let tl' = List.map (reduceaux context []) tl in + reduceaux (tys@context) tl' body' + | t -> t + in + (match decofix (reduceaux context [] term) with + C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1)) + | C.Appl (C.MutConstruct (_,_,_,j) :: tl) -> + let (arity, r, num_ingredients) = + match CicEnvironment.get_obj mutind with + C.InductiveDefinition (tl,ingredients,r) -> + let (_,_,arity,_) = List.nth tl i + and num_ingredients = + List.fold_right + (fun (k,l) i -> + if k < cookingsno then i + List.length l else i + ) ingredients 0 + in + (arity,r,num_ingredients) + | _ -> raise WrongUriToInductiveDefinition + in + let ts = + let num_to_eat = r + num_ingredients in + let rec eat_first = + function + (0,l) -> l + | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) + | _ -> raise (Impossible 5) + in + eat_first (num_to_eat,tl) + in + reduceaux context (ts@l) (List.nth pl (j-1)) + | C.Cast _ | C.Implicit -> + raise (Impossible 2) (* we don't trust our whd ;-) *) + | _ -> + let outtype' = reduceaux context [] outtype in + let term' = reduceaux context [] term in + let pl' = List.map (reduceaux context []) pl in + let res = + C.MutCase (mutind,cookingsno,i,outtype',term',pl') + in + if l = [] then res else C.Appl (res::l) + ) + | C.Fix (i,fl) -> + let tys = + List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl + in + let t' () = + let fl' = + List.map + (function (n,recindex,ty,bo) -> + (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo) + ) fl + in + C.Fix (i, fl') + in + let (_,recindex,_,body) = List.nth fl i in + let recparam = + try + Some (List.nth l recindex) + with + _ -> None + in + (match recparam with + Some recparam -> + (match reduceaux context [] recparam with + C.MutConstruct _ + | C.Appl ((C.MutConstruct _)::_) -> + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl))) + fl + body + in + (* Possible optimization: substituting whd recparam in l*) + reduceaux context l body' + | _ -> if l = [] then t' () else C.Appl ((t' ())::l) + ) + | None -> if l = [] then t' () else C.Appl ((t' ())::l) + ) + | C.CoFix (i,fl) -> + let tys = + List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl + in + let t' = + let fl' = + List.map + (function (n,ty,bo) -> + (n,reduceaux context [] ty, reduceaux (tys@context) [] bo) + ) fl + in + C.CoFix (i, fl') + in + if l = [] then t' else C.Appl (t'::l) + in + reduceaux context [] +;; + +exception WrongShape;; +exception AlreadySimplified;; + +(*CSC: I fear it is still weaker than Coq's one. For example, Coq is *) +(*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *) +(*CSC: Fix foo *) +(*CSC: {foo [n,m:nat]:nat := *) +(*CSC: Cases m of O => n | (S p) => (foo (S O) p) end *) +(*CSC: } *) +(* Takes a well-typed term and *) +(* 1) Performs beta-iota-zeta reduction until delta reduction is needed *) +(* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *) +(* w.r.t. zero or more variables and if the Fix can be reduced, than it *) +(* is reduced, the delta-reduction is succesfull and the whole algorithm *) +(* is applied again to the new redex; Step 3) is applied to the result *) +(* of the recursive simplification. Otherwise, if the Fix can not be *) +(* reduced, than the delta-reductions fails and the delta-redex is *) +(* not reduced. Otherwise, if the delta-residual is not the *) +(* lambda-abstraction of a Fix, then it is reduced and the result is *) +(* directly returned, without performing step 3). *) +(* 3) Folds the application of the constant to the arguments that did not *) +(* change in every iteration, i.e. to the actual arguments for the *) +(* lambda-abstractions that precede the Fix. *) +(*CSC: It does not perform simplification in a Case *) +let simpl context = + (* reduceaux is equal to the reduceaux locally defined inside *) + (*reduce, but for the const case. *) + (**** Step 1 ****) + let rec reduceaux context l = + let module C = Cic in + let module S = CicSubstitution in + function + C.Rel n as t -> + (match List.nth context (n-1) with + Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l) + | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo) + | None -> raise RelToHiddenHypothesis + ) + | C.Var uri as t -> + (match CicEnvironment.get_cooked_obj uri 0 with + C.Definition _ -> raise ReferenceToDefinition + | C.Axiom _ -> raise ReferenceToAxiom + | C.CurrentProof _ -> raise ReferenceToCurrentProof + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l) + | C.Variable (_,Some body,_) -> reduceaux context l body + ) + | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) + | C.Sort _ as t -> t (* l should be empty *) + | C.Implicit as t -> t + | C.Cast (te,ty) -> + C.Cast (reduceaux context l te, reduceaux context l ty) + | C.Prod (name,s,t) -> + assert (l = []) ; + C.Prod (name, + reduceaux context [] s, + reduceaux ((Some (name,C.Decl s))::context) [] t) + | C.Lambda (name,s,t) -> + (match l with + [] -> + C.Lambda (name, + reduceaux context [] s, + reduceaux ((Some (name,C.Decl s))::context) [] t) + | he::tl -> reduceaux context tl (S.subst he t) + (* when name is Anonimous the substitution should be superfluous *) + ) + | C.LetIn (n,s,t) -> + reduceaux context l (S.subst (reduceaux context [] s) t) + | C.Appl (he::tl) -> + let tl' = List.map (reduceaux context []) tl in + reduceaux context (tl'@l) he + | C.Appl [] -> raise (Impossible 1) + | C.Const (uri,cookingsno) as t -> + (match CicEnvironment.get_cooked_obj uri cookingsno with + C.Definition (_,body,_,_) -> + begin + try + (**** Step 2 ****) + let res,constant_args = + let rec aux rev_constant_args l = + function + C.Lambda (name,s,t) as t' -> + begin + match l with + [] -> raise WrongShape + | he::tl -> + (* when name is Anonimous the substitution should be *) + (* superfluous *) + aux (he::rev_constant_args) tl (S.subst he t) + end + | C.LetIn (_,s,t) -> + aux rev_constant_args l (S.subst s t) + | C.Fix (i,fl) as t -> + let tys = + List.map (function (name,_,ty,_) -> + Some (C.Name name, C.Decl ty)) fl + in + let (_,recindex,_,body) = List.nth fl i in + let recparam = + try + List.nth l recindex + with + _ -> raise AlreadySimplified + in + (match CicReduction.whd context recparam with + C.MutConstruct _ + | C.Appl ((C.MutConstruct _)::_) -> + let body' = + let counter = ref (List.length fl) in + List.fold_right + (function _ -> + decr counter ; S.subst (C.Fix (!counter,fl)) + ) fl body + in + (* Possible optimization: substituting whd *) + (* recparam in l *) + reduceaux (tys@context) l body', + List.rev rev_constant_args + | _ -> raise AlreadySimplified + ) + | _ -> raise WrongShape + in + aux [] l body + in + (**** Step 3 ****) + let term_to_fold = + match constant_args with + [] -> C.Const (uri,cookingsno) + | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args) + in + let reduced_term_to_fold = reduce context term_to_fold in + replace (=) reduced_term_to_fold term_to_fold res + with + WrongShape -> + (* The constant does not unfold to a Fix lambda-abstracted *) + (* w.r.t. zero or more variables. We just perform reduction. *) + reduceaux context l body + | AlreadySimplified -> + (* If we performed delta-reduction, we would find a Fix *) + (* not applied to a constructor. So, we refuse to perform *) + (* delta-reduction. *) + if l = [] then + t + else + C.Appl (t::l) + end + | C.Axiom _ -> if l = [] then t else C.Appl (t::l) + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof (_,_,body,_) -> reduceaux context l body + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l) + | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l) + | C.MutCase (mutind,cookingsno,i,outtype,term,pl) -> + let decofix = + function + C.CoFix (i,fl) as t -> + let tys = + List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + reduceaux (tys@context) [] body' + | C.Appl (C.CoFix (i,fl) :: tl) -> + let tys = + List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + let tl' = List.map (reduceaux context []) tl in + reduceaux (tys@context) tl body' + | t -> t + in + (match decofix (reduceaux context [] term) with + C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1)) + | C.Appl (C.MutConstruct (_,_,_,j) :: tl) -> + let (arity, r, num_ingredients) = + match CicEnvironment.get_obj mutind with + C.InductiveDefinition (tl,ingredients,r) -> + let (_,_,arity,_) = List.nth tl i + and num_ingredients = + List.fold_right + (fun (k,l) i -> + if k < cookingsno then i + List.length l else i + ) ingredients 0 + in + (arity,r,num_ingredients) + | _ -> raise WrongUriToInductiveDefinition + in + let ts = + let num_to_eat = r + num_ingredients in + let rec eat_first = + function + (0,l) -> l + | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) + | _ -> raise (Impossible 5) + in + eat_first (num_to_eat,tl) + in + reduceaux context (ts@l) (List.nth pl (j-1)) + | C.Cast _ | C.Implicit -> + raise (Impossible 2) (* we don't trust our whd ;-) *) + | _ -> + let outtype' = reduceaux context [] outtype in + let term' = reduceaux context [] term in + let pl' = List.map (reduceaux context []) pl in + let res = + C.MutCase (mutind,cookingsno,i,outtype',term',pl') + in + if l = [] then res else C.Appl (res::l) + ) + | C.Fix (i,fl) -> + let tys = + List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl + in + let t' () = + let fl' = + List.map + (function (n,recindex,ty,bo) -> + (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo) + ) fl + in + C.Fix (i, fl') + in + let (_,recindex,_,body) = List.nth fl i in + let recparam = + try + Some (List.nth l recindex) + with + _ -> None + in + (match recparam with + Some recparam -> + (match reduceaux context [] recparam with + C.MutConstruct _ + | C.Appl ((C.MutConstruct _)::_) -> + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl))) + fl + body + in + (* Possible optimization: substituting whd recparam in l*) + reduceaux context l body' + | _ -> if l = [] then t' () else C.Appl ((t' ())::l) + ) + | None -> if l = [] then t' () else C.Appl ((t' ())::l) + ) + | C.CoFix (i,fl) -> + let tys = + List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl + in + let t' = + let fl' = + List.map + (function (n,ty,bo) -> + (n,reduceaux context [] ty, reduceaux (tys@context) [] bo) + ) fl + in + C.CoFix (i, fl') + in + if l = [] then t' else C.Appl (t'::l) + in + reduceaux context [] +;; diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli new file mode 100644 index 000000000..aa0a3a648 --- /dev/null +++ b/helm/gTopLevel/proofEngineReduction.mli @@ -0,0 +1,45 @@ +(* Copyright (C) 2002, 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 Impossible of int +exception ReferenceToDefinition +exception ReferenceToAxiom +exception ReferenceToVariable +exception ReferenceToCurrentProof +exception ReferenceToInductiveDefinition +exception WrongUriToInductiveDefinition +exception RelToHiddenHypothesis +exception WrongShape +exception AlreadySimplified + +val syntactic_equality : alpha_equivalence:bool -> Cic.term -> Cic.term -> bool +val replace : + equality:(Cic.term -> 'a -> bool) -> + what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term +val replace_lifting : + equality:(Cic.term -> Cic.term -> bool) -> + what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term +val reduce : Cic.context -> Cic.term -> Cic.term +val simpl : Cic.context -> Cic.term -> Cic.term diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml new file mode 100644 index 000000000..d53ea70ea --- /dev/null +++ b/helm/gTopLevel/topLevel/topLevel.ml @@ -0,0 +1,208 @@ +let connection_param = "host=mowgli.cs.unibo.it dbname=helm user=helm" + +let show_queries = ref false + +let use_db = ref true + +let db_down = ref true + +let nl = "

\n" + +let check_db () = + if ! db_down then + if ! use_db then begin Mqint.init connection_param; db_down := false; true end + else begin print_endline "Not issuing in restricted mode"; false end + else true + +let default_confirm q = + let module Util = MQueryUtil in + if ! show_queries then print_string (Util.text_of_query q ^ nl); + let b = check_db () in + if ! db_down then print_endline "db_down"; b + +let get_terms () = + let terms = ref [] in + let lexbuf = Lexing.from_channel stdin in + try + while true do + match CicTextualParserContext.main + (UriManager.uri_of_string "cic:/dummy") [] [] + CicTextualLexer.token lexbuf + with + | None -> () + | Some (_, expr) -> terms := expr :: ! terms + done; + ! terms + with + CicTextualParser0.Eof -> ! terms + +let pp_type_of uri = + let u = UriManager.uri_of_string uri in + let s = match (CicEnvironment.get_obj u) with + | Cic.Definition (_, _, ty, _) -> CicPp.ppterm ty + | Cic.Axiom (_, ty, _) -> CicPp.ppterm ty + | Cic.Variable (_, _, ty) -> CicPp.ppterm ty + | _ -> "Current proof or inductive definition." +(* + | Cic.CurrentProof (_,conjs,te,ty) -> + | C.InductiveDefinition _ -> +*) + in print_endline s; flush stdout + +let set_dbms i = + if i = 1 then Mqint.set_database Mqint.postgres_db else + if i = 2 then Mqint.set_database Mqint.galax_db else () + +let get_dbms s = + if s = Mqint.postgres_db then 1 else + if s = Mqint.galax_db then 2 else 0 + +let dbc () = + let on = check_db () in + if on then + begin + let dbms = Mqint.get_database () in + prerr_endline ("toplevel: current dbms is n." ^ + string_of_int (get_dbms dbms) ^ " (" ^ dbms ^ ")"); + Mqint.check () + end + +let rec display = function + | [] -> () + | term :: tail -> + display tail; + print_string ("? " ^ CicPp.ppterm term ^ nl); + flush stdout + +let levels l = + let module Gen = MQueryGenerator in + let rec levels_aux = function + | [] -> () + | term :: tail -> + levels_aux tail; + print_string ("? " ^ CicPp.ppterm term ^ nl); + print_string (Gen.string_of_levels (Gen.levels_of_term [] [] term) nl); + flush stdout + in + levels_aux l + +let execute ich = + let module Util = MQueryUtil in + let module Gen = MQueryGenerator in + Gen.set_confirm_query default_confirm; + try + let q = Util.query_of_text (Lexing.from_channel ich) in + print_endline (Util.text_of_result (Gen.execute_query q) nl); + flush stdout + with Gen.Discard -> () + +let locate name = + let module Util = MQueryUtil in + let module Gen = MQueryGenerator in + Gen.set_confirm_query default_confirm; + try + print_endline (Util.text_of_result (Gen.locate name) nl); + flush stdout + with Gen.Discard -> () + +let mbackward n m l = + let module Util = MQueryUtil in + let module Gen = MQueryGenerator in + let queries = ref [] in + let confirm query = + if List.mem query ! queries then false + else begin queries := query :: ! queries; default_confirm query end + in + let rec backward level = function + | [] -> () + | term :: tail -> + backward level tail; + try + if Mqint.get_stat () then + print_string ("? " ^ CicPp.ppterm term ^ nl); + let t0 = Sys.time () in + let r = Gen.backward [] [] term level in + let t1 = Sys.time () -. t0 in + let info = Gen.get_query_info () in + let num = List.nth info 0 in + let gen = List.nth info 1 in + if Mqint.get_stat () then + print_string (num ^ " GEN = " ^ gen ^ ":" ^ string_of_float t1 ^ "s" ^ nl); + print_string (Util.text_of_result r nl); + flush stdout + with Gen.Discard -> () + in + Gen.set_confirm_query confirm; + for level = max m n downto min m n do + prerr_endline ("toplevel: backward: trying level " ^ + string_of_int level); + backward level l + done; + prerr_endline ("toplevel: backward: " ^ + string_of_int (List.length ! queries) ^ + " queries issued") + +let prerr_help () = + prerr_endline "\nUSAGE: toplevel.opt OPTIONS < INPUTFILE\n"; + prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for"; + prerr_endline "testing purposes. Toplevel reads its input from stdin and produces ith output"; + prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n"; + prerr_endline "OPTIONS:\n"; + prerr_endline "-h -help shows this help message"; + prerr_endline "-q -show-queries outputs generated queries"; + prerr_endline "-s -stat outputs interpreter statistics"; + prerr_endline "-c -db-check checks the database connection"; + prerr_endline "-i -interpreter NUMBER sets the dbms to be used (default 1)"; + prerr_endline "-r -restricted -nodb enables restricted mode: queries are not issued"; + prerr_endline "-t -typeof URI outputs the CIC type of the given HELM object"; + prerr_endline "-x -execute issues a query given in the input file"; + prerr_endline "-d -disply outputs the CIC terms given in the input file"; + prerr_endline "-l -levels outputs the cut levels of the CIC terms given in the input file"; + prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias"; + prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all CIC terms"; + prerr_endline " in the input file"; + prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0 on all"; + prerr_endline " CIC terms in the input file\n"; + prerr_endline "NOTES: interpreter numbers are 1 for postgres and 2 for galax"; + prerr_endline " CIC terms are read with the HELM CIC Textual Parser"; + prerr_endline " -typeof does not work with inductive types and proofs in progress\n" + +let parse_args () = + let rec parse = function + | [] -> () + | ("-h"|"-help") :: rem -> prerr_help () + | ("-d"|"-display") :: rem -> display (get_terms ()) + | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem + | ("-l"|"-levels") :: rem -> levels (get_terms ()) + | ("-x"|"-execute") :: rem -> execute stdin; parse rem + | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem + | ("-s"|"-stat") :: rem -> Mqint.set_stat true; parse rem + | ("-r"|"-restricted"|"-nodb") :: rem -> use_db := false; parse rem + | ("-i"|"-interpreter") :: dbms :: rem -> set_dbms (int_of_string dbms); parse rem + | ("-c"|"-db-check") :: rem -> dbc (); parse rem + | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem + | ("-B"|"-backward") :: arg :: rem -> + let m = (int_of_string arg) in + mbackward m m (get_terms ()) + | ("-MB"|"-multi-backward") :: arg :: rem -> + let m = (int_of_string arg) in + mbackward m 0 (get_terms ()) + | _ :: rem -> parse rem + in + parse (List.tl (Array.to_list Sys.argv)) + +let _ = + let module Gen = MQueryGenerator in + CicCooking.init () ; + Logger.log_callback := + (Logger.log_to_html + ~print_and_flush:(function s -> print_string s ; flush stdout)) ; + Mqint.set_stat false; + Gen.set_log_file "MQGenLog.htm"; + set_dbms 1; + parse_args (); + if not ! db_down then Mqint.close (); + Gen.set_confirm_query (fun _ -> true); + prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^ + " seconds"); + exit 0 diff --git a/helm/ocaml/.cvsignore b/helm/ocaml/.cvsignore new file mode 100644 index 000000000..18745fc01 --- /dev/null +++ b/helm/ocaml/.cvsignore @@ -0,0 +1,19 @@ +META.helm-cic +META.helm-getter +META.helm-cic_annotations +META.helm-pxp +META.helm-cic_annotations_cache +META.helm-urimanager +META.helm-cic_cache +META.helm-xml +META.helm-cic_proof_checking +META.helm-cic_textual_parser +META.helm-cic_unification +META.helm-mathql_interpreter +META.helm-mathql +Makefile +Makefile.common +configure +config.log +config.cache +config.status diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli new file mode 100644 index 000000000..22fd5d657 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -0,0 +1,69 @@ +(* 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 *) +(* 24/01/2000 *) +(* *) +(* This module implements a trival cache system (an hash-table) for cic *) +(* objects. Uses the getter (getter.ml) and the parser (cicParser.ml) *) +(* *) +(******************************************************************************) + +exception CircularDependency of string;; + +(* get_obj uri *) +(* returns the cic object whose uri is uri. If the term is not just in cache, *) +(* then it is parsed via CicParser.term_of_xml from the file whose name is *) +(* the result of Getter.get uri *) +val get_obj : UriManager.uri -> Cic.obj + +type type_checked_obj = + CheckedObj of Cic.obj (* cooked obj *) + | UncheckedObj of Cic.obj (* uncooked obj *) + +(* is_type_checked uri cookingsno *) +(*CSC commento falso ed obsoleto *) +(* returns (true,object) if the object has been type-checked *) +(* otherwise it returns (false,object) and freeze the object for *) +(* type-checking *) +(* set_type_checking_info must be called to unfreeze the object *) +val is_type_checked : UriManager.uri -> int -> type_checked_obj + +(* set_type_checking_info uri *) +(* must be called once the type-checking of uri is finished *) +(* The object whose uri is uri is unfreezed and won't be type-checked *) +(* again in the future (is_type_checked will return true) *) +val set_type_checking_info : UriManager.uri -> unit + +(* get_cooked_obj uri cookingsno *) +val get_cooked_obj : UriManager.uri -> int -> Cic.obj + +(* set_cooking_function cooking_function *) +val set_cooking_function : + (Cic.obj -> UriManager.uri -> (int * Cic.obj) list) -> unit diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml new file mode 100644 index 000000000..fce4e7f48 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -0,0 +1,260 @@ +(* 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 *) +(* 24/01/2000 *) +(* *) +(* This module implements a very simple Coq-like pretty printer that, given *) +(* an object of cic (internal representation) returns a string describing the *) +(* object in a syntax similar to that of coq *) +(* *) +(******************************************************************************) + +exception CicPpInternalError;; +exception NotEnoughElements;; + +(* Utility functions *) + +let string_of_name = + function + Cic.Name s -> s + | Cic.Anonimous -> "_" +;; + +(* 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 +;; + +(* pp t l *) +(* pretty-prints a term t of cic in an environment l where l is a list of *) +(* identifier names used to resolve DeBrujin indexes. The head of l is the *) +(* name associated to the greatest DeBrujin index in t *) +let rec pp t l = + let module C = Cic in + match t with + C.Rel n -> + begin + try + (match get_nth l n with + Some (C.Name s) -> s + | _ -> raise CicPpInternalError + ) + with + NotEnoughElements -> string_of_int (List.length l - n) + end + | C.Var uri -> UriManager.name_of_uri uri + | C.Meta (n,l1) -> + "?" ^ (string_of_int n) ^ "[" ^ + String.concat " ; " + (List.map (function None -> "_" | Some t -> pp t l) l1) ^ + "]" + | C.Sort s -> + (match s with + C.Prop -> "Prop" + | C.Set -> "Set" + | C.Type -> "Type" + ) + | C.Implicit -> "?" + | C.Prod (b,s,t) -> + (match b with + C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l) + | C.Anonimous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")" + ) + | C.Cast (v,t) -> pp v l + | C.Lambda (b,s,t) -> + "[" ^ string_of_name b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l) + | C.LetIn (b,s,t) -> + "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l) + | C.Appl li -> + "(" ^ + (List.fold_right + (fun x i -> pp x l ^ (match i with "" -> "" | _ -> " ") ^ i) + li "" + ) ^ ")" + | C.Const (uri,_) -> UriManager.name_of_uri uri + | C.MutInd (uri,_,n) -> + begin + try + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (dl,_,_) -> + let (name,_,_,_) = get_nth dl (n+1) in + name + | _ -> raise CicPpInternalError + ) + with + NotEnoughElements -> + UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1) + end + | C.MutConstruct (uri,_,n1,n2) -> + begin + try + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (dl,_,_) -> + let (_,_,_,cons) = get_nth dl (n1+1) in + let (id,_,_) = get_nth cons n2 in + id + | _ -> raise CicPpInternalError + ) + with + NotEnoughElements -> + UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^ + string_of_int n2 + end + | C.MutCase (uri,_,n1,ty,te,patterns) -> + let connames = + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (dl,_,_) -> + let (_,_,_,cons) = get_nth dl (n1+1) in + List.map (fun (id,_,_) -> id) cons + | _ -> raise CicPpInternalError + ) + in + "\n<" ^ pp ty l ^ ">Cases " ^ pp te l ^ " of " ^ + List.fold_right (fun (x,y) i -> "\n " ^ x ^ " => " ^ pp y l ^ i) + (List.combine connames patterns) "" ^ + "\nend" + | C.Fix (no, funs) -> + let snames = List.map (fun (name,_,_,_) -> name) funs in + let names = + List.rev (List.map (function name -> Some (C.Name name)) snames) + in + "\nFix " ^ get_nth snames (no + 1) ^ " {" ^ + List.fold_right + (fun (name,ind,ty,bo) i -> "\n" ^ name ^ " / " ^ string_of_int ind ^ + " : " ^ pp ty l ^ " := \n" ^ + pp bo (names@l) ^ i) + funs "" ^ + "}\n" + | C.CoFix (no,funs) -> + let snames = List.map (fun (name,_,_) -> name) funs in + let names = + List.rev (List.map (function name -> Some (C.Name name)) snames) + in + "\nCoFix " ^ get_nth snames (no + 1) ^ " {" ^ + List.fold_right + (fun (name,ty,bo) i -> "\n" ^ name ^ + " : " ^ pp ty l ^ " := \n" ^ + pp bo (names@l) ^ i) + funs "" ^ + "}\n" +;; + +let ppterm t = + pp t [] +;; + +(* ppinductiveType (typename, inductive, arity, cons) names *) +(* pretty-prints a single inductive definition (typename, inductive, arity, *) +(* cons) where the cic terms in the inductive definition need to be *) +(* evaluated in the environment names that is the list of typenames of the *) +(* mutual inductive definitions defined in the block of mutual inductive *) +(* definitions to which this one belongs to *) +let ppinductiveType (typename, inductive, arity, cons) names = + (if inductive then "\nInductive " else "\nCoInductive ") ^ typename ^ ": " ^ + (*CSC: bug found: was pp arity names ^ " =\n " ^*) + pp arity [] ^ " =\n " ^ + List.fold_right + (fun (id,ty,_) i -> id ^ " : " ^ pp ty names ^ + (if i = "" then "\n" else "\n | ") ^ i) + cons "" +;; + +(* ppobj obj returns a string with describing the cic object obj in a syntax *) +(* similar to the one used by Coq *) +let ppobj obj = + let module C = Cic in + let module U = UriManager in + match obj with + C.Definition (id, t1, t2, params) -> + "Definition of " ^ id ^ + "(" ^ + List.fold_right + (fun (_,x) i -> + List.fold_right + (fun x i -> + U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i' + ) x "" ^ match i with "" -> "" | i' -> " " ^ i' + ) params "" ^ ")" ^ + ":\n" ^ pp t1 [] ^ " : " ^ pp t2 [] + | C.Axiom (id, ty, params) -> + "Axiom " ^ id ^ "(" ^ + List.fold_right + (fun (_,x) i -> + List.fold_right + (fun x i -> + U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i' + ) x "" ^ match i with "" -> "" | i' -> " " ^ i' + ) params "" ^ + "):\n" ^ pp ty [] + | C.Variable (name, bo, ty) -> + "Variable " ^ name ^ ":\n" ^ pp ty [] ^ "\n" ^ + (match bo with None -> "" | Some bo -> ":= " ^ pp bo []) + | C.CurrentProof (name, conjectures, value, ty) -> + "Current Proof:\n" ^ + let separate s = if s = "" then "" else s ^ " ; " in + List.fold_right + (fun (n, context, t) i -> + let conjectures',name_context = + List.fold_right + (fun context_entry (i,name_context) -> + (match context_entry with + Some (n,C.Decl at) -> + (separate i) ^ + string_of_name n ^ ":" ^ pp at name_context ^ " ", + (Some n)::name_context + | Some (n,C.Def at) -> + (separate i) ^ + string_of_name n ^ ":= " ^ pp at name_context ^ " ", + (Some n)::name_context + | None -> + (separate i) ^ "_ :? _ ", None::name_context) + ) context ("",[]) + in + conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^ + pp t name_context ^ "\n" ^ i + ) conjectures "" ^ + "\n" ^ pp value [] ^ " : " ^ pp ty [] + | C.InductiveDefinition (l, params, nparams) -> + "Parameters = " ^ + List.fold_right + (fun (_,x) i -> + List.fold_right + (fun x i -> + U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i' + ) x "" ^ match i with "" -> "" | i' -> " " ^ i' + ) params "" ^ "\n" ^ + "NParams = " ^ string_of_int nparams ^ "\n" ^ + let names = List.rev (List.map (fun (n,_,_,_) -> Some (C.Name n)) l) in + List.fold_right (fun x i -> ppinductiveType x names ^ i) l "" +;; diff --git a/helm/ocaml/mathql/.depend b/helm/ocaml/mathql/.depend new file mode 100644 index 000000000..769e30c89 --- /dev/null +++ b/helm/ocaml/mathql/.depend @@ -0,0 +1,8 @@ +mQueryTParser.cmi: mathQL.cmo +mQueryUtil.cmi: mathQL.cmo +mQueryTParser.cmo: mathQL.cmo mQueryTParser.cmi +mQueryTParser.cmx: mathQL.cmx mQueryTParser.cmi +mQueryTLexer.cmo: mQueryTParser.cmi +mQueryTLexer.cmx: mQueryTParser.cmx +mQueryUtil.cmo: mQueryTLexer.cmo mQueryTParser.cmi mathQL.cmo mQueryUtil.cmi +mQueryUtil.cmx: mQueryTLexer.cmx mQueryTParser.cmx mathQL.cmx mQueryUtil.cmi diff --git a/helm/ocaml/mathql/Makefile b/helm/ocaml/mathql/Makefile new file mode 100644 index 000000000..c381b8dc8 --- /dev/null +++ b/helm/ocaml/mathql/Makefile @@ -0,0 +1,16 @@ +PACKAGE = mathql +REQUIRES = helm-urimanager +PREDICATES = + +INTERFACE_FILES = mQueryTParser.mli mQueryUtil.mli + +IMPLEMENTATION_FILES = mathQL.ml mQueryTParser.ml mQueryTLexer.ml \ + mQueryUtil.ml + +EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi mQueryTLexer.cmi \ + mQueryTLexer.mll mQueryTParser.mly + +EXTRA_OBJECTS_TO_CLEAN = mQueryTParser.ml mQueryTParser.mli \ + mQueryTLexer.ml + +include ../Makefile.common diff --git a/helm/ocaml/mathql/mQueryTLexer.mll b/helm/ocaml/mathql/mQueryTLexer.mll new file mode 100644 index 000000000..a0884e79d --- /dev/null +++ b/helm/ocaml/mathql/mQueryTLexer.mll @@ -0,0 +1,104 @@ +(* 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 *) +(* *) +(* Ferruccio Guidi *) +(* 23/05/2002 *) +(* *) +(* *) +(******************************************************************************) + +{ + open MQueryTParser +} + +let SPC = [' ' '\t' '\n']+ +let ALPHA = ['A'-'Z' 'a'-'z'] +let NUM = ['0'-'9'] +let IDEN = ALPHA (NUM | ALPHA)* +let QSTR = [^ '"' '\\']+ + +rule comm_token = parse + | "*)" { query_token lexbuf } + | [^ '*']* { comm_token lexbuf } +and string_token = parse + | '"' { DQ } + | '\\' _ { STR (String.sub (Lexing.lexeme lexbuf) 1 1) } + | QSTR { STR (Lexing.lexeme lexbuf) } + | eof { EOF } +and query_token = parse + | "(*" { comm_token lexbuf } + | SPC { query_token lexbuf } + | '"' { STR (qstr string_token lexbuf) } + | '(' { LP } + | ')' { RP } + | '{' { LC } + | '}' { RC } + | '@' { AT } + | '%' { PC } + | '$' { DL } + | '.' { FS } + | ',' { CM } + | '/' { SL } + | "and" { AND } + | "attr" { ATTR } + | "attribute" { ATTRIB } + | "be" { BE } + | "diff" { DIFF } + | "eq" { EQ } + | "ex" { EX } + | "false" { FALSE } + | "fun" { FUN } + | "in" { IN } + | "intersect" { INTER } + | "let" { LET } + | "meet" { MEET } + | "not" { NOT } + | "or" { OR } + | "pattern" { PAT } + | "ref" { REF } + | "refof" { REFOF } + | "relation" { REL } + | "select" { SELECT } + | "sub" { SUB } + | "super" { SUPER } + | "true" { TRUE } + | "union" { UNION } + | "where" { WHERE } + | IDEN { ID (Lexing.lexeme lexbuf) } + | eof { EOF } +and result_token = parse + | SPC { result_token lexbuf } + | '"' { STR (qstr string_token lexbuf) } + | '{' { LC } + | '}' { RC } + | ',' { CM } + | ';' { SC } + | '=' { IS } + | "attr" { ATTR } + | eof { EOF } diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly new file mode 100644 index 000000000..f32a41187 --- /dev/null +++ b/helm/ocaml/mathql/mQueryTParser.mly @@ -0,0 +1,189 @@ +/* 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 */ +/* */ +/* Ferruccio Guidi */ +/* 23/05/2002 */ +/* */ +/* */ +/******************************************************************************/ + +%{ + let analyze x = + let module M = MathQL in + let rec join l1 l2 = match l1, l2 with + | [], _ -> l2 + | _, [] -> l1 + | s1 :: tl1, s2 :: _ when s1 < s2 -> s1 :: join tl1 l2 + | s1 :: _, s2 :: tl2 when s2 < s1 -> s2 :: join l1 tl2 + | s1 :: tl1, s2 :: tl2 -> s1 :: join tl1 tl2 + in + let rec an_val = function + | M.Const _ -> [] + | M.VVar _ -> [] + | M.Record (rv, _) -> [rv] + | M.Fun (_, x) -> an_val x + | M.Attribute (_, _, x) -> an_val x + | M.RefOf x -> an_set x + and an_boole = function + | M.False -> [] + | M.True -> [] + | M.Ex _ _ -> [] + | M.Not x -> an_boole x + | M.And (x, y) -> join (an_boole x) (an_boole y) + | M.Or (x, y) -> join (an_boole x) (an_boole y) + | M.Sub (x, y) -> join (an_val x) (an_val y) + | M.Meet (x, y) -> join (an_val x) (an_val y) + | M.Eq (x, y) -> join (an_val x) (an_val y) + and an_set = function + | M.SVar _ -> [] + | M.RVar _ -> [] + | M.Relation (_, _, x, _) -> an_set x + | M.Pattern x -> an_val x + | M.Ref x -> an_val x + | M.Union (x, y) -> join (an_set x) (an_set y) + | M.Intersect (x, y) -> join (an_set x) (an_set y) + | M.Diff (x, y) -> join (an_set x) (an_set y) + | M.LetSVar (_, x, y) -> join (an_set x) (an_set y) + | M.LetVVar (_, x, y) -> join (an_val x) (an_set y) + | M.Select (_, x, y) -> join (an_set x) (an_boole y) + in + an_boole x +%} + %token ID STR + %token SL IS LC RC CM SC LP RP AT PC DL FS DQ EOF + %token AND ATTR ATTRIB BE DIFF EQ EX FALSE FUN IN INTER LET MEET NOT OR + %token PAT REF REFOF REL SELECT SUB SUPER TRUE UNION WHERE + %left DIFF WHERE REFOF + %left OR UNION + %left AND INTER + %nonassoc REL + %nonassoc NOT EX IN ATTR + + %start qstr query result + %type qstr + %type query + %type result +%% + qstr: + | DQ { "" } + | STR qstr { $1 ^ $2 } + ; + svar: + | PC ID { $2 } + ; + rvar: + | AT ID { $2 } + ; + vvar: + | DL ID { $2 } + ; + qstr_list: + | STR CM qstr_list { $1 :: $3 } + | STR { [$1] } + ; + vvar_list: + | vvar CM vvar_list { $1 :: $3 } + | vvar { [$1] } + ; + qstr_path: + | STR SL qstr_path { $1 :: $3 } + | STR { [$1] } + ; + ref_op: + | SUB { MathQL.SubOp } + | SUPER { MathQL.SuperOp } + | { MathQL.ExactOp } + ; + val_exp: + | STR { MathQL.Const [$1] } + | FUN STR val_exp { MathQL.Fun ($2, $3) } + | ATTRIB ref_op qstr_path val_exp { MathQL.Attribute ($2, $3, $4) } + | rvar FS vvar { MathQL.Record ($1, $3) } + | vvar { MathQL.VVar $1 } + | LC qstr_list RC { MathQL.Const $2 } + | LC RC { MathQL.Const [] } + | REFOF set_exp { MathQL.RefOf $2 } + | LP val_exp RP { $2 } + ; + boole_exp: + | TRUE { MathQL.True } + | FALSE { MathQL.False } + | LP boole_exp RP { $2 } + | NOT boole_exp { MathQL.Not $2 } + | EX boole_exp { MathQL.Ex (analyze $2) $2 } + | val_exp SUB val_exp { MathQL.Sub ($1, $3) } + | val_exp MEET val_exp { MathQL.Meet ($1, $3) } + | val_exp EQ val_exp { MathQL.Eq ($1, $3) } + | boole_exp AND boole_exp { MathQL.And ($1, $3) } + | boole_exp OR boole_exp { MathQL.Or ($1, $3) } + ; + set_exp: + | REF val_exp { MathQL.Ref $2 } + | PAT val_exp { MathQL.Pattern $2 } + | LP set_exp RP { $2 } + | SELECT rvar IN set_exp WHERE boole_exp { MathQL.Select ($2, $4, $6) } + | REL ref_op qstr_path set_exp ATTR vvar_list { MathQL.Relation ($2, $3, $4, $6) } + | REL ref_op qstr_path set_exp { MathQL.Relation ($2, $3, $4, []) } + | svar { MathQL.SVar $1 } + | rvar { MathQL.RVar $1 } + | set_exp UNION set_exp { MathQL.Union ($1, $3) } + | set_exp INTER set_exp { MathQL.Intersect ($1, $3) } + | set_exp DIFF set_exp { MathQL.Diff ($1, $3) } + | LET svar BE set_exp IN set_exp { MathQL.LetSVar ($2, $4, $6) } + | LET vvar BE val_exp IN set_exp { MathQL.LetVVar ($2, $4, $6) } + ; + query: + | set_exp EOF { $1 } + ; + attribute: + | STR IS qstr_list { ($1, $3) } + | STR { ($1, []) } + ; + attr_list: + | attribute SC attr_list { $1 :: $3 } + | attribute { [$1] } + ; + group: + LC attr_list RC { $2 } + ; + group_list: + | group CM group_list { $1 :: $3 } + | group { [$1] } + ; + resource: + | STR ATTR group_list { ($1, $3) } + | STR { ($1, []) } + ; + resource_list: + | resource SC resource_list { $1 :: $3 } + | resource { [$1] } + | { [] } + ; + result: + | resource_list EOF { $1 } diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml new file mode 100644 index 000000000..ea1829719 --- /dev/null +++ b/helm/ocaml/mathql/mQueryUtil.ml @@ -0,0 +1,124 @@ +(* 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 *) +(* *) +(* Ferruccio Guidi *) +(* 30/04/2002 *) +(* *) +(* *) +(******************************************************************************) + + +(* text linearization and parsing *******************************************) + +let rec txt_list f s = function + | [] -> "" + | [a] -> f a + | a :: tail -> f a ^ s ^ txt_list f s tail + +let txt_qstr s = "\"" ^ s ^ "\"" + +let text_of_query x = + let module M = MathQL in + let txt_svar sv = "%" ^ sv in + let txt_rvar rv = "@" ^ rv in + let txt_vvar vv = "$" ^ vv in + let txt_ref = function + | M.ExactOp -> "" + | M.SubOp -> "sub " + | M.SuperOp -> "super " + in + let txt_vvar_list l = + l + in + let rec txt_val = function + | M.Const [s] -> txt_qstr s + | M.Const l -> "{" ^ txt_list txt_qstr ", " l ^ "}" + | M.VVar vv -> txt_vvar vv + | M.Record (rv, vv) -> txt_rvar rv ^ "." ^ txt_vvar vv + | M.Fun (s, x) -> "fun " ^ txt_qstr s ^ " " ^ txt_val x + | M.Attribute (r, p, x) -> "attribute " ^ txt_ref r ^ txt_list txt_qstr "/" p ^ " " ^ txt_val x + | M.RefOf x -> "refof " ^ txt_set x + and txt_boole = function + | M.False -> "false" + | M.True -> "true" + | M.Ex b x -> "ex " ^ txt_boole x +(* | M.Ex b x -> "ex [" ^ txt_list txt_rvar "," b ^ "] " ^ txt_boole x *) + | M.Not x -> "not " ^ txt_boole x + | M.And (x, y) -> "(" ^ txt_boole x ^ " and " ^ txt_boole y ^ ")" + | M.Or (x, y) -> "(" ^ txt_boole x ^ " or " ^ txt_boole y ^ ")" + | M.Sub (x, y) -> "(" ^ txt_val x ^ " sub " ^ txt_val y ^ ")" + | M.Meet (x, y) -> "(" ^ txt_val x ^ " meet " ^ txt_val y ^ ")" + | M.Eq (x, y) -> "(" ^ txt_val x ^ " eq " ^ txt_val y ^ ")" + and txt_set = function + | M.SVar sv -> txt_svar sv + | M.RVar rv -> txt_rvar rv + | M.Relation (r, p, x, []) -> "relation " ^ txt_ref r ^ txt_list txt_qstr "/" p ^ " " ^ txt_set x + | M.Relation (r, p, x, l) -> "relation " ^ txt_ref r ^ txt_list txt_qstr "/" p ^ " " ^ txt_set x ^ " attr " ^ txt_list txt_vvar ", " l + | M.Union (x, y) -> "(" ^ txt_set x ^ " union " ^ txt_set y ^ ")" + | M.Intersect (x, y) -> "(" ^ txt_set x ^ " intersect " ^ txt_set y ^ ")" + | M.Diff (x, y) -> "(" ^ txt_set x ^ " diff " ^ txt_set y ^ ")" + | M.LetSVar (sv, x, y) -> "let " ^ txt_svar sv ^ " be " ^ txt_set x ^ " in " ^ txt_set y + | M.LetVVar (vv, x, y) -> "let " ^ txt_vvar vv ^ " be " ^ txt_val x ^ " in " ^ txt_set y + | M.Select (rv, x, y) -> "select " ^ txt_rvar rv ^ " in " ^ txt_set x ^ " where " ^ txt_boole y + | M.Pattern x -> "pattern " ^ txt_val x + | M.Ref x -> "ref " ^ txt_val x + in + txt_set x + +let text_of_result x sep = + let txt_attr = function + | (s, []) -> txt_qstr s + | (s, l) -> txt_qstr s ^ "=" ^ txt_list txt_qstr ", " l + in + let txt_group l = "{" ^ txt_list txt_attr "; " l ^ "}" in + let txt_res = function + | (s, []) -> txt_qstr s + | (s, l) -> txt_qstr s ^ " attr " ^ txt_list txt_group ", " l + in + let txt_set l = txt_list txt_res ("; " ^ sep) l ^ sep in + txt_set x + +let query_of_text lexbuf = + MQueryTParser.query MQueryTLexer.query_token lexbuf + +let result_of_text lexbuf = + MQueryTParser.result MQueryTLexer.result_token lexbuf + +(* conversion functions *****************************************************) + +type uriref = UriManager.uri * (int list) + +let string_of_uriref (uri, fi) = + let module UM = UriManager in + let str = UM.string_of_uri uri in + let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in + match fi with + | [] -> str + | [t] -> str ^ xp t ^ ")" + | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" diff --git a/helm/ocaml/mathql/mQueryUtil.mli b/helm/ocaml/mathql/mQueryUtil.mli new file mode 100644 index 000000000..9881b3b54 --- /dev/null +++ b/helm/ocaml/mathql/mQueryUtil.mli @@ -0,0 +1,49 @@ +(* 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 *) +(* *) +(* Ferruccio Guidi *) +(* 30/04/2002 *) +(* *) +(* *) +(******************************************************************************) + + +val text_of_query : MathQL.query -> string + +val text_of_result : MathQL.result -> string -> string + +val query_of_text : Lexing.lexbuf -> MathQL.query + +val result_of_text : Lexing.lexbuf -> MathQL.result + + +type uriref = UriManager.uri * (int list) + +val string_of_uriref : uriref -> string + diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml new file mode 100644 index 000000000..d375d92af --- /dev/null +++ b/helm/ocaml/mathql/mathQL.ml @@ -0,0 +1,100 @@ +(* 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://www.cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Ferruccio Guidi *) +(* Irene Schena *) +(* 10/09/2002 *) +(* *) +(* *) +(******************************************************************************) + + +(* input data structures ****************************************************) + +type svar = string (* the name of a variable for a resource set *) + +type rvar = string (* the name of a variable for a resource *) + +type vvar = string (* the name of a variable for an attribute value *) + +type refine_op = ExactOp + | SubOp + | SuperOp + +type path = string list + +type vvar_list = vvar list + +type set_exp = SVar of svar + | RVar of rvar + | Ref of val_exp + | Pattern of val_exp + | Relation of refine_op * path * set_exp * vvar_list + | Select of rvar * set_exp * boole_exp + | Union of set_exp * set_exp + | Intersect of set_exp * set_exp + | Diff of set_exp * set_exp + | LetSVar of svar * set_exp * set_exp + | LetVVar of vvar * val_exp * set_exp + +and boole_exp = False + | True + | Not of boole_exp + | Ex of rvar list * boole_exp + | And of boole_exp * boole_exp + | Or of boole_exp * boole_exp + | Sub of val_exp * val_exp + | Meet of val_exp * val_exp + | Eq of val_exp * val_exp + +and val_exp = Const of string list + | RefOf of set_exp + | Record of rvar * vvar + | VVar of vvar + | Fun of string * val_exp + | Attribute of refine_op * path * val_exp + +type query = set_exp + + +(* output data structures ***************************************************) + +type value = string list (* the value of an attribute *) + +type attribute = string * value (* an attribute *) + +type attribute_group = attribute list (* a group of attributes *) + +type attribute_set = attribute_group list (* the attributes of an URI *) + +type resource = string * attribute_set (* an attributed URI *) + +type resource_set = resource list (* the query result *) + +type result = resource_set diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend new file mode 100644 index 000000000..72a3dd440 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/.depend @@ -0,0 +1,22 @@ +dbconn.cmo: dbconn.cmi +dbconn.cmx: dbconn.cmi +utility.cmo: dbconn.cmi utility.cmi +utility.cmx: dbconn.cmx utility.cmi +union.cmo: union.cmi +union.cmx: union.cmi +relation.cmo: dbconn.cmi union.cmi utility.cmi relation.cmi +relation.cmx: dbconn.cmx union.cmx utility.cmx relation.cmi +diff.cmo: diff.cmi +diff.cmx: diff.cmi +meet.cmo: meet.cmi +meet.cmx: meet.cmi +sub.cmo: sub.cmi +sub.cmx: sub.cmi +intersect.cmo: intersect.cmi +intersect.cmx: intersect.cmi +func.cmo: dbconn.cmi intersect.cmi utility.cmi func.cmi +func.cmx: dbconn.cmx intersect.cmx utility.cmx func.cmi +mqint.cmo: context.cmo dbconn.cmi diff.cmi intersect.cmi meet.cmi \ + relation.cmi sub.cmi union.cmi mqint.cmi +mqint.cmx: context.cmx dbconn.cmx diff.cmx intersect.cmx meet.cmx \ + relation.cmx sub.cmx union.cmx mqint.cmi diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile new file mode 100644 index 000000000..5328d04d2 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/Makefile @@ -0,0 +1,15 @@ +PACKAGE = mathql_interpreter +REQUIRES = helm-urimanager postgres unix natile-galax helm-mathql +PREDICATES = + +INTERFACE_FILES = dbconn.mli utility.mli union.mli relation.mli diff.mli meet.mli sub.mli intersect.mli func.mli mqint.mli + +IMPLEMENTATION_FILES = dbconn.ml utility.ml union.ml relation.ml diff.ml meet.ml sub.ml intersect.ml context.ml func.ml mqint.ml + +# $(INTERFACE_FILES:%.mli=%.ml) + +EXTRA_OBJECTS_TO_INSTALL = context.ml + +EXTRA_OBJECTS_TO_CLEAN = + +include ../Makefile.common diff --git a/helm/ocaml/mathql_interpreter/context.ml b/helm/ocaml/mathql_interpreter/context.ml new file mode 100644 index 000000000..c9431d1af --- /dev/null +++ b/helm/ocaml/mathql_interpreter/context.ml @@ -0,0 +1,30 @@ +(* contexts *****************************************************************) + +type svar_context = (MathQL.svar * MathQL.resource_set) list + +type rvar_context = (MathQL.rvar * MathQL.resource) list + +type group_context = (MathQL.rvar * MathQL.attribute_group) list + +type vvar_context = (MathQL.vvar * MathQL.value) list + + +type context = {svars: svar_context; (* contesto delle svar *) + rvars: rvar_context; (* contesto delle rvar *) + groups: group_context; (* contesto dei gruppi *) + vvars: vvar_context (* contesto delle vvar introdotte con let-in *) + } + +let upd_svars c s = + {svars = s; rvars = c.rvars; groups = c.groups; vvars = c.vvars} + +let upd_rvars c s = + {svars = c.svars; rvars = s; groups = c.groups; vvars = c.vvars} + +let upd_groups c s = + {svars = c.svars; rvars = c.rvars; groups = s; vvars = c.vvars} + +let upd_vvars c s = + {svars = c.svars; rvars = c.rvars; groups = c.groups; vvars = s} + + diff --git a/helm/ocaml/mathql_interpreter/dbconn.ml b/helm/ocaml/mathql_interpreter/dbconn.ml new file mode 100644 index 000000000..b38eabe87 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/dbconn.ml @@ -0,0 +1,74 @@ +(* 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://www.cs.unibo.it/helm/. + *) + +(* + * gestione della connessione al database + *) + +(* + * le eccezioni lanciate dalle funzioni init e pgc sono + * definite nel modulo Mathql + *) +open MathQL;; + +exception InvalidURI of string +exception ConnectionFailed of string +exception InvalidConnection + +(* + * connessione al db + *) +let conn = ref None + +(* + * controllo sulla connessione + *) +let pgc () = + match !conn with + None -> raise InvalidConnection + | Some c -> c +;; + +(* + * inizializzazione della connessione + * + * TODO + * passare i parametri della connessione come argomento di init + *) +let init connection_param = + try ( + conn := Some (new Postgres.connection connection_param); + ) with + _ -> raise (ConnectionFailed ("init: " ^ connection_param)) +;; + +(* + * chiusura della connessione + *) +let close () = + match !conn with + None -> () + | Some c -> c#close +;; diff --git a/helm/ocaml/mathql_interpreter/dbconn.mli b/helm/ocaml/mathql_interpreter/dbconn.mli new file mode 100644 index 000000000..ecfbcd66a --- /dev/null +++ b/helm/ocaml/mathql_interpreter/dbconn.mli @@ -0,0 +1,28 @@ +(* 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/. + *) + +val pgc : unit -> Postgres.connection +val init : string -> unit +val close : unit -> unit diff --git a/helm/ocaml/mathql_interpreter/diff.ml b/helm/ocaml/mathql_interpreter/diff.ml new file mode 100644 index 000000000..b4e09196e --- /dev/null +++ b/helm/ocaml/mathql_interpreter/diff.ml @@ -0,0 +1,98 @@ +(* 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/. + *) + +(* + * vecchia implementazione del comando DIFF + + +exception NotCompatible;; + +(* intersect_attributes is successful iff there is no attribute with *) +(* two different values in the two lists. The returned list is the *) +(* union of the two lists. *) +let rec intersect_attributes (attr1, attr2) = + match attr1, attr2 with + [],_ -> attr2 + | _,[] -> attr1 + | (key1,value1)::tl1, (key2,_)::_ when key1 < key2 -> + (key1,value1)::(intersect_attributes (tl1,attr2)) + | (key1,_)::_, (key2,value2)::tl2 when key2 < key1 -> + (key2,value2)::(intersect_attributes (attr1,tl2)) + | entry1::tl1, entry2::tl2 when entry1 = entry2 -> + entry1::(intersect_attributes (tl1,tl2)) + | _, _ -> raise NotCompatible (* same keys, different values *) +;; + + +let rec diff_ex l1 l2 = + let module S = Mathql_semantics in + match (l1, l2) with + [],_ -> [] + | l,[] -> l + | {S.uri = uri1}::_, {S.uri = uri2}::tl2 when uri2 < uri1 -> + (diff_ex l1 tl2) + | {S.uri = uri1 ; S.attributes = attributes1}::tl1, + {S.uri = uri2}::_ when uri1 < uri2 -> + {S.uri = uri1 ; S.attributes = attributes1 ; S.extra = ""}::(diff_ex tl1 l2) + | {S.uri = uri1 ; S.attributes = attributes1}::tl1, + {S.uri = uri2 ; S.attributes = attributes2}::tl2 -> + try + let attributes' = intersect_attributes (attributes1, attributes2) in + diff_ex tl1 tl2 + with + NotCompatible -> + {S.uri = uri1 ; S.attributes = attributes1 ; S.extra = ""}::(diff_ex tl1 tl2) +;; +*) + +(* + * implementazione del comando DIFF + *) +let rec diff_ex rs1 rs2 = + match (rs1, rs2) with + [],_ -> [] + | l,[] -> l + | (uri1,l)::tl1,(uri2,_)::_ when uri1 < uri2 -> (uri1,l)::(diff_ex tl1 rs2) + | (uri1,_)::_,(uri2,_)::tl2 when uri2 < uri1 -> (diff_ex rs1 tl2) + | (uri1,_)::tl1, (uri2,_)::tl2 -> (diff_ex tl1 tl2) +;; + + + + +let diff_ex l1 l2 = + let before = Sys.time () in + let res = diff_ex l1 l2 in + let after = Sys.time () in + let ll1 = string_of_int (List.length l1) in + let ll2 = string_of_int (List.length l2) in + let diff = string_of_float (after -. before) in + print_endline + ("DIFF(" ^ ll1 ^ ", " ^ ll2 ^ ") = " ^ string_of_int (List.length res) ^ + ": " ^ diff ^ "s") ; + flush stdout ; + res +;; + diff --git a/helm/ocaml/mathql_interpreter/diff.mli b/helm/ocaml/mathql_interpreter/diff.mli new file mode 100644 index 000000000..1cd9cf4de --- /dev/null +++ b/helm/ocaml/mathql_interpreter/diff.mli @@ -0,0 +1,27 @@ +(* 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/. + *) + +val diff_ex : + MathQL.resource_set -> MathQL.resource_set -> MathQL.resource_set diff --git a/helm/ocaml/mathql_interpreter/func.ml b/helm/ocaml/mathql_interpreter/func.ml new file mode 100644 index 000000000..1338af008 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/func.ml @@ -0,0 +1,56 @@ +(* 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/. + *) + +(* + * + *) + +open Dbconn;; +open Utility;; +open Intersect;; + +(* + * implementazione delle funzioni dublin core + *) +let rec func_dc tab outv inv = function + [] -> [] + | s::tl -> let res = + let c = pgc () in + let q = ("select " ^ tab ^ "." ^ outv ^ " from " ^ tab ^ " where " ^ tab ^ "." ^ inv ^ " = '" ^ s ^ "'") in + pgresult_to_string_list (c#exec q) + in + append (res,(func_dc tab outv inv tl)) +;; + +(* + * + *) +let fun_ex f value = + match f with + "name" -> func_dc "names" "name" "uri" value + | "reference" -> func_dc "names" "uri" "name" value + | _ -> [] +;; + diff --git a/helm/ocaml/mathql_interpreter/func.mli b/helm/ocaml/mathql_interpreter/func.mli new file mode 100644 index 000000000..2858ce0da --- /dev/null +++ b/helm/ocaml/mathql_interpreter/func.mli @@ -0,0 +1,26 @@ +(* 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/. + *) + +val fun_ex: string -> MathQL.value -> MathQL.value diff --git a/helm/ocaml/mathql_interpreter/intersect.ml b/helm/ocaml/mathql_interpreter/intersect.ml new file mode 100644 index 000000000..73bebaa50 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/intersect.ml @@ -0,0 +1,75 @@ +(* 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/. + *) + + +(* Catenates two lists preserving order and getting rid of duplicates *) +let rec append (l1,l2) = + match l1,l2 with + [],_ -> l2 + | _,[] -> l1 + | s1::tl1, s2::_ when s1 < s2 -> s1::append (tl1,l2) + | s1::_, s2::tl2 when s2 < s1 -> s2::append (l1,tl2) + | s1::tl1, s2::tl2 -> s1::append (tl1,tl2) + +;; + + +(* Sums two attribute groups preserving order *) +let rec sum_groups(gr1, gr2) = + match gr1, gr2 with + [],_ -> gr2 + | _,[] -> gr1 + | gr1, gr2 when gr1 = gr2 -> gr1 + | (key1,l1)::tl1, (key2,l2)::_ when key1 < key2 -> (key1,l1)::(sum_groups (tl1,gr2)) + | (key1,l1)::_, (key2,l2)::tl2 when key2 < key1 -> (key2,l2)::(sum_groups (gr1,tl2)) + | (key1,l1)::tl1, (key2,l2)::tl2 -> (key1,(append (l1,l2)))::(sum_groups (tl1,tl2)) + +;; + +(* Product between an attribute set and a group of attributes *) +let rec sub_prod (aset, gr) = (*prende un aset e un gr, fa la somma tra tutti i gruppi di aset e gr*) + match aset with + [] -> [] + | gr1::tl1 -> sum_groups (gr1, gr)::(sub_prod(tl1, gr)) +;; + + +(* Cartesian product between two attribute sets*) +let rec prod (as1, as2) = + match as1, as2 with + [],_ -> [] + | _,[] -> [] + | gr1::tl1, _ -> append((sub_prod (as2, gr1)), (prod (tl1, as2))) (* chiamo la sub_prod con un el. as1 e as2 *) +;; + +(* Intersection between two resource sets, preserves order and gets rid of duplicates *) +let rec intersect_ex rs1 rs2 = + match (rs1, rs2) with + [],_ + | _,[] -> [] + | (uri1,_)::tl1, (uri2,_)::_ when uri1 < uri2 -> intersect_ex tl1 rs2 + | (uri1,_)::_, (uri2,_)::tl2 when uri2 < uri1 -> intersect_ex rs1 tl2 + | (uri1,as1)::tl1, (uri2,as2)::tl2 -> (uri1, prod(as1,as2))::intersect_ex tl1 tl2 +;; diff --git a/helm/ocaml/mathql_interpreter/intersect.mli b/helm/ocaml/mathql_interpreter/intersect.mli new file mode 100644 index 000000000..5045162b6 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/intersect.mli @@ -0,0 +1,30 @@ +(* 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/. + *) + +val intersect_ex : + MathQL.result -> MathQL.result -> MathQL.result + +val append: + (string list * string list) -> string list diff --git a/helm/ocaml/mathql_interpreter/meet.ml b/helm/ocaml/mathql_interpreter/meet.ml new file mode 100644 index 000000000..bf0b5d780 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/meet.ml @@ -0,0 +1,34 @@ +(* 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/. + *) + + +let rec meet_ex v1 v2 = + match v1,v2 with + [],_ + | _,[] -> false + | s1::tl1, s2::_ when s1 < s2 -> meet_ex tl1 v2 + | s1::_, s2::tl2 when s2 < s1 -> meet_ex v1 tl2 + | _, _ -> true +;; diff --git a/helm/ocaml/mathql_interpreter/meet.mli b/helm/ocaml/mathql_interpreter/meet.mli new file mode 100644 index 000000000..366abd7fd --- /dev/null +++ b/helm/ocaml/mathql_interpreter/meet.mli @@ -0,0 +1,27 @@ +(* 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/. + *) + + +val meet_ex: MathQL.value -> MathQL.value -> bool diff --git a/helm/ocaml/mathql_interpreter/mqint.ml b/helm/ocaml/mathql_interpreter/mqint.ml new file mode 100644 index 000000000..54dc0e05c --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mqint.ml @@ -0,0 +1,213 @@ +(* 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/. + *) + + + + +(* + * implementazione del'interprete MathQL + *) + + + + +open Dbconn;; +open Union;; +open Intersect;; +open Meet;; +open Sub;; +open Context;; +open Diff;; +open Relation;; +open Func;; + + +exception BooleExpTrue + +let init connection_param = Dbconn.init connection_param + +let close () = Dbconn.close () + +let check () = + let status = Dbconn.pgc () + in () + +let stat = ref false + +let set_stat b = stat := b + +let get_stat () = ! stat + +let postgres_db = "postgres" + +let galax_db = "galax" + +let dbname = ref postgres_db + +let set_database s = + if s = postgres_db || s = galax_db then dbname := s + else raise (Invalid_argument s) + +let get_database () = ! dbname + +(* valuta una MathQL.set_exp e ritorna un MathQL.resource_set *) + +let rec exec_set_exp c = function + MathQL.SVar svar -> List.assoc svar c.svars + | MathQL.RVar rvar -> [List.assoc rvar c.rvars] + | MathQL.Ref vexp -> List.map (fun s -> (s,[])) (exec_val_exp c vexp) + | MathQL.Intersect (sexp1, sexp2) -> + let before = Sys.time() in + let rs1 = exec_set_exp c sexp1 in + let rs2 = exec_set_exp c sexp2 in + let res = intersect_ex rs1 rs2 in + let after = Sys.time() in + let ll1 = string_of_int (List.length rs1) in + let ll2 = string_of_int (List.length rs2) in + let diff = string_of_float (after -. before) in + if ! stat then + (print_endline("INTERSECT(" ^ ll1 ^ "," ^ ll2 ^ ") = " ^ string_of_int (List.length res) ^ + ": " ^ diff ^ "s"); + flush stdout); + res + | MathQL.Union (sexp1, sexp2) -> + let before = Sys.time () in + let res = union_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2) in + let after = Sys.time() in + let diff = string_of_float (after -. before) in + if ! stat then + (print_endline ("UNION: " ^ diff ^ "s"); + flush stdout); + res + | MathQL.LetSVar (svar, sexp1, sexp2) -> + let before = Sys.time() in + let c1 = upd_svars c ((svar, exec_set_exp c sexp1) :: c.svars) in + let res = exec_set_exp c1 sexp2 in + if ! stat then + (print_string ("LETIN " ^ svar ^ " = " ^ string_of_int (List.length res) ^ ": "); + print_endline (string_of_float (Sys.time() -. before) ^ "s"); + flush stdout); + res + | MathQL.LetVVar (vvar, vexp, sexp) -> + let before = Sys.time() in + let c1 = upd_vvars c ((vvar, exec_val_exp c vexp) :: c.vvars) in + let res = exec_set_exp c1 sexp in + if ! stat then + (print_string ("LETIN " ^ vvar ^ " = " ^ string_of_int (List.length res) ^ ": "); + print_endline (string_of_float (Sys.time() -. before) ^ "s"); + flush stdout); + res + | MathQL.Relation (rop, path, sexp, attl) -> + let before = Sys.time() in + if ! dbname = postgres_db then + (let res = relation_ex rop path (exec_set_exp c sexp) attl in + if ! stat then + (print_string ("RELATION " ^ (List.hd path) ^ " = " ^ string_of_int(List.length res) ^ ": "); + print_endline (string_of_float (Sys.time() -. before) ^ "s"); + flush stdout); + res) + else + (let res = relation_galax_ex rop path (exec_set_exp c sexp) attl in + if ! stat then + (print_string ("RELATION-GALAX " ^ (List.hd path) ^ " = " ^ string_of_int(List.length res) ^ ": "); + print_endline (string_of_float (Sys.time() -. before) ^ "s"); + flush stdout); + res) + + + | MathQL.Select (rvar, sexp, bexp) -> + let before = Sys.time() in + let rset = (exec_set_exp c sexp) in + let rec select_ex rset = + match rset with + [] -> [] + | r::tl -> let c1 = upd_rvars c ((rvar,r)::c.rvars) in + if (exec_boole_exp c1 bexp) then r::(select_ex tl) + else select_ex tl + in + let res = select_ex rset in + if ! stat then + (print_string ("SELECT " ^ rvar ^ " = " ^ string_of_int (List.length res) ^ ": "); + print_endline (string_of_float (Sys.time() -. before) ^ "s"); + flush stdout); + res + | MathQL.Diff (sexp1, sexp2) -> diff_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2) + | _ -> assert false + +(* valuta una MathQL.boole_exp e ritorna un boole *) + +and exec_boole_exp c = function + MathQL.False -> false + | MathQL.True -> true + | MathQL.Not x -> not (exec_boole_exp c x) + | MathQL.And (x, y) -> (exec_boole_exp c x) && (exec_boole_exp c y) + | MathQL.Or (x, y) -> (exec_boole_exp c x) || (exec_boole_exp c y) + | MathQL.Sub (vexp1, vexp2) -> sub_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2) + | MathQL.Meet (vexp1, vexp2) -> meet_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2) + | MathQL.Eq (vexp1, vexp2) -> (exec_val_exp c vexp1) = (exec_val_exp c vexp2) + | MathQL.Ex l bexp -> + if l = [] then (exec_boole_exp c bexp) + else + let latt = List.map (fun uri -> + let (r,attl) = List.assoc uri c.rvars in (uri,attl)) l (*latt = l + attributi*) + in + try + let rec prod c = function + [] -> if (exec_boole_exp c bexp) then raise BooleExpTrue + | (uri,attl)::tail1 -> let rec sub_prod attl = + match attl with +(*per ogni el. di attl *) [] -> () +(*devo andare in ric. su tail1*) | att::tail2 -> let c1 = upd_groups c ((uri,att)::c.groups) in + prod c1 tail1; sub_prod tail2 + in + sub_prod attl + in + prod c latt; false + with BooleExpTrue -> true + +(* valuta una MathQL.val_exp e ritorna un MathQL.value *) + +and exec_val_exp c = function + MathQL.Const x -> let + ol = List.sort compare x in + let rec edup = function + + [] -> [] + | s::tl -> if tl <> [] then + if s = (List.hd tl) then edup tl + else s::(edup tl) + else s::[] + in + edup ol + | MathQL.Record (rvar, vvar) -> List.assoc vvar (List.assoc rvar c.groups) + + | MathQL.VVar s -> List.assoc s c.vvars + | MathQL.RefOf sexp -> List.map (fun (s,_) -> s) (exec_set_exp c sexp) + | MathQL.Fun (s, vexp) -> fun_ex s (exec_val_exp c vexp) + | MathQL.Attribute (rop, path, vexp) -> [] + +(* valuta una MathQL.set_exp nel contesto vuoto e ritorna un MathQL.resource_set *) +and execute x = + exec_set_exp {svars = []; rvars = []; groups = []; vvars = []} x diff --git a/helm/ocaml/mathql_interpreter/mqint.mli b/helm/ocaml/mathql_interpreter/mqint.mli new file mode 100644 index 000000000..414515308 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mqint.mli @@ -0,0 +1,46 @@ +(* 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/. + *) + +val init : string -> unit (* open database *) + +val execute : MathQL.query -> MathQL.result (* execute query *) + +val close : unit -> unit (* close database *) + +val check : unit -> unit (* check connection *) + +val set_stat : bool -> unit (* set stat emission *) + +val get_stat : unit -> bool (* check stat emission *) + +val postgres_db : string (* postgres *) + +val galax_db : string (* galax *) + +val set_database : string -> unit (* switch postgres/galax *) + +val get_database : unit -> string (* check db used *) + + diff --git a/helm/ocaml/mathql_interpreter/relation.ml b/helm/ocaml/mathql_interpreter/relation.ml new file mode 100644 index 000000000..94dc10870 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/relation.ml @@ -0,0 +1,149 @@ +(* 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://www.cs.unibo.it/helm/. + *) + + +(* + * implementazione del comando Relation + *) + + + + +open Union;; +open Dbconn;; +open Utility;; + + + + +let get_prop_id propl = + let prop = List.hd propl in + if prop="refObj" then "F" + else if prop="backPointer" then "B" + else assert false +;; + + +let relation_ex rop path rset attl = + if path = [] then [] + else + let usek = get_prop_id path in + let vvar = if attl = [] then "position" + else List.hd attl + in + let c = pgc () in + let rset_list = (* lista di singoletti:resource_set di un elemento *) + (List.fold_left (fun acc (uri,l) -> + let tv = pgresult_to_string (c#exec ("select id from registry where uri='" ^ uri ^ "'")) in + let qq = "select uri, context from t" ^ tv ^ " where prop_id='" ^ usek ^ "' order by uri asc" in + let res = c#exec qq in + (List.map + (function + [uri;context] -> [(uri,[[(vvar,[context])]])] + | _ -> assert false ) + res#get_list) @ acc + ) + [] rset + ) + in + let rec edup = function + [] -> [] + | rs1::tl -> union_ex rs1 (edup tl) + in + edup rset_list +;; + + + +(**** IMPLEMENTAZIONE DELLA RELATION PER GALAX ****) + + +(* trasforma un uri in un filename *) +let tofname uri = + if String.contains uri ':' then + (let len = String.length uri in + let scuri = String.sub uri 4 (len-4) in (*tolgo cic:*) + if String.contains scuri '#' then + (let pos = String.index scuri '#' in + let s1 = Str.string_before scuri pos in + let xp = Str.string_after scuri pos in + let xp = Str.global_replace (Str.regexp "#xpointer(1") "" xp in + let xp = Str.global_replace (Str.regexp "\/") "," xp in + let xp = Str.global_replace (Str.regexp ")") "" xp in + let fname = (s1 ^ xp) in + fname) + else + scuri) + else uri + + +(* prende una lista di uri (contenente alternativamente uri e pos) e costruisce una lista di resource *) +let rec rsetl uril vvar = + match uril with + | uri::tl -> let scuri = (*tofname*) uri in + [(scuri, [[(vvar, [(List.hd tl)])]])]::(rsetl (List.tl tl) vvar) + | [] -> [] + + +(* prende una resource e una vvar e restituisce la lista delle resource in relazione (refObj o backPointer in base al parametro "path") con tale resource e associa alla proprieta' il nome della vvar contenuto in "attl" *) +let muse path attl r = + if path = [] then [] + else + let vvar = if attl = [] then "position" + else List.hd attl + in + let uri = fst r in + let furi = tofname uri in + let dtag = List.hd path in + let dir = + match dtag with + "refObj" -> "/projects/helm/metadata/create4/forward" + | _ -> "/projects/helm/metadata/create4/backward" + in + let xq ="namespace h=\"http://www.cs.unibo.it/helm/schemas/mattone.rdf#\" + namespace rdf=\"http://www.w3.org/1999/02/22-rdf-syntax-ns#\" + for $i in document(" ^ "\"" ^ dir ^ furi ^ ".xml" ^ "\"" ^ + ")/rdf:RDF/h:Object/h:" ^ dtag ^ "/h:Occurrence + return ($i/h:occurrence, $i/h:position)" + + in + let uril = Toputils.eval_query_string xq in (* e' una lista di liste di stringhe*) + let hd_uril = List.hd uril in(*prendo la testa che contiene altern. lista di uri e pos. *) + let rset_list = rsetl hd_uril vvar in (* da hd_uril costruisco una lista di resource_set(singoletti)*) + let rec edup = function + [] -> [] + | rs1::tl -> union_ex rs1 (edup tl) + in + edup rset_list + + + + +(* prende un resource_set, una vvar (primo el. di attl) a cui associare la posizione, e la relazione (refObj o backPointer) e per ogni resource chiama la muse +NOTA: "rop" per ora non viene usato perche' vale sempre "ExactOp" *) +let relation_galax_ex rop path rset attl = + List.stable_sort (fun (uri1,l1) (uri2,l2) -> compare uri1 uri2) (List.concat (List.map (muse path attl) rset)) + + diff --git a/helm/ocaml/mathql_interpreter/relation.mli b/helm/ocaml/mathql_interpreter/relation.mli new file mode 100644 index 000000000..aa7c75509 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/relation.mli @@ -0,0 +1,30 @@ +(* 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/. + *) + +val relation_ex : + MathQL.refine_op -> MathQL.path -> MathQL.resource_set -> MathQL.vvar_list -> MathQL.resource_set + +val relation_galax_ex : + MathQL.refine_op -> MathQL.path -> MathQL.resource_set -> MathQL.vvar_list -> MathQL.resource_set diff --git a/helm/ocaml/mathql_interpreter/select.ml b/helm/ocaml/mathql_interpreter/select.ml new file mode 100644 index 000000000..ee9f329ba --- /dev/null +++ b/helm/ocaml/mathql_interpreter/select.ml @@ -0,0 +1,153 @@ +(* 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://www.cs.unibo.it/helm/. + *) + +(* + * implementazione del comando SELECT + *) +(* +open MathQL;; +open Func;; +open Utility;; + +exception ExecuteFunctionNotInitialized;; +let execute = + ref + (function _ -> raise ExecuteFunctionNotInitialized) +;; + +(* + * valutazione di una stringa + *) +let stringeval env = + let module S = Mathql_semantics in + function + MQCons s -> + s + | MQFunc (f, rvar) -> + let {S.uri = uri} = List.assoc rvar env in + apply_func f uri + | MQStringRVar rvar -> + let {S.uri = uri} = List.assoc rvar env in + uri + | MQStringSVar svar -> + let (_,{S.attributes = attributes}) = List.hd env in + List.assoc svar attributes + | MQMConclusion -> + "MainConclusion" + | MQConclusion -> + "InConclusion" +;; + +(* + * + *) +let rec is_good env = + let module S = Mathql_semantics in + function + MQAnd (b1, b2) -> + (is_good env b1) && (is_good env b2) + | MQOr (b1, b2) -> + (is_good env b1) || (is_good env b2) + | MQNot b1 -> + not (is_good env b1) + | MQTrue -> + true + | MQFalse -> + false + | MQIs (s1, s2) -> + (stringeval env s1) = (stringeval env s2) +(*CSC: magari le prossime funzioni dovrebbero andare in un file a parte, *) +(*CSC: insieme alla [execute] che utilizzano *) + | MQSetEqual (q1,q2) -> + (* set_of_result returns an ordered list of uris without duplicates *) + let rec set_of_result = + function + _,[] -> [] + | (Some olduri as v),{S.uri = uri}::tl when uri = olduri -> + set_of_result (v,tl) + | _,{S.uri = uri}::tl -> + uri::(set_of_result (Some uri, tl)) + in + let ul1 = set_of_result (None,!execute env q1) in + let ul2 = set_of_result (None,!execute env q2) in + print_endline ("MQSETEQUAL(" ^ + string_of_int (List.length (!execute env q1)) ^ ">" ^ + string_of_int (List.length ul1) ^ "," ^ + string_of_int (List.length (!execute env q2)) ^ ">" ^ + string_of_int (List.length ul2) ^ ")") ; + flush stdout ; + (try + List.fold_left2 (fun b uri1 uri2 -> b && uri1=uri2) true ul1 ul2 + with + _ -> false) + | MQSubset (q1,q2) -> +(*CSC: codice cut&paste da sopra: ridurlo facendo un'unica funzione h.o. *) + (* set_of_result returns an ordered list of uris without duplicates *) + let rec set_of_result = + function + _,[] -> [] + | (Some olduri as v),{S.uri = uri}::tl when uri = olduri -> + set_of_result (v,tl) + | _,{S.uri = uri}::tl -> + uri::(set_of_result (Some uri, tl)) + in + let ul1 = set_of_result (None,!execute env q1) in + let ul2 = set_of_result (None,!execute env q2) in + print_endline ("MQSUBSET(" ^ + string_of_int (List.length (!execute env q1)) ^ ">" ^ + string_of_int (List.length ul1) ^ "," ^ + string_of_int (List.length (!execute env q2)) ^ ">" ^ + string_of_int (List.length ul2) ^ ")") ; + flush stdout ; + let rec is_subset s1 s2 = + match s1,s2 with + [],_ -> true + | _,[] -> false + | uri1::tl1,uri2::tl2 when uri1 = uri2 -> + is_subset tl1 tl2 + | uri1::_,uri2::tl2 when uri1 > uri2 -> + is_subset s1 tl2 + | _,_ -> false + in + is_subset ul1 ul2 +;; + +(* + * implementazione del comando SELECT + *) +let select_ex env avar alist abool = + let _ = print_string ("SELECT = ") + and t = Sys.time () in + let result = + List.filter (function entry -> is_good ((avar,entry)::env) abool) alist + in + print_string (string_of_int (List.length result) ^ ": ") ; + print_endline (string_of_float (Sys.time () -. t) ^ "s") ; + flush stdout ; + result +;; *) + +let select_ex rvar rset bexp + diff --git a/helm/ocaml/mathql_interpreter/sortedby.ml b/helm/ocaml/mathql_interpreter/sortedby.ml new file mode 100644 index 000000000..b9a05a002 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/sortedby.ml @@ -0,0 +1,62 @@ +(* 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://www.cs.unibo.it/helm/. + *) + +(* + * implementazione del comando SORTEDBY + *) + +open MathQL;; +open Func;; +open Utility;; + +(* + * implementazione del comando SORTEDBY + *) +let sortedby_ex alist order afunc = + let before = Sys.time () in + let res = + let module S = Mathql_semantics in + (Sort.list + (fun {S.extra = e1} {S.extra = e2} -> + match order with + MQAsc -> e1 < e2 + | MQDesc -> e1 > e2 + ) + (List.map + (fun {S.uri = u ; S.attributes = attr} -> {S.uri = u ; S.attributes = attr ; S.extra = (apply_func afunc u)}) + alist + ) + ) + in + let after = Sys.time () + and ll1 = string_of_int (List.length alist) in + let diff = string_of_float (after -. before) in + print_endline + ("SORTEDBY(" ^ ll1 ^ ") = " ^ string_of_int (List.length res) ^ + ": " ^ diff ^ "s") ; + flush stdout ; + res +;; + diff --git a/helm/ocaml/mathql_interpreter/sub.ml b/helm/ocaml/mathql_interpreter/sub.ml new file mode 100644 index 000000000..e59bf049d --- /dev/null +++ b/helm/ocaml/mathql_interpreter/sub.ml @@ -0,0 +1,34 @@ +(* 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/. + *) + + +let rec sub_ex v1 v2 = + match v1,v2 with + [],_ -> true + | _,[] -> false + | s1::_, s2::_ when s1 < s2 -> false + | s1::_, s2::tl2 when s2 < s1 -> sub_ex v1 tl2 + | s1::tl1, s2::tl2 -> sub_ex tl1 tl2 +;; diff --git a/helm/ocaml/mathql_interpreter/sub.mli b/helm/ocaml/mathql_interpreter/sub.mli new file mode 100644 index 000000000..b81f542c4 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/sub.mli @@ -0,0 +1,27 @@ +(* 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/. + *) + + +val sub_ex: MathQL.value -> MathQL.value -> bool diff --git a/helm/ocaml/mathql_interpreter/union.ml b/helm/ocaml/mathql_interpreter/union.ml new file mode 100644 index 000000000..e2d9fcb01 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/union.ml @@ -0,0 +1,52 @@ +(* 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/. + *) + +(* + * implementazione del comando UNION + *) + + +(* Merges two attribute group lists preserves order and gets rid of duplicates*) +let rec merge l1 l2 = + match (l1,l2) with + [],l + | l,[] -> l + | g1::tl1,g2::_ when g1 < g2 -> g1::(merge tl1 l2) + | g1::_,g2::tl2 when g2 < g1 -> g2::(merge l1 tl2) + | g1::tl1,g2::tl2 -> g1::(merge tl1 tl2) +;; + +(* preserves order and gets rid of duplicates *) +let rec union_ex rs1 rs2 = + match (rs1, rs2) with + [],l + | l,[] -> l + | (uri1,l1)::tl1,(uri2,_)::_ when uri1 < uri2 -> (uri1,l1)::(union_ex tl1 rs2) + | (uri1,_)::_,(uri2,l2)::tl2 when uri2 < uri1 -> (uri2,l2)::(union_ex rs1 tl2) + | (uri1,l1)::tl1,(uri2,l2)::tl2 -> if l1 = l2 then (uri1,l1)::(union_ex tl1 tl2) + else (uri1,merge l1 l2)::(union_ex tl1 tl2) +;; + + diff --git a/helm/ocaml/mathql_interpreter/union.mli b/helm/ocaml/mathql_interpreter/union.mli new file mode 100644 index 000000000..6890bdb0c --- /dev/null +++ b/helm/ocaml/mathql_interpreter/union.mli @@ -0,0 +1,27 @@ +(* 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/. + *) + +val union_ex : +MathQL.result -> MathQL.result -> MathQL.result diff --git a/helm/on-line/xslt/ls2html.xsl b/helm/on-line/xslt/ls2html.xsl new file mode 100644 index 000000000..f0376baa5 --- /dev/null +++ b/helm/on-line/xslt/ls2html.xsl @@ -0,0 +1,158 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + [{$alt}] + + + + + + + + + + + + + + + + Index of <xsl:value-of select="$uri"/> + + + + + + + + + + + + + + +
+

+ + + + + + + + + + + + + + + + + + + + + + + + text.gif + generic.red.gif + + + + + [{@name}] + + + + + + + + + + + + + + + + + + + + + Body + + + + + + -- 2.39.2