From 26687f6c7acd3c9ec642625288a8a2185c5b81c5 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 21 May 2003 11:24:19 +0000 Subject: [PATCH] moved to helm/ocaml/mathql_test --- helm/gTopLevel/topLevel/.cvsignore | 1 - helm/gTopLevel/topLevel/.depend | 2 - helm/gTopLevel/topLevel/Makefile | 49 ------- helm/gTopLevel/topLevel/esempi.cic | 125 ----------------- helm/gTopLevel/topLevel/topLevel.ml | 202 ---------------------------- 5 files changed, 379 deletions(-) delete mode 100644 helm/gTopLevel/topLevel/.cvsignore delete mode 100644 helm/gTopLevel/topLevel/.depend delete mode 100644 helm/gTopLevel/topLevel/Makefile delete mode 100644 helm/gTopLevel/topLevel/esempi.cic delete mode 100644 helm/gTopLevel/topLevel/topLevel.ml diff --git a/helm/gTopLevel/topLevel/.cvsignore b/helm/gTopLevel/topLevel/.cvsignore deleted file mode 100644 index 197e6e54e..000000000 --- a/helm/gTopLevel/topLevel/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -*.cmi *.cmo *.cmx topLevel.opt diff --git a/helm/gTopLevel/topLevel/.depend b/helm/gTopLevel/topLevel/.depend deleted file mode 100644 index 0bd921fe1..000000000 --- a/helm/gTopLevel/topLevel/.depend +++ /dev/null @@ -1,2 +0,0 @@ -topLevel.cmo: ../mQueryGenerator.cmi -topLevel.cmx: ../mQueryGenerator.cmx diff --git a/helm/gTopLevel/topLevel/Makefile b/helm/gTopLevel/topLevel/Makefile deleted file mode 100644 index 5b3146531..000000000 --- a/helm/gTopLevel/topLevel/Makefile +++ /dev/null @@ -1,49 +0,0 @@ -BIN_DIR = /usr/local/bin -REQUIRES = helm-urimanager helm-cic_textual_parser helm-cic_proof_checking helm-mathql helm-mathql_interpreter -PREDICATES = -OCAMLOPTIONS = -I .. -package "$(REQUIRES)" -predicates "$(PREDICATES)" -OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) -OCAMLDEP = ocamldep -I .. - -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: topLevel -opt: topLevel.opt - -DEPOBJS = topLevel.ml - -TOPLEVELOBJS = ../mQueryLevels.cmo ../mQueryGenerator.cmo topLevel.cmo - -depend: - $(OCAMLDEP) $(DEPOBJS) > .depend - -topLevel: $(TOPLEVELOBJS) $(LIBRARIES) - $(OCAMLC) -linkpkg -o topLevel $(TOPLEVELOBJS) - -topLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) - $(OCAMLOPT) -linkpkg -o topLevel.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 topLevel topLevel.opt - -install: - cp topLevel topLevel.opt $(BIN_DIR) - -uninstall: - rm -f $(BIN_DIR)/topLevel $(BIN_DIR)/topLevel.opt - -.PHONY: install uninstall clean - -ifneq ($(MAKECMDGOALS), depend) - include .depend -endif diff --git a/helm/gTopLevel/topLevel/esempi.cic b/helm/gTopLevel/topLevel/esempi.cic deleted file mode 100644 index 38e5f3333..000000000 --- a/helm/gTopLevel/topLevel/esempi.cic +++ /dev/null @@ -1,125 +0,0 @@ -alias BV /Sophia-Antipolis/HARDWARE/GENE/BV/BV.con -alias BV_increment /Sophia-Antipolis/HARDWARE/ADDER/IncrDecr/BV_increment.con -alias BV_increment_carry /Sophia-Antipolis/HARDWARE/ADDER/IncrDecr/BV_increment_carry.con -alias BV_to_nat /Sophia-Antipolis/HARDWARE/GENE/BV/BV_to_nat.con -alias Exp /Eindhoven/POCKLINGTON/exp/Exp.con -alias IZR /Coq/Reals/Raxioms/IZR.con -alias Int_part /Coq/Reals/R_Ifp/Int_part.con -alias Mod /Eindhoven/POCKLINGTON/mod/Mod.con -alias NEG /Coq/ZArith/fast_integer/fast_integers/Z.ind#1/1/3 -alias O /Coq/Init/Datatypes/nat.ind#1/1/1 -alias POS /Coq/ZArith/fast_integer/fast_integers/Z.ind#1/1/2 -alias Prime /Eindhoven/POCKLINGTON/prime/Prime.con -alias R /Coq/Reals/Rdefinitions/R.con -alias R0 /Coq/Reals/Rdefinitions/R0.con -alias R1 /Coq/Reals/Rdefinitions/R1.con -alias Rgt /Coq/Reals/Rdefinitions/Rgt.con -alias Rinv /Coq/Reals/Rdefinitions/Rinv.con -alias Rle /Coq/Reals/Rdefinitions/Rle.con -alias Rlt /Coq/Reals/Rdefinitions/Rlt.con -alias Rminus /Coq/Reals/Rdefinitions/Rminus.con -alias Rmult /Coq/Reals/Rdefinitions/Rmult.con -alias Ropp /Coq/Reals/Rdefinitions/Ropp.con -alias Rplus /Coq/Reals/Rdefinitions/Rplus.con -alias S /Coq/Init/Datatypes/nat.ind#1/1/2 -alias Z /Coq/ZArith/fast_integer/fast_integers/Z.ind#1/1 -alias ZERO /Coq/ZArith/fast_integer/fast_integers/Z.ind#1/1/1 -alias ZExp /Eindhoven/POCKLINGTON/exp/ZExp.con -alias Zdiv2 /Coq/ZArith/Zmisc/arith/Zdiv2.con -alias Zge /Coq/ZArith/zarith_aux/Zge.con -alias Zle /Coq/ZArith/zarith_aux/Zle.con -alias Zlt /Coq/ZArith/zarith_aux/Zlt.con -alias Zminus /Coq/ZArith/zarith_aux/Zminus.con -alias Zmult /Coq/ZArith/fast_integer/fast_integers/Zmult.con -alias Zodd /Coq/ZArith/Zmisc/arith/Zodd.con -alias Zplus /Coq/ZArith/fast_integer/fast_integers/Zplus.con -alias Zpower_nat /Coq/omega/Zpower/section1/Zpower_nat.con -alias Zpower_pos /Coq/omega/Zpower/section1/Zpower_pos.con -alias Zpred /Coq/ZArith/zarith_aux/Zpred.con -alias Zs /Coq/ZArith/zarith_aux/Zs.con -alias ad /Coq/IntMap/Addr/ad.ind#1/1 -alias ad_bit /Coq/IntMap/Addr/ad_bit.con -alias ad_double_plus_un /Coq/IntMap/Addr/ad_double_plus_un.con -alias ad_x /Coq/IntMap/Addr/ad.ind#1/1/2 -alias ad_xor /Coq/IntMap/Addr/ad_xor.con -alias allex /Eindhoven/POCKLINGTON/fermat/allex.con -alias and /Coq/Init/Logic/Conjunction/and.ind#1/1 -alias appbv /Sophia-Antipolis/HARDWARE/GENE/BV/appbv.con -alias bool /Coq/Init/Datatypes/bool.ind#1/1 -alias consbv /Sophia-Antipolis/HARDWARE/GENE/BV/consbv.con -alias convert /Coq/ZArith/fast_integer/fast_integers/convert.con -alias div2 /Coq/Arith/Div2/div2.con -alias double /Coq/Arith/Div2/double.con -alias eq /Coq/Init/Logic/Equality/eq.ind#1/1 -alias eq_ind /Coq/Init/Logic/Equality/eq_ind.con -alias eq_ind_r /Coq/Init/Logic/Logic_lemmas/eq_ind_r.con -alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1 -alias even /Coq/Arith/Even/even.ind#1/1 -alias ex /Coq/Init/Logic/First_order_quantifiers/ex.ind#1/1 -alias f_equal /Coq/Init/Logic/Logic_lemmas/equality/f_equal.con -alias iff /Coq/Init/Logic/Equivalence/iff.con -alias le /Coq/Init/Peano/le.ind#1/1 -alias lengthbv /Sophia-Antipolis/HARDWARE/GENE/BV/lengthbv.con -alias lift_rec_r /Rocq/LAMBDA/Substitution/lift_rec_r.con -alias log_inf /Coq/omega/Zlogarithm/Log_pos/log_inf.con -alias log_sup /Coq/omega/Zlogarithm/Log_pos/log_sup.con -alias lt /Coq/Init/Peano/lt.con -alias mapmult /Eindhoven/POCKLINGTON/list/mapmult.con -alias minus /Coq/Arith/Minus/minus.con -alias mult /Coq/Init/Peano/mult.con -alias nat /Coq/Init/Datatypes/nat.ind#1/1 -alias nat_of_ad /Coq/IntMap/Adalloc/AdAlloc/nat_of_ad.con -alias negb /Coq/Bool/Bool/negb.con -alias nilbv /Sophia-Antipolis/HARDWARE/GENE/BV/nilbv.con -alias not /Coq/Init/Logic/not.con -alias odd /Coq/Arith/Even/even.ind#1/2 -alias or /Coq/Init/Logic/Disjunction/or.ind#1/1 -alias permmod /Eindhoven/POCKLINGTON/fermat/permmod.con -alias plus /Coq/Init/Peano/plus.con -alias positive /Coq/ZArith/fast_integer/fast_integers/positive.ind#1/1 -alias power2 /Sophia-Antipolis/HARDWARE/GENE/Arith_compl/power2.con -alias pred /Coq/Init/Peano/pred.con -alias redexes /Rocq/LAMBDA/Redexes/redexes.ind#1/1 -alias shift_nat /Coq/omega/Zpower/Powers_of_2/shift_nat.con -alias shift_pos /Coq/omega/Zpower/Powers_of_2/shift_pos.con -alias subst_rec_r /Rocq/LAMBDA/Substitution/subst_rec_r.con -alias two_p /Coq/omega/Zpower/Powers_of_2/two_p.con -alias until /Eindhoven/POCKLINGTON/fermat/until.con -alias xH /Coq/ZArith/fast_integer/fast_integers/positive.ind#1/1/3 -alias xI /Coq/ZArith/fast_integer/fast_integers/positive.ind#1/1/1 -alias xO /Coq/ZArith/fast_integer/fast_integers/positive.ind#1/1/2 -alias zproduct /Eindhoven/POCKLINGTON/list/zproduct.con - -!n:nat.(eq nat (mult (S (S O)) n) O); -!n:nat.(eq nat (plus O n) (plus n O)); -!n:nat.!m:nat.(le (mult (S (S O)) n) (mult (S (S O)) m)); -!p:nat.(eq nat p p)->(eq nat p p); -!p:nat.!q:nat.(le p q)->(or (le (S p) q) (eq nat p q)); -!n:nat.(eq nat (double (S n)) (S (S (double n)))); -!n:nat.(and (iff (even n) (eq nat (div2 n) (div2 (S n)))) (iff (odd n) (eq nat (S (div2 n)) (div2 (S n))))); -!n:nat.!m:nat.!p:nat.(eq nat (minus n m) (minus (plus p n) (plus p m))); -!a:Z.!n:nat.(eq Z (Exp a (pred (S n))) (Exp a n)); -!a:Z.!x:Z.(eq Z (ZExp a (Zminus (Zplus x (POS xH)) (POS xH))) (ZExp a x)); -!p:nat.!a:Z.(Prime p)->(not (Mod a ZERO p))->(allex p (until (pred p)) (mapmult a (until (pred p)))); -!a:Z.!n:nat.(eq Z (zproduct (mapmult a (until n))) (Zmult (Exp a n) (zproduct (until n)))); -!p:nat.!a:Z.(Prime p)->(not (Mod a ZERO p))->(permmod p (until (pred p)) (mapmult a (until (pred p)))); -!p:nat.(Prime p)->(not (Mod (zproduct (until (pred p))) ZERO p)); -!p:nat.!n:nat.(lt O n)->(lt n p)->(Prime p)->(not (Mod (zproduct (until n)) ZERO p)); -!p:positive.(eq nat (convert (xI p)) (S (mult (S (S O)) (convert p)))); -!a:ad.(eq nat (nat_of_ad (ad_double_plus_un a)) (S (mult (S (S O)) (nat_of_ad a)))); -!p:positive.!a:ad.(eq bool (ad_bit (ad_xor (ad_x (xI p)) a) O) (negb (ad_bit a O))); -!r:R.(and (Rle (IZR (Int_part r)) r) (Rgt (Rminus (IZR (Int_part r)) r) (Ropp R1))); -!eps:R.(Rgt eps R0)->(Rlt (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))) eps); -!x:Z.(Zge x ZERO)->(Zodd x)->(eq Z x (Zplus (Zmult (POS (xO xH)) (Zdiv2 x)) (POS xH))); -!v:Z.!l1:Z.!l2:Z.!x:positive.(eq Z (Zplus (Zplus (Zmult v (POS x)) l1) (Zplus (Zmult v (NEG x)) l2)) (Zplus l1 l2)); -!v:Z.!l1:Z.!l2:Z.!x:positive.(eq Z (Zplus (Zplus (Zmult v (NEG x)) l1) (Zplus (Zmult v (POS x)) l2)) (Zplus l1 l2)); -!p:positive.(and (Zle (two_p (log_inf p)) (POS p)) (Zlt (POS p) (two_p (Zs (log_inf p))))); -!x:positive.(and (Zlt (two_p (Zpred (log_sup x))) (POS x)) (Zle (POS x) (two_p (log_sup x)))); -!n:nat.!x:positive.(eq Z (POS (shift_nat n x)) (Zmult (Zpower_nat (POS (xO xH)) n) (POS x))); -!p:positive.!x:positive.(eq Z (POS (shift_pos p x)) (Zmult (Zpower_pos (POS (xO xH)) p) (POS x))); -!U:redexes.!V:redexes.!k:nat.!p:nat.!n:nat.(eq redexes (lift_rec_r (subst_rec_r V U p) (plus p n) k) (subst_rec_r (lift_rec_r V (S (plus p n)) k) (lift_rec_r U n k) p)); -!U:redexes.!V:redexes.!W:redexes.!n:nat.!p:nat.(eq redexes (subst_rec_r (subst_rec_r V U p) W (plus p n)) (subst_rec_r (subst_rec_r V W (S (plus p n))) (subst_rec_r U W n) p)); -!v:BV.(eq nat (BV_to_nat (appbv (BV_increment v) (consbv (BV_increment_carry v) nilbv))) (S (BV_to_nat v))); -!l:BV.!n:BV.(eq nat (BV_to_nat (appbv l n)) (plus (BV_to_nat l) (mult (power2 (lengthbv l)) (BV_to_nat n)))); -!x:Z.(Zle ZERO x)->(eq Z (Zdiv2 (Zplus (Zmult (POS (xO xH)) x) (POS xH))) x); -!n:Z.(Zle (POS xH) n)->(Zle ZERO (Zplus (Zdiv2 (Zminus n (POS (xO xH)))) (POS xH))); diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml deleted file mode 100644 index 06ef93ab5..000000000 --- a/helm/gTopLevel/topLevel/topLevel.ml +++ /dev/null @@ -1,202 +0,0 @@ -let connection_param = "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" - -let show_queries = ref false - -let use_db = ref true - -let db_down = ref true - -let nl = "

\n" - -let check_db () = - if ! db_down then - if ! use_db then begin Mqint.init connection_param; db_down := false; true end - else begin print_endline "Not issuing in restricted mode"; false end - else true - -let default_confirm q = - let module Util = MQueryUtil in - if ! show_queries then Util.text_of_query print_string 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 - let dom,mk_term = - CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf - in - match dom with - [] -> terms := (snd (mk_term (function _ -> None))) :: !terms - | _ -> assert false - 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.Constant (_, _, 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 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 - Util.text_of_result print_string (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 - Util.text_of_result print_string (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 - - - - -(* FG: Mettere a posto qui. - let list_of_must,can = MQueryLevels.out_restr [] [] term in - let len = List.length list_of_must in - let must = if level < len then List.nth list_of_must level else can in -*) - - let r = [] (* FG e anche qui: Gen.searchPattern must can *) 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); - Util.text_of_result print_string 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 -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 - | ("-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 - 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 -- 2.39.2