From 795c7a7a2f45650204e6d5a5974a0eedec6af7af Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 5 Sep 2002 13:39:08 +0000 Subject: [PATCH] some small improvements: command line sintax changed, -MB added --- helm/gTopLevel/topLevel/Makefile | 2 +- helm/gTopLevel/topLevel/Readme | 14 ++-- helm/gTopLevel/topLevel/esempi.cic | 125 ++++++++++++++++++++++++++++ helm/gTopLevel/topLevel/topLevel.ml | 84 +++++++++++++------ 4 files changed, 194 insertions(+), 31 deletions(-) create mode 100644 helm/gTopLevel/topLevel/esempi.cic diff --git a/helm/gTopLevel/topLevel/Makefile b/helm/gTopLevel/topLevel/Makefile index e0af8f6ed..01dd0e173 100644 --- a/helm/gTopLevel/topLevel/Makefile +++ b/helm/gTopLevel/topLevel/Makefile @@ -1,5 +1,5 @@ BIN_DIR = /usr/local/bin -REQUIRES = helm-cic_textual_parser helm-cic_proof_checking helm-mathql helm-mathql_interpreter +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) diff --git a/helm/gTopLevel/topLevel/Readme b/helm/gTopLevel/topLevel/Readme index a59bba799..1607e5d83 100644 --- a/helm/gTopLevel/topLevel/Readme +++ b/helm/gTopLevel/topLevel/Readme @@ -6,10 +6,12 @@ L'input puo' contenere piu' di un termine CIC (usare ; per separare). Sintassi: topLevel -Opzioni : -locate : invocazione do Locate - -backward : invocazione di Backward - -show : mostra solo i termini CIC nell'input - -test : mostra l'attribuzione dei livelli per - la backward, ma non la esegue +Opzioni : -display : mostra solo i termini CIC nell'input + -typeof : mostra il tipo dell'oggetto indicato + non riconosce tipi induttivi e prove incomplete + -levels : mostra l'attribuzione dei livelli + -locate : invocazione di Locate + -backward : invocazione di Backward + -mbackward : invoca le Backward con indice da a 0 -le opzioni si possono anche scrivere -l -b -s e -t \ No newline at end of file +le opzioni si possono anche scrivere -d -t -l -L -B e -MB nell'ordine. diff --git a/helm/gTopLevel/topLevel/esempi.cic b/helm/gTopLevel/topLevel/esempi.cic new file mode 100644 index 000000000..38e5f3333 --- /dev/null +++ b/helm/gTopLevel/topLevel/esempi.cic @@ -0,0 +1,125 @@ +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 index 216639399..32ae4d1cb 100644 --- a/helm/gTopLevel/topLevel/topLevel.ml +++ b/helm/gTopLevel/topLevel/topLevel.ml @@ -3,14 +3,30 @@ let get_terms () = let lexbuf = Lexing.from_channel stdin in try while true do - match CicTextualParser.main CicTextualLexer.token lexbuf with - | None -> () - | Some expr -> terms := expr :: ! terms + 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 locate name = print_endline (MQueryGenerator.locate name); flush stdout @@ -22,44 +38,64 @@ let rec display = function print_endline ("? " ^ CicPp.ppterm term ^ "

"); flush stdout -let rec levels level = function +let rec levels = function | [] -> () | term :: tail -> - levels level tail; + levels tail; print_endline ("? " ^ CicPp.ppterm term ^ "

"); - print_endline (MQueryGenerator.levels [] [] term level); + print_endline (MQueryGenerator.levels [] [] term); flush stdout -let rec backward level = function - | [] -> () - | term :: tail -> - backward level tail; - print_endline ("? " ^ CicPp.ppterm term ^ "

"); - print_endline (MQueryGenerator.backward [] [] term level); - flush stdout - +let mbackward n m l = + let queries = ref [] in + let issue query = + if List.mem query ! queries then false + else begin queries := query :: ! queries; true end + in + let rec backward level = function + | [] -> () + | term :: tail -> + backward level tail; + print_endline ("? " ^ CicPp.ppterm term ^ "

"); + print_endline (MQueryGenerator.backward [] [] term level); + flush stdout + in + MQueryGenerator.call_back issue; + 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"); + MQueryGenerator.call_back (fun _ -> true) + let parse_args () = let rec parse = function | [] -> () - | ("-l"|"-locate") :: arg :: rem -> - locate arg; parse rem - | ("-d"|"-display") :: rem -> - display (get_terms ()) - | ("-t"|"-test") :: arg :: rem -> - levels (int_of_string arg) (get_terms ()) - | ("-b"|"-backward") :: arg :: rem -> - backward (int_of_string arg) (get_terms ()) + | ("-d"|"-display") :: rem -> display (get_terms ()) + | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem + | ("-l"|"-levels") :: rem -> levels (get_terms ()) + | ("-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"|"-mbackward") :: 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 _ = - CicCooking.init () ; + CicCooking.init () ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(function s -> print_string s ; flush stdout)) ; MQueryGenerator.init (); parse_args (); MQueryGenerator.close (); + prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^ + " seconds"); exit 0 -;; -- 2.39.2