'V7_3_new_exportation'.
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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))
--- /dev/null
+!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
--- /dev/null
+(* 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<n*1/d
+*)
+
+let tac_zero_inf_pos (n,d) ~status =
+ (*let cste = pf_parse_constr gl in*)
+ let pall str ~status:(proof,goal) t =
+ debug ("tac "^str^" :\n" );
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> 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);;
+
+
--- /dev/null
+val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic
+val fourier_tac: ProofEngineTypes.tactic
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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 =
+ "<html>" ^
+ " <body bgColor=\"white\">"
+;;
+
+let htmlfooter =
+ " </body>" ^
+ "</html>"
+;;
+
+(*
+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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ 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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ 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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ end
+ | None ->
+ output_html outputhtml
+ ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ end
+ | None ->
+ output_html outputhtml
+ ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+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
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ end
+ | None ->
+ output_html outputhtml
+ ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ end
+ | None ->
+ output_html outputhtml
+ ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+
+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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ Xml.xml_cdata
+ ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+ xml
+ >]
+ in
+ Xml.pp ~quiet:true xml' (Some prooffile) ;
+ output_html outputhtml
+ ("<h1 color=\"Green\">Current proof saved to " ^
+ prooffile ^ "</h1>")
+;;
+
+(* 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
+ ("<h1 color=\"Green\">Current proof loaded from " ^
+ prooffile ^ "</h1>")
+ | _ -> assert false
+ with
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
+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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ 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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ 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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+
+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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
+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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
+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
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
+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 ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
+;;
+
+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 = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") in
+ output_html outputhtml html ;
+ let uri' = user_uri_choice uris in
+ ignore ((inputt#insert_text uri') ~pos:0)
+ with
+ e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+
+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 =
+ " <h1>Backward Query: </h1>" ^
+ " <h2>Levels: </h2> " ^
+ MQueryGenerator.string_of_levels (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
+ " <pre>" ^ get_last_query result ^ "</pre>" 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
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+
+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:"<html><body bgColor=\"white\"></body></html>"
+ ~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 = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") 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 ();
+;;
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
+(* 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 = " <p>\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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
+(* 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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+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)
--- /dev/null
+(* 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
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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 []
+;;
--- /dev/null
+(* 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
--- /dev/null
+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 = " <p>\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
--- /dev/null
+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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 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 ""
+;;
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
+(* 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 }
--- /dev/null
+/* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ */
+
+/******************************************************************************/
+/* */
+/* PROJECT HELM */
+/* */
+/* Ferruccio Guidi <fguidi@cs.unibo.it> */
+/* 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 <string> 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 <string> qstr
+ %type <MathQL.query> query
+ %type <MathQL.result> 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 }
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
+(* 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 ^ ")"
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
+(* 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
+
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://www.cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
+(* Irene Schena <schena@cs.unibo.it> *)
+(* 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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+(* 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}
+
+
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://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
+;;
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+val pgc : unit -> Postgres.connection
+val init : string -> unit
+val close : unit -> unit
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(*
+ * 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
+;;
+
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+val diff_ex :
+ MathQL.resource_set -> MathQL.resource_set -> MathQL.resource_set
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(*
+ *
+ *)
+
+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
+ | _ -> []
+;;
+
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+val fun_ex: string -> MathQL.value -> MathQL.value
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+
+(* 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
+;;
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+val intersect_ex :
+ MathQL.result -> MathQL.result -> MathQL.result
+
+val append:
+ (string list * string list) -> string list
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+
+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
+;;
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+
+val meet_ex: MathQL.value -> MathQL.value -> bool
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+
+
+
+(*
+ * 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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+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 *)
+
+
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://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))
+
+
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://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
+
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://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
+;;
+
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+
+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
+;;
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+
+val sub_ex: MathQL.value -> MathQL.value -> bool
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(*
+ * 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)
+;;
+
+
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+val union_ex :
+MathQL.result -> MathQL.result -> MathQL.result
--- /dev/null
+<?xml version="1.0"?>
+
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
+
+<xsl:import href="utils.xsl"/>
+
+<xsl:output method="html" encoding="iso-8859-1"/>
+
+<!-- uri must end with '/' -->
+<xsl:param name="uri" select="''"/>
+<xsl:param name="keys" select="''"/>
+<xsl:param name="getterURL" select="''"/>
+<xsl:param name="interfaceURL" select="''"/>
+<xsl:param name="target" select="''"/>
+
+<xsl:template name="chop">
+ <xsl:param name="uri" select="''"/>
+ <xsl:param name="prefix" select="''"/>
+ <xsl:variable name="newprefix" select="substring-before($uri,'/')"/>
+ <xsl:choose>
+ <xsl:when test="$newprefix = ''"><xsl:value-of select="$prefix"/></xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="chop">
+ <xsl:with-param name="uri" select="substring-after($uri,'/')"/>
+ <xsl:with-param name="prefix" select="concat($prefix,$newprefix,'/')"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:variable name="uridotdot">
+ <xsl:call-template name="chop">
+ <xsl:with-param name="uri" select="substring($uri,1,string-length($uri)-1)"/>
+ </xsl:call-template>
+</xsl:variable>
+
+<xsl:template name="makeDir">
+ <xsl:param name="uri" select="''"/>
+ <xsl:param name="basename" select="''"/>
+ <xsl:param name="icon" select="''"/>
+ <xsl:param name="alt" select="''"/>
+ <tr>
+ <td>
+ <img border="0" src="{concat($interfaceURL,'/icons/',$icon)}" alt="[{$alt}]"/>
+ </td>
+ <td>
+ <xsl:variable name="quoteduri">
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="$uri"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <a
+ onClick=
+ "top.{$target}uri='{$quoteduri}';
+ refresh{$target}Header('{$interfaceURL}/html/library/header.html');
+ var search='?keys={$keys}' +
+ '&xmluri=' + escape('{$getterURL}ls?format=xml'+'&baseuri={$quoteduri}')+
+ '&param.uri={$quoteduri}' +
+ '&param.keys={$keys}' +
+ '&param.getterURL={$getterURL}' +
+ '&param.target={$target}' +
+ '&param.interfaceURL={$interfaceURL}';
+ var pathname = this.pathname;
+ if (pathname.charAt(0) != '/')
+ pathname = '/' + pathname;
+ this.href=
+ this.protocol + '//' + this.host + pathname + search + this.hash;"
+ onMouseOver="window.status='{$quoteduri}'; return true"
+ href="apply"
+ ><xsl:value-of select="$basename"/></a>
+ </td>
+ </tr>
+</xsl:template>
+
+<xsl:template match="/">
+ <html>
+ <head>
+ <title>Index of <xsl:value-of select="$uri"/></title>
+ <xsl:copy-of select="document(concat($interfaceURL,'/javascript/control.js_xml'))" />
+ <xsl:copy-of select="document(concat($interfaceURL,'/javascript/utils.js_xml'))" />
+ </head>
+ <body bgcolor="#ffffff" text="#000000">
+ <table>
+ <xsl:if test="$uridotdot != ''">
+ <xsl:call-template name="makeDir">
+ <xsl:with-param name="uri" select="$uridotdot"/>
+ <xsl:with-param name="basename" select="'Parent Directory'"/>
+ <xsl:with-param name="icon" select="'back.gif'"/>
+ <xsl:with-param name="alt" select="'Parent Directory'"/>
+ </xsl:call-template>
+ </xsl:if>
+ <xsl:apply-templates select="*"/>
+ </table>
+ <hr noshade="yes" align="left" width="80%"/>
+ </body>
+ </html>
+</xsl:template>
+
+<xsl:template match="section">
+ <xsl:variable name="diruri">
+ <xsl:value-of select="."/>
+ </xsl:variable>
+ <xsl:call-template name="makeDir">
+ <xsl:with-param name="uri" select="concat($uri,$diruri,'/')"/>
+ <xsl:with-param name="basename" select="$diruri"/>
+ <xsl:with-param name="icon" select="'folder.gif'"/>
+ <xsl:with-param name="alt" select="$uri"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="object">
+ <xsl:variable name="name" select="@name"/>
+ <xsl:variable name="ann" select="ann/@value"/>
+ <xsl:variable name="types" select="types/@value"/>
+ <xsl:variable name="body" select="body/@value"/>
+ <xsl:variable name="icon">
+ <xsl:choose>
+ <xsl:when test="$ann = 'YES'">text.gif</xsl:when>
+ <xsl:otherwise>generic.red.gif</xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+ <tr>
+ <td>
+ <img border="0" src="{concat($interfaceURL,'/icons/',$icon)}" alt="[{@name}]"/>
+ </td>
+ <td>
+ <xsl:variable name="quoteduri">
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="$uri"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:variable name="quotedname">
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="$name"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:variable name="quotedbodyname">
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="concat($name,'.body')"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <a href="" target="{$target}"
+ onClick="this.href=makeURL('{$target}','{concat($quoteduri,$quotedname)}','{$ann}','{$types}')"
+ onMouseOver="window.status='{concat($quoteduri,$quotedname)}'; return true"
+ ><xsl:value-of select="$name"/></a>
+ <xsl:if test="not($body='NO')">
+ <xsl:text> </xsl:text>
+ <a href="" target="{$target}"
+ onClick="this.href=makeURL('{$target}','{concat($quoteduri,$quotedbodyname)}','{$ann}','{$types}')"
+ onMouseOver="window.status='{concat($quoteduri,$quotedname)}'; return true"
+ >Body</a>
+ </xsl:if>
+ </td>
+ </tr>
+</xsl:template>
+
+</xsl:stylesheet>
projects / helm.git / commitdiff