--- /dev/null
+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)));
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
print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
flush stdout
-let rec levels level = function
+let rec levels = function
| [] -> ()
| term :: tail ->
- levels level tail;
+ levels tail;
print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
- 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 ^ "<p>");
- 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 ^ "<p>");
+ 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
-;;
projects / helm.git / commitdiff