mirror of
https://github.com/gryf/tagbar.git
synced 2026-02-14 12:55:48 +01:00
Add tests to repository
This commit is contained in:
Jan Larres
98
tests/ocaml/fifteen.ml
Normal file
98
tests/ocaml/fifteen.ml
Normal file
@@ -0,0 +1,98 @@
|
||||
(* $Id: fifteen.ml,v 1.8 2001/09/06 08:47:55 garrigue Exp $ *)
|
||||
|
||||
open StdLabels
|
||||
open Gaux
|
||||
open Gtk
|
||||
open GObj
|
||||
open GMain
|
||||
|
||||
class position ~init_x ~init_y ~min_x ~min_y ~max_x ~max_y = object
|
||||
val mutable x = init_x
|
||||
val mutable y = init_y
|
||||
method current = (x, y)
|
||||
method up () = if y > min_y then y <- y-1 else (); (x, y)
|
||||
method down () = if y < max_y then y <- y+1 else (); (x, y)
|
||||
method left () = if x > min_x then x <- x-1 else (); (x, y)
|
||||
method right () = if x < max_x then x <- x+1 else (); (x, y)
|
||||
end
|
||||
|
||||
let game_init () = (* generate initial puzzle state *)
|
||||
let rec game_aux acc rest n_invert =
|
||||
let len = List.length rest in
|
||||
if len=0 then
|
||||
if n_invert mod 2 = 0 then
|
||||
acc (* to be solvable, n_invert must be even *)
|
||||
else
|
||||
(List.hd (List.tl acc))::(List.hd acc)::(List.tl (List.tl acc))
|
||||
else begin
|
||||
let rec extract n xs =
|
||||
if (n=0) then (List.hd xs, List.tl xs)
|
||||
else
|
||||
let (ans, ys) = extract (n-1) (List.tl xs) in
|
||||
(ans, List.hd xs :: ys) in
|
||||
let ran = Random.int len in
|
||||
let (elm, rest1) = extract ran rest in
|
||||
let rec count p xs = match xs with
|
||||
[] -> 0
|
||||
| y :: ys -> let acc = count p ys in
|
||||
if p y then 1+acc else acc
|
||||
in
|
||||
let new_n_invert = count (fun x -> elm > x) acc in
|
||||
game_aux (elm :: acc) rest1 (n_invert+new_n_invert)
|
||||
end in
|
||||
let rec from n = if n=0 then [] else n :: from (n-1) in
|
||||
game_aux [] (from 15) 0
|
||||
|
||||
let _ = Random.init (int_of_float (Sys.time () *. 1000.))
|
||||
let window = GWindow.window ()
|
||||
let _ = window#connect#destroy ~callback:GMain.Main.quit
|
||||
|
||||
let tbl = GPack.table ~rows:4 ~columns:4 ~homogeneous:true ~packing:window#add ()
|
||||
let dummy = GMisc.label ~text:"" ~packing:(tbl#attach ~left:3 ~top:3) ()
|
||||
let arr = Array.create_matrix ~dimx:4 ~dimy:4 dummy
|
||||
let init = game_init ()
|
||||
let _ =
|
||||
for i = 0 to 15 do
|
||||
let j = i mod 4 in
|
||||
let k = i/4 in
|
||||
let frame =
|
||||
GBin.frame ~shadow_type:`OUT ~width:32 ~height:32
|
||||
~packing:(tbl#attach ~left:j ~top:k) () in
|
||||
if i < 15 then
|
||||
arr.(j).(k) <-
|
||||
GMisc.label ~text:(string_of_int (List.nth init i))
|
||||
~packing:frame#add ()
|
||||
done
|
||||
let pos = new position ~init_x:3 ~init_y:3 ~min_x:0 ~min_y:0 ~max_x:3 ~max_y:3
|
||||
|
||||
open GdkKeysyms
|
||||
|
||||
let _ =
|
||||
window#event#connect#key_press ~callback:
|
||||
begin fun ev ->
|
||||
let (x0, y0) = pos#current in
|
||||
let wid0 = arr.(x0).(y0) in
|
||||
let key = GdkEvent.Key.keyval ev in
|
||||
if key = _q || key = _Escape then (Main.quit (); exit 0) else
|
||||
let (x1, y1) =
|
||||
if key = _h || key = _Left then
|
||||
pos#right ()
|
||||
else if key = _j || key = _Down then
|
||||
pos#up ()
|
||||
else if key = _k || key = _Up then
|
||||
pos#down ()
|
||||
else if key = _l || key = _Right then
|
||||
pos#left ()
|
||||
else (x0, y0)
|
||||
in
|
||||
let wid1 = arr.(x1).(y1) in
|
||||
wid0#set_text (wid1#text);
|
||||
wid1#set_text "";
|
||||
true
|
||||
end
|
||||
|
||||
let main () =
|
||||
window#show ();
|
||||
Main.main ()
|
||||
|
||||
let _ = main ()
|
||||
153
tests/ocaml/heap.ml
Normal file
153
tests/ocaml/heap.ml
Normal file
@@ -0,0 +1,153 @@
|
||||
(************************************************************************)
|
||||
(* v * The Coq Proof Assistant / The Coq Development Team *)
|
||||
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
|
||||
(* \VV/ **************************************************************)
|
||||
(* // * This file is distributed under the terms of the *)
|
||||
(* * GNU Lesser General Public License Version 2.1 *)
|
||||
(************************************************************************)
|
||||
|
||||
(* $Id$ *)
|
||||
|
||||
(*s Heaps *)
|
||||
|
||||
module type Ordered = sig
|
||||
type t
|
||||
val compare : t -> t -> int
|
||||
end
|
||||
|
||||
module type S =sig
|
||||
|
||||
(* Type of functional heaps *)
|
||||
type t
|
||||
|
||||
(* Type of elements *)
|
||||
type elt
|
||||
|
||||
(* The empty heap *)
|
||||
val empty : t
|
||||
|
||||
(* [add x h] returns a new heap containing the elements of [h], plus [x];
|
||||
complexity $O(log(n))$ *)
|
||||
val add : elt -> t -> t
|
||||
|
||||
(* [maximum h] returns the maximum element of [h]; raises [EmptyHeap]
|
||||
when [h] is empty; complexity $O(1)$ *)
|
||||
val maximum : t -> elt
|
||||
|
||||
(* [remove h] returns a new heap containing the elements of [h], except
|
||||
the maximum of [h]; raises [EmptyHeap] when [h] is empty;
|
||||
complexity $O(log(n))$ *)
|
||||
val remove : t -> t
|
||||
|
||||
(* usual iterators and combinators; elements are presented in
|
||||
arbitrary order *)
|
||||
val iter : (elt -> unit) -> t -> unit
|
||||
|
||||
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
|
||||
|
||||
end
|
||||
|
||||
exception EmptyHeap
|
||||
|
||||
(*s Functional implementation *)
|
||||
|
||||
module Functional(X : Ordered) = struct
|
||||
|
||||
(* Heaps are encoded as complete binary trees, i.e., binary trees
|
||||
which are full expect, may be, on the bottom level where it is filled
|
||||
from the left.
|
||||
These trees also enjoy the heap property, namely the value of any node
|
||||
is greater or equal than those of its left and right subtrees.
|
||||
|
||||
There are 4 kinds of complete binary trees, denoted by 4 constructors:
|
||||
[FFF] for a full binary tree (and thus 2 full subtrees);
|
||||
[PPF] for a partial tree with a partial left subtree and a full
|
||||
right subtree;
|
||||
[PFF] for a partial tree with a full left subtree and a full right subtree
|
||||
(but of different heights);
|
||||
and [PFP] for a partial tree with a full left subtree and a partial
|
||||
right subtree. *)
|
||||
|
||||
type t =
|
||||
| Empty
|
||||
| FFF of t * X.t * t (* full (full, full) *)
|
||||
| PPF of t * X.t * t (* partial (partial, full) *)
|
||||
| PFF of t * X.t * t (* partial (full, full) *)
|
||||
| PFP of t * X.t * t (* partial (full, partial) *)
|
||||
|
||||
type elt = X.t
|
||||
|
||||
let empty = Empty
|
||||
|
||||
(* smart constructors for insertion *)
|
||||
let p_f l x r = match l with
|
||||
| Empty | FFF _ -> PFF (l, x, r)
|
||||
| _ -> PPF (l, x, r)
|
||||
|
||||
let pf_ l x = function
|
||||
| Empty | FFF _ as r -> FFF (l, x, r)
|
||||
| r -> PFP (l, x, r)
|
||||
|
||||
let rec add x = function
|
||||
| Empty ->
|
||||
FFF (Empty, x, Empty)
|
||||
(* insertion to the left *)
|
||||
| FFF (l, y, r) | PPF (l, y, r) ->
|
||||
if X.compare x y > 0 then p_f (add y l) x r else p_f (add x l) y r
|
||||
(* insertion to the right *)
|
||||
| PFF (l, y, r) | PFP (l, y, r) ->
|
||||
if X.compare x y > 0 then pf_ l x (add y r) else pf_ l y (add x r)
|
||||
|
||||
let maximum = function
|
||||
| Empty -> raise EmptyHeap
|
||||
| FFF (_, x, _) | PPF (_, x, _) | PFF (_, x, _) | PFP (_, x, _) -> x
|
||||
|
||||
(* smart constructors for removal; note that they are different
|
||||
from the ones for insertion! *)
|
||||
let p_f l x r = match l with
|
||||
| Empty | FFF _ -> FFF (l, x, r)
|
||||
| _ -> PPF (l, x, r)
|
||||
|
||||
let pf_ l x = function
|
||||
| Empty | FFF _ as r -> PFF (l, x, r)
|
||||
| r -> PFP (l, x, r)
|
||||
|
||||
let rec remove = function
|
||||
| Empty ->
|
||||
raise EmptyHeap
|
||||
| FFF (Empty, _, Empty) ->
|
||||
Empty
|
||||
| PFF (l, _, Empty) ->
|
||||
l
|
||||
(* remove on the left *)
|
||||
| PPF (l, x, r) | PFF (l, x, r) ->
|
||||
let xl = maximum l in
|
||||
let xr = maximum r in
|
||||
let l' = remove l in
|
||||
if X.compare xl xr >= 0 then
|
||||
p_f l' xl r
|
||||
else
|
||||
p_f l' xr (add xl (remove r))
|
||||
(* remove on the right *)
|
||||
| FFF (l, x, r) | PFP (l, x, r) ->
|
||||
let xl = maximum l in
|
||||
let xr = maximum r in
|
||||
let r' = remove r in
|
||||
if X.compare xl xr > 0 then
|
||||
pf_ (add xr (remove l)) xl r'
|
||||
else
|
||||
pf_ l xr r'
|
||||
|
||||
let rec iter f = function
|
||||
| Empty ->
|
||||
()
|
||||
| FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) ->
|
||||
iter f l; f x; iter f r
|
||||
|
||||
let rec fold f h x0 = match h with
|
||||
| Empty ->
|
||||
x0
|
||||
| FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) ->
|
||||
fold f l (fold f r (f x x0))
|
||||
|
||||
end
|
||||
294
tests/ocaml/kb.ml
Normal file
294
tests/ocaml/kb.ml
Normal file
@@ -0,0 +1,294 @@
|
||||
(* ========================================================================= *)
|
||||
(* Knuth-Bendix completion done by HOL inference. John Harrison 2005 *)
|
||||
(* *)
|
||||
(* This was written by fairly mechanical modification of the code at *)
|
||||
(* *)
|
||||
(* http://www.cl.cam.ac.uk/users/jrh/atp/order.ml *)
|
||||
(* http://www.cl.cam.ac.uk/users/jrh/atp/completion.ml *)
|
||||
(* *)
|
||||
(* for HOL's slightly different term structure, with ad hoc term *)
|
||||
(* manipulations replaced by inference on equational theorems. We also have *)
|
||||
(* the optimization of throwing left-reducible rules back into the set of *)
|
||||
(* critical pairs. However, we don't prioritize smaller critical pairs or *)
|
||||
(* anything like that; this is still a very naive implementation. *)
|
||||
(* *)
|
||||
(* For something very similar done 15 years ago, see Konrad Slind's Master's *)
|
||||
(* thesis: "An Implementation of Higher Order Logic", U Calgary 1991. *)
|
||||
(* ========================================================================= *)
|
||||
|
||||
let is_realvar w x = is_var x & not(mem x w);;
|
||||
|
||||
let rec real_strip w tm =
|
||||
if mem tm w then tm,[] else
|
||||
let l,r = dest_comb tm in
|
||||
let f,args = real_strip w l in f,args@[r];;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Construct a weighting function. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let weight lis (f,n) (g,m) =
|
||||
let i = index f lis and j = index g lis in
|
||||
i > j or i = j & n > m;;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Generic lexicographic ordering function. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let rec lexord ord l1 l2 =
|
||||
match (l1,l2) with
|
||||
(h1::t1,h2::t2) -> if ord h1 h2 then length t1 = length t2
|
||||
else h1 = h2 & lexord ord t1 t2
|
||||
| _ -> false;;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Lexicographic path ordering. Note that we also use the weights *)
|
||||
(* to define the set of constants, so they don't literally have to be *)
|
||||
(* constants in the HOL sense. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let rec lpo_gt w s t =
|
||||
if is_realvar w t then not(s = t) & mem t (frees s)
|
||||
else if is_realvar w s or is_abs s or is_abs t then false else
|
||||
let f,fargs = real_strip w s and g,gargs = real_strip w t in
|
||||
exists (fun si -> lpo_ge w si t) fargs or
|
||||
forall (lpo_gt w s) gargs &
|
||||
(f = g & lexord (lpo_gt w) fargs gargs or
|
||||
weight w (f,length fargs) (g,length gargs))
|
||||
and lpo_ge w s t = (s = t) or lpo_gt w s t;;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Unification. Again we have the weights "w" fixing the set of constants. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let rec istriv w env x t =
|
||||
if is_realvar w t then t = x or defined env t & istriv w env x (apply env t)
|
||||
else if is_const t then false else
|
||||
let f,args = strip_comb t in
|
||||
exists (istriv w env x) args & failwith "cyclic";;
|
||||
|
||||
let rec unify w env tp =
|
||||
match tp with
|
||||
((Var(_,_) as x),t) | (t,(Var(_,_) as x)) when not(mem x w) ->
|
||||
if defined env x then unify w env (apply env x,t)
|
||||
else if istriv w env x t then env else (x|->t) env
|
||||
| (Comb(f,x),Comb(g,y)) -> unify w (unify w env (x,y)) (f,g)
|
||||
| (s,t) -> if s = t then env else failwith "unify: not unifiable";;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Full unification, unravelling graph into HOL-style instantiation list. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let fullunify w (s,t) =
|
||||
let env = unify w undefined (s,t) in
|
||||
let th = map (fun (x,t) -> (t,x)) (graph env) in
|
||||
let rec subs t =
|
||||
let t' = vsubst th t in
|
||||
if t' = t then t else subs t' in
|
||||
map (fun (t,x) -> (subs t,x)) th;;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Construct "overlaps": ways of rewriting subterms using unification. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let LIST_MK_COMB f ths = rev_itlist (fun s t -> MK_COMB(t,s)) ths (REFL f);;
|
||||
|
||||
let rec listcases fn rfn lis acc =
|
||||
match lis with
|
||||
[] -> acc
|
||||
| h::t -> fn h (fun i h' -> rfn i (h'::map REFL t)) @
|
||||
listcases fn (fun i t' -> rfn i (REFL h::t')) t acc;;
|
||||
|
||||
let rec overlaps w th tm rfn =
|
||||
let l,r = dest_eq(concl th) in
|
||||
if not (is_comb tm) then [] else
|
||||
let f,args = strip_comb tm in
|
||||
listcases (overlaps w th) (fun i a -> rfn i (LIST_MK_COMB f a)) args
|
||||
(try [rfn (fullunify w (l,tm)) th] with Failure _ -> []);;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Rename variables canonically to avoid clashes or remove redundancy. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let fixvariables s th =
|
||||
let fvs = subtract (frees(concl th)) (freesl(hyp th)) in
|
||||
let gvs = map2 (fun v n -> mk_var(s^string_of_int n,type_of v))
|
||||
fvs (1--(length fvs)) in
|
||||
INST (zip gvs fvs) th;;
|
||||
|
||||
let renamepair (th1,th2) = fixvariables "x" th1,fixvariables "y" th2;;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Find all critical pairs. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let crit1 w eq1 eq2 =
|
||||
let l1,r1 = dest_eq(concl eq1)
|
||||
and l2,r2 = dest_eq(concl eq2) in
|
||||
overlaps w eq1 l2 (fun i th -> TRANS (SYM(INST i th)) (INST i eq2));;
|
||||
|
||||
let thm_union l1 l2 =
|
||||
itlist (fun th ths -> let th' = fixvariables "x" th in
|
||||
let tm = concl th' in
|
||||
if exists (fun th'' -> concl th'' = tm) ths then ths
|
||||
else th'::ths)
|
||||
l1 l2;;
|
||||
|
||||
let critical_pairs w tha thb =
|
||||
let th1,th2 = renamepair (tha,thb) in
|
||||
if concl th1 = concl th2 then crit1 w th1 th2 else
|
||||
filter (fun th -> let l,r = dest_eq(concl th) in l <> r)
|
||||
(thm_union (crit1 w th1 th2) (thm_union (crit1 w th2 th1) []));;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Normalize an equation and try to orient it. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let normalize_and_orient w eqs th =
|
||||
let th' = GEN_REWRITE_RULE TOP_DEPTH_CONV eqs th in
|
||||
let s',t' = dest_eq(concl th') in
|
||||
if lpo_ge w s' t' then th' else if lpo_ge w t' s' then SYM th'
|
||||
else failwith "Can't orient equation";;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Print out status report to reduce user boredom. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let status(eqs,crs) eqs0 =
|
||||
if eqs = eqs0 & (length crs) mod 1000 <> 0 then () else
|
||||
(print_string(string_of_int(length eqs)^" equations and "^
|
||||
string_of_int(length crs)^" pending critical pairs");
|
||||
print_newline());;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Basic completion, throwing back left-reducible rules. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let left_reducible eqs eq =
|
||||
can (CHANGED_CONV(GEN_REWRITE_CONV (LAND_CONV o ONCE_DEPTH_CONV) eqs))
|
||||
(concl eq);;
|
||||
|
||||
let rec complete w (eqs,crits) =
|
||||
match crits with
|
||||
(eq::ocrits) ->
|
||||
let trip =
|
||||
try let eq' = normalize_and_orient w eqs eq in
|
||||
let s',t' = dest_eq(concl eq') in
|
||||
if s' = t' then (eqs,ocrits) else
|
||||
let crits',eqs' = partition(left_reducible [eq']) eqs in
|
||||
let eqs'' = eq'::eqs' in
|
||||
eqs'',
|
||||
ocrits @ crits' @ itlist ((@) o critical_pairs w eq') eqs'' []
|
||||
with Failure _ ->
|
||||
if exists (can (normalize_and_orient w eqs)) ocrits
|
||||
then (eqs,ocrits@[eq])
|
||||
else failwith "complete: no orientable equations" in
|
||||
status trip eqs; complete w trip
|
||||
| [] -> eqs;;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Overall completion. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let complete_equations wts eqs =
|
||||
let eqs' = map (normalize_and_orient wts []) eqs in
|
||||
complete wts ([],eqs');;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Knuth-Bendix example 4: the inverse property. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
complete_equations [`1`; `(*):num->num->num`; `i:num->num`]
|
||||
[SPEC_ALL(ASSUME `!a b. i(a) * a * b = b`)];;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Knuth-Bendix example 6: central groupoids. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
complete_equations [`(*):num->num->num`]
|
||||
[SPEC_ALL(ASSUME `!a b c. (a * b) * (b * c) = b`)];;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Knuth-Bendix example 9: cancellation law. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
complete_equations
|
||||
[`1`; `( * ):num->num->num`; `(+):num->num->num`; `(-):num->num->num`]
|
||||
(map SPEC_ALL (CONJUNCTS (ASSUME
|
||||
`(!a b:num. a - a * b = b) /\
|
||||
(!a b:num. a * b - b = a) /\
|
||||
(!a. a * 1 = a) /\
|
||||
(!a. 1 * a = a)`)));;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Another example: pure congruence closure (no variables). *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
complete_equations [`c:A`; `f:A->A`]
|
||||
(map SPEC_ALL (CONJUNCTS (ASSUME
|
||||
`((f(f(f(f(f c))))) = c:A) /\ (f(f(f c)) = c)`)));;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Knuth-Bendix example 1: group theory. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let eqs = map SPEC_ALL (CONJUNCTS (ASSUME
|
||||
`(!x. 1 * x = x) /\ (!x. i(x) * x = 1) /\
|
||||
(!x y z. (x * y) * z = x * y * z)`));;
|
||||
|
||||
complete_equations [`1`; `(*):num->num->num`; `i:num->num`] eqs;;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Near-rings (from Aichinger's Diplomarbeit). *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let eqs = map SPEC_ALL (CONJUNCTS (ASSUME
|
||||
`(!x. 0 + x = x) /\
|
||||
(!x. neg x + x = 0) /\
|
||||
(!x y z. (x + y) + z = x + y + z) /\
|
||||
(!x y z. (x * y) * z = x * y * z) /\
|
||||
(!x y z. (x + y) * z = (x * z) + (y * z))`));;
|
||||
|
||||
let nreqs =
|
||||
complete_equations
|
||||
[`0`; `(+):num->num->num`; `neg:num->num`; `( * ):num->num->num`] eqs;;
|
||||
|
||||
(*** This weighting also works OK, though the system is a bit bigger
|
||||
|
||||
let nreqs =
|
||||
complete_equations
|
||||
[`0`; `(+):num->num->num`; `( * ):num->num->num`; `INV`] eqs;;
|
||||
|
||||
****)
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* A "completion" tactic. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let COMPLETE_TAC w th =
|
||||
let eqs = map SPEC_ALL (CONJUNCTS(SPEC_ALL th)) in
|
||||
let eqs' = complete_equations w eqs in
|
||||
MAP_EVERY (ASSUME_TAC o GEN_ALL) eqs';;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Solve example problems in gr *)
|
||||
|
||||
g `(!x. 1 * x = x) /\
|
||||
(!x. i(x) * x = 1) /\
|
||||
(!x y z. (x * y) * z = x * y * z)
|
||||
==> !x y. i(y) * i(i(i(x * i(y)))) * x = 1`;;
|
||||
|
||||
e (DISCH_THEN(COMPLETE_TAC [`1`; `(*):num->num->num`; `i:num->num`]));;
|
||||
e (ASM_REWRITE_TAC[]);;
|
||||
|
||||
g `(!x. 0 + x = x) /\
|
||||
(!x. neg x + x = 0) /\
|
||||
(!x y z. (x + y) + z = x + y + z) /\
|
||||
(!x y z. (x * y) * z = x * y * z) /\
|
||||
(!x y z. (x + y) * z = (x * z) + (y * z))
|
||||
==> (neg 0 * (x * y + z + neg(neg(w + z))) + neg(neg b + neg a) =
|
||||
a + b)`;;
|
||||
|
||||
e (DISCH_THEN(COMPLETE_TAC
|
||||
[`0`; `(+):num->num->num`; `neg:num->num`; `( * ):num->num->num`]));;
|
||||
e (ASM_REWRITE_TAC[]);;
|
||||
82
tests/ocaml/xmlParser.mli
Normal file
82
tests/ocaml/xmlParser.mli
Normal file
@@ -0,0 +1,82 @@
|
||||
(*
|
||||
* Xml Light, an small Xml parser/printer with DTD support.
|
||||
* Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
|
||||
*
|
||||
* This library is free software; you can redistribute it and/or
|
||||
* modify it under the terms of the GNU Lesser General Public
|
||||
* License as published by the Free Software Foundation; either
|
||||
* version 2.1 of the License, or (at your option) any later version.
|
||||
*
|
||||
* This library has the special exception on linking described in file
|
||||
* README.
|
||||
*
|
||||
* This library 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
|
||||
* Lesser General Public License for more details.
|
||||
*
|
||||
* You should have received a copy of the GNU Lesser General Public
|
||||
* License along with this library; if not, write to the Free Software
|
||||
* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston,
|
||||
* MA 02110-1301 USA
|
||||
*)
|
||||
|
||||
(** Xml Light Parser
|
||||
|
||||
While basic parsing functions can be used in the {!Xml} module, this module
|
||||
is providing a way to create, configure and run an Xml parser.
|
||||
|
||||
*)
|
||||
|
||||
(** Abstract type for an Xml parser. *)
|
||||
type t
|
||||
|
||||
(** Several kind of resources can contain Xml documents. *)
|
||||
type source =
|
||||
| SFile of string
|
||||
| SChannel of in_channel
|
||||
| SString of string
|
||||
| SLexbuf of Lexing.lexbuf
|
||||
|
||||
(** This function returns a new parser with default options. *)
|
||||
val make : unit -> t
|
||||
|
||||
(** This function enable or disable automatic DTD proving with the parser.
|
||||
Note that Xml documents having no reference to a DTD are never proved
|
||||
when parsed (but you can prove them later using the {!Dtd} module
|
||||
{i (by default, prove is true)}. *)
|
||||
val prove : t -> bool -> unit
|
||||
|
||||
(** When parsing an Xml document from a file using the {!Xml.parse_file}
|
||||
function, the DTD file if declared by the Xml document has to be in the
|
||||
same directory as the xml file. When using other parsing functions,
|
||||
such as on a string or on a channel, the parser will raise everytime
|
||||
{!Xml.File_not_found} if a DTD file is needed and prove enabled. To enable
|
||||
the DTD loading of the file, the user have to configure the Xml parser
|
||||
with a [resolve] function which is taking as argument the DTD filename and
|
||||
is returning a checked DTD. The user can then implement any kind of DTD
|
||||
loading strategy, and can use the {!Dtd} module functions to parse and check
|
||||
the DTD file {i (by default, the resolve function is raising}
|
||||
{!Xml.File_not_found}). *)
|
||||
val resolve : t -> (string -> Dtd.checked) -> unit
|
||||
|
||||
(** When a Xml document is parsed, the parser will check that the end of the
|
||||
document is reached, so for example parsing ["<A/><B/>"] will fail instead
|
||||
of returning only the A element. You can turn off this check by setting
|
||||
[check_eof] to [false] {i (by default, check_eof is true)}. *)
|
||||
val check_eof : t -> bool -> unit
|
||||
|
||||
(** Once the parser is configurated, you can run the parser on a any kind
|
||||
of xml document source to parse its contents into an Xml data structure. *)
|
||||
val parse : t -> source -> Xml.xml
|
||||
|
||||
(** When several PCData elements are separed by a \n (or \r\n), you can
|
||||
either split the PCData in two distincts PCData or merge them with \n
|
||||
as seperator into one PCData. The default behavior is to concat the
|
||||
PCData, but this can be changed for a given parser with this flag. *)
|
||||
val concat_pcdata : t -> bool -> unit
|
||||
|
||||
(**/**)
|
||||
|
||||
(* internal usage only... *)
|
||||
val _raises : (Xml.error_msg -> Lexing.lexbuf -> exn) -> (string -> exn) -> (Dtd.parse_error_msg -> Lexing.lexbuf -> exn) -> unit
|
||||
Reference in New Issue
Block a user